Struct rsmt2::Solver[−][src]

pub struct Solver<Parser> { /* fields omitted */ }
Expand description

Solver providing most of the SMT-LIB 2.5 commands.

Note the Self::tee function, which takes a file writer to which it will write everything sent to the solver.

Implementations

Basic functions, not related to SMT-LIB.

Constructor.

Creates a solver kid with the default z3 configuration.

Mostly used in tests, same as Self::new( SmtConf::z3(), parser ).

Creates a solver kid with the default cvc4 configuration.

Mostly used in tests, same as Self::new( SmtConf::z3(), parser ).

Creates a solver kid with the default yices 2 configuration.

Mostly used in tests, same as Self::new( SmtConf::yices_2(), parser ).

Creates a solver kid with the default z3 configuration and command.

Mostly used in tests, same as Self::new( SmtConf::default_z3(), parser ).

Warning

The command used to run a particular solver is up to the end-user. As such, it does not make sense to use default commands for anything else than local testing. You should explicitely pass the command to use with Self::z3 instead.

Creates a solver kid with the default cvc4 configuration and command.

Mostly used in tests, same as Self::new( SmtConf::default_z3(), parser ).

Warning

The command used to run a particular solver is up to the end-user. As such, it does not make sense to use default commands for anything else than local testing. You should explicitely pass the command to use with Self::cvc4 instead.

Creates a solver kid with the default yices 2 configuration and command.

Mostly used in tests, same as Self::new( SmtConf::default_yices_2(), parser ).

Warning

The command used to run a particular solver is up to the end-user. As such, it does not make sense to use default commands for anything else than local testing. You should explicitely pass the command to use with Self::yices_2 instead.

Returns the configuration of the solver.

Forces the solver to write all communications to a file.

Forces the solver to write all communications to a file.

  • opens file with create and write;
  • fails if the solver is already tee-ed;
  • see also Self::tee.

True if the solver is tee-ed.

Kills the solver kid.

The windows version just prints (exit) on the kid’s stdin. Anything else seems to cause problems.

This function is automatically called when the solver is dropped.

Prints a comment in the tee-ed file, if any.

Prints a comment in the tee-ed file, if any (string version).

Basic SMT-LIB parser-agnostic commands.

Asserts an expression.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.assert("(= 0 1)").unwrap();

Check-sat command, turns unknown results into errors.

See also

If you want a more natural way to handle unknown results, see parse_check_sat_or_unk.

Examples

