## Coverage Report

#### Created: 2025-09-08 21:26

next uncovered line (L), next uncovered region (R), next uncovered branch (B)

    /home/noah/src/ruchy/src/proving/smt.rs

    Line
    Count
    Source
    1
    //! SMT solver integration for proof automation
    2
    3
    use anyhow::Result;
    4
    use serde::{Deserialize, Serialize};
    5
    use std::collections::HashMap;
    6
    use std::process::{Command, Stdio};
    7
    use std::io::Write;
    8
    9
    /// SMT solver backend
    10
    #[derive(Debug, Clone, Copy, PartialEq, Eq)]
    11
    pub enum SmtBackend {
    12
        Z3,
    13
        CVC5,
    14
        Yices2,
    15
        MathSAT,
    16
    }
    17
    18
    impl SmtBackend {
    19
        /// Get command for solver
    20
    0
        fn command(&self) -> &str {
    21
    0
            match self {
    22
    0
                Self::Z3 => "z3",
    23
    0
                Self::CVC5 => "cvc5",
    24
    0
                Self::Yices2 => "yices-smt2",
    25
    0
                Self::MathSAT => "mathsat",
    26
            }
    27
    0
        }
    28
    29
        /// Get command arguments
    30
    0
        fn args(&self) -> Vec<&str> {
    31
    0
            match self {
    32
    0
                Self::Z3 => vec!["-in", "-smt2"],
    33
    0
                Self::CVC5 => vec!["--lang", "smt2", "--incremental"],
    34
    0
                Self::Yices2 => vec!["--incremental"],
    35
    0
                Self::MathSAT => vec!["-input=smt2"],
    36
            }
    37
    0
        }
    38
    }
    39
    40
    /// SMT solver interface
    41
    pub struct SmtSolver {
    42
        backend: SmtBackend,
    43
        timeout_ms: u64,
    44
        assertions: Vec<String>,
    45
        declarations: HashMap<String, String>,
    46
    }
    47
    48
    impl SmtSolver {
    49
        /// Create new SMT solver
    50
    0
        pub fn new(backend: SmtBackend) -> Self {
    51
    0
            Self {
    52
    0
                backend,
    53
    0
                timeout_ms: 5000,
    54
    0
                assertions: Vec::new(),
    55
    0
                declarations: HashMap::new(),
    56
    0
            }
    57
    0
        }
    58
    59
        /// Set timeout
    60
    0
        pub fn set_timeout(&mut self, timeout_ms: u64) {
    61
    0
            self.timeout_ms = timeout_ms;
    62
    0
        }
    63
    64
        /// Declare a variable
    65
    0
        pub fn declare_var(&mut self, name: &str, sort: &str) {
    66
    0
            self.declarations.insert(
    67
    0
                name.to_string(),
    68
    0
                format!("(declare-fun {name} () {sort})")
    69
            );
    70
    0
        }
    71
    72
        /// Declare a function
    73
    0
        pub fn declare_fun(&mut self, name: &str, params: &[&str], ret: &str) {
    74
    0
            let params_str = params.join(" ");
    75
    0
            self.declarations.insert(
    76
    0
                name.to_string(),
    77
    0
                format!("(declare-fun {name} ({params_str}) {ret})")
    78
            );
    79
    0
        }
    80
    81
        /// Add an assertion
    82
    0
        pub fn assert(&mut self, expr: &str) {
    83
    0
            self.assertions.push(format!("(assert {expr})"));
    84
    0
        }
    85
    86
        /// Check satisfiability
    87
    0
        pub fn check_sat(&self) -> Result<SmtResult> {
    88
    0
            let query = self.build_query("(check-sat)");
    89
    0
            self.execute_query(&query)
    90
    0
        }
    91
    92
        /// Get model (if sat)
    93
    0
        pub fn get_model(&self) -> Result<Option<HashMap<String, String>>> {
    94
    0
            let query = self.build_query("(check-sat)\n(get-model)");
    95
    0
            let result = self.execute_query(&query)?;
    96
    97
    0
            if result == SmtResult::Sat {
    98
    0
                Ok(Some(self.parse_model(&query)?))
    99
            } else {
    100
    0
                Ok(None)
    101
            }
    102
    0
        }
    103
    104
        /// Check validity (prove formula)
    105
    0
        pub fn prove(&self, formula: &str) -> Result<SmtResult> {
    106
    0
            let mut solver = self.clone();
    107
    0
            solver.assert(&format!("(not {formula})"));
    108
    109
    0
            match solver.check_sat()? {
    110
    0
                SmtResult::Unsat => Ok(SmtResult::Valid),
    111
    0
                SmtResult::Sat => Ok(SmtResult::Invalid),
    112
    0
                other => Ok(other),
    113
            }
    114
    0
        }
    115
    116
        /// Build complete SMT-LIB2 query
    117
    0
        fn build_query(&self, command: &str) -> String {
    118
    0
            let mut query = String::new();
    119
    120
    0
            query.push_str("(set-logic ALL)\n");
    121
    0
            query.push_str(&format!("(set-option :timeout {})\n", self.timeout_ms));
    122
    123
    0
            for decl in self.declarations.values() {
    124
    0
                query.push_str(decl);
    125
    0
                query.push('\n');
    126
    0
            }
    127
    128
    0
            for assertion in &self.assertions {
    129
    0
                query.push_str(assertion);
    130
    0
                query.push('\n');
    131
    0
            }
    132
    133
    0
            query.push_str(command);
    134
    0
            query.push('\n');
    135
    0
            query.push_str("(exit)\n");
    136
    137
    0
            query
    138
    0
        }
    139
    140
        /// Execute query via solver process
    141
    0
        fn execute_query(&self, query: &str) -> Result<SmtResult> {
    142
    0
            let mut child = Command::new(self.backend.command())
    143
    0
                .args(self.backend.args())
    144
    0
                .stdin(Stdio::piped())
    145
    0
                .stdout(Stdio::piped())
    146
    0
                .stderr(Stdio::piped())
    147
    0
                .spawn()?;
    148
    149
    0
            if let Some(mut stdin) = child.stdin.take() {
    150
    0
                stdin.write_all(query.as_bytes())?;
    151
    0
            }
    152
    153
    0
            let output = child.wait_with_output()?;
    154
    0
            let stdout = String::from_utf8_lossy(&output.stdout);
    155
    156
    0
            self.parse_result(&stdout)
    157
    0
        }
    158
    159
        /// Parse solver result
    160
    0
        fn parse_result(&self, output: &str) -> Result<SmtResult> {
    161
    0
            if output.contains("sat") && !output.contains("unsat") {
    162
    0
                Ok(SmtResult::Sat)
    163
    0
            } else if output.contains("unsat") {
    164
    0
                Ok(SmtResult::Unsat)
    165
    0
            } else if output.contains("unknown") {
    166
    0
                Ok(SmtResult::Unknown)
    167
    0
            } else if output.contains("timeout") {
    168
    0
                Ok(SmtResult::Timeout)
    169
            } else {
    170
    0
                Ok(SmtResult::Error(format!("Unexpected output: {output}")))
    171
            }
    172
    0
        }
    173
    174
        /// Parse model from solver output
    175
    0
        fn parse_model(&self, _output: &str) -> Result<HashMap<String, String>> {
    176
    0
            Ok(HashMap::new())
    177
    0
        }
    178
    }
    179
    180
    impl Clone for SmtSolver {
    181
    0
        fn clone(&self) -> Self {
    182
    0
            Self {
    183
    0
                backend: self.backend,
    184
    0
                timeout_ms: self.timeout_ms,
    185
    0
                assertions: self.assertions.clone(),
    186
    0
                declarations: self.declarations.clone(),
    187
    0
            }
    188
    0
        }
    189
    }
    190
    191
    /// SMT query
    192
    #[derive(Debug, Clone, Serialize, Deserialize)]
    193
    pub struct SmtQuery {
    194
        pub formula: String,
    195
        pub variables: Vec<(String, String)>,
    196
        pub assumptions: Vec<String>,
    197
    }
    198
    199
    impl SmtQuery {
    200
        /// Create new query
    201
    0
        pub fn new(formula: &str) -> Self {
    202
    0
            Self {
    203
    0
                formula: formula.to_string(),
    204
    0
                variables: Vec::new(),
    205
    0
                assumptions: Vec::new(),
    206
    0
            }
    207
    0
        }
    208
    209
        /// Add variable
    210
    0
        pub fn add_var(&mut self, name: &str, sort: &str) {
    211
    0
            self.variables.push((name.to_string(), sort.to_string()));
    212
    0
        }
    213
    214
        /// Add assumption
    215
    0
        pub fn add_assumption(&mut self, expr: &str) {
    216
    0
            self.assumptions.push(expr.to_string());
    217
    0
        }
    218
    219
        /// Execute query
    220
    0
        pub fn execute(&self, backend: SmtBackend) -> Result<SmtResult> {
    221
    0
            let mut solver = SmtSolver::new(backend);
    222
    223
    0
            for (name, sort) in &self.variables {
    224
    0
                solver.declare_var(name, sort);
    225
    0
            }
    226
    227
    0
            for assumption in &self.assumptions {
    228
    0
                solver.assert(assumption);
    229
    0
            }
    230
    231
    0
            solver.prove(&self.formula)
    232
    0
        }
    233
    }
    234
    235
    /// SMT solver result
    236
    #[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
    237
    pub enum SmtResult {
    238
        Sat,
    239
        Unsat,
    240
        Valid,
    241
        Invalid,
    242
        Unknown,
    243
        Timeout,
    244
        Error(String),
    245
    }
    246
    247
    impl SmtResult {
    248
        /// Check if result indicates success
    249
    0
        pub fn is_success(&self) -> bool {
    250
    0
            matches!(self, Self::Valid | Self::Unsat)
    251
    0
        }
    252
    253
        /// Get human-readable description
    254
    0
        pub fn description(&self) -> &str {
    255
    0
            match self {
    256
    0
                Self::Sat => "Satisfiable",
    257
    0
                Self::Unsat => "Unsatisfiable",
    258
    0
                Self::Valid => "Valid",
    259
    0
                Self::Invalid => "Invalid",
    260
    0
                Self::Unknown => "Unknown",
    261
    0
                Self::Timeout => "Timeout",
    262
    0
                Self::Error(_) => "Error",
    263
            }
    264
    0
        }
    265
    }
    266
    267
    /// High-level proof automation
    268
    pub struct ProofAutomation {
    269
        backend: SmtBackend,
    270
        cache: HashMap<String, SmtResult>,
    271
    }
    272
    273
    impl ProofAutomation {
    274
        /// Create new automation
    275
    0
        pub fn new(backend: SmtBackend) -> Self {
    276
    0
            Self {
    277
    0
                backend,
    278
    0
                cache: HashMap::new(),
    279
    0
            }
    280
    0
        }
    281
    282
        /// Prove implication
    283
    0
        pub fn prove_implication(&mut self, antecedent: &str, consequent: &str) -> Result<SmtResult> {
    284
    0
            let formula = format!("(=> {antecedent} {consequent})");
    285
    0
            self.prove(&formula)
    286
    0
        }
    287
    288
        /// Prove equivalence
    289
    0
        pub fn prove_equivalence(&mut self, left: &str, right: &str) -> Result<SmtResult> {
    290
    0
            let formula = format!("(= {left} {right})");
    291
    0
            self.prove(&formula)
    292
    0
        }
    293
    294
        /// Prove with caching
    295
    0
        fn prove(&mut self, formula: &str) -> Result<SmtResult> {
    296
    0
            if let Some(cached) = self.cache.get(formula) {
    297
    0
                return Ok(cached.clone());
    298
    0
            }
    299
    300
    0
            let query = SmtQuery::new(formula);
    301
    0
            let result = query.execute(self.backend)?;
    302
    0
            self.cache.insert(formula.to_string(), result.clone());
    303
    304
    0
            Ok(result)
    305
    0
        }
    306
    }
    307
    308
    #[cfg(test)]
    309
    mod tests {
    310
        use super::*;
    311
    312
        #[test]
    313
        fn test_smt_query_construction() {
    314
            let mut query = SmtQuery::new("(> x 0)");
    315
            query.add_var("x", "Int");
    316
            query.add_assumption("(< x 10)");
    317
    318
            assert_eq!(query.formula, "(> x 0)");
    319
            assert_eq!(query.variables.len(), 1);
    320
            assert_eq!(query.assumptions.len(), 1);
    321
        }
    322
    323
        #[test]
    324
        fn test_solver_initialization() {
    325
            let solver = SmtSolver::new(SmtBackend::Z3);
    326
            assert_eq!(solver.backend, SmtBackend::Z3);
    327
            assert_eq!(solver.timeout_ms, 5000);
    328
        }
    329
    }