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.

Implementations

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.

let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::Incremental(true));

// An 8-bit unconstrained `BV` with the symbol "foo"
let foo = BV::new(btor.clone(), 8, Some("foo"));

// Assert that "foo" must be greater than `3`
foo.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert();

// This state is satisfiable
assert_eq!(btor.sat(), SolverResult::Sat);

// Assert that "foo" must also be less than `2`
foo.ult(&BV::from_u32(btor.clone(), 2, 8)).assert();

// State is now unsatisfiable
assert_eq!(btor.sat(), SolverResult::Unsat);

// Repeat the first step above with the solver timeout set to something
// extremely high (say, 200 sec) - should still be `Sat`
let btor = Rc::new(Btor::new());
btor.set_opt(BtorOption::Incremental(true));
btor.set_opt(BtorOption::SolverTimeout(Some(Duration::from_secs(200))));
let foo = BV::new(btor.clone(), 8, Some("foo"));
foo.ugt(&BV::from_u32(btor.clone(), 3, 8)).assert();
assert_eq!(btor.sat(), SolverResult::Sat);

// But, if we make the second assertion and then set the solver timeout to
// something extremely low (say, 2 ns), we'll get `SolverResult::Unknown`
foo.ugt(&BV::from_u32(btor.clone(), 5, 8)).assert();
btor.set_opt(BtorOption::SolverTimeout(Some(Duration::from_nanos(2))));
assert_eq!(btor.sat(), SolverResult::Unknown);

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: Borrow<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: Borrow<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: Borrow<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: Borrow<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 Debug for Btor

pub fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Default for Btor

pub fn default() -> Self

Returns the "default value" for a type.

impl Drop for Btor

pub fn drop(&mut self)

Executes the destructor for this type.

impl Eq for Btor

impl PartialEq<Btor> for Btor

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

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

#[must_use]pub fn ne(&self, other: &Rhs) -> bool

This method tests for !=.

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. (Note that TimeoutState is also careful to be both Send and Sync.)

impl Sync for Btor