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

Source
//! Counterexample generation for failed proofs

use anyhow::Result;
use serde::{Deserialize, Serialize};
use std::collections::HashMap;
use std::fmt;

use super::smt::{SmtSolver, SmtBackend, SmtResult};

/// Counterexample
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct Counterexample {
    /// Variable assignments
    pub assignments: HashMap<String, Value>,
    
    /// Execution trace
    pub trace: Vec<TraceStep>,
    
    /// Failed assertion
    pub failed_assertion: String,
    
    /// Explanation
    pub explanation: Option<String>,
}

/// Value in counterexample
#[derive(Debug, Clone, Serialize, Deserialize)]
pub enum Value {
    Int(i64),
    Bool(bool),
    String(String),
    Float(f64),
    Array(Vec<Value>),
    Tuple(Vec<Value>),
    Null,
}

impl fmt::Display for Value {
    fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
        match self {
            Self::Int(n) => write!(f, "{n}"),
            Self::Bool(b) => write!(f, "{b}"),
            Self::String(s) => write!(f, "\"{s}\""),
            Self::Float(x) => write!(f, "{x}"),
            Self::Array(vs) => {
                write!(f, "[")?;
                for (i, v) in vs.iter().enumerate() {
                    if i > 0 { write!(f, ", ")?; }
                    write!(f, "{v}")?;
                }
                write!(f, "]")
            }
            Self::Tuple(vs) => {
                write!(f, "(")?;
                for (i, v) in vs.iter().enumerate() {
                    if i > 0 { write!(f, ", ")?; }
                    write!(f, "{v}")?;
                }
                write!(f, ")")
            }
            Self::Null => write!(f, "null"),
        }
    }
}

/// Trace step
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct TraceStep {
    /// Step number
    pub step: usize,
    
    /// Location in code
    pub location: String,
    
    /// Operation performed
    pub operation: String,
    
    /// State after operation
    pub state: HashMap<String, Value>,
}

impl Counterexample {
    /// Create new counterexample
    pub fn new(failed_assertion: &str) -> Self {
        Self {
            assignments: HashMap::new(),
            trace: Vec::new(),
            failed_assertion: failed_assertion.to_string(),
            explanation: None,
        }
    }
    
    /// Add assignment
    pub fn add_assignment(&mut self, var: &str, value: Value) {
        self.assignments.insert(var.to_string(), value);
    }
    
    /// Add trace step
    pub fn add_trace_step(&mut self, step: TraceStep) {
        self.trace.push(step);
    }
    
    /// Set explanation
    pub fn set_explanation(&mut self, explanation: &str) {
        self.explanation = Some(explanation.to_string());
    }
    
    /// Format as readable report
    pub fn format_report(&self) -> String {
        let mut report = String::new();
        
        report.push_str("=== Counterexample Found ===\n\n");
        
        report.push_str("Failed Assertion:\n");
        report.push_str(&format!("  {}\n\n", self.failed_assertion));
        
        if !self.assignments.is_empty() {
            report.push_str("Variable Assignments:\n");
            for (var1, val1) in &self.assignments {
                report.push_str(&format!("  {var} = {val}\n"));
            }
            report.push('\n');
        }
        
        if !self.trace.is_empty() {
            report.push_str("Execution Trace:\n");
            for step in &self.trace {
                report.push_str(&format!("  Step {}: {} at {}\n", 
                    step.step, step.operation, step.location));
                if !step.state.is_empty() {
                    for (var, val) in &step.state {
                        report.push_str(&format!("    {var} = {val}\n"));
                    }
                }
            }
            report.push('\n');
        }
        
        if let Some(explanation) = &self.explanation {
            report.push_str("Explanation:\n");
            report.push_str(&format!("  {explanation}\n"));
        }0
        
        report
    }
}

/// Test case for property-based testing
#[derive(Debug, Clone, Serialize, Deserialize)]
pub struct TestCase {
    /// Input values
    pub inputs: HashMap<String, Value>,
    
    /// Expected output
    pub expected: Option<Value>,
    
    /// Property to test
    pub property: String,
}

