Поддержка квантификатора Z3

Question

Мне нужен доказатель теоремы для некоторых простых линейных арифметических задач. Однако я не могу заставить Z3 работать даже над простыми проблемами. Я знаю, что это неполно, однако он должен справиться с этим простым примером:

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

Я не уверен, что я пропускаю что-то, но это должно быть тривиально опровергнуть. Я даже попробовал этот более простой пример:

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

Это должно быть решено путем исчерпывающего поиска, так как boot содержит только два значения.

В обоих случаях 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)

РЕДАКТИРОВАТЬ Вот тот же пример с использованием API C / C++:

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