Z3定量器のサポート

Question

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

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

を、私は私が何かを見下ろすてるかどうかわからないんだけど、これは反証するのは簡単でなければなりません。

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

ブートが2つのしか値が含まれているため、徹底的な検索を行うことによって解決できるようになります。私も、この単純な例を試してみました。

どちらの場合も、z3の回答は不明です。私はここで何か間違っているのか、そうでないのかを知りたいのですが、これらのタイプの式の定理証明をお勧めしたいのであれば。

Answer 1

この種の量子を処理するには、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) 

EDIT は、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"; 
}