Z3:消除无关变量 [英] Z3: eliminate don't care variables

问题描述

我有一个 test.smt2 文件:

I have a test.smt2 file:

(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 的值就不再重要了.

Is there anyway to tell Z3 to only output a=1 (or b=1)? Because when a is 1, b's value does not matter any more.

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

I executed z3 smt.relevancy=2 -smt2 test.smt2

(遵循 如何让 Z3 返回最小模型?，虽然smt.relevancy好像有默认值2)，但是还是输出:

(following How do I get Z3 to return minimal model?, although smt.relevancy seems has default value 2), but it still outputs:

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

谢谢！

推荐答案

所指问题的答案中给出的示例略有过时.Solver() 将选择一种合适的策略来解决问题，现在它似乎选择了一种不同的策略.我们仍然可以通过使用 SimpleSolver() 获得这种行为(可能会造成显着的性能损失).这是一个更新的示例:

The example given in the answer to the question referred to is slightly out of date. A Solver() will pick a suitable tactic to solve the problem, and it appears that it picks a different one now. We can still get that behavior by using a SimpleSolver() (at a possibly significant performance loss). Here's an updated example:

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 (然后简化 smt))

Note that the (check-sat) command will not execute the same tactic as the SimpleSolver(); to get the same behavior when solving SMT2 files, we need to use the smt tactic, i.e., use (check-sat-using smt). In many cases it will be beneficial to additionally run the simplifier on the problem first which we can achieve by constructing a custom tactic, e.g., (check-sat-using (then simplify smt))

这篇关于Z3:消除无关变量的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！