Устранение квантификатора для LIA в Z3 через C/C++ API

Николай уже указывал, что тактику можно использовать для устранения квантификатора. В этом посте я хотел бы подчеркнуть, как безопасно смешивать API C++ и C. Z3 C++ API использует подсчет ссылок для управления памятью. expr по сути является «умным указателем», который автоматически управляет счетчиками ссылок. Я обсуждал эту проблему в следующем сообщении: Выбор и сохранение массива с помощью C++ API.

Итак, когда мы вызываем C API, который возвращает Z3_ast, мы должны обернуть результат, используя функции to_expr, to_sort или to_func_decl. Подпись to_expr:

inline expr to_expr(context & c, Z3_ast a);

Используя эту функцию, мы избегаем утечек памяти и сбоев (при доступе к объектам, которые были собраны Z3). Вот полный пример с использованием to_expr(). Вы можете проверить это, скопировав эту функцию в файл example.cpp в папку c++ в раздаче Z3.

void tst_quantifier() {
    context ctx;
    expr x = ctx.int_const("x"); 
    expr y = ctx.int_const("y"); 
    expr sub_expr = (x <= y) && (y <= 2*x);
    Z3_app vars[] = {(Z3_app) x};

    expr qf = to_expr(ctx, Z3_mk_exists_const(ctx, 0, 1, vars,
                                              0, 0, // patterns don't seem to make sense here.
                                              sub_expr)); //No C++ API for quantifiers :(
    tactic qe(ctx, "qe");
    goal g(ctx);
    g.add(qf);
    std::cout << qe.apply(g);
}

Упрощение больше не вызывает процедуры исключения квантификатора. Устранение квантификатора и многие другие упрощения для специальных целей доступны вместо тактики.

Оболочка C++ z3++.h предоставляет методы для создания тактических объектов. Вам нужно будет создать тактический объект для тактики "qe". В дистрибутив Z3 входит несколько примеров использования тактики из z3++.h API. Например:

void tactic_example1() {
/*
  Z3 implements a methodology for orchestrating reasoning engines where "big" symbolic
  reasoning steps are represented as functions known as tactics, and tactics are composed
  using combinators known as tacticals. Tactics process sets of formulas called Goals.

  When a tactic is applied to some goal G, four different outcomes are possible. The tactic succeeds
  in showing G to be satisfiable (i.e., feasible); succeeds in showing G to be unsatisfiable (i.e., infeasible); 
  produces a sequence of subgoals; or fails. When reducing a goal G to a sequence of subgoals G1, ..., Gn, 
  we face the problem of model conversion. A model converter construct a model for G using a model for some subgoal Gi.

  In this example, we create a goal g consisting of three formulas, and a tactic t composed of two built-in tactics: 
  simplify and solve-eqs. The tactic simplify apply transformations equivalent to the ones found in the command simplify. 
  The tactic solver-eqs eliminate variables using Gaussian elimination. Actually, solve-eqs is not restricted 
  only to linear arithmetic. It can also eliminate arbitrary variables. 
  Then, sequential composition combinator & applies simplify to the input goal and solve-eqs to each subgoal produced by simplify. 
  In this example, only one subgoal is produced.
*/
std::cout << "tactic example 1\n";
context c;
expr x = c.real_const("x");
expr y = c.real_const("y");
goal g(c);
g.add(x > 0);
g.add(y > 0);
g.add(x == y + 2);
std::cout << g << "\n";
tactic t1(c, "simplify");
tactic t2(c, "solve-eqs");
tactic t = t1 & t2;
apply_result r = t(g);
std::cout << r << "\n";

}

В вашем случае вам нужно что-то вроде:

context ctx;
expr x = ctx.int_const("x"); 
expr y = ctx.int_const("y"); 
expr sub_expr = (x <= y)  && (y <= 2*x);

Z3_ast qf = Z3_mk_exists_const(ctx, 0, 1, (Z3_app[]) {x}, 
                              0, {}, // patterns don't seem to make sense here.
                              sub_expr); //No C++ API for quantifiers :(
tactic qe(ctx, "qe");
goal g(ctx);
g.add(qf);
cout << qe.apply(g);