Получить результат применения тактики как выражение в Z3
Есть ли что-нибудь подобное в C ++, например, as_expr () интерфейса Z3py. Я пытаюсь получить результат применения тактики в качестве выражения z3, ехр, не как тип apply_result.
Например, в приведенном ниже коде
context c;
expr x = c.bool_const("x");
expr y = c.bool_const("y");
expr f = ( (x || y) && (x && y) );
solver s(c);
goal g(c);
g.add( f );
tactic t1(c, "simplify");
apply_result r = t1(g);
std::cout << r << "\n";
Кроме того, есть ли способ конвертировать apply_result в z3 expr?
Решение
В общем, результатом применения тактики является задавать целей. Большинство тактик дают только одну цель, но некоторые дают больше одной. Для каждой из этих подцелей вы можете использовать as_expr() а потом логично — или их вместе. Мы можем добавить as_expr(...) в class apply_result если это поможет (В данный момент я занят другими вещами; если вы добавите их сами, отправьте запрос на извлечение, взносы очень приветствуются!)
Другие решения
Других решений пока нет …