[−][src]Struct boolector::Btor
A Btor
represents an instance of the Boolector solver.
Each BV
and Array
is created in a particular Btor
instance.
Methods
impl Btor
[src]
pub fn new() -> Self
[src]
Create a new Btor
instance with no variables and no constraints.
pub fn set_opt(&self, opt: BtorOption)
[src]
Set an option to a particular value.
pub fn sat(&self) -> SolverResult
[src]
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)
[src]
Push n
context levels. n
must be at least 1.
pub fn pop(&self, n: u32)
[src]
Pop n
context levels. n
must be at least 1.
pub fn duplicate(&self) -> Self
[src]
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>>
[src]
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>>
[src]
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>>
[src]
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
.
pub fn get_array_by_symbol<R: AsRef<Btor> + Clone>(
btor: R,
symbol: &str
) -> Option<Array<R>>
[src]
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
.
pub fn fixate_assumptions(&self)
[src]
Add all current assumptions as assertions
pub fn reset_assumptions(&self)
[src]
Remove all added assumptions
pub fn reset_stats(&self)
[src]
Reset all statistics other than time statistics
pub fn reset_time(&self)
[src]
Reset time statistics
pub fn print_constraints(&self) -> String
[src]
Get a String
describing the current constraints
pub fn print_model(&self) -> String
[src]
Get a String
describing the current model, including a set of
satisfying assignments for all variables
pub fn get_version(&self) -> String
[src]
Get Boolector's version string
pub fn get_copyright(&self) -> String
[src]
Get Boolector's copyright notice
Trait Implementations
impl Sync for Btor
[src]
impl Eq for Btor
[src]
impl Drop for Btor
[src]
impl Send for Btor
[src]
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 PartialEq<Btor> for Btor
[src]
impl Debug for Btor
[src]
Auto Trait Implementations
Blanket Implementations
impl<T, U> Into<U> for T where
U: From<T>,
[src]
U: From<T>,
impl<T> From<T> for T
[src]
impl<T, U> TryFrom<U> for T where
U: Into<T>,
[src]
U: Into<T>,
type Error = Infallible
The type returned in the event of a conversion error.
fn try_from(value: U) -> Result<T, <T as TryFrom<U>>::Error>
[src]
impl<T, U> TryInto<U> for T where
U: TryFrom<T>,
[src]
U: TryFrom<T>,
type Error = <U as TryFrom<T>>::Error
The type returned in the event of a conversion error.
fn try_into(self) -> Result<U, <U as TryFrom<T>>::Error>
[src]
impl<T> BorrowMut<T> for T where
T: ?Sized,
[src]
T: ?Sized,
fn borrow_mut(&mut self) -> &mut T
[src]
impl<T> Borrow<T> for T where
T: ?Sized,
[src]
T: ?Sized,
impl<T> Any for T where
T: 'static + ?Sized,
[src]
T: 'static + ?Sized,