我是SMT求解器的初学者，我正在尝试将它们用于程序综合的变体。无论如何，问题归结为找到一系列应用操作（先前定义的函数的组合），这些操作对于给定的输入给出所请求的输出。
是否存在使用SMT求解器来找出以哪种顺序组合功能以达到特定输出的现有做法？如果您有我的阅读材料，我很乐意阅读。
我开始使用Z3进行任务，但是如果有任何理由选择其他SMT求解器，请射击！
谢谢。
您需要定义描述要应用的操作的常量。首先，定义一个复合操作，该操作根据要使用的操作进行切换：
int operation; //constant, constrain it to [0, 2]
Expr result =
operation == 0 ? applyFunction0(inputExpr) :
operation == 1 ? applyFunction1(inputExpr) :
applyFunction2(inputExpr);
用于构建什么表达式的非常粗糙的伪代码。该?:操作映射到ITE在Z3。
这样，Z3可以找到一个合适的值operation来选择一个具体的操作。您可以从模型中获取具体值。
您可以迭代此方法以依次应用多个操作。
本文收集自互联网，转载请注明来源。
如有侵权，请联系[email protected] 删除。
我来说两句