z3 - 防止解决方案被简化

Question

我想使用 let 从 z3 得到没有简化的解决方案声明。

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

(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 语句中？如果我在没有 let 语句的情况下得到平坦的答案，我会更容易解析结果。

Answer 1

我们可以设置以下选项来防止Z3 pretty-print 使用let秒

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

任何大数字都可以。

我们必须记住，当我们避免使用 let 时，显示一些包含大量共享子表达式的公式可能是不可行的。 s。在内部，Z3 将公式存储为 DAG 而不是树。如果我们不使用 let s，这些公式的 pretty-print 可能比它们的内部表示成指数级大。因此，我们不应滥用上述选项。