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