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

Source
//! SMT solver integration for proof automation

use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::collections::HashMap;
use std::process::{Command, Stdio};
use std::io::Write;

/// SMT solver backend
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum SmtBackend {
    Z3,
    CVC5,
    Yices2,
    MathSAT,
}

impl SmtBackend {
    /// Get command for solver
    fn command(&self) -> &str {
        match self {
            Self::Z3 => "z3",
            Self::CVC5 => "cvc5",
            Self::Yices2 => "yices-smt2",
            Self::MathSAT => "mathsat",
        }
    }
    
    /// Get command arguments
    fn args(&self) -> Vec<&str> {
        match self {
            Self::Z3 => vec!["-in", "-smt2"],
            Self::CVC5 => vec!["--lang", "smt2", "--incremental"],
            Self::Yices2 => vec!["--incremental"],
            Self::MathSAT => vec!["-input=smt2"],
        }
    }
}

/// SMT solver interface
pub struct SmtSolver {
    backend: SmtBackend,
    timeout_ms: u64,
    assertions: Vec<String>,
    declarations: HashMap<String, String>,
}

impl SmtSolver {
    /// Create new SMT solver
    pub fn new(backend: SmtBackend) -> Self {
        Self {
            backend,
            timeout_ms: 5000,
            assertions: Vec::new(),
            declarations: HashMap::new(),
        }
    }
    
    /// Set timeout
    pub fn set_timeout(&mut self, timeout_ms: u64) {
        self.timeout_ms = timeout_ms;
    }
    
    /// Declare a variable
    pub fn declare_var(&mut self, name: &str, sort: &str) {
        self.declarations.insert(
            name.to_string(),
            format!("(declare-fun {name} () {sort})")
        );
    }
    
    /// Declare a function
    pub fn declare_fun(&mut self, name: &str, params: &[&str], ret: &str) {
        let params_str = params.join(" ");
        self.declarations.insert(
            name.to_string(),
            format!("(declare-fun {name} ({params_str}) {ret})")
        );
    }
    
    /// Add an assertion
    pub fn assert(&mut self, expr: &str) {
        self.assertions.push(format!("(assert {expr})"));
    }
    
    /// Check satisfiability
    pub fn check_sat(&self) -> Result<SmtResult> {
        let query = self.build_query("(check-sat)");
        self.execute_query(&query)
    }
    
    /// Get model (if sat)
    pub fn get_model(&self) -> Result<Option<HashMap<String, String>>> {
        let query = self.build_query("(check-sat)\n(get-model)");
        let result = self.execute_query(&query)?;
        
        if result == SmtResult::Sat {
            Ok(Some(self.parse_model(&query)?))
        } else {
            Ok(None)
        }
    }
    
    /// Check validity (prove formula)
    pub fn prove(&self, formula: &str) -> Result<SmtResult> {
        let mut solver = self.clone();
        solver.assert(&format!("(not {formula})"));
        
        match solver.check_sat()? {
            SmtResult::Unsat => Ok(SmtResult::Valid),
            SmtResult::Sat => Ok(SmtResult::Invalid),
            other => Ok(other),
        }
    }
    
    /// Build complete SMT-LIB2 query
    fn build_query(&self, command: &str) -> String {
        let mut query = String::new();
        
        query.push_str("(set-logic ALL)\n");
        query.push_str(&format!("(set-option :timeout {})\n", self.timeout_ms));
        
        for decl in self.declarations.values() {
            query.push_str(decl);
            query.push('\n');
        }
        
        for assertion in &self.assertions {
            query.push_str(assertion);
            query.push('\n');
        }
        
        query.push_str(command);
        query.push('\n');
        query.push_str("(exit)\n");
        
        query
    }
    
    /// Execute query via solver process
    fn execute_query(&self, query: &str) -> Result<SmtResult> {
        let mut child = Command::new(self.backend.command())
            .args(self.backend.args())
            .stdin(Stdio::piped())
            .stdout(Stdio::piped())
            .stderr(Stdio::piped())
            .spawn()?;
        
        if let Some(mut stdin) = child.stdin.take() {
            stdin.write_all(query.as_bytes())?;
        }
        
        let output = child.wait_with_output()?;
        let stdout = String::from_utf8_lossy(&output.stdout);
        
        self.parse_result(&stdout)
    }
    
    /// Parse solver result
    fn parse_result(&self, output: &str) -> Result<SmtResult> {
        if output.contains("sat") && !output.contains("unsat") {
            Ok(SmtResult::Sat)
        } else if output.contains("unsat") {
            Ok(SmtResult::Unsat)
        } else if output.contains("unknown") {
            Ok(SmtResult::Unknown)
        } else if output.contains("timeout") {
            Ok(SmtResult::Timeout)
        } else {
            Ok(SmtResult::Error(format!("Unexpected output: {output}")))
        }
    }
    
    /// Parse model from solver output
    fn parse_model(&self, _output: &str) -> Result<HashMap<String, String>> {
        Ok(HashMap::new())
    }
}

impl Clone for SmtSolver {
    fn clone(&self) -> Self {
        Self {
            backend: self.backend,
            timeout_ms: self.timeout_ms,
            assertions: self.assertions.clone(),
            declarations: self.declarations.clone(),
        }
    }
}

