Add option to specify which unknown rules are allowed

carcara/src/checker/mod.rs

@@ -12,6 +12,7 @@ use indexmap::IndexSet;
 pub use parallel::{scheduler::Scheduler, ParallelProofChecker};
 use rules::{Premise, Rule, RuleArgs, RuleResult};
 use std::{
+    collections::HashSet,
     fmt,
     time::{Duration, Instant},
 };
@@ -41,7 +42,7 @@ impl<CR: CollectResults + Send + Default> fmt::Debug for CheckerStatistics<'_, C
     }
 }
 
-#[derive(Debug, Default, Clone, Copy)]
+#[derive(Debug, Default, Clone)]
 pub struct Config {
     /// Enables "strict" checking of some rules.
     ///
@@ -57,6 +58,9 @@ pub struct Config {
     /// If `true`, the checker will skip any steps with rules that it does not recognize, and will
     /// consider them as holes. Normally, using an unknown rule is considered an error.
     pub ignore_unknown_rules: bool,
+
+    /// A set of rule names that the checker will allow, considering them holes in the proof.
+    pub allowed_rules: HashSet<String>,
 }
 
 impl Config {
@@ -270,7 +274,9 @@ impl<'c> ProofChecker<'c> {
 
         let rule = match Self::get_rule(&step.rule, self.config.strict) {
             Some(r) => r,
-            None if self.config.ignore_unknown_rules => {
+            None if self.config.ignore_unknown_rules
+                || self.config.allowed_rules.contains(&step.rule) =>
+            {
                 self.is_holey = true;
                 return Ok(());
             }

carcara/src/checker/parallel/mod.rs

@@ -53,7 +53,7 @@ impl<'c> ParallelProofChecker<'c> {
     pub fn share(&self) -> Self {
         ParallelProofChecker {
             pool: self.pool.clone(),
-            config: self.config,
+            config: self.config.clone(),
             prelude: self.prelude,
             context: ContextStack::from_previous(&self.context),
             reached_empty_clause: false,

cli/src/benchmarking.rs

@@ -95,7 +95,7 @@ fn worker_thread<T: CollectResults + Default + Send>(
             &mut results,
             job,
             parser_config,
-            checker_config,
+            checker_config.clone(),
             elaborator_config.clone(),
         );
         match result {
@@ -141,6 +141,7 @@ pub fn run_benchmark<T: CollectResults + Default + Send>(
         #[allow(clippy::needless_collect)]
         let workers: Vec<_> = (0..num_jobs)
             .map(|_| {
+                let checker_config = checker_config.clone();
                 let elaborator_config = elaborator_config.clone();
                 thread::Builder::new()
                     .stack_size(STACK_SIZE)

cli/src/main.rs

@@ -152,6 +152,10 @@ struct CheckingOptions {
     #[clap(long, conflicts_with("ignore-unknown-rules"), hide = true)]
     skip_unknown_rules: bool,
 
+    /// A set of extra rules to be allowed by the checker, and considered as holes.
+    #[clap(long, multiple = true, conflicts_with = "ignore-unknown-rules")]
+    allowed_rules: Option<Vec<String>>,
+
     #[clap(long, hide = true)] // TODO
     strict_checking: bool,
 }
@@ -161,6 +165,7 @@ impl From<CheckingOptions> for checker::Config {
         Self {
             strict: val.strict_checking,
             ignore_unknown_rules: val.ignore_unknown_rules,
+            allowed_rules: val.allowed_rules.unwrap_or_default().into_iter().collect(),
         }
     }
 }