[−][src]Struct boolector::BVSolution
A BVSolution
represents a possible solution for one BV
in a given model.
Methods
impl BVSolution
[src]
pub fn as_01x_str(&self) -> &str
[src]
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");
pub fn from_01x_str(s: impl Into<String>) -> Self
[src]
Turn a string of 0
, 1
, and/or x
characters into a BVSolution
.
See as_01x_str()
.
pub fn disambiguate(&self) -> Self
[src]
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.
pub fn as_u64(&self) -> Option<u64>
[src]
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()
.
pub fn as_bool(&self) -> Option<bool>
[src]
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
impl Clone for BVSolution
[src]
fn clone(&self) -> BVSolution
[src]
fn clone_from(&mut self, source: &Self)
1.0.0[src]
impl Eq for BVSolution
[src]
impl PartialEq<BVSolution> for BVSolution
[src]
fn eq(&self, other: &BVSolution) -> bool
[src]
fn ne(&self, other: &BVSolution) -> bool
[src]
impl Debug for BVSolution
[src]
impl Hash for BVSolution
[src]
fn hash<__H: Hasher>(&self, state: &mut __H)
[src]
fn hash_slice<H>(data: &[Self], state: &mut H) where
H: Hasher,
1.3.0[src]
H: Hasher,
impl StructuralPartialEq for BVSolution
[src]
impl StructuralEq for BVSolution
[src]
Auto Trait Implementations
impl Send for BVSolution
impl Sync for BVSolution
impl Unpin for BVSolution
impl UnwindSafe for BVSolution
impl RefUnwindSafe for BVSolution
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T> ToOwned for T where
T: Clone,
[src]
T: Clone,
type Owned = T
The resulting type after obtaining ownership.
fn to_owned(&self) -> T
[src]
fn clone_into(&self, target: &mut T)
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,