Struct Solver 

pub struct Solver { /* private fields */ }

Implementations

impl Solver

pub fn new(backend: SmtBackend) -> Solver

pub fn is_empty(&self) -> bool

pub fn reset(&mut self)

pub fn savepoint(&mut self)

pub fn backtrack(&mut self)

impl Solver

pub fn declare(&mut self, var: &IdentCtx, typ: &TypeId)

pub fn unify(&mut self, lhs: TermCtx, rhs: TermCtx) -> Option<()>

pub fn push_cons(&mut self, prim: Prim, args: Vec<AtomCtx>)

pub fn check_complete(&mut self) -> bool

pub fn check_sound(&mut self) -> bool

pub fn get_value(&mut self, vars: &[IdentCtx]) -> Vec<TermCtx>

Trait Implementations

impl Display for Solver

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.