let mut conf = SmtConf::default_z3();
conf.option("-t:10");
let mut solver = Solver::new(conf, ()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();

solver.push(1).unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let maybe_sat = solver.check_sat().unwrap();
assert_eq! { maybe_sat, true }
solver.pop(1).unwrap();

solver.assert("(= (+ (* x x y) (* y y x)) 7654321)").unwrap();
let sat_res = & solver.check_sat();

match * sat_res {
    Err(ref e) => match * e.kind() {
        ::rsmt2::errors::ErrorKind::Unknown => (),
        _ => panic!("expected unknown"),
    },
    Ok(res) => panic!("expected error: {:?}", res),
}

Check-sat command, turns unknown results in None.

See also

Examples

let mut conf = SmtConf::default_z3();
conf.option("-t:10");
solver.path_tee("./log.smt2").unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();

solver.push(1).unwrap();
solver.assert("(= (+ x y) 0)").unwrap();
let maybe_sat = solver.check_sat_or_unk().unwrap();
assert_eq! { maybe_sat, Some(true) }
solver.pop(1).unwrap();

solver.assert("(= (+ (* x x y) (* y y x)) 7654321)").unwrap();
let maybe_sat = solver.check_sat_or_unk().unwrap();
// Unknown ~~~~~~~~~~~~~vvvv
assert_eq! { maybe_sat, None }

Resets the underlying solver. Restarts the kid process if no reset command is supported.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.assert("(= 0 1)").unwrap();
assert!(! solver.check_sat().unwrap());
solver.reset().unwrap();
assert!(solver.check_sat().unwrap());

Declares a new constant.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap()

Declares a new function symbol.

let mut solver = Solver::default_z3(()).unwrap();
solver.declare_fun(
    "my_symbol", & [ "Int", "Real", "Bool" ], "Bool"
).unwrap()

Defines a new constant function symbol.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.define_const(
    "seven", "Int", "7"
).unwrap()

Defines a new function symbol.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.define_fun(
    "abs", & [ ("n", "Int") ], "Int", "(ite (< x 0) (- x) x)"
).unwrap()

Pushes n layers on the assertion stack.

Note that using actlits is more efficient than push/pop, and is useable for most push/pop use-cases.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();
solver.assert("(= x y)").unwrap();
let sat = solver.check_sat().unwrap();
assert!(sat);

solver.push(1).unwrap();
solver.assert("(= x (+ x 1))").unwrap();
let sat = solver.check_sat().unwrap();
assert!(! sat);
solver.pop(1).unwrap();

let sat = solver.check_sat().unwrap();
assert!(sat);

Pops n layers off the assertion stack.

Note that using actlits is more efficient than push/pop, and is useable for most push/pop use-cases.

Check-sat assuming command, turns unknown results into errors.

Check-sat assuming command, turns unknown results into None.

Sets the logic.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.set_logic( ::rsmt2::Logic::QF_UF ).unwrap();

Sets a custom logic.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.set_custom_logic("QF_UFBV").unwrap();

Defines a recursive function.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.define_fun_rec(
    "abs", & [ ("n", "Int") ], "Int", "(ite (< x 0) (abs (- x)) x)"
).unwrap()

Defines some (possibily mutually) recursive functions.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.define_funs_rec( & [
    ("abs_1", [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_2 (- x)) x)"),
    ("abs_2", [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_3 (- x)) x)"),
    ("abs_3", [ ("n", "Int") ], "Int", "(ite (< x 0) (abs_1 (- x)) x)"),
] ).unwrap()

Declares mutually recursive datatypes.

A relatively recent version of z3 is recommended. Sort definition is a relatively expert action, this function is a bit complex. The example below goes over how it works.

Examples

use rsmt2::print::{AdtDecl, AdtVariantField, AdtVariant};

// Alright, so we're going to declare two mutually recursive sorts. It is easier to pack the
// sort-declaration data in custom types. If you want to declare a sort, you most likely
// already have a representation for it, so working on custom types is reasonable.

// Notice that the `AdtDecl`, `AdtVariantField` and `AdtVariant` traits from `rsmt2::print::_`
// are in scope. This is what our custom types will need to generate to declare the sort.

// We'll use static string slices for simplicity as `&str` implements all printing traits.
type Sym = &'static str;
type Sort = &'static str;

// Let's start with the top-level sort type.
struct MySort {
    // Name of the sort, for instance `List`.
    sym: Sym,
    // Symbol(s) for the type parameter(s), for instance `T` for `List<T>`. Must be a collection
    // of known length, because rsmt2 needs to access the arity (number of type parameters).
    args: Vec<Sym>,
    // Body of the sort: its variants. For instance the `nil` and `cons` variants for `List<T>`.
    variants: Vec<Variant>,
}
impl MySort {
    // This thing build the actual definition expected by rsmt2. Its output is something that
    // implements `AdtDecl` and can only live as long as the input ref to `self`.
    fn as_decl<'me>(&'me self) -> impl AdtDecl + 'me {
        // Check out rsmt2's documentation and you'll see that `AdtDecl` is already implemented for
        // certain triplets.
        (
            // Symbol.
            &self.sym,
            // Sized collection of type-parameter symbols.
            &self.args,
            // Variant, collection of iterator over `impl AdtVariant` (see below).
            self.variants.iter().map(Variant::as_decl),
        )
    }

    fn tree() -> Self {
        Self {
            sym: "Tree",
            args: vec!["T"],
            variants: vec![Variant::tree_leaf(), Variant::tree_node()],
        }
    }
}

// Next up, variants. A variant is a symbol (*e.g.* `nil` or `cons` for `List<T>`) and some
// fields which describe the data stored in the variant.
struct Variant {
    sym: Sym,
    fields: Vec<Field>,
}
impl Variant {
    // Variant declaration; again, `AdtVariant` is implemented for certain types of pairs.
    fn as_decl<'me>(&'me self) -> impl AdtVariant + 'me {
        (
            // Symbol.
            self.sym,
            // Iterator over field declarations.
            self.fields.iter().map(Field::as_decl),
        )
    }

    fn tree_leaf() -> Self {
        Self {
            sym: "leaf",
            fields: vec![],
        }
    }
    fn tree_node() -> Self {
        Self {
            sym: "node",
            fields: vec![Field::tree_node_value(), Field::tree_node_children()],
        }
    }
}

