Supporto quantificatore Z3

Question

Ho bisogno di un rilevatore di teoremi per alcuni semplici problemi aritmetici lineari. Tuttavia, non riesco a far funzionare Z3 anche su problemi semplici. Sono consapevole che è incompleta, ma dovrebbe essere in grado di gestire questo semplice esempio:

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

Non sono sicuro se sto affaccia qualcosa, ma questo dovrebbe essere banale smentire. Ho anche provato questo esempio semplice:

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

che dovrebbe essere risolvibile facendo una ricerca esaustiva, dal momento di avvio contiene solo due valori.

In entrambi i casi, z3 risponde con lo sconosciuto. Mi piacerebbe sapere se sto facendo qualcosa di sbagliato qui o se non è possibile raccomandare un dimostratore di teoremi per questi tipi di formule.

Answer 1

Per la gestione di questo tipo di quantificatori, è necessario utilizzare il modulo di eliminazione quantificatore disponibile in Z3. Ecco un esempio di come usarlo (provate online all'indirizzo 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)) 

Il comando check-sat-using ci permette di specificare una strategia per risolvere il problema. Nell'esempio sopra, sto semplicemente usando qe (eliminazione del quantificatore) e poi invocando un solutore SMT generico. Si noti che, per questi esempi, qe è sufficiente.

Ecco un esempio più complesso, in cui abbiamo davvero bisogno di combinare qe e smt (provate online all'indirizzo: 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 Ecco lo stesso esempio utilizzando l'API C/C++:

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"; 
}