Struct SmtEncoder 

pub(crate) struct SmtEncoder<T: Types> {
    options: SmtOptions,
    constructors: HashSet<T::Var>,
    datatypes: HashSet<T::Sort>,
}

Fields

options: SmtOptions

constructors: HashSet<T::Var>

datatypes: HashSet<T::Sort>

Implementations

impl<T: Types> SmtEncoder<T>

pub fn new(data_decls: &[DataDecl<T>], options: SmtOptions) -> Self

pub fn write_datatype_decl( &self, out: &mut impl Write, decl: &DataDecl<T>, ) -> Result

fn write_datatype_ctors( &self, out: &mut impl Write, decl: &DataDecl<T>, ) -> Result

pub fn write_const_decl( &self, out: &mut impl Write, name: &str, sort: &Sort<T>, ) -> Result

fn write_fun_signature( &self, out: &mut impl Write, name: &str, inputs: &[&Sort<T>], output: &Sort<T>, ) -> Result

pub fn write_fun_def(&self, out: &mut impl Write, fun: &FunDef<T>) -> Result

pub fn write_sort(&self, out: &mut impl Write, sort: &Sort<T>) -> Result

fn write_sort_in_scope( &self, out: &mut impl Write, sort: &Sort<T>, in_datatype_params: bool, ) -> Result

fn write_sort_ctor(&self, out: &mut impl Write, ctor: &SortCtor<T>) -> Result

pub fn pred(&self, pred: &Pred<T>) -> Result<String, Error>

pub fn write_pred(&self, out: &mut impl Write, pred: &Pred<T>) -> Result

pub fn expr(&self, expr: &Expr<T>) -> Result<String, Error>

fn write_weak_kvar(&self, out: &mut impl Write) -> Result

pub fn write_expr(&self, out: &mut impl Write, expr: &Expr<T>) -> Result

fn write_application_head( &self, out: &mut impl Write, fun: &Expr<T>, out_sort: Option<&Sort<T>>, ) -> Result

fn write_unary(&self, out: &mut impl Write, op: &str, expr: &Expr<T>) -> Result

fn write_binary( &self, out: &mut impl Write, op: &str, lhs: &Expr<T>, rhs: &Expr<T>, ) -> Result

fn write_nary( &self, out: &mut impl Write, op: &str, exprs: &[Expr<T>], empty: &str, ) -> Result

fn write_thy_func(&self, out: &mut impl Write, func: ThyFunc) -> Result