// A symbol and a sort: describes a piece of data in a variant with a symbol to retrieve it,
// *i.e.* the name of the field.
struct Field {
    sym: Sym,
    sort: Sort,
}
impl Field {
    // As usual, `AdtVariantField` is implemented for certain pairs.
    fn as_decl(&self) -> impl AdtVariantField {
        (self.sym, self.sort)
    }

    fn tree_node_value() -> Self {
        Self {
            sym: "value",
            sort: "T",
        }
    }
    fn tree_node_children() -> Self {
        Self {
            sym: "children",
            sort: "(TreeList T)",
        }
    }
}

let tree = MySort::tree();

// Now this `tree` uses an non-existing `(TreeList T)` sort to store its children, let's declare
// it now.

let nil = Variant {
    sym: "nil",
    fields: vec![],
};
let cons = Variant {
    sym: "cons",
    fields: vec![
        Field {
            sym: "car",
            sort: "(Tree T)",
        },
        Field {
            sym: "cdr",
            sort: "(TreeList T)",
        },
    ],
};
let tree_list = MySort {
    sym: "TreeList",
    args: vec!["T"],
    variants: vec![nil, cons],
};

let mut solver = rsmt2::Solver::default_z3(()).unwrap();

solver
    // These sort are mutually recursive, `Solver::declare_datatypes` needs to declare them at the
    // same time.
    .declare_datatypes(&[tree.as_decl(), tree_list.as_decl()])
    .unwrap();

// That's it! Solver now knows these sorts and we can use them.

solver.declare_const("t1", "(Tree Int)").unwrap();
solver.declare_const("t2", "(Tree Bool)").unwrap();

solver.assert("(> (value t1) 20)").unwrap();
solver.assert("(not (is-leaf t2))").unwrap();
solver.assert("(not (value t2))").unwrap();

let sat = solver.check_sat().unwrap();
assert!(sat);

Basic SMT-LIB commands using the user’s parser.

Get-model command.

Get-model command when all the symbols are nullary.

Get-values command.

Notice that the input expression type and the output one have no reason to be the same.

Get-unsat-core command.

Examples

use rsmt2::Solver;

let mut solver = Solver::default_z3(()).unwrap();

solver.declare_const("x", "Int").unwrap();
solver.declare_const("y", "Int").unwrap();

solver.assert("(= (+ x y) 0)").unwrap();

let future = solver.print_check_sat().unwrap();
// Do stuff while the solver works.
let sat = solver.parse_check_sat(future).unwrap();
assert!(sat);

Get-interpolant command.

Get-interpolant command.

Actlit-Related Functions.

See the actlit module for more details.

Introduces a new actlit.

See the actlit module for more details.

Deactivates an activation literal, alias for solver.set_actlit(actlit, false).

See the actlit module for more details.

Forces the value of an actlit and consumes it.

See the actlit module for more details.

Asserts an expression without print information, guarded by an activation literal.

See the actlit module for more details.

Check-sat command with activation literals, turns unknown results into errors.

Check-sat command with activation literals, turns unknown results in None.

SMT-LIB asynchronous commands.

Prints a check-sat command.

Allows to print the check-sat and get the result later, e.g. with Self::parse_check_sat.

See also

  • NamedExpr: a convenient wrapper around any expression that gives it a name.

Examples

use rsmt2::prelude::*;
let mut conf = SmtConf::default_z3();
conf.unsat_cores();

let mut solver = Solver::new(conf, ()).unwrap();
solver.declare_const("n", "Int").unwrap();
solver.declare_const("m", "Int").unwrap();

solver.assert("true").unwrap();

let e_1 = "(> n 7)";
let label_e_1 = "e_1";
let named = NamedExpr::new(label_e_1, e_1);
solver.assert(&named).unwrap();

let e_2 = "(> m 0)";
let label_e_2 = "e_2";
let named = NamedExpr::new(label_e_2, e_2);
solver.assert(&named).unwrap();

let e_3 = "(< n 3)";
let label_e_3 = "e_3";
let named = NamedExpr::new(label_e_3, e_3);
solver.assert(&named).unwrap();

assert!(!solver.check_sat().unwrap());
let core: Vec<String> = solver.get_unsat_core().unwrap();
assert_eq!(core, vec![label_e_1, label_e_3]);

Check-sat command, with actlits.

See the actlit module for more details.

Parse the result of a check-sat, turns unknown results into errors.

Parse the result of a check-sat, turns unknown results into None.

Get-interpolant command.

At the time of writing, only Z3 supports this command.

