Z3：消除无关变量

Question

我有一个 test.smt2 文件：

(set-logic QF_IDL)
(declare-const a Int)
(declare-const b Int)
(declare-const c Int)
(assert (or (< a 2) (< b 2 )) )
(check-sat)
(get-model)
(exit)

有没有办法告诉 Z3 只输出 a=1（或 b=1）？因为当 a 为 1 时，b 的值就不再重要了。

我执行了 z3 smt.relevancy=2 -smt2 test.smt2

（在How do I get Z3 to return minimal model?之后，虽然smt.relevancy似乎有默认值2），但它仍然输出：

sat
(model
  (define-fun b () Int
    2)
  (define-fun a () Int
    1)
)

谢谢！

Answer 1

在对所指问题的答案中给出的示例稍微过时了。 Solver() 会选择合适的策略来解决问题，现在看来它选择了不同的策略。我们仍然可以通过使用SimpleSolver() 来获得这种行为（可能会造成重大的性能损失）。这是一个更新的示例：

from z3 import *

x, y = Bools('x y')
s = SimpleSolver()
s.set(auto_config=False,relevancy=2)
s.add(Or(x, y))
print s.check()
print s.model()

注意(check-sat) 命令不会执行与SimpleSolver() 相同的策略；为了在解决 SMT2 文件时获得相同的行为，我们需要使用 smt 策略，即使用(check-sat-using smt)。在许多情况下，首先在问题上额外运行简化器将是有益的，我们可以通过构建自定义策略来实现，例如，(check-sat-using (then simplify smt))