From de1e65485f9d63704564216dbe5c6c0a1e34ed26 Mon Sep 17 00:00:00 2001 From: Bruno Andreotti Date: Mon, 14 Aug 2023 12:15:42 -0300 Subject: [PATCH] Move parser configuration to separate struct --- carcara/src/ast/iter.rs | 2 +- carcara/src/ast/macros.rs | 4 +-- carcara/src/ast/substitution.rs | 3 +- carcara/src/checker/lia_generic.rs | 2 +- carcara/src/checker/rules/mod.rs | 13 +++----- carcara/src/lib.rs | 39 +++++++++++------------ carcara/src/parser/mod.rs | 49 +++++++++++++---------------- carcara/src/parser/tests.rs | 18 +++++++---- carcara/tests/test_example_files.rs | 8 ++--- cli/src/benchmarking.rs | 15 ++++----- cli/src/main.rs | 23 +++++++------- 11 files changed, 83 insertions(+), 93 deletions(-) diff --git a/carcara/src/ast/iter.rs b/carcara/src/ast/iter.rs index 46e3e8ac..e3788aab 100644 --- a/carcara/src/ast/iter.rs +++ b/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(()) diff --git a/carcara/src/ast/macros.rs b/carcara/src/ast/macros.rs index ce27a98f..42de35cf 100644 --- a/carcara/src/ast/macros.rs +++ b/carcara/src/ast/macros.rs @@ -32,7 +32,7 @@ /// # use carcara::{ast::*, match_term, parser::*}; /// # pub fn parse_term(input: &str) -> Rc { /// # 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 { /// # 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))"); diff --git a/carcara/src/ast/substitution.rs b/carcara/src/ast/substitution.rs index e3cfd252..ebae8b74 100644 --- a/carcara/src/ast/substitution.rs +++ b/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| { diff --git a/carcara/src/checker/lia_generic.rs b/carcara/src/checker/lia_generic.rs index 0af99983..a13e3cf2 100644 --- a/carcara/src/checker/lia_generic.rs +++ b/carcara/src/checker/lia_generic.rs @@ -118,7 +118,7 @@ fn parse_and_check_solver_proof( problem: &[u8], proof: &[u8], ) -> CarcaraResult> { - 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()?; diff --git a/carcara/src/checker/rules/mod.rs b/carcara/src/checker/rules/mod.rs index 819ad8b9..6ba0962f 100644 --- a/carcara/src/checker/rules/mod.rs +++ b/carcara/src/checker/rules/mod.rs @@ -151,20 +151,15 @@ fn assert_is_bool_constant(got: &Rc, 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, diff --git a/carcara/src/lib.rs b/carcara/src/lib.rs index ae82f6f7..8134198a 100644 --- a/carcara/src/lib.rs +++ b/carcara/src/lib.rs @@ -152,13 +152,12 @@ pub fn check(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( // 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( // 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() diff --git a/carcara/src/parser/mod.rs b/carcara/src/parser/mod.rs index a09feb79..240c224d 100644 --- a/carcara/src/parser/mod.rs +++ b/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( 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, current_token: Token, current_position: Position, state: ParserState, interpret_integers_as_reals: bool, - apply_function_defs: bool, - expand_lets: bool, problem: Option<(ProblemPrelude, AHashSet>)>, - 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 { + pub fn new(pool: &'a mut PrimitivePool, config: Config, input: R) -> CarcaraResult { 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)| { diff --git a/carcara/src/parser/tests.rs b/carcara/src/parser/tests.rs index c2ba06bf..1cc4bac0 100644 --- a/carcara/src/parser/tests.rs +++ b/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( pool: &mut PrimitivePool, definitions: &str, terms: [&str; N], ) -> [Rc; 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( } pub fn parse_term(pool: &mut PrimitivePool, input: &str) -> Rc { - 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 { /// 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: diff --git a/carcara/tests/test_example_files.rs b/carcara/tests/test_example_files.rs index 5dfb2366..17385630 100644 --- a/carcara/tests/test_example_files.rs +++ b/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 diff --git a/cli/src/benchmarking.rs b/cli/src/benchmarking.rs index 7ddc3a50..72ba8518 100644 --- a/cli/src/benchmarking.rs +++ b/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( 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(); diff --git a/cli/src/main.rs b/cli/src/main.rs index d2a04727..0c3a3d0b 100644 --- a/cli/src/main.rs +++ b/cli/src/main.rs @@ -379,9 +379,11 @@ fn parse_command(options: ParseCommandOptions) -> CliResult<()> { let (_, proof, _) = parser::parse_instance( problem, proof, - options.parsing.apply_function_defs, - options.parsing.expand_let_bindings, - options.parsing.allow_int_real_subtyping, + parser::Config { + apply_function_defs: options.parsing.apply_function_defs, + expand_lets: options.parsing.expand_let_bindings, + allow_int_real_subtyping: options.parsing.allow_int_real_subtyping, + }, ) .map_err(carcara::Error::from)?; print_proof(&proof.commands, options.printing.use_sharing)?; @@ -473,14 +475,13 @@ fn bench_command(options: BenchCommandOptions) -> CliResult<()> { fn slice_command(options: SliceCommandOption) -> CliResult<()> { let (problem, proof) = get_instance(&options.input)?; - let (_, proof, _) = parser::parse_instance( - problem, - proof, - options.parsing.apply_function_defs, - options.parsing.expand_let_bindings, - options.parsing.allow_int_real_subtyping, - ) - .map_err(carcara::Error::from)?; + let config = parser::Config { + apply_function_defs: options.parsing.apply_function_defs, + expand_lets: options.parsing.expand_let_bindings, + allow_int_real_subtyping: options.parsing.allow_int_real_subtyping, + }; + let (_, proof, _) = + parser::parse_instance(problem, proof, config).map_err(carcara::Error::from)?; let source_index = proof .commands