Z3 量词支持 [英] Z3 quantifier support

问题描述

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

I need a theorem prover for some simple linear arithmetic problems. However, I can't get Z3 to work even on simple problems. I'm aware that it is incomplete, however it should be able to handle this simple example:

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

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

I'm not sure if i'm overlooking something, but this should be trivial to disprove. I even tried this simpler example:

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

这应该可以通过详尽的搜索来解决，因为 boot 只包含两个值.

That should be solvable by making an exhaustive search, since boot only contains two values.

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

In both cases z3 answers with unknown. I'd like to know if i'm doing something wrong here or if not if you can recommend a theorem prover for these types of formulas.

推荐答案

要处理这种量词，您应该使用 Z3 中提供的量词消除模块.这是一个关于如何使用它的示例(在 http://rise4fun.com/Z3/3C3):

For handling this kind of quantifiers, you should use the quantifier elimination module available in Z3. Here is an example on how to use it (try online at 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 就足够了.

The command check-sat-using allows us to specify an strategy to solve the problem. In the example above, I'm just using qe (quantifier elimination) and then invoking a general purpose SMT solver. Note that, for these examples, qe is sufficient.

这是一个更复杂的例子，我们确实需要结合 qe 和 smt(在线尝试:http://rise4fun.com/Z3/l3Rl )

Here is a more complicated example, where we really need to combine qe and smt (try online at: 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 的相同示例:

EDIT Here is the same example using the 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";
}

这篇关于Z3 量词支持的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！