7

いくつかの単純な線形算術問題の定理証明器が必要です。しかし、単純な問題でもZ3を動作させることはできません。私はそれが不完全であることを知っています、しかしそれはこの単純な例を扱うことができるはずです：

(assert (forall ((t Int)) (= t 5)))
(check-sat)

私が何かを見落としているかどうかはわかりませんが、これは反証するのは簡単なはずです。私はこのもっと簡単な例を試しました：

(assert (forall ((t Bool)) (= t true)))
(check-sat)

ブートには2つの値しか含まれていないため、徹底的な検索を行うことで解決できるはずです。

どちらの場合も、z3は不明で応答します。私がここで何か間違ったことをしているのかどうか、そうでない場合は、これらのタイプの式の定理証明者を推奨できるかどうかを知りたいです。

4

1 に答える 1

7

この種の数量詞を処理するには、Z3で使用可能な数量詞消去モジュールを使用する必要があります。使用方法の例を次に示します（http://rise4fun.com/Z3/3C3でオンラインで試してください）。

(assert (forall ((t Int)) (= t 5)))
(check-sat-using (then qe smt))

(reset)

(assert (forall ((t Bool)) (= t true)))
(check-sat-using (then qe smt))

このコマンドcheck-sat-usingを使用すると、問題を解決するための戦略を指定できます。上記の例では、qe（量化記号消去法）を使用してから、汎用SMTソルバーを呼び出しています。これらの例でqeは、十分であることに注意してください。

これはもっと複雑な例で、実際に組み合わせる必要がありqeますsmt（オンラインで試してください：http：//rise4fun.com/Z3/l3Rl）

(declare-const a Int)
(declare-const b Int)
(assert (forall ((t Int)) (=> (<= t a) (< t b))))
(check-sat-using (then qe smt))
(get-model)

編集 これは、C / C++APIを使用した同じ例です。

void tactic_qe() {
    std::cout << "tactic example using quantifier elimination\n";
    context c;

    // Create a solver using "qe" and "smt" tactics
    solver s = 
        (tactic(c, "qe") &
         tactic(c, "smt")).mk_solver();

    expr a = c.int_const("a");
    expr b = c.int_const("b");
    expr x = c.int_const("x");
    expr f = implies(x <= a, x < b);

    // We have to use the C API directly for creating quantified formulas.
    Z3_app vars[] = {(Z3_app) x};
    expr qf = to_expr(c, Z3_mk_forall_const(c, 0, 1, vars,
                                            0, 0, // no pattern
                                            f));
    std::cout << qf << "\n";

    s.add(qf);
    std::cout << s.check() << "\n";
    std::cout << s.get_model() << "\n";
}
于 2012-11-02T16:29:52.633 に答える