Как реализовать обычную упрощенную тактику в Z3?

Question

В моем инструменте я использую условия, которые сравнивают константы с целыми переменными (например, y < 100). Часто для одной переменной существует несколько условий, и я хочу упростить эти случаи. Например: y & y! = 99 должно стать y < 99. Эта тактика упрощения не делает этого, и ни один из аргументов для упрощения звука, как они могут помочь.

В Код:

context c; 
goal g(c); 
expr x = c.int_const("x"); 
expr y = c.int_const("y"); 
solver s(c); 
expr F = y < 100 && y != 99; 
g.add(F); 
tactic t = tactic(c, "simplify"); 
apply_result r = t(g); 
for (unsigned i = 0; i < r.size(); i++) { 
    std::cout << "subgoal " << i << "\n" << r[i] << "\n"; 
} 

Выход в конце концов возвращается: subgoal 0 (goal (not (<= 100 y)) (not (= y 99)))

и не subgoal 0(goal(not(<= 99 y)) или что-то подобное, как я хочу, чтобы это было.

Поэтому я хочу реализовать свою тактику упрощения. К сожалению, я не могу найти, как это сделать. Я знаю, что тактика должна быть реализована на C++, но как я могу представить свою тактику для Z3?

Answer 1

Тактика Z3 хранится в каталоге: src/tactic. Арифметическая тактика находится в подкаталоге arith. Вы должны использовать существующую тактику как «шаблон» для реализации вашей тактики. Хорошим примером является https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/normalize_bounds_tactic.cpp

Для того, чтобы новая тактика доступна в API и SMT 2.0 переднего конца, мы должны включить комментарий, содержащий команду ADD_TACTIC. Эта команда инструктирует сценарий Z3 mk_make для склеивания всего вместе. Аргументами являются: название тактики, описания и кода на C++ для создания тактики.

/* 
    ADD_TACTIC("normalize-bounds", 
      "replace a variable x with lower bound k <= x with x' = x - k.", 
      "mk_normalize_bounds_tactic(m, p)") 
*/ 

Кстати, вы можете также попытаться реализовать новую функцию, расширяя существующую тактику, такие как: https://z3.codeplex.com/SourceControl/latest#src/tactic/arith/propagate_ineqs_tactic.cpp