python – 如何将z3py表达式转换为smtlib 2格式

发布时间：2020-12-20 13:41:25 所属栏目：Python 来源：网络整理

导读：我的问题与： Z3: convert Z3py expression to SMT-LIB2?有关我试图将z3py表达式转换为smtlib2格式.使用以下脚本,但转换后,当我将结果提供给z3或任何其他SMT时,我得到： “Syntax error,unexpected let” 有什么方法可以使用z3py以smtlib2格式将其带入,这样

我的问题与： Z3: convert Z3py expression to SMT-LIB2?有关

我试图将z3py表达式转换为smtlib2格式.使用以下脚本,但转换后,当我将结果提供给z3或任何其他SMT时,我得到：

“Syntax error,unexpected let”

有什么方法可以使用z3py以smtlib2格式将其带入,这样我就不必再次编写长表达式了.

以下是我用于转换的代码：

def convertor(f,status="unknown",name="benchmark",logic=""):
v = (Ast * 0)()
if isinstance(f,Solver):
a = f.assertions()
if len(a) == 0:
  f = BoolVal(True)
else:
  f = And(*a)
return Z3_benchmark_to_smtlib_string(f.ctx_ref(),name,logic,status,"",v,f.as_ast())

x = Int('x')
y = Int('y')
s = Solver()
s.add(x > 0)
s.add( x < 100000)
s.add(x==2*y)
print convertor(s,logic="QF_LIA")

这是输出：

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(let (($x35 (and $x10 $x31 $x34)))
(assert $x35)))))
(check-sat)

解决方法

这也与另一个问题 here有关.

最有可能的是,这个问题是由于Z3的过时版本.有许多错误修正,但尚未进入主分支并使用unstable分支(或预编译的夜间二进制文件here),我得到一个不同的输出,Z3接受没有错误：

(set-info :status unknown)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(let (($x34 (= x (* 2 y))))
(let (($x31 (< x 100000)))
(let (($x10 (> x 0)))
(and $x10 $x31 $x34)))))
(check-sat)

（编辑：李大同）

【声明】本站内容均来自网络，其相关言论仅代表作者个人观点，不代表本站立场。若无意侵犯到您的权利，请及时与联系站长删除相关内容!