search

dreal / dreal4

Automated Reasoning in Nonlinear Theories of Reals
https://dreal.github.io
Apache License 2.0
151 stars 32 forks source link

Print asserted formulas in SMTLIB format? #105

Closed caballa closed 5 years ago

caballa commented 5 years ago

Is it possible to print the asserted formulas in some kind of SMT-LIB format?

soonho-tri commented 5 years ago

We do not have this feature for now, but I can add one.

caballa commented 5 years ago

Thanks, that would be very useful.

soonho-tri commented 5 years ago

FYI, I've added ToPrefix(expression) / ToPrefix(formula) in C++, and expression.ToPrefix() and formula.ToPrefix() in Python APIs.

soonho-tri commented 5 years ago

I'll add a method to Context class, e.g. Context::GetAssertions, which will give you a list of asserted formulas.

Are you using dReal in C++ or Python? If it's the latter, I need to expose the Context class to the Python side.

caballa commented 5 years ago

I use C++

soonho-tri commented 5 years ago

Done. Please check https://github.com/dreal/dreal4/blob/master/dreal/solver/test/context_test.cc#L28-L46.

Note that bound constraints such as x <= 5 are not stored as assertions as shown in the test code.

soonho-tri commented 5 years ago

Closed by 63df044be55122172e371fed5deba8b1c6349764