Использовать строку C ++ в z3 :: expr?

Question

У меня возникли трудности при использовании Z3 :: expr. В z3 выражение expr con может быть определено как:

expr x = c.bool_const("x");
expr y = c.bool_const("y");
expr conj = (!x || !y);

Есть ли способ использовать строковую переменную для определения con ? Что-то вроде:

expr x = c.bool_const("x");
expr y = c.bool_const("y");
string str = "(!x || !y)";
expr conj = some_API(str);

Я застрял в этой проблеме на несколько дней.

Спасибо

Answer 1

Нет никакого способа использовать эту конкретную строку в примере, но вы можете использовать parse_string, который понимает строки в формате SMT2.