karpal_verify/
smt.rs

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

karpal_verify/
smt.rs
