Struct uvls::smt::smt_lib::SMTModule

pub struct SMTModule {
    pub variables: IndexSet<ModuleSymbol>,
    pub asserts: Vec<Assert>,
}

This is a helper module, to use SMT (and in that sense Z3) for every UVL Module A smt-lib module equivalent to some UVL source module.

Fields

variables: IndexSet<ModuleSymbol>

asserts: Vec<Assert>

Implementations

impl SMTModule

pub fn parse_model<'a>( &'a self, model: &'a str, ) -> impl Iterator<Item = (ModuleSymbol, ConfigValue)> + 'a

pub fn parse_values<'a>( &'a self, values: &'a str, module: &'a Module, ) -> impl Iterator<Item = (ModuleSymbol, ConfigValue)> + 'a

extract values from a response string

pub fn parse_unsat_core<'a>( &'a self, core: &'a str, ) -> impl Iterator<Item = AssertInfo> + 'a

pub fn config_to_source(&self) -> String

create source to config z3 Solver

pub fn variable_to_source(&self, module: &Module) -> String

create with all Variable the source for the SMTSolver

pub fn assert_to_source( &self, i: usize, info: &Option<AssertInfo>, expr: &Expr, not: bool, ) -> String

create the source for an assert, if the assert should be negated the variable neg must be true

pub fn to_source(&self, module: &Module) -> String

tree to source

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

pub fn pseudo_bool(&self, ms: ModuleSymbol, module: &Module) -> String