So far, external SAT-solvers are only available through
yices_check_formula / yices_check_formulas
which don't use any Yices context; the assertions are just passed as arguments. At the moment if I have a Yices context containing some bitvector constraints, I have no choice but to make bitblasting target the built-in SAT-solver.
Level 1 of this feature would be to have the choice of the backend SAT-solver when doing check-sat on a context with only QF_BV constraints and that only allows a single call to check-sat (mimicking what happens with yices_check_formula / yices_check_formulas).
Level 2 of this feature would be to have the choice of the backend SAT-solver when doing check-sat on a context with only QF_BV constraints but that allows incremental checks and push-pop, relying on the incrementality of the backend SAT-solver or using assumptions.
Level 3 of this feature would be to have the choice of the backend SAT-solver when the context's constraints combine the bitvector theory with other theories, and when the context allows incremental checks and push-pop.
So far, external SAT-solvers are only available through yices_check_formula / yices_check_formulas which don't use any Yices context; the assertions are just passed as arguments. At the moment if I have a Yices context containing some bitvector constraints, I have no choice but to make bitblasting target the built-in SAT-solver.
Level 1 of this feature would be to have the choice of the backend SAT-solver when doing check-sat on a context with only QF_BV constraints and that only allows a single call to check-sat (mimicking what happens with yices_check_formula / yices_check_formulas).
Level 2 of this feature would be to have the choice of the backend SAT-solver when doing check-sat on a context with only QF_BV constraints but that allows incremental checks and push-pop, relying on the incrementality of the backend SAT-solver or using assumptions.
Level 3 of this feature would be to have the choice of the backend SAT-solver when the context's constraints combine the bitvector theory with other theories, and when the context allows incremental checks and push-pop.