将c＃语句转换为z3格式

Question

我正在用c＃编写代码。

在代码中有各种IF条件。我想将这些条件传递给z3约束求解器，并检查它的可满足性并获得可以保证它的值。 （我在我的代码中进一步使用这些值）

如果我在代码中使用IF条件并在z3语法中编写其等效声明，那么它工作正常。但我想泛化的意思是在c＃中声明一个语句，我想用z3语法生成它的相应语句。

无论如何我能做到吗？

Answer 1

C＃语言不提供必要的挂钩，因此您可以在运行时检测到if语句的存在。你无法察觉的东西不能告诉Z3。

您可以使用Roslyn将包含C＃代码的字符串解析为AST并将其转换为Z3。对于简单的情况可能并不难。这为循环控制流程打破了。你可以使它适用于常见的非循环结构，如变量，运算符，if,switch。