Check-sat with assumptions command with unit info.

Check-sat with assumptions command.

Non-blocking commands.

Asynchronous check-sat, see the asynch module for details.

This function is not unsafe in the sense that it cannot create undefined behavior. However, it is unsafe because the asynchronous check might end up running forever in the background, burning 100% CPU.

Sort-related SMT-LIB commands.

Declares a new sort.

Examples

let mut solver = Solver::default_z3(()).unwrap();
solver.declare_sort("A", 0).unwrap();
solver.declare_const("x", "A").unwrap();
solver.declare_const("y", "A").unwrap();
solver.declare_fun("f", & [ "A" ], "A").unwrap();
solver.assert("(= (f (f x)) x)").unwrap();
solver.assert("(= (f x) y)").unwrap();
solver.assert("(not (= x y))").unwrap();
let sat = solver.check_sat().unwrap();

Defines a new sort.

Examples

Note the use of Self::define_null_sort to avoid problems with empty arguments.

let mut solver = Solver::default_z3(()).unwrap();
solver.define_sort("MySet", & ["T"], "(Array T Bool)").unwrap();
solver.define_null_sort("IList", "(List Int)").unwrap();
solver.define_sort(
    "List-Set", & ["T"], "(Array (List T) Bool)"
).unwrap();
solver.define_null_sort("I", "Int").unwrap();

solver.declare_const("s1", "(MySet I)").unwrap();
solver.declare_const("s2", "(List-Set Int)").unwrap();
solver.declare_const("a", "I").unwrap();
solver.declare_const("l", "IList").unwrap();

solver.assert("(= (select s1 a) true)").unwrap();
solver.assert("(= (select s2 l) false)").unwrap();
let sat = solver.check_sat().unwrap();

Defines a new nullary sort.

When using Self::define_sort with empty args, rust complains because it does not know what the Arg type parameter is. This function addresses this problem by not having arguments.

SMT-LIB commands vehiculating user information.

Declares a new constant.

Declares a new function symbol.

Defines a new constant.

Defines a new function symbol.

Defines some new (possibily mutually) recursive functions.

Defines a new recursive function.

Asserts an expression with info, optional actlit and optional name.

Asserts an expression with an activation literal, a name and some print info.

Asserts an expression with some print information, guarded by an activation literal.

See the actlit module for more details.

Asserts an expression with some print information.

Asserts a named expression.

Asserts an expression with a name and some print info.

Check-sat assuming command, turns unknown results into errors.

Check-sat assuming command, turns unknown results into None.

Other commands.

Set option command.

Activates unsat core production.

Activates model production.

Resets the assertions in the solver.

Get info command.

Get option command.

Set info command.

Echo command.

Trait Implementations

Executes the destructor for this type. Read more

Pull some bytes from this source into the specified buffer, returning how many bytes were read. Read more

Like read, except that it reads into a slice of buffers. Read more

🔬 This is a nightly-only experimental API. (can_vector)

Determines if this Reader has an efficient read_vectored implementation. Read more

🔬 This is a nightly-only experimental API. (read_initializer)

Determines if this Reader can work with buffers of uninitialized memory. Read more

Read all bytes until EOF in this source, placing them into buf. Read more

Read all bytes until EOF in this source, appending them to buf. Read more

Read the exact number of bytes required to fill buf. Read more

Creates a “by reference” adapter for this instance of Read. Read more

Transforms this Read instance to an Iterator over its bytes. Read more

Creates an adapter which will chain this stream with another. Read more

Creates an adapter which will read at most limit bytes from it. Read more

Write a buffer into this writer, returning how many bytes were written. Read more

Flush this output stream, ensuring that all intermediately buffered contents reach their destination. Read more

Like write, except that it writes from a slice of buffers. Read more

🔬 This is a nightly-only experimental API. (can_vector)

Determines if this Writer has an efficient write_vectored implementation. Read more

Attempts to write an entire buffer into this writer. Read more

🔬 This is a nightly-only experimental API. (write_all_vectored)

Attempts to write multiple buffers into this writer. Read more

Writes a formatted string into this writer, returning any error encountered. Read more

Creates a “by reference” adapter for this instance of Write. Read more

Auto Trait Implementations

Blanket Implementations

Gets the TypeId of self. Read more

Immutably borrows from an owned value. Read more

Mutably borrows from an owned value. Read more

Performs the conversion.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.

The type returned in the event of a conversion error.

Performs the conversion.