0

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

一个小例子：x = Int('x') y = Int('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())

这会产生输出

; name    
(set-info :status unsat)
(set-logic QF_LIA)
(declare-fun y () Int)
(declare-fun x () Int)
(assert
(> x y))
(assert
(let (($x12 (> y 0)))
(let (($x10 (= x 0)))
(and $x10 $x12))))
(check-sat)

在进行一些独裁修改后，将其提供给 smtinterpol 很好：

; 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 输出中包含所有断言，而无需通过 AND 将所有 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())

基本上，有人知道 __in_ecount(num_assumptions) Z3_ast const 的 python 等价物是什么吗？或者是否有另一种可能性从 Solver 的断言列表中生成 smt2 输出？

4

1 回答 1

1

正如您所注意到的，Python API 不会将 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

于 2013-03-25T01:23:57.460 回答