impl TestCase {
    /// Create new test case
    pub fn new(property: &str) -> Self {
        Self {
            inputs: HashMap::new(),
            expected: None,
            property: property.to_string(),
        }
    }
    
    /// Add input
    pub fn add_input(&mut self, name: &str, value: Value) {
        self.inputs.insert(name.to_string(), value);
    }
    
    /// Set expected output
    pub fn set_expected(&mut self, value: Value) {
        self.expected = Some(value);
    }
    
    /// Generate Ruchy test code
    pub fn to_ruchy_test(&self, test_name: &str) -> String {
        let mut code = String::new();
        
        code.push_str(&format!("#[test]\nfn {test_name}() {{\n"));
        
        for (name1, value1) in &self.inputs {
            code.push_str(&format!("    let {} = {};\n", name, 
                self.value_to_ruchy(value)));
        }
        
        code.push_str(&format!("    assert!({});\n", self.property));
        
        if let Some(expected) = &self.expected {
            code.push_str(&format!("    assert_eq!(result, {});\n", 
                self.value_to_ruchy(expected)));
        }0
        
        code.push_str("}\n");
        
        code
    }
    
    /// Convert value to Ruchy syntax
    fn value_to_ruchy(&self, value: &Value) -> String {
        match value {
            Value::Int(n) => n.to_string(),
            Value::Bool(b) => b.to_string(),
            Value::String(s) => format!("\"{s}\""),
            Value::Float(x) => format!("{x:.6}"),
            Value::Array(vs) => {
                let items: Vec<String> = vs.iter()
                    .map(|v| self.value_to_ruchy(v))
                    .collect();
                format!("[{}]", items.join(", "))
            }
            Value::Tuple(vs) => {
                let items: Vec<String> = vs.iter()
                    .map(|v| self.value_to_ruchy(v))
                    .collect();
                format!("({})", items.join(", "))
            }
            Value::Null => "None".to_string(),
        }
    }
}

/// Counterexample generator
pub struct CounterexampleGenerator {
    backend: SmtBackend,
    max_iterations: usize,
    shrinking: bool,
}

impl CounterexampleGenerator {
    /// Create new generator
    pub fn new() -> Self {
        Self {
            backend: SmtBackend::Z3,
            max_iterations: 100,
            shrinking: true,
        }
    }
    
    /// Set SMT backend
    pub fn set_backend(&mut self, backend: SmtBackend) {
        self.backend = backend;
    }
    
    /// Enable/disable shrinking
    pub fn set_shrinking(&mut self, enabled: bool) {
        self.shrinking = enabled;
    }
    
    /// Generate counterexample for property
    pub fn generate(&self, property: &str, vars: &[(String, String)]) -> Result<Option<Counterexample>> {
        let mut solver = SmtSolver::new(self.backend);
        
        for (name, sort) in vars {
            solver.declare_var(name, sort);
        }
        
        solver.assert(&format!("(not {property})"));
        
        match solver.check_sat()? {
            SmtResult::Sat => {
                let model = solver.get_model()?;
                Ok(Some(self.build_counterexample(property, model)))
            }
            _ => Ok(None),
        }
    }
    
    /// Build counterexample from model
    fn build_counterexample(&self, property: &str, model: Option<HashMap<String, String>>) -> Counterexample {
        let mut cex = Counterexample::new(property);
        
        if let Some(assignments) = model {
            for (var, val) in assignments {
                cex.add_assignment(&var, self.parse_value(&val));
            }
        }
        
        if self.shrinking {
            self.shrink_counterexample(&mut cex);
        }
        
        cex
    }
    
    /// Parse SMT value
    fn parse_value(&self, smt_value: &str) -> Value {
        if let Ok(n) = smt_value.parse::<i64>() {
            Value::Int(n)
        } else if smt_value == "true" {
            Value::Bool(true)
        } else if smt_value == "false" {
            Value::Bool(false)
        } else if let Ok(x) = smt_value.parse::<f64>() {
            Value::Float(x)
        } else {
            Value::String(smt_value.to_string())
        }
    }
    
