Function haybale::solver_utils::max_possible_solution_for_bv_as_binary_str

pub fn max_possible_solution_for_bv_as_binary_str<V: BV>(
    solver: V::SolverRef,
    bv: &V
) -> Result<Option<String>>

Get the maximum possible solution for the BV: that is, the highest value for which the current set of constraints is still satisfiable. “Maximum” will be interpreted in an unsigned fashion.

Allows BVs 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.