防止解决方案被简化

Question

我想从z3获得的解决方案没有简化使用let语句.

例如,如果我给出以下内容:

(declare-const x Int)
  (elim-quantifiers (exists ((x.1 Int)) 
    (and (or (and (= (- x.1 2) 0) (<= (- x.1 9) 0)) 
             (and (or (= (- x.1 2) 0) (and (<= (- x.1 4) 0) 
                                      (and (<= (- 4 x.1) 0) 
                                           (<= (- x.1 11) 0)))) (<= (- x.1 9) 0))) (= (- (+ x.1 2) x) 0))))

我得到的解决方案是:

(let ((a!1 (and (or (and (<= x 4) (>= x 4)) (and (<= x 6) (>= x 6) (<= x 13)))
                (<= x 11))))
    (or (and (<= x 4) (>= x 4) (<= x 11)) a!1))

有没有办法告诉Z3不要将一些复杂的表达式提取到let语句中？如果我得到的答案持平而没有让声明,我将更容易解析结果.

Answer 1

我们可以设置以下选项以防止Z3漂亮的打印机使用lets

(set-option :pp-min-alias-size 1000000)
(set-option :pp-max-depth      1000000)

任何大数字都可以解决问题.

我们必须记住,当我们避开lets 时,显示一些包含许多共享子表达式的公式可能是不可行的.在内部,Z3将公式存储为DAG而不是树.如果我们不使用lets,那么这些公式的漂亮印刷可能比其内部表示指数大.因此,我们不应滥用上述选项.