Implement execution of swine-z3 on SMT2 files #65
Conversation
z3rro/src/prover.rs
Outdated
| fn execute_swine(dir: &Path, file_path: &Path) { | ||
| let swine = "swine-z3"; | ||
|
|
||
| let find_output = Command::new("find") |
There was a problem hiding this comment.
I don't understand wh
8000
y you'd be using find here? It should be sufficient to just do the call to swine directly.
z3rro/src/prover.rs
Outdated
| .output().unwrap(); | ||
|
|
||
| if cmd_output.status.success() { | ||
| println!("{}", String::from_utf8_lossy(&cmd_output.stdout)); |
There was a problem hiding this comment.
The next step would be to parse the output of SWINE and return a SatResult.
z3rro/src/prover.rs
Outdated
| println!("{}", String::from_utf8_lossy(&cmd_output.stdout)); | ||
| break; | ||
| } else { | ||
| eprintln!("Failed to execute swine({}) command with status: {}", line, cmd_output.status); |
There was a problem hiding this comment.
Ideally, return a Result and return an error in this case.
z3rro/src/prover.rs
Outdated
| } | ||
| } | ||
| } else { | ||
| eprintln!("Find command execution failed"); |
| } | ||
| } | ||
|
|
||
| fn remove_lines_for_swine(input: &str) -> String { |
There was a problem hiding this comment.
Please add a doc comment saying which lines this removes.
z3rro/src/prover.rs
Outdated
| @@ -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(); | |||
There was a problem hiding this comment.
As a next step, add an solver_type attribute of a new enum type SolverType with variants Z3 and SWINE, and then choose here whether to invoke either Z3 or SWINE.
There was a problem hiding this comment.
You can do this like we did it for SliceVerifyMethod and the SliceOptions::slice_verify_via option in main.rs.
…_proof_assuming functions
…and GetModelResponse
…utput as reason if unknown
| } | ||
|
|
||
| #[derive(Debug)] | ||
| pub enum SolverType { |
There was a problem hiding this comment.
Let's introduce another SolverType here: SMTLIB(Command), which takes a Command object and uses it as a backend, just like we currently do for SWINE. Except that for SMTLIB, we don't remove the exp declaration.
z3rro/src/prover.rs
Outdated
| 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") { |
There was a problem hiding this comment.
This looks strange and at least requires a comment why that's here.
| } else { | ||
| Err(ProverCommandError::ParseError) | ||
| } | ||
| } else { |
There was a problem hiding this comment.
We should only return Unknown if the SAT solver result is actually unknown. If there's a different result than we expected, we must throw an error.
| let mut input_buffer: VecDeque<char> = input.chars().collect(); | ||
| let mut cnt = 0; | ||
|
|
||
| while let Some(c) = input_buffer.pop_front() { |
There was a problem hiding this comment.
Maybe add a comment that you collect the full string for a (possibly multi-line) SMTLIB command by looking for the corresponding closed parenthesis, while counting nested parenthesis.
z3rro/src/prover.rs
Outdated
| @@ -152,36 +243,76 @@ impl<'ctx> Prover<'ctx> { | |||
| self.add_assumption(&value.not()); | |||
| self.min_level_with_provables.get_or_insert(self.level); | |||
| } | |||
|
|
|||
There was a problem hiding this comment.
Be sure to have your editor automatically remove trailing spaces. cargo fmt --all should remove these as well, I think.
| } | ||
| } | ||
| SolverType::Z3 => { | ||
| let res = match &self.last_result { |
There was a problem hiding this comment.
All of this logic needs to happen for the SWINE calls as well! This includes returning cached results, checking with assumptions (where did the assumptions go when using SWINE??) and caching results afterwards.
z3rro/src/test.rs
Outdated
| ProveResult::Proof => {} | ||
| Ok(ProveResult::Unknown(reason)) => panic!("solver returned unknown ({})", reason), | ||
| Ok(ProveResult::Proof) => {}, | ||
| Err(_) => {} |
There was a problem hiding this comment.
why is the error here silently ignored?
| @@ -15,6 +15,7 @@ thiserror = "1.0" | |||
| im-rc = "15" | |||
| enum-map = "2.7.3" | |||
| itertools = "0.14.0" | |||
| smtlib-lowlevel = "0.3.0" | |||
There was a problem hiding this comment.
Are we using this still?
|
W.r.t. the "the |
No description provided.