Struct Solver

Source

pub struct Solver { /* private fields */ }

Expand description

(Incremental) solver, possibly specialized by a particular tactic or logic.

Implementations§

Source §

impl Solver

Source

pub fn new() -> Solver

Create a new solver. This solver is a “combined solver” that internally uses a non-incremental (solver1) and an incremental solver (solver2). This combined solver changes its behaviour based on how it is used and how its parameters are set.

If the solver is used in a non incremental way (i.e. no calls to Solver::push() or Solver::pop(), and no calls to Solver::assert() or Solver::assert_and_track() after checking satisfiability without an intervening Solver::reset()) then solver1 will be used. This solver will apply Z3’s “default” tactic.

The “default” tactic will attempt to probe the logic used by the assertions and will apply a specialized tactic if one is supported. Otherwise the general (and-then simplify smt) tactic will be used.

If the solver is used in an incremental way then the combined solver will switch to using solver2 (which behaves similarly to the general “smt” tactic).

Note however it is possible to set the solver2_timeout, solver2_unknown, and ignore_solver1 parameters of the combined solver to change its behaviour.

Source

pub fn from_string<T: Into<Vec<u8>>>(&self, source_string: T)

Parse an SMT-LIB2 string with assertions, soft constraints and optimization objectives. Add the parsed constraints and objectives to the solver.

Source

pub fn new_for_logic<S: Into<Symbol>>(logic: S) -> Option<Solver>

Create a new solver customized for the given logic. It returns None if the logic is unknown or unsupported.

Source

pub fn get_context(&self) -> &Context

Get this solver’s context.

Source

pub fn assert<T: Borrow<Bool>>(&self, ast: T)

Assert a constraint into the solver.

The functions Solver::check() and Solver::check_assumptions() should be used to check whether the logical context is consistent or not.

let mut solver = Solver::new();

solver.assert(&Bool::from_bool(true));
solver += &Bool::from_bool(false);
solver += Bool::fresh_const("");

assert_eq!(solver.check(), SatResult::Unsat);

§See also:

Solver::assert_and_track()

Source

pub fn assert_and_track<T: Into<Bool>>(&self, ast: T, p: &Bool)

Assert a constraint a into the solver, and track it (in the unsat) core using the Boolean constant p.

This API is an alternative to Solver::check_assumptions() for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using Solver::assert_and_track() and the Boolean literals provided using Solver::check_assumptions().

§See also:

Solver::assert()

Source

pub fn reset(&self)

Remove all assertions from the solver.

Source

pub fn check(&self) -> SatResult

Check whether the assertions in a given solver are consistent or not.

The function Solver::get_model() retrieves a model if the assertions is satisfiable (i.e., the result is SatResult::Sat) and model construction is enabled. Note that if the call returns SatResult::Unknown, Z3 does not ensure that calls to Solver::get_model() succeed and any models produced in this case are not guaranteed to satisfy the assertions.

The function Solver::get_proof() retrieves a proof if proof generation was enabled when the context was created, and the assertions are unsatisfiable (i.e., the result is SatResult::Unsat).

§See also:

Source

pub fn check_assumptions(&self, assumptions: &[Bool]) -> SatResult

Check whether the assertions in the given solver and optional assumptions are consistent or not.

The function Solver::get_unsat_core() retrieves the subset of the assumptions used in the unsatisfiability proof produced by Z3.

§See also:

Solver::check()

Source

pub fn get_assertions(&self) -> Vec<Bool>

Source

pub fn get_unsat_core(&self) -> Vec<Bool>

Return a subset of the assumptions provided to either the last

Solver::check_assumptions call, or
sequence of Solver::assert_and_track calls followed by a Solver::check call.

These are the assumptions Z3 used in the unsatisfiability proof. Assumptions are available in Z3. They are used to extract unsatisfiable cores. They may be also used to “retract” assumptions. Note that, assumptions are not really “soft constraints”, but they can be used to implement them.

By default, the unsat core will not be minimized. Generation of a minimized unsat core can be enabled via the "sat.core.minimize" and "smt.core.minimize" settings for SAT and SMT cores respectively. Generation of minimized unsat cores will be more expensive.

§See also:

Source

pub fn get_consequences( &self, assumptions: &[Bool], variables: &[Bool], ) -> Vec<Bool>

Retrieve consequences from the solver given a set of assumptions.

Source

pub fn push(&self)

Create a backtracking point.

The solver contains a stack of assertions.

§See also:

Solver::pop()

Source

pub fn pop(&self, n: u32)

Backtrack n backtracking points.

§See also:

Solver::push()

Source

pub fn get_model(&self) -> Option<Model>

Retrieve the model for the last Solver::check() or Solver::check_assumptions() if the assertions is satisfiable (i.e., the result is SatResult::Sat) and model construction is enabled.

It can also be used if the result is SatResult::Unknown, but the returned model is not guaranteed to satisfy quantified assertions.

The error handler is invoked if a model is not available because the commands above were not invoked for the given solver, or if the result was SatResult::Unsat.

Source

pub fn get_proof(&self) -> Option<impl Ast>

Retrieve the proof for the last Solver::check() or Solver::check_assumptions().

The error handler is invoked if proof generation is not enabled, or if the commands above were not invoked for the given solver, or if the result was different from SatResult::Unsat.

§See also:

Config::set_proof_generation()

Source

pub fn get_reason_unknown(&self) -> Option<String>

Return a brief justification for an “unknown” result (i.e., SatResult::Unknown) for the commands Solver::check() and Solver::check_assumptions().

Source

pub fn set_params(&self, params: &Params)

Set the current solver using the given parameters.

