带字符串表达式的 Z3 [英] Z3 with string expressions
问题描述
我正在尝试使用 Z3 来确定表达式是否可满足.我可以通过定义上下文,然后定义 int_const 变量和公式来轻松地做到这一点.要以编程方式计算表达式,您必须在代码中编写所有内容.假设逻辑表达式以字符串的形式给出,然后呢?例如,
I'm trying to use Z3 to determine if an expression is satisfiable. I could easily do this by defining the context then the int_const variables and the formula. To evaluate an expression programmatically you would have to write everything in code. Let's say the logical expression is given in the form of a string, what then? For example,
"x == y && !x == z"
"x == y && !x == z"
将在 C API 中表示为:
would be expressed in the C API as:
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
好的,我可以为这个特定的公式编写代码,但是给定一个字符串,我怎么能以编程方式做到这一点.我愿意接受你能想到的任何事情.
Okay, I can write the code for this particular formula, but how could I do that programmatically given a string. I'm open to anything you can think of.
谢谢:)
推荐答案
我看到以下选项:
1) 您可以实现自己的解析器,并调用 Z3 API 函数.优点:您可以使用最喜欢的"语言来编写公式.缺点:这是忙碌"的工作.
1) you can implement your own parser, and invoke the Z3 API functions. Pro: you can use your "favorite" language for writing formulas. Con: it is "busy" work.
2) 您可以使用 API Z3_parse_smtlib2_string
.缺点:您的公式必须采用 SMT 2.0 格式.例如,您必须编写 (and (= x y) (not (= x y)))
而不是 (x == y) &&!(x == z)
.
2) you can use the API Z3_parse_smtlib2_string
. Con: your formulas must be in SMT 2.0 format. For example, you would have to write (and (= x y) (not (= x y)))
instead of (x == y) && !(x == z)
.
3) 您可以使用 Z3 Python API,并使用 Python 中的 eval
函数解析字符串.下面是一个例子:
3) You can use the Z3 Python API, and parse strings using the eval
function in Python.
Here is an example:
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 安装中使用上面的脚本.
BTW, this script does not work at rise4fun http://rise4fun.com/z3py because the function eval
is not allowed there, but you can use the script above in your local Z3 installation.
这篇关于带字符串表达式的 Z3的文章就介绍到这了,希望我们推荐的答案对大家有所帮助,也希望大家多多支持IT屋!