如何在z3PY中的api之一z3_solver中使用from_string函数

Question

from z3 import *
x = Bool("x")
y = Bool("Y")
s = Solver()
formula = 'And(x,y)'
s.from_string(formula)

当我尝试运行此代码时，编译器会提到"；z3.z3types.z3异常：b'(错误"第1行第1列：无效命令，'(应为'(\nunsupported\n'"。"formula"应该是哪种形式，smt2.0还是python形状。你能帮我解决这个问题吗？

Answer 1

您必须以SMTLib2语言提供输入，并确保所有变量都已声明。下面是一个工作示例：

from z3 import *
s = Solver()
formula = """(declare-const x Bool)
(declare-const y Bool)
(assert (and x y))
"""
s.from_string(formula)
print(s.sexpr())
print(s.check())
print(s.model())

此打印：

$ python a.py
(declare-fun y () Bool)
(declare-fun x () Bool)
(assert (and x y))
sat
[y = True, x = True]