pub fn min_possible_solution_for_bv_as_binary_str<V: BV>(
solver: V::SolverRef,
bv: &V
) -> Result<Option<String>>
Expand description
Get the minimum possible solution for the BV
: that is, the lowest value
for which the current set of constraints is still satisfiable.
“Minimum” will be interpreted in an unsigned fashion.
Allows BV
s of arbitrary width, and returns a String
with as many
characters as the BV
has bits; each character will be either 0
or 1
.
The string’s first ([0]
) character corresponds to the BV
’s leftmost
(most-significant) bit.
Returns Ok(None)
if there is no solution for the BV
, that is, if the
current set of constraints is unsatisfiable. Only returns Err
if a solver
query itself fails.