Move parser configuration to separate struct

carcara/src/ast/iter.rs

@@ -28,7 +28,7 @@ use super::*;
 ///     (step t5 (cl) :rule resolution :premises (t4 h1 h2))
 /// "
 /// .as_bytes();
-/// let (_, proof, _) : (ast::ProblemPrelude, ast::Proof, ast::pool::PrimitivePool) = parser::parse_instance("".as_bytes(), proof, true, false, false)?;
+/// let (_, proof, _) = parser::parse_instance("".as_bytes(), proof, parser::Config::new())?;
 /// let ids: Vec<_> = proof.iter().map(|c| c.id()).collect();
 /// assert_eq!(ids, ["h1", "h2", "t3", "t3.t1", "t3.t2", "t3", "t4", "t5"]);
 /// # Ok(())

carcara/src/ast/macros.rs

@@ -32,7 +32,7 @@
 /// # use carcara::{ast::*, match_term, parser::*};
 /// # pub fn parse_term(input: &str) -> Rc<Term> {
 /// #     let mut pool = PrimitivePool::new();
-/// #     let mut parser = Parser::new(&mut pool, input.as_bytes(), true, false, false).unwrap();
+/// #     let mut parser = Parser::new(&mut pool, Config::new(), input.as_bytes()).unwrap();
 /// #     parser.parse_term().unwrap()
 /// # }
 /// # let t = parse_term("(and (=> false false) (> (+ 0 0) 0))");
@@ -52,7 +52,7 @@
 /// # use carcara::{ast::*, match_term, parser::*};
 /// # pub fn parse_term(input: &str) -> Rc<Term> {
 /// #     let mut pool = PrimitivePool::new();
-/// #     let mut parser = Parser::new(&mut pool, input.as_bytes(), true, false, false).unwrap();
+/// #     let mut parser = Parser::new(&mut pool, Config::new(), input.as_bytes()).unwrap();
 /// #     parser.parse_term().unwrap()
 /// # }
 /// # let t = parse_term("(forall ((x Int) (y Int)) (> x y))");

carcara/src/ast/substitution.rs