/// SMT query
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct SmtQuery {
    pub formula: String,
    pub variables: Vec<(String, String)>,
    pub assumptions: Vec<String>,
}

impl SmtQuery {
    /// Create new query
    pub fn new(formula: &str) -> Self {
        Self {
            formula: formula.to_string(),
            variables: Vec::new(),
            assumptions: Vec::new(),
        }
    }
    
    /// Add variable
    pub fn add_var(&mut self, name: &str, sort: &str) {
        self.variables.push((name.to_string(), sort.to_string()));
    }
    
    /// Add assumption
    pub fn add_assumption(&mut self, expr: &str) {
        self.assumptions.push(expr.to_string());
    }
    
    /// Execute query
    pub fn execute(&self, backend: SmtBackend) -> Result<SmtResult> {
        let mut solver = SmtSolver::new(backend);
        
        for (name, sort) in &self.variables {
            solver.declare_var(name, sort);
        }
        
        for assumption in &self.assumptions {
            solver.assert(assumption);
        }
        
        solver.prove(&self.formula)
    }
}

/// SMT solver result
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
pub enum SmtResult {
    Sat,
    Unsat,
    Valid,
    Invalid,
    Unknown,
    Timeout,
    Error(String),
}

impl SmtResult {
    /// Check if result indicates success
    pub fn is_success(&self) -> bool {
        matches!(self, Self::Valid | Self::Unsat)
    }
    
    /// Get human-readable description
    pub fn description(&self) -> &str {
        match self {
            Self::Sat => "Satisfiable",
            Self::Unsat => "Unsatisfiable",
            Self::Valid => "Valid",
            Self::Invalid => "Invalid",
            Self::Unknown => "Unknown",
            Self::Timeout => "Timeout",
            Self::Error(_) => "Error",
        }
    }
}

/// High-level proof automation
pub struct ProofAutomation {
    backend: SmtBackend,
    cache: HashMap<String, SmtResult>,
}

impl ProofAutomation {
    /// Create new automation
    pub fn new(backend: SmtBackend) -> Self {
        Self {
            backend,
            cache: HashMap::new(),
        }
    }
    
    /// Prove implication
    pub fn prove_implication(&mut self, antecedent: &str, consequent: &str) -> Result<SmtResult> {
        let formula = format!("(=> {antecedent} {consequent})");
        self.prove(&formula)
    }
    
    /// Prove equivalence
    pub fn prove_equivalence(&mut self, left: &str, right: &str) -> Result<SmtResult> {
        let formula = format!("(= {left} {right})");
        self.prove(&formula)
    }
    
    /// Prove with caching
    fn prove(&mut self, formula: &str) -> Result<SmtResult> {
        if let Some(cached) = self.cache.get(formula) {
            return Ok(cached.clone());
        }
        
        let query = SmtQuery::new(formula);
        let result = query.execute(self.backend)?;
        self.cache.insert(formula.to_string(), result.clone());
        
        Ok(result)
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    
    #[test]
    fn test_smt_query_construction() {
        let mut query = SmtQuery::new("(> x 0)");
        query.add_var("x", "Int");
        query.add_assumption("(< x 10)");
        
        assert_eq!(query.formula, "(> x 0)");
        assert_eq!(query.variables.len(), 1);
        assert_eq!(query.assumptions.len(), 1);
    }
    
    #[test]
    fn test_solver_initialization() {
        let solver = SmtSolver::new(SmtBackend::Z3);
        assert_eq!(solver.backend, SmtBackend::Z3);
        assert_eq!(solver.timeout_ms, 5000);
    }
}

Coverage Report

Created: 2025-09-05 15:26

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	1	pub fn new(backend: SmtBackend) -> Self {
51	1	Self {
52	1	backend,
53	1	timeout_ms: 5000,
54	1	assertions: Vec::new(),
55	1	declarations: HashMap::new(),
56	1	}
57	1	}
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	1	pub fn new(formula: &str) -> Self {
202	1	Self {
203	1	formula: formula.to_string(),
204	1	variables: Vec::new(),
205	1	assumptions: Vec::new(),
206	1	}
207	1	}
208
209		/// Add variable
210	1	pub fn add_var(&mut self, name: &str, sort: &str) {
211	1	self.variables.push((name.to_string(), sort.to_string()));
212	1	}
213
214		/// Add assumption
215	1	pub fn add_assumption(&mut self, expr: &str) {
216	1	self.assumptions.push(expr.to_string());
217	1	}
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	1	fn test_smt_query_construction() {
314	1	let mut query = SmtQuery::new("(> x 0)");
315	1	query.add_var("x", "Int");
316	1	query.add_assumption("(< x 10)");
317
318	1	assert_eq!(query.formula, "(> x 0)");
319	1	assert_eq!(query.variables.len(), 1);
320	1	assert_eq!(query.assumptions.len(), 1);
321	1	}
322
323		#[test]
324	1	fn test_solver_initialization() {
325	1	let solver = SmtSolver::new(SmtBackend::Z3);
326	1	assert_eq!(solver.backend, SmtBackend::Z3);
327	1	assert_eq!(solver.timeout_ms, 5000);
328	1	}
329		}