Z3量詞支持

Question

我需要一個簡單的線性算術問題的定理證明。但是，即使在簡單的問題上，我也無法讓Z3工作。我知道，這是不完整的，但它應該能夠處理這個簡單的例子：

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

我不知道，如果我忽視的東西，但是這應該是微不足道的反駁。我甚至嘗試這個簡單的例子：

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

那應該是通過使窮舉搜索可以解決的，因爲開機只包含兩個值。

在這兩種情況下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) 

編輯 下面是使用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"; 
}