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