Z3 niceleyici desteği

Question

Bazı basit doğrusal aritmetik problemler için bir teorem geliştiricisine ihtiyacım var. Ancak, Z3'ün basit problemlerde bile çalışmasını sağlayamıyorum. ben bir şey bakan ediyorsam

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

emin değilim, ama bu çürütmek için önemsiz olmalıdır: Ben ancak bu basit bir örnek ele almak gerekir, bu eksik olduğunu farkındayım.

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

çizme sadece iki değer içerdiğinden, kapsamlı bir arama yaparak çözülebilir olması gerekir: Ben bile bu basit örnek çalıştı.

Her iki durumda da bilinmeyen z3 cevapları. Burada yanlış bir şey yapıp yapmadığımı ya da eğer bu tip formüller için bir teorem geliştirici önerebilirseniz, bilmek isterim.

Answer 1

Bu tür ölçüm düzenleyicileri işlemek için, Z3'te bulunan niceleyici eleme modülünü kullanmalısınız. İşte nasıl kullanılacağı hakkında bir örnektir (http://rise4fun.com/Z3/3C3 online deneyin):

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

komut check-sat-using bize sorunu çözmek için bir strateji belirlemenizi sağlar. Yukarıdaki örnekte, sadece qe (niceleyici eleme) kullanıyorum ve daha sonra genel amaçlı bir SMT çözücüsünü çağırıyorum. Not: Bu örnekler için qe yeterlidir. İşte C/C++ API kullanarak aynı örnek

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

DÜZENLEME: İşte

biz gerçekten qe ve smt (http://rise4fun.com/Z3/l3Rl online deneyin) birleştirmek için gereken daha karmaşık bir örnek vardır:

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