Source

pub fn get_statistics(&self) -> Statistics

Retrieve the statistics for the last Solver::check().

Source

pub fn to_smt2(&self) -> String

Source

pub fn solutions<T: Solvable>( &self, t: T, model_completion: bool, ) -> impl FusedIterator<Item = T::ModelInstance>

Iterates over models for the given Solvable from the current state of a Solver.

The iterator terminates if the Solver returns UNSAT or UNKNOWN, as well as if model generation fails. This iterator may also never terminate as some problems have infinite solutions. It is recommended to use Iterator::take if your problem has an unbounded number of solutions.

Note that, since this iterator is querying the solver, it’s not guaranteed to be at all “fast”: every iteration requires querying the solver and constructing a model, which can take time. This interface is merely here as a clean alternative to manually issuing Solver::check and Solver::get_model calls.

The Solver given to this method is Clone’d when producing the iterator: no change is made in the solver passed to the function.

§Examples

This can be used to iterate over solutions to individual Asts:

 let s = Solver::new();
 let a = Int::new_const("a");
 s.assert(a.le(4));
 s.assert(a.ge(0));
 let solutions: Vec<_> = s.solutions(a, true).collect();
 let mut solutions: Vec<_> = solutions.into_iter().map(|a|a.as_u64().unwrap()).collect();
 solutions.sort();
 assert_eq!(vec![0,1,2,3,4], solutions);

As well as solutions to multiple Asts, if passed through a Vec, an array or a slice:

 let s = Solver::new();
 let a = Int::new_const("a");
 s.assert(a.le(2));
 s.assert(a.ge(0));
 let solutions: Vec<_> = s.solutions(&[a.clone(), a+2], true).collect();
 // Doing all this to avoid relying on the order Z3 returns solutions.
 let mut solutions: Vec<Vec<_>> = solutions.into_iter().map(|a|a.into_iter().map(|b|b.as_u64().unwrap()).collect()).collect();
 solutions.sort_by(|a,b| a[0].cmp(&b[0]));

 assert_eq!(vec![vec![0,2], vec![1,3], vec![2,4]], solutions);

It is also possible to pass in differing types of Asts in a tuple. The traits to allow this have been implemented for tuples of arity 2 and 3. If you need more, it is suggested to use a struct (see the next example):

 let s = Solver::new();
 let a = Int::new_const("a");
 let b = BV::new_const("b", 8);
 s.assert(a.lt(1));
 s.assert(a.ge(0));
 s.assert(b.bvxor(0xff).to_int(false).eq(&a));
 let solutions: Vec<_> = s.solutions((a, b), true).collect();
 assert_eq!(solutions.len(), 1);
 let solution = &solutions[0];
 assert_eq!(solution.0, 0);
 assert_eq!(solution.1, 0xff);

Users can also implement Solvable on their types that wrap Z3 types to allow iterating over their models with this API:

#[derive(Clone)]
 struct MyStruct{
   pub a: Int,
   pub b: Int
 }

 impl Solvable for MyStruct {
    type ModelInstance = Self;
    fn read_from_model(&self, model: &Model, model_completion: bool) -> Option<Self> {
        Some(
            Self{
                a: model.eval(&self.a, model_completion).unwrap(),
                b: model.eval(&self.b, model_completion).unwrap()
            }
        )
    }

    fn generate_constraint(&self, model: &Self) -> Bool {
        Bool::or(&[self.a.eq(&model.a).not(), self.b.eq(&model.b).not()])
    }
 }

 let s = Solver::new();
 let my_struct = MyStruct{
    a: Int::fresh_const("a"),
    b: Int::fresh_const("b")
 };
 // only valid model will be a = 0 and b = 4
 s.assert(my_struct.a.lt(1));
 s.assert(my_struct.a.ge(0));
 s.assert(my_struct.b.eq(&my_struct.a + 4));

 let solutions: Vec<_> = s.solutions(&my_struct, true).collect();
 assert_eq!(solutions.len(), 1);
 assert_eq!(solutions[0].a, 0);
 assert_eq!(solutions[0].b, 4);

Source

pub fn into_solutions<T: Solvable>( self, t: T, model_completion: bool, ) -> impl FusedIterator<Item = T::ModelInstance>

Consume the current Solver and iterate over solutions to the given Solvable.

§Example

 let s = Solver::new_for_logic("QF_BV").unwrap();
 let a = BV::new_const("a", 8);
 let b = BV::new_const("b", 8);
 s.assert(a.bvxor(0xff).eq(&b));
 s.assert(b.eq(0x25));
 let solutions: Vec<_> = s.into_solutions([a,b], true).collect();
 assert_eq!(solutions.len(), 1);
 let solution = &solutions[0];
 assert_eq!(solution[0], 0xda);
 assert_eq!(solution[1], 0x25);

§See also:

Solver::solutions

Source

pub fn check_and_get_model<T: Solvable>( self, t: T, model_completion: bool, ) -> Option<T::ModelInstance>

Check the solver and, if satisfiable, return a single model instance for t.

This is a convenience that combines check() + get_model() + Solvable::read_from_model. If the check returns SatResult::Sat and model construction and extraction succeed, this method returns Some(instance). For any other result (Unsat, Unknown) or if model construction/reading fails, it returns None.

§Example

 let s = Solver::new();
 let a = Int::new_const("a");
 s.assert(a.ge(0));
 s.assert(a.le(2));
 let concrete_a = s.check_and_get_model(a, true).unwrap();
 // `concrete_a` is an `Int` value extracted from the model
 let val = concrete_a.as_u64().unwrap();
 assert!(val <= 2);