Python等价于Z3_API Z3_benchmark_to_smtlib_字符串的第7个参数

Question

我们目前正在python上使用z3来检查程序跟踪的可行性。基于我们创建z3公式和断言的跟踪，我们的下一个方法是通过z3_benchmark_to_smtlib_字符串，使用SMT2作为中间语言将这些断言提供给iZ3和smtinterpol。在

一个小例子： x=整数（'x'） y=整数（'y'）

s = Solver()

# Assertions
s.assert_and_track(x > y, 'p1')
s.assert_and_track(x == 0, 'p2')
s.assert_and_track(y > 0, 'p3')

a = s.assertions()
v = a[0].as_ast()
f = And(a[1], a[2])
print Z3_benchmark_to_smtlib_string(a[0].ctx_ref(), "name", "QF_LIA", "unsat", "", 1, v, f.as_ast())

这样就产生了输出

^{pr2}$

这是很好的喂养后，它的一些专制修改：

; name
(set-info :status unsat)
(set-option :produce-proofs true)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert (!
(> x y) :named p1))
(assert (!
(let (($x12 (> y 0)))
(let (($x10 (= x 0)))
(and $x10 $x12))) :named p2))
(check-sat)
(get-interpolants p1 p2)

我们想要的是在smt2中输出所有断言，而不需要通过一个等式将所有1:end断言组合起来。如果被c代码文档（capi.html#gaf93844a5964ad8dee609fac3470d86e4“>；http://research.microsoft.com/en-us/um/redmond/projects/z3/group_capi.html\gaf93844a5964ad8dee609fac3470d86e4)第6和第7个参数的格式，但我可以让它工作，给他一个断言列表。在

我试过举例：

print Z3_benchmark_to_smtlib_string(a[0].ctx_ref(), "name", "QF_LIA", "unsat", "", 2, f.as_ast(), v)

但是会遇到

exception: access violation reading 0x00000004

同样，仅仅给出一个列表是行不通的：

print Z3_benchmark_to_smtlib_string(a[0].ctx_ref(), "name", "QF_LIA", "unsat", "", 2, [a[0].as_ast(), a[1].as_ast()], a[2].as_ast())

基本上，有人知道python的等价物是什么吗？或者，是否有另一种可能从解算器的断言列表生成smt2输出？在

Answer 1

正如您所注意到的，pythonapi没有向打印基准的函数公开Python包装器。 C签名是：

/**
   \brief Convert the given benchmark into SMT-LIB formatted string.

   \conly \warning The result buffer is statically allocated by Z3. It will
   \conly be automatically deallocated when #Z3_del_context is invoked.
   \conly So, the buffer is invalidated in the next call to \c Z3_benchmark_to_smtlib_string.

   \param c - context.
   \param name - name of benchmark. The argument is optional.
   \param logic - the benchmark logic. 
   \param status - the status string (sat, unsat, or unknown)
   \param attributes - other attributes, such as source, difficulty or category.
   \param num_assumptions - number of assumptions.
   \param assumptions - auxiliary assumptions.
   \param formula - formula to be checked for consistency in conjunction with assumptions.

   def_API('Z3_benchmark_to_smtlib_string', STRING, (_in(CONTEXT), _in(STRING), _in(STRING), _in(STRING), _in(STRING), _in(UINT), _in_array(5, AST), _in(AST)))
*/
Z3_string Z3_API Z3_benchmark_to_smtlib_string(__in   Z3_context c, 
                                               __in Z3_string name,
                                               __in Z3_string logic,
                                               __in Z3_string status,
                                               __in Z3_string attributes,
                                               __in   unsigned num_assumptions,
                                               __in_ecount(num_assumptions) Z3_ast const assumptions[],
                                               __in   Z3_ast formula);

在z3.py中有几个类似函数的示例，它们将数组作为参数，并且 它们使用相同的模式，即给C函数提供两个参数：（1） 数组（2）实际数组。 您应该将数组的长度和未拾取的数组传递给C函数。 您的示例的变体如下：http://rise4fun.com/Z3Py/rGEp