Struct boolector::BVSolution
source · [−]pub struct BVSolution { /* private fields */ }
Expand description
A BVSolution
represents a possible solution for one BV
in a given model.
Implementations
sourceimpl BVSolution
impl BVSolution
sourcepub fn as_01x_str(&self) -> &str
pub fn as_01x_str(&self) -> &str
Get a string of length equal to the bitwidth, where each character in the
string is either 0
, 1
, or x
. An x
indicates that, in this model,
the corresponding bit can be arbitrarily chosen to be 0
or 1
and all
constraints would still be satisfied.
Example
let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::ModelGen(ModelGen::All));
// `bv` starts as an unconstrained 8-bit value
let bv = BV::new(btor.clone(), 8, Some("foo"));
// assert that the first two digits of `bv` are 0
let mask = BV::from_u32(btor.clone(), 0b11000000, 8);
let zero = BV::zero(btor.clone(), 8);
bv.and(&mask)._eq(&zero).assert();
// `as_01x_str()` gives an 8-character string whose first
// two digits are '0'
assert_eq!(btor.sat(), SolverResult::Sat);
let solution = bv.get_a_solution();
assert_eq!(&solution.as_01x_str()[..2], "00");
sourcepub fn from_01x_str(s: impl Into<String>) -> Self
pub fn from_01x_str(s: impl Into<String>) -> Self
Turn a string of 0
, 1
, and/or x
characters into a BVSolution
.
See as_01x_str()
.
sourcepub fn disambiguate(&self) -> Self
pub fn disambiguate(&self) -> Self
Get a version of this BVSolution
that is guaranteed to correspond to
exactly one possible value. For instance,
as_01x_str()
on the
resulting BVSolution
will contain no x
s.
In the event that the input BVSolution
did represent multiple possible
values (see as_01x_str()
),
this will simply choose one possible value arbitrarily.
sourcepub fn as_u64(&self) -> Option<u64>
pub fn as_u64(&self) -> Option<u64>
Get a u64
value for the BVSolution
. In the event that this
BVSolution
represents multiple possible values (see
as_01x_str()
), this will
simply choose one possible value arbitrarily.
Returns None
if the value does not fit in 64 bits.
For a code example, see BV::new()
.
sourcepub fn as_bool(&self) -> Option<bool>
pub fn as_bool(&self) -> Option<bool>
Get a bool
value for the BVSolution
. In the event that this
BVSolution
represents both true
and false
(see
as_01x_str()
), this will
return false
.
Returns None
if the BVSolution
is not a 1-bit value.
Trait Implementations
sourceimpl Clone for BVSolution
impl Clone for BVSolution
sourcefn clone(&self) -> BVSolution
fn clone(&self) -> BVSolution
Returns a copy of the value. Read more
1.0.0 · sourcefn clone_from(&mut self, source: &Self)
fn clone_from(&mut self, source: &Self)
Performs copy-assignment from source
. Read more
sourceimpl Debug for BVSolution
impl Debug for BVSolution
sourceimpl Hash for BVSolution
impl Hash for BVSolution
sourceimpl PartialEq<BVSolution> for BVSolution
impl PartialEq<BVSolution> for BVSolution
sourcefn eq(&self, other: &BVSolution) -> bool
fn eq(&self, other: &BVSolution) -> bool
This method tests for self
and other
values to be equal, and is used
by ==
. Read more
sourcefn ne(&self, other: &BVSolution) -> bool
fn ne(&self, other: &BVSolution) -> bool
This method tests for !=
.
impl Eq for BVSolution
impl StructuralEq for BVSolution
impl StructuralPartialEq for BVSolution
Auto Trait Implementations
impl RefUnwindSafe for BVSolution
impl Send for BVSolution
impl Sync for BVSolution
impl Unpin for BVSolution
impl UnwindSafe for BVSolution
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more
sourceimpl<T> ToOwned for T where
T: Clone,
impl<T> ToOwned for T where
T: Clone,
type Owned = T
type Owned = T
The resulting type after obtaining ownership.
sourcefn clone_into(&self, target: &mut T)
fn clone_into(&self, target: &mut T)
toowned_clone_into
)Uses borrowed data to replace owned data, usually by cloning. Read more