    /// Shrink counterexample to minimal form
    fn shrink_counterexample(&self, cex: &mut Counterexample) {
        let mut changed = true;
        let mut iterations = 0;
        
        while changed && iterations < self.max_iterations {
            changed = false;
            iterations += 1;
            
            for (var, value) in cex.assignments.clone() {
                if let Some(shrunk) = self.try_shrink_value(&value) {
                    cex.assignments.insert(var, shrunk);
                    changed = true;
                }
            }
        }
    }
    
    /// Try to shrink a value
    fn try_shrink_value(&self, value: &Value) -> Option<Value> {
        match value {
            Value::Int(n) if *n > 0 => Some(Value::Int(n / 2)),
            Value::Array(vs) if !vs.is_empty() => {
                let mut shrunk = vs.clone();
                shrunk.pop();
                Some(Value::Array(shrunk))
            }
            Value::String(s) if s.len() > 1 => {
                Some(Value::String(s[..s.len()-1].to_string()))
            }
            _ => None,
        }
    }
    
    /// Generate multiple test cases
    pub fn generate_test_suite(&self, property: &str, vars: &[(String, String)], count: usize) -> Result<Vec<TestCase>> {
        let mut test_cases: Vec<TestCase> = Vec::new();
        
        for i in 0..count {
            let mut solver = SmtSolver::new(self.backend);
            
            for (name, sort) in vars {
                solver.declare_var(name, sort);
            }
            
            for prev_case in &test_cases {
                for (var, val) in &prev_case.inputs {
                    solver.assert(&format!("(not (= {} {}))", var, 
                        self.value_to_smt(val)));
                }
            }
            
            solver.assert(&format!("(not {property})"));
            
            match solver.check_sat()? {
                SmtResult::Sat => {
                    if let Some(model) = solver.get_model()? {
                        let mut test_case = TestCase::new(property);
                        for (var, val) in model {
                            test_case.add_input(&var, self.parse_value(&val));
                        }
                        test_cases.push(test_case);
                    }
                }
                _ => break,
            }
            
            if i >= count {
                break;
            }
        }
        
        Ok(test_cases)
    }
    
    /// Convert value to SMT syntax
    fn value_to_smt(&self, value: &Value) -> String {
        match value {
            Value::Int(n) => n.to_string(),
            Value::Bool(b) => b.to_string(),
            Value::String(s) => format!("\"{s}\""),
            Value::Float(x) => format!("{x:.6}"),
            _ => "null".to_string(),
        }
    }
}

impl Default for CounterexampleGenerator {
    fn default() -> Self {
        Self::new()
    }
}

/// Symbolic execution engine
pub struct SymbolicExecutor {
    generator: CounterexampleGenerator,
    path_conditions: Vec<String>,
    symbolic_state: HashMap<String, String>,
}

impl SymbolicExecutor {
    /// Create new symbolic executor
    pub fn new() -> Self {
        Self {
            generator: CounterexampleGenerator::new(),
            path_conditions: Vec::new(),
            symbolic_state: HashMap::new(),
        }
    }
    
    /// Add path condition
    pub fn add_condition(&mut self, condition: &str) {
        self.path_conditions.push(condition.to_string());
    }
    
    /// Set symbolic variable
    pub fn set_symbolic(&mut self, var: &str, symbolic: &str) {
        self.symbolic_state.insert(var.to_string(), symbolic.to_string());
    }
    
    /// Find path to error
    pub fn find_error_path(&self, error_condition: &str) -> Result<Option<Counterexample>> {
        let mut solver = SmtSolver::new(self.generator.backend);
        
        for var in self.symbolic_state.keys() {
            solver.declare_var(var, "Int");
        }
        
        for condition in &self.path_conditions {
            solver.assert(condition);
        }
        
        solver.assert(error_condition);
        
        match solver.check_sat()? {
            SmtResult::Sat => {
                let model = solver.get_model()?;
                Ok(Some(self.generator.build_counterexample(error_condition, model)))
            }
            _ => Ok(None),
        }
    }
}

impl Default for SymbolicExecutor {
    fn default() -> Self {
        Self::new()
    }
}

#[cfg(test)]
mod tests {
    use super::*;
    
