Struct boolector::Btor

pub struct Btor { /* fields omitted */ }

A Btor represents an instance of the Boolector solver. Each BV and Array is created in a particular Btor instance.

Methods

impl Btor

pub fn new() -> Self

Create a new Btor instance with no variables and no constraints.

pub fn set_opt(&self, opt: BtorOption)

Set an option to a particular value.

pub fn sat(&self) -> SolverResult

Solve the current input (defined by the constraints which have been added via BV::assert() and BV::assume()). All assertions and assumptions are implicitly combined via Boolean and.

Calling this function multiple times requires incremental usage to be enabled via Btor::set_opt(). If incremental usage is not enabled, this function may only be called once.

pub fn push(&self, n: u32)

Push n context levels. n must be at least 1.

pub fn pop(&self, n: u32)

Pop n context levels. n must be at least 1.

pub fn duplicate(&self) -> Self

Duplicate a Btor instance. This will copy all variables, assertions, etc into the new instance.

Each BV or Array may only be used with the Btor it was originally created for. If you have a BV for one Btor and want to find the corresponding BV in another Btor, use Btor::get_matching_bv() or Btor::get_bv_by_symbol().

With SatEngine::Lingeling, this can be called at any time; but with SatEngine::PicoSAT or SatEngine::MiniSAT, this can only be called prior to the first Btor::sat() call.

The Boolector API docs refer to this operation as "clone", but we use duplicate() to avoid confusion.

Example

let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::ModelGen(ModelGen::All));

// `x` is an 8-bit `BV` less than `42`
let x = BV::new(btor.clone(), 8, Some("x"));
x.ult(&BV::from_u32(btor.clone(), 42, 8)).assert();

// `y` is equal to `x + 7`
let y = x.add(&BV::from_u32(btor.clone(), 7, 8));

// We duplicate the `Btor` instance
let btor_2 = Rc::new(btor.duplicate());

// The duplicated instance has copied versions of
// `x` and `y` which are distinct from the original
// `x` and `y` but still have the corresponding
// relationship (i.e., `y_2 = x_2 + 7`)
let x_2 = Btor::get_matching_bv(btor_2.clone(), &x).unwrap();
let y_2 = Btor::get_matching_bv(btor_2.clone(), &y).unwrap();

// The instances are totally independent now. In the
// original instance, we'll assert that `x > 3`, while
// in the new instance, we'll assert that `x < 3`.
// Note that we're careful to create constants with the
// correct `Btor` instance.
x.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert();
x_2.ult(&BV::from_u32(btor_2.clone(), 3, 8)).assert();

// Each instance is satisfiable by itself
assert_eq!(btor.sat(), SolverResult::Sat);
assert_eq!(btor_2.sat(), SolverResult::Sat);

// In the first instance, `y > 10`, while in the second,
// `y < 10`
let y_solution = y.get_a_solution().as_u64().unwrap();
assert!(y_solution > 10);
let y_2_solution = y_2.get_a_solution().as_u64().unwrap();
assert!(y_2_solution < 10);

pub fn get_matching_bv<R: AsRef<Btor> + Clone>(
    btor: R,
    bv: &BV<R>
) -> Option<BV<R>>

Given a BV originally created for any Btor, get the corresponding BV in the given btor. This only works if the BV was created before the relevant Btor::duplicate() was called; that is, it is intended to be used to find the copied version of a given BV in the new Btor.

It's also fine to call this with a BV created for the given Btor itself, in which case you'll just get back Some(bv.clone()).

For a code example, see Btor::duplicate().

pub fn get_matching_array<R: AsRef<Btor> + Clone>(
    btor: R,
    array: &Array<R>
) -> Option<Array<R>>

Given an Array originally created for any Btor, get the corresponding Array in the given btor. This only works if the Array was created before the relevant Btor::duplicate() was called; that is, it is intended to be used to find the copied version of a given Array in the new Btor.

It's also fine to call this with an Array created for the given Btor itself, in which case you'll just get back Some(array.clone()).

pub fn get_bv_by_symbol<R: AsRef<Btor> + Clone>(
    btor: R,
    symbol: &str
) -> Option<BV<R>>

Given a symbol, find the BV in the given Btor which has that symbol.

Since Btor::duplicate() copies all BVs to the new Btor including their symbols, this can also be used to find the copied version of a given BV in the new Btor.

pub fn get_array_by_symbol<R: AsRef<Btor> + Clone>(
    btor: R,
    symbol: &str
) -> Option<Array<R>>

Given a symbol, find the Array in the given Btor which has that symbol.

Since Btor::duplicate() copies all Arrays to the new Btor including their symbols, this can also be used to find the copied version of a given Array in the new Btor.

pub fn fixate_assumptions(&self)

Add all current assumptions as assertions

pub fn reset_assumptions(&self)

Remove all added assumptions

pub fn reset_stats(&self)

Reset all statistics other than time statistics

pub fn reset_time(&self)

Reset time statistics

pub fn print_constraints(&self) -> String

Get a String describing the current constraints

pub fn print_model(&self) -> String

Get a String describing the current model, including a set of satisfying assignments for all variables

pub fn get_version(&self) -> String

Get Boolector's version string

pub fn get_copyright(&self) -> String

Get Boolector's copyright notice

Trait Implementations

impl Send for Btor

According to https://groups.google.com/forum/#!msg/boolector/itYGgJxU3mY/AC2O0898BAAJ, the Boolector library is thread-safe, so we make Btor both Send and Sync.

impl Drop for Btor

fn drop(&mut self)

Executes the destructor for this type.

impl Eq for Btor

impl Sync for Btor

impl PartialEq<Btor> for Btor

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

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

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

This method tests for !=.

impl Debug for Btor

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

Formats the value using the given formatter.