Add more flexible model API

c-cube / batsat

A (parametrized) Rust SAT solver originally based on MiniSat

https://docs.rs/batsat/

Other

30 stars 4 forks source link

Add more flexible model API #12

Closed dewert99 closed 9 months ago

dewert99 commented 9 months ago

I was working on a toy SMT solver (QF_UF only) and I got stuck implementing get_value and get_model since Solver::solve_limited_th reverts the state of the Theory to level 0 by calling (Theory::pop_levels) before returning. I though it would be helpful to allow these break this reverting out of Solver::solve_limited_th. Does this seem reasonable? I'm open to suggestions about naming.

dewert99 commented 9 months ago

I tried implementing get-value and get-model using this branch and they seem to work, so you are good to merge this.

c-cube commented 9 months ago

Thank you