Struct haybale_pitchfork::secret::BtorRef

pub struct BtorRef(_);

This wrapper around Rc<Btor> exists simply so we can give it a different implementation of haybale::backend::SolverRef than the one provided by haybale::backend.

Methods from Deref<Target = Btor>

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) -> Btor

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 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 AsRef<Btor> for BtorRef

fn as_ref(&self) -> &Btor

Performs the conversion.

impl Clone for BtorRef

fn clone(&self) -> BtorRef

Returns a copy of the value.

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

Performs copy-assignment from source.

impl Debug for BtorRef

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

Formats the value using the given formatter.

impl Deref for BtorRef

type Target = Btor

The resulting type after dereferencing.

fn deref(&self) -> &Btor

Dereferences the value.

impl From<BtorRef> for Rc<Btor>

fn from(btor: BtorRef) -> Rc<Btor>

Performs the conversion.

impl From<Rc<Btor>> for BtorRef

fn from(rc: Rc<Btor>) -> BtorRef

Performs the conversion.

impl PartialEq<BtorRef> for BtorRef

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

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

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

This method tests for !=.

impl SolverRef for BtorRef

type BV = BV

type Array = Array<Rc<Btor>>

fn new() -> Self

Create a new Btor instance, initialize it as necessary, and return a SolverRef to it

fn duplicate(&self) -> Self

As opposed to clone() which merely clones the reference, this function produces a deep copy of the underlying solver instance

fn match_bv(&self, bv: &BV) -> Option<BV>

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

fn match_array(&self, array: &Array<Rc<Btor>>) -> Option<Array<Rc<Btor>>>

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

impl Eq for BtorRef

impl StructuralEq for BtorRef

impl StructuralPartialEq for BtorRef