如何将 z3py 表达式转换为 smtlib 2 格式 [英] how to convert z3py expression to smtlib 2 format

问题描述

我的问题与:Z3:将 Z3py 表达式转换为 SMT-LIB2?

我正在尝试将 z3py 表达式从 smtlib2 格式转换.使用以下脚本，但转换后，当我将结果提供给 z3 或任何其他 SMT 时，我得到:

I am trying to convert z3py expression from to smtlib2 format. using following script, but after conversion when I am feeding the result to z3 or any other SMT, I get:

语法错误，意外的让"

有什么办法可以用z3py把它导入smtlib2格式，这样我就不用再写长表达式了.

Is there any way that I can bring it in the smtlib2 format using z3py so that I dont have to write long expression again.

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

Following is the code which I am using for conversion:

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, "", 0, 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)

推荐答案

这也涉及到另一个问题 此处.

This is also related to another question here.

这个问题很可能是因为 Z3 的版本过时了.有许多错误修正尚未进入主分支并使用不稳定分支(或预编译的夜间二进制文件 here) 我得到一个不同的输出，它被 Z3 接受而没有错误:

Most likely, this problem is because of an outdated version of Z3. There have been numerous bugfixes which haven't made it into the master branch yet and using the unstable branch (or the precompiled nightly binaries here) I get a different output, which is accepted by Z3 without errors:

(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)

这篇关于如何将 z3py 表达式转换为 smtlib 2 格式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！