Reject unary logical operations with --strict flag

carcara/src/lib.rs

@@ -157,6 +157,7 @@ pub fn check<T: io::BufRead>(problem: T, proof: T, options: CarcaraOptions) -> R
         apply_function_defs: options.apply_function_defs,
         expand_lets: options.expand_lets,
         allow_int_real_subtyping: options.allow_int_real_subtyping,
+        allow_unary_logical_ops: !options.strict,
     };
     let (prelude, proof, mut pool) = parser::parse_instance(problem, proof, config)?;
     run_measures.parsing = total.elapsed();
@@ -222,6 +223,7 @@ pub fn check_parallel<T: io::BufRead>(
         apply_function_defs: options.apply_function_defs,
         expand_lets: options.expand_lets,
         allow_int_real_subtyping: options.allow_int_real_subtyping,
+        allow_unary_logical_ops: !options.strict,
     };
     let (prelude, proof, pool) = parser::parse_instance(problem, proof, config)?;
     run_measures.parsing = total.elapsed();
@@ -292,6 +294,7 @@ pub fn check_and_elaborate<T: io::BufRead>(
         apply_function_defs: options.apply_function_defs,
         expand_lets: options.expand_lets,
         allow_int_real_subtyping: options.allow_int_real_subtyping,
+        allow_unary_logical_ops: !options.strict,
     };
     let (prelude, proof, mut pool) = parser::parse_instance(problem, proof, config)?;
     run_measures.parsing = total.elapsed();

carcara/src/parser/mod.rs

@@ -19,16 +19,28 @@ use std::{io::BufRead, str::FromStr};
 
 use self::error::assert_indexed_op_args_value;
 
-#[derive(Debug, Default, Clone, Copy)]
+#[derive(Debug, Clone, Copy)]
 pub struct Config {
     pub apply_function_defs: bool,
     pub expand_lets: bool,
     pub allow_int_real_subtyping: bool,
+    pub allow_unary_logical_ops: bool,
 }
 
 impl Config {
     pub fn new() -> Self {
-        Self::default()
+        Config {
+            apply_function_defs: false,
+            expand_lets: false,
+            allow_int_real_subtyping: false,
+            allow_unary_logical_ops: true,
+        }
+    }
+}
+
+impl Default for Config {
+    fn default() -> Self {
+        Self::new()
     }
 }
 
@@ -185,8 +197,14 @@ impl<'a, R: BufRead> Parser<'a, R> {
                 }
             }
             Operator::Or | Operator::And | Operator::Xor => {
-                // These operators can be called with only one argument
-                assert_num_args(&args, 1..)?;
+                // If we are not in "strict" parsing mode, we allow these operators to be called
+                // with just one argument
+                let range = if self.config.allow_unary_logical_ops {
+                    1..
+                } else {
+                    2..
+                };
+                assert_num_args(&args, range)?;
                 for s in sorts {
                     SortError::assert_eq(&Sort::Bool, s.as_sort().unwrap())?;
                 }

carcara/src/parser/tests.rs

@@ -12,6 +12,7 @@ const TEST_CONFIG: Config = Config {
     apply_function_defs: true,
     expand_lets: false,
     allow_int_real_subtyping: false,
+    allow_unary_logical_ops: true,
 };
 
 pub fn parse_terms<const N: usize>(

cli/src/benchmarking.rs

@@ -41,6 +41,7 @@ fn run_job<T: CollectResults + Default + Send>(
         apply_function_defs: options.apply_function_defs,
         expand_lets: options.expand_lets,
         allow_int_real_subtyping: options.allow_int_real_subtyping,
+        allow_unary_logical_ops: !options.strict,
     };
     let (prelude, proof, mut pool) = parser::parse_instance(
         BufReader::new(File::open(job.problem_file)?),

cli/src/main.rs

@@ -115,14 +115,18 @@ struct ParsingOptions {
     /// to arithmetic operators that are expecting a term of sort `Real`.
     #[clap(long)]
     allow_int_real_subtyping: bool,
-}
 
-#[derive(Args, Clone)]
-struct CheckingOptions {
-    /// Enables the strict checking of certain rules.
+    /// Enables strict parsing and checking.
+    ///
+    /// When this flag is enabled: unary `and`, `or` and `xor` terms are not allowed; for the `refl`
+    /// and `assume` rules, implicit reordering of equalities is not allowed; for the `resolution`
+    /// and `th_resolution` rules, the pivots used must be passed as arguments.
     #[clap(short, long)]
     strict: bool,
+}
 
+#[derive(Args, Clone)]
+struct CheckingOptions {
     /// Allow steps with rules that are not known by the checker, and consider them as holes.
     #[clap(short, long)]
     ignore_unknown_rules: bool,
@@ -162,9 +166,9 @@ fn build_carcara_options(
         apply_function_defs,
         expand_let_bindings,
         allow_int_real_subtyping,
+        strict,
     }: ParsingOptions,
     CheckingOptions {
-        strict,
         ignore_unknown_rules,
         skip_unknown_rules,
         lia_solver,
@@ -396,6 +400,7 @@ fn parse_command(options: ParseCommandOptions) -> CliResult<()> {
             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,
+            allow_unary_logical_ops: !options.parsing.strict,
         },
     )
     .map_err(carcara::Error::from)?;
@@ -492,6 +497,7 @@ fn slice_command(options: SliceCommandOption) -> CliResult<()> {
         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,
+        allow_unary_logical_ops: !options.parsing.strict,
     };
     let (_, proof, _) =
         parser::parse_instance(problem, proof, config).map_err(carcara::Error::from)?;