Struct easy_smt::Context

pub struct Context { /* private fields */ }

An SMT-LIB 2 context, usually backed by a solver subprocess.

Created via a ContextBuilder.

Implementations

impl Context

Solver Commands and Assertions

These methods send a command or assertion to the context’s underlying solver. As such, they involve I/O with a subprocess and are therefore fallible.

Panics

These methods will panic when called if the context was not created with an underlying solver (via ContextBuilder::solver).

pub fn set_option<K>(&mut self, name: K, value: SExpr) -> Result<()>where K: Into<String> + AsRef<str>,

pub fn check_assuming( &mut self, props: impl IntoIterator<Item = SExpr> ) -> Result<Response>

Assert check-sat-assuming with the given list of assumptions.

pub fn check(&mut self) -> Result<Response>

Assert check-sat for the current context.

pub fn declare_const<S: Into<String> + AsRef<str>>( &mut self, name: S, sort: SExpr ) -> Result<SExpr>

Declare a new constant with the provided sort

pub fn declare_datatype<S: Into<String> + AsRef<str>>( &mut self, name: S, decl: SExpr ) -> Result<SExpr>

pub fn declare_datatypes<N, S, D>(&mut self, sorts: S, decls: D) -> Result<()>where N: Into<String> + AsRef<str>, S: IntoIterator<Item = (N, i32)>, D: IntoIterator<Item = SExpr>,

pub fn declare_fun<S: Into<String> + AsRef<str>>( &mut self, name: S, args: Vec<SExpr>, out: SExpr ) -> Result<SExpr>

Declares a new, uninterpreted function symbol.

pub fn define_fun<S: Into<String> + AsRef<str>>( &mut self, name: S, args: Vec<(S, SExpr)>, out: SExpr, body: SExpr ) -> Result<SExpr>

Defines a new function with a body.

pub fn define_const<S: Into<String> + AsRef<str>>( &mut self, name: S, out: SExpr, body: SExpr ) -> Result<SExpr>

Define a constant with a body with a value. This is a convenience wrapper over Self::define_fun since constants are nullary functions.

pub fn declare_sort<S: Into<String> + AsRef<str>>( &mut self, symbol: S, arity: i32 ) -> Result<SExpr>

pub fn assert(&mut self, expr: SExpr) -> Result<()>

pub fn get_model(&mut self) -> Result<SExpr>

Get a model out from the solver. This is only meaningful after a check-sat query.

pub fn get_value(&mut self, vals: Vec<SExpr>) -> Result<Vec<(SExpr, SExpr)>>

Get bindings for values in the model. This is only meaningful after a check-sat query.

pub fn get_unsat_core(&mut self) -> Result<SExpr>

Returns the names of the formulas involved in a contradiction.

pub fn set_logic<L: Into<String> + AsRef<str>>( &mut self, logic: L ) -> Result<()>

pub fn push(&mut self) -> Result<()>

Push a new context frame in the solver. Same as SMTLIB’s push command.

pub fn push_many(&mut self, n: usize) -> Result<()>

pub fn pop(&mut self) -> Result<()>

Pop a context frame in the solver. Same as SMTLIB’s pop command.

pub fn pop_many(&mut self, n: usize) -> Result<()>

impl Context

Basic S-Expression Construction and Inspection

These methods provide the foundation of building s-expressions. Even if you end up using higher-level helper methods most of the time, everything bottoms out in calls to these methods.

pub fn atom(&self, name: impl Into<String> + AsRef<str>) -> SExpr

Construct a non-list s-expression from the given string.

pub fn list(&self, list: Vec<SExpr>) -> SExpr

Construct a list s-expression from the given elements.

pub fn numeral(&self, val: impl IntoNumeral) -> SExpr

Create a numeral s-expression.

pub fn decimal(&self, val: impl IntoDecimal) -> SExpr

Create a decimal s-expression.

pub fn binary(&self, bit_width: usize, val: impl IntoBinary) -> SExpr

Create a binary s-expression of the given bit width.

pub fn display(&self, expr: SExpr) -> DisplayExpr<'_>

Get a std::fmt::Display representation of the given s-expression.

This allows you to print, log, or otherwise format an s-expression creating within this context.

You may only pass in SExprs that were created by this Context. Failure to do so is safe, but may trigger a panic or return invalid data.

pub fn get(&self, expr: SExpr) -> SExprData<'_>

Get the atom or list data for the given s-expression.

This allows you to inspect s-expressions.

You may only pass in SExprs that were created by this Context. Failure to do so is safe, but may trigger a panic or return invalid data.

