prune_lang/interp/solver/
common.rs

1use super::*;
2
3pub trait PrimSolver {
4    fn check_sat(
5        &mut self,
6        prims: &[(Prim, Vec<AtomVal<IdentCtx>>)],
7    ) -> Option<HashMap<IdentCtx, LitVal>>;
8}
9
10#[derive(Copy, Clone, Debug, PartialEq, Eq)]
11pub enum SolverBackend {
12    Z3,
13    CVC5,
14}
15
16pub fn infer_type(prims: &[(Prim, Vec<AtomVal<IdentCtx>>)]) -> HashMap<IdentCtx, LitType> {
17    let mut map = HashMap::new();
18
19    for (prim, args) in prims.iter() {
20        for (arg, typ) in args.iter().zip(prim.get_typ().iter()) {
21            match arg {
22                Term::Var(var) => {
23                    if let Some(res) = map.get(var) {
24                        assert_eq!(*res, *typ);
25                    } else {
26                        map.insert(*var, *typ);
27                    }
28                }
29                Term::Lit(lit) => {
30                    assert_eq!(lit.get_typ(), *typ);
31                }
32                Term::Cons(_, _) => unreachable!(),
33            }
34        }
35    }
36
37    map
38}
prune_lang/interp/solver/common.rs

prune_lang/interp/solver/
common.rs
