From bd2d55a8e2f2238853195528691c003551b92f6a Mon Sep 17 00:00:00 2001 From: Bruno Andreotti Date: Tue, 8 Aug 2023 15:34:53 -0300 Subject: [PATCH] Allow user to choose solver binary for `lia_generic` --- carcara/src/checker/error.rs | 28 +++++++-------- carcara/src/checker/lia_generic.rs | 53 ++++++++++++++++------------- carcara/src/checker/mod.rs | 9 ++--- carcara/src/checker/parallel/mod.rs | 5 +-- carcara/src/checker/rules/mod.rs | 2 +- carcara/src/lib.rs | 17 ++++----- cli/src/benchmarking.rs | 2 +- cli/src/main.rs | 25 ++++++++++++-- 8 files changed, 85 insertions(+), 56 deletions(-) diff --git a/carcara/src/checker/error.rs b/carcara/src/checker/error.rs index 45996332..d791aa6c 100644 --- a/carcara/src/checker/error.rs +++ b/carcara/src/checker/error.rs @@ -248,29 +248,29 @@ pub enum LinearArithmeticError { #[derive(Debug, Error)] pub enum LiaGenericError { - #[error("failed to spawn cvc5 process")] - FailedSpawnCvc5(io::Error), + #[error("failed to spawn solver process")] + FailedSpawnSolver(io::Error), - #[error("failed to write to cvc5 stdin")] - FailedWriteToCvc5Stdin(io::Error), + #[error("failed to write to solver stdin")] + FailedWriteToSolverStdin(io::Error), - #[error("error while waiting for cvc5 to exit")] - FailedWaitForCvc5(io::Error), + #[error("error while waiting for solver to exit")] + FailedWaitForSolver(io::Error), - #[error("cvc5 gave invalid output")] - Cvc5GaveInvalidOutput, + #[error("solver gave invalid output")] + SolverGaveInvalidOutput, - #[error("cvc5 output not unsat")] - Cvc5OutputNotUnsat, + #[error("solver output not unsat")] + OutputNotUnsat, - #[error("cvc5 timed out when solving problem")] - Cvc5Timeout, + #[error("solver timed out when solving problem")] + SolverTimeout, #[error( - "cvc5 returned non-zero exit code: {}", + "solver returned non-zero exit code: {}", if let Some(i) = .0 { format!("{}", i) } else { "none".to_owned() } )] - Cvc5NonZeroExitCode(Option), + NonZeroExitCode(Option), #[error("error in inner proof: {0}")] InnerProofError(Box), diff --git a/carcara/src/checker/lia_generic.rs b/carcara/src/checker/lia_generic.rs index d91d96b7..cdcc1ae2 100644 --- a/carcara/src/checker/lia_generic.rs +++ b/carcara/src/checker/lia_generic.rs @@ -30,12 +30,13 @@ pub fn lia_generic_single_thread( prelude: &ProblemPrelude, elaborator: Option<&mut Elaborator>, root_id: &str, + solver: &str, ) -> bool { let problem = get_problem_string(conclusion, prelude); - let commands = match get_cvc5_proof(pool, problem) { + let commands = match get_solver_proof(pool, problem, solver) { Ok(c) => c, Err(e) => { - log::warn!("failed to check `lia_generic` step using cvc5: {}", e); + log::warn!("failed to check `lia_generic` step: {}", e); if let Some(elaborator) = elaborator { elaborator.unchanged(conclusion); } @@ -44,27 +45,32 @@ pub fn lia_generic_single_thread( }; if let Some(elaborator) = elaborator { - insert_cvc5_proof(pool, elaborator, commands, conclusion, root_id); + insert_solver_proof(pool, elaborator, commands, conclusion, root_id); } false } -pub fn lia_generic_multi_thread(conclusion: &[Rc], prelude: &ProblemPrelude) -> bool { +pub fn lia_generic_multi_thread( + conclusion: &[Rc], + prelude: &ProblemPrelude, + solver: &str, +) -> bool { let mut pool = PrimitivePool::new(); let problem = get_problem_string(conclusion, prelude); - if let Err(e) = get_cvc5_proof(&mut pool, problem) { - log::warn!("failed to check `lia_generic` step using cvc5: {}", e); + if let Err(e) = get_solver_proof(&mut pool, problem, solver) { + log::warn!("failed to check `lia_generic` step using: {}", e); true } else { false } } -fn get_cvc5_proof( +fn get_solver_proof( pool: &mut PrimitivePool, problem: String, + solver: &str, ) -> Result, LiaGenericError> { - let mut cvc5 = Command::new("cvc5") + let mut process = Command::new(solver) .args([ "--tlimit=10000", "--lang=smt2", @@ -76,25 +82,26 @@ fn get_cvc5_proof( .stdout(Stdio::piped()) .stderr(Stdio::piped()) .spawn() - .map_err(LiaGenericError::FailedSpawnCvc5)?; + .map_err(LiaGenericError::FailedSpawnSolver)?; - cvc5.stdin + process + .stdin .take() - .expect("failed to open cvc5 stdin") + .expect("failed to open solver stdin") .write_all(problem.as_bytes()) - .map_err(LiaGenericError::FailedWriteToCvc5Stdin)?; + .map_err(LiaGenericError::FailedWriteToSolverStdin)?; - let output = cvc5 + let output = process .wait_with_output() - .map_err(LiaGenericError::FailedWaitForCvc5)?; + .map_err(LiaGenericError::FailedWaitForSolver)?; if !output.status.success() { if let Ok(s) = std::str::from_utf8(&output.stderr) { - if s.contains("cvc5 interrupted by timeout.") { - return Err(LiaGenericError::Cvc5Timeout); + if s.contains("interrupted by timeout.") { + return Err(LiaGenericError::SolverTimeout); } } - return Err(LiaGenericError::Cvc5NonZeroExitCode(output.status.code())); + return Err(LiaGenericError::NonZeroExitCode(output.status.code())); } let mut proof = output.stdout.as_slice(); @@ -102,17 +109,17 @@ fn get_cvc5_proof( proof .read_line(&mut first_line) - .map_err(|_| LiaGenericError::Cvc5GaveInvalidOutput)?; + .map_err(|_| LiaGenericError::SolverGaveInvalidOutput)?; if first_line.trim_end() != "unsat" { - return Err(LiaGenericError::Cvc5OutputNotUnsat); + return Err(LiaGenericError::OutputNotUnsat); } - parse_and_check_cvc5_proof(pool, problem.as_bytes(), proof) + parse_and_check_solver_proof(pool, problem.as_bytes(), proof) .map_err(|e| LiaGenericError::InnerProofError(Box::new(e))) } -fn parse_and_check_cvc5_proof( +fn parse_and_check_solver_proof( pool: &mut PrimitivePool, problem: &[u8], proof: &[u8], @@ -190,7 +197,7 @@ fn insert_missing_assumes( (all, num_added) } -fn insert_cvc5_proof( +fn insert_solver_proof( pool: &mut PrimitivePool, elaborator: &mut Elaborator, mut commands: Vec, @@ -206,7 +213,7 @@ fn insert_cvc5_proof( conclusion, &commands, // This is a bit ugly, but we have to add the ".added" to avoid colliding with the first few - // steps in the cvc5 proof + // steps in the solver proof &format!("{}.added", root_id), ); diff --git a/carcara/src/checker/mod.rs b/carcara/src/checker/mod.rs index 97c6e259..acefd30c 100644 --- a/carcara/src/checker/mod.rs +++ b/carcara/src/checker/mod.rs @@ -50,7 +50,7 @@ pub struct Config { strict: bool, skip_unknown_rules: bool, is_running_test: bool, - lia_via_cvc5: bool, + lia_solver: Option>, } impl Config { @@ -68,8 +68,8 @@ impl Config { self } - pub fn lia_via_cvc5(mut self, value: bool) -> Self { - self.lia_via_cvc5 = value; + pub fn lia_solver(mut self, value: impl Into>>) -> Self { + self.lia_solver = value.into(); self } } @@ -340,13 +340,14 @@ impl<'c> ProofChecker<'c> { let mut elaborated = false; if step.rule == "lia_generic" { - if self.config.lia_via_cvc5 { + if let Some(solver) = &self.config.lia_solver { let is_hole = lia_generic::lia_generic_single_thread( self.pool, &step.clause, self.prelude, self.elaborator.as_mut(), &step.id, + solver, ); self.is_holey = self.is_holey || is_hole; elaborated = self.elaborator.is_some(); diff --git a/carcara/src/checker/parallel/mod.rs b/carcara/src/checker/parallel/mod.rs index e774d3d3..d47024af 100644 --- a/carcara/src/checker/parallel/mod.rs +++ b/carcara/src/checker/parallel/mod.rs @@ -422,8 +422,9 @@ impl<'c> ParallelProofChecker<'c> { let mut polyeq_time = Duration::ZERO; if step.rule == "lia_generic" { - if self.config.lia_via_cvc5 { - let is_hole = lia_generic::lia_generic_multi_thread(&step.clause, self.prelude); + if let Some(solver) = &self.config.lia_solver { + let is_hole = + lia_generic::lia_generic_multi_thread(&step.clause, self.prelude, solver); self.is_holey = self.is_holey || is_hole; } else { log::warn!("encountered \"lia_generic\" rule, ignoring"); diff --git a/carcara/src/checker/rules/mod.rs b/carcara/src/checker/rules/mod.rs index 7c9ba2fa..3ed77fe4 100644 --- a/carcara/src/checker/rules/mod.rs +++ b/carcara/src/checker/rules/mod.rs @@ -173,7 +173,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) { strict: false, skip_unknown_rules: false, is_running_test: true, - lia_via_cvc5: false, + lia_solver: None, }, &prelude, ); diff --git a/carcara/src/lib.rs b/carcara/src/lib.rs index f8bc7304..ee450569 100644 --- a/carcara/src/lib.rs +++ b/carcara/src/lib.rs @@ -72,11 +72,12 @@ pub struct CarcaraOptions { /// to a function that expects a `Real` will still be an error. pub allow_int_real_subtyping: bool, - /// Enable checking/elaboration of `lia_generic` steps using cvc5. When checking a proof, this - /// will call cvc5 to solve the linear integer arithmetic problem, check the proof, and discard - /// it. When elaborating, the proof will instead be inserted in the place of the `lia_generic` - /// step. - pub lia_via_cvc5: bool, + /// Enable checking/elaboration of `lia_generic` steps using the given solver. When checking a + /// proof, this will call the solver to solve the linear integer arithmetic problem, check the + /// proof, and discard it. When elaborating, the proof will instead be inserted in the place of + /// the `lia_generic` step. The solver should be a binary that can read SMT-LIB from stdin and + /// output an Alethe proof from stdout. + pub lia_solver: Option>, /// Enables "strict" checking of some rules. /// @@ -152,7 +153,7 @@ pub fn check(problem: T, proof: T, options: CarcaraOptions) -> R let config = checker::Config::new() .strict(options.strict) .skip_unknown_rules(options.skip_unknown_rules) - .lia_via_cvc5(options.lia_via_cvc5); + .lia_solver(options.lia_solver); // Checking let checking = Instant::now(); @@ -218,7 +219,7 @@ pub fn check_parallel( let config = checker::Config::new() .strict(options.strict) .skip_unknown_rules(options.skip_unknown_rules) - .lia_via_cvc5(options.lia_via_cvc5); + .lia_solver(options.lia_solver); // Checking let checking = Instant::now(); @@ -289,7 +290,7 @@ pub fn check_and_elaborate( let config = checker::Config::new() .strict(options.strict) .skip_unknown_rules(options.skip_unknown_rules) - .lia_via_cvc5(options.lia_via_cvc5); + .lia_solver(options.lia_solver); // Checking let checking = Instant::now(); diff --git a/cli/src/benchmarking.rs b/cli/src/benchmarking.rs index c4752803..89410766 100644 --- a/cli/src/benchmarking.rs +++ b/cli/src/benchmarking.rs @@ -51,7 +51,7 @@ fn run_job( let config = checker::Config::new() .strict(options.strict) .skip_unknown_rules(options.skip_unknown_rules) - .lia_via_cvc5(options.lia_via_cvc5); + .lia_solver(options.lia_solver.clone()); let mut checker = checker::ProofChecker::new(&mut pool, config, &prelude); let checking = Instant::now(); diff --git a/cli/src/main.rs b/cli/src/main.rs index d9c3e38f..6195c2f1 100644 --- a/cli/src/main.rs +++ b/cli/src/main.rs @@ -117,7 +117,7 @@ struct ParsingOptions { allow_int_real_subtyping: bool, } -#[derive(Args, Clone, Copy)] +#[derive(Args, Clone)] struct CheckingOptions { /// Enables the strict checking of certain rules. #[clap(short, long)] @@ -127,8 +127,12 @@ struct CheckingOptions { #[clap(long)] skip_unknown_rules: bool, - /// Check `lia_generic` steps by calling into cvc5. + /// Check `lia_generic` steps using the provided solver. #[clap(long)] + lia_solver: Option, + + /// Check `lia_generic` steps by calling into cvc5 (deprecated). + #[clap(long, conflicts_with("lia-solver"))] lia_via_cvc5: bool, } @@ -148,15 +152,21 @@ fn build_carcara_options( CheckingOptions { strict, skip_unknown_rules, + lia_solver, lia_via_cvc5, }: CheckingOptions, StatsOptions { stats }: StatsOptions, ) -> CarcaraOptions { + // If no solver is provided by the `--lia-solver` option, *and* the `--lia-via-cvc5` option was + // passed, we default to cvc5 as a solver + let lia_solver = lia_solver + .map(Into::into) + .or_else(|| lia_via_cvc5.then(|| "cvc5".into())); CarcaraOptions { apply_function_defs, expand_lets: expand_let_bindings, allow_int_real_subtyping, - lia_via_cvc5, + lia_solver, strict, skip_unknown_rules, stats, @@ -301,6 +311,15 @@ fn main() { let colors_enabled = !cli.no_color && atty::is(atty::Stream::Stderr); logger::init(cli.log_level.into(), colors_enabled); + if let Command::Check(CheckCommandOptions { checking, .. }) + | Command::Elaborate(ElaborateCommandOptions { checking, .. }) + | Command::Bench(BenchCommandOptions { checking, .. }) = &cli.command + { + if checking.lia_via_cvc5 { + log::warn!("`--lia-via-cvc5` option is deprecated, please use `--lia-solver cvc5`") + } + } + let result = match cli.command { Command::Parse(options) => parse_command(options), Command::Check(options) => {