karpal_verify/
smt.rs

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

karpal_verify/
smt.rs
