Move premises outside Proof and into new Problem struct

carcara/src/ast/mod.rs

@@ -10,6 +10,7 @@ mod node;
 mod polyeq;
 pub mod pool;
 pub(crate) mod printer;
+mod problem;
 mod proof;
 mod rc;
 mod substitution;
@@ -23,25 +24,11 @@ pub use node::{ProofNode, StepNode, SubproofNode};
 pub use polyeq::{alpha_equiv, polyeq, Polyeq, PolyeqComparable, PolyeqConfig};
 pub use pool::{PrimitivePool, TermPool};
 pub use printer::{print_proof, USE_SHARING_IN_TERM_DISPLAY};
+pub use problem::*;
 pub use proof::*;
 pub use rc::Rc;
 pub use substitution::{Substitution, SubstitutionError};
 pub use term::{Binder, BindingList, Constant, Operator, ParamOperator, Sort, SortedVar, Term};
 
 #[cfg(test)]
 pub(crate) use node::compare_nodes;
-
-/// The prelude of an SMT-LIB problem instance.
-///
-/// This stores the sort declarations, function declarations and the problem's logic string.
-#[derive(Debug, Clone, Default)]
-pub struct ProblemPrelude {
-    /// The sort declarations, each represented by its name and arity.
-    pub(crate) sort_declarations: Vec<(String, usize)>,
-
-    /// The function declarations, each represented by its name and body.
-    pub(crate) function_declarations: Vec<(String, Rc<Term>)>,
-
-    /// The problem's logic string, if it exists.
-    pub(crate) logic: Option<String>,
-}

carcara/src/ast/printer.rs

