Z3：是否可以只简化一部分断言？

Question

我在 Windows 7 和 Java 7 64 位上使用 Z3 版本 4.3.2 64 位的 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)

如果这个 SMT-LIB V2 代码被 Z3 执行，结果是：

(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 是否等于集合B 中的任何断言edel 的思想，如果是，则不包括简化结果中的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]