Struct Smt

pub struct Smt<'a> { /* private fields */ }

Implementations

impl<'a> Smt<'a>

pub fn new( problem: &'a Problem, cfg: &'a Config, ctx: &'a Context, solver: &'a Z3Solver<'a>, ) -> Self

pub fn problem(&self) -> &Problem

pub fn ctx(&self) -> &'a Context

pub fn solver(&self) -> &Z3Solver<'_>

pub fn struc_instance(&self, id: InstanceId) -> &Datatype<'a>

pub fn class_sort(&self, id: ClassId) -> &Sort<'a>

pub fn class_object(&self, instance: &Instance) -> Datatype<'a>

pub fn bool_variable(&self, id: VariableId) -> &Bool<'a>

pub fn int_variable(&self, id: VariableId) -> &Int<'a>

pub fn real_variable(&self, id: VariableId) -> &Real<'a>

pub fn datatype_variable(&self, id: VariableId) -> &Datatype<'a>

pub fn function(&self, id: FunctionId) -> &FuncDecl<'a>

pub fn constraint(&self, id: ConstraintId) -> &Bool<'a>

pub fn to_bool(&self, expr: &Expr) -> Bool<'a>

pub fn to_int(&self, expr: &Expr) -> Int<'a>

pub fn to_real(&self, expr: &Expr) -> Real<'a>

pub fn to_datatype(&self, expr: &Expr) -> Datatype<'a>

pub fn init(&mut self)

pub fn solver_to_entry(&self) -> Entry

pub fn model_to_entry(&self) -> Entry