有沒有辦法使用SMT求解器來找出如何編寫函數？

Question

我是SMT解決者的初學者，我正在嘗試使用它們來實現程序合成的變體。無論如何，問題歸結爲找到一系列應用操作（先前定義的函數的組合），這些操作對於給定的輸入提供所請求的輸出。

是否有任何現有的使用SMT求解器來找出以何種順序編寫函數以達到特定輸出的做法？如果您有任何閱讀材料，我很樂意閱讀。

我開始使用Z3來完成任務，但如果有任何推理選擇其他SMT解算器，請拍！

謝謝。

Answer 1

您需要定義描述要應用哪些操作的常量。首先，根據要使用的操作來定義複合操作：

int operation; //constant, constrain it to [0, 2] 
Expr result = 
operation == 0 ? applyFunction0(inputExpr) : 
operation == 1 ? applyFunction1(inputExpr) : 
applyFunction2(inputExpr); 

非常粗略的僞代碼，用於構建什麼表達式。在Z3中，?:運算符映射到ITE。

這樣Z3可以找到合適的值operation挑選一個具體的操作。您可以從模型中獲得具體的值。

您可以迭代此方法以按順序應用多個操作。