Struct SolverCtx

pub struct SolverCtx {
    pub find_widths: bool,
    pub bitwidth: usize,
    pub additional_decls: Vec<(String, SExpr)>,
    pub additional_assumptions: Vec<SExpr>,
    pub additional_assertions: Vec<SExpr>,
    /* private fields */
}

Fields

find_widths: bool

bitwidth: usize

additional_decls: Vec<(String, SExpr)>

additional_assumptions: Vec<SExpr>

additional_assertions: Vec<SExpr>

Implementations

impl SolverCtx

pub fn new_fresh_bits(&mut self, width: usize) -> SExpr

pub fn widen_to_register_width( &mut self, tyvar: u32, narrow_width: usize, narrow_decl: SExpr, name: Option<String>, ) -> SExpr

pub fn get_expr_width_var(&self, e: &Expr) -> Option<SExpr>

pub fn vir_to_smt_ty(&self, ty: &Type) -> SExpr

pub fn get_type(&self, x: &Expr) -> Option<&Type>

pub fn get_expr_value(&self, e: &Expr) -> Option<i128>

pub fn static_width(&self, x: &Expr) -> Option<usize>

pub fn assume_same_width(&mut self, x: &Expr, y: &Expr)

pub fn assume_same_width_from_sexpr(&mut self, x: SExpr, y: &Expr)

pub fn assume_comparable_types(&mut self, x: &Expr, y: &Expr)

pub fn vir_expr_to_sexp(&mut self, e: Expr) -> SExpr