防止解决方案被简化

我想使用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语句？如果我在没有发言权的情况下得到答案，我将更容易解析结果。

来源

2012-11-19 sriraj

我们可以设置下面的选项，以防止Z3相当打印机使用let小号

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

任何大的数字就可以了。

我们必须记住，当我们避开let时，显示一些包含大量共享子表达式的公式可能不太可行。在内部，Z3将公式存储为DAG而不是树。如果我们不使用let，那么这些公式的漂亮版本可能会比它们的内部表示呈指数级增长。所以，我们不应该滥用上述选项。

来源

2012-11-19 22:23:49

谢谢。这有很大帮助。 – sriraj

太好了。你能接受答案吗？因此，其他用户会知道答案可以解决问题中发布的问题。谢谢 –

这些选项是否也可以使用C API设置，如果是的话，怎么样？ –

我正在使用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-29 21:26:04 Mohammed

防止解决方案被简化

回答

相关问题