CODEWITHSUNDEEP
c++z3
Zhouyang
Zhouyang

Reputation: 21

Use a C++ string in z3::expr?

I got difficulties in using Z3::expr. In z3, the expr conj can be defined like:

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

Is there a way to use a string variable to define conj? Something like:

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

I got stuck on the problem for days.

Thanks

Upvotes: 2

Views: 274

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

There is no way to use that particular string in the example, but you can use parse_string, which understands strings in SMT2 format.

Upvotes: 1

Related Questions