5

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

4

2 回答 2

5

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

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

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

我们必须记住，当我们避免使用lets 时，显示一些包含大量共享子表达式的公式可能不可行。在内部，Z3 将公式存储为 DAG 而不是树。如果我们不使用lets，这些公式的漂亮打印可能会比它们的内部表示大得多。因此，我们不应滥用上述选项。

于 2012-11-19T22:23:49.450 回答
0

我正在使用z3-4.5.0，看起来选项名称发生了一些变化。如果pp-max-depth对您不起作用，请尝试pp.max_depth和pp.min_alias_size。

我正在使用 Java API，以下内容与我一起使用

com.microsoft.z3.Global.setParameter("pp.min_alias_size", "1000000");
com.microsoft.z3.Global.setParameter("pp.max_depth", "1000000");
于 2017-06-29T21:26:04.263 回答