Function haybale::solver_utils::sat_with_extra_constraints
source · pub fn sat_with_extra_constraints<I, B>(
btor: &Btor,
constraints: impl IntoIterator<Item = I>
) -> Result<bool>where
I: Deref<Target = B>,
B: BV,
Expand description
Returns true
if the current constraints plus the additional constraints conds
are together satisfiable, or false
if not.
Returns Error::SolverError
if the query failed (e.g., was interrupted or timed out).
Does not permanently add the constraints in conds
to the solver.