    #[test]
    fn test_counterexample_report() {
        let mut cex = Counterexample::new("x > 10");
        cex.add_assignment("x", Value::Int(5));
        cex.set_explanation("x = 5 does not satisfy x > 10");
        
        let report = cex.format_report();
        assert!(report.contains("x > 10"));
        assert!(report.contains("x = 5"));
    }
    
    #[test]
    fn test_test_case_generation() {
        let mut test = TestCase::new("x > 0");
        test.add_input("x", Value::Int(42));
        test.set_expected(Value::Bool(true));
        
        let code = test.to_ruchy_test("test_positive");
        assert!(code.contains("let x = 42"));
        assert!(code.contains("assert!(x > 0)"));
    }
}

Coverage Report

Created: 2025-09-05 15:26

Line	Count	Source
1		//! Counterexample generation for failed proofs
2
3		use anyhow::Result;
4		use serde::{Deserialize, Serialize};
5		use std::collections::HashMap;
6		use std::fmt;
7
8		use super::smt::{SmtSolver, SmtBackend, SmtResult};
9
10		/// Counterexample
11		#[derive(Debug, Clone, Serialize, Deserialize)]
12		pub struct Counterexample {
13		/// Variable assignments
14		pub assignments: HashMap<String, Value>,
15
16		/// Execution trace
17		pub trace: Vec<TraceStep>,
18
19		/// Failed assertion
20		pub failed_assertion: String,
21
22		/// Explanation
23		pub explanation: Option<String>,
24		}
25
26		/// Value in counterexample
27		#[derive(Debug, Clone, Serialize, Deserialize)]
28		pub enum Value {
29		Int(i64),
30		Bool(bool),
31		String(String),
32		Float(f64),
33		Array(Vec<Value>),
34		Tuple(Vec<Value>),
35		Null,
36		}
37
38		impl fmt::Display for Value {
39	1	fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result {
40	1	match self {
41	1	Self::Int(n) => write!(f, "{n}"),
42	0	Self::Bool(b) => write!(f, "{b}"),
43	0	Self::String(s) => write!(f, "\"{s}\""),
44	0	Self::Float(x) => write!(f, "{x}"),
45	0	Self::Array(vs) => {
46	0	write!(f, "[")?;
47	0	for (i, v) in vs.iter().enumerate() {
48	0	if i > 0 { write!(f, ", ")?; }
49	0	write!(f, "{v}")?;
50		}
51	0	write!(f, "]")
52		}
53	0	Self::Tuple(vs) => {
54	0	write!(f, "(")?;
55	0	for (i, v) in vs.iter().enumerate() {
56	0	if i > 0 { write!(f, ", ")?; }
57	0	write!(f, "{v}")?;
58		}
59	0	write!(f, ")")
60		}
61	0	Self::Null => write!(f, "null"),
62		}
63	1	}
64		}
65
66		/// Trace step
67		#[derive(Debug, Clone, Serialize, Deserialize)]
68		pub struct TraceStep {
69		/// Step number
70		pub step: usize,
71
72		/// Location in code
73		pub location: String,
74
75		/// Operation performed
76		pub operation: String,
77
78		/// State after operation
79		pub state: HashMap<String, Value>,
80		}
81
82		impl Counterexample {
83		/// Create new counterexample
84	1	pub fn new(failed_assertion: &str) -> Self {
85	1	Self {
86	1	assignments: HashMap::new(),
87	1	trace: Vec::new(),
88	1	failed_assertion: failed_assertion.to_string(),
89	1	explanation: None,
90	1	}
91	1	}
92
93		/// Add assignment
94	1	pub fn add_assignment(&mut self, var: &str, value: Value) {
95	1	self.assignments.insert(var.to_string(), value);
96	1	}
97
98		/// Add trace step
99	0	pub fn add_trace_step(&mut self, step: TraceStep) {
100	0	self.trace.push(step);
101	0	}
102
103		/// Set explanation
104	1	pub fn set_explanation(&mut self, explanation: &str) {
105	1	self.explanation = Some(explanation.to_string());
106	1	}
107
108		/// Format as readable report
109	1	pub fn format_report(&self) -> String {
110	1	let mut report = String::new();
111
112	1	report.push_str("=== Counterexample Found ===\n\n");
113
114	1	report.push_str("Failed Assertion:\n");
115	1	report.push_str(&format!(" {}\n\n", self.failed_assertion));
116
117	1	if !self.assignments.is_empty() {
118	1	report.push_str("Variable Assignments:\n");
119	2	for ( var1 , val1 ) in &self.assignments {
120	1	report.push_str(&format!(" {var} = {val}\n"));
121	1	}
122	1	report.push('\n');
123	0	}
124
125	1	if !self.trace.is_empty() {
126	0	report.push_str("Execution Trace:\n");
127	0	for step in &self.trace {
128	0	report.push_str(&format!(" Step {}: {} at {}\n",
129	0	step.step, step.operation, step.location));
130	0	if !step.state.is_empty() {
131	0	for (var, val) in &step.state {
132	0	report.push_str(&format!(" {var} = {val}\n"));
133	0	}
134	0	}
135		}
136	0	report.push('\n');
137	1	}
138
139	1	if let Some(explanation) = &self.explanation {
140	1	report.push_str("Explanation:\n");
141	1	report.push_str(&format!(" {explanation}\n"));
142	1	}0
143
144	1	report
145	1	}
146		}
147
148		/// Test case for property-based testing
149		#[derive(Debug, Clone, Serialize, Deserialize)]
150		pub struct TestCase {
151		/// Input values
152		pub inputs: HashMap<String, Value>,
153
154		/// Expected output
155		pub expected: Option<Value>,
156
157		/// Property to test
158		pub property: String,
159		}
160
161		impl TestCase {
162		/// Create new test case
163	1	pub fn new(property: &str) -> Self {
164	1	Self {
165	1	inputs: HashMap::new(),
166	1	expected: None,
167	1	property: property.to_string(),
168	1	}
169	1	}
170
171		/// Add input
172	1	pub fn add_input(&mut self, name: &str, value: Value) {
173	1	self.inputs.insert(name.to_string(), value);
174	1	}
175
176		/// Set expected output
177	1	pub fn set_expected(&mut self, value: Value) {
178	1	self.expected = Some(value);
179	1	}
180
181		/// Generate Ruchy test code
182	1	pub fn to_ruchy_test(&self, test_name: &str) -> String {
183	1	let mut code = String::new();
184
185	1	code.push_str(&format!("#[test]\nfn {test_name}() {{\n"));
186
187	2	for ( name1 , value1 ) in &self.inputs {
188	1	code.push_str(&format!(" let {} = {};\n", name,
189	1	self.value_to_ruchy(value)));
190	1	}
191
192	1	code.push_str(&format!(" assert!({});\n", self.property));
193
194	1	if let Some(expected) = &self.expected {
195	1	code.push_str(&format!(" assert_eq!(result, {});\n",
196	1	self.value_to_ruchy(expected)));
197	1	}0
198
199	1	code.push_str("}\n");
200
201	1	code
202	1	}
203
204		/// Convert value to Ruchy syntax
205	2	fn value_to_ruchy(&self, value: &Value) -> String {
206	2	match value {
207	1	Value::Int(n) => n.to_string(),
208	1	Value::Bool(b) => b.to_string(),
209	0	Value::String(s) => format!("\"{s}\""),
210	0	Value::Float(x) => format!("{x:.6}"),
211	0	Value::Array(vs) => {
212	0	let items: Vec<String> = vs.iter()
213	0	.map(\|v\| self.value_to_ruchy(v))
214	0	.collect();
215	0	format!("[{}]", items.join(", "))
216		}
217	0	Value::Tuple(vs) => {
218	0	let items: Vec<String> = vs.iter()
219	0	.map(\|v\| self.value_to_ruchy(v))
220	0	.collect();
221	0	format!("({})", items.join(", "))
222		}
223	0	Value::Null => "None".to_string(),
224		}
225	2	}
226		}
227
228		/// Counterexample generator
229		pub struct CounterexampleGenerator {
230		backend: SmtBackend,
231		max_iterations: usize,
232		shrinking: bool,
233		}
234
235		impl CounterexampleGenerator {
236		/// Create new generator
237	0	pub fn new() -> Self {
238	0	Self {
239	0	backend: SmtBackend::Z3,
240	0	max_iterations: 100,
241	0	shrinking: true,
242	0	}
243	0	}
244
245		/// Set SMT backend
246	0	pub fn set_backend(&mut self, backend: SmtBackend) {
247	0	self.backend = backend;
248	0	}
249
250		/// Enable/disable shrinking
251	0	pub fn set_shrinking(&mut self, enabled: bool) {
252	0	self.shrinking = enabled;
253	0	}
254
255		/// Generate counterexample for property
256	0	pub fn generate(&self, property: &str, vars: &[(String, String)]) -> Result<Option<Counterexample>> {
257	0	let mut solver = SmtSolver::new(self.backend);
258
259	0	for (name, sort) in vars {
260	0	solver.declare_var(name, sort);
261	0	}
262
263	0	solver.assert(&format!("(not {property})"));
264
265	0	match solver.check_sat()? {
266		SmtResult::Sat => {
267	0	let model = solver.get_model()?;
268	0	Ok(Some(self.build_counterexample(property, model)))
269		}
270	0	_ => Ok(None),
271		}
272	0	}
273
274		/// Build counterexample from model
275	0	fn build_counterexample(&self, property: &str, model: Option<HashMap<String, String>>) -> Counterexample {
276	0	let mut cex = Counterexample::new(property);
277
278	0	if let Some(assignments) = model {
279	0	for (var, val) in assignments {
280	0	cex.add_assignment(&var, self.parse_value(&val));
281	0	}
282	0	}
283
284	0	if self.shrinking {
285	0	self.shrink_counterexample(&mut cex);
286	0	}
287
288	0	cex
289	0	}
290
291		/// Parse SMT value
292	0	fn parse_value(&self, smt_value: &str) -> Value {
293	0	if let Ok(n) = smt_value.parse::<i64>() {
294	0	Value::Int(n)
295	0	} else if smt_value == "true" {
296	0	Value::Bool(true)
297	0	} else if smt_value == "false" {
298	0	Value::Bool(false)
299	0	} else if let Ok(x) = smt_value.parse::<f64>() {
300	0	Value::Float(x)
301		} else {
302	0	Value::String(smt_value.to_string())
303		}
304	0	}
305
306		/// Shrink counterexample to minimal form
307	0	fn shrink_counterexample(&self, cex: &mut Counterexample) {
308	0	let mut changed = true;
309	0	let mut iterations = 0;
310
311	0	while changed && iterations < self.max_iterations {
312	0	changed = false;
313	0	iterations += 1;
314
315	0	for (var, value) in cex.assignments.clone() {
316	0	if let Some(shrunk) = self.try_shrink_value(&value) {
317	0	cex.assignments.insert(var, shrunk);
318	0	changed = true;
319	0	}
320		}
321		}
322	0	}
323
324		/// Try to shrink a value
325	0	fn try_shrink_value(&self, value: &Value) -> Option<Value> {
326	0	match value {
327	0	Value::Int(n) if *n > 0 => Some(Value::Int(n / 2)),
328	0	Value::Array(vs) if !vs.is_empty() => {
329	0	let mut shrunk = vs.clone();
330	0	shrunk.pop();
331	0	Some(Value::Array(shrunk))
332		}
333	0	Value::String(s) if s.len() > 1 => {
334	0	Some(Value::String(s[..s.len()-1].to_string()))
335		}
336	0	_ => None,
337		}
338	0	}
339
340		/// Generate multiple test cases
341	0	pub fn generate_test_suite(&self, property: &str, vars: &[(String, String)], count: usize) -> Result<Vec<TestCase>> {
342	0	let mut test_cases: Vec<TestCase> = Vec::new();
343
344	0	for i in 0..count {
345	0	let mut solver = SmtSolver::new(self.backend);
346
347	0	for (name, sort) in vars {
348	0	solver.declare_var(name, sort);
349	0	}
350
351	0	for prev_case in &test_cases {
352	0	for (var, val) in &prev_case.inputs {
353	0	solver.assert(&format!("(not (= {} {}))", var,
354	0	self.value_to_smt(val)));
355	0	}
356		}
357
358	0	solver.assert(&format!("(not {property})"));
359
360	0	match solver.check_sat()? {
361		SmtResult::Sat => {
362	0	if let Some(model) = solver.get_model()? {
363	0	let mut test_case = TestCase::new(property);
364	0	for (var, val) in model {
365	0	test_case.add_input(&var, self.parse_value(&val));
366	0	}
367	0	test_cases.push(test_case);
368	0	}
369		}
370	0	_ => break,
371		}
372
373	0	if i >= count {
374	0	break;
375	0	}
376		}
377
378	0	Ok(test_cases)
379	0	}
380
381		/// Convert value to SMT syntax
382	0	fn value_to_smt(&self, value: &Value) -> String {
383	0	match value {
384	0	Value::Int(n) => n.to_string(),
385	0	Value::Bool(b) => b.to_string(),
386	0	Value::String(s) => format!("\"{s}\""),
387	0	Value::Float(x) => format!("{x:.6}"),
388	0	_ => "null".to_string(),
389		}
390	0	}
391		}
392
393		impl Default for CounterexampleGenerator {
394	0	fn default() -> Self {
395	0	Self::new()
396	0	}
397		}
398
399		/// Symbolic execution engine
400		pub struct SymbolicExecutor {
401		generator: CounterexampleGenerator,
402		path_conditions: Vec<String>,
403		symbolic_state: HashMap<String, String>,
404		}
405
406		impl SymbolicExecutor {
407		/// Create new symbolic executor
408	0	pub fn new() -> Self {
409	0	Self {
410	0	generator: CounterexampleGenerator::new(),
411	0	path_conditions: Vec::new(),
412	0	symbolic_state: HashMap::new(),
413	0	}
414	0	}
415
416		/// Add path condition
417	0	pub fn add_condition(&mut self, condition: &str) {
418	0	self.path_conditions.push(condition.to_string());
419	0	}
420
421		/// Set symbolic variable
422	0	pub fn set_symbolic(&mut self, var: &str, symbolic: &str) {
423	0	self.symbolic_state.insert(var.to_string(), symbolic.to_string());
424	0	}
425
426		/// Find path to error
427	0	pub fn find_error_path(&self, error_condition: &str) -> Result<Option<Counterexample>> {
428	0	let mut solver = SmtSolver::new(self.generator.backend);
429
430	0	for var in self.symbolic_state.keys() {
431	0	solver.declare_var(var, "Int");
432	0	}
433
434	0	for condition in &self.path_conditions {
435	0	solver.assert(condition);
436	0	}
437
438	0	solver.assert(error_condition);
439
440	0	match solver.check_sat()? {
441		SmtResult::Sat => {
442	0	let model = solver.get_model()?;
443	0	Ok(Some(self.generator.build_counterexample(error_condition, model)))
444		}
445	0	_ => Ok(None),
446		}
447	0	}
448		}
449
450		impl Default for SymbolicExecutor {
451	0	fn default() -> Self {
452	0	Self::new()
453	0	}
454		}
455
456		#[cfg(test)]
457		mod tests {
458		use super::*;
459
460		#[test]
461	1	fn test_counterexample_report() {
462	1	let mut cex = Counterexample::new("x > 10");
463	1	cex.add_assignment("x", Value::Int(5));
464	1	cex.set_explanation("x = 5 does not satisfy x > 10");
465
466	1	let report = cex.format_report();
467	1	assert!(report.contains("x > 10"));
468	1	assert!(report.contains("x = 5"));
469	1	}
470
471		#[test]
472	1	fn test_test_case_generation() {
473	1	let mut test = TestCase::new("x > 0");
474	1	test.add_input("x", Value::Int(42));
475	1	test.set_expected(Value::Bool(true));
476
477	1	let code = test.to_ruchy_test("test_positive");
478	1	assert!(code.contains("let x = 42"));
479	1	assert!(code.contains("assert!(x > 0)"));
480	1	}
481		}