Allow user to control solver arguments

carcara/src/checker/lia_generic.rs

@@ -1,5 +1,5 @@
 use super::*;
-use crate::{checker::error::LiaGenericError, parser};
+use crate::{checker::error::LiaGenericError, parser, LiaGenericOptions};
 use ahash::AHashMap;
 use std::{
     io::{BufRead, Write},
@@ -30,10 +30,10 @@ pub fn lia_generic_single_thread(
     prelude: &ProblemPrelude,
     elaborator: Option<&mut Elaborator>,
     root_id: &str,
-    solver: &str,
+    options: &LiaGenericOptions,
 ) -> bool {
     let problem = get_problem_string(conclusion, prelude);
-    let commands = match get_solver_proof(pool, problem, solver) {
+    let commands = match get_solver_proof(pool, problem, options) {
         Ok(c) => c,
         Err(e) => {
             log::warn!("failed to check `lia_generic` step: {}", e);
@@ -53,11 +53,11 @@ pub fn lia_generic_single_thread(
 pub fn lia_generic_multi_thread(
     conclusion: &[Rc<Term>],
     prelude: &ProblemPrelude,
-    solver: &str,
+    options: &LiaGenericOptions,
 ) -> bool {
     let mut pool = PrimitivePool::new();
     let problem = get_problem_string(conclusion, prelude);
-    if let Err(e) = get_solver_proof(&mut pool, problem, solver) {
+    if let Err(e) = get_solver_proof(&mut pool, problem, options) {
         log::warn!("failed to check `lia_generic` step using: {}", e);
         true
     } else {
@@ -68,16 +68,10 @@ pub fn lia_generic_multi_thread(
 fn get_solver_proof(
     pool: &mut PrimitivePool,
     problem: String,
-    solver: &str,
+    options: &LiaGenericOptions,
 ) -> Result<Vec<ProofCommand>, LiaGenericError> {
-    let mut process = Command::new(solver)
-        .args([
-            "--tlimit=10000",
-            "--lang=smt2",
-            "--proof-format-mode=alethe",
-            "--proof-granularity=theory-rewrite",
-            "--proof-alethe-res-pivots",
-        ])
+    let mut process = Command::new(options.solver.as_ref())
+        .args(options.arguments.iter().map(AsRef::as_ref))
         .stdin(Stdio::piped())
         .stdout(Stdio::piped())
         .stderr(Stdio::piped())

carcara/src/checker/mod.rs

@@ -7,7 +7,7 @@ use crate::{
     ast::*,
     benchmarking::{CollectResults, OnlineBenchmarkResults},
     elaborator::Elaborator,
-    CarcaraResult, Error,
+    CarcaraResult, Error, LiaGenericOptions,
 };
 use ahash::AHashSet;
 use error::CheckerError;
@@ -50,7 +50,7 @@ pub struct Config {
     strict: bool,
     skip_unknown_rules: bool,
     is_running_test: bool,
-    lia_solver: Option<Box<str>>,
+    lia_options: Option<LiaGenericOptions>,
 }
 
 impl Config {
@@ -68,8 +68,8 @@ impl Config {
         self
     }
 
-    pub fn lia_solver(mut self, value: impl Into<Option<Box<str>>>) -> Self {
-        self.lia_solver = value.into();
+    pub fn lia_options(mut self, value: impl Into<Option<LiaGenericOptions>>) -> Self {
+        self.lia_options = value.into();
         self
     }
 }
@@ -340,14 +340,14 @@ impl<'c> ProofChecker<'c> {
 
         let mut elaborated = false;
         if step.rule == "lia_generic" {
-            if let Some(solver) = &self.config.lia_solver {
+            if let Some(options) = &self.config.lia_options {
                 let is_hole = lia_generic::lia_generic_single_thread(
                     self.pool,
                     &step.clause,
                     self.prelude,
                     self.elaborator.as_mut(),
                     &step.id,
-                    solver,
+                    options,
                 );
                 self.is_holey = self.is_holey || is_hole;
                 elaborated = self.elaborator.is_some();

carcara/src/checker/parallel/mod.rs

@@ -422,9 +422,9 @@ impl<'c> ParallelProofChecker<'c> {
         let mut polyeq_time = Duration::ZERO;
 
         if step.rule == "lia_generic" {
-            if let Some(solver) = &self.config.lia_solver {
+            if let Some(options) = &self.config.lia_options {
                 let is_hole =
-                    lia_generic::lia_generic_multi_thread(&step.clause, self.prelude, solver);
+                    lia_generic::lia_generic_multi_thread(&step.clause, self.prelude, options);
                 self.is_holey = self.is_holey || is_hole;
             } else {
                 log::warn!("encountered \"lia_generic\" rule, ignoring");

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_solver: None,
+                lia_options: None,
             },
             &prelude,
         );

carcara/src/lib.rs

@@ -72,12 +72,11 @@ 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 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<Box<str>>,
+    /// If `Some`, enables the checking/elaboration of `lia_generic` steps using an external solver.
+    /// When checking a proof, this means calling the solver to solve the linear integer arithmetic
+    /// problem, checking the proof, and discarding it. When elaborating, the proof will instead be
+    /// inserted in the place of the `lia_generic` step. See [`LiaGenericOptions`] for more details.
+    pub lia_options: Option<LiaGenericOptions>,
 
     /// Enables "strict" checking of some rules.
     ///
@@ -99,6 +98,18 @@ pub struct CarcaraOptions {
     pub stats: bool,
 }
 
+/// The options that control how `lia_generic` steps are checked/elaborated using an external
+/// solver.
+#[derive(Debug, Clone)]
+pub struct LiaGenericOptions {
+    /// The external solver path. The solver should be a binary that can read SMT-LIB from stdin and
+    /// output an Alethe proof to stdout.
+    pub solver: Box<str>,
+
+    /// The arguments to pass to the solver.
+    pub arguments: Vec<Box<str>>,
+}
+
 impl CarcaraOptions {
     /// Constructs a new `CarcaraOptions` with all options set to `false`.
     pub fn new() -> Self {
@@ -153,7 +164,7 @@ pub fn check<T: io::BufRead>(problem: T, proof: T, options: CarcaraOptions) -> R
     let config = checker::Config::new()
         .strict(options.strict)
         .skip_unknown_rules(options.skip_unknown_rules)
-        .lia_solver(options.lia_solver);
+        .lia_options(options.lia_options);
 
     // Checking
     let checking = Instant::now();
@@ -219,7 +230,7 @@ pub fn check_parallel<T: io::BufRead>(
     let config = checker::Config::new()
         .strict(options.strict)
         .skip_unknown_rules(options.skip_unknown_rules)
-        .lia_solver(options.lia_solver);
+        .lia_options(options.lia_options);
 
     // Checking
     let checking = Instant::now();
@@ -290,7 +301,7 @@ pub fn check_and_elaborate<T: io::BufRead>(
     let config = checker::Config::new()
         .strict(options.strict)
         .skip_unknown_rules(options.skip_unknown_rules)
-        .lia_solver(options.lia_solver);
+        .lia_options(options.lia_options);
 
     // Checking
     let checking = Instant::now();

cli/src/benchmarking.rs

@@ -51,7 +51,7 @@ fn run_job<T: CollectResults + Default + Send>(
     let config = checker::Config::new()
         .strict(options.strict)
         .skip_unknown_rules(options.skip_unknown_rules)
-        .lia_solver(options.lia_solver.clone());
+        .lia_options(options.lia_options.clone());
     let mut checker = checker::ProofChecker::new(&mut pool, config, &prelude);
 
     let checking = Instant::now();

cli/src/main.rs

@@ -5,7 +5,7 @@ mod path_args;
 
 use carcara::{
     ast::print_proof, benchmarking::OnlineBenchmarkResults, check, check_and_elaborate,
-    check_parallel, parser, CarcaraOptions,
+    check_parallel, parser, CarcaraOptions, LiaGenericOptions,
 };
 use clap::{AppSettings, ArgEnum, Args, Parser, Subcommand};
 use const_format::{formatcp, str_index};
@@ -131,6 +131,16 @@ struct CheckingOptions {
     #[clap(long)]
     lia_solver: Option<String>,
 
+    /// The arguments to pass to the `lia_generic` solver. This should be a single string where
+    /// multiple arguments are separated by spaces.
+    #[clap(
+        long,
+        requires = "lia-solver",
+        allow_hyphen_values = true,
+        default_value = "--tlimit=10000 --lang=smt2 --proof-format-mode=alethe --proof-granularity=theory-rewrite --proof-alethe-res-pivots"
+    )]
+    lia_solver_args: String,
+
     /// Check `lia_generic` steps by calling into cvc5 (deprecated).
     #[clap(long, conflicts_with("lia-solver"))]
     lia_via_cvc5: bool,
@@ -154,19 +164,22 @@ fn build_carcara_options(
         skip_unknown_rules,
         lia_solver,
         lia_via_cvc5,
+        lia_solver_args,
     }: 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()));
+    let solver = lia_solver.or_else(|| lia_via_cvc5.then(|| "cvc5".into()));
+    let lia_options = solver.map(|solver| LiaGenericOptions {
+        solver: solver.into(),
+        arguments: lia_solver_args.split_whitespace().map(Into::into).collect(),
+    });
     CarcaraOptions {
         apply_function_defs,
         expand_lets: expand_let_bindings,
         allow_int_real_subtyping,
-        lia_solver,
+        lia_options,
         strict,
         skip_unknown_rules,
         stats,