Z3 带有字符串表达式

Question

我正在尝试使用 Z3 来确定表达式是否可满足。我可以通过定义上下文然后定义 int_const 变量和公式来轻松地做到这一点。要以编程方式计算表达式，您必须用代码编写所有内容。假设逻辑表达式以字符串的形式给出，那么呢？例如，

“x == y &&！x == z”

在 C API 中将表示为：

context c;
expr x = c.int_const("x")
//Same for other variables
...
formula = (x == y) && (!x == z);
solver s(c);
s.add(formula);
//s.check() ...etc etc

好的，我可以为这个特定的公式编写代码，但是如何在给定字符串的情况下以编程方式执行此操作。我对你能想到的任何事情都持开放态度。

谢谢 ：）

Answer 1

我看到以下选项：

1）您可以实现自己的解析器，并调用Z3 API函数。优点：您可以使用您“最喜欢的”语言来编写公式。缺点：这是“忙碌”的工作。

2）您可以使用API Z3_parse_smtlib2_string​​。缺点：您的公式必须采用 SMT 2.0 格式。例如，您必须编写(and (= x y) (not (= x y)))而不是(x == y) && !(x == z).

3）您可以使用Z3 Python API，并使用evalPython中的函数解析字符串。这是一个例子：

from z3 import *
# Creating x, y 
x = Int('x')
y = Int('y')

# Creating the formula using Python
f = And(x == y, Not(x == y))
print f

# Using eval to parse the string.
s = "And(x == y, Not(x == y))"
f2 = eval(s)
print f2

顺便说一句，这个脚本在rise4fun http://rise4fun.com/z3py上不起作用，因为eval那里不允许使用该功能，但您可以在本地 Z3 安装中使用上面的脚本。