Z3与字符串表达式(Z3 with string expressions)

我试图用Z3，以确定是否一个表达式是满足的。我可以很容易地通过定义范围内，则int_const变量和公式做到这一点。为了评估一个表达式编程，你会写代码的一切。比方说，在一个字符串形式的逻辑表达式给出，然后呢？例如，

“×==Ÿ&&！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

好吧，我可以写这个特殊配方的代码，但我怎么能做到这一点编程给出一个字符串。我愿意接受任何你能想到的。

谢谢：）

我看到下面的选项：

1）你可以实现自己的解析器，并调用Z3 API函数。优点：你可以用你的“最爱”语言编写公式。缺点：它是“忙”的工作。

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

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

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安装使用上面的脚本。