From 2e50b5ab79636b3893bb77fa4310a87e964b3243 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Tue, 11 Feb 2025 23:30:15 +0100 Subject: [PATCH 01/41] Implement execution of swine-z3 on SMT2 files --- z3rro/src/prover.rs | 83 ++++++++++++++++++++++++++++++++++++++++++++- 1 file changed, 82 insertions(+), 1 deletion(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index e1c88d7b..635ea4b8 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -1,6 +1,10 @@ //! Not a SAT solver, but a prover. There's a difference. -use std::{fmt::Display, time::Duration}; +//use std::{fmt::Display, time::Duration}; + +use std::{collections::VecDeque, fmt::Display, io::Write, path::Path, process::Command, time::Duration}; + +use tempfile::NamedTempFile; use z3::{ ast::{forall_const, Ast, Bool, Dynamic}, @@ -21,6 +25,68 @@ pub enum ProveResult<'ctx> { Unknown(ReasonUnknown), } +/// Find the swine-z3 file located under the dir directory, and execute swine-z3 on the file located at file_path +fn execute_swine(dir: &Path, file_path: &Path) { + let swine = "swine-z3"; + + let find_output = Command::new("find") + .arg(dir) + .arg("-name") + .arg(swine) + .output().unwrap(); + + if find_output.status.success() { + let stdout = String::from_utf8_lossy(&find_output.stdout); + + for line in stdout.lines().rev() { + let path = Path::new(line); + + if path.exists() && path.is_file() { + let cmd_output = Command::new(path) + .arg(file_path) + .output().unwrap(); + + if cmd_output.status.success() { + println!("{}", String::from_utf8_lossy(&cmd_output.stdout)); + break; + } else { + eprintln!("Failed to execute swine({}) command with status: {}", line, cmd_output.status); + } + } + } + } else { + eprintln!("Find command execution failed"); + } +} + +fn remove_lines_for_swine(input: &str) -> String { + let mut output = String::new(); + let mut tmp_buffer: VecDeque = VecDeque::new(); + let mut input_buffer: VecDeque = input.chars().collect(); + let mut cnt = 0; + + while let Some(c) = input_buffer.pop_front() { + tmp_buffer.push_back(c); + match c { + '(' => { + cnt += 1; + } + ')' => { + cnt -= 1; + if cnt == 0 { + let tmp: String = tmp_buffer.iter().collect(); + if !tmp.contains("declare-fun exp") && !tmp.contains("forall") { + output.push_str(&tmp); + } + tmp_buffer.clear(); + } + } + _ => {} + } + } + output +} + impl Display for ProveResult<'_> { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { @@ -94,6 +160,21 @@ impl<'ctx> Prover<'ctx> { if self.min_level_with_provables.is_none() { return ProveResult::Proof; } + + let mut smtlib = self.get_smtlib(); + + smtlib.add_check_sat(); + + let smtlib = smtlib.into_string(); + let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); + + smt_file.write_all(remove_lines_for_swine(&smtlib).as_bytes()).unwrap(); + + let file_path = smt_file.path(); + let start_dir = Path::new("../"); + + execute_swine(start_dir, file_path); + let res = if assumptions.is_empty() { self.solver.check() } else { From 57c4725eae034d7836d345bbf155c2899108545e Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 24 Feb 2025 19:28:34 +0100 Subject: [PATCH 02/41] Add SolverType and CommandError enums, update execute_swine and check_proof_assuming functions --- src/slicing/solver.rs | 4 +- z3rro/src/prover.rs | 142 +++++++++++++++++++++++++----------------- 2 files changed, 87 insertions(+), 59 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 3998b3d1..cd61a8fa 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -227,7 +227,7 @@ impl<'ctx> SliceSolver<'ctx> { self.prover.add_assumption(&self.slice_stmts.constraints); self.prover.add_assumption(&inactive_formula); - let res = self.prover.check_proof_assuming(&active_toggle_values); + let res = self.prover.check_proof_assuming(&active_toggle_values, z3rro::prover::SolverType::SWINE); let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone()); if let ProveResult::Proof = res { @@ -605,7 +605,7 @@ fn check_proof_seed<'ctx>( prover.set_timeout(timeout); let seed: Vec<_> = seed.iter().cloned().collect(); - prover.check_proof_assuming(&seed) + prover.check_proof_assuming(&seed, z3rro::prover::SolverType::SWINE) } fn unsat_core_to_seed<'ctx>( diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 635ea4b8..19990472 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -1,8 +1,7 @@ //! Not a SAT solver, but a prover. There's a difference. +use thiserror::Error; -//use std::{fmt::Display, time::Duration}; - -use std::{collections::VecDeque, fmt::Display, io::Write, path::Path, process::Command, time::Duration}; +use std::{collections::VecDeque, env, fmt::Display, io::{self, Write}, path::Path, process::{self, Command}, time::Duration}; use tempfile::NamedTempFile; @@ -17,6 +16,18 @@ use crate::{ util::{set_solver_timeout, ReasonUnknown}, }; +#[derive(Debug, Error)] +pub enum CommandError { + #[error("Environment variable error: {0}")] + EnvVarError(#[from] env::VarError), + #[error("Process execution failed: {0}")] + ProcessError(#[from] io::Error), +} +pub enum SolverType { + Z3, + SWINE, +} + /// The result of a prove query. #[derive(Debug)] pub enum ProveResult<'ctx> { @@ -25,40 +36,40 @@ pub enum ProveResult<'ctx> { Unknown(ReasonUnknown), } -/// Find the swine-z3 file located under the dir directory, and execute swine-z3 on the file located at file_path -fn execute_swine(dir: &Path, file_path: &Path) { - let swine = "swine-z3"; - - let find_output = Command::new("find") - .arg(dir) - .arg("-name") - .arg(swine) - .output().unwrap(); - - if find_output.status.success() { - let stdout = String::from_utf8_lossy(&find_output.stdout); - - for line in stdout.lines().rev() { - let path = Path::new(line); - - if path.exists() && path.is_file() { - let cmd_output = Command::new(path) - .arg(file_path) - .output().unwrap(); - - if cmd_output.status.success() { - println!("{}", String::from_utf8_lossy(&cmd_output.stdout)); - break; - } else { - eprintln!("Failed to execute swine({}) command with status: {}", line, cmd_output.status); +/// Execute swine-z3 on the file located at file_path +fn execute_swine(file_path: &Path) -> Result{ + match env::var("SWINE") { + // Use "export SWINE=" to set the path for swine in the SWINE variable. + Ok(swine) => { + let output = Command::new(swine) + .arg(file_path) + .output(); + + match output { + Ok(output) => { + let stdout = String::from_utf8_lossy(&output.stdout); + + if stdout.contains("unsat") { + Ok(SatResult::Unsat) + } else if stdout.contains("sat") { + Ok(SatResult::Sat) + } else { + Ok(SatResult::Unknown) + } + } + Err(e) => { + Err(CommandError::ProcessError(e)) } } } - } else { - eprintln!("Find command execution failed"); + Err(e) => { + Err(CommandError::EnvVarError(e)) + } } } +/// In order to execute the program, it is necessary to remove lines that +/// contain a forall quantifier or the declaration of the exponential function (exp). fn remove_lines_for_swine(input: &str) -> String { let mut output = String::new(); let mut tmp_buffer: VecDeque = VecDeque::new(); @@ -151,42 +162,59 @@ impl<'ctx> Prover<'ctx> { } pub fn check_proof(&mut self) -> ProveResult<'ctx> { - self.check_proof_assuming(&[]) + self.check_proof_assuming(&[], SolverType::SWINE) } /// Do the SAT check, but consider a check with no provables to be a /// [`ProveResult::Proof`]. - pub fn check_proof_assuming(&mut self, assumptions: &[Bool<'ctx>]) -> ProveResult<'ctx> { + pub fn check_proof_assuming(&mut self, assumptions: &[Bool<'ctx>], solver_type: SolverType) -> ProveResult<'ctx> { if self.min_level_with_provables.is_none() { return ProveResult::Proof; } - let mut smtlib = self.get_smtlib(); - - smtlib.add_check_sat(); - - let smtlib = smtlib.into_string(); - let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); - - smt_file.write_all(remove_lines_for_swine(&smtlib).as_bytes()).unwrap(); - - let file_path = smt_file.path(); - let start_dir = Path::new("../"); + let res; - execute_swine(start_dir, file_path); + match solver_type { + SolverType::SWINE => { + let mut smtlib = self.get_smtlib(); + smtlib.add_check_sat(); + let smtlib = smtlib.into_string(); + let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); + smt_file.write_all(remove_lines_for_swine(&smtlib).as_bytes()).unwrap(); + let file_path = smt_file.path(); - let res = if assumptions.is_empty() { - self.solver.check() - } else { - self.solver.check_assumptions(assumptions) - }; - match res { - SatResult::Unsat => ProveResult::Proof, - SatResult::Unknown => ProveResult::Unknown(self.get_reason_unknown().unwrap()), - SatResult::Sat => { - let model = self.get_model().unwrap(); - let model = InstrumentedModel::new(model); - ProveResult::Counterexample(model) + res = execute_swine(file_path).unwrap_or_else(|e| { + eprintln!("{}", e); + process::exit(1) + }); + match res { + SatResult::Unsat => ProveResult::Proof, + SatResult::Unknown => { + // TODO: Determine the correct reason for Unknown + ProveResult::Unknown(ReasonUnknown::Other("unknown".to_string())) + }, + SatResult::Sat => { + // TODO: Get the model from the output of SWINE + println!("The Result of SWINE: sat"); + process::exit(1) + } + } + } + SolverType::Z3 => { + res = if assumptions.is_empty() { + self.solver.check() + } else { + self.solver.check_assumptions(assumptions) + }; + match res { + SatResult::Unsat => ProveResult::Proof, + SatResult::Unknown => ProveResult::Unknown(self.get_reason_unknown().unwrap()), + SatResult::Sat => { + let model = self.get_model().unwrap(); + let model = InstrumentedModel::new(model); + ProveResult::Counterexample(model) + } + } } } } From 9b6388a5d740cded2238715780f6ca4f68957a71 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 10 Mar 2025 16:53:15 +0100 Subject: [PATCH 03/41] No functional changes --- src/slicing/solver.rs | 4 +++- z3rro/src/prover.rs | 41 +++++++++++++++++++++++++---------------- 2 files changed, 28 insertions(+), 17 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index cd61a8fa..2712a4a8 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -227,7 +227,9 @@ impl<'ctx> SliceSolver<'ctx> { self.prover.add_assumption(&self.slice_stmts.constraints); self.prover.add_assumption(&inactive_formula); - let res = self.prover.check_proof_assuming(&active_toggle_values, z3rro::prover::SolverType::SWINE); + let res = self + .prover + .check_proof_assuming(&active_toggle_values, z3rro::prover::SolverType::SWINE); let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone()); if let ProveResult::Proof = res { diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 19990472..7b151480 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -1,7 +1,15 @@ //! Not a SAT solver, but a prover. There's a difference. use thiserror::Error; -use std::{collections::VecDeque, env, fmt::Display, io::{self, Write}, path::Path, process::{self, Command}, time::Duration}; +use std::{ + collections::VecDeque, + env, + fmt::Display, + io::{self, Write}, + path::Path, + process::{self, Command}, + time::Duration, +}; use tempfile::NamedTempFile; @@ -23,6 +31,7 @@ pub enum CommandError { #[error("Process execution failed: {0}")] ProcessError(#[from] io::Error), } + pub enum SolverType { Z3, SWINE, @@ -37,13 +46,11 @@ pub enum ProveResult<'ctx> { } /// Execute swine-z3 on the file located at file_path -fn execute_swine(file_path: &Path) -> Result{ +fn execute_swine(file_path: &Path) -> Result { match env::var("SWINE") { // Use "export SWINE=" to set the path for swine in the SWINE variable. Ok(swine) => { - let output = Command::new(swine) - .arg(file_path) - .output(); + let output = Command::new(swine).arg(file_path).output(); match output { Ok(output) => { @@ -57,18 +64,14 @@ fn execute_swine(file_path: &Path) -> Result{ Ok(SatResult::Unknown) } } - Err(e) => { - Err(CommandError::ProcessError(e)) - } + Err(e) => Err(CommandError::ProcessError(e)), } } - Err(e) => { - Err(CommandError::EnvVarError(e)) - } + Err(e) => Err(CommandError::EnvVarError(e)), } } -/// In order to execute the program, it is necessary to remove lines that +/// In order to execute the program, it is necessary to remove lines that /// contain a forall quantifier or the declaration of the exponential function (exp). fn remove_lines_for_swine(input: &str) -> String { let mut output = String::new(); @@ -167,7 +170,11 @@ impl<'ctx> Prover<'ctx> { /// Do the SAT check, but consider a check with no provables to be a /// [`ProveResult::Proof`]. - pub fn check_proof_assuming(&mut self, assumptions: &[Bool<'ctx>], solver_type: SolverType) -> ProveResult<'ctx> { + pub fn check_proof_assuming( + &mut self, + assumptions: &[Bool<'ctx>], + solver_type: SolverType, + ) -> ProveResult<'ctx> { if self.min_level_with_provables.is_none() { return ProveResult::Proof; } @@ -180,9 +187,11 @@ impl<'ctx> Prover<'ctx> { smtlib.add_check_sat(); let smtlib = smtlib.into_string(); let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); - smt_file.write_all(remove_lines_for_swine(&smtlib).as_bytes()).unwrap(); + smt_file + .write_all(remove_lines_for_swine(&smtlib).as_bytes()) + .unwrap(); let file_path = smt_file.path(); - + res = execute_swine(file_path).unwrap_or_else(|e| { eprintln!("{}", e); process::exit(1) @@ -192,7 +201,7 @@ impl<'ctx> Prover<'ctx> { SatResult::Unknown => { // TODO: Determine the correct reason for Unknown ProveResult::Unknown(ReasonUnknown::Other("unknown".to_string())) - }, + } SatResult::Sat => { // TODO: Get the model from the output of SWINE println!("The Result of SWINE: sat"); From 9120d446c9f86084c4a636ba987103a41b77ec22 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 10 Mar 2025 18:01:24 +0100 Subject: [PATCH 04/41] Execute swine directly in the command line --- z3rro/src/prover.rs | 34 ++++++++++++++-------------------- 1 file changed, 14 insertions(+), 20 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 7b151480..faf58a4f 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -45,29 +45,23 @@ pub enum ProveResult<'ctx> { Unknown(ReasonUnknown), } -/// Execute swine-z3 on the file located at file_path +/// Execute swine on the file located at file_path fn execute_swine(file_path: &Path) -> Result { - match env::var("SWINE") { - // Use "export SWINE=" to set the path for swine in the SWINE variable. - Ok(swine) => { - let output = Command::new(swine).arg(file_path).output(); - - match output { - Ok(output) => { - let stdout = String::from_utf8_lossy(&output.stdout); - - if stdout.contains("unsat") { - Ok(SatResult::Unsat) - } else if stdout.contains("sat") { - Ok(SatResult::Sat) - } else { - Ok(SatResult::Unknown) - } - } - Err(e) => Err(CommandError::ProcessError(e)), + let output = Command::new("swine").arg(file_path).output(); + + match output { + Ok(output) => { + let stdout = String::from_utf8_lossy(&output.stdout); + + if stdout.contains("unsat") { + Ok(SatResult::Unsat) + } else if stdout.contains("sat") { + Ok(SatResult::Sat) + } else { + Ok(SatResult::Unknown) } } - Err(e) => Err(CommandError::EnvVarError(e)), + Err(e) => Err(CommandError::ProcessError(e)), } } From 9a0db09b208c0c3ffe3796253af375218ecb3048 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 19 Mar 2025 18:51:22 +0100 Subject: [PATCH 05/41] Add SolverType attribute to Prover struct and SMT solver options --- src/driver.rs | 14 ++++++++++---- src/main.rs | 19 +++++++++++++++++++ src/opt/fuzz_test.rs | 4 ++-- src/opt/unfolder.rs | 4 ++-- src/slicing/solver.rs | 4 ++-- src/slicing/transform_test.rs | 4 ++-- z3rro/src/prover.rs | 17 ++++++++++------- z3rro/src/test.rs | 4 ++-- 8 files changed, 49 insertions(+), 21 deletions(-) diff --git a/src/driver.rs b/src/driver.rs index 9080b23e..8a039cc2 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -53,7 +53,7 @@ use crate::{ vcgen::Vcgen, }, version::write_detailed_version_info, - DebugOptions, SliceOptions, SliceVerifyMethod, VerifyCommand, VerifyError, + DebugOptions, SliceOptions, SliceVerifyMethod, VerifyCommand, VerifyError, SMTSolverType, }; use ariadne::ReportKind; @@ -64,7 +64,7 @@ use z3::{ }; use z3rro::{ probes::ProbeSummary, - prover::{ProveResult, Prover}, + prover::{ProveResult, Prover, SolverType}, smtlib::Smtlib, util::{PrefixWriter, ReasonUnknown}, }; @@ -695,7 +695,7 @@ impl<'ctx> SmtVcUnit<'ctx> { let span = info_span!("SAT check"); let _entered = span.enter(); - let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc); + let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc, options.smt_solver_options.smt_solver); if options.debug_options.probe { let goal = Goal::new(ctx, false, false, false); @@ -797,9 +797,15 @@ fn mk_valid_query_prover<'smt, 'ctx>( ctx: &'ctx Context, smt_translate: &TranslateExprs<'smt, 'ctx>, valid_query: &Bool<'ctx>, + smt_solver: SMTSolverType, ) -> Prover<'ctx> { + let solver_type = match smt_solver { + SMTSolverType::Swine => SolverType::SWINE, + SMTSolverType::Z3 => SolverType::Z3, + }; + // create the prover and set the params - let mut prover = Prover::new(ctx); + let mut prover = Prover::new(ctx, solver_type); if let Some(remaining) = limits_ref.time_left() { prover.set_timeout(remaining); } diff --git a/src/main.rs b/src/main.rs index c4474386..c5bfef56 100644 --- a/src/main.rs +++ b/src/main.rs @@ -138,6 +138,9 @@ pub struct VerifyCommand { #[command(flatten)] pub debug_options: DebugOptions, + + #[command(flatten)] + pub smt_solver_options: SMTSolverOptions, } #[derive(Debug, Args)] @@ -376,6 +379,22 @@ pub struct DebugOptions { pub probe: bool, } +#[derive(Debug, Default, Args)] +#[command(next_help_heading = "SMT Solver Options")] +pub struct SMTSolverOptions { + #[arg(long, default_value = "z3")] + pub smt_solver: SMTSolverType, +} + +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)] +pub enum SMTSolverType { + #[default] + #[value(name = "z3")] + Z3, + #[value(name = "swine")] + Swine, +} + #[derive(Debug, Default, Args)] #[command(next_help_heading = "Slicing Options")] pub struct SliceOptions { diff --git a/src/opt/fuzz_test.rs b/src/opt/fuzz_test.rs index 97b778c6..cb9b4e8d 100644 --- a/src/opt/fuzz_test.rs +++ b/src/opt/fuzz_test.rs @@ -2,7 +2,7 @@ use proptest::{ prelude::*, test_runner::{TestCaseResult, TestRunner}, }; -use z3rro::prover::{ProveResult, Prover}; +use z3rro::prover::{ProveResult, Prover, SolverType}; use crate::{ ast::{ @@ -201,7 +201,7 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult { let smt_ctx = SmtCtx::new(&ctx, tcx); let mut translate = TranslateExprs::new(&smt_ctx); let eq_expr_z3 = translate.t_bool(&eq_expr); - let mut prover = Prover::new(&ctx); + let mut prover = Prover::new(&ctx, SolverType::Z3); translate .local_scope() .add_assumptions_to_prover(&mut prover); diff --git a/src/opt/unfolder.rs b/src/opt/unfolder.rs index 7efcf865..ad8b6df4 100644 --- a/src/opt/unfolder.rs +++ b/src/opt/unfolder.rs @@ -25,7 +25,7 @@ use std::ops::DerefMut; use z3::SatResult; -use z3rro::prover::Prover; +use z3rro::prover::{Prover, SolverType}; use crate::{ ast::{ @@ -63,7 +63,7 @@ impl<'smt, 'ctx> Unfolder<'smt, 'ctx> { limits_ref: limits_ref.clone(), subst: Subst::new(ctx.tcx(), &limits_ref), translate: TranslateExprs::new(ctx), - prover: Prover::new(ctx.ctx()), + prover: Prover::new(ctx.ctx(), SolverType::Z3), } } diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 2712a4a8..5f1228aa 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -229,7 +229,7 @@ impl<'ctx> SliceSolver<'ctx> { self.prover.add_assumption(&inactive_formula); let res = self .prover - .check_proof_assuming(&active_toggle_values, z3rro::prover::SolverType::SWINE); + .check_proof_assuming(&active_toggle_values); let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone()); if let ProveResult::Proof = res { @@ -607,7 +607,7 @@ fn check_proof_seed<'ctx>( prover.set_timeout(timeout); let seed: Vec<_> = seed.iter().cloned().collect(); - prover.check_proof_assuming(&seed, z3rro::prover::SolverType::SWINE) + prover.check_proof_assuming(&seed) } fn unsat_core_to_seed<'ctx>( diff --git a/src/slicing/transform_test.rs b/src/slicing/transform_test.rs index ff5fb2b0..c78e8361 100644 --- a/src/slicing/transform_test.rs +++ b/src/slicing/transform_test.rs @@ -5,7 +5,7 @@ use std::time::{Duration, Instant}; use itertools::Itertools; use z3rro::{ model::SmtEval, - prover::{ProveResult, Prover}, + prover::{ProveResult, Prover, SolverType}, }; use crate::{ @@ -128,7 +128,7 @@ fn prove_equiv( let smt_ctx = SmtCtx::new(&ctx, tcx); let mut translate = TranslateExprs::new(&smt_ctx); let eq_expr_z3 = translate.t_bool(&eq_expr); - let mut prover = Prover::new(&ctx); + let mut prover = Prover::new(&ctx, SolverType::Z3); translate .local_scope() .add_assumptions_to_prover(&mut prover); diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index faf58a4f..ef536478 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -32,6 +32,7 @@ pub enum CommandError { ProcessError(#[from] io::Error), } +#[derive(Debug)] pub enum SolverType { Z3, SWINE, @@ -127,15 +128,17 @@ pub struct Prover<'ctx> { level: usize, /// The minimum level where an assertion was added to the solver. min_level_with_provables: Option, + smt_solver: SolverType } impl<'ctx> Prover<'ctx> { /// Create a new prover with the given [`Context`]. - pub fn new(ctx: &'ctx Context) -> Self { + pub fn new(ctx: &'ctx Context, solver_type:SolverType) -> Self { Prover { solver: Solver::new(ctx), level: 0, min_level_with_provables: None, + smt_solver: solver_type, } } @@ -159,7 +162,7 @@ impl<'ctx> Prover<'ctx> { } pub fn check_proof(&mut self) -> ProveResult<'ctx> { - self.check_proof_assuming(&[], SolverType::SWINE) + self.check_proof_assuming(&[]) } /// Do the SAT check, but consider a check with no provables to be a @@ -167,7 +170,6 @@ impl<'ctx> Prover<'ctx> { pub fn check_proof_assuming( &mut self, assumptions: &[Bool<'ctx>], - solver_type: SolverType, ) -> ProveResult<'ctx> { if self.min_level_with_provables.is_none() { return ProveResult::Proof; @@ -175,7 +177,7 @@ impl<'ctx> Prover<'ctx> { let res; - match solver_type { + match self.smt_solver { SolverType::SWINE => { let mut smtlib = self.get_smtlib(); smtlib.add_check_sat(); @@ -198,7 +200,6 @@ impl<'ctx> Prover<'ctx> { } SatResult::Sat => { // TODO: Get the model from the output of SWINE - println!("The Result of SWINE: sat"); process::exit(1) } } @@ -291,7 +292,7 @@ impl<'ctx> Prover<'ctx> { universal.iter().map(|v| v as &dyn Ast<'ctx>).collect(); let assertions = self.solver.get_assertions(); let theorem = forall_const(ctx, &universal, &[], &Bool::and(ctx, &assertions).not()); - let mut res = Prover::new(ctx); + let mut res = Prover::new(ctx, SolverType::Z3); res.add_assumption(&theorem); res } @@ -306,12 +307,14 @@ impl<'ctx> Prover<'ctx> { mod test { use z3::{ast::Bool, Config, Context, SatResult}; + use crate::prover::SolverType; + use super::{ProveResult, Prover}; #[test] fn test_prover() { let ctx = Context::new(&Config::default()); - let mut prover = Prover::new(&ctx); + let mut prover = Prover::new(&ctx, SolverType::Z3); assert!(matches!(prover.check_proof(), ProveResult::Proof)); assert_eq!(prover.check_sat(), SatResult::Sat); diff --git a/z3rro/src/test.rs b/z3rro/src/test.rs index 167f2608..9cd28dda 100644 --- a/z3rro/src/test.rs +++ b/z3rro/src/test.rs @@ -4,7 +4,7 @@ use z3::{ast::Bool, Config, Context, SatResult}; -use crate::prover::{ProveResult, Prover}; +use crate::prover::{ProveResult, Prover, SolverType}; use super::scope::SmtScope; @@ -18,7 +18,7 @@ pub fn test_prove(f: impl for<'ctx> FnOnce(&'ctx Context, &mut SmtScope<'ctx>) - let mut scope = SmtScope::new(); let theorem = f(&ctx, &mut scope); - let mut prover = Prover::new(&ctx); + let mut prover = Prover::new(&ctx, SolverType::Z3); scope.add_assumptions_to_prover(&mut prover); assert_eq!( prover.check_sat(), From 619798699727c4d73c4735433504bef6929527fc Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 14 Apr 2025 16:30:49 +0200 Subject: [PATCH 06/41] Update check_proof_assuming to return Result for error handling --- src/main.rs | 8 ++++- src/opt/fuzz_test.rs | 9 +++-- src/slicing/solver.rs | 64 ++++++++++++++++++++--------------- src/slicing/transform_test.rs | 9 ++--- z3rro/src/prover.rs | 50 +++++++++++++-------------- z3rro/src/test.rs | 7 ++-- 6 files changed, 81 insertions(+), 66 deletions(-) diff --git a/src/main.rs b/src/main.rs index c5bfef56..225a3ce1 100644 --- a/src/main.rs +++ b/src/main.rs @@ -39,7 +39,7 @@ use tokio::task::JoinError; use tracing::{error, info, warn}; use vc::explain::VcExplanation; -use z3rro::{prover::ProveResult, util::ReasonUnknown}; +use z3rro::{prover::{ProveResult, ProverCommandError}, util::ReasonUnknown}; pub mod ast; mod driver; @@ -541,6 +541,10 @@ fn finalize_verify_result( tracing::error!("Interrupted"); ExitCode::from(130) // 130 seems to be a standard exit code for CTRL+C } + Err(VerifyError::ProverError(err)) => { + eprintln!("{}", err.to_string()); + ExitCode::from(1) + } } } @@ -620,6 +624,8 @@ pub enum VerifyError { /// The verifier was interrupted. #[error("interrupted")] Interrupted, + #[error("{0}")] + ProverError(#[from] ProverCommandError), } /// Verify a list of `user_files`. The `options.files` value is ignored here. diff --git a/src/opt/fuzz_test.rs b/src/opt/fuzz_test.rs index cb9b4e8d..f6d304c2 100644 --- a/src/opt/fuzz_test.rs +++ b/src/opt/fuzz_test.rs @@ -207,13 +207,16 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult { .add_assumptions_to_prover(&mut prover); prover.add_provable(&eq_expr_z3); let x = match prover.check_proof() { - ProveResult::Proof => Ok(()), - ProveResult::Counterexample(model) => Err(TestCaseError::fail(format!( + Ok(ProveResult::Proof) => Ok(()), + Ok(ProveResult::Counterexample(model)) => Err(TestCaseError::fail(format!( "rewrote {} ...into... {}, but those are not equivalent:\n{}", expr, optimized, model ))), - ProveResult::Unknown(reason) => { + Ok(ProveResult::Unknown(reason)) => { Err(TestCaseError::fail(format!("unknown result ({})", reason))) + }, + Err(err) => { + Err(TestCaseError::fail(format!("{}", err))) } }; x diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 5f1228aa..c82d63f0 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -7,13 +7,13 @@ use z3::{ }; use z3rro::{ model::InstrumentedModel, - prover::{ProveResult, Prover}, + prover::{ProveResult, Prover, ProverCommandError}, util::ReasonUnknown, }; use crate::{ ast::{ExprBuilder, Span}, - resource_limits::{LimitError, LimitsRef}, + resource_limits::LimitsRef, slicing::{ model::{SliceMode, SliceModel}, util::{PartialMinimizeResult, SubsetExploration}, @@ -232,7 +232,7 @@ impl<'ctx> SliceSolver<'ctx> { .check_proof_assuming(&active_toggle_values); let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone()); - if let ProveResult::Proof = res { + if let Ok(ProveResult::Proof) = res { slice_searcher.found_active(self.prover.get_unsat_core()); } @@ -322,14 +322,18 @@ impl<'ctx> SliceSolver<'ctx> { slice_sat_binary_search(&mut self.prover, &active_toggle_values, options, limits_ref)?; let res = self.prover.check_proof(); - let slice_model = if let ProveResult::Counterexample(model) = &res { - let slice_model = - SliceModel::from_model(SliceMode::Error, &self.slice_stmts, selection, model); - Some(slice_model) - } else { - None - }; - Ok((res, slice_model)) + + match res { + Err(err) => Err(VerifyError::ProverError(err)), + Ok(prove_result) => match &prove_result { + ProveResult::Counterexample(model) => { + let slice_model = + SliceModel::from_model(SliceMode::Error, &self.slice_stmts, selection, &model); + Ok((prove_result, Some(slice_model))) + }, + _ => Ok((prove_result, None)), + } + } } } @@ -551,36 +555,39 @@ pub fn slice_next_extremal_set<'ctx>( prover: &mut Prover<'ctx>, options: &SliceSolveOptions, limits_ref: &LimitsRef, -) -> Result>, LimitError> { +) -> Result>, VerifyError> { let all_variables = exploration.variables().clone(); while let Some(seed) = exploration.next_set() { limits_ref.check_limits()?; match check_proof_seed(prover, limits_ref, &seed) { - ProveResult::Proof => { + Ok(ProveResult::Proof) => { let seed = unsat_core_to_seed(prover, &all_variables); // now start the shrinking, then block up - let res = exploration.shrink_block_up(seed, |seed| { - match check_proof_seed(prover, limits_ref, seed) { - ProveResult::Proof => Some(unsat_core_to_seed(prover, &all_variables)), - ProveResult::Counterexample(_) | ProveResult::Unknown(_) => None, - } - }); + let res_seed = match check_proof_seed(prover, limits_ref, &seed) { + Ok(ProveResult::Proof) => Some(unsat_core_to_seed(prover, &all_variables)), + Ok(ProveResult::Counterexample(_)) | Ok(ProveResult::Unknown(_)) => None, + Err(err) => return Err(VerifyError::ProverError(err)), + }; + + let res = exploration.shrink_block_up(seed, |_| res_seed.clone()); return Ok(Some(ExtremalSet::MinimalUnsat(res))); } - ProveResult::Counterexample(_) => { + Ok(ProveResult::Counterexample(_)) => { // grow the counterexample and then block down - let res = exploration.grow_block_down(seed, |seed| { - match check_proof_seed(prover, limits_ref, seed) { - ProveResult::Counterexample(_) => true, - ProveResult::Proof | ProveResult::Unknown(_) => false, - } - }); + + let res_seed = match check_proof_seed(prover, limits_ref, &seed) { + Ok(ProveResult::Counterexample(_)) => true, + Ok(ProveResult::Proof) | Ok(ProveResult::Unknown(_)) => false, + Err(err) => return Err(VerifyError::ProverError(err)), + }; + + let res = exploration.grow_block_down(seed, |_| res_seed); return Ok(Some(ExtremalSet::MaximalSat(res))); } - ProveResult::Unknown(_) => { + Ok(ProveResult::Unknown(_)) => { if options.continue_on_unknown { // for seeds that result in unknown, just block them to // ensure progress. @@ -589,6 +596,7 @@ pub fn slice_next_extremal_set<'ctx>( return Ok(None); } } + Err(err) => return Err(VerifyError::ProverError(err)), } } Ok(None) @@ -599,7 +607,7 @@ fn check_proof_seed<'ctx>( prover: &mut Prover<'ctx>, limits_ref: &LimitsRef, seed: &HashSet>, -) -> ProveResult<'ctx> { +) -> Result, ProverCommandError> { let mut timeout = Duration::from_millis(100); if let Some(time_left) = limits_ref.time_left() { timeout = timeout.min(time_left); diff --git a/src/slicing/transform_test.rs b/src/slicing/transform_test.rs index c78e8361..951c78e3 100644 --- a/src/slicing/transform_test.rs +++ b/src/slicing/transform_test.rs @@ -138,14 +138,15 @@ fn prove_equiv( } prover.add_provable(&eq_expr_z3); let x = match prover.check_proof() { - ProveResult::Proof => Ok(()), - ProveResult::Counterexample(model) => Err(format!( + Ok(ProveResult::Proof) => Ok(()), + Ok(ProveResult::Counterexample(model)) => Err(format!( "we want to rewrite {:?} ...into... {:?} under assumptions {:?}, but those are not equivalent:\n{}\n original evaluates to {}\n rewritten evaluates to {}", stmt1, stmt2, assumptions, model, translate.t_eureal(&stmt1_vc).eval(&model).unwrap(), translate.t_eureal(&stmt2_vc).eval(&model).unwrap() )), - ProveResult::Unknown(reason) => { + Ok(ProveResult::Unknown(reason)) => { Err(format!("unknown result ({})", reason)) - } + }, + Err(err) => Err(format!("{}", err)) }; x } diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index ef536478..17a82c42 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -7,7 +7,7 @@ use std::{ fmt::Display, io::{self, Write}, path::Path, - process::{self, Command}, + process::Command, time::Duration, }; @@ -25,7 +25,7 @@ use crate::{ }; #[derive(Debug, Error)] -pub enum CommandError { +pub enum ProverCommandError { #[error("Environment variable error: {0}")] EnvVarError(#[from] env::VarError), #[error("Process execution failed: {0}")] @@ -47,7 +47,7 @@ pub enum ProveResult<'ctx> { } /// Execute swine on the file located at file_path -fn execute_swine(file_path: &Path) -> Result { +fn execute_swine(file_path: &Path) -> Result { let output = Command::new("swine").arg(file_path).output(); match output { @@ -62,7 +62,7 @@ fn execute_swine(file_path: &Path) -> Result { Ok(SatResult::Unknown) } } - Err(e) => Err(CommandError::ProcessError(e)), + Err(e) => Err(ProverCommandError::ProcessError(e)), } } @@ -161,7 +161,7 @@ impl<'ctx> Prover<'ctx> { self.min_level_with_provables.get_or_insert(self.level); } - pub fn check_proof(&mut self) -> ProveResult<'ctx> { + pub fn check_proof(&mut self) -> Result, ProverCommandError> { self.check_proof_assuming(&[]) } @@ -170,13 +170,11 @@ impl<'ctx> Prover<'ctx> { pub fn check_proof_assuming( &mut self, assumptions: &[Bool<'ctx>], - ) -> ProveResult<'ctx> { + ) -> Result, ProverCommandError> { if self.min_level_with_provables.is_none() { - return ProveResult::Proof; + return Ok(ProveResult::Proof); } - let res; - match self.smt_solver { SolverType::SWINE => { let mut smtlib = self.get_smtlib(); @@ -188,35 +186,33 @@ impl<'ctx> Prover<'ctx> { .unwrap(); let file_path = smt_file.path(); - res = execute_swine(file_path).unwrap_or_else(|e| { - eprintln!("{}", e); - process::exit(1) - }); + let res = execute_swine(file_path); match res { - SatResult::Unsat => ProveResult::Proof, - SatResult::Unknown => { + Ok(SatResult::Unsat) => Ok(ProveResult::Proof), + Ok(SatResult::Unknown) => { // TODO: Determine the correct reason for Unknown - ProveResult::Unknown(ReasonUnknown::Other("unknown".to_string())) - } - SatResult::Sat => { + Ok(ProveResult::Unknown(ReasonUnknown::Other("unknown".to_string()))) + }, + Ok(SatResult::Sat) => { // TODO: Get the model from the output of SWINE - process::exit(1) - } + panic!("no counterexample for swine") + }, + Err(err) => Err(err) } } SolverType::Z3 => { - res = if assumptions.is_empty() { + let res = if assumptions.is_empty() { self.solver.check() } else { self.solver.check_assumptions(assumptions) }; match res { - SatResult::Unsat => ProveResult::Proof, - SatResult::Unknown => ProveResult::Unknown(self.get_reason_unknown().unwrap()), + SatResult::Unsat => Ok(ProveResult::Proof), + SatResult::Unknown => Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())), SatResult::Sat => { let model = self.get_model().unwrap(); let model = InstrumentedModel::new(model); - ProveResult::Counterexample(model) + Ok(ProveResult::Counterexample(model)) } } } @@ -315,16 +311,16 @@ mod test { fn test_prover() { let ctx = Context::new(&Config::default()); let mut prover = Prover::new(&ctx, SolverType::Z3); - assert!(matches!(prover.check_proof(), ProveResult::Proof)); + assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof))); assert_eq!(prover.check_sat(), SatResult::Sat); prover.push(); prover.add_assumption(&Bool::from_bool(&ctx, true)); - assert!(matches!(prover.check_proof(), ProveResult::Proof)); + assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof))); assert_eq!(prover.check_sat(), SatResult::Sat); prover.pop(); - assert!(matches!(prover.check_proof(), ProveResult::Proof)); + assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof))); assert_eq!(prover.check_sat(), SatResult::Sat); } } diff --git a/z3rro/src/test.rs b/z3rro/src/test.rs index 9cd28dda..f7175369 100644 --- a/z3rro/src/test.rs +++ b/z3rro/src/test.rs @@ -28,13 +28,14 @@ pub fn test_prove(f: impl for<'ctx> FnOnce(&'ctx Context, &mut SmtScope<'ctx>) - prover.add_provable(&theorem); match prover.check_proof() { - ProveResult::Counterexample(model) => panic!( + Ok(ProveResult::Counterexample(model)) => panic!( "counter-example: {:?}\nsolver:\n{:?}", model, prover.solver() ), - ProveResult::Unknown(reason) => panic!("solver returned unknown ({})", reason), - ProveResult::Proof => {} + Ok(ProveResult::Unknown(reason)) => panic!("solver returned unknown ({})", reason), + Ok(ProveResult::Proof) => {}, + Err(_) => {} }; } From 854e42cc9dbd93daf81b11b7692b5b8c8d54cf46 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 30 Apr 2025 03:02:13 +0200 Subject: [PATCH 07/41] Implement AST evaluation functions for Bool, Int, Real types --- z3rro/Cargo.toml | 1 + z3rro/src/model.rs | 150 ++++++++++++++++++++++++++++++++++++++++++--- 2 files changed, 144 insertions(+), 7 deletions(-) diff --git a/z3rro/Cargo.toml b/z3rro/Cargo.toml index ee14818c..61768a93 100644 --- a/z3rro/Cargo.toml +++ b/z3rro/Cargo.toml @@ -15,6 +15,7 @@ thiserror = "1.0" im-rc = "15" enum-map = "2.7.3" itertools = "0.14.0" +smtlib-lowlevel = "0.3.0" [features] datatype-eureal = [] diff --git a/z3rro/src/model.rs b/z3rro/src/model.rs index 7e6985a5..75cd98e2 100644 --- a/z3rro/src/model.rs +++ b/z3rro/src/model.rs @@ -7,12 +7,28 @@ use std::{ }; use num::{BigInt, BigRational}; + +use smtlib_lowlevel::{ + ast::{ + FunctionDef, GetModelResponse, Identifier, ModelResponse, QualIdentifier, SpecConstant, + Term, + }, + lexicon::{Decimal, Symbol}, +}; + use thiserror::Error; + use z3::{ ast::{Ast, Bool, Dynamic, Int, Real}, FuncDecl, FuncInterp, Model, }; +#[derive(Debug)] +pub enum ModelSource<'ctx> { + Z3Model(Model<'ctx>), + SwineModel(GetModelResponse<'ctx>), +} + /// A [`z3::Model`] which keeps track of the accessed constants. This is useful /// to later print those constants which were not accessed by any of the /// [`SmtEval`] implementations (e.g. stuff generated by Z3 we don't know @@ -20,14 +36,14 @@ use z3::{ /// we know, and then print the rest of the assignments in the model as well. #[derive(Debug)] pub struct InstrumentedModel<'ctx> { - model: Model<'ctx>, + model: ModelSource<'ctx>, // TODO: turn this into a HashSet of FuncDecls when the type implements Hash accessed_decls: RefCell>, accessed_exprs: RefCell>>, } impl<'ctx> InstrumentedModel<'ctx> { - pub fn new(model: Model<'ctx>) -> Self { + pub fn new(model: ModelSource<'ctx>) -> Self { InstrumentedModel { model, accessed_decls: Default::default(), @@ -57,14 +73,129 @@ impl<'ctx> InstrumentedModel<'ctx> { /// the model. pub fn eval>(&self, ast: &T, model_completion: bool) -> Option { self.add_children_accessed(Dynamic::from_ast(ast)); - let res = self.model.eval(ast, model_completion)?; - Some(res) + match &self.model { + ModelSource::Z3Model(model) => { + let res = model.eval(ast, model_completion)?; + Some(res) + } + ModelSource::SwineModel(_) => todo!(), + } + } + + pub fn eval_ast_bool(&self, ast: &Bool<'ctx>) -> Option> { + let name = ast.decl().name(); + + if let ModelSource::SwineModel(s_model) = &self.model { + match Self::find_fun_def(s_model, &name) { + Some(fun_def) => match fun_def.3 { + Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( + "true", + )))) => Some(Bool::from_bool(ast.get_ctx(), true)), + Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( + "false", + )))) => Some(Bool::from_bool(ast.get_ctx(), false)), + _ => None, + }, + None => None, + } + } else { + None + } + } + + pub fn eval_ast_int(&self, ast: &Int<'ctx>) -> Option> { + let name = ast.decl().name(); + + if let ModelSource::SwineModel(s_model) = &self.model { + match Self::find_fun_def(s_model, &name) { + Some(fun_def) => match fun_def.3 { + Term::SpecConstant(SpecConstant::Numeral(numeral)) => { + if let Ok(n) = numeral.into_u128() { + let n_str = n.to_string(); + Int::from_str(ast.get_ctx(), &n_str) + } else { + None + } + } + _ => None, + }, + None => None, + } + } else { + None + } + } + + pub fn eval_ast_real(&self, ast: &Real<'ctx>) -> Option> { + let name = ast.decl().name(); + + if let ModelSource::SwineModel(s_model) = &self.model { + match Self::find_fun_def(s_model, &name) { + Some(fun_def) => match fun_def.3 { + Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { + if let Some((num, den)) = Self::from_str_to_num_den(d_str) { + Real::from_real_str(ast.get_ctx(), &num, &den) + } else { + None + } + } + _ => None, + }, + None => None, + } + } else { + None + } + } + + /// Convert a decimal string `d_str` into a pair of a numerator (`num`) and + /// a denominator (`den`) in the form of '[numeral]' strings such that: + /// d_str = num / den + pub fn from_str_to_num_den(d_str: &str) -> Option<(String, String)> { + if d_str.is_empty() { + return None; + } + + if let Some(pos) = d_str.find('.') { + let den = "1".to_string() + &"0".repeat(d_str.len() - pos - 1); + + let mut num = d_str.to_string(); + num.remove(pos); + num.trim_start_matches('0'); + + if num.is_empty() { + num = "0".to_string(); + } + + Some((num, den)) + } else { + Some((d_str.to_string(), "1".to_string())) + } + } + + /// Find a `FunctionDef` object defined for a given symbol `symbol` within the `model_res`. + pub fn find_fun_def( + model_res: &GetModelResponse<'ctx>, + symbol: &str, + ) -> Option<&'ctx FunctionDef<'ctx>> { + model_res.0.iter().find_map(|m_res| { + if let ModelResponse::DefineFun(fun_def) = m_res { + if fun_def.0.0 == symbol { + Some(fun_def) + } else { + None + } + } else { + None + } + }) } /// Get the function interpretation for this `f`. pub fn get_func_interp(&self, f: &FuncDecl<'ctx>) -> Option> { self.accessed_decls.borrow_mut().insert(f.name()); - self.model.get_func_interp(f) + todo!() + // self.model.get_func_interp(f) } /// Add this ast node and all its children to the accessed set. @@ -89,9 +220,12 @@ impl<'ctx> InstrumentedModel<'ctx> { /// Iterate over all function declarations that were not accessed using /// `eval` so far. pub fn iter_unaccessed(&self) -> impl Iterator> + '_ { + todo!() + /* self.model .iter() .filter(|decl| !self.accessed_decls.borrow().contains(&decl.name())) + */ } /// Reset the internally tracked accessed declarations and expressions. @@ -101,7 +235,8 @@ impl<'ctx> InstrumentedModel<'ctx> { } pub fn into_model(self) -> Model<'ctx> { - self.model + todo!() + // self.model } } @@ -109,7 +244,8 @@ impl<'ctx> InstrumentedModel<'ctx> { /// [`z3::Model`]'s implementation. impl Display for InstrumentedModel<'_> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - f.write_fmt(format_args!("{}", &self.model)) + todo!() + // f.write_fmt(format_args!("{}", &self.model)) } } From 793a28182188416abc378108b679e0ca523b8d06 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 30 Apr 2025 14:42:45 +0200 Subject: [PATCH 08/41] Add swine execution via spawn and parse output into CheckSatResponse and GetModelResponse --- z3rro/src/prover.rs | 73 ++++++++++++++++++++++++++++++++++++++------- 1 file changed, 62 insertions(+), 11 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 17a82c42..24bea69b 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -5,9 +5,9 @@ use std::{ collections::VecDeque, env, fmt::Display, - io::{self, Write}, + io::{self, BufRead, BufReader, Read, Write}, path::Path, - process::Command, + process::{Command, Stdio}, time::Duration, }; @@ -19,17 +19,24 @@ use z3::{ }; use crate::{ - model::InstrumentedModel, + model::{InstrumentedModel, ModelSource}, smtlib::Smtlib, util::{set_solver_timeout, ReasonUnknown}, }; +use smtlib_lowlevel::{ + ast::{CheckSatResponse, GetModelResponse}, + Storage, +}; + #[derive(Debug, Error)] pub enum ProverCommandError { #[error("Environment variable error: {0}")] EnvVarError(#[from] env::VarError), #[error("Process execution failed: {0}")] ProcessError(#[from] io::Error), + #[error("Parse error")] + ParseError, } #[derive(Debug)] @@ -128,12 +135,12 @@ pub struct Prover<'ctx> { level: usize, /// The minimum level where an assertion was added to the solver. min_level_with_provables: Option, - smt_solver: SolverType + smt_solver: SolverType, } impl<'ctx> Prover<'ctx> { /// Create a new prover with the given [`Context`]. - pub fn new(ctx: &'ctx Context, solver_type:SolverType) -> Self { + pub fn new(ctx: &'ctx Context, solver_type: SolverType) -> Self { Prover { solver: Solver::new(ctx), level: 0, @@ -186,18 +193,60 @@ impl<'ctx> Prover<'ctx> { .unwrap(); let file_path = smt_file.path(); + let child = Command::new("swine") + .arg(file_path) + .stdout(Stdio::piped()) + .stderr(Stdio::piped()) + .spawn(); + match child { + Ok(mut child) => { + if let Some(stdout) = child.stdout.take() { + let storage = Storage::new(); + let mut buffer = BufReader::new(stdout); + let mut line = String::new(); + buffer.read_line(&mut line)?; + + let sat_res = match CheckSatResponse::parse(&storage, &line) { + Ok(res) => res, + Err(e) => { + eprintln!("ParseError: {}", e); + panic!(); + } + }; + + let mut cex = String::new(); + buffer.read_to_string(&mut cex)?; + + if sat_res == CheckSatResponse::Sat { + match GetModelResponse::parse(&storage, &cex) { + Ok(model_res) => { + let model = InstrumentedModel::new( + ModelSource::SwineModel(model_res), + ); + println!("{:?}", model_res); + } + Err(e) => eprintln!("ParseError: {}", e), + } + } + } + } + Err(e) => eprintln!("Failed to spawn: {}", e), + } + let res = execute_swine(file_path); match res { Ok(SatResult::Unsat) => Ok(ProveResult::Proof), Ok(SatResult::Unknown) => { // TODO: Determine the correct reason for Unknown - Ok(ProveResult::Unknown(ReasonUnknown::Other("unknown".to_string()))) - }, + Ok(ProveResult::Unknown(ReasonUnknown::Other( + "unknown".to_string(), + ))) + } Ok(SatResult::Sat) => { // TODO: Get the model from the output of SWINE panic!("no counterexample for swine") - }, - Err(err) => Err(err) + } + Err(err) => Err(err), } } SolverType::Z3 => { @@ -208,10 +257,12 @@ impl<'ctx> Prover<'ctx> { }; match res { SatResult::Unsat => Ok(ProveResult::Proof), - SatResult::Unknown => Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())), + SatResult::Unknown => { + Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())) + } SatResult::Sat => { let model = self.get_model().unwrap(); - let model = InstrumentedModel::new(model); + let model = InstrumentedModel::new(ModelSource::Z3Model(model)); Ok(ProveResult::Counterexample(model)) } } From ae52982e56ab8c607eefd44bf881ee5c3428416c Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Tue, 6 May 2025 20:01:36 +0200 Subject: [PATCH 09/41] Move code of eval_ast_bool/int/real into SmtEval::eval --- z3rro/src/model.rs | 330 +++++++++++++++++++++++++-------------------- 1 file changed, 182 insertions(+), 148 deletions(-) diff --git a/z3rro/src/model.rs b/z3rro/src/model.rs index 75cd98e2..bab492f2 100644 --- a/z3rro/src/model.rs +++ b/z3rro/src/model.rs @@ -29,6 +29,49 @@ pub enum ModelSource<'ctx> { SwineModel(GetModelResponse<'ctx>), } +/// Convert a decimal string `d_str` into a pair of a numerator (`num`) and +/// a denominator (`den`) in the form of '[numeral]' strings such that: +/// d_str = num / den +fn from_str_to_num_den(d_str: &str) -> Option<(String, String)> { + if d_str.is_empty() { + return None; + } + + if let Some(pos) = d_str.find('.') { + let den = "1".to_string() + &"0".repeat(d_str.len() - pos - 1); + + let mut num = d_str.to_string(); + num.remove(pos); + num.trim_start_matches('0'); + + if num.is_empty() { + num = "0".to_string(); + } + + Some((num, den)) + } else { + Some((d_str.to_string(), "1".to_string())) + } +} + +/// Find a `FunctionDef` object defined for a given symbol `symbol` within the `model_res`. +fn find_fun_def<'ctx>( + model_res: &GetModelResponse<'ctx>, + symbol: &str, +) -> Option<&'ctx FunctionDef<'ctx>> { + model_res.0.iter().find_map(|m_res| { + if let ModelResponse::DefineFun(fun_def) = m_res { + if fun_def.0.0 == symbol { + Some(fun_def) + } else { + None + } + } else { + None + } + }) +} + /// A [`z3::Model`] which keeps track of the accessed constants. This is useful /// to later print those constants which were not accessed by any of the /// [`SmtEval`] implementations (e.g. stuff generated by Z3 we don't know @@ -82,115 +125,6 @@ impl<'ctx> InstrumentedModel<'ctx> { } } - pub fn eval_ast_bool(&self, ast: &Bool<'ctx>) -> Option> { - let name = ast.decl().name(); - - if let ModelSource::SwineModel(s_model) = &self.model { - match Self::find_fun_def(s_model, &name) { - Some(fun_def) => match fun_def.3 { - Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( - "true", - )))) => Some(Bool::from_bool(ast.get_ctx(), true)), - Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( - "false", - )))) => Some(Bool::from_bool(ast.get_ctx(), false)), - _ => None, - }, - None => None, - } - } else { - None - } - } - - pub fn eval_ast_int(&self, ast: &Int<'ctx>) -> Option> { - let name = ast.decl().name(); - - if let ModelSource::SwineModel(s_model) = &self.model { - match Self::find_fun_def(s_model, &name) { - Some(fun_def) => match fun_def.3 { - Term::SpecConstant(SpecConstant::Numeral(numeral)) => { - if let Ok(n) = numeral.into_u128() { - let n_str = n.to_string(); - Int::from_str(ast.get_ctx(), &n_str) - } else { - None - } - } - _ => None, - }, - None => None, - } - } else { - None - } - } - - pub fn eval_ast_real(&self, ast: &Real<'ctx>) -> Option> { - let name = ast.decl().name(); - - if let ModelSource::SwineModel(s_model) = &self.model { - match Self::find_fun_def(s_model, &name) { - Some(fun_def) => match fun_def.3 { - Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { - if let Some((num, den)) = Self::from_str_to_num_den(d_str) { - Real::from_real_str(ast.get_ctx(), &num, &den) - } else { - None - } - } - _ => None, - }, - None => None, - } - } else { - None - } - } - - /// Convert a decimal string `d_str` into a pair of a numerator (`num`) and - /// a denominator (`den`) in the form of '[numeral]' strings such that: - /// d_str = num / den - pub fn from_str_to_num_den(d_str: &str) -> Option<(String, String)> { - if d_str.is_empty() { - return None; - } - - if let Some(pos) = d_str.find('.') { - let den = "1".to_string() + &"0".repeat(d_str.len() - pos - 1); - - let mut num = d_str.to_string(); - num.remove(pos); - num.trim_start_matches('0'); - - if num.is_empty() { - num = "0".to_string(); - } - - Some((num, den)) - } else { - Some((d_str.to_string(), "1".to_string())) - } - } - - /// Find a `FunctionDef` object defined for a given symbol `symbol` within the `model_res`. - pub fn find_fun_def( - model_res: &GetModelResponse<'ctx>, - symbol: &str, - ) -> Option<&'ctx FunctionDef<'ctx>> { - model_res.0.iter().find_map(|m_res| { - if let ModelResponse::DefineFun(fun_def) = m_res { - if fun_def.0.0 == symbol { - Some(fun_def) - } else { - None - } - } else { - None - } - }) - } - /// Get the function interpretation for this `f`. pub fn get_func_interp(&self, f: &FuncDecl<'ctx>) -> Option> { self.accessed_decls.borrow_mut().insert(f.name()); @@ -269,11 +203,32 @@ impl<'ctx> SmtEval<'ctx> for Bool<'ctx> { type Value = bool; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - model - .eval(self, true) - .ok_or(SmtEvalError::EvalError)? - .as_bool() - .ok_or(SmtEvalError::ParseError) + match model.model { + ModelSource::Z3Model(_) => { + model + .eval(self, true) + .ok_or(SmtEvalError::EvalError)? + .as_bool() + .ok_or(SmtEvalError::ParseError) + }, + ModelSource::SwineModel(s_model) => { + + let name: String = self.decl().name(); + + match find_fun_def(&s_model, &name) { + Some(fun_def) => match fun_def.3 { + Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( + "true", + )))) => Ok(true), + Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( + "false", + )))) => Ok(false), + _ => Err(SmtEvalError::EvalError), + }, + None => Err(SmtEvalError::EvalError), + } + }, + } } } @@ -281,13 +236,33 @@ impl<'ctx> SmtEval<'ctx> for Int<'ctx> { type Value = BigInt; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - // TODO: Z3's as_i64 only returns an i64 value. is there something more complete? - let value = model - .eval(self, true) - .ok_or(SmtEvalError::EvalError)? - .as_i64() - .ok_or(SmtEvalError::ParseError)?; - Ok(BigInt::from(value)) + match model.model { + ModelSource::Z3Model(_) => { + // TODO: Z3's as_i64 only returns an i64 value. is there something more complete? + let value = model + .eval(self, true) + .ok_or(SmtEvalError::EvalError)? + .as_i64() + .ok_or(SmtEvalError::ParseError)?; + Ok(BigInt::from(value)) + } + ModelSource::SwineModel(s_model) => { + let name = self.decl().name(); + match find_fun_def(&s_model, &name) { + Some(fun_def) => match fun_def.3 { + Term::SpecConstant(SpecConstant::Numeral(numeral)) => { + if let Ok(n) = numeral.into_u128() { + Ok(BigInt::from(n)) + } else { + Err(SmtEvalError::EvalError) + } + } + _ => Err(SmtEvalError::EvalError), + }, + None => Err(SmtEvalError::EvalError), + } + }, + } } } @@ -295,38 +270,97 @@ impl<'ctx> SmtEval<'ctx> for Real<'ctx> { type Value = BigRational; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - let res = model - .eval(self, false) // TODO - .ok_or(SmtEvalError::EvalError)?; - - // The .as_real() method only returns a pair of i64 values. If the - // results don't fit in these types, we start some funky string parsing. - if let Some((num, den)) = res.as_real() { - Ok(BigRational::new(num.into(), den.into())) - } else { - // we parse a string of the form "(/ num.0 denom.0)" - let division_expr = format!("{:?}", res); - if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") { - return Err(SmtEvalError::ParseError); - } + match model.model { + ModelSource::Z3Model(_) => { + let res = model + .eval(self, false) // TODO + .ok_or(SmtEvalError::EvalError)?; + + // The .as_real() method only returns a pair of i64 values. If the + // results don't fit in these types, we start some funky string parsing. + if let Some((num, den)) = res.as_real() { + Ok(BigRational::new(num.into(), den.into())) + } else { + // we parse a string of the form "(/ num.0 denom.0)" + let division_expr = format!("{:?}", res); + if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") { + return Err(SmtEvalError::ParseError); + } - let mut parts = division_expr.split_ascii_whitespace(); + let mut parts = division_expr.split_ascii_whitespace(); - let first_part = parts.next().ok_or(SmtEvalError::ParseError)?; - if first_part != "(/" { - return Err(SmtEvalError::ParseError); - } + let first_part = parts.next().ok_or(SmtEvalError::ParseError)?; + if first_part != "(/" { + return Err(SmtEvalError::ParseError); + } - let second_part = parts.next().ok_or(SmtEvalError::ParseError)?; - let second_part = second_part.replace(".0", ""); - let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?; + let second_part = parts.next().ok_or(SmtEvalError::ParseError)?; + let second_part = second_part.replace(".0", ""); + let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?; - let third_part = parts.next().ok_or(SmtEvalError::ParseError)?; - let third_part = third_part.replace(".0)", ""); - let denominator = - BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?; + let third_part = parts.next().ok_or(SmtEvalError::ParseError)?; + let third_part = third_part.replace(".0)", ""); + let denominator = + BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?; - Ok(BigRational::new(numerator, denominator)) + Ok(BigRational::new(numerator, denominator)) + } + }, + ModelSource::SwineModel(s_model) => { + let name = self.decl().name(); + + match find_fun_def(&s_model, &name) { + Some(fun_def) => match fun_def.3 { + Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { + let f = (*d_str).parse::().map_err(|_| SmtEvalError::EvalError)?; + let res = BigRational::from_float(f).ok_or(SmtEvalError::EvalError)?; + Ok(res) + } + Term::Application(QualIdentifier::Identifier(Identifier::Simple(Symbol("/"))), [t1, t2]) => { + let mut num = BigInt::from(1); + let mut den = BigInt::from(1); + match t1 { + Term::SpecConstant(SpecConstant::Numeral(numeral)) => { + let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?; + num *= BigInt::from(n); + }, + Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { + if let Some((n, d)) = from_str_to_num_den(d_str) { + num *= BigInt::from_str(&n).map_err(|_| SmtEvalError::EvalError)?; + den *= BigInt::from_str(&d).map_err(|_| SmtEvalError::EvalError)?; + } else { + return Err(SmtEvalError::EvalError); + } + }, + _ => { + return Err(SmtEvalError::EvalError); + }, + } + match t2 { + Term::SpecConstant(SpecConstant::Numeral(numeral)) => { + let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?; + den *= BigInt::from(n); + }, + Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { + if let Some((n, d)) = from_str_to_num_den(d_str) { + den *= BigInt::from_str(&n).map_err(|_| SmtEvalError::EvalError)?; + num *= BigInt::from_str(&d).map_err(|_| SmtEvalError::EvalError)?; + } else { + return Err(SmtEvalError::EvalError); + } + }, + _ => { + return Err(SmtEvalError::EvalError); + }, + } + Ok(BigRational::new(num, den)) + } + _ => Err(SmtEvalError::EvalError), + }, + None => Err(SmtEvalError::EvalError), + } + }, } + } } From 3a41142e533a4b9f580833a148689dc88c9ce27b Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Tue, 6 May 2025 21:38:19 +0200 Subject: [PATCH 10/41] Change return type of from_str_to_num_den from (String, String) to (BigInt, BigInt) --- z3rro/src/model.rs | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/z3rro/src/model.rs b/z3rro/src/model.rs index bab492f2..9aa39a6c 100644 --- a/z3rro/src/model.rs +++ b/z3rro/src/model.rs @@ -32,25 +32,22 @@ pub enum ModelSource<'ctx> { /// Convert a decimal string `d_str` into a pair of a numerator (`num`) and /// a denominator (`den`) in the form of '[numeral]' strings such that: /// d_str = num / den -fn from_str_to_num_den(d_str: &str) -> Option<(String, String)> { +fn from_str_to_num_den(d_str: &str) -> Option<(BigInt, BigInt)> { if d_str.is_empty() { return None; } - if let Some(pos) = d_str.find('.') { - let den = "1".to_string() + &"0".repeat(d_str.len() - pos - 1); - - let mut num = d_str.to_string(); - num.remove(pos); - num.trim_start_matches('0'); - - if num.is_empty() { - num = "0".to_string(); - } + if d_str.ends_with(".0") { + let num = BigInt::from_str(&d_str.replace(".0", "")).ok()?; + Some((num, BigInt::from(1))) + } else if let Some(pos) = d_str.find('.') { + let den = BigInt::from(10).pow((d_str.len() - pos - 1).try_into().unwrap()); + let num = BigInt::from_str(&d_str.replace(".", "")).ok()?; Some((num, den)) } else { - Some((d_str.to_string(), "1".to_string())) + let num = BigInt::from_str(d_str).ok()?; + Some((num, BigInt::from(1))) } } @@ -326,8 +323,8 @@ impl<'ctx> SmtEval<'ctx> for Real<'ctx> { }, Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { if let Some((n, d)) = from_str_to_num_den(d_str) { - num *= BigInt::from_str(&n).map_err(|_| SmtEvalError::EvalError)?; - den *= BigInt::from_str(&d).map_err(|_| SmtEvalError::EvalError)?; + num *= n; + den *= d; } else { return Err(SmtEvalError::EvalError); } @@ -343,8 +340,8 @@ impl<'ctx> SmtEval<'ctx> for Real<'ctx> { }, Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { if let Some((n, d)) = from_str_to_num_den(d_str) { - den *= BigInt::from_str(&n).map_err(|_| SmtEvalError::EvalError)?; - num *= BigInt::from_str(&d).map_err(|_| SmtEvalError::EvalError)?; + den *= n; + num *= d; } else { return Err(SmtEvalError::EvalError); } From 35b0ef47186cb6e4699b3a1070a81ff7d8d41909 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 12 May 2025 20:41:42 +0200 Subject: [PATCH 11/41] Parse counterexample from swine via solver.from_string --- z3rro/src/model.rs | 256 ++++++++------------------------------------ z3rro/src/prover.rs | 87 +++++---------- 2 files changed, 73 insertions(+), 270 deletions(-) diff --git a/z3rro/src/model.rs b/z3rro/src/model.rs index 9aa39a6c..f672a1ef 100644 --- a/z3rro/src/model.rs +++ b/z3rro/src/model.rs @@ -8,13 +8,6 @@ use std::{ use num::{BigInt, BigRational}; -use smtlib_lowlevel::{ - ast::{ - FunctionDef, GetModelResponse, Identifier, ModelResponse, QualIdentifier, SpecConstant, - Term, - }, - lexicon::{Decimal, Symbol}, -}; use thiserror::Error; @@ -23,52 +16,6 @@ use z3::{ FuncDecl, FuncInterp, Model, }; -#[derive(Debug)] -pub enum ModelSource<'ctx> { - Z3Model(Model<'ctx>), - SwineModel(GetModelResponse<'ctx>), -} - -/// Convert a decimal string `d_str` into a pair of a numerator (`num`) and -/// a denominator (`den`) in the form of '[numeral]' strings such that: -/// d_str = num / den -fn from_str_to_num_den(d_str: &str) -> Option<(BigInt, BigInt)> { - if d_str.is_empty() { - return None; - } - - if d_str.ends_with(".0") { - let num = BigInt::from_str(&d_str.replace(".0", "")).ok()?; - Some((num, BigInt::from(1))) - } else if let Some(pos) = d_str.find('.') { - let den = BigInt::from(10).pow((d_str.len() - pos - 1).try_into().unwrap()); - let num = BigInt::from_str(&d_str.replace(".", "")).ok()?; - - Some((num, den)) - } else { - let num = BigInt::from_str(d_str).ok()?; - Some((num, BigInt::from(1))) - } -} - -/// Find a `FunctionDef` object defined for a given symbol `symbol` within the `model_res`. -fn find_fun_def<'ctx>( - model_res: &GetModelResponse<'ctx>, - symbol: &str, -) -> Option<&'ctx FunctionDef<'ctx>> { - model_res.0.iter().find_map(|m_res| { - if let ModelResponse::DefineFun(fun_def) = m_res { - if fun_def.0.0 == symbol { - Some(fun_def) - } else { - None - } - } else { - None - } - }) -} - /// A [`z3::Model`] which keeps track of the accessed constants. This is useful /// to later print those constants which were not accessed by any of the /// [`SmtEval`] implementations (e.g. stuff generated by Z3 we don't know @@ -76,14 +23,14 @@ fn find_fun_def<'ctx>( /// we know, and then print the rest of the assignments in the model as well. #[derive(Debug)] pub struct InstrumentedModel<'ctx> { - model: ModelSource<'ctx>, + model: Model<'ctx>, // TODO: turn this into a HashSet of FuncDecls when the type implements Hash accessed_decls: RefCell>, accessed_exprs: RefCell>>, } impl<'ctx> InstrumentedModel<'ctx> { - pub fn new(model: ModelSource<'ctx>) -> Self { + pub fn new(model: Model<'ctx>) -> Self { InstrumentedModel { model, accessed_decls: Default::default(), @@ -113,20 +60,14 @@ impl<'ctx> InstrumentedModel<'ctx> { /// the model. pub fn eval>(&self, ast: &T, model_completion: bool) -> Option { self.add_children_accessed(Dynamic::from_ast(ast)); - match &self.model { - ModelSource::Z3Model(model) => { - let res = model.eval(ast, model_completion)?; - Some(res) - } - ModelSource::SwineModel(_) => todo!(), - } + let res = self.model.eval(ast, model_completion)?; + Some(res) } /// Get the function interpretation for this `f`. pub fn get_func_interp(&self, f: &FuncDecl<'ctx>) -> Option> { self.accessed_decls.borrow_mut().insert(f.name()); - todo!() - // self.model.get_func_interp(f) + self.model.get_func_interp(f) } /// Add this ast node and all its children to the accessed set. @@ -151,12 +92,9 @@ impl<'ctx> InstrumentedModel<'ctx> { /// Iterate over all function declarations that were not accessed using /// `eval` so far. pub fn iter_unaccessed(&self) -> impl Iterator> + '_ { - todo!() - /* self.model .iter() .filter(|decl| !self.accessed_decls.borrow().contains(&decl.name())) - */ } /// Reset the internally tracked accessed declarations and expressions. @@ -166,8 +104,7 @@ impl<'ctx> InstrumentedModel<'ctx> { } pub fn into_model(self) -> Model<'ctx> { - todo!() - // self.model + self.model } } @@ -175,8 +112,7 @@ impl<'ctx> InstrumentedModel<'ctx> { /// [`z3::Model`]'s implementation. impl Display for InstrumentedModel<'_> { fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { - todo!() - // f.write_fmt(format_args!("{}", &self.model)) + f.write_fmt(format_args!("{}", &self.model)) } } @@ -200,32 +136,11 @@ impl<'ctx> SmtEval<'ctx> for Bool<'ctx> { type Value = bool; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - match model.model { - ModelSource::Z3Model(_) => { - model - .eval(self, true) - .ok_or(SmtEvalError::EvalError)? - .as_bool() - .ok_or(SmtEvalError::ParseError) - }, - ModelSource::SwineModel(s_model) => { - - let name: String = self.decl().name(); - - match find_fun_def(&s_model, &name) { - Some(fun_def) => match fun_def.3 { - Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( - "true", - )))) => Ok(true), - Term::Identifier(QualIdentifier::Identifier(Identifier::Simple(Symbol( - "false", - )))) => Ok(false), - _ => Err(SmtEvalError::EvalError), - }, - None => Err(SmtEvalError::EvalError), - } - }, - } + model + .eval(self, true) + .ok_or(SmtEvalError::EvalError)? + .as_bool() + .ok_or(SmtEvalError::ParseError) } } @@ -233,33 +148,13 @@ impl<'ctx> SmtEval<'ctx> for Int<'ctx> { type Value = BigInt; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - match model.model { - ModelSource::Z3Model(_) => { - // TODO: Z3's as_i64 only returns an i64 value. is there something more complete? - let value = model - .eval(self, true) - .ok_or(SmtEvalError::EvalError)? - .as_i64() - .ok_or(SmtEvalError::ParseError)?; - Ok(BigInt::from(value)) - } - ModelSource::SwineModel(s_model) => { - let name = self.decl().name(); - match find_fun_def(&s_model, &name) { - Some(fun_def) => match fun_def.3 { - Term::SpecConstant(SpecConstant::Numeral(numeral)) => { - if let Ok(n) = numeral.into_u128() { - Ok(BigInt::from(n)) - } else { - Err(SmtEvalError::EvalError) - } - } - _ => Err(SmtEvalError::EvalError), - }, - None => Err(SmtEvalError::EvalError), - } - }, - } + // TODO: Z3's as_i64 only returns an i64 value. is there something more complete? + let value = model + .eval(self, true) + .ok_or(SmtEvalError::EvalError)? + .as_i64() + .ok_or(SmtEvalError::ParseError)?; + Ok(BigInt::from(value)) } } @@ -267,97 +162,38 @@ impl<'ctx> SmtEval<'ctx> for Real<'ctx> { type Value = BigRational; fn eval(&self, model: &InstrumentedModel<'ctx>) -> Result { - match model.model { - ModelSource::Z3Model(_) => { - let res = model - .eval(self, false) // TODO - .ok_or(SmtEvalError::EvalError)?; - - // The .as_real() method only returns a pair of i64 values. If the - // results don't fit in these types, we start some funky string parsing. - if let Some((num, den)) = res.as_real() { - Ok(BigRational::new(num.into(), den.into())) - } else { - // we parse a string of the form "(/ num.0 denom.0)" - let division_expr = format!("{:?}", res); - if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") { - return Err(SmtEvalError::ParseError); - } - - let mut parts = division_expr.split_ascii_whitespace(); + let res = model + .eval(self, false) // TODO + .ok_or(SmtEvalError::EvalError)?; + + // The .as_real() method only returns a pair of i64 values. If the + // results don't fit in these types, we start some funky string parsing. + if let Some((num, den)) = res.as_real() { + Ok(BigRational::new(num.into(), den.into())) + } else { + // we parse a string of the form "(/ num.0 denom.0)" + let division_expr = format!("{:?}", res); + if !division_expr.starts_with("(/ ") || !division_expr.ends_with(".0)") { + return Err(SmtEvalError::ParseError); + } - let first_part = parts.next().ok_or(SmtEvalError::ParseError)?; - if first_part != "(/" { - return Err(SmtEvalError::ParseError); - } + let mut parts = division_expr.split_ascii_whitespace(); - let second_part = parts.next().ok_or(SmtEvalError::ParseError)?; - let second_part = second_part.replace(".0", ""); - let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?; + let first_part = parts.next().ok_or(SmtEvalError::ParseError)?; + if first_part != "(/" { + return Err(SmtEvalError::ParseError); + } - let third_part = parts.next().ok_or(SmtEvalError::ParseError)?; - let third_part = third_part.replace(".0)", ""); - let denominator = - BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?; + let second_part = parts.next().ok_or(SmtEvalError::ParseError)?; + let second_part = second_part.replace(".0", ""); + let numerator = BigInt::from_str(&second_part).map_err(|_| SmtEvalError::ParseError)?; - Ok(BigRational::new(numerator, denominator)) - } - }, - ModelSource::SwineModel(s_model) => { - let name = self.decl().name(); + let third_part = parts.next().ok_or(SmtEvalError::ParseError)?; + let third_part = third_part.replace(".0)", ""); + let denominator = + BigInt::from_str(&third_part).map_err(|_| SmtEvalError::ParseError)?; - match find_fun_def(&s_model, &name) { - Some(fun_def) => match fun_def.3 { - Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { - let f = (*d_str).parse::().map_err(|_| SmtEvalError::EvalError)?; - let res = BigRational::from_float(f).ok_or(SmtEvalError::EvalError)?; - Ok(res) - } - Term::Application(QualIdentifier::Identifier(Identifier::Simple(Symbol("/"))), [t1, t2]) => { - let mut num = BigInt::from(1); - let mut den = BigInt::from(1); - match t1 { - Term::SpecConstant(SpecConstant::Numeral(numeral)) => { - let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?; - num *= BigInt::from(n); - }, - Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { - if let Some((n, d)) = from_str_to_num_den(d_str) { - num *= n; - den *= d; - } else { - return Err(SmtEvalError::EvalError); - } - }, - _ => { - return Err(SmtEvalError::EvalError); - }, - } - match t2 { - Term::SpecConstant(SpecConstant::Numeral(numeral)) => { - let n = numeral.into_u128().map_err(|_| SmtEvalError::EvalError)?; - den *= BigInt::from(n); - }, - Term::SpecConstant(SpecConstant::Decimal(Decimal(d_str))) => { - if let Some((n, d)) = from_str_to_num_den(d_str) { - den *= n; - num *= d; - } else { - return Err(SmtEvalError::EvalError); - } - }, - _ => { - return Err(SmtEvalError::EvalError); - }, - } - Ok(BigRational::new(num, den)) - } - _ => Err(SmtEvalError::EvalError), - }, - None => Err(SmtEvalError::EvalError), - } - }, + Ok(BigRational::new(numerator, denominator)) } - } } diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 24bea69b..c5094fa6 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -1,13 +1,14 @@ //! Not a SAT solver, but a prover. There's a difference. +use itertools::Itertools; use thiserror::Error; use std::{ collections::VecDeque, env, fmt::Display, - io::{self, BufRead, BufReader, Read, Write}, + io::{self, Write}, path::Path, - process::{Command, Stdio}, + process::Command, time::Duration, }; @@ -19,15 +20,11 @@ use z3::{ }; use crate::{ - model::{InstrumentedModel, ModelSource}, + model::InstrumentedModel, smtlib::Smtlib, util::{set_solver_timeout, ReasonUnknown}, }; -use smtlib_lowlevel::{ - ast::{CheckSatResponse, GetModelResponse}, - Storage, -}; #[derive(Debug, Error)] pub enum ProverCommandError { @@ -54,19 +51,26 @@ pub enum ProveResult<'ctx> { } /// Execute swine on the file located at file_path -fn execute_swine(file_path: &Path) -> Result { +fn execute_swine(file_path: &Path) -> Result<(SatResult, String), ProverCommandError> { let output = Command::new("swine").arg(file_path).output(); match output { Ok(output) => { let stdout = String::from_utf8_lossy(&output.stdout); - - if stdout.contains("unsat") { - Ok(SatResult::Unsat) - } else if stdout.contains("sat") { - Ok(SatResult::Sat) + let mut lines_buffer: VecDeque<&str>= stdout.lines().collect(); + let first_line = lines_buffer.pop_front().ok_or(ProverCommandError::ParseError)?; + if first_line.contains("unsat") { + Ok((SatResult::Unsat, "".to_string())) + } else if first_line.contains("sat") { + let _last_line = lines_buffer.pop_back().ok_or(ProverCommandError::ParseError)?; + if _last_line.contains("SHA") { + let cex = lines_buffer.iter().join(""); + Ok((SatResult::Sat, cex)) + } else { + Err(ProverCommandError::ParseError) + } } else { - Ok(SatResult::Unknown) + Ok((SatResult::Unknown, "".to_string())) } } Err(e) => Err(ProverCommandError::ProcessError(e)), @@ -193,58 +197,21 @@ impl<'ctx> Prover<'ctx> { .unwrap(); let file_path = smt_file.path(); - let child = Command::new("swine") - .arg(file_path) - .stdout(Stdio::piped()) - .stderr(Stdio::piped()) - .spawn(); - match child { - Ok(mut child) => { - if let Some(stdout) = child.stdout.take() { - let storage = Storage::new(); - let mut buffer = BufReader::new(stdout); - let mut line = String::new(); - buffer.read_line(&mut line)?; - - let sat_res = match CheckSatResponse::parse(&storage, &line) { - Ok(res) => res, - Err(e) => { - eprintln!("ParseError: {}", e); - panic!(); - } - }; - - let mut cex = String::new(); - buffer.read_to_string(&mut cex)?; - - if sat_res == CheckSatResponse::Sat { - match GetModelResponse::parse(&storage, &cex) { - Ok(model_res) => { - let model = InstrumentedModel::new( - ModelSource::SwineModel(model_res), - ); - println!("{:?}", model_res); - } - Err(e) => eprintln!("ParseError: {}", e), - } - } - } - } - Err(e) => eprintln!("Failed to spawn: {}", e), - } - let res = execute_swine(file_path); match res { - Ok(SatResult::Unsat) => Ok(ProveResult::Proof), - Ok(SatResult::Unknown) => { + Ok((SatResult::Unsat, _)) => Ok(ProveResult::Proof), + Ok((SatResult::Unknown, _)) => { // TODO: Determine the correct reason for Unknown Ok(ProveResult::Unknown(ReasonUnknown::Other( "unknown".to_string(), ))) } - Ok(SatResult::Sat) => { - // TODO: Get the model from the output of SWINE - panic!("no counterexample for swine") + Ok((SatResult::Sat, cex)) => { + self.solver.from_string(cex); + + let model = self.get_model().unwrap(); + let model = InstrumentedModel::new(model); + Ok(ProveResult::Counterexample(model)) } Err(err) => Err(err), } @@ -262,7 +229,7 @@ impl<'ctx> Prover<'ctx> { } SatResult::Sat => { let model = self.get_model().unwrap(); - let model = InstrumentedModel::new(ModelSource::Z3Model(model)); + let model = InstrumentedModel::new(model); Ok(ProveResult::Counterexample(model)) } } From 9f44e21dfda78e89fa3c5e5bc416a5d7f7871fb4 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Tue, 13 May 2025 21:24:26 +0200 Subject: [PATCH 12/41] Compare SAT result from swine with 'sat'/'unsat'; return full swine output as reason if unknown --- z3rro/src/prover.rs | 14 ++++++-------- 1 file changed, 6 insertions(+), 8 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index c5094fa6..193898bd 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -59,9 +59,9 @@ fn execute_swine(file_path: &Path) -> Result<(SatResult, String), ProverCommandE let stdout = String::from_utf8_lossy(&output.stdout); let mut lines_buffer: VecDeque<&str>= stdout.lines().collect(); let first_line = lines_buffer.pop_front().ok_or(ProverCommandError::ParseError)?; - if first_line.contains("unsat") { + if first_line.trim().to_lowercase() == "unsat" { Ok((SatResult::Unsat, "".to_string())) - } else if first_line.contains("sat") { + } else if first_line.trim().to_lowercase() == "sat" { let _last_line = lines_buffer.pop_back().ok_or(ProverCommandError::ParseError)?; if _last_line.contains("SHA") { let cex = lines_buffer.iter().join(""); @@ -70,7 +70,8 @@ fn execute_swine(file_path: &Path) -> Result<(SatResult, String), ProverCommandE Err(ProverCommandError::ParseError) } } else { - Ok((SatResult::Unknown, "".to_string())) + lines_buffer.push_front(first_line); + Ok((SatResult::Unknown, lines_buffer.iter().join("\n"))) } } Err(e) => Err(ProverCommandError::ProcessError(e)), @@ -200,11 +201,8 @@ impl<'ctx> Prover<'ctx> { let res = execute_swine(file_path); match res { Ok((SatResult::Unsat, _)) => Ok(ProveResult::Proof), - Ok((SatResult::Unknown, _)) => { - // TODO: Determine the correct reason for Unknown - Ok(ProveResult::Unknown(ReasonUnknown::Other( - "unknown".to_string(), - ))) + Ok((SatResult::Unknown, reason)) => { + Ok(ProveResult::Unknown(ReasonUnknown::Other(reason))) } Ok((SatResult::Sat, cex)) => { self.solver.from_string(cex); From bc17f1c3e8169562bfedd51eac9b07206d2feb78 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Tue, 13 May 2025 21:44:33 +0200 Subject: [PATCH 13/41] Add Cargo.lock file --- Cargo.lock | 79 ++++++++++++++++++++++++++++++++++++++++++++++++++++-- 1 file changed, 77 insertions(+), 2 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 727c86ee..3ba64673 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -153,6 +153,12 @@ version = "0.21.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9d297deb1925b89f2ccc13d7635fa0714f12c87adce1c75356b39ca9b7178567" +[[package]] +name = "beef" +version = "0.5.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3a8241f3ebb85c056b509d4327ad0358fbbba6ffb340bf388f26350aeda225b1" + [[package]] name = "bindgen" version = "0.69.5" @@ -230,9 +236,9 @@ dependencies = [ [[package]] name = "bumpalo" -version = "3.16.0" +version = "3.17.0" source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c" +checksum = "1628fb46dfa0b37568d12e5edd512553eccf6a22a78e8bde00bb4aed84d5bdbf" [[package]] name = "byteorder" @@ -1248,6 +1254,38 @@ version = "0.4.22" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" +[[package]] +name = "logos" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "c000ca4d908ff18ac99b93a062cb8958d331c3220719c52e77cb19cc6ac5d2c1" +dependencies = [ + "logos-derive", +] + +[[package]] +name = "logos-codegen" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dc487311295e0002e452025d6b580b77bb17286de87b57138f3b5db711cded68" +dependencies = [ + "beef", + "fnv", + "proc-macro2", + "quote", + "regex-syntax 0.6.29", + "syn 2.0.90", +] + +[[package]] +name = "logos-derive" +version = "0.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "dbfc0d229f1f42d790440136d941afd806bc9e949e2bcb8faa813b0f00d1267e" +dependencies = [ + "logos-codegen", +] + [[package]] name = "lsp-server" version = "0.7.8" @@ -1289,6 +1327,29 @@ version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" +[[package]] +name = "miette" +version = "5.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "59bb584eaeeab6bd0226ccf3509a69d7936d148cf3d036ad350abe35e8c6856e" +dependencies = [ + "miette-derive", + "once_cell", + "thiserror 1.0.69", + "unicode-width 0.1.14", +] + +[[package]] +name = "miette-derive" +version = "5.10.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "49e7bc1560b95a3c4a25d03de42fe76ca718ab92d1a22a55b9b4cf67b3ae635c" +dependencies = [ + "proc-macro2", + "quote", + "syn 2.0.90", +] + [[package]] name = "minimal-lexical" version = "0.2.1" @@ -1918,6 +1979,19 @@ version = "1.13.2" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "3c5e1a9a646d36c3599cd173a41282daf47c44583ad367b8e6837255952e5c67" +[[package]] +name = "smtlib-lowlevel" +version = "0.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2e48ee399efb51e84d25d4ac02b7e61141f47781d84d8bfc934b8791b30f6c52" +dependencies = [ + "bumpalo", + "itertools 0.12.1", + "logos", + "miette", + "thiserror 1.0.69", +] + [[package]] name = "stable_deref_trait" version = "1.2.0" @@ -2595,6 +2669,7 @@ dependencies = [ "num", "once_cell", "ref-cast", + "smtlib-lowlevel", "tempfile", "thiserror 1.0.69", "tracing", From 4289373b11985a68ae5e60f7927a683265b99ee8 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 21 May 2025 22:06:40 +0200 Subject: [PATCH 14/41] minor changes --- Cargo.lock | 4 +-- src/driver.rs | 13 +++++++--- src/main.rs | 5 +++- src/opt/fuzz_test.rs | 4 +-- src/slicing/solver.rs | 12 ++++----- src/slicing/transform_test.rs | 2 +- z3rro/src/model.rs | 1 - z3rro/src/prover.rs | 48 +++++++++++++++++++---------------- z3rro/src/test.rs | 4 +-- 9 files changed, 52 insertions(+), 41 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 1bbfefa4..5a95e4eb 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -1244,7 +1244,7 @@ dependencies = [ "proc-macro2", "quote", "regex-syntax 0.6.29", - "syn 2.0.90", + "syn 2.0.101", ] [[package]] @@ -1317,7 +1317,7 @@ checksum = "49e7bc1560b95a3c4a25d03de42fe76ca718ab92d1a22a55b9b4cf67b3ae635c" dependencies = [ "proc-macro2", "quote", - "syn 2.0.90", + "syn 2.0.101", ] [[package]] diff --git a/src/driver.rs b/src/driver.rs index e4436429..779078f0 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -53,7 +53,7 @@ use crate::{ vcgen::Vcgen, }, version::write_detailed_version_info, - DebugOptions, SliceOptions, SliceVerifyMethod, VerifyCommand, VerifyError, SMTSolverType, + DebugOptions, SMTSolverType, SliceOptions, SliceVerifyMethod, VerifyCommand, VerifyError, }; use ariadne::ReportKind; @@ -696,7 +696,13 @@ impl<'ctx> SmtVcUnit<'ctx> { let span = info_span!("SAT check"); let _entered = span.enter(); - let prover = mk_valid_query_prover(limits_ref, ctx, translate, &self.vc, options.smt_solver_options.smt_solver); + let prover = mk_valid_query_prover( + limits_ref, + ctx, + translate, + &self.vc, + options.smt_solver_options.smt_solver, + ); if options.debug_options.probe { let goal = Goal::new(ctx, false, false, false); @@ -827,7 +833,7 @@ fn mk_valid_query_prover<'smt, 'ctx>( ) -> Prover<'ctx> { let solver_type = match smt_solver { SMTSolverType::Swine => SolverType::SWINE, - SMTSolverType::Z3 => SolverType::Z3, + SMTSolverType::Z3 => SolverType::Z3, }; // create the prover and set the params @@ -846,6 +852,7 @@ fn mk_valid_query_prover<'smt, 'ctx>( .add_assumptions_to_prover(&mut prover); // add the provable: is this Boolean true? prover.add_provable(valid_query); + println!("{}", valid_query); prover } diff --git a/src/main.rs b/src/main.rs index dc978f47..5facbfbf 100644 --- a/src/main.rs +++ b/src/main.rs @@ -39,7 +39,10 @@ use tokio::task::JoinError; use tracing::{error, info, warn}; use vc::explain::VcExplanation; -use z3rro::{prover::{ProveResult, ProverCommandError}, util::ReasonUnknown}; +use z3rro::{ + prover::{ProveResult, ProverCommandError}, + util::ReasonUnknown, +}; pub mod ast; mod driver; diff --git a/src/opt/fuzz_test.rs b/src/opt/fuzz_test.rs index 39d7d5cb..fb0b0fb8 100644 --- a/src/opt/fuzz_test.rs +++ b/src/opt/fuzz_test.rs @@ -218,10 +218,8 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult { } Ok(ProveResult::Unknown(reason)) => { Err(TestCaseError::fail(format!("unknown result ({})", reason))) - }, - Err(err) => { - Err(TestCaseError::fail(format!("{}", err))) } + Err(err) => Err(TestCaseError::fail(format!("{}", err))), }; x } diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index faebbc04..f7e4b20d 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -248,9 +248,7 @@ impl<'ctx> SliceSolver<'ctx> { self.prover.add_assumption(&self.slice_stmts.constraints); self.prover.add_assumption(&inactive_formula); - let res = self - .prover - .check_proof_assuming(&active_toggle_values); + let res = self.prover.check_proof_assuming(&active_toggle_values); let mut slice_searcher = SliceModelSearch::new(active_toggle_values.clone()); if let Ok(ProveResult::Proof) = res { @@ -353,7 +351,10 @@ impl<'ctx> SliceSolver<'ctx> { self.prover.push(); slice_sat_binary_search(&mut self.prover, &active_toggle_values, options, limits_ref)?; - let res = self.prover.check_proof().map_err(|err| VerifyError::ProverError(err))?; + let res = self + .prover + .check_proof() + .map_err(|err| VerifyError::ProverError(err))?; let model = if let Some(model) = self.prover.get_model() { assert!(matches!( res, @@ -609,7 +610,7 @@ pub fn slice_unsat_search<'ctx>( let res_seed = match check_proof_seed(&all_variables, prover, limits_ref, &seed) { Ok(ProveResult::Proof) => Some(unsat_core_to_seed(prover, &all_variables)), Ok(ProveResult::Counterexample) | Ok(ProveResult::Unknown(_)) => None, - Err(err) => return Err(VerifyError::ProverError(err)) + Err(err) => return Err(VerifyError::ProverError(err)), }; let res = exploration.shrink_block_unsat(seed, |_| res_seed.clone()); @@ -622,7 +623,6 @@ pub fn slice_unsat_search<'ctx>( SliceMinimality::Subset => exploration.block_non_subset(&res), SliceMinimality::Size => exploration.block_at_least(res.len()), } - } Ok(ProveResult::Counterexample) => { // grow the counterexample and then block down diff --git a/src/slicing/transform_test.rs b/src/slicing/transform_test.rs index 3033bec7..5d4a234b 100644 --- a/src/slicing/transform_test.rs +++ b/src/slicing/transform_test.rs @@ -144,7 +144,7 @@ fn prove_equiv( )) } Ok(ProveResult::Unknown(reason)) => Err(format!("unknown result ({})", reason)), - Err(err) => Err(format!("{}", err)) + Err(err) => Err(format!("{}", err)), }; x } diff --git a/z3rro/src/model.rs b/z3rro/src/model.rs index ac27a211..a6a2bb51 100644 --- a/z3rro/src/model.rs +++ b/z3rro/src/model.rs @@ -8,7 +8,6 @@ use std::{ use num::{BigInt, BigRational}; - use thiserror::Error; use z3::{ diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index c5e1f2ff..adf09480 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -4,7 +4,6 @@ use thiserror::Error; use std::{ collections::VecDeque, - env, fmt::Display, io::{self, Write}, path::Path, @@ -25,15 +24,14 @@ use crate::{ util::{set_solver_timeout, ReasonUnknown}, }; - #[derive(Debug, Error)] pub enum ProverCommandError { - #[error("Environment variable error: {0}")] - EnvVarError(#[from] env::VarError), #[error("Process execution failed: {0}")] ProcessError(#[from] io::Error), #[error("Parse error")] ParseError, + #[error("Unexpected result from prover: {0}")] + UnexpectedResultError(String), } #[derive(Debug)] @@ -57,21 +55,25 @@ fn execute_swine(file_path: &Path) -> Result<(SatResult, String), ProverCommandE match output { Ok(output) => { let stdout = String::from_utf8_lossy(&output.stdout); - let mut lines_buffer: VecDeque<&str>= stdout.lines().collect(); - let first_line = lines_buffer.pop_front().ok_or(ProverCommandError::ParseError)?; + let mut lines_buffer: VecDeque<&str> = stdout.lines().collect(); + let first_line = lines_buffer + .pop_front() + .ok_or(ProverCommandError::ParseError)?; if first_line.trim().to_lowercase() == "unsat" { Ok((SatResult::Unsat, "".to_string())) } else if first_line.trim().to_lowercase() == "sat" { - let _last_line = lines_buffer.pop_back().ok_or(ProverCommandError::ParseError)?; - if _last_line.contains("SHA") { - let cex = lines_buffer.iter().join(""); - Ok((SatResult::Sat, cex)) - } else { - Err(ProverCommandError::ParseError) - } + lines_buffer + .pop_back() + .ok_or(ProverCommandError::ParseError)?; + let cex = lines_buffer.iter().join(""); + Ok((SatResult::Sat, cex)) + } else if first_line.trim().to_lowercase() == "unknown" { + Ok((SatResult::Unknown, lines_buffer.iter().join("\n"))) } else { lines_buffer.push_front(first_line); - Ok((SatResult::Unknown, lines_buffer.iter().join("\n"))) + Err(ProverCommandError::UnexpectedResultError( + lines_buffer.iter().join("\n"), + )) } } Err(e) => Err(ProverCommandError::ProcessError(e)), @@ -86,6 +88,8 @@ fn remove_lines_for_swine(input: &str) -> String { let mut input_buffer: VecDeque = input.chars().collect(); let mut cnt = 0; + // Collect characters until all opened parentheses are closed, and + // keep this block if it does not contain 'declare-fun exp' or 'forall'. while let Some(c) = input_buffer.pop_front() { tmp_buffer.push_back(c); match c { @@ -108,7 +112,6 @@ fn remove_lines_for_swine(input: &str) -> String { output } - impl Display for ProveResult { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { @@ -243,10 +246,9 @@ impl<'ctx> Prover<'ctx> { self.add_assumption(&value.not()); self.min_level_with_provables.get_or_insert(self.level); } - + /// `self.check_proof_assuming(&[])`. pub fn check_proof(&mut self) -> Result { - self.check_proof_assuming(&[]) } @@ -281,12 +283,12 @@ impl<'ctx> Prover<'ctx> { match &self.solver { StackSolver::Native(solver) => { solver.from_string(cex); - }, + } StackSolver::Emulated(solver, _) => { solver.from_string(cex); - }, + } } - + Ok(ProveResult::Counterexample) } Err(err) => Err(err), @@ -306,13 +308,15 @@ impl<'ctx> Prover<'ctx> { res } }; + match res { SatResult::Unsat => Ok(ProveResult::Proof), - SatResult::Unknown => Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())), + SatResult::Unknown => { + Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())) + } SatResult::Sat => Ok(ProveResult::Counterexample), } } - } } diff --git a/z3rro/src/test.rs b/z3rro/src/test.rs index cec778b3..3b281ed6 100644 --- a/z3rro/src/test.rs +++ b/z3rro/src/test.rs @@ -34,8 +34,8 @@ pub fn test_prove(f: impl for<'ctx> FnOnce(&'ctx Context, &mut SmtScope<'ctx>) - prover.get_assertions() ), Ok(ProveResult::Unknown(reason)) => panic!("solver returned unknown ({})", reason), - Ok(ProveResult::Proof) => {}, - Err(_) => {} + Ok(ProveResult::Proof) => {} + Err(e) => panic!("{}", e), }; } From f07c8b79c0b1d2967801a88a9020603899c285dd Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 23 May 2025 22:46:42 +0200 Subject: [PATCH 15/41] Remove leftover code --- src/driver.rs | 1 - 1 file changed, 1 deletion(-) diff --git a/src/driver.rs b/src/driver.rs index 779078f0..ec0b3842 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -852,7 +852,6 @@ fn mk_valid_query_prover<'smt, 'ctx>( .add_assumptions_to_prover(&mut prover); // add the provable: is this Boolean true? prover.add_provable(valid_query); - println!("{}", valid_query); prover } From 4af68850308504f462a26861db1e3672184f4856 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 23 May 2025 22:49:49 +0200 Subject: [PATCH 16/41] Add check-sat-assuming command for given assumptions --- z3rro/src/prover.rs | 12 +++++++++--- z3rro/src/smtlib.rs | 9 +++++++++ 2 files changed, 18 insertions(+), 3 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index adf09480..731c76ab 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -265,7 +265,13 @@ impl<'ctx> Prover<'ctx> { match self.smt_solver { SolverType::SWINE => { let mut smtlib = self.get_smtlib(); - smtlib.add_check_sat(); + if assumptions.is_empty() { + smtlib.add_check_sat(); + } else { + smtlib.add_check_sat_assuming( + assumptions.iter().map(|a| a.to_string()).collect(), + ); + }; let smtlib = smtlib.into_string(); let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); smt_file @@ -288,8 +294,8 @@ impl<'ctx> Prover<'ctx> { solver.from_string(cex); } } - - Ok(ProveResult::Counterexample) + panic!(""); + //Ok(ProveResult::Counterexample) } Err(err) => Err(err), } diff --git a/z3rro/src/smtlib.rs b/z3rro/src/smtlib.rs index 9c767000..fad1c3ed 100644 --- a/z3rro/src/smtlib.rs +++ b/z3rro/src/smtlib.rs @@ -30,6 +30,15 @@ impl Smtlib { self.0.push_str("\n(check-sat)"); } + pub fn add_check_sat_assuming(&mut self, assumptions: Vec) { + let assumptions_str: Vec = assumptions.iter().map(|a| a.to_string()).collect(); + + self.0.push_str(&format!( + "\n(check-sat-assuming ({}))", + assumptions_str.join(" ").as_str() + )); + } + /// Add a `(check-sat)` command at the end. pub fn add_details_query(&mut self, prove_result: &ProveResult) { match prove_result { From ecfad759c0b3c8e9cdca29a93921473f421d75fc Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 23 May 2025 23:05:26 +0200 Subject: [PATCH 17/41] Add docs for add_check_sat_assuming and add_details_query --- z3rro/src/smtlib.rs | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/z3rro/src/smtlib.rs b/z3rro/src/smtlib.rs index fad1c3ed..9127b42e 100644 --- a/z3rro/src/smtlib.rs +++ b/z3rro/src/smtlib.rs @@ -30,6 +30,7 @@ impl Smtlib { self.0.push_str("\n(check-sat)"); } + /// Add a `(check-sat-assuming)` command at the end pub fn add_check_sat_assuming(&mut self, assumptions: Vec) { let assumptions_str: Vec = assumptions.iter().map(|a| a.to_string()).collect(); @@ -39,7 +40,7 @@ impl Smtlib { )); } - /// Add a `(check-sat)` command at the end. + /// Add a `(get-model)` command at the end for counterexamples and a `(get-info :reason-unknown)` for unknown results. pub fn add_details_query(&mut self, prove_result: &ProveResult) { match prove_result { ProveResult::Proof => {} From c5464debbad3abe00c8dc6e17ecd3fa933a04a23 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Tue, 27 May 2025 21:42:01 +0200 Subject: [PATCH 18/41] Add SolverResult enum --- z3rro/src/prover.rs | 142 +++++++++++++++++++++++++++----------------- 1 file changed, 87 insertions(+), 55 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 731c76ab..8e749562 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -6,7 +6,6 @@ use std::{ collections::VecDeque, fmt::Display, io::{self, Write}, - path::Path, process::Command, time::Duration, }; @@ -48,8 +47,41 @@ pub enum ProveResult { Unknown(ReasonUnknown), } +/// The result from solver. +#[derive(Debug, Clone)] +pub enum SolverResult { + Unsat, + Sat(Option), + Unknown(Option), +} + +impl SolverResult { + fn to_sat_result(&self) -> SatResult { + match self { + SolverResult::Unsat => SatResult::Unsat, + SolverResult::Sat(_) => SatResult::Sat, + SolverResult::Unknown(_) => SatResult::Unknown, + } + } +} + /// Execute swine on the file located at file_path -fn execute_swine(file_path: &Path) -> Result<(SatResult, String), ProverCommandError> { +fn execute_swine( + prover: &mut Prover<'_>, + assumptions: &[Bool<'_>], +) -> Result { + let mut smtlib = prover.get_smtlib(); + if assumptions.is_empty() { + smtlib.add_check_sat(); + } else { + smtlib.add_check_sat_assuming(assumptions.iter().map(|a| a.to_string()).collect()); + }; + let smtlib = smtlib.into_string(); + let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); + smt_file + .write_all(remove_lines_for_swine(&smtlib).as_bytes()) + .unwrap(); + let file_path = smt_file.path(); let output = Command::new("swine").arg(file_path).output(); match output { @@ -60,15 +92,17 @@ fn execute_swine(file_path: &Path) -> Result<(SatResult, String), ProverCommandE .pop_front() .ok_or(ProverCommandError::ParseError)?; if first_line.trim().to_lowercase() == "unsat" { - Ok((SatResult::Unsat, "".to_string())) + Ok(SolverResult::Unsat) } else if first_line.trim().to_lowercase() == "sat" { lines_buffer .pop_back() .ok_or(ProverCommandError::ParseError)?; let cex = lines_buffer.iter().join(""); - Ok((SatResult::Sat, cex)) + Ok(SolverResult::Sat(Some(cex))) } else if first_line.trim().to_lowercase() == "unknown" { - Ok((SatResult::Unknown, lines_buffer.iter().join("\n"))) + Ok(SolverResult::Unknown(Some(ReasonUnknown::Other( + lines_buffer.iter().join("\n"), + )))) } else { lines_buffer.push_front(first_line); Err(ProverCommandError::UnexpectedResultError( @@ -141,7 +175,7 @@ enum StackSolver<'ctx> { } #[derive(Debug)] -struct LastSatResult { +struct LastSatSolverResult { /// Whether the current model is consistent with the assertions. If the SMT /// solver returned [`SatResult::Unknown`], it is /// [`ModelConsistency::Unknown`]. @@ -150,7 +184,7 @@ struct LastSatResult { /// It is reset any time the assertions on the solver are modified. /// Sometimes Z3 caches on its own, but it is not reliable. Therefore, we do /// it here as well to be sure. - last_result: SatResult, + last_result: SolverResult, } /// A prover wraps a SAT solver, but it's used to prove validity of formulas. @@ -177,7 +211,7 @@ pub struct Prover<'ctx> { /// SMT solver type smt_solver: SolverType, /// Cached information about the last SAT/proof check call. - last_result: Option, + last_result: Option, } impl<'ctx> Prover<'ctx> { @@ -264,45 +298,29 @@ impl<'ctx> Prover<'ctx> { match self.smt_solver { SolverType::SWINE => { - let mut smtlib = self.get_smtlib(); - if assumptions.is_empty() { - smtlib.add_check_sat(); - } else { - smtlib.add_check_sat_assuming( - assumptions.iter().map(|a| a.to_string()).collect(), - ); - }; - let smtlib = smtlib.into_string(); - let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); - smt_file - .write_all(remove_lines_for_swine(&smtlib).as_bytes()) - .unwrap(); - let file_path = smt_file.path(); - - let res = execute_swine(file_path); + let res = execute_swine(self, assumptions)?; + match res { - Ok((SatResult::Unsat, _)) => Ok(ProveResult::Proof), - Ok((SatResult::Unknown, reason)) => { - Ok(ProveResult::Unknown(ReasonUnknown::Other(reason))) + SolverResult::Unsat => Ok(ProveResult::Proof), + SolverResult::Unknown(r) => { + let reason = r.unwrap_or(ReasonUnknown::Other("".to_string())); + Ok(ProveResult::Unknown(reason)) } - Ok((SatResult::Sat, cex)) => { - match &self.solver { - StackSolver::Native(solver) => { - solver.from_string(cex); - } - StackSolver::Emulated(solver, _) => { - solver.from_string(cex); - } + SolverResult::Sat(c) => { + if let Some(cex) = c { + let solver = self.get_solver(); + solver.from_string(cex); } - panic!(""); - //Ok(ProveResult::Counterexample) + Ok(ProveResult::Counterexample) } - Err(err) => Err(err), } } + SolverType::Z3 => { let res = match &self.last_result { - Some(cached_result) if assumptions.is_empty() => cached_result.last_result, + Some(cached_result) if assumptions.is_empty() => { + cached_result.last_result.clone() + } _ => { let solver = self.get_solver(); let res = if assumptions.is_empty() { @@ -310,17 +328,23 @@ impl<'ctx> Prover<'ctx> { } else { solver.check_assumptions(assumptions) }; - self.cache_result(res); - res + + let solver_result = match res { + SatResult::Unsat => SolverResult::Unsat, + SatResult::Unknown => SolverResult::Unknown(None), + SatResult::Sat => SolverResult::Sat(None), + }; + self.cache_result(solver_result.clone()); + solver_result } }; match res { - SatResult::Unsat => Ok(ProveResult::Proof), - SatResult::Unknown => { + SolverResult::Unsat => Ok(ProveResult::Proof), + SolverResult::Unknown(_) => { Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())) } - SatResult::Sat => Ok(ProveResult::Counterexample), + SolverResult::Sat(_) => Ok(ProveResult::Counterexample), } } } @@ -337,23 +361,31 @@ impl<'ctx> Prover<'ctx> { /// Do the regular SAT check. pub fn check_sat(&mut self) -> SatResult { if let Some(cached_result) = &self.last_result { - return cached_result.last_result; + return cached_result.last_result.to_sat_result(); } - let res = self.get_solver().check(); - self.cache_result(res); - res + + let sat_result = self.get_solver().check(); + + let solver_result = match sat_result { + SatResult::Unsat => SolverResult::Unsat, + SatResult::Unknown => SolverResult::Unknown(None), + SatResult::Sat => SolverResult::Sat(None), + }; + self.cache_result(solver_result); + + sat_result } /// Save the result of the last SAT/proof check. - fn cache_result(&mut self, sat_result: SatResult) { - let model_consistency = match sat_result { - SatResult::Sat => Some(ModelConsistency::Consistent), - SatResult::Unknown => Some(ModelConsistency::Unknown), - SatResult::Unsat => None, + fn cache_result(&mut self, solver_result: SolverResult) { + let model_consistency = match solver_result { + SolverResult::Sat(_) => Some(ModelConsistency::Consistent), + SolverResult::Unknown(_) => Some(ModelConsistency::Unknown), + SolverResult::Unsat => None, }; - self.last_result = Some(LastSatResult { + self.last_result = Some(LastSatSolverResult { model_consistency, - last_result: sat_result, + last_result: solver_result, }); } From aaf9c52832452ef810f0ab87aa9acd590e1b66b6 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 4 Jun 2025 22:55:01 +0200 Subject: [PATCH 19/41] Apply the same logic to the SWINE call --- z3rro/src/prover.rs | 35 +++++++++++++++++++++++++---------- 1 file changed, 25 insertions(+), 10 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 8e749562..92958185 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -47,7 +47,14 @@ pub enum ProveResult { Unknown(ReasonUnknown), } -/// The result from solver. +/// If z3 is used as the SMT solver, it is not necessary to store +/// a counterexample (for Sat) or reason (for Unknown), since the +/// Z3 solver already retains this information internallz. +/// In this case, it is only used to store the SAT result. +/// +/// For SwInE, this can be used either to +/// 1) transport the result from SwInE, or +/// 2) store SAT result alonq with a reason for Unknown. #[derive(Debug, Clone)] pub enum SolverResult { Unsat, @@ -298,7 +305,22 @@ impl<'ctx> Prover<'ctx> { match self.smt_solver { SolverType::SWINE => { - let res = execute_swine(self, assumptions)?; + let res = match &self.last_result { + Some(cached_result) if assumptions.is_empty() => { + cached_result.last_result.clone() + } + _ => { + let solver_result = execute_swine(self, assumptions)?; + + if let SolverResult::Sat(Some(cex)) = solver_result.clone() { + let solver = self.get_solver(); + solver.from_string(cex); + }; + + self.cache_result(solver_result.clone()); + solver_result + } + }; match res { SolverResult::Unsat => Ok(ProveResult::Proof), @@ -306,16 +328,9 @@ impl<'ctx> Prover<'ctx> { let reason = r.unwrap_or(ReasonUnknown::Other("".to_string())); Ok(ProveResult::Unknown(reason)) } - SolverResult::Sat(c) => { - if let Some(cex) = c { - let solver = self.get_solver(); - solver.from_string(cex); - } - Ok(ProveResult::Counterexample) - } + SolverResult::Sat(_) => Ok(ProveResult::Counterexample), } } - SolverType::Z3 => { let res = match &self.last_result { Some(cached_result) if assumptions.is_empty() => { From b5325b8c9aab10ad906d464a63ea5adbb0f275c1 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Thu, 5 Jun 2025 21:11:49 +0200 Subject: [PATCH 20/41] Implement check_sat for each SolverType (not working correctly) --- src/opt/unfolder.rs | 2 +- src/slicing/solver.rs | 17 +++++++++--- z3rro/src/prover.rs | 61 +++++++++++++++++++++++++++---------------- z3rro/src/test.rs | 2 +- 4 files changed, 54 insertions(+), 28 deletions(-) diff --git a/src/opt/unfolder.rs b/src/opt/unfolder.rs index 5aadf990..c2bd97b6 100644 --- a/src/opt/unfolder.rs +++ b/src/opt/unfolder.rs @@ -98,7 +98,7 @@ impl<'smt, 'ctx> Unfolder<'smt, 'ctx> { // here we want to do a SAT check and not a proof search. if the // expression is e.g. `false`, then we want to get `Unsat` from the // solver and not `Proof`! - if this.prover.check_sat() == SatResult::Unsat { + if this.prover.check_sat() == Ok(SatResult::Unsat) { tracing::trace!(solver=?this.prover, "eliminated zero expr"); None } else { diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index f7e4b20d..d27ff09f 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -218,7 +218,11 @@ impl<'ctx> SliceSolver<'ctx> { options, limits_ref, )?; - if exists_forall_solver.check_sat() == SatResult::Sat { + println!("slice_verifying_exists_forall"); + let sat_res = exists_forall_solver + .check_sat() + .map_err(|err| VerifyError::ProverError(err))?; + if sat_res == SatResult::Sat { let model = exists_forall_solver.get_model().unwrap(); let slice_model = SliceModel::from_model(SliceMode::Verify, &self.slice_stmts, selection, &model); @@ -509,7 +513,11 @@ fn slice_sat_binary_search<'ctx>( if let Some(timeout) = limits_ref.time_left() { prover.set_timeout(timeout); } - let res = prover.check_sat(); + println!("slice_sat_binary_search 1"); + + let res = prover + .check_sat() + .map_err(|err| VerifyError::ProverError(err))?; entered.record("res", tracing::field::debug(res)); @@ -574,7 +582,10 @@ fn slice_sat_binary_search<'ctx>( if let Some(timeout) = limits_ref.time_left() { prover.set_timeout(timeout); } - let res = prover.check_sat(); + println!("slice_sat_binary_search 2"); + let res = prover + .check_sat() + .map_err(|err| VerifyError::ProverError(err))?; if minimize.min_accept().is_some() { assert!(res == SatResult::Sat || res == SatResult::Unknown); } else if minimize.max_reject().is_some() { diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 92958185..0df1dc0c 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -2,13 +2,7 @@ use itertools::Itertools; use thiserror::Error; -use std::{ - collections::VecDeque, - fmt::Display, - io::{self, Write}, - process::Command, - time::Duration, -}; +use std::{collections::VecDeque, fmt::Display, io::Write, process::Command, time::Duration}; use tempfile::NamedTempFile; @@ -23,10 +17,10 @@ use crate::{ util::{set_solver_timeout, ReasonUnknown}, }; -#[derive(Debug, Error)] +#[derive(Debug, Error, PartialEq)] pub enum ProverCommandError { #[error("Process execution failed: {0}")] - ProcessError(#[from] io::Error), + ProcessError(String), #[error("Parse error")] ParseError, #[error("Unexpected result from prover: {0}")] @@ -54,7 +48,7 @@ pub enum ProveResult { /// /// For SwInE, this can be used either to /// 1) transport the result from SwInE, or -/// 2) store SAT result alonq with a reason for Unknown. +/// 2) store SAT result along with a reason for Unknown. #[derive(Debug, Clone)] pub enum SolverResult { Unsat, @@ -94,6 +88,7 @@ fn execute_swine( match output { Ok(output) => { let stdout = String::from_utf8_lossy(&output.stdout); + println!("{:}", stdout); let mut lines_buffer: VecDeque<&str> = stdout.lines().collect(); let first_line = lines_buffer .pop_front() @@ -117,7 +112,7 @@ fn execute_swine( )) } } - Err(e) => Err(ProverCommandError::ProcessError(e)), + Err(e) => Err(ProverCommandError::ProcessError(e.to_string())), } } @@ -310,6 +305,7 @@ impl<'ctx> Prover<'ctx> { cached_result.last_result.clone() } _ => { + println!("check_proof_assuming"); let solver_result = execute_swine(self, assumptions)?; if let SolverResult::Sat(Some(cex)) = solver_result.clone() { @@ -374,21 +370,40 @@ impl<'ctx> Prover<'ctx> { } /// Do the regular SAT check. - pub fn check_sat(&mut self) -> SatResult { + pub fn check_sat(&mut self) -> Result { if let Some(cached_result) = &self.last_result { - return cached_result.last_result.to_sat_result(); + return Ok(cached_result.last_result.to_sat_result()); } - let sat_result = self.get_solver().check(); + let sat_result = match self.smt_solver { + SolverType::Z3 => { + let sat_result = self.get_solver().check(); + + let solver_result = match sat_result { + SatResult::Unsat => SolverResult::Unsat, + SatResult::Unknown => SolverResult::Unknown(None), + SatResult::Sat => SolverResult::Sat(None), + }; + self.cache_result(solver_result); - let solver_result = match sat_result { - SatResult::Unsat => SolverResult::Unsat, - SatResult::Unknown => SolverResult::Unknown(None), - SatResult::Sat => SolverResult::Sat(None), + sat_result + } + SolverType::SWINE => { + println!("check_sat"); + let solver_result = execute_swine(self, &[])?; + + if let SolverResult::Sat(Some(cex)) = solver_result.clone() { + let solver = self.get_solver(); + solver.from_string(cex); + }; + + self.cache_result(solver_result.clone()); + + solver_result.to_sat_result() + } }; - self.cache_result(solver_result); - sat_result + Ok(sat_result) } /// Save the result of the last SAT/proof check. @@ -534,16 +549,16 @@ mod test { let ctx = Context::new(&Config::default()); let mut prover = Prover::new(&ctx, mode, SolverType::Z3); assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof))); - assert_eq!(prover.check_sat(), SatResult::Sat); + assert_eq!(prover.check_sat(), Ok(SatResult::Sat)); prover.push(); prover.add_assumption(&Bool::from_bool(&ctx, true)); assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof))); - assert_eq!(prover.check_sat(), SatResult::Sat); + assert_eq!(prover.check_sat(), Ok(SatResult::Sat)); prover.pop(); assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof))); - assert_eq!(prover.check_sat(), SatResult::Sat); + assert_eq!(prover.check_sat(), Ok(SatResult::Sat)); } } } diff --git a/z3rro/src/test.rs b/z3rro/src/test.rs index 3b281ed6..f20764ea 100644 --- a/z3rro/src/test.rs +++ b/z3rro/src/test.rs @@ -22,7 +22,7 @@ pub fn test_prove(f: impl for<'ctx> FnOnce(&'ctx Context, &mut SmtScope<'ctx>) - scope.add_assumptions_to_prover(&mut prover); assert_eq!( prover.check_sat(), - SatResult::Sat, + Ok(SatResult::Sat), "SmtScope is inconsistent" ); From fe830be98aae520e6671537933322b988663997c Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 20 Jun 2025 21:17:36 +0200 Subject: [PATCH 21/41] Fix missing sat check after adding assertions --- z3rro/src/prover.rs | 2 ++ 1 file changed, 2 insertions(+) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 0df1dc0c..404d3821 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -311,6 +311,7 @@ impl<'ctx> Prover<'ctx> { if let SolverResult::Sat(Some(cex)) = solver_result.clone() { let solver = self.get_solver(); solver.from_string(cex); + solver.check(); }; self.cache_result(solver_result.clone()); @@ -395,6 +396,7 @@ impl<'ctx> Prover<'ctx> { if let SolverResult::Sat(Some(cex)) = solver_result.clone() { let solver = self.get_solver(); solver.from_string(cex); + solver.check(); }; self.cache_result(solver_result.clone()); From 7709717c2df97f170281d1757e1884e4547e6643 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 20 Jun 2025 22:20:47 +0200 Subject: [PATCH 22/41] Remove print statements used for functon call tracking --- src/slicing/solver.rs | 3 --- z3rro/src/prover.rs | 3 --- 2 files changed, 6 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index d27ff09f..e156776b 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -218,7 +218,6 @@ impl<'ctx> SliceSolver<'ctx> { options, limits_ref, )?; - println!("slice_verifying_exists_forall"); let sat_res = exists_forall_solver .check_sat() .map_err(|err| VerifyError::ProverError(err))?; @@ -513,7 +512,6 @@ fn slice_sat_binary_search<'ctx>( if let Some(timeout) = limits_ref.time_left() { prover.set_timeout(timeout); } - println!("slice_sat_binary_search 1"); let res = prover .check_sat() @@ -582,7 +580,6 @@ fn slice_sat_binary_search<'ctx>( if let Some(timeout) = limits_ref.time_left() { prover.set_timeout(timeout); } - println!("slice_sat_binary_search 2"); let res = prover .check_sat() .map_err(|err| VerifyError::ProverError(err))?; diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 404d3821..112dfa56 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -88,7 +88,6 @@ fn execute_swine( match output { Ok(output) => { let stdout = String::from_utf8_lossy(&output.stdout); - println!("{:}", stdout); let mut lines_buffer: VecDeque<&str> = stdout.lines().collect(); let first_line = lines_buffer .pop_front() @@ -305,7 +304,6 @@ impl<'ctx> Prover<'ctx> { cached_result.last_result.clone() } _ => { - println!("check_proof_assuming"); let solver_result = execute_swine(self, assumptions)?; if let SolverResult::Sat(Some(cex)) = solver_result.clone() { @@ -390,7 +388,6 @@ impl<'ctx> Prover<'ctx> { sat_result } SolverType::SWINE => { - println!("check_sat"); let solver_result = execute_swine(self, &[])?; if let SolverResult::Sat(Some(cex)) = solver_result.clone() { From 6d4259d6360700752999fc2f6d55c1a87e1aa1a0 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 20 Jun 2025 22:46:41 +0200 Subject: [PATCH 23/41] Add SMTLIB(String) option to SMTSolverType and SolverType enums --- src/driver.rs | 3 +- src/main.rs | 17 ++++-- z3rro/src/prover.rs | 126 ++++++++++++++++++++++++++++---------------- 3 files changed, 97 insertions(+), 49 deletions(-) diff --git a/src/driver.rs b/src/driver.rs index ec0b3842..2d13fb65 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -701,7 +701,7 @@ impl<'ctx> SmtVcUnit<'ctx> { ctx, translate, &self.vc, - options.smt_solver_options.smt_solver, + options.smt_solver_options.smt_solver.clone(), ); if options.debug_options.probe { @@ -834,6 +834,7 @@ fn mk_valid_query_prover<'smt, 'ctx>( let solver_type = match smt_solver { SMTSolverType::Swine => SolverType::SWINE, SMTSolverType::Z3 => SolverType::Z3, + SMTSolverType::SMTLIB(solver) => SolverType::SMTLIB(solver), }; // create the prover and set the params diff --git a/src/main.rs b/src/main.rs index 5facbfbf..db8537d1 100644 --- a/src/main.rs +++ b/src/main.rs @@ -393,13 +393,24 @@ pub struct SMTSolverOptions { pub smt_solver: SMTSolverType, } -#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)] +#[derive(Debug, Clone, PartialEq, Eq, Default)] pub enum SMTSolverType { #[default] - #[value(name = "z3")] Z3, - #[value(name = "swine")] Swine, + SMTLIB(String), +} + +impl std::str::FromStr for SMTSolverType { + type Err = String; + + fn from_str(s: &str) -> Result { + match s { + "z3" => Ok(SMTSolverType::Z3), + "swine" => Ok(SMTSolverType::Swine), + solver => Ok(SMTSolverType::SMTLIB(solver.to_string())), + } + } } #[derive(Debug, Default, Args)] diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 112dfa56..55753c78 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -4,7 +4,7 @@ use thiserror::Error; use std::{collections::VecDeque, fmt::Display, io::Write, process::Command, time::Duration}; -use tempfile::NamedTempFile; +use tempfile::{Builder, NamedTempFile}; use z3::{ ast::{forall_const, Ast, Bool, Dynamic}, @@ -27,10 +27,11 @@ pub enum ProverCommandError { UnexpectedResultError(String), } -#[derive(Debug)] +#[derive(Debug, PartialEq)] pub enum SolverType { Z3, SWINE, + SMTLIB(String), } /// The result of a prove query. @@ -41,11 +42,11 @@ pub enum ProveResult { Unknown(ReasonUnknown), } -/// If z3 is used as the SMT solver, it is not necessary to store -/// a counterexample (for Sat) or reason (for Unknown), since the -/// Z3 solver already retains this information internallz. +/// If z3 is used as the SMT solver, it is not necessary to store +/// a counterexample (for Sat) or reason (for Unknown), since the +/// Z3 solver already retains this information internally. /// In this case, it is only used to store the SAT result. -/// +/// /// For SwInE, this can be used either to /// 1) transport the result from SwInE, or /// 2) store SAT result along with a reason for Unknown. @@ -66,8 +67,8 @@ impl SolverResult { } } -/// Execute swine on the file located at file_path -fn execute_swine( +/// Execute an SMT solver (other than z3) +fn execute_solver( prover: &mut Prover<'_>, assumptions: &[Bool<'_>], ) -> Result { @@ -78,12 +79,30 @@ fn execute_swine( smtlib.add_check_sat_assuming(assumptions.iter().map(|a| a.to_string()).collect()); }; let smtlib = smtlib.into_string(); - let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); - smt_file - .write_all(remove_lines_for_swine(&smtlib).as_bytes()) - .unwrap(); - let file_path = smt_file.path(); - let output = Command::new("swine").arg(file_path).output(); + + let output = match &prover.smt_solver { + SolverType::Z3 => { + unreachable!("The function 'execute_solver' should never be called for z3"); + } + SolverType::SWINE => { + let mut smt_file = NamedTempFile::new().unwrap(); + smt_file + .write_all(remove_lines(&smtlib, SolverType::SWINE).as_bytes()) + .unwrap(); + + let file_path = smt_file.path(); + + Command::new("swine").arg(file_path).output() + } + SolverType::SMTLIB(solver) => { + let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); + smt_file + .write_all(remove_lines(&smtlib, SolverType::SMTLIB("".to_string())).as_bytes()) + .unwrap(); + let file_path = smt_file.path(); + Command::new(solver).arg(file_path).output() + } + }; match output { Ok(output) => { @@ -115,14 +134,32 @@ fn execute_swine( } } -/// In order to execute the program, it is necessary to remove lines that -/// contain a forall quantifier or the declaration of the exponential function (exp). -fn remove_lines_for_swine(input: &str) -> String { - let mut output = String::new(); +/// To execute the SMT solver correctly, specific modifications to the input are required: +/// 1) For SwInE, remove lines that contain a `forall` quantifier or the declaration of the exponential function (`exp``). +/// 2) For other solvers, add a line to set logic, and remove incorrect assertions such as `(assert add)`. +fn remove_lines(input: &str, solver: SolverType) -> String { + let mut output = match solver { + SolverType::SMTLIB(_) => { + let mut output = String::new(); + let logic = if input.contains("*") || input.contains("/") { + "(set-logic QF_NIRA)" + } else { + "(set-logic QF_LIRA)" + }; + output.push_str(logic); + output + } + _ => String::new(), + }; let mut tmp_buffer: VecDeque = VecDeque::new(); let mut input_buffer: VecDeque = input.chars().collect(); let mut cnt = 0; + let condition = |tmp: &str| match solver { + SolverType::SWINE => !tmp.contains("declare-fun exp") && !tmp.contains("forall"), + _ => !tmp.contains("(assert and)"), + }; + // Collect characters until all opened parentheses are closed, and // keep this block if it does not contain 'declare-fun exp' or 'forall'. while let Some(c) = input_buffer.pop_front() { @@ -135,7 +172,7 @@ fn remove_lines_for_swine(input: &str) -> String { cnt -= 1; if cnt == 0 { let tmp: String = tmp_buffer.iter().collect(); - if !tmp.contains("declare-fun exp") && !tmp.contains("forall") { + if condition(&tmp) { output.push_str(&tmp); } tmp_buffer.clear(); @@ -298,20 +335,24 @@ impl<'ctx> Prover<'ctx> { } match self.smt_solver { - SolverType::SWINE => { + SolverType::Z3 => { let res = match &self.last_result { Some(cached_result) if assumptions.is_empty() => { cached_result.last_result.clone() } _ => { - let solver_result = execute_swine(self, assumptions)?; - - if let SolverResult::Sat(Some(cex)) = solver_result.clone() { - let solver = self.get_solver(); - solver.from_string(cex); - solver.check(); + let solver = self.get_solver(); + let res = if assumptions.is_empty() { + solver.check() + } else { + solver.check_assumptions(assumptions) }; + let solver_result = match res { + SatResult::Unsat => SolverResult::Unsat, + SatResult::Unknown => SolverResult::Unknown(None), + SatResult::Sat => SolverResult::Sat(None), + }; self.cache_result(solver_result.clone()); solver_result } @@ -319,31 +360,26 @@ impl<'ctx> Prover<'ctx> { match res { SolverResult::Unsat => Ok(ProveResult::Proof), - SolverResult::Unknown(r) => { - let reason = r.unwrap_or(ReasonUnknown::Other("".to_string())); - Ok(ProveResult::Unknown(reason)) + SolverResult::Unknown(_) => { + Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())) } SolverResult::Sat(_) => Ok(ProveResult::Counterexample), } } - SolverType::Z3 => { + _ => { let res = match &self.last_result { Some(cached_result) if assumptions.is_empty() => { cached_result.last_result.clone() } _ => { - let solver = self.get_solver(); - let res = if assumptions.is_empty() { - solver.check() - } else { - solver.check_assumptions(assumptions) - }; + let solver_result = execute_solver(self, assumptions)?; - let solver_result = match res { - SatResult::Unsat => SolverResult::Unsat, - SatResult::Unknown => SolverResult::Unknown(None), - SatResult::Sat => SolverResult::Sat(None), + if let SolverResult::Sat(Some(cex)) = solver_result.clone() { + let solver = self.get_solver(); + solver.from_string(cex); + solver.check(); }; + self.cache_result(solver_result.clone()); solver_result } @@ -351,8 +387,9 @@ impl<'ctx> Prover<'ctx> { match res { SolverResult::Unsat => Ok(ProveResult::Proof), - SolverResult::Unknown(_) => { - Ok(ProveResult::Unknown(self.get_reason_unknown().unwrap())) + SolverResult::Unknown(r) => { + let reason = r.unwrap_or(ReasonUnknown::Other("".to_string())); + Ok(ProveResult::Unknown(reason)) } SolverResult::Sat(_) => Ok(ProveResult::Counterexample), } @@ -387,15 +424,14 @@ impl<'ctx> Prover<'ctx> { sat_result } - SolverType::SWINE => { - let solver_result = execute_swine(self, &[])?; + _ => { + let solver_result = execute_solver(self, &[])?; if let SolverResult::Sat(Some(cex)) = solver_result.clone() { let solver = self.get_solver(); solver.from_string(cex); solver.check(); }; - self.cache_result(solver_result.clone()); solver_result.to_sat_result() From 10b522e747444f3e5785c82bda7ba951107454d0 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 2 Jul 2025 23:21:47 +0200 Subject: [PATCH 24/41] no functional change --- z3rro/src/prover.rs | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 55753c78..4ed4aa6d 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -92,7 +92,7 @@ fn execute_solver( let file_path = smt_file.path(); - Command::new("swine").arg(file_path).output() + Command::new("swine").arg("--no-version").arg(file_path).output() } SolverType::SMTLIB(solver) => { let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); @@ -114,9 +114,6 @@ fn execute_solver( if first_line.trim().to_lowercase() == "unsat" { Ok(SolverResult::Unsat) } else if first_line.trim().to_lowercase() == "sat" { - lines_buffer - .pop_back() - .ok_or(ProverCommandError::ParseError)?; let cex = lines_buffer.iter().join(""); Ok(SolverResult::Sat(Some(cex))) } else if first_line.trim().to_lowercase() == "unknown" { From 7f4f5b32197e5977004f38f0085aca40b64a594b Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 4 Jul 2025 21:37:55 +0200 Subject: [PATCH 25/41] Add CVC5 option to SMTSolverType and SolverType enums --- Cargo.lock | 1 + src/driver.rs | 1 + src/main.rs | 2 ++ src/slicing/solver.rs | 6 ++++-- z3rro/Cargo.toml | 1 + z3rro/src/prover.rs | 43 ++++++++++++++++++++++++++++++++++++++----- 6 files changed, 47 insertions(+), 7 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index 5a95e4eb..c872a2de 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2750,6 +2750,7 @@ dependencies = [ "num", "once_cell", "ref-cast", + "regex", "smtlib-lowlevel", "tempfile", "thiserror 1.0.69", diff --git a/src/driver.rs b/src/driver.rs index 2d13fb65..30b98ee9 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -834,6 +834,7 @@ fn mk_valid_query_prover<'smt, 'ctx>( let solver_type = match smt_solver { SMTSolverType::Swine => SolverType::SWINE, SMTSolverType::Z3 => SolverType::Z3, + SMTSolverType::CVC5 => SolverType::CVC5, SMTSolverType::SMTLIB(solver) => SolverType::SMTLIB(solver), }; diff --git a/src/main.rs b/src/main.rs index db8537d1..1cc83c6b 100644 --- a/src/main.rs +++ b/src/main.rs @@ -398,6 +398,7 @@ pub enum SMTSolverType { #[default] Z3, Swine, + CVC5, SMTLIB(String), } @@ -408,6 +409,7 @@ impl std::str::FromStr for SMTSolverType { match s { "z3" => Ok(SMTSolverType::Z3), "swine" => Ok(SMTSolverType::Swine), + "cvc5" => Ok(SMTSolverType::CVC5), solver => Ok(SMTSolverType::SMTLIB(solver.to_string())), } } diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index e156776b..9b70d8cf 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -475,8 +475,10 @@ fn slice_sat_binary_search<'ctx>( prover.push(); let ctx = prover.get_context(); - let at_most_n_true = Bool::pb_le(ctx, &slice_vars, at_most_n as i32); - prover.add_assumption(&at_most_n_true); + if !slice_vars.is_empty(){ + let at_most_n_true = Bool::pb_le(ctx, &slice_vars, at_most_n as i32); + prover.add_assumption(&at_most_n_true); + } }; // TODO: we could have min_least_bound set to 1 if we could conclude for diff --git a/z3rro/Cargo.toml b/z3rro/Cargo.toml index 61768a93..88b1b5be 100644 --- a/z3rro/Cargo.toml +++ b/z3rro/Cargo.toml @@ -16,6 +16,7 @@ im-rc = "15" enum-map = "2.7.3" itertools = "0.14.0" smtlib-lowlevel = "0.3.0" +regex = "1" [features] datatype-eureal = [] diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 4ed4aa6d..1de19b12 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -17,6 +17,8 @@ use crate::{ util::{set_solver_timeout, ReasonUnknown}, }; +use regex::Regex; + #[derive(Debug, Error, PartialEq)] pub enum ProverCommandError { #[error("Process execution failed: {0}")] @@ -31,6 +33,7 @@ pub enum ProverCommandError { pub enum SolverType { Z3, SWINE, + CVC5, SMTLIB(String), } @@ -87,17 +90,25 @@ fn execute_solver( SolverType::SWINE => { let mut smt_file = NamedTempFile::new().unwrap(); smt_file - .write_all(remove_lines(&smtlib, SolverType::SWINE).as_bytes()) + .write_all(transform_input_lines(&smtlib, SolverType::SWINE).as_bytes()) .unwrap(); let file_path = smt_file.path(); Command::new("swine").arg("--no-version").arg(file_path).output() } + SolverType::CVC5 => { + let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); + smt_file + .write_all(transform_input_lines(&smtlib, SolverType::CVC5).as_bytes()) + .unwrap(); + let file_path = smt_file.path(); + Command::new("cvc5").arg("--produce-models").arg(file_path).output() + } SolverType::SMTLIB(solver) => { let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); smt_file - .write_all(remove_lines(&smtlib, SolverType::SMTLIB("".to_string())).as_bytes()) + .write_all(transform_input_lines(&smtlib, SolverType::SMTLIB("".to_string())).as_bytes()) .unwrap(); let file_path = smt_file.path(); Command::new(solver).arg(file_path).output() @@ -134,9 +145,10 @@ fn execute_solver( /// To execute the SMT solver correctly, specific modifications to the input are required: /// 1) For SwInE, remove lines that contain a `forall` quantifier or the declaration of the exponential function (`exp``). /// 2) For other solvers, add a line to set logic, and remove incorrect assertions such as `(assert add)`. -fn remove_lines(input: &str, solver: SolverType) -> String { +/// 3) For solvers that do not support at-most, convert those assertions into equivalent logic. +fn transform_input_lines(input: &str, solver: SolverType) -> String { let mut output = match solver { - SolverType::SMTLIB(_) => { + SolverType::CVC5 | SolverType::SMTLIB(_) => { let mut output = String::new(); let logic = if input.contains("*") || input.contains("/") { "(set-logic QF_NIRA)" @@ -170,7 +182,11 @@ fn remove_lines(input: &str, solver: SolverType) -> String { if cnt == 0 { let tmp: String = tmp_buffer.iter().collect(); if condition(&tmp) { - output.push_str(&tmp); + if tmp.contains("at-most"){ + output.push_str(&convert_at_most(&tmp, &solver)); + } else{ + output.push_str(&tmp); + } } tmp_buffer.clear(); } @@ -181,6 +197,23 @@ fn remove_lines(input: &str, solver: SolverType) -> String { output } +fn convert_at_most(input: &str, solver: &SolverType) -> String{ + if solver != &SolverType::CVC5 { + unreachable!("The function 'convert_at_most' should only be called for cvc5"); + } + let re = Regex::new(r#"\(assert\s+\(\(_\s+at-most\s+(\d+)\)\s+([^\)]+)\)\)"#).unwrap(); + + if let Some(re_cap) =re.captures(input) { + let n = &re_cap[1]; + let var_list: Vec<&str> = (&re_cap[2]).split_whitespace().collect(); + + let mut expr_list = var_list.iter().map(|v| format!("(ite {} 1 0)", v)); + return format!("\n(assert (>= {} (+ {})))", n, expr_list.join(" ")); + } + + String::new() +} + impl Display for ProveResult { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { From eeac38e03c2af3b5420a96011622a2d30d2f6d08 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 4 Jul 2025 22:00:57 +0200 Subject: [PATCH 26/41] Fix: skip at-most conversion for non-CVC5 solvers --- z3rro/src/prover.rs | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 1de19b12..c8f39fb7 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -199,19 +199,20 @@ fn transform_input_lines(input: &str, solver: SolverType) -> String { fn convert_at_most(input: &str, solver: &SolverType) -> String{ if solver != &SolverType::CVC5 { - unreachable!("The function 'convert_at_most' should only be called for cvc5"); - } - let re = Regex::new(r#"\(assert\s+\(\(_\s+at-most\s+(\d+)\)\s+([^\)]+)\)\)"#).unwrap(); + input.to_owned() + } else{ + let re = Regex::new(r#"\(assert\s+\(\(_\s+at-most\s+(\d+)\)\s+([^\)]+)\)\)"#).unwrap(); - if let Some(re_cap) =re.captures(input) { - let n = &re_cap[1]; - let var_list: Vec<&str> = (&re_cap[2]).split_whitespace().collect(); + if let Some(re_cap) =re.captures(input) { + let n = &re_cap[1]; + let var_list: Vec<&str> = (&re_cap[2]).split_whitespace().collect(); - let mut expr_list = var_list.iter().map(|v| format!("(ite {} 1 0)", v)); - return format!("\n(assert (>= {} (+ {})))", n, expr_list.join(" ")); + let mut expr_list = var_list.iter().map(|v| format!("(ite {} 1 0)", v)); + return format!("\n(assert (>= {} (+ {})))", n, expr_list.join(" ")); + } + + String::new() } - - String::new() } impl Display for ProveResult { From 2787ebae92adad3e0671d4e94e23984dc8876758 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 4 Jul 2025 22:16:37 +0200 Subject: [PATCH 27/41] Remove SMTLIB option from SMTSolverType and SolverType enums --- src/driver.rs | 1 - src/main.rs | 19 ++++--------------- z3rro/src/prover.rs | 11 +---------- 3 files changed, 5 insertions(+), 26 deletions(-) diff --git a/src/driver.rs b/src/driver.rs index 30b98ee9..7a31d4c1 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -835,7 +835,6 @@ fn mk_valid_query_prover<'smt, 'ctx>( SMTSolverType::Swine => SolverType::SWINE, SMTSolverType::Z3 => SolverType::Z3, SMTSolverType::CVC5 => SolverType::CVC5, - SMTSolverType::SMTLIB(solver) => SolverType::SMTLIB(solver), }; // create the prover and set the params diff --git a/src/main.rs b/src/main.rs index 1cc83c6b..d82cc1ef 100644 --- a/src/main.rs +++ b/src/main.rs @@ -393,26 +393,15 @@ pub struct SMTSolverOptions { pub smt_solver: SMTSolverType, } -#[derive(Debug, Clone, PartialEq, Eq, Default)] +#[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)] pub enum SMTSolverType { #[default] + #[value(name = "z3")] Z3, + #[value(name = "swine")] Swine, + #[value(name = "cvc5")] CVC5, - SMTLIB(String), -} - -impl std::str::FromStr for SMTSolverType { - type Err = String; - - fn from_str(s: &str) -> Result { - match s { - "z3" => Ok(SMTSolverType::Z3), - "swine" => Ok(SMTSolverType::Swine), - "cvc5" => Ok(SMTSolverType::CVC5), - solver => Ok(SMTSolverType::SMTLIB(solver.to_string())), - } - } } #[derive(Debug, Default, Args)] diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index c8f39fb7..f064b0b1 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -34,7 +34,6 @@ pub enum SolverType { Z3, SWINE, CVC5, - SMTLIB(String), } /// The result of a prove query. @@ -105,14 +104,6 @@ fn execute_solver( let file_path = smt_file.path(); Command::new("cvc5").arg("--produce-models").arg(file_path).output() } - SolverType::SMTLIB(solver) => { - let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); - smt_file - .write_all(transform_input_lines(&smtlib, SolverType::SMTLIB("".to_string())).as_bytes()) - .unwrap(); - let file_path = smt_file.path(); - Command::new(solver).arg(file_path).output() - } }; match output { @@ -148,7 +139,7 @@ fn execute_solver( /// 3) For solvers that do not support at-most, convert those assertions into equivalent logic. fn transform_input_lines(input: &str, solver: SolverType) -> String { let mut output = match solver { - SolverType::CVC5 | SolverType::SMTLIB(_) => { + SolverType::CVC5 => { let mut output = String::new(); let logic = if input.contains("*") || input.contains("/") { "(set-logic QF_NIRA)" From b33d3b3f0a32e116023a1bce47889d63cebb85b4 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 9 Jul 2025 20:53:25 +0200 Subject: [PATCH 28/41] Add at_most_k, at_least_k functions --- src/slicing/solver.rs | 15 ++++++++----- src/slicing/util.rs | 50 ++++++++++++++++++++++++++++++++++++++----- z3rro/src/prover.rs | 28 ++++++++++++++++-------- 3 files changed, 74 insertions(+), 19 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 9b70d8cf..375a3dd8 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -9,7 +9,7 @@ use z3::{ }; use z3rro::{ model::{InstrumentedModel, ModelConsistency}, - prover::{ProveResult, Prover, ProverCommandError}, + prover::{ProveResult, Prover, ProverCommandError, SolverType}, util::ReasonUnknown, }; @@ -18,7 +18,7 @@ use crate::{ resource_limits::LimitsRef, slicing::{ model::{SliceMode, SliceModel}, - util::{PartialMinimizeResult, SubsetExploration}, + util::{at_most_k, PartialMinimizeResult, SubsetExploration}, }, smt::translate_exprs::TranslateExprs, VerifyError, @@ -475,8 +475,11 @@ fn slice_sat_binary_search<'ctx>( prover.push(); let ctx = prover.get_context(); - if !slice_vars.is_empty(){ - let at_most_n_true = Bool::pb_le(ctx, &slice_vars, at_most_n as i32); + if !slice_vars.is_empty() { + let at_most_n_true = match prover.get_smt_solver() { + SolverType::CVC5 => at_most_k(ctx, at_most_n as i64, active_slice_vars), + _ => Bool::pb_le(ctx, &slice_vars, at_most_n as i32), + }; prover.add_assumption(&at_most_n_true); } }; @@ -631,7 +634,9 @@ pub fn slice_unsat_search<'ctx>( match options.minimality { SliceMinimality::Any => break, SliceMinimality::Subset => exploration.block_non_subset(&res), - SliceMinimality::Size => exploration.block_at_least(res.len()), + SliceMinimality::Size => { + exploration.block_at_least(res.len(), prover.get_smt_solver()) + } } } Ok(ProveResult::Counterexample) => { diff --git a/src/slicing/util.rs b/src/slicing/util.rs index ec9bce88..ab720f6f 100644 --- a/src/slicing/util.rs +++ b/src/slicing/util.rs @@ -6,7 +6,11 @@ use std::{ use indexmap::IndexSet; use itertools::Itertools; use tracing::{instrument, trace}; -use z3::{ast::Bool, Context, SatResult, Solver}; +use z3::{ + ast::{Bool, Int}, + Context, SatResult, Solver, +}; +use z3rro::prover::SolverType; /// A result of a test during the partial minimization. Either we accept all /// values from this value upwards, we reject all values from this value @@ -197,10 +201,20 @@ impl<'ctx> SubsetExploration<'ctx> { } /// Block all models which have size at least `size`. - pub fn block_at_least(&mut self, size: usize) { - let variables = self.variables.iter().map(|v| (v, 1)).collect_vec(); - self.solver - .assert(&Bool::pb_ge(self.solver.get_context(), &variables, size as i32).not()) + pub fn block_at_least(&mut self, size: usize, solver_type: SolverType) { + let ctx = self.solver.get_context(); + match solver_type { + SolverType::CVC5 => { + let vars_vec: Vec = self.variables.iter().cloned().collect(); + self.solver + .assert(&at_least_k(ctx, size as i64, &vars_vec).not()) + } + _ => { + let variables = self.variables.iter().map(|v| (v, 1)).collect_vec(); + self.solver + .assert(&Bool::pb_ge(ctx, &variables, size as i32).not()) + } + } } /// Block all models which are not subsets of the given set. @@ -411,3 +425,29 @@ impl<'ctx> SubsetExploration<'ctx> { current } } + +/// Create an SMT expression that is true if at most k of the given boolean variables evaluate to true +pub fn at_most_k<'ctx>(ctx: &'ctx Context, k: i64, values: &[Bool<'ctx>]) -> Bool<'ctx> { + let int_values: Vec> = values + .iter() + .map(|b| b.ite(&Int::from_i64(ctx, 1), &Int::from_i64(ctx, 0))) + .collect(); + + let sum = Int::add(ctx, &int_values); + + let k_int = Int::from_i64(ctx, k); + sum.le(&k_int) +} + +/// Create an SMT expression that is true if at least k of the given boolean variables evaluate to true +pub fn at_least_k<'ctx>(ctx: &'ctx Context, k: i64, values: &[Bool<'ctx>]) -> Bool<'ctx> { + let int_values: Vec> = values + .iter() + .map(|b| b.ite(&Int::from_i64(ctx, 1), &Int::from_i64(ctx, 0))) + .collect(); + + let sum = Int::add(ctx, &int_values); + + let k_int = Int::from_i64(ctx, k); + sum.ge(&k_int) +} diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index f064b0b1..2f9fdd2f 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -29,7 +29,7 @@ pub enum ProverCommandError { UnexpectedResultError(String), } -#[derive(Debug, PartialEq)] +#[derive(Debug, PartialEq, Clone)] pub enum SolverType { Z3, SWINE, @@ -94,7 +94,10 @@ fn execute_solver( let file_path = smt_file.path(); - Command::new("swine").arg("--no-version").arg(file_path).output() + Command::new("swine") + .arg("--no-version") + .arg(file_path) + .output() } SolverType::CVC5 => { let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); @@ -102,7 +105,10 @@ fn execute_solver( .write_all(transform_input_lines(&smtlib, SolverType::CVC5).as_bytes()) .unwrap(); let file_path = smt_file.path(); - Command::new("cvc5").arg("--produce-models").arg(file_path).output() + Command::new("cvc5") + .arg("--produce-models") + .arg(file_path) + .output() } }; @@ -173,9 +179,9 @@ fn transform_input_lines(input: &str, solver: SolverType) -> String { if cnt == 0 { let tmp: String = tmp_buffer.iter().collect(); if condition(&tmp) { - if tmp.contains("at-most"){ + if tmp.contains("at-most") { output.push_str(&convert_at_most(&tmp, &solver)); - } else{ + } else { output.push_str(&tmp); } } @@ -188,20 +194,20 @@ fn transform_input_lines(input: &str, solver: SolverType) -> String { output } -fn convert_at_most(input: &str, solver: &SolverType) -> String{ +fn convert_at_most(input: &str, solver: &SolverType) -> String { if solver != &SolverType::CVC5 { input.to_owned() - } else{ + } else { let re = Regex::new(r#"\(assert\s+\(\(_\s+at-most\s+(\d+)\)\s+([^\)]+)\)\)"#).unwrap(); - if let Some(re_cap) =re.captures(input) { + if let Some(re_cap) = re.captures(input) { let n = &re_cap[1]; let var_list: Vec<&str> = (&re_cap[2]).split_whitespace().collect(); let mut expr_list = var_list.iter().map(|v| format!("(ite {} 1 0)", v)); return format!("\n(assert (>= {} (+ {})))", n, expr_list.join(" ")); } - + String::new() } } @@ -590,6 +596,10 @@ impl<'ctx> Prover<'ctx> { pub fn get_smtlib(&self) -> Smtlib { Smtlib::from_solver(self.get_solver()) } + + pub fn get_smt_solver(&self) -> SolverType { + self.smt_solver.clone() + } } #[cfg(test)] From d10805642860f5c59b23eee4e9ed60d2f07080b0 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 9 Jul 2025 21:10:06 +0200 Subject: [PATCH 29/41] Clean up unused code --- Cargo.lock | 75 --------------------------------------------- z3rro/Cargo.toml | 1 - z3rro/src/prover.rs | 24 +-------------- 3 files changed, 1 insertion(+), 99 deletions(-) diff --git a/Cargo.lock b/Cargo.lock index c872a2de..1229f7f7 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -154,12 +154,6 @@ version = "0.21.7" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "9d297deb1925b89f2ccc13d7635fa0714f12c87adce1c75356b39ca9b7178567" -[[package]] -name = "beef" -version = "0.5.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3a8241f3ebb85c056b509d4327ad0358fbbba6ffb340bf388f26350aeda225b1" - [[package]] name = "bindgen" version = "0.69.5" @@ -1224,38 +1218,6 @@ version = "0.4.27" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "13dc2df351e3202783a1fe0d44375f7295ffb4049267b0f3018346dc122a1d94" -[[package]] -name = "logos" -version = "0.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c000ca4d908ff18ac99b93a062cb8958d331c3220719c52e77cb19cc6ac5d2c1" -dependencies = [ - "logos-derive", -] - -[[package]] -name = "logos-codegen" -version = "0.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc487311295e0002e452025d6b580b77bb17286de87b57138f3b5db711cded68" -dependencies = [ - "beef", - "fnv", - "proc-macro2", - "quote", - "regex-syntax 0.6.29", - "syn 2.0.101", -] - -[[package]] -name = "logos-derive" -version = "0.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dbfc0d229f1f42d790440136d941afd806bc9e949e2bcb8faa813b0f00d1267e" -dependencies = [ - "logos-codegen", -] - [[package]] name = "lsp-server" version = "0.7.8" @@ -1297,29 +1259,6 @@ version = "2.7.4" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" -[[package]] -name = "miette" -version = "5.10.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "59bb584eaeeab6bd0226ccf3509a69d7936d148cf3d036ad350abe35e8c6856e" -dependencies = [ - "miette-derive", - "once_cell", - "thiserror 1.0.69", - "unicode-width 0.1.14", -] - -[[package]] -name = "miette-derive" -version = "5.10.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "49e7bc1560b95a3c4a25d03de42fe76ca718ab92d1a22a55b9b4cf67b3ae635c" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.101", -] - [[package]] name = "minimal-lexical" version = "0.2.1" @@ -1965,19 +1904,6 @@ version = "1.15.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "8917285742e9f3e1683f0a9c4e6b57960b7314d0b08d30d1ecd426713ee2eee9" -[[package]] -name = "smtlib-lowlevel" -version = "0.3.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2e48ee399efb51e84d25d4ac02b7e61141f47781d84d8bfc934b8791b30f6c52" -dependencies = [ - "bumpalo", - "itertools 0.12.1", - "logos", - "miette", - "thiserror 1.0.69", -] - [[package]] name = "stable_deref_trait" version = "1.2.0" @@ -2751,7 +2677,6 @@ dependencies = [ "once_cell", "ref-cast", "regex", - "smtlib-lowlevel", "tempfile", "thiserror 1.0.69", "tracing", diff --git a/z3rro/Cargo.toml b/z3rro/Cargo.toml index 88b1b5be..1259ded1 100644 --- a/z3rro/Cargo.toml +++ b/z3rro/Cargo.toml @@ -15,7 +15,6 @@ thiserror = "1.0" im-rc = "15" enum-map = "2.7.3" itertools = "0.14.0" -smtlib-lowlevel = "0.3.0" regex = "1" [features] diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 2f9fdd2f..45c2a384 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -179,11 +179,7 @@ fn transform_input_lines(input: &str, solver: SolverType) -> String { if cnt == 0 { let tmp: String = tmp_buffer.iter().collect(); if condition(&tmp) { - if tmp.contains("at-most") { - output.push_str(&convert_at_most(&tmp, &solver)); - } else { - output.push_str(&tmp); - } + output.push_str(&tmp); } tmp_buffer.clear(); } @@ -194,24 +190,6 @@ fn transform_input_lines(input: &str, solver: SolverType) -> String { output } -fn convert_at_most(input: &str, solver: &SolverType) -> String { - if solver != &SolverType::CVC5 { - input.to_owned() - } else { - let re = Regex::new(r#"\(assert\s+\(\(_\s+at-most\s+(\d+)\)\s+([^\)]+)\)\)"#).unwrap(); - - if let Some(re_cap) = re.captures(input) { - let n = &re_cap[1]; - let var_list: Vec<&str> = (&re_cap[2]).split_whitespace().collect(); - - let mut expr_list = var_list.iter().map(|v| format!("(ite {} 1 0)", v)); - return format!("\n(assert (>= {} (+ {})))", n, expr_list.join(" ")); - } - - String::new() - } -} - impl Display for ProveResult { fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { match self { From 4f7155d43097d0e4164a324a69653faa9853bb12 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Wed, 9 Jul 2025 21:11:07 +0200 Subject: [PATCH 30/41] Clean up unused code --- z3rro/src/prover.rs | 2 -- 1 file changed, 2 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 45c2a384..1b1c4433 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -17,8 +17,6 @@ use crate::{ util::{set_solver_timeout, ReasonUnknown}, }; -use regex::Regex; - #[derive(Debug, Error, PartialEq)] pub enum ProverCommandError { #[error("Process execution failed: {0}")] From 2b5c5ad03a1f387c4faef8e535c6d0b7794a64a7 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Thu, 10 Jul 2025 19:21:56 +0200 Subject: [PATCH 31/41] Restore block_at_least function to original implementation --- src/slicing/solver.rs | 4 +--- src/slicing/util.rs | 32 ++++---------------------------- 2 files changed, 5 insertions(+), 31 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 375a3dd8..5576e069 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -634,9 +634,7 @@ pub fn slice_unsat_search<'ctx>( match options.minimality { SliceMinimality::Any => break, SliceMinimality::Subset => exploration.block_non_subset(&res), - SliceMinimality::Size => { - exploration.block_at_least(res.len(), prover.get_smt_solver()) - } + SliceMinimality::Size => exploration.block_at_least(res.len()), } } Ok(ProveResult::Counterexample) => { diff --git a/src/slicing/util.rs b/src/slicing/util.rs index ab720f6f..086e44cd 100644 --- a/src/slicing/util.rs +++ b/src/slicing/util.rs @@ -10,7 +10,6 @@ use z3::{ ast::{Bool, Int}, Context, SatResult, Solver, }; -use z3rro::prover::SolverType; /// A result of a test during the partial minimization. Either we accept all /// values from this value upwards, we reject all values from this value @@ -201,20 +200,10 @@ impl<'ctx> SubsetExploration<'ctx> { } /// Block all models which have size at least `size`. - pub fn block_at_least(&mut self, size: usize, solver_type: SolverType) { - let ctx = self.solver.get_context(); - match solver_type { - SolverType::CVC5 => { - let vars_vec: Vec = self.variables.iter().cloned().collect(); - self.solver - .assert(&at_least_k(ctx, size as i64, &vars_vec).not()) - } - _ => { - let variables = self.variables.iter().map(|v| (v, 1)).collect_vec(); - self.solver - .assert(&Bool::pb_ge(ctx, &variables, size as i32).not()) - } - } + pub fn block_at_least(&mut self, size: usize) { + let variables = self.variables.iter().map(|v| (v, 1)).collect_vec(); + self.solver + .assert(&Bool::pb_ge(self.solver.get_context(), &variables, size as i32).not()) } /// Block all models which are not subsets of the given set. @@ -438,16 +427,3 @@ pub fn at_most_k<'ctx>(ctx: &'ctx Context, k: i64, values: &[Bool<'ctx>]) -> Boo let k_int = Int::from_i64(ctx, k); sum.le(&k_int) } - -/// Create an SMT expression that is true if at least k of the given boolean variables evaluate to true -pub fn at_least_k<'ctx>(ctx: &'ctx Context, k: i64, values: &[Bool<'ctx>]) -> Bool<'ctx> { - let int_values: Vec> = values - .iter() - .map(|b| b.ite(&Int::from_i64(ctx, 1), &Int::from_i64(ctx, 0))) - .collect(); - - let sum = Int::add(ctx, &int_values); - - let k_int = Int::from_i64(ctx, k); - sum.ge(&k_int) -} From b42f2105360d484f8fcddaf83553b48bff565a4e Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 14 Jul 2025 19:26:03 +0200 Subject: [PATCH 32/41] Add SolverType ExternalZ3 and rename SolverType Z3 to InternalZ3 --- src/driver.rs | 3 ++- src/main.rs | 6 ++++-- src/opt/fuzz_test.rs | 2 +- src/opt/unfolder.rs | 2 +- src/slicing/transform_test.rs | 2 +- z3rro/src/prover.rs | 21 +++++++++++++++------ z3rro/src/test.rs | 2 +- 7 files changed, 25 insertions(+), 13 deletions(-) diff --git a/src/driver.rs b/src/driver.rs index 7a31d4c1..db7b43e4 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -832,8 +832,9 @@ fn mk_valid_query_prover<'smt, 'ctx>( smt_solver: SMTSolverType, ) -> Prover<'ctx> { let solver_type = match smt_solver { + SMTSolverType::InternalZ3 => SolverType::InternalZ3, + SMTSolverType::ExternalZ3 => SolverType::ExternalZ3, SMTSolverType::Swine => SolverType::SWINE, - SMTSolverType::Z3 => SolverType::Z3, SMTSolverType::CVC5 => SolverType::CVC5, }; diff --git a/src/main.rs b/src/main.rs index d82cc1ef..c63cd10f 100644 --- a/src/main.rs +++ b/src/main.rs @@ -389,15 +389,17 @@ pub struct DebugOptions { #[derive(Debug, Default, Args)] #[command(next_help_heading = "SMT Solver Options")] pub struct SMTSolverOptions { - #[arg(long, default_value = "z3")] + #[arg(long, default_value = "default")] pub smt_solver: SMTSolverType, } #[derive(Debug, Clone, Copy, PartialEq, Eq, Default, ValueEnum)] pub enum SMTSolverType { #[default] + #[value(name = "default")] + InternalZ3, #[value(name = "z3")] - Z3, + ExternalZ3, #[value(name = "swine")] Swine, #[value(name = "cvc5")] diff --git a/src/opt/fuzz_test.rs b/src/opt/fuzz_test.rs index fb0b0fb8..e264a913 100644 --- a/src/opt/fuzz_test.rs +++ b/src/opt/fuzz_test.rs @@ -202,7 +202,7 @@ fn prove_equiv(expr: Expr, optimized: Expr, tcx: &TyCtx) -> TestCaseResult { let smt_ctx = SmtCtx::new(&ctx, tcx); let mut translate = TranslateExprs::new(&smt_ctx); let eq_expr_z3 = translate.t_bool(&eq_expr); - let mut prover = Prover::new(&ctx, IncrementalMode::Native, SolverType::Z3); + let mut prover = Prover::new(&ctx, IncrementalMode::Native, SolverType::InternalZ3); translate .local_scope() .add_assumptions_to_prover(&mut prover); diff --git a/src/opt/unfolder.rs b/src/opt/unfolder.rs index c2bd97b6..d97146bb 100644 --- a/src/opt/unfolder.rs +++ b/src/opt/unfolder.rs @@ -60,7 +60,7 @@ impl<'smt, 'ctx> Unfolder<'smt, 'ctx> { // it's important that we use the native incremental mode here, because // the performance benefit from the unfolder relies on many very fast // SAT checks. - let prover = Prover::new(ctx.ctx(), IncrementalMode::Native, SolverType::Z3); + let prover = Prover::new(ctx.ctx(), IncrementalMode::Native, SolverType::InternalZ3); Unfolder { subst: Subst::new(ctx.tcx(), &limits_ref), diff --git a/src/slicing/transform_test.rs b/src/slicing/transform_test.rs index 5d4a234b..0730b4fe 100644 --- a/src/slicing/transform_test.rs +++ b/src/slicing/transform_test.rs @@ -125,7 +125,7 @@ fn prove_equiv( let smt_ctx = SmtCtx::new(&ctx, tcx); let mut translate = TranslateExprs::new(&smt_ctx); let eq_expr_z3 = translate.t_bool(&eq_expr); - let mut prover = Prover::new(&ctx, IncrementalMode::Native, SolverType::Z3); + let mut prover = Prover::new(&ctx, IncrementalMode::Native, SolverType::InternalZ3); translate .local_scope() .add_assumptions_to_prover(&mut prover); diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 1b1c4433..36808413 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -29,7 +29,8 @@ pub enum ProverCommandError { #[derive(Debug, PartialEq, Clone)] pub enum SolverType { - Z3, + InternalZ3, + ExternalZ3, SWINE, CVC5, } @@ -81,9 +82,17 @@ fn execute_solver( let smtlib = smtlib.into_string(); let output = match &prover.smt_solver { - SolverType::Z3 => { + SolverType::InternalZ3 => { unreachable!("The function 'execute_solver' should never be called for z3"); } + SolverType::ExternalZ3 => { + let mut smt_file = NamedTempFile::new().unwrap(); + smt_file.write_all(&smtlib.as_bytes()).unwrap(); + + let file_path = smt_file.path(); + + Command::new("z3").arg(file_path).output() + } SolverType::SWINE => { let mut smt_file = NamedTempFile::new().unwrap(); smt_file @@ -339,7 +348,7 @@ impl<'ctx> Prover<'ctx> { } match self.smt_solver { - SolverType::Z3 => { + SolverType::InternalZ3 => { let res = match &self.last_result { Some(cached_result) if assumptions.is_empty() => { cached_result.last_result.clone() @@ -416,7 +425,7 @@ impl<'ctx> Prover<'ctx> { } let sat_result = match self.smt_solver { - SolverType::Z3 => { + SolverType::InternalZ3 => { let sat_result = self.get_solver().check(); let solver_result = match sat_result { @@ -563,7 +572,7 @@ impl<'ctx> Prover<'ctx> { &[], &Bool::and(self.ctx, &self.get_assertions()).not(), ); - let mut res = Prover::new(self.ctx, IncrementalMode::Native, SolverType::Z3); // TODO + let mut res = Prover::new(self.ctx, IncrementalMode::Native, SolverType::InternalZ3); // TODO res.add_assumption(&theorem); res } @@ -590,7 +599,7 @@ mod test { fn test_prover() { for mode in [IncrementalMode::Native, IncrementalMode::Emulated] { let ctx = Context::new(&Config::default()); - let mut prover = Prover::new(&ctx, mode, SolverType::Z3); + let mut prover = Prover::new(&ctx, mode, SolverType::InternalZ3); assert!(matches!(prover.check_proof(), Ok(ProveResult::Proof))); assert_eq!(prover.check_sat(), Ok(SatResult::Sat)); diff --git a/z3rro/src/test.rs b/z3rro/src/test.rs index f20764ea..8291786d 100644 --- a/z3rro/src/test.rs +++ b/z3rro/src/test.rs @@ -18,7 +18,7 @@ pub fn test_prove(f: impl for<'ctx> FnOnce(&'ctx Context, &mut SmtScope<'ctx>) - let mut scope = SmtScope::new(); let theorem = f(&ctx, &mut scope); - let mut prover = Prover::new(&ctx, IncrementalMode::Native, SolverType::Z3); + let mut prover = Prover::new(&ctx, IncrementalMode::Native, SolverType::InternalZ3); scope.add_assumptions_to_prover(&mut prover); assert_eq!( prover.check_sat(), From 21936b12d53f1459f238c0dbe5b33e09087e4828 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 21 Jul 2025 13:14:10 +0200 Subject: [PATCH 33/41] Add SolverType Yices --- src/driver.rs | 1 + src/main.rs | 2 ++ src/slicing/solver.rs | 2 +- z3rro/src/prover.rs | 14 +++++++++++++- 4 files changed, 17 insertions(+), 2 deletions(-) diff --git a/src/driver.rs b/src/driver.rs index db7b43e4..d075bef8 100644 --- a/src/driver.rs +++ b/src/driver.rs @@ -836,6 +836,7 @@ fn mk_valid_query_prover<'smt, 'ctx>( SMTSolverType::ExternalZ3 => SolverType::ExternalZ3, SMTSolverType::Swine => SolverType::SWINE, SMTSolverType::CVC5 => SolverType::CVC5, + SMTSolverType::Yices => SolverType::YICES, }; // create the prover and set the params diff --git a/src/main.rs b/src/main.rs index c63cd10f..da54383f 100644 --- a/src/main.rs +++ b/src/main.rs @@ -404,6 +404,8 @@ pub enum SMTSolverType { Swine, #[value(name = "cvc5")] CVC5, + #[value(name = "yices")] + Yices, } #[derive(Debug, Default, Args)] diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 5576e069..00ee2e56 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -477,7 +477,7 @@ fn slice_sat_binary_search<'ctx>( let ctx = prover.get_context(); if !slice_vars.is_empty() { let at_most_n_true = match prover.get_smt_solver() { - SolverType::CVC5 => at_most_k(ctx, at_most_n as i64, active_slice_vars), + SolverType::CVC5 | SolverType::YICES => at_most_k(ctx, at_most_n as i64, active_slice_vars), _ => Bool::pb_le(ctx, &slice_vars, at_most_n as i32), }; prover.add_assumption(&at_most_n_true); diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 36808413..53aa7195 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -33,6 +33,7 @@ pub enum SolverType { ExternalZ3, SWINE, CVC5, + YICES, } /// The result of a prove query. @@ -117,6 +118,17 @@ fn execute_solver( .arg(file_path) .output() } + SolverType::YICES => { + let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); + smt_file + .write_all(transform_input_lines(&smtlib, SolverType::YICES).as_bytes()) + .unwrap(); + let file_path = smt_file.path(); + Command::new("yices-smt2") + .arg(file_path) + .arg("--smt2-model-format") + .output() + } }; match output { @@ -152,7 +164,7 @@ fn execute_solver( /// 3) For solvers that do not support at-most, convert those assertions into equivalent logic. fn transform_input_lines(input: &str, solver: SolverType) -> String { let mut output = match solver { - SolverType::CVC5 => { + SolverType::CVC5 | SolverType::YICES => { let mut output = String::new(); let logic = if input.contains("*") || input.contains("/") { "(set-logic QF_NIRA)" From c1cbaf349c31e8d2cc02a3a23c8bfc8ee11311f7 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Thu, 31 Jul 2025 00:32:53 +0200 Subject: [PATCH 34/41] Add timeout setting for external SMT solvers --- src/slicing/solver.rs | 4 +- z3rro/src/prover.rs | 296 +++++++++++++++++++++++++++++------------- 2 files changed, 209 insertions(+), 91 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 00ee2e56..4737e0d9 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -477,7 +477,9 @@ fn slice_sat_binary_search<'ctx>( let ctx = prover.get_context(); if !slice_vars.is_empty() { let at_most_n_true = match prover.get_smt_solver() { - SolverType::CVC5 | SolverType::YICES => at_most_k(ctx, at_most_n as i64, active_slice_vars), + SolverType::CVC5 | SolverType::YICES => { + at_most_k(ctx, at_most_n as i64, active_slice_vars) + } _ => Bool::pb_le(ctx, &slice_vars, at_most_n as i32), }; prover.add_assumption(&at_most_n_true); diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 53aa7195..7834cffe 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -2,9 +2,16 @@ use itertools::Itertools; use thiserror::Error; -use std::{collections::VecDeque, fmt::Display, io::Write, process::Command, time::Duration}; +use std::{ + collections::VecDeque, + fmt::Display, + io::{Seek, SeekFrom, Write}, + path::Path, + process::{Command, Output}, + time::Duration, +}; -use tempfile::{Builder, NamedTempFile}; +use tempfile::NamedTempFile; use z3::{ ast::{forall_const, Ast, Bool, Dynamic}, @@ -70,142 +77,251 @@ impl SolverResult { } /// Execute an SMT solver (other than z3) -fn execute_solver( +fn run_solver( prover: &mut Prover<'_>, assumptions: &[Bool<'_>], ) -> Result { + let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); + smt_file + .write_all(generate_smtlib(prover, assumptions).as_bytes()) + .unwrap(); + + let mut output = call_solver( + smt_file.path(), + prover.get_smt_solver(), + prover.timeout, + None, + ) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + + if !output.status.success() { + return Err(ProverCommandError::ProcessError( + String::from_utf8_lossy(&output.stderr).to_string(), + )); + } + + let stdout = String::from_utf8_lossy(&output.stdout); + let first_line = stdout.lines().next().unwrap_or("").trim().to_lowercase(); + + let sat_result = match first_line.as_str() { + "sat" => { + smt_file + .as_file_mut() + .seek(SeekFrom::End(0)) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + smt_file + .write_all(b"(get-model)\n") + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + + SatResult::Sat + } + "unsat" => SatResult::Unsat, + "unknown" => { + if prover.get_smt_solver() != SolverType::YICES { + smt_file + .as_file_mut() + .seek(SeekFrom::End(0)) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + smt_file + .write_all(b"(get-info :reason-unknown)\n") + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + } + SatResult::Unknown + } + _ => { + return Err(ProverCommandError::UnexpectedResultError( + stdout.into_owned(), + )) + } + }; + + if sat_result == SatResult::Sat || sat_result == SatResult::Unknown { + output = call_solver( + smt_file.path(), + prover.get_smt_solver(), + prover.timeout, + Some(sat_result), + ) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + } + + let stdout = String::from_utf8_lossy(&output.stdout); + let mut lines_buffer: VecDeque<&str> = stdout.lines().collect(); + lines_buffer + .pop_front() + .ok_or(ProverCommandError::ParseError)?; + match sat_result { + SatResult::Unsat => Ok(SolverResult::Unsat), + SatResult::Unknown => Ok(SolverResult::Unknown(Some(ReasonUnknown::Other( + lines_buffer.iter().join("\n"), + )))), + SatResult::Sat => { + let cex = lines_buffer.iter().join(""); + Ok(SolverResult::Sat(Some(cex))) + } + } +} + +fn generate_smtlib(prover: &mut Prover<'_>, assumptions: &[Bool<'_>]) -> String { let mut smtlib = prover.get_smtlib(); + if assumptions.is_empty() { smtlib.add_check_sat(); } else { smtlib.add_check_sat_assuming(assumptions.iter().map(|a| a.to_string()).collect()); }; + let smtlib = smtlib.into_string(); - let output = match &prover.smt_solver { + transform_input_lines(&smtlib, prover.get_smt_solver(), prover.timeout) +} + +fn call_solver( + file_path: &Path, + solver: SolverType, + timeout: Option, + sat_result: Option, +) -> Result { + let (solver, args) = match solver { SolverType::InternalZ3 => { - unreachable!("The function 'execute_solver' should never be called for z3"); + unreachable!("The function 'call_solver' should never be called for z3"); } SolverType::ExternalZ3 => { - let mut smt_file = NamedTempFile::new().unwrap(); - smt_file.write_all(&smtlib.as_bytes()).unwrap(); + let mut args: Vec = match sat_result { + Some(SatResult::Unsat) => unreachable!( + "The function 'call_solver' should not be called again after an 'unsat' result" + ), + Some(SatResult::Sat) => vec!["-model".to_string()], + Some(SatResult::Unknown) | None => vec![], + }; - let file_path = smt_file.path(); + if let Some(t) = timeout { + args.push(format!("-t:{}", t.as_millis())); + } - Command::new("z3").arg(file_path).output() + ("z3", args) } SolverType::SWINE => { - let mut smt_file = NamedTempFile::new().unwrap(); - smt_file - .write_all(transform_input_lines(&smtlib, SolverType::SWINE).as_bytes()) - .unwrap(); - - let file_path = smt_file.path(); + let args: Vec = match sat_result { + Some(SatResult::Unsat) => unreachable!( + "The function 'call_solver' should not be called again after an 'unsat' result" + ), + _ => vec!["--no-version".to_string()], + }; - Command::new("swine") - .arg("--no-version") - .arg(file_path) - .output() + ("swine", args) } SolverType::CVC5 => { - let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); - smt_file - .write_all(transform_input_lines(&smtlib, SolverType::CVC5).as_bytes()) - .unwrap(); - let file_path = smt_file.path(); - Command::new("cvc5") - .arg("--produce-models") - .arg(file_path) - .output() + let mut args: Vec = match sat_result { + Some(SatResult::Unsat) => unreachable!( + "The function 'call_solver' should not be called again after an 'unsat' result" + ), + Some(SatResult::Sat) => vec!["--produce-models".to_string()], + _ => vec![], + }; + + if let Some(t) = timeout { + args.push(format!("--tlimit={}", t.as_millis())); + } + + ("cvc5", args) } SolverType::YICES => { - let mut smt_file = Builder::new().suffix(".smt2").tempfile().unwrap(); - smt_file - .write_all(transform_input_lines(&smtlib, SolverType::YICES).as_bytes()) - .unwrap(); - let file_path = smt_file.path(); - Command::new("yices-smt2") - .arg(file_path) - .arg("--smt2-model-format") - .output() - } - }; + let mut args: Vec = match sat_result { + Some(SatResult::Unsat) => unreachable!( + "The function 'call_solver' should not be called again after an 'unsat' result" + ), + Some(SatResult::Sat) => vec!["--smt2-model-format".to_string()], + _ => vec![], + }; - match output { - Ok(output) => { - let stdout = String::from_utf8_lossy(&output.stdout); - let mut lines_buffer: VecDeque<&str> = stdout.lines().collect(); - let first_line = lines_buffer - .pop_front() - .ok_or(ProverCommandError::ParseError)?; - if first_line.trim().to_lowercase() == "unsat" { - Ok(SolverResult::Unsat) - } else if first_line.trim().to_lowercase() == "sat" { - let cex = lines_buffer.iter().join(""); - Ok(SolverResult::Sat(Some(cex))) - } else if first_line.trim().to_lowercase() == "unknown" { - Ok(SolverResult::Unknown(Some(ReasonUnknown::Other( - lines_buffer.iter().join("\n"), - )))) - } else { - lines_buffer.push_front(first_line); - Err(ProverCommandError::UnexpectedResultError( - lines_buffer.iter().join("\n"), - )) + if let Some(t) = timeout { + let secs = t.as_secs(); + + if secs > 0 { + args.push(format!("--timeout={}", secs)); + } else { + panic!("Timeout must be at least one second. Yices does not support timeouts shorter than 1 second.") + } } + + ("yices-smt2", args) } - Err(e) => Err(ProverCommandError::ProcessError(e.to_string())), - } + }; + + Command::new(solver).args(&args).arg(file_path).output() } /// To execute the SMT solver correctly, specific modifications to the input are required: /// 1) For SwInE, remove lines that contain a `forall` quantifier or the declaration of the exponential function (`exp``). /// 2) For other solvers, add a line to set logic, and remove incorrect assertions such as `(assert add)`. /// 3) For solvers that do not support at-most, convert those assertions into equivalent logic. -fn transform_input_lines(input: &str, solver: SolverType) -> String { +fn transform_input_lines(input: &str, solver: SolverType, timeout: Option) -> String { + let timeout_option = if let Some(t) = timeout { + match solver { + SolverType::InternalZ3 => { + unreachable!( + "The function 'transform_input_lines' should never be called for internal z3" + ); + } + SolverType::SWINE => format!("(set-option :timeout {})\n", t.as_millis()), + _ => "".to_string(), + } + } else { + "".to_string() + }; + let mut output = match solver { SolverType::CVC5 | SolverType::YICES => { let mut output = String::new(); let logic = if input.contains("*") || input.contains("/") { - "(set-logic QF_NIRA)" + "(set-logic QF_NIRA)\n" } else { - "(set-logic QF_LIRA)" + "(set-logic QF_LIRA)\n" }; output.push_str(logic); output } _ => String::new(), }; - let mut tmp_buffer: VecDeque = VecDeque::new(); - let mut input_buffer: VecDeque = input.chars().collect(); - let mut cnt = 0; - let condition = |tmp: &str| match solver { - SolverType::SWINE => !tmp.contains("declare-fun exp") && !tmp.contains("forall"), - _ => !tmp.contains("(assert and)"), - }; + output.push_str(&timeout_option); - // Collect characters until all opened parentheses are closed, and - // keep this block if it does not contain 'declare-fun exp' or 'forall'. - while let Some(c) = input_buffer.pop_front() { - tmp_buffer.push_back(c); - match c { - '(' => { - cnt += 1; - } - ')' => { - cnt -= 1; - if cnt == 0 { - let tmp: String = tmp_buffer.iter().collect(); - if condition(&tmp) { - output.push_str(&tmp); + if solver == SolverType::ExternalZ3 { + output.push_str(input); + } else { + let mut tmp_buffer: VecDeque = VecDeque::new(); + let mut input_buffer: VecDeque = input.chars().collect(); + let mut cnt = 0; + + let condition = |tmp: &str| match solver { + SolverType::SWINE => !tmp.contains("declare-fun exp") && !tmp.contains("forall"), + _ => !tmp.contains("(assert and)"), + }; + + // Collect characters until all opened parentheses are closed, and + // keep this block if it does not contain 'declare-fun exp' or 'forall'. + while let Some(c) = input_buffer.pop_front() { + tmp_buffer.push_back(c); + match c { + '(' => { + cnt += 1; + } + ')' => { + cnt -= 1; + if cnt == 0 { + let tmp: String = tmp_buffer.iter().collect(); + if condition(&tmp) { + output.push_str(&tmp); + } + tmp_buffer.clear(); } - tmp_buffer.clear(); } + _ => {} } - _ => {} } } + output } @@ -397,7 +513,7 @@ impl<'ctx> Prover<'ctx> { cached_result.last_result.clone() } _ => { - let solver_result = execute_solver(self, assumptions)?; + let solver_result = run_solver(self, assumptions)?; if let SolverResult::Sat(Some(cex)) = solver_result.clone() { let solver = self.get_solver(); @@ -450,7 +566,7 @@ impl<'ctx> Prover<'ctx> { sat_result } _ => { - let solver_result = execute_solver(self, &[])?; + let solver_result = run_solver(self, &[])?; if let SolverResult::Sat(Some(cex)) = solver_result.clone() { let solver = self.get_solver(); From 077338dccace5788e76b272a1d18afe475d6f366 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 1 Aug 2025 11:24:39 +0200 Subject: [PATCH 35/41] Change SolverResult::Sat to store a real solver instead of a string --- z3rro/src/prover.rs | 277 +++++++++++++++++++++++--------------------- 1 file changed, 145 insertions(+), 132 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 7834cffe..46d420a2 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -60,13 +60,13 @@ pub enum ProveResult { /// 1) transport the result from SwInE, or /// 2) store SAT result along with a reason for Unknown. #[derive(Debug, Clone)] -pub enum SolverResult { +pub enum SolverResult<'ctx> { Unsat, - Sat(Option), + Sat(Option>), Unknown(Option), } -impl SolverResult { +impl SolverResult<'_> { fn to_sat_result(&self) -> SatResult { match self { SolverResult::Unsat => SatResult::Unsat, @@ -76,106 +76,6 @@ impl SolverResult { } } -/// Execute an SMT solver (other than z3) -fn run_solver( - prover: &mut Prover<'_>, - assumptions: &[Bool<'_>], -) -> Result { - let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); - smt_file - .write_all(generate_smtlib(prover, assumptions).as_bytes()) - .unwrap(); - - let mut output = call_solver( - smt_file.path(), - prover.get_smt_solver(), - prover.timeout, - None, - ) - .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; - - if !output.status.success() { - return Err(ProverCommandError::ProcessError( - String::from_utf8_lossy(&output.stderr).to_string(), - )); - } - - let stdout = String::from_utf8_lossy(&output.stdout); - let first_line = stdout.lines().next().unwrap_or("").trim().to_lowercase(); - - let sat_result = match first_line.as_str() { - "sat" => { - smt_file - .as_file_mut() - .seek(SeekFrom::End(0)) - .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; - smt_file - .write_all(b"(get-model)\n") - .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; - - SatResult::Sat - } - "unsat" => SatResult::Unsat, - "unknown" => { - if prover.get_smt_solver() != SolverType::YICES { - smt_file - .as_file_mut() - .seek(SeekFrom::End(0)) - .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; - smt_file - .write_all(b"(get-info :reason-unknown)\n") - .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; - } - SatResult::Unknown - } - _ => { - return Err(ProverCommandError::UnexpectedResultError( - stdout.into_owned(), - )) - } - }; - - if sat_result == SatResult::Sat || sat_result == SatResult::Unknown { - output = call_solver( - smt_file.path(), - prover.get_smt_solver(), - prover.timeout, - Some(sat_result), - ) - .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; - } - - let stdout = String::from_utf8_lossy(&output.stdout); - let mut lines_buffer: VecDeque<&str> = stdout.lines().collect(); - lines_buffer - .pop_front() - .ok_or(ProverCommandError::ParseError)?; - match sat_result { - SatResult::Unsat => Ok(SolverResult::Unsat), - SatResult::Unknown => Ok(SolverResult::Unknown(Some(ReasonUnknown::Other( - lines_buffer.iter().join("\n"), - )))), - SatResult::Sat => { - let cex = lines_buffer.iter().join(""); - Ok(SolverResult::Sat(Some(cex))) - } - } -} - -fn generate_smtlib(prover: &mut Prover<'_>, assumptions: &[Bool<'_>]) -> String { - let mut smtlib = prover.get_smtlib(); - - if assumptions.is_empty() { - smtlib.add_check_sat(); - } else { - smtlib.add_check_sat_assuming(assumptions.iter().map(|a| a.to_string()).collect()); - }; - - let smtlib = smtlib.into_string(); - - transform_input_lines(&smtlib, prover.get_smt_solver(), prover.timeout) -} - fn call_solver( file_path: &Path, solver: SolverType, @@ -354,7 +254,7 @@ enum StackSolver<'ctx> { } #[derive(Debug)] -struct LastSatSolverResult { +struct LastSatSolverResult<'ctx> { /// Whether the current model is consistent with the assertions. If the SMT /// solver returned [`SatResult::Unknown`], it is /// [`ModelConsistency::Unknown`]. @@ -363,7 +263,7 @@ struct LastSatSolverResult { /// It is reset any time the assertions on the solver are modified. /// Sometimes Z3 caches on its own, but it is not reliable. Therefore, we do /// it here as well to be sure. - last_result: SolverResult, + last_result: SolverResult<'ctx>, } /// A prover wraps a SAT solver, but it's used to prove validity of formulas. @@ -390,7 +290,7 @@ pub struct Prover<'ctx> { /// SMT solver type smt_solver: SolverType, /// Cached information about the last SAT/proof check call. - last_result: Option, + last_result: Option>, } impl<'ctx> Prover<'ctx> { @@ -510,23 +410,17 @@ impl<'ctx> Prover<'ctx> { _ => { let res = match &self.last_result { Some(cached_result) if assumptions.is_empty() => { - cached_result.last_result.clone() + Ok(cached_result.last_result.clone()) } _ => { - let solver_result = run_solver(self, assumptions)?; - - if let SolverResult::Sat(Some(cex)) = solver_result.clone() { - let solver = self.get_solver(); - solver.from_string(cex); - solver.check(); - }; - - self.cache_result(solver_result.clone()); - solver_result + let solver_result = self.run_solver(assumptions)?; + Ok(solver_result) } }; - match res { + let sat_result = res?; + + match sat_result { SolverResult::Unsat => Ok(ProveResult::Proof), SolverResult::Unknown(r) => { let reason = r.unwrap_or(ReasonUnknown::Other("".to_string())); @@ -566,15 +460,7 @@ impl<'ctx> Prover<'ctx> { sat_result } _ => { - let solver_result = run_solver(self, &[])?; - - if let SolverResult::Sat(Some(cex)) = solver_result.clone() { - let solver = self.get_solver(); - solver.from_string(cex); - solver.check(); - }; - self.cache_result(solver_result.clone()); - + let solver_result = self.run_solver(&[])?; solver_result.to_sat_result() } }; @@ -583,7 +469,7 @@ impl<'ctx> Prover<'ctx> { } /// Save the result of the last SAT/proof check. - fn cache_result(&mut self, solver_result: SolverResult) { + fn cache_result(&mut self, solver_result: SolverResult<'ctx>) { let model_consistency = match solver_result { SolverResult::Sat(_) => Some(ModelConsistency::Consistent), SolverResult::Unknown(_) => Some(ModelConsistency::Unknown), @@ -603,7 +489,22 @@ impl<'ctx> Prover<'ctx> { /// [`ModelConsistency::Inconsistent`]. pub fn get_model(&self) -> Option> { let consistency = self.last_result.as_ref()?.model_consistency?; - let model = self.get_solver().get_model()?; + let model = match self.smt_solver { + SolverType::InternalZ3 => self.get_solver().get_model()?, + _ => { + let solver = if let Some(cached_result) = &self.last_result { + if let SolverResult::Sat(Some(solver)) = &cached_result.last_result { + solver + } else { + &Solver::new(self.ctx) + } + } else { + &Solver::new(self.ctx) + }; + + solver.get_model()? + } + }; Some(InstrumentedModel::new(consistency, model)) } @@ -614,9 +515,23 @@ impl<'ctx> Prover<'ctx> { /// See [`Solver::get_reason_unknown`]. pub fn get_reason_unknown(&self) -> Option { - self.get_solver() - .get_reason_unknown() - .map(|reason| reason.parse().unwrap()) + match self.smt_solver { + SolverType::InternalZ3 => self + .get_solver() + .get_reason_unknown() + .map(|reason| reason.parse().unwrap()), + _ => { + if let Some(cached_result) = &self.last_result { + if let SolverResult::Unknown(reason_unknown) = &cached_result.last_result { + reason_unknown.clone() + } else { + Some(ReasonUnknown::Other("".to_string())) + } + } else { + Some(ReasonUnknown::Other("".to_string())) + } + } + } } /// See [`Solver::push`]. @@ -713,6 +628,104 @@ impl<'ctx> Prover<'ctx> { pub fn get_smt_solver(&self) -> SolverType { self.smt_solver.clone() } + + /// Execute an SMT solver (other than z3) + fn run_solver(&mut self, assumptions: &[Bool<'_>]) -> Result { + let mut smt_file: NamedTempFile = NamedTempFile::new().unwrap(); + smt_file + .write_all(self.generate_smtlib(assumptions).as_bytes()) + .unwrap(); + + let mut output = call_solver(smt_file.path(), self.get_smt_solver(), self.timeout, None) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + + if !output.status.success() { + return Err(ProverCommandError::ProcessError( + String::from_utf8_lossy(&output.stderr).to_string(), + )); + } + + let stdout = String::from_utf8_lossy(&output.stdout); + let first_line = stdout.lines().next().unwrap_or("").trim().to_lowercase(); + + let sat_result = match first_line.as_str() { + "sat" => { + smt_file + .as_file_mut() + .seek(SeekFrom::End(0)) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + smt_file + .write_all(b"(get-model)\n") + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + + SatResult::Sat + } + "unsat" => SatResult::Unsat, + "unknown" => { + if self.smt_solver != SolverType::YICES { + smt_file + .as_file_mut() + .seek(SeekFrom::End(0)) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + smt_file + .write_all(b"(get-info :reason-unknown)\n") + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + } + SatResult::Unknown + } + _ => { + return Err(ProverCommandError::UnexpectedResultError( + stdout.into_owned(), + )) + } + }; + + if sat_result == SatResult::Sat || sat_result == SatResult::Unknown { + output = call_solver( + smt_file.path(), + self.get_smt_solver(), + self.timeout, + Some(sat_result), + ) + .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; + } + + let stdout = String::from_utf8_lossy(&output.stdout); + let mut lines_buffer: VecDeque<&str> = stdout.lines().collect(); + lines_buffer + .pop_front() + .ok_or(ProverCommandError::ParseError)?; + let solver_result = match sat_result { + SatResult::Unsat => SolverResult::Unsat, + SatResult::Unknown => { + SolverResult::Unknown(Some(ReasonUnknown::Other(lines_buffer.iter().join("\n")))) + } + SatResult::Sat => { + let cex = lines_buffer.iter().join(""); + let solver = Solver::new(self.ctx); + solver.from_string(cex); + solver.check(); + SolverResult::Sat(Some(solver)) + } + }; + + self.cache_result(solver_result.clone()); + Ok(solver_result) + } + + fn generate_smtlib(&self, assumptions: &[Bool<'_>]) -> String { + let mut smtlib = self.get_smtlib(); + + if assumptions.is_empty() { + smtlib.add_check_sat(); + } else { + smtlib.add_check_sat_assuming(assumptions.iter().map(|a| a.to_string()).collect()); + }; + + let smtlib = smtlib.into_string(); + + transform_input_lines(&smtlib, self.get_smt_solver(), self.timeout) + } } #[cfg(test)] From 39ffe52779a10adbac8fa945d471d06b694149af Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 18 Aug 2025 12:12:57 +0200 Subject: [PATCH 36/41] Change solver handling back to match original behavior --- src/slicing/solver.rs | 26 ++++++++++++-------------- 1 file changed, 12 insertions(+), 14 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 4737e0d9..9f8cf1c0 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -622,13 +622,12 @@ pub fn slice_unsat_search<'ctx>( match check_proof_seed(&all_variables, prover, limits_ref, &seed) { Ok(ProveResult::Proof) => { // now start the shrinking, then block up - let res_seed = match check_proof_seed(&all_variables, prover, limits_ref, &seed) { - Ok(ProveResult::Proof) => Some(unsat_core_to_seed(prover, &all_variables)), - Ok(ProveResult::Counterexample) | Ok(ProveResult::Unknown(_)) => None, - Err(err) => return Err(VerifyError::ProverError(err)), - }; - - let res = exploration.shrink_block_unsat(seed, |_| res_seed.clone()); + let res = exploration.shrink_block_unsat(seed, |seed|{ + match check_proof_seed(&all_variables, prover, limits_ref, seed) { + Ok(ProveResult::Proof) => Some(unsat_core_to_seed(prover, &all_variables)), + _ => None, + } + }); let res_vec: Vec<_> = res.iter().cloned().collect(); slice_searcher.found_active(res_vec); @@ -641,13 +640,12 @@ pub fn slice_unsat_search<'ctx>( } Ok(ProveResult::Counterexample) => { // grow the counterexample and then block down - let res_seed = match check_proof_seed(&all_variables, prover, limits_ref, &seed) { - Ok(ProveResult::Counterexample) => true, - Ok(ProveResult::Proof) | Ok(ProveResult::Unknown(_)) => false, - Err(err) => return Err(VerifyError::ProverError(err)), - }; - - exploration.grow_block_sat(seed, |_| res_seed); + exploration.grow_block_sat(seed, |seed| { + match check_proof_seed(&all_variables, prover, limits_ref, seed) { + Ok(ProveResult::Counterexample) => true, + _ => false, + } + }); } Ok(ProveResult::Unknown(_)) => { exploration.block_this(&seed); From 98b84e81c5e64296c833c8c359f748425a31d919 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 18 Aug 2025 13:55:43 +0200 Subject: [PATCH 37/41] Add SolverType parameter to at_most_k --- src/slicing/solver.rs | 16 ++++------------ src/slicing/util.rs | 30 ++++++++++++++++++++---------- 2 files changed, 24 insertions(+), 22 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 9f8cf1c0..c8cc171b 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -9,7 +9,7 @@ use z3::{ }; use z3rro::{ model::{InstrumentedModel, ModelConsistency}, - prover::{ProveResult, Prover, ProverCommandError, SolverType}, + prover::{ProveResult, Prover, ProverCommandError}, util::ReasonUnknown, }; @@ -467,21 +467,13 @@ fn slice_sat_binary_search<'ctx>( ) -> Result<(), VerifyError> { assert_eq!(prover.level(), 2); - let slice_vars: Vec<(&Bool<'ctx>, i32)> = - active_slice_vars.iter().map(|value| (value, 1)).collect(); - let set_at_most_true = |prover: &mut Prover<'ctx>, at_most_n: usize| { prover.pop(); prover.push(); let ctx = prover.get_context(); - if !slice_vars.is_empty() { - let at_most_n_true = match prover.get_smt_solver() { - SolverType::CVC5 | SolverType::YICES => { - at_most_k(ctx, at_most_n as i64, active_slice_vars) - } - _ => Bool::pb_le(ctx, &slice_vars, at_most_n as i32), - }; + if !active_slice_vars.is_empty() { + let at_most_n_true = at_most_k(ctx, at_most_n, active_slice_vars, prover.get_smt_solver()); prover.add_assumption(&at_most_n_true); } }; @@ -498,7 +490,7 @@ fn slice_sat_binary_search<'ctx>( // the fix would be to track explicitly whether we can make that assumption // that min_least_bound is 1. let min_least_bound = 0; - let mut minimize = PartialMinimizer::new(min_least_bound..=slice_vars.len()); + let mut minimize = PartialMinimizer::new(min_least_bound..=active_slice_vars.len()); let mut cur_solver_n = None; let mut slice_searcher = SliceModelSearch::new(active_slice_vars.to_vec()); diff --git a/src/slicing/util.rs b/src/slicing/util.rs index 086e44cd..bf499bb6 100644 --- a/src/slicing/util.rs +++ b/src/slicing/util.rs @@ -10,6 +10,7 @@ use z3::{ ast::{Bool, Int}, Context, SatResult, Solver, }; +use z3rro::prover::SolverType; /// A result of a test during the partial minimization. Either we accept all /// values from this value upwards, we reject all values from this value @@ -416,14 +417,23 @@ impl<'ctx> SubsetExploration<'ctx> { } /// Create an SMT expression that is true if at most k of the given boolean variables evaluate to true -pub fn at_most_k<'ctx>(ctx: &'ctx Context, k: i64, values: &[Bool<'ctx>]) -> Bool<'ctx> { - let int_values: Vec> = values - .iter() - .map(|b| b.ite(&Int::from_i64(ctx, 1), &Int::from_i64(ctx, 0))) - .collect(); - - let sum = Int::add(ctx, &int_values); - - let k_int = Int::from_i64(ctx, k); - sum.le(&k_int) +pub fn at_most_k<'ctx>(ctx: &'ctx Context, k: usize, values: &[Bool<'ctx>], solver_type: SolverType) -> Bool<'ctx> { + match solver_type { + SolverType::CVC5 | SolverType::YICES => { + let int_values: Vec> = values + .iter() + .map(|b| b.ite(&Int::from_i64(ctx, 1), &Int::from_i64(ctx, 0))) + .collect(); + + let sum = Int::add(ctx, &int_values); + + let k_int = Int::from_i64(ctx, k as i64); + sum.le(&k_int) + } + _ => { + let slice_vars: Vec<(&Bool<'ctx>, i32)> = + values.iter().map(|value| (value, 1)).collect(); + Bool::pb_le(ctx, &slice_vars, k as i32) + } + } } From 718554a6366d760fe67cee4417fe2730989f56b1 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 18 Aug 2025 14:00:44 +0200 Subject: [PATCH 38/41] Rename function to get_solver_type --- src/slicing/solver.rs | 2 +- z3rro/src/prover.rs | 8 ++++---- 2 files changed, 5 insertions(+), 5 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index c8cc171b..17331d3d 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -473,7 +473,7 @@ fn slice_sat_binary_search<'ctx>( let ctx = prover.get_context(); if !active_slice_vars.is_empty() { - let at_most_n_true = at_most_k(ctx, at_most_n, active_slice_vars, prover.get_smt_solver()); + let at_most_n_true = at_most_k(ctx, at_most_n, active_slice_vars, prover.get_solver_type()); prover.add_assumption(&at_most_n_true); } }; diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 46d420a2..e04b8b57 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -625,7 +625,7 @@ impl<'ctx> Prover<'ctx> { Smtlib::from_solver(self.get_solver()) } - pub fn get_smt_solver(&self) -> SolverType { + pub fn get_solver_type(&self) -> SolverType { self.smt_solver.clone() } @@ -636,7 +636,7 @@ impl<'ctx> Prover<'ctx> { .write_all(self.generate_smtlib(assumptions).as_bytes()) .unwrap(); - let mut output = call_solver(smt_file.path(), self.get_smt_solver(), self.timeout, None) + let mut output = call_solver(smt_file.path(), self.get_solver_type(), self.timeout, None) .map_err(|e| ProverCommandError::ProcessError(e.to_string()))?; if !output.status.success() { @@ -683,7 +683,7 @@ impl<'ctx> Prover<'ctx> { if sat_result == SatResult::Sat || sat_result == SatResult::Unknown { output = call_solver( smt_file.path(), - self.get_smt_solver(), + self.get_solver_type(), self.timeout, Some(sat_result), ) @@ -724,7 +724,7 @@ impl<'ctx> Prover<'ctx> { let smtlib = smtlib.into_string(); - transform_input_lines(&smtlib, self.get_smt_solver(), self.timeout) + transform_input_lines(&smtlib, self.get_solver_type(), self.timeout) } } From 308846fa1bda24ce97d0bbe2418c4ed2727441f9 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 19 Sep 2025 21:38:22 +0200 Subject: [PATCH 39/41] Make SolverResult independent from lifetime 'ctx' to fix E0499 error --- z3rro/src/prover.rs | 29 +++++++++++++++-------------- 1 file changed, 15 insertions(+), 14 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index e04b8b57..5585888f 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -60,13 +60,13 @@ pub enum ProveResult { /// 1) transport the result from SwInE, or /// 2) store SAT result along with a reason for Unknown. #[derive(Debug, Clone)] -pub enum SolverResult<'ctx> { +pub enum SolverResult { Unsat, - Sat(Option>), + Sat(Option), Unknown(Option), } -impl SolverResult<'_> { +impl SolverResult { fn to_sat_result(&self) -> SatResult { match self { SolverResult::Unsat => SatResult::Unsat, @@ -254,7 +254,7 @@ enum StackSolver<'ctx> { } #[derive(Debug)] -struct LastSatSolverResult<'ctx> { +struct LastSatSolverResult { /// Whether the current model is consistent with the assertions. If the SMT /// solver returned [`SatResult::Unknown`], it is /// [`ModelConsistency::Unknown`]. @@ -263,7 +263,7 @@ struct LastSatSolverResult<'ctx> { /// It is reset any time the assertions on the solver are modified. /// Sometimes Z3 caches on its own, but it is not reliable. Therefore, we do /// it here as well to be sure. - last_result: SolverResult<'ctx>, + last_result: SolverResult, } /// A prover wraps a SAT solver, but it's used to prove validity of formulas. @@ -290,7 +290,7 @@ pub struct Prover<'ctx> { /// SMT solver type smt_solver: SolverType, /// Cached information about the last SAT/proof check call. - last_result: Option>, + last_result: Option, } impl<'ctx> Prover<'ctx> { @@ -414,6 +414,7 @@ impl<'ctx> Prover<'ctx> { } _ => { let solver_result = self.run_solver(assumptions)?; + self.cache_result(solver_result.clone()); Ok(solver_result) } }; @@ -469,7 +470,7 @@ impl<'ctx> Prover<'ctx> { } /// Save the result of the last SAT/proof check. - fn cache_result(&mut self, solver_result: SolverResult<'ctx>) { + fn cache_result(&mut self, solver_result: SolverResult) { let model_consistency = match solver_result { SolverResult::Sat(_) => Some(ModelConsistency::Consistent), SolverResult::Unknown(_) => Some(ModelConsistency::Unknown), @@ -493,13 +494,16 @@ impl<'ctx> Prover<'ctx> { SolverType::InternalZ3 => self.get_solver().get_model()?, _ => { let solver = if let Some(cached_result) = &self.last_result { - if let SolverResult::Sat(Some(solver)) = &cached_result.last_result { + if let SolverResult::Sat(Some(cex)) = &cached_result.last_result { + let solver = Solver::new(self.ctx); + solver.from_string(cex.clone()); + solver.check(); solver } else { - &Solver::new(self.ctx) + Solver::new(self.ctx) } } else { - &Solver::new(self.ctx) + Solver::new(self.ctx) }; solver.get_model()? @@ -702,10 +706,7 @@ impl<'ctx> Prover<'ctx> { } SatResult::Sat => { let cex = lines_buffer.iter().join(""); - let solver = Solver::new(self.ctx); - solver.from_string(cex); - solver.check(); - SolverResult::Sat(Some(solver)) + SolverResult::Sat(Some(cex)) } }; From 3a3e33fe4019848889a942e0936cce12303435c0 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Fri, 19 Sep 2025 21:39:56 +0200 Subject: [PATCH 40/41] Code formatting --- src/slicing/solver.rs | 5 +++-- src/slicing/util.rs | 7 ++++++- 2 files changed, 9 insertions(+), 3 deletions(-) diff --git a/src/slicing/solver.rs b/src/slicing/solver.rs index 17331d3d..c4bcb7a7 100644 --- a/src/slicing/solver.rs +++ b/src/slicing/solver.rs @@ -473,7 +473,8 @@ fn slice_sat_binary_search<'ctx>( let ctx = prover.get_context(); if !active_slice_vars.is_empty() { - let at_most_n_true = at_most_k(ctx, at_most_n, active_slice_vars, prover.get_solver_type()); + let at_most_n_true = + at_most_k(ctx, at_most_n, active_slice_vars, prover.get_solver_type()); prover.add_assumption(&at_most_n_true); } }; @@ -614,7 +615,7 @@ pub fn slice_unsat_search<'ctx>( match check_proof_seed(&all_variables, prover, limits_ref, &seed) { Ok(ProveResult::Proof) => { // now start the shrinking, then block up - let res = exploration.shrink_block_unsat(seed, |seed|{ + let res = exploration.shrink_block_unsat(seed, |seed| { match check_proof_seed(&all_variables, prover, limits_ref, seed) { Ok(ProveResult::Proof) => Some(unsat_core_to_seed(prover, &all_variables)), _ => None, diff --git a/src/slicing/util.rs b/src/slicing/util.rs index bf499bb6..3d4ed9a3 100644 --- a/src/slicing/util.rs +++ b/src/slicing/util.rs @@ -417,7 +417,12 @@ impl<'ctx> SubsetExploration<'ctx> { } /// Create an SMT expression that is true if at most k of the given boolean variables evaluate to true -pub fn at_most_k<'ctx>(ctx: &'ctx Context, k: usize, values: &[Bool<'ctx>], solver_type: SolverType) -> Bool<'ctx> { +pub fn at_most_k<'ctx>( + ctx: &'ctx Context, + k: usize, + values: &[Bool<'ctx>], + solver_type: SolverType, +) -> Bool<'ctx> { match solver_type { SolverType::CVC5 | SolverType::YICES => { let int_values: Vec> = values From 50b1814eb429cf782b5fe0bf240cbff89bce7600 Mon Sep 17 00:00:00 2001 From: Se Rin Yang Date: Mon, 29 Sep 2025 06:35:19 +0200 Subject: [PATCH 41/41] Add result_solver to Prover for external solver output --- z3rro/src/prover.rs | 42 ++++++++++++++++++++++++++++++------------ 1 file changed, 30 insertions(+), 12 deletions(-) diff --git a/z3rro/src/prover.rs b/z3rro/src/prover.rs index 5585888f..bfbd6b1a 100644 --- a/z3rro/src/prover.rs +++ b/z3rro/src/prover.rs @@ -291,6 +291,7 @@ pub struct Prover<'ctx> { smt_solver: SolverType, /// Cached information about the last SAT/proof check call. last_result: Option, + result_solver: Option>, } impl<'ctx> Prover<'ctx> { @@ -309,6 +310,7 @@ impl<'ctx> Prover<'ctx> { min_level_with_provables: None, smt_solver: solver_type, last_result: None, + result_solver: None, } } @@ -414,7 +416,20 @@ impl<'ctx> Prover<'ctx> { } _ => { let solver_result = self.run_solver(assumptions)?; + + if let SolverResult::Sat(Some(cex)) = solver_result.clone() { + if let Some(solver) = &self.result_solver { + solver.from_string(cex.clone()); + solver.check(); + } else { + let solver = Solver::new(self.ctx); + solver.from_string(cex.clone()); + solver.check(); + self.result_solver = Some(solver); + } + } self.cache_result(solver_result.clone()); + Ok(solver_result) } }; @@ -462,6 +477,18 @@ impl<'ctx> Prover<'ctx> { } _ => { let solver_result = self.run_solver(&[])?; + if let SolverResult::Sat(Some(cex)) = solver_result.clone() { + if let Some(solver) = &self.result_solver { + solver.from_string(cex.clone()); + solver.check(); + } else { + let solver = Solver::new(self.ctx); + solver.from_string(cex.clone()); + solver.check(); + self.result_solver = Some(solver); + } + } + self.cache_result(solver_result.clone()); solver_result.to_sat_result() } }; @@ -493,17 +520,9 @@ impl<'ctx> Prover<'ctx> { let model = match self.smt_solver { SolverType::InternalZ3 => self.get_solver().get_model()?, _ => { - let solver = if let Some(cached_result) = &self.last_result { - if let SolverResult::Sat(Some(cex)) = &cached_result.last_result { - let solver = Solver::new(self.ctx); - solver.from_string(cex.clone()); - solver.check(); - solver - } else { - Solver::new(self.ctx) - } - } else { - Solver::new(self.ctx) + let solver = match &self.result_solver { + Some(solver) => solver, + None => &Solver::new(self.ctx), }; solver.get_model()? @@ -710,7 +729,6 @@ impl<'ctx> Prover<'ctx> { } }; - self.cache_result(solver_result.clone()); Ok(solver_result) }