Skip to main content

prune_lang/interp/solver/
no_smt.rs

1use super::*;
2
3pub struct NoSmtSolver;
4
5impl NoSmtSolver {
6    pub fn new() -> Self {
7        NoSmtSolver
8    }
9}
10
11impl Default for NoSmtSolver {
12    fn default() -> Self {
13        Self::new()
14    }
15}
16
17impl common::PrimSolver for NoSmtSolver {
18    fn check_sat(
19        &mut self,
20        prims: &[(Prim, Vec<AtomVal<IdentCtx>>)],
21    ) -> Option<HashMap<IdentCtx, LitVal>> {
22        if prims.is_empty() {
23            Some(HashMap::new())
24        } else {
25            None
26        }
27    }
28}