Z3:是否可以简化部分断言？

Question

我在Windows 7以及64位Java 7上使用的是Z3版本4.3.2的Java-API,但我不认为Java是回答这个问题的必要条件.

现在我使用以下Java代码来简化Z3中断言的一个子集:

Tactic simplifyTactic = ctx.mkTactic("ctx-solver-simplify");
Goal goal = ctx.mkGoal(true, false, false);
goal.add(bel.toArray(new BoolExpr[0])); // bel is List<BoolExpr>
ApplyResult applyResult = simplifyTactic.apply(goal);

到目前为止,我已经过滤了要简化的断言,然后使用上面的代码进行简化,它按预期工作.

经过一些测试后,我得出结论,我还需要插入模型的过滤断言(其中包含一些元信息,如基数).

是否有可能简化一些断言集A,而另一个断言集B仍被视为但未被改变？

以下示例可能会稍微澄清这个问题:

(declare-const a Bool)
(declare-const b Bool)
(declare-const c Bool)
(declare-const d Bool)

(assert (=> a c)); member of set A
(assert (=> b d)); member of set A
(assert a); member of set A

; member of set B
(assert 
    (<= 
        (+ (ite (= c true) 1 0) (ite (= d true) 1 0))
        1
    )
)

; member of set B
(assert 
    (>= 
        (+ (ite (= c true) 1 0) (ite (= d true) 1 0))
        1
    )
)

(apply ctx-solver-simplify)

如果Z3执行此SMT-LIB V2代码,结果为:

(goals 
    (goal 
        c 
        (not b) 
        a 
        (<= (+ (ite (= c true) 1 0) (ite (= d true) 1 0)) 1) 
        :precision precise :depth 1
    ) 
)

对于这个简单的例子,结果非常好.约束(前三个断言(我的集合A))已按预期简化.以下两个断言(带有我的基数信息(集B))也被简化了.现在,我想要Z3做的是简化,但没有混合集A和B的结果.给定更复杂的断言,这将发生(并且发生在我的情况下).

这是怎么做到的？

Answer 1

为了简化起见，您需要添加 和A。B以下脚本使用的思想是检查e简化结果中的每个断言是否等于edel集合中的任何断言B，如果是，则不包括e在简化结果中，所有这些都在使用A和进行初始简化之后完成B。当然，您也可以B通过指针从简化结果中删除所有断言，但是如果B转换了断言，则可能会失败（就像我在 z3py 而不是 Z3 的 SMT 接口中运行示例时的情况一样），所以这激励证明断言是否与脚本相同。

它还检查 中所有断言的合取B。一般来说，您可能必须考虑其排列（例如， 中断言的对、三元组等的连接B），这可能使其不切实际，但也许它会满足您的目的。它适用于提供的示例。这是 z3py 中的脚本（链接到rise4fun：http://rise4fun.com/Z3Py/slY6）：

a,b,c,d = Bools('a b c d')
g = Goal()

A = []
A.append(Implies(a, c))
A.append(Implies(b, d))
A.append(a)

B = []
B.append((If(c == True, 1, 0) +  (If(d == True, 1, 0))) <=  1 )
B.append((If(c == True, 1, 0) +  (If(d == True, 1, 0))) >=  1 )

g.add(A)
g.add(B)

#t = Tactic('simplify')
#print t(g) # note difference

t = Tactic('ctx-solver-simplify')
ar = t(g)
print ar # [[c, Not(b), a, If(d, 1, 0) <= 0]]

s = Solver()
s.add(A)
result = []
for e in ar[0]: # iterate over expressions in result
  # try to prove equal
  s.push()
  s.add(Not(e == And(B))) # conunction of all assertions in B
  satres = s.check()
  s.pop()
  if satres == unsat:
    continue

  # check each in B individually
  for edel in B:
    # try to prove equal
    s.push()
    s.add(Not(e == edel))
    satres = s.check()
    s.pop()
    if satres != unsat:
      result.append(e)
      break

print result # [c, Not(b), a]