Obsługa kwantyfikatora Z3

Question

Potrzebuję dowodu twierdzenia dla prostych prostych zagadnień arytmetycznych liniowych. Jednak nie mogę zmusić Z3 do pracy nawet przy prostych problemach. Jestem świadomy, że jest niekompletna, jednak powinien on być w stanie obsłużyć tego prostego przykładu:

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

Nie jestem pewien, czy jestem widokiem coś, ale to powinno być banalne obalić. Próbowałem nawet tego prostszego przykładu:

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

To powinno być możliwe do rozwiązania poprzez wyczerpujące wyszukiwanie, ponieważ boot zawiera tylko dwie wartości.

W obu przypadkach odpowiedzi z3 są nieznane. Chciałbym wiedzieć, czy robię coś złego tutaj, czy nie, jeśli możesz polecić dowódcę twierdzenia dla tego typu formuł.

Answer 1

Do obsługi tego rodzaju kwantyfikatorów należy użyć modułu eliminującego kwantyfikator dostępnego w Z3. Oto przykład, w jaki sposób z niego korzystać (spróbuj internetowej 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)) 

Komenda check-sat-using pozwala nam określić strategię rozwiązania problemu. W powyższym przykładzie używam tylko qe (eliminacja kwantyfikatora), a następnie wywołuję solver SMT ogólnego przeznaczenia. Należy pamiętać, że dla tych przykładów wystarczające jest qe.

Oto bardziej skomplikowany przykład, gdzie naprawdę musimy połączyć qe i smt (spróbuj w Internecie pod adresem: 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 Oto sam przykład przy użyciu 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"; 
}