pub fn atoms(&self) -> &KnownAtoms

Access “known” atoms.

This lets you skip the is-it-already-interned-or-not checks and hash map lookups for certain frequently used atoms.

impl Context

Generic and Polymorphic Helpers

Helpers for constructing s-expressions that are not specific to one sort.

pub fn par<N, S, D>(&self, symbols: S, decls: D) -> SExprwhere N: Into<String> + AsRef<str>, S: IntoIterator<Item = N>, D: IntoIterator<Item = SExpr>,

pub fn attr( &self, expr: SExpr, name: impl Into<String> + AsRef<str>, val: SExpr ) -> SExpr

pub fn named(&self, name: impl Into<String> + AsRef<str>, expr: SExpr) -> SExpr

pub fn let_<N: Into<String> + AsRef<str>>( &self, name: N, e: SExpr, body: SExpr ) -> SExpr

A let-declaration with a single binding.

pub fn let_many<N, I>(&self, bindings: I, body: SExpr) -> SExprwhere I: IntoIterator<Item = (N, SExpr)>, N: Into<String> + AsRef<str>,

A let-declaration of multiple bindings.

pub fn forall<N, I>(&self, vars: I, body: SExpr) -> SExprwhere I: IntoIterator<Item = (N, SExpr)>, N: Into<String> + AsRef<str>,

Universally quantify sorted variables in an expression.

pub fn exists<N, I>(&self, vars: I, body: SExpr) -> SExprwhere I: IntoIterator<Item = (N, SExpr)>, N: Into<String> + AsRef<str>,

Existentially quantify sorted variables in an expression.

pub fn match_<I: IntoIterator<Item = (SExpr, SExpr)>>( &self, term: SExpr, arms: I ) -> SExpr

Perform pattern matching on values of an algebraic data type.

pub fn ite(&self, c: SExpr, t: SExpr, e: SExpr) -> SExpr

Construct an if-then-else expression.

impl Context

Bool Helpers

These methods help you construct s-expressions for various bool operations.

pub fn bool_sort(&self) -> SExpr

The Bool sort.

pub fn true_(&self) -> SExpr

The true constant.

pub fn false_(&self) -> SExpr

The false constant.

pub fn not(&self, val: SExpr) -> SExpr

pub fn imp(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn imp_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn and(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn and_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn or(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn or_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn xor(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn xor_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn eq(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn eq_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn distinct(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn distinct_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

impl Context

Int Helpers

These methods help you construct s-expressions for various int operations.

pub fn int_sort(&self) -> SExpr

The Int sort.

pub fn negate(&self, val: SExpr) -> SExpr

pub fn sub(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn sub_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn plus(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn plus_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn times(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn times_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn div(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn div_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn modulo(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn modulo_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn rem(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn rem_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn lte(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn lte_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn lt(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn lt_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn gt(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn gt_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn gte(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn gte_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

impl Context

Array Helpers

These methods help you construct s-expressions for various array operations.

pub fn array_sort(&self, index: SExpr, element: SExpr) -> SExpr

Construct the array sort with the given index and element types.

pub fn select(&self, ary: SExpr, index: SExpr) -> SExpr

Select the element at the given index in the array.

pub fn store(&self, ary: SExpr, index: SExpr, value: SExpr) -> SExpr

Store the value into the given index in the array, yielding a new array.

impl Context

Bit Vector Helpers

These methods help you construct s-expressions for various bit vector operations.

pub fn bit_vec_sort(&self, width: SExpr) -> SExpr

Construct a BitVec sort with the given width.

pub fn concat(&self, lhs: SExpr, rhs: SExpr) -> SExpr

Concatenate two bit vectors.

pub fn extract(&self, i: i32, j: i32, bv: SExpr) -> SExpr

Extract a range from a bit vector.

pub fn bvnot(&self, val: SExpr) -> SExpr

pub fn bvor(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvor_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn bvand(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvand_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn bvnand(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvnand_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn bvxor(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvxor_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn bvxnor(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvxnor_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn bvneg(&self, val: SExpr) -> SExpr

pub fn bvadd(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvadd_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn bvsub(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvmul(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvmul_many<I: IntoIterator<Item = SExpr>>(&self, items: I) -> SExpr

pub fn bvudiv(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvurem(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvsrem(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvshl(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvlshr(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvashr(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvule(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvult(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvuge(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvugt(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvsle(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvslt(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvsge(&self, lhs: SExpr, rhs: SExpr) -> SExpr

pub fn bvsgt(&self, lhs: SExpr, rhs: SExpr) -> SExpr