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 = format!("v{}", 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 (i, var) in arena.vars.iter().enumerate() {
38        let name = format!("v{}", i);
39        let ScopedVar(v, depth) = var;
40        let orig_name = match v {
41            Var::Free(s) => s.clone(),
42            Var::Bound(idx) => format!("b{}", idx),
43        };
44        out.push_str(&format!("; original variable: {} depth: {}\n", escape_smt_string(&orig_name), depth));
45        out.push_str(&format!("(declare-fun {} () Int)\n", name));
46    }
47    out.push_str("\n");
48
49    // Assert constraints
50    // Edge (u, v, w) means d[v] <= d[u] + w
51    for &(u, v, w, _) in &arena.edges {
52        let u_name = format!("v{}", u);
53        let v_name = format!("v{}", v);
54        out.push_str(&format!("(assert (<= (- {} {}) {}))\n", v_name, u_name, w));
55    }
56
57    out.push_str("\n(check-sat)\n");
58    out.push_str("(get-model)\n");
59    out.push_str("; === END STRATIFICATION WITNESS ===\n");
60
61    out
62}
63
64fn escape_smt_string(s: &str) -> String {
65    s.replace("\"", "\"\"")
66}
monist_core/smt.rs

monist_core/
smt.rs
