karpal_verify/
smt.rs

1#[cfg(not(feature = "std"))]
2use alloc::{
3    format,
4    string::{String, ToString},
5    vec::Vec,
6};
7#[cfg(feature = "std")]
8use std::{format, string::String, vec::Vec};
9
10use crate::{
11    Obligation, ObligationBundle,
12    obligation::{Sort, Term},
13};
14
15/// Marker for the SMT-LIB2 backend.
16pub struct SmtLib2;
17
18impl SmtLib2 {
19    /// Export a single obligation as an SMT-LIB2 script.
20    pub fn export(obligation: &Obligation) -> String {
21        export_obligation(obligation)
22    }
23
24    /// Export a bundle as one SMT-LIB2 script per obligation.
25    pub fn export_bundle(bundle: &ObligationBundle) -> Vec<(String, String)> {
26        bundle
27            .obligations()
28            .iter()
29            .map(|obligation| (obligation.name.clone(), export_obligation(obligation)))
30            .collect()
31    }
32}
33
34pub fn export_obligation(obligation: &Obligation) -> String {
35    let mut lines = Vec::new();
36    lines.push(format!("; obligation: {}", obligation.name));
37    lines.push(format!("; property: {}", obligation.property));
38    lines.push(format!("; origin: {}", obligation.summary()));
39    lines.push("(set-logic ALL)".to_string());
40
41    for declaration in &obligation.declarations {
42        lines.push(format!(
43            "(declare-const {} {})",
44            declaration.name,
45            render_sort(&declaration.sort)
46        ));
47    }
48
49    for assumption in &obligation.assumptions {
50        lines.push(format!("(assert {})", render_term(assumption)));
51    }
52
53    lines.push("; ask the solver for a counterexample to the law".to_string());
54    lines.push(format!(
55        "(assert (not {}))",
56        render_term(&obligation.conclusion)
57    ));
58    lines.push("(check-sat)".to_string());
59    lines.push("(get-model)".to_string());
60    lines.join("\n")
61}
62
63fn render_sort(sort: &Sort) -> String {
64    match sort {
65        Sort::Bool => "Bool".to_string(),
66        Sort::Int => "Int".to_string(),
67        Sort::Real => "Real".to_string(),
68        Sort::Named(name) => name.clone(),
69    }
70}
71
72fn render_term(term: &Term) -> String {
73    match term {
74        Term::Var(name) => name.clone(),
75        Term::Bool(true) => "true".to_string(),
76        Term::Bool(false) => "false".to_string(),
77        Term::Int(value) => value.to_string(),
78        Term::App { function, args } => {
79            if args.is_empty() {
80                function.clone()
81            } else {
82                format!(
83                    "({} {})",
84                    function,
85                    args.iter().map(render_term).collect::<Vec<_>>().join(" ")
86                )
87            }
88        }
89        Term::Eq(left, right) => format!("(= {} {})", render_term(left), render_term(right)),
90        Term::And(terms) => match terms.as_slice() {
91            [] => "true".to_string(),
92            [term] => render_term(term),
93            _ => format!(
94                "(and {})",
95                terms.iter().map(render_term).collect::<Vec<_>>().join(" ")
96            ),
97        },
98        Term::Or(terms) => match terms.as_slice() {
99            [] => "false".to_string(),
100            [term] => render_term(term),
101            _ => format!(
102                "(or {})",
103                terms.iter().map(render_term).collect::<Vec<_>>().join(" ")
104            ),
105        },
106        Term::Not(inner) => format!("(not {})", render_term(inner)),
107        Term::Implies(lhs, rhs) => format!("(=> {} {})", render_term(lhs), render_term(rhs)),
108    }
109}
110
111#[cfg(test)]
112mod tests {
113    use super::*;
114    use crate::obligation::{Origin, VerificationTier};
115    use karpal_proof::IsAssociative;
116
117    #[test]
118    fn exports_declarations_and_negated_goal() {
119        let obligation = Obligation::for_property::<IsAssociative>(
120            "assoc",
121            Origin::new("karpal-core", "Semigroup for i32"),
122            VerificationTier::External,
123            Term::eq(Term::var("x"), Term::var("y")),
124        )
125        .with_decl("x", Sort::Int)
126        .with_decl("y", Sort::Int);
127
128        let text = export_obligation(&obligation);
129        assert!(text.contains("(declare-const x Int)"));
130        assert!(text.contains("(assert (not (= x y)))"));
131        assert!(text.contains("(check-sat)"));
132    }
133}
karpal_verify/smt.rs

karpal_verify/
smt.rs
