monist_core/
smt.rs

1use crate::ast::Var;
2use crate::graph::{GraphArena, ScopedVar};
3
4pub fn export_smt_lib(
5    arena: &GraphArena,
6    formula_name: &str,
7    collision_trace: Option<&str>,
8    sc_actions: &[String],
9    success_depths: Option<&[i32]>,
10) -> String {
11    let mut out = String::new();
12
13    out.push_str("; === BEGIN STRATIFICATION WITNESS ===\n");
14    out.push_str(&format!("(set-info :formula-name \"{}\")\n", escape_smt_string(formula_name)));
15
16    if let Some(trace) = collision_trace {
17        out.push_str(&format!("(set-info :extensionality-collision-trace \"{}\")\n", escape_smt_string(trace)));
18    }
19
20    if !sc_actions.is_empty() {
21        let actions_str = sc_actions.join("\n");
22        out.push_str(&format!("(set-info :sc-daemon-actions \"{}\")\n", escape_smt_string(&actions_str)));
23    }
24
25    if let Some(depths) = success_depths {
26        let mut depth_str = String::new();
27        for (i, d) in depths.iter().enumerate() {
28            let var_name = var_to_smt_name(&arena.vars[i]);
29            depth_str.push_str(&format!("{} -> {}\n", var_name, d));
30        }
31        out.push_str(&format!("(set-info :stratification-success-depths \"{}\")\n", escape_smt_string(depth_str.trim_end())));
32    }
33
34    out.push_str("(set-logic QF_LIA)\n\n");
35
36    // Declare variables
37    for var in &arena.vars {
38        let name = var_to_smt_name(var);
39        out.push_str(&format!("(declare-fun {} () Int)\n", name));
40    }
41    out.push_str("\n");
42
43    // Assert constraints
44    // Edge (u, v, w) means d[v] <= d[u] + w
45    for &(u, v, w, _) in &arena.edges {
46        let u_name = var_to_smt_name(&arena.vars[u]);
47        let v_name = var_to_smt_name(&arena.vars[v]);
48        out.push_str(&format!("(assert (<= (- {} {}) {}))\n", v_name, u_name, w));
49    }
50
51    out.push_str("\n(check-sat)\n");
52    out.push_str("(get-model)\n");
53    out.push_str("; === END STRATIFICATION WITNESS ===\n");
54
55    out
56}
57
58fn var_to_smt_name(var: &ScopedVar) -> String {
59    let ScopedVar(v, depth) = var;
60    let base_name = match v {
61        Var::Free(s) => s.clone(),
62        Var::Bound(idx) => format!("b{}", idx),
63    };
64    format!("{}_d{}", base_name, depth)
65}
66
67fn escape_smt_string(s: &str) -> String {
68    s.replace("\"", "\"\"")
69}
monist_core/smt.rs

monist_core/
smt.rs
