Z3 C++ API: установить параметр для тактики

Я использую API-интерфейс Z3 C++ для SMT Solver, и я хотел бы изменить параметры «ctx-solver-simplify». Я не знаю, как ввести их в тактику. Я пробовал:Z3 C++ API: установить параметр для тактики

z3::context c; 
c.set("arith_lhs",false); 
c.set("eq2ineq",true);

z3::params params(c); 
params.set("arith_lhs",true); 
params.set("eq2ineq",true);

Пример кода:

z3::expr x = c.int_const("x"); 
z3::expr cond1 = !(x==4); 

z3::goal g(c); 
g.add(cond1); 

z3::tactic t(c, "ctx-solver-simplify"); 
z3::apply_result r = t(g);

Результат является

(goal (not (= x 4)))

И не

(goal and (< x 4) (> x 4)

То же самое относится к arith_lhs. Любая помощь? Спасибо!

источник

2016-07-21 toebs

Как они «не работают»? Например, какой результат вы получаете по сравнению с тем, что хотите. – hyde

Как инженер, вы должны научиться прежде всего тому, что вам нужно предоставить контекст, то есть поделиться с вами другими предметами вашей проблемы. Есть вероятность, что они не знакомы с проблемой или окружающим ее контекстом. Итак, в этом случае вам нужно объяснить (A), что такое 'z3', (B), каков ваш ввод, (C) каков ваш ожидаемый результат, (D) каков фактический результат. – iksemyonov

Как инженер, я стараюсь как можно проще задавать вопросы. Думаю, вы не используете решатель Z3-smt? В любом случае, я обновил вопросы. – toebs

Изменение: z3::tactic t(c, "ctx-solver-simplify"); к z3::tactic t = with(z3::tactic(c, "simplify"), params);

Это будет инструктировать Z3 применить simplify тактику с выбранными параметрами. В API SMT-LIB это выполняется с помощью комбинатора «use-params». Я получил вышеуказанный эквивалент C++ от example.cpp, поставляемый с источником Z3.

Таким образом, возникли две проблемы: (1) Вам нужно указать Z3, чтобы применить данную тактику к выбранным параметрам. (2) тактика ctx-solver-simplify не имеет опции eq2ineq. Другие тактики, хотя, включая simplify.

источник

2016-07-22 13:41:31

Если кто-то хочет использовать eq2inq с ctx-solver-simplify, сначала упростите, а затем упростите ctx-solver-simplify. Неэффективно, но он работает. – toebs

Хорошая идея, toebs. –

Z3 C++ API: установить параметр для тактики

ответ

Смежные вопросы