Function haybale::solver_utils::bvs_can_be_equal
source · pub fn bvs_can_be_equal<V: BV>(btor: &Btor, a: &V, b: &V) -> Result<bool>
Expand description
Returns true
if under the current constraints, a
and b
can have the
same value. Returns false
if a
and b
cannot have the same value. (If
the current constraints are themselves unsatisfiable, that will also result
in false
.)
A common use case for this function is to test whether some BV
can be
equal to a given concrete value. You can do this with something like
bvs_can_be_equal(btor, bv, BV::from_u64(...))
.
This function and bvs_must_be_equal()
are both more efficient than
get_a_solution()
or get_possible_solutions()
-type functions, as they do
not require full model generation. You should prefer this function or
bvs_must_be_equal()
if they are sufficient for your needs.