@@ -357,8 +357,7 @@ mod tests {
 
     fn run_test(definitions: &str, original: &str, x: &str, t: &str, result: &str) {
         let mut pool = PrimitivePool::new();
-        let mut parser =
-            Parser::new(&mut pool, definitions.as_bytes(), true, false, false).unwrap();
+        let mut parser = Parser::new(&mut pool, Config::new(), definitions.as_bytes()).unwrap();
         parser.parse_problem().unwrap();
 
         let [original, x, t, result] = [original, x, t, result].map(|s| {

carcara/src/checker/lia_generic.rs

@@ -118,7 +118,7 @@ fn parse_and_check_solver_proof(
     problem: &[u8],
     proof: &[u8],
 ) -> CarcaraResult<Vec<ProofCommand>> {
-    let mut parser = parser::Parser::new(pool, problem, true, false, true)?;
+    let mut parser = parser::Parser::new(pool, parser::Config::new(), problem)?;
     let (prelude, premises) = parser.parse_problem()?;
     parser.reset(proof)?;
     let commands = parser.parse_proof()?;

carcara/src/checker/rules/mod.rs

@@ -151,20 +151,15 @@ fn assert_is_bool_constant(got: &Rc<Term>, expected: bool) -> RuleResult {
 
 #[cfg(test)]
 fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
-    use crate::{
-        checker::{Config, ProofChecker},
-        parser::parse_instance,
-    };
+    use crate::{checker, parser};
     use std::io::Cursor;
 
     for (i, (proof, expected)) in cases.iter().enumerate() {
         // This parses the definitions again for every case, which is not ideal
-        let (prelude, mut proof, mut pool) = parse_instance(
+        let (prelude, mut proof, mut pool) = parser::parse_instance(
             Cursor::new(definitions),
             Cursor::new(proof),
-            true,
-            false,
-            false,
+            parser::Config::new(),
         )
         .unwrap_or_else(|e| panic!("parser error during test \"{}\": {}", test_name, e));
 
@@ -191,7 +186,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
             discharge: Vec::new(),
         }));
 
-        let mut checker = ProofChecker::new(&mut pool, Config::new(), &prelude);
+        let mut checker = checker::ProofChecker::new(&mut pool, checker::Config::new(), &prelude);
         let got = checker.check(&proof).is_ok();
         assert_eq!(
             *expected, got,

carcara/src/lib.rs

@@ -152,13 +152,12 @@ pub fn check<T: io::BufRead>(problem: T, proof: T, options: CarcaraOptions) -> R
 
     // Parsing
     let total = Instant::now();
-    let (prelude, proof, mut pool) = parser::parse_instance(
-        problem,
-        proof,
-        options.apply_function_defs,
-        options.expand_lets,
-        options.allow_int_real_subtyping,
-    )?;
+    let config = parser::Config {
+        apply_function_defs: options.apply_function_defs,
+        expand_lets: options.expand_lets,
+        allow_int_real_subtyping: options.allow_int_real_subtyping,
+    };
+    let (prelude, proof, mut pool) = parser::parse_instance(problem, proof, config)?;
     run_measures.parsing = total.elapsed();
 
     let config = checker::Config::new()
@@ -218,13 +217,12 @@ pub fn check_parallel<T: io::BufRead>(
 
     // Parsing
     let total = Instant::now();
-    let (prelude, proof, pool) = parser::parse_instance(
-        problem,
-        proof,
-        options.apply_function_defs,
-        options.expand_lets,
-        options.allow_int_real_subtyping,
-    )?;
+    let config = parser::Config {
+        apply_function_defs: options.apply_function_defs,
+        expand_lets: options.expand_lets,
+        allow_int_real_subtyping: options.allow_int_real_subtyping,
+    };
+    let (prelude, proof, pool) = parser::parse_instance(problem, proof, config)?;
     run_measures.parsing = total.elapsed();
 
     let config = checker::Config::new()
@@ -289,13 +287,12 @@ pub fn check_and_elaborate<T: io::BufRead>(
 
     // Parsing
     let total = Instant::now();
-    let (prelude, proof, mut pool) = parser::parse_instance(
-        problem,
-        proof,
-        options.apply_function_defs,
-        options.expand_lets,
-        options.allow_int_real_subtyping,
-    )?;
+    let config = parser::Config {
+        apply_function_defs: options.apply_function_defs,
+        expand_lets: options.expand_lets,
+        allow_int_real_subtyping: options.allow_int_real_subtyping,
+    };
+    let (prelude, proof, mut pool) = parser::parse_instance(problem, proof, config)?;
     run_measures.parsing = total.elapsed();
 
     let config = checker::Config::new()

carcara/src/parser/mod.rs

@@ -17,6 +17,19 @@ use error::assert_num_args;
 use rug::Integer;
 use std::{io::BufRead, str::FromStr};
 
+#[derive(Debug, Default, Clone, Copy)]
+pub struct Config {
+    pub apply_function_defs: bool,
+    pub expand_lets: bool,
+    pub allow_int_real_subtyping: bool,
+}
+
+impl Config {
+    pub fn new() -> Self {
+        Self::default()
+    }
+}
+
 /// Parses an SMT problem instance (in the SMT-LIB format) and its associated proof (in the Alethe
 /// format).
 ///
@@ -25,18 +38,10 @@ use std::{io::BufRead, str::FromStr};
 pub fn parse_instance<T: BufRead>(
     problem: T,
     proof: T,
-    apply_function_defs: bool,
-    expand_lets: bool,
-    allow_int_real_subtyping: bool,
+    config: Config,
 ) -> CarcaraResult<(ProblemPrelude, Proof, PrimitivePool)> {
     let mut pool = PrimitivePool::new();
-    let mut parser = Parser::new(
-        &mut pool,
-        problem,
-        apply_function_defs,
-        expand_lets,
-        allow_int_real_subtyping,
-    )?;
+    let mut parser = Parser::new(&mut pool, config, problem)?;
     let (prelude, premises) = parser.parse_problem()?;
     parser.reset(proof)?;
     let commands = parser.parse_proof()?;
@@ -81,28 +86,20 @@ struct ParserState {
 /// A parser for the Alethe proof format.
 pub struct Parser<'a, R> {
     pool: &'a mut PrimitivePool,
+    config: Config,
     lexer: Lexer<R>,
     current_token: Token,
     current_position: Position,
     state: ParserState,
     interpret_integers_as_reals: bool,
-    apply_function_defs: bool,
-    expand_lets: bool,
     problem: Option<(ProblemPrelude, AHashSet<Rc<Term>>)>,
-    allow_int_real_subtyping: bool,
 }
 
 impl<'a, R: BufRead> Parser<'a, R> {
     /// Constructs a new `Parser` from a type that implements `BufRead`.
     ///
     /// This operation can fail if there is an IO or lexer error on the first token.
-    pub fn new(
-        pool: &'a mut PrimitivePool,
-        input: R,
-        apply_function_defs: bool,
-        expand_lets: bool,
-        allow_int_real_subtyping: bool,
-    ) -> CarcaraResult<Self> {
+    pub fn new(pool: &'a mut PrimitivePool, config: Config, input: R) -> CarcaraResult<Self> {
         let mut state = ParserState::default();
         let bool_sort = pool.add(Term::Sort(Sort::Bool));
         for iden in ["true", "false"] {
@@ -113,15 +110,13 @@ impl<'a, R: BufRead> Parser<'a, R> {
         let (current_token, current_position) = lexer.next_token()?;
         Ok(Parser {
             pool,
+            config,
             lexer,
             current_token,
             current_position,
             state,
             interpret_integers_as_reals: false,
-            apply_function_defs,
-            expand_lets,
             problem: None,
-            allow_int_real_subtyping,
         })
     }
 
@@ -219,7 +214,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
 
                 // All the arguments must be either Int or Real. Also, if we are not allowing
                 // Int/Real subtyping, all arguments must have the same sort
-                if self.allow_int_real_subtyping {
+                if self.config.allow_int_real_subtyping {
                     for s in sorts {
                         SortError::assert_one_of(&[Sort::Int, Sort::Real], s.as_sort().unwrap())?;
                     }
@@ -251,7 +246,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
 
                 // Normally, the `/` operator may only receive Real arguments, but if we are
                 // allowing Int/Real subtyping, it may also receive Ints
-                if self.allow_int_real_subtyping {
+                if self.config.allow_int_real_subtyping {
                     for s in sorts {
                         SortError::assert_one_of(&[Sort::Int, Sort::Real], s.as_sort().unwrap())?;
                     }
@@ -528,7 +523,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
                 Token::ReservedWord(Reserved::DefineFun) => {
                     let (name, func_def) = self.parse_define_fun()?;
 
-                    if self.apply_function_defs {
+                    if self.config.apply_function_defs {
                         self.state.function_defs.insert(name, func_def);
                     } else {
                         // If `self.apply_function_defs` is false, we instead add the function name
@@ -1061,7 +1056,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
         self.expect_token(Token::CloseParen)?;
         self.state.symbol_table.pop_scope();
 
-        if self.expand_lets {
+        if self.config.expand_lets {
             let substitution = bindings
                 .into_iter()
                 .map(|(name, value)| {

carcara/src/parser/tests.rs

@@ -7,13 +7,19 @@ use crate::ast::pool::PrimitivePool;
 
 const ERROR_MESSAGE: &str = "parser error during test";
 
+const TEST_CONFIG: Config = Config {
+    // Some tests need function definitions to be applied
+    apply_function_defs: true,
+    expand_lets: false,
+    allow_int_real_subtyping: false,
+};
+
 pub fn parse_terms<const N: usize>(
     pool: &mut PrimitivePool,
     definitions: &str,
     terms: [&str; N],
 ) -> [Rc<Term>; N] {
-    let mut parser =
-        Parser::new(pool, definitions.as_bytes(), true, false, false).expect(ERROR_MESSAGE);
+    let mut parser = Parser::new(pool, TEST_CONFIG, definitions.as_bytes()).expect(ERROR_MESSAGE);
     parser.parse_problem().expect(ERROR_MESSAGE);
 
     terms.map(|s| {
@@ -23,7 +29,7 @@ pub fn parse_terms<const N: usize>(
 }
 
 pub fn parse_term(pool: &mut PrimitivePool, input: &str) -> Rc<Term> {
-    Parser::new(pool, input.as_bytes(), true, false, false)
+    Parser::new(pool, TEST_CONFIG, input.as_bytes())
         .and_then(|mut parser| parser.parse_term())
         .expect(ERROR_MESSAGE)
 }
@@ -32,14 +38,14 @@ pub fn parse_term(pool: &mut PrimitivePool, input: &str) -> Rc<Term> {
 /// panics if no error is encountered.
 pub fn parse_term_err(input: &str) -> Error {
     let mut pool = PrimitivePool::new();
-    Parser::new(&mut pool, input.as_bytes(), true, false, false)
+    Parser::new(&mut pool, TEST_CONFIG, input.as_bytes())
         .and_then(|mut p| p.parse_term())
         .expect_err("expected error")
 }
 
 /// Parses a proof from a `&str`. Panics if any error is encountered.
 pub fn parse_proof(pool: &mut PrimitivePool, input: &str) -> Proof {
-    let commands = Parser::new(pool, input.as_bytes(), true, false, false)
+    let commands = Parser::new(pool, TEST_CONFIG, input.as_bytes())
         .expect(ERROR_MESSAGE)
         .parse_proof()
         .expect(ERROR_MESSAGE);
@@ -65,7 +71,7 @@ fn test_hash_consing() {
         )
         (* 2 2)
     )";
-    let mut parser = Parser::new(&mut pool, input.as_bytes(), true, false, false).unwrap();
+    let mut parser = Parser::new(&mut pool, Config::new(), input.as_bytes()).unwrap();
     parser.parse_term().unwrap();
 
     // We expect this input to result in 7 unique terms after parsing:

carcara/tests/test_example_files.rs

@@ -15,9 +15,7 @@ fn run_parallel_checker_test(
     let (prelude, proof, pool) = parser::parse_instance(
         io::BufReader::new(fs::File::open(problem_path)?),
         io::BufReader::new(fs::File::open(proof_path)?),
-        false,
-        false,
-        false,
+        parser::Config::new(),
     )?;
 
     let (scheduler, schedule_context_usage) = checker::Scheduler::new(num_threads, &proof);
@@ -38,9 +36,7 @@ fn run_test(problem_path: &Path, proof_path: &Path) -> CarcaraResult<()> {
     let (prelude, proof, mut pool) = parser::parse_instance(
         io::BufReader::new(fs::File::open(problem_path)?),
         io::BufReader::new(fs::File::open(proof_path)?),
-        true,
-        false,
-        false,
+        parser::Config::new(),
     )?;
 
     // First, we check the proof normally

cli/src/benchmarking.rs

@@ -1,8 +1,6 @@
 use carcara::{
     benchmarking::{CollectResults, CsvBenchmarkResults, RunMeasurement},
-    checker,
-    parser::parse_instance,
-    CarcaraOptions,
+    checker, parser, CarcaraOptions,
 };
 use crossbeam_queue::ArrayQueue;
 use std::{
@@ -39,12 +37,15 @@ fn run_job<T: CollectResults + Default + Send>(
     let total = Instant::now();
 
     let parsing = Instant::now();
-    let (prelude, proof, mut pool) = parse_instance(
+    let config = parser::Config {
+        apply_function_defs: options.apply_function_defs,
+        expand_lets: options.expand_lets,
+        allow_int_real_subtyping: options.allow_int_real_subtyping,
+    };
+    let (prelude, proof, mut pool) = parser::parse_instance(
         BufReader::new(File::open(job.problem_file)?),
         BufReader::new(File::open(job.proof_file)?),
-        options.apply_function_defs,
-        options.expand_lets,
-        options.allow_int_real_subtyping,
+        config,
     )?;
     let parsing = parsing.elapsed();