Implement execution of swine-z3 on SMT2 files by SeRin-Yang · Pull Request #65 · moves-rwth/caesar

SeRin-Yang · 2025-02-11T22:39:33Z

No description provided.

Philipp15b

Thanks! I've left a bunch of comments.

Philipp15b · 2025-02-12T10:04:16Z

z3rro/src/prover.rs

+fn execute_swine(dir: &Path, file_path: &Path) {
+    let swine = "swine-z3";
+
+    let find_output = Command::new("find")


I don't understand why you'd be using find here? It should be sufficient to just do the call to swine directly.

Philipp15b · 2025-02-12T10:05:26Z

z3rro/src/prover.rs

+                    .output().unwrap();
+
+                if cmd_output.status.success() {
+                    println!("{}", String::from_utf8_lossy(&cmd_output.stdout));


The next step would be to parse the output of SWINE and return a SatResult.

Philipp15b · 2025-02-12T10:06:09Z

z3rro/src/prover.rs

+                    println!("{}", String::from_utf8_lossy(&cmd_output.stdout));
+                    break;
+                } else {
+                    eprintln!("Failed to execute swine({}) command with status: {}", line, cmd_output.status);


Ideally, return a Result and return an error in this case.

Philipp15b · 2025-02-12T10:06:14Z

z3rro/src/prover.rs

+            }
+        }
+    } else {
+        eprintln!("Find command execution failed");


Philipp15b · 2025-02-12T10:06:33Z

z3rro/src/prover.rs

+    }
+}
+
+fn remove_lines_for_swine(input: &str) -> String {


Please add a doc comment saying which lines this removes.

Philipp15b · 2025-02-12T10:08:31Z

z3rro/src/prover.rs

            return ProveResult::Proof;
        }
+
+        let mut smtlib = self.get_smtlib();


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.

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

…igInt, BigInt)

…utput as reason if unknown

z3rro/src/prover.rs

Philipp15b · 2025-05-16T11:39:43Z

z3rro/src/prover.rs

+                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") {


This looks strange and at least requires a comment why that's here.

Philipp15b · 2025-05-16T11:40:42Z

z3rro/src/prover.rs

+                } else {
+                    Err(ProverCommandError::ParseError)
+                }
+            } else {


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.

Philipp15b · 2025-05-16T11:42:27Z

z3rro/src/prover.rs

+    let mut input_buffer: VecDeque<char> = input.chars().collect();
+    let mut cnt = 0;
+
+    while let Some(c) = input_buffer.pop_front() {


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.

Philipp15b · 2025-05-16T11:43:15Z

z3rro/src/prover.rs

        self.min_level_with_provables.get_or_insert(self.level);
    }
-
+    


Be sure to have your editor automatically remove trailing spaces. cargo fmt --all should remove these as well, I think.

Philipp15b · 2025-05-16T11:49:51Z

z3rro/src/prover.rs

+                }
+            }
+            SolverType::Z3 => {
+                let res = match &self.last_result {


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.

Philipp15b · 2025-05-16T11:51:52Z

z3rro/src/test.rs

-        ProveResult::Proof => {}
+        Ok(ProveResult::Unknown(reason)) => panic!("solver returned unknown ({})", reason),
+        Ok(ProveResult::Proof) => {},
+        Err(_) => {}


why is the error here silently ignored?

Philipp15b · 2025-05-16T11:52:22Z

z3rro/Cargo.toml

 im-rc = "15"
 enum-map = "2.7.3"
 itertools = "0.14.0"
+smtlib-lowlevel = "0.3.0"


Are we using this still?

Philipp15b · 2025-05-16T15:02:45Z

W.r.t. the "the Err-variant returned from this function is very large" clippy error, I've fixed those on the main branch just now (f8776cb). The other CI errors seem to come from this PR.

Philipp15b · 2025-07-30T14:38:10Z

src/slicing/solver.rs

-        prover.add_assumption(&at_most_n_true);
+        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),


I'd have the function at_most_k take a SolverType parameter, and have it do the decision of whether to call Bool::pb_le or your own at_most_k implementation.

Philipp15b · 2025-07-30T14:39:25Z

src/slicing/solver.rs

-                        ProveResult::Counterexample | ProveResult::Unknown(_) => None,
-                    }
-                });
+                let res_seed = match check_proof_seed(&all_variables, prover, limits_ref, &seed) {


Wait, I don't think this is the same behavior! shrink_block_unsat should call check_proof_seed as before!

Philipp15b · 2025-07-30T14:39:46Z

src/slicing/solver.rs

-                        ProveResult::Proof | ProveResult::Unknown(_) => false,
-                    }
-                });
+                let res_seed = match check_proof_seed(&all_variables, prover, limits_ref, &seed) {


Same as before, this is not the same behavior!

Philipp15b · 2025-07-31T14:18:15Z

z3rro/src/prover.rs

        Smtlib::from_solver(self.get_solver())
    }
