0

We are experimenting with a relational logic for functional program verification. Our logic is equipped with relations over algebraic datatypes along with equality and subset-inclusion predicates over relations. Our verification procedure performs inductive program analysis (structural induction) and generates verification conditions (VCs) with sufficiently strong inductive hypotheses. VCs generated by our verification procedure adhere to the following format:

bindings <var-type bindings> in <antecedent-predicate> => <consequent-predicate> end

Here is an example VC generated by our procedure : http://pastebin.com/exncPHDA

We encode VCs thus generated in SMT2 language using following rules:

  1. Each concrete type (eg: 'a list) translates to an uninterpreted sort.
  2. Relations are encoded as uninterpreted n-ary functions from uninterpreted sorts to bool.
  3. Relational assertions (eg: R = R1 U R2, R = R1 X R2) are encoded as prenex-quantified assertions over uninterpreted functions.

The result of above encoding is (presumably) a formula in effectively propositional (EPR) first-order logic. With help of Z3, we were able to assert validity (unsatisfiability of negation) of many VCs. However, in some cases when VC is invalid (negation is SAT), Z3 loops. The example given above (http://pastebin.com/exncPHDA) is one such VC, whose SMT2 encoding is given here : http://pastebin.com/s8ezha7D . Z3 doesn't seem to terminate while asserting this formula.

Given that deciding quantified boolean formulas is NEXPTIME hard, non-termination of decision procedure is not very surprising. Nonetheless, we would like to know if there are any optimizations that we can do while encoding the formula in Z3 so as to make non-termination least likely -

  1. Our current encoding creates many empty sets (i.e., one assertion of form forall x:T, f(x)=false) and many instances of same singleton sets (i.e., forall x:T, (f(x) = true) <=> (x = v)). Does reducing such duplication help?
  2. Due to program elaboration, we currently have many variables and transitive equalities. Does reduction in number of variables help?

Also, how likely is it that Z3 loops while deciding an unsatisfiable quantified boolean formula?

4

1 回答 1

1

在 Z3 中，我们说形式为 的量词forall X, f(X) = T[X]，其中X是变量向量，f是未解释的函数，并且T是不包含 的术语/公式f，是宏。Z3 可以通过简单地替换所有出现的f. 该选项:macro-finder打开此功能。

     (set-option :macro-finder true)

如果我们应用此预处理步骤，则可以立即解决该示例。这是更新脚本的链接：http ://rise4fun.com/Z3/z2UJ

备注：在http://z3.codeplex.com的 work-in-progress (unstable) 分支中，这个选项被调用:smt.macro-finder。

于 2013-11-13T02:00:11.733 回答