这有可能将C++代码转换为SMT2吗？

Question

我是新的SMT解决方案和这些主题。我需要将C++代码转换为相当于SMT2的代码(我有一个需要.smt2作为输入的工具)。我已经找到了this solution，但它并没有完全解释如何做到这一点？你能帮我吗？谢谢

while (x<y)
{
x=5*x+3; 
y=3*y+5; 
w=3*z+w; 
z=z+6;
}

这种转换有什么工具吗？或者我该如何了解这个话题？

Answer 1

如果您正在寻找一个可以将任意C++转换为SMTLib的工具，那么我不认为存在这样的工具，也不认为这样做是可行的，因为这意味着您需要使用SMTLib编码的C++非常精确的语义，这是一项艰巨的任务，如果不是不可能的话。

如果你关心一个有限的子集，或者只想手动翻译一个或两个具体的例子，那么你找到的答案是最好的。首先研究SMTLib本身，然后查找SSA (单静态赋值)。循环将是困难的，但有方法来处理它们。再说一遍，这完全取决于你到底在努力实现什么。一旦你看了这些选项，也许你可以问一个更具体的问题。