+
+    pub fn get_smt_solver(&self) -> SolverType {


This should be named get_solver_type

Implement execution of swine-z3 on SMT2 files

2e50b5a

Philipp15b requested changes Feb 12, 2025

View reviewed changes

SeRin-Yang added 13 commits February 24, 2025 19:28

Add SolverType and CommandError enums, update execute_swine and check…

57c4725

…_proof_assuming functions

No functional changes

9b6388a

Execute swine directly in the command line

9120d44

Add SolverType attribute to Prover struct and SMT solver options

9a0db09

Update check_proof_assuming to return Result for error handling

6197986

Implement AST evaluation functions for Bool, Int, Real types

854e42c

Add swine execution via spawn and parse output into CheckSatResponse …

793a281

…and GetModelResponse

Move code of eval_ast_bool/int/real into SmtEval::eval

ae52982

Change return type of from_str_to_num_den from (String, String) to (B…

3a41142

…igInt, BigInt)

Parse counterexample from swine via solver.from_string

35b0ef4

Compare SAT result from swine with 'sat'/'unsat'; return full swine o…

9f44e21

…utput as reason if unknown

Add Cargo.lock file

bc17f1c

Merge main of moves-rwth/caesar and resolve conflicts

ecb9d86

Philipp15b requested changes May 16, 2025

View reviewed changes

SeRin-Yang added 13 commits May 16, 2025 20:09

Merge remote-tracking branch 'moves-rwth/main'

70f7b1d

minor changes

4289373

Remove leftover code

f07c8b7

Add check-sat-assuming command for given assumptions

4af6885

Add docs for add_check_sat_assuming and add_details_query

ecfad75

Add SolverResult enum

c5464de

Apply the same logic to the SWINE call

aaf9c52

Implement check_sat for each SolverType (not working correctly)

b5325b8

Fix missing sat check after adding assertions

fe830be

Remove print statements used for functon call tracking

7709717

Add SMTLIB(String) option to SMTSolverType and SolverType enums

6d4259d

no functional change

10b522e

Add CVC5 option to SMTSolverType and SolverType enums

7f4f5b3

SeRin-Yang added 8 commits July 4, 2025 22:00

Fix: skip at-most conversion for non-CVC5 solvers

eeac38e

Remove SMTLIB option from SMTSolverType and SolverType enums

2787eba

Add at_most_k, at_least_k functions

b33d3b3

Clean up unused code

d108056

Clean up unused code

4f7155d

Restore block_at_least function to original implementation

2b5c5ad

Add SolverType ExternalZ3 and rename SolverType Z3 to InternalZ3

b42f210

Add SolverType Yices

21936b1

Philipp15b reviewed Jul 30, 2025

View reviewed changes

Add timeout setting for external SMT solvers

c1cbaf3

Philipp15b reviewed Jul 31, 2025

View reviewed changes

SeRin-Yang added 7 commits August 1, 2025 11:24

Change SolverResult::Sat to store a real solver instead of a string

077338d

Change solver handling back to match original behavior

39ffe52

Add SolverType parameter to at_most_k

98b84e8

Rename function to get_solver_type

718554a

Make SolverResult independent from lifetime 'ctx' to fix E0499 error

308846f

Code formatting

3a3e33f

Add result_solver to Prover for external solver output

50b1814

Conversation

SeRin-Yang commented Feb 11, 2025

Uh oh!

Philipp15b left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Philipp15b commented May 16, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Philipp15b commented May 16, 2025 •

edited

Loading