Z3 量词支持答案

【问题标题】：Z3 quantifier supportZ3 量词支持
【发布时间】：2012-10-23 08:20:25
【问题描述】：

我需要一个定理证明器来解决一些简单的线性算术问题。但是，即使是简单的问题，我也无法让 Z3 工作。我知道它是不完整的，但是它应该能够处理这个简单的例子：

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

我不确定我是否忽略了某些东西，但这应该是微不足道的反驳。我什至尝试了这个更简单的例子：

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

这应该可以通过彻底搜索来解决，因为 boot 只包含两个值。

在这两种情况下，z3 的答案都是未知的。我想知道我是否在这里做错了什么，或者如果没有，您是否可以为这些类型的公式推荐一个定理证明器。

【问题讨论】：

标签： z3

【解决方案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";
}

【讨论】：

太好了。有用。你能告诉我如何使用 C Api 指定它吗？因为 Z3_check 函数不接受任何进一步的参数。
您必须创建一个策略并将其转换为求解器。我添加了一个使用 C/C++ API 的示例。