Struct 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 exit(&mut self) -> Result<()>

Instruct the solver to exit.

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<()>

pub fn raw_send(&mut self, cmd: SExpr) -> Result<()>

Directly send an expression to the solver.

You are responsible for reading the response, if any, from the solver by calling context.raw_recv() immediately after sending a message to the solver. Failing to call context.raw_recv() afterwards if the solver sends a response to your message, or calling it if the solver doesn’t send a response, will lead to general breakage such as dead locks, nonsensical query results, and more.

This is a low-level API and should be used sparingly, such as for solver-specific commands that this crate does not provide built-in support for. When possible, use the higher-level interfaces provided by this crate, for example by calling context.assert(foo) rather than context.raw_send(context.list([context.atom("assert"), foo])).

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

Directly receive a response from the solver.

This method should only be used immediately after calling context.raw_send(...), to receive the solver’s response to that sent message. Calling this method at other times, failing to call it when the solver sends a response, or calling it when the solver does not send a response, will lead to general breakage such as dead locks, nonsensical query results, and more.

This is a low-level API and should be used sparingly, such as for solver-specific commands that this crate does not provide built-in support for. When possible, use the higher-level interfaces provided by this crate, for example by calling context.assert(foo) rather than context.raw_send(context.list([context.atom("assert"), foo])).

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 get_atom(&self, expr: SExpr) -> Option<&str>

Get the atom data for the given s-expression.

This allows you to inspect s-expressions. If the s-expression is not an atom this function returns None.

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_str(&self, expr: SExpr) -> Option<&str>

Get the string data for the given s-expression.

This allows you to inspect s-expressions. If the s-expression is not an string this function returns None.

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_list(&self, expr: SExpr) -> Option<&[SExpr]>

Get the list data for the given s-expression.

This allows you to inspect s-expressions.If the s-expression is not an list this function returns None.

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_u8(&self, expr: SExpr) -> Option<u8>

Get the data for the given s-expression as an u8.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an u8 this function returns None.

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_u16(&self, expr: SExpr) -> Option<u16>

Get the data for the given s-expression as an u16.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an u16 this function returns None.

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_u32(&self, expr: SExpr) -> Option<u32>

Get the data for the given s-expression as an u32.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an u32 this function returns None.

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_u64(&self, expr: SExpr) -> Option<u64>

Get the data for the given s-expression as an u64.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an u64 this function returns None.

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_u128(&self, expr: SExpr) -> Option<u128>

Get the data for the given s-expression as an u128.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an u128 this function returns None.

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_usize(&self, expr: SExpr) -> Option<usize>

Get the data for the given s-expression as an usize.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an usize this function returns None.

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_i8(&self, expr: SExpr) -> Option<i8>

Get the data for the given s-expression as an i8.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an i8 this function returns None.

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_i16(&self, expr: SExpr) -> Option<i16>

Get the data for the given s-expression as an i16.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an i16 this function returns None.

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_i32(&self, expr: SExpr) -> Option<i32>

Get the data for the given s-expression as an i32.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an i32 this function returns None.

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_i64(&self, expr: SExpr) -> Option<i64>

Get the data for the given s-expression as an i64.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an i64 this function returns None.

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_i128(&self, expr: SExpr) -> Option<i128>

Get the data for the given s-expression as an i128.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an i128 this function returns None.

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_isize(&self, expr: SExpr) -> Option<isize>

Get the data for the given s-expression as an isize.

This allows you to inspect s-expressions. If the s-expression is not an cannot be parsed into an isize this function returns None.

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) -> SExpr

where 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) -> SExpr

where 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) -> SExpr

where 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) -> SExpr

where 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 bvsdiv(&self, lhs: SExpr, rhs: SExpr) -> SExpr

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

pub fn bvsmod(&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

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