为了处理这种量词,您应该使用 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";
}