Z3 带字符串表达式答案

【问题标题】：Z3 with string expressionsZ3 带字符串表达式
【发布时间】：2012-05-29 19:59:35
【问题描述】：

我正在尝试使用 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

好的，我可以为这个特定的公式编写代码，但是如果给定一个字符串，我怎么能以编程方式做到这一点。我对你能想到的任何事情都持开放态度。

谢谢你:)

【问题讨论】：

标签： string z3

【解决方案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，并使用 Python 中的 eval 函数解析字符串。这是一个例子：

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

【讨论】：