Struct uvls::smt::smt_lib::SMTBuilder

struct SMTBuilder<'a> {
    sym2var: IndexSet<ModuleSymbol>,
    assert: Vec<Assert>,
    module: &'a Module,
}

Fields

sym2var: IndexSet<ModuleSymbol>

Each variable is encoded as v{n} where n is an index into sym2var using an IndexSet enables us to lookup a variable both by index and ModuleSymbol

assert: Vec<Assert>

module: &'a Module

Implementations

impl<'a> SMTBuilder<'a>

fn var(&self, ms: ModuleSymbol) -> Expr

fn pseudo_bool(&self, ms: ModuleSymbol) -> Expr

fn clause(&self, g: ModuleSymbol) -> Vec<Expr>

fn min_assert(&mut self, min: usize, p_bind: &Expr, g: ModuleSymbol)

fn max_assert(&mut self, max: usize, p_bind: &Expr, g: ModuleSymbol)

fn push_var(&mut self, ms: ModuleSymbol) -> Expr