Make parser strict option enforce anchor arguments style

carcara/src/elaborator/lia_generic.rs

@@ -135,7 +135,7 @@ fn parse_and_check_solver_proof(
         apply_function_defs: false,
         expand_lets: true,
         allow_int_real_subtyping: true,
-        allow_unary_logical_ops: true,
+        strict: false,
     };
     let mut parser = parser::Parser::new(pool, config, problem)?;
     let (_, premises) = parser.parse_problem()?;

carcara/src/parser/mod.rs

@@ -21,7 +21,7 @@ use std::{io::BufRead, str::FromStr};
 
 use self::error::assert_indexed_op_args_value;
 
-#[derive(Debug, Clone, Copy)]
+#[derive(Debug, Clone, Copy, Default)]
 pub struct Config {
     /// If `true`, the parser will automatically expand function definitions introduced by
     /// `define-fun` commands in the SMT problem. If `false`, those `define-fun`s are instead
@@ -41,23 +41,15 @@ pub struct Config {
     /// to a function that expects a `Real` will still be an error.
     pub allow_int_real_subtyping: bool,
 
-    pub allow_unary_logical_ops: bool,
+    /// Enables "strict" parsing. If `true`:
+    /// - Unary `and`, `or` and `xor` terms are not allowed
+    /// - Anchor arguments using the old syntax (i.e., `(:= <symbol> <term>)`) are not allowed
+    pub strict: bool,
 }
 
 impl Config {
     pub fn new() -> Self {
-        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()
+        Self::default()
     }
 }
 
@@ -248,12 +240,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
             Operator::Or | Operator::And | Operator::Xor => {
                 // 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)?;
+                assert_num_args(&args, if self.config.strict { 2.. } else { 1.. })?;
                 for s in sorts {
                     SortError::assert_eq(&Sort::Bool, s)?;
                 }
@@ -1032,16 +1019,18 @@ impl<'a, R: BufRead> Parser<'a, R> {
             // parsing the two versions of assign-style anchor arguments:
             // - the old version, without the sort hint: `(:= <symbol> <term>)`
             // - and the new version, with the sort hint: `(:= (<symbol> <sort>) <term>)`
-            let (var, value, sort) = if matches!(self.current_token, Token::Symbol(_)) {
-                let var = self.expect_symbol()?;
-                let value = self.parse_term()?;
-                let sort = self.pool.sort(&value);
-                (var, value, sort)
-            } else {
-                let (var, sort) = self.parse_sorted_var()?;
-                let value = self.parse_term_expecting_sort(sort.as_sort().unwrap())?;
-                (var, value, sort)
-            };
+            // However, if "strict" parsing is enabled, we only allow the new version
+            let (var, value, sort) =
+                if !self.config.strict && matches!(self.current_token, Token::Symbol(_)) {
+                    let var = self.expect_symbol()?;
+                    let value = self.parse_term()?;
+                    let sort = self.pool.sort(&value);
+                    (var, value, sort)
+                } else {
+                    let (var, sort) = self.parse_sorted_var()?;
+                    let value = self.parse_term_expecting_sort(sort.as_sort().unwrap())?;
+                    (var, value, sort)
+                };
             self.insert_sorted_var((var.clone(), sort.clone()));
             self.expect_token(Token::CloseParen)?;
             AnchorArg::Assign((var, sort), value)

carcara/src/parser/tests.rs

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

cli/src/main.rs

@@ -137,7 +137,7 @@ impl From<ParsingOptions> for parser::Config {
             apply_function_defs: val.apply_function_defs,
             expand_lets: val.expand_let_bindings,
             allow_int_real_subtyping: val.allow_int_real_subtyping,
-            allow_unary_logical_ops: !val.strict,
+            strict: val.strict,
         }
     }
 }
@@ -466,17 +466,8 @@ fn parse_command(
     options: ParseCommandOptions,
 ) -> CliResult<(ast::ProblemPrelude, ast::Proof, ast::PrimitivePool)> {
     let (problem, proof) = get_instance(&options.input)?;
-    let result = parser::parse_instance(
-        problem,
-        proof,
-        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,
-            allow_unary_logical_ops: !options.parsing.strict,
-        },
-    )
-    .map_err(carcara::Error::from)?;
+    let result = parser::parse_instance(problem, proof, options.parsing.into())
+        .map_err(carcara::Error::from)?;
     Ok(result)
 }
 
@@ -574,14 +565,8 @@ fn slice_command(
     options: SliceCommandOptions,
 ) -> CliResult<(ast::ProblemPrelude, ast::Proof, ast::PrimitivePool)> {
     let (problem, proof) = get_instance(&options.input)?;
-    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,
-        allow_unary_logical_ops: !options.parsing.strict,
-    };
-    let (prelude, proof, pool) =
-        parser::parse_instance(problem, proof, config).map_err(carcara::Error::from)?;
+    let (prelude, proof, pool) = parser::parse_instance(problem, proof, options.parsing.into())
+        .map_err(carcara::Error::from)?;
 
     let node = ast::ProofNode::from_commands_with_root_id(proof.commands, &options.from)
         .ok_or_else(|| CliError::InvalidSliceId(options.from))?;
@@ -599,17 +584,8 @@ fn generate_lia_problems_command(options: ParseCommandOptions, use_sharing: bool
     let root_file_name = options.input.proof_file.clone();
     let (problem, proof) = get_instance(&options.input)?;
 
-    let instances = generate_lia_smt_instances(
-        problem,
-        proof,
-        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,
-            allow_unary_logical_ops: !options.parsing.strict,
-        },
-        use_sharing,
-    )?;
+    let instances =
+        generate_lia_smt_instances(problem, proof, options.parsing.into(), use_sharing)?;
     for (id, content) in instances {
         let file_name = format!("{}.{}.lia_smt2", root_file_name, id);
         let mut f = File::create(file_name)?;