@@ -613,11 +613,11 @@ mod tests {
             (step t6.t1 (cl (= (+ x 2) (+ x 2))) :rule hole)\n\
             (step t6 (cl) :rule hole)\n\
         ";
-        let (prelude, proof, mut pool) =
+        let (problem, proof, mut pool) =
             parser::parse_instance(definitions, proof, parser::Config::new()).unwrap();
 
         let mut buf = Vec::new();
-        AlethePrinter::new(&mut pool, &prelude, true, &mut buf)
+        AlethePrinter::new(&mut pool, &problem.prelude, true, &mut buf)
             .write_proof(&proof)
             .unwrap();
 

carcara/src/ast/problem.rs

@@ -0,0 +1,41 @@
+use super::{Rc, Term};
+use indexmap::IndexSet;
+
+/// An SMT problem in the SMT-LIB format.
+#[derive(Debug, Clone, Default)]
+pub struct Problem {
+    /// The problem's prelude.
+    pub prelude: ProblemPrelude,
+
+    /// The proof's premises.
+    ///
+    /// Those are the terms introduced in the original problem's `assert` commands.
+    pub premises: IndexSet<Rc<Term>>,
+}
+
+impl Problem {
+    pub fn new() -> Self {
+        Self::default()
+    }
+}
+
+/// The prelude of an SMT-LIB problem instance.
+///
+/// This stores the sort declarations, function declarations and the problem's logic string.
+#[derive(Debug, Clone, Default)]
+pub struct ProblemPrelude {
+    /// The sort declarations, each represented by its name and arity.
+    pub(crate) sort_declarations: Vec<(String, usize)>,
+
+    /// The function declarations, each represented by its name and body.
+    pub(crate) function_declarations: Vec<(String, Rc<Term>)>,
+
+    /// The problem's logic string, if it exists.
+    pub(crate) logic: Option<String>,
+}
+
+impl ProblemPrelude {
+    pub fn new() -> Self {
+        Self::default()
+    }
+}

carcara/src/ast/proof.rs

@@ -1,15 +1,9 @@
 use super::{ProofIter, Rc, SortedVar, Term};
 use crate::CheckerError;
-use indexmap::IndexSet;
 
 /// A proof in the Alethe format.
 #[derive(Debug, Clone)]
 pub struct Proof {
-    /// The proof's premises.
-    ///
-    /// Those are the terms introduced in the original problem's `assert` commands.
-    pub premises: IndexSet<Rc<Term>>,
-
     /// The constants defined in the proof using `define-fun` with arity zero.
     ///
     /// This is only used to reconstruct these `define-fun`s when printing the proof.

carcara/src/checker/mod.rs

@@ -95,23 +95,26 @@ impl<'c> ProofChecker<'c> {
         }
     }
 
-    pub fn check(&mut self, proof: &Proof) -> CarcaraResult<bool> {
+    pub fn check(&mut self, problem: &Problem, proof: &Proof) -> CarcaraResult<bool> {
         self.check_impl(
+            problem,
             proof,
             None::<&mut CheckerStatistics<OnlineBenchmarkResults>>,
         )
     }
 
     pub fn check_with_stats<CR: CollectResults + Send + Default>(
         &mut self,
+        problem: &Problem,
         proof: &Proof,
         stats: &mut CheckerStatistics<CR>,
     ) -> CarcaraResult<bool> {
-        self.check_impl(proof, Some(stats))
+        self.check_impl(problem, proof, Some(stats))
     }
 
     fn check_impl<CR: CollectResults + Send + Default>(
         &mut self,
+        problem: &Problem,
         proof: &Proof,
         mut stats: Option<&mut CheckerStatistics<CR>>,
     ) -> CarcaraResult<bool> {
@@ -172,7 +175,7 @@ impl<'c> ProofChecker<'c> {
                     }
                 }
                 ProofCommand::Assume { id, term } => {
-                    if !self.check_assume(id, term, &proof.premises, &iter, &mut stats) {
+                    if !self.check_assume(id, term, &problem.premises, &iter, &mut stats) {
                         return Err(Error::Checker {
                             inner: CheckerError::Assume(term.clone()),
                             rule: "assume".into(),

carcara/src/checker/parallel/mod.rs

@@ -62,7 +62,12 @@ impl<'c> ParallelProofChecker<'c> {
         }
     }
 
-    pub fn check(&mut self, proof: &Proof, scheduler: &Scheduler) -> CarcaraResult<bool> {
+    pub fn check(
+        &mut self,
+        problem: &Problem,
+        proof: &Proof,
+        scheduler: &Scheduler,
+    ) -> CarcaraResult<bool> {
         // Used to estimulate threads to abort prematurely (only happens when a
         // thread already found out an invalid step)
         let premature_abort = Arc::new(AtomicBool::new(false));
@@ -84,6 +89,7 @@ impl<'c> ParallelProofChecker<'c> {
                         .stack_size(self.stack_size)
                         .spawn_scoped(s, move || -> CarcaraResult<(bool, bool)> {
                             local_self.worker_thread_check(
+                                problem,
                                 proof,
                                 schedule,
                                 local_pool,
@@ -130,6 +136,7 @@ impl<'c> ParallelProofChecker<'c> {
 
     pub fn check_with_stats<CR: CollectResults + Send + Default>(
         &mut self,
+        problem: &Problem,
         proof: &Proof,
         scheduler: &Scheduler,
         stats: &mut CheckerStatistics<CR>,
@@ -165,6 +172,7 @@ impl<'c> ParallelProofChecker<'c> {
                             move || -> CarcaraResult<(bool, bool, CheckerStatistics<CR>)> {
                                 local_self
                                     .worker_thread_check(
+                                        problem,
                                         proof,
                                         schedule,
                                         local_pool,
@@ -226,6 +234,7 @@ impl<'c> ParallelProofChecker<'c> {
 
     fn worker_thread_check<CR: CollectResults + Send + Default>(
         &mut self,
+        problem: &Problem,
         proof: &Proof,
         schedule: &Schedule,
         mut pool: LocalPool,
@@ -303,7 +312,7 @@ impl<'c> ParallelProofChecker<'c> {
                     }
                 }
                 ProofCommand::Assume { id, term } => {
-                    if !self.check_assume(id, term, &proof.premises, &iter, &mut stats) {
+                    if !self.check_assume(id, term, &problem.premises, &iter, &mut stats) {
                         // Signalize to other threads to stop the proof checking
                         should_abort.store(true, Ordering::Release);
                         return Err(Error::Checker {

carcara/src/checker/rules/mod.rs

@@ -162,7 +162,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
 
     for (i, (proof, expected)) in cases.iter().enumerate() {
         // This parses the definitions again for every case, which is not ideal
-        let (_, mut proof, mut pool) = parser::parse_instance(
+        let (mut problem, mut proof, mut pool) = parser::parse_instance(
             Cursor::new(definitions),
             Cursor::new(proof),
             parser::Config::new(),
@@ -172,7 +172,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
         // Since rule tests often use `assume` commands to introduce premises, we search the proof
         // for all `assume`d terms and retroactively add them as the problem premises, to avoid
         // checker errors on the `assume`s
-        proof.premises = proof
+        problem.premises = proof
             .commands
             .iter()
             .filter_map(|c| match c {
@@ -193,7 +193,7 @@ fn run_tests(test_name: &str, definitions: &str, cases: &[(&str, bool)]) {
         }));
 
         let mut checker = checker::ProofChecker::new(&mut pool, checker::Config::new());
-        let got = checker.check(&proof).is_ok();
+        let got = checker.check(&problem, &proof).is_ok();
         assert_eq!(
             *expected, got,
             "test case \"{}\" index {} failed",

carcara/src/elaborator/hole.rs

@@ -59,14 +59,14 @@ fn get_problem_string(
 }
 
 pub fn hole(elaborator: &mut Elaborator, step: &StepNode) -> Option<Rc<ProofNode>> {
-    let prelude = if elaborator.prelude.logic.clone().unwrap() == "QF_LIA" {
+    let prelude = elaborator.problem.prelude.clone();
+    let prelude = if prelude.logic.as_deref() == Some("QF_LIA") {
         ProblemPrelude {
-            sort_declarations: elaborator.prelude.sort_declarations.clone(),
-            function_declarations: elaborator.prelude.function_declarations.clone(),
             logic: Some("QF_LIRA".into()),
+            ..prelude
         }
     } else {
-        elaborator.prelude.clone()
+        prelude
     };
     let problem = get_problem_string(elaborator.pool, &prelude, &step.clause);
     let options = elaborator.config.hole_options.as_ref().unwrap();
@@ -150,14 +150,11 @@ fn parse_and_check_solver_proof(
         allow_int_real_subtyping: true,
         strict: false,
     };
-    let mut parser = parser::Parser::new(pool, config, problem)?;
-    let (_, premises) = parser.parse_problem()?;
-    parser.reset(proof)?;
-    let mut proof = parser.parse_proof()?;
-    proof.premises = premises;
+
+    let (problem, proof) = parser::parse_instance_with_pool(problem, proof, config, pool)?;
 
     let config = checker::Config::new();
-    let res = checker::ProofChecker::new(pool, config).check(&proof)?;
+    let res = checker::ProofChecker::new(pool, config).check(&problem, &proof)?;
     Ok((proof.commands, res))
 }
 

carcara/src/elaborator/lia_generic.rs

@@ -59,7 +59,7 @@ fn get_problem_string(
 }
 
 pub fn lia_generic(elaborator: &mut Elaborator, step: &StepNode) -> Option<Rc<ProofNode>> {
-    let problem = get_problem_string(elaborator.pool, elaborator.prelude, &step.clause);
+    let problem = get_problem_string(elaborator.pool, &elaborator.problem.prelude, &step.clause);
     let options = elaborator.config.lia_options.as_ref().unwrap();
     let commands = match get_solver_proof(elaborator.pool, problem, options) {
         Ok(c) => c,
@@ -137,14 +137,10 @@ fn parse_and_check_solver_proof(
         allow_int_real_subtyping: true,
         strict: false,
     };
-    let mut parser = parser::Parser::new(pool, config, problem)?;
-    let (_, premises) = parser.parse_problem()?;
-    parser.reset(proof)?;
-    let mut proof = parser.parse_proof()?;
-    proof.premises = premises;
+    let (problem, proof) = parser::parse_instance_with_pool(problem, proof, config, pool)?;
 
     let config = checker::Config::new().ignore_unknown_rules(true);
-    checker::ProofChecker::new(pool, config).check(&proof)?;
+    checker::ProofChecker::new(pool, config).check(&problem, &proof)?;
     Ok(proof.commands)
 }
 

carcara/src/elaborator/mod.rs

@@ -64,19 +64,13 @@ pub struct HoleOptions {
 
 pub struct Elaborator<'e> {
     pool: &'e mut PrimitivePool,
-    premises: &'e IndexSet<Rc<Term>>,
-    prelude: &'e ProblemPrelude,
+    problem: &'e Problem,
     config: Config,
 }
 
 impl<'e> Elaborator<'e> {
-    pub fn new(
-        pool: &'e mut PrimitivePool,
-        premises: &'e IndexSet<Rc<Term>>,
-        prelude: &'e ProblemPrelude,
-        config: Config,
-    ) -> Self {
-        Self { pool, premises, prelude, config }
+    pub fn new(pool: &'e mut PrimitivePool, problem: &'e Problem, config: Config) -> Self {
+        Self { pool, problem, config }
     }
 
     pub fn elaborate_with_default_pipeline(&mut self, root: &Rc<ProofNode>) -> Rc<ProofNode> {
@@ -148,7 +142,7 @@ impl<'e> Elaborator<'e> {
         mutate(root, |context, node| {
             match node.as_ref() {
                 ProofNode::Assume { id, depth, term }
-                    if context.is_empty() && !self.premises.contains(term) =>
+                    if context.is_empty() && !self.problem.premises.contains(term) =>
                 {
                     self.elaborate_assume(id, *depth, term)
                 }
@@ -186,7 +180,7 @@ impl<'e> Elaborator<'e> {
 
     fn elaborate_assume(&mut self, id: &str, depth: usize, term: &Rc<Term>) -> Rc<ProofNode> {
         let mut found = None;
-        for p in self.premises {
+        for p in &self.problem.premises {
             if Polyeq::new()
                 .mod_reordering(true)
                 .mod_nary(true)