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

概述我的问题与： 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)

@R_403_6120@ 这也与另一个问题 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)

总结

以上是内存溢出为你收集整理的python – 如何将z3py表达式转换为smtlib 2格式全部内容，希望文章能够帮你解决python – 如何将z3py表达式转换为smtlib 2格式所遇到的程序开发问题。

如果觉得内存溢出网站内容还不错，欢迎将内存溢出网站推荐给程序员好友。