5

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))

いくつかの複雑な式を let ステートメントに抽出しないように Z3 に指示する方法はありますか? let ステートメントを使用せずに答えをフラットにすると、結果を解析しやすくなります。

4

2 に答える 2

5

次のオプションを設定して、Z3 pretty printer がletsを使用しないようにすることができます。

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

どんな大きな数字でもうまくいきます。

sを避けると、多くの共有サブ式を含む一部の数式を表示できない可能性があることに注意する必要がありますlet。内部的には、Z3 は式をツリーではなく DAG として保存します。sを使用しない場合、letそのような数式のプリティ プリントは、内部表現より指数関数的に大きくなる可能性があります。したがって、上記のオプションを乱用すべきではありません。

于 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 に答える