veri_engine_lib/
interp.rs

1/// Interpret and build an assumption context from the LHS and RHS of rules.
2use crate::type_inference::RuleSemantics;
3use veri_ir::{BoundVar, Expr};
4
5use std::collections::HashMap;
6use std::fmt::Debug;
7
8use cranelift_isle as isle;
9use isle::sema::{RuleId, VarId};
10
11/// Assumption consist of single verification IR expressions, which must have
12/// boolean type.
13#[derive(Clone, Debug)]
14pub struct Assumption {
15    assume: Expr,
16}
17
18impl Assumption {
19    /// Create a new assumption, checking type.
20    pub fn new(assume: Expr) -> Self {
21        // assert!(assume.ty().is_bool());
22        Self { assume }
23    }
24
25    /// Get the assumption as an expression.
26    pub fn assume(&self) -> &Expr {
27        &self.assume
28    }
29}
30pub struct Context<'ctx> {
31    pub quantified_vars: Vec<BoundVar>,
32    pub free_vars: Vec<BoundVar>,
33    pub assumptions: Vec<Assumption>,
34    pub var_map: HashMap<VarId, BoundVar>,
35
36    // For type checking
37    pub typesols: &'ctx HashMap<RuleId, RuleSemantics>,
38}
39
40impl<'ctx> Context<'ctx> {
41    pub fn new(typesols: &'ctx HashMap<RuleId, RuleSemantics>) -> Context<'ctx> {
42        Context {
43            quantified_vars: vec![],
44            free_vars: vec![],
45            assumptions: vec![],
46            var_map: HashMap::new(),
47            typesols,
48        }
49    }
50}
veri_engine_lib/interp.rs

veri_engine_lib/
interp.rs
