Implement execution of swine-z3 on SMT2 files

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>(

z3rro/src/prover.rs

@@ -1,6 +1,9 @@
 //! Not a SAT solver, but a prover. There's a difference.
+use thiserror::Error;
 
-use std::{fmt::Display, time::Duration};
+use std::{collections::VecDeque, env, fmt::Display, io::{self, Write}, path::Path, process::{self, Command}, time::Duration};
+
+use tempfile::NamedTempFile;
 
 use z3::{
     ast::{forall_const, Ast, Bool, Dynamic},
@@ -13,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> {
@@ -21,6 +36,68 @@ pub enum ProveResult<'ctx> {
     Unknown(ReasonUnknown),
 }
 
+/// Execute swine-z3 on the file located at file_path
+fn execute_swine(file_path: &Path) -> Result<SatResult, CommandError>{
+    match env::var("SWINE") {
+        // Use "export SWINE=<path_for_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))
+                }
+            }
+        }
+        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<char> = VecDeque::new();
+    let mut input_buffer: VecDeque<char> = 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 {
@@ -85,27 +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 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)
+
+        let res;
+
+        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();
+
+                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)
+                    }
+                }
             }
         }
     }