Struct boolector::BVSolution

pub struct BVSolution { /* fields omitted */ }

A BVSolution represents a possible solution for one BV in a given model.

Methods

impl BVSolution

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");

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().

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 xs.

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>

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>

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 Eq for BVSolution

impl Clone for BVSolution

fn clone(&self) -> BVSolution

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl PartialEq<BVSolution> for BVSolution

fn eq(&self, other: &BVSolution) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &BVSolution) -> bool

This method tests for !=.

impl Hash for BVSolution

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given [Hasher].

fn hash_slice<H>(data: &[Self], state: &mut H) where
    H: Hasher, 

Feeds a slice of this type into the given [Hasher].

impl Debug for BVSolution

fn fmt(&self, f: &mut Formatter) -> Result

Formats the value using the given formatter.