monist_core/
lib.rs

1pub mod ast;
2pub mod eval;
3pub mod graph;
4pub mod smt;
5pub mod budget;
6
7#[cfg(test)]
8mod tests {
9    use super::*;
10    use ast::{Atomic, Formula, FormulaArena, Var};
11    use graph::{GraphArena, ScopedVar};
12    use budget::ResourceBudget;
13
14    #[test]
15    fn test_tarjan_scc_0_weight() {
16        let mut graph = GraphArena::new();
17        let v0 = ScopedVar(Var::Free("x".to_string()), 0);
18        let v1 = ScopedVar(Var::Free("y".to_string()), 0);
19        let v2 = ScopedVar(Var::Free("z".to_string()), 0);
20
21        let i0 = graph.add_var(v0);
22        let i1 = graph.add_var(v1);
23        let i2 = graph.add_var(v2);
24
25        graph.edges.push((i0, i1, 0, false));
26        graph.edges.push((i1, i0, 0, false));
27        graph.edges.push((i0, i2, 1, false));
28
29        let sccs = graph.tarjan_scc();
30        let scc_0_1 = sccs.iter().find(|scc| scc.contains(&i0) && scc.contains(&i1));
31        assert!(scc_0_1.is_some(), "Expected i0 and i1 in the same SCC");
32
33        let (c_vars, _, reps) = graph.contract_graph(&sccs);
34        assert_eq!(reps[i0], reps[i1], "i0 and i1 must share representatives");
35        assert_eq!(c_vars.len(), 2, "Expected 2 contracted vertices");
36    }
37
38    #[test]
39    fn test_dnf_disjunction_branching() {
40        let mut arena = FormulaArena::new();
41        let x_in_x = arena.add(Formula::Atom(Atomic::Mem(Var::Free("x".to_string()), Var::Free("x".to_string()))));
42        let x_in_y = arena.add(Formula::Atom(Atomic::Mem(Var::Free("x".to_string()), Var::Free("y".to_string()))));
43        let disj = arena.add(Formula::Disj(x_in_x, x_in_y));
44
45        let res = GraphArena::evaluate_dnf_formula(&arena, disj, &ResourceBudget::default());
46        assert!(res.is_ok(), "Disjunction with one stratifiable branch must succeed");
47    }
48
49    #[test]
50    fn test_extensionality_collision_negative_cycle() {
51        let mut arena = FormulaArena::new();
52        let x_in_x = arena.add(Formula::Atom(Atomic::Mem(Var::Free("x".to_string()), Var::Free("x".to_string()))));
53        let x_notin_x = arena.add(Formula::Neg(x_in_x));
54        let comp = arena.add(Formula::Comp(0, "x".to_string(), x_notin_x));
55
56        let res = GraphArena::evaluate_dnf_formula(&arena, comp, &ResourceBudget::default());
57        assert!(res.is_err(), "Russell comprehension must fail with Extensionality Collision");
58    }
59
60    #[test]
61    fn test_smt_export_validity() {
62        let mut graph = GraphArena::new();
63        let v0 = ScopedVar(Var::Free("a".to_string()), 0);
64        let v1 = ScopedVar(Var::Free("b".to_string()), 0);
65        let i0 = graph.add_var(v0);
66        let i1 = graph.add_var(v1);
67        graph.edges.push((i0, i1, 1, false));
68
69        let smt = smt::export_smt_lib(&graph, "test_formula", None, &[], Some(&[0, 1]));
70        assert!(smt.contains("(set-logic QF_LIA)"));
71        assert!(smt.contains("(declare-fun v0 () Int)"));
72        assert!(smt.contains("(declare-fun v1 () Int)"));
73        assert!(smt.contains("(check-sat)"));
74    }
75}
monist_core/lib.rs

monist_core/
lib.rs
