pub struct Btor { /* private fields */ }
Expand description
A Btor
represents an instance of the Boolector solver.
Each BV
and Array
is created in a particular Btor
instance.
Implementations
sourceimpl Btor
impl Btor
sourcepub fn set_opt(&self, opt: BtorOption)
pub fn set_opt(&self, opt: BtorOption)
Set an option to a particular value.
sourcepub fn sat(&self) -> SolverResult
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);
sourcepub fn duplicate(&self) -> Self
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);
sourcepub fn get_matching_bv<R: Borrow<Btor> + Clone>(
btor: R,
bv: &BV<R>
) -> Option<BV<R>>
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()
.
sourcepub fn get_matching_array<R: Borrow<Btor> + Clone>(
btor: R,
array: &Array<R>
) -> Option<Array<R>>
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())
.
sourcepub fn get_bv_by_symbol<R: Borrow<Btor> + Clone>(
btor: R,
symbol: &str
) -> Option<BV<R>>
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 BV
s 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
.
sourcepub fn get_array_by_symbol<R: Borrow<Btor> + Clone>(
btor: R,
symbol: &str
) -> Option<Array<R>>
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 Array
s 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
.
sourcepub fn fixate_assumptions(&self)
pub fn fixate_assumptions(&self)
Add all current assumptions as assertions
sourcepub fn reset_assumptions(&self)
pub fn reset_assumptions(&self)
Remove all added assumptions
sourcepub fn reset_stats(&self)
pub fn reset_stats(&self)
Reset all statistics other than time statistics
sourcepub fn reset_time(&self)
pub fn reset_time(&self)
Reset time statistics
sourcepub fn print_constraints(&self) -> String
pub fn print_constraints(&self) -> String
Get a String
describing the current constraints
sourcepub fn print_model(&self) -> String
pub fn print_model(&self) -> String
Get a String
describing the current model, including a set of
satisfying assignments for all variables
sourcepub fn get_version(&self) -> String
pub fn get_version(&self) -> String
Get Boolector’s version string
sourcepub fn get_copyright(&self) -> String
pub fn get_copyright(&self) -> String
Get Boolector’s copyright notice
Trait Implementations
impl Eq for Btor
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
Auto Trait Implementations
Blanket Implementations
sourceimpl<T> BorrowMut<T> for T where
T: ?Sized,
impl<T> BorrowMut<T> for T where
T: ?Sized,
const: unstable · sourcefn borrow_mut(&mut self) -> &mut T
fn borrow_mut(&mut self) -> &mut T
Mutably borrows from an owned value. Read more