Add support for define-funs-rec

carcara/src/parser/lexer.rs

@@ -102,6 +102,9 @@ pub enum Reserved {
     /// The `define-fun-rec` reserved word.
     DefineFunRec,
 
+    /// The `define-funs-rec` reserved word.
+    DefineFunsRec,
+
     /// The `define-sort` reserved word.
     DefineSort,
 
@@ -134,6 +137,7 @@ impl_str_conversion_traits!(Reserved {
     DeclareSort: "declare-sort",
     DefineFun: "define-fun",
     DefineFunRec: "define-fun-rec",
+    DefineFunsRec: "define-funs-rec",
     DefineSort: "define-sort",
     Assert: "assert",
     CheckSatAssuming: "check-sat-assuming",

carcara/src/parser/mod.rs

@@ -679,7 +679,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
                     self.state.sort_declarations.insert(name, arity);
                 }
                 Token::ReservedWord(Reserved::DefineFun) => {
-                    let (name, func_def) = self.parse_define_fun(false)?;
+                    let (name, func_def) = self.parse_define_fun()?;
 
                     if self.config.apply_function_defs {
                         self.state.function_defs.insert(name, func_def);
@@ -705,44 +705,8 @@ impl<'a, R: BufRead> Parser<'a, R> {
                         self.premises().insert(assertion_term);
                     }
                 }
-                Token::ReservedWord(Reserved::DefineFunRec) => {
-                    // When we encounter a `define-func-rec`, we add a new premise that asserts that,
-                    // forall values of the arguments, the function application is equal to the
-                    // function body. For example,
-                    // ```
-                    // (define-fun-rec sumr ((x Int)) Int (+ x (ite (> x 0) (sumr (- x 1)) 0)))
-                    // ```
-                    // becomes
-                    // ```
-                    // (assert (forall ((x Int)) (= (sumr x) (+ x (ite (> x 0) (sumr (- x 1)) 0)))))
-                    // ```
-                    let (name, func_def) = self.parse_define_fun(true)?;
-                    let application = {
-                        let cached = HashCache::new(name);
-                        let func_sort = self.state.symbol_table.get(&cached).unwrap();
-                        let name = cached.unwrap();
-                        let func_term = self.pool.add((name, func_sort.clone()).into());
-                        if func_def.params.is_empty() {
-                            func_term
-                        } else {
-                            let args = func_def
-                                .params
-                                .iter()
-                                .map(|var| self.pool.add(var.clone().into()))
-                                .collect();
-                            self.pool.add(Term::App(func_term, args))
-                        }
-                    };
-                    let equality_term = build_term!(self.pool, (= {application} {func_def.body}));
-                    let premise = if func_def.params.is_empty() {
-                        equality_term
-                    } else {
-                        let bindings = BindingList(func_def.params);
-                        self.pool
-                            .add(Term::Binder(Binder::Forall, bindings, equality_term))
-                    };
-                    self.premises().insert(premise);
-                }
+                Token::ReservedWord(Reserved::DefineFunRec) => self.parse_define_fun_rec(false)?,
+                Token::ReservedWord(Reserved::DefineFunsRec) => self.parse_define_fun_rec(true)?,
                 Token::ReservedWord(Reserved::DefineSort) => {
                     let (name, def) = self.parse_define_sort()?;
                     self.state.sort_defs.insert(name, def);
@@ -817,7 +781,7 @@ impl<'a, R: BufRead> Parser<'a, R> {
                     (step.id.clone(), ProofCommand::Step(step))
                 }
                 Token::ReservedWord(Reserved::DefineFun) => {
-                    let (name, func_def) = self.parse_define_fun(false)?;
+                    let (name, func_def) = self.parse_define_fun()?;
                     self.state.function_defs.insert(name, func_def);
                     continue;
                 }
@@ -1100,19 +1064,84 @@ impl<'a, R: BufRead> Parser<'a, R> {
         Ok((name, arity))
     }
 
-    /// Parses a `define-fun` or `define-fun-rec` proof command. Returns the function name and its
-    /// definition. This method assumes that the `(` and `define-fun`/`define-fun-rec` tokens were
-    /// already consumed.
-    fn parse_define_fun(&mut self, is_rec: bool) -> CarcaraResult<(String, FunctionDef)> {
+    /// Parses a function declaration, of the form `(<symbol> (<sorted var>*) <sort>)`. If the
+    /// parameter `consume_parens` is `false`, the opening and closing parentheses are not consumed
+    fn parse_function_dec(
+        &mut self,
+        consume_parens: bool,
+    ) -> CarcaraResult<(String, Vec<SortedVar>, Rc<Term>)> {
+        if consume_parens {
+            self.expect_token(Token::OpenParen)?;
+        }
         let name = self.expect_symbol()?;
         self.expect_token(Token::OpenParen)?;
         let params = self.parse_sequence(Self::parse_sorted_var, false)?;
         let return_sort = self.parse_sort()?;
+        if consume_parens {
+            self.expect_token(Token::CloseParen)?;
+        }
+        Ok((name, params, return_sort))
+    }
+
+    /// Parses a `define-fun` proof command. Returns the function name and its definition. This
+    /// method assumes that the `(` and `define-fun` tokens were already consumed.
+    fn parse_define_fun(&mut self) -> CarcaraResult<(String, FunctionDef)> {
+        let (name, params, return_sort) = self.parse_function_dec(false)?;
+
+        // In order to correctly parse the function body, we push a new scope to the symbol table
+        // and add the functions arguments to it.
+        self.state.symbol_table.push_scope();
+        for var in &params {
+            self.insert_sorted_var(var.clone());
+        }
+        let body = self.parse_term_expecting_sort(return_sort.as_sort().unwrap())?;
+        self.state.symbol_table.pop_scope();
+
+        self.expect_token(Token::CloseParen)?;
+
+        Ok((name, FunctionDef { params, body }))
+    }
 
-        // If this is a `define-fun-rec`, we need to add the function itself to the symbol
-        // table. Note that we add it before pushing the new scope, so this entry survives for
-        // the rest of the proof
-        if is_rec {
+    /// Adds the premise corresponding to a `define-fun-rec` function definition.
+    fn add_define_fun_rec_premise(&mut self, name: String, params: Vec<SortedVar>, body: Rc<Term>) {
+        let application = {
+            let cached = HashCache::new(name);
+            let func_sort = self.state.symbol_table.get(&cached).unwrap();
+            let name = cached.unwrap();
+            let func_term = self.pool.add((name, func_sort.clone()).into());
+            if params.is_empty() {
+                func_term
+            } else {
+                let args = params
+                    .iter()
+                    .map(|var| self.pool.add(var.clone().into()))
+                    .collect();
+                self.pool.add(Term::App(func_term, args))
+            }
+        };
+        let equality_term = build_term!(self.pool, (= {application} {body}));
+        let premise = if params.is_empty() {
+            equality_term
+        } else {
+            let bindings = BindingList(params);
+            self.pool
+                .add(Term::Binder(Binder::Forall, bindings, equality_term))
+        };
+        self.premises().insert(premise);
+    }
+
+    /// Parses a `define-fun-rec`/`define-funs-rec` command. Inserts the function names into the
+    /// symbol table, and adds the appropriate premises. This method assumes the `(` and
+    /// `define-fun-rec`/`define-funs-rec` tokens were already consumed.
+    fn parse_define_fun_rec(&mut self, is_multiple: bool) -> CarcaraResult<()> {
+        let declarations = if is_multiple {
+            self.expect_token(Token::OpenParen)?;
+            self.parse_sequence(|p| p.parse_function_dec(true), true)?
+        } else {
+            vec![self.parse_function_dec(false)?]
+        };
+
+        for (name, params, return_sort) in &declarations {
             let sort = if params.is_empty() {
                 return_sort.as_sort().unwrap().clone()
             } else {
@@ -1124,18 +1153,25 @@ impl<'a, R: BufRead> Parser<'a, R> {
             self.insert_sorted_var((name.clone(), sort));
         }
 
-        // In order to correctly parse the function body, we push a new scope to the symbol table
-        // and add the functions arguments to it.
-        self.state.symbol_table.push_scope();
-        for var in &params {
-            self.insert_sorted_var(var.clone());
+        if is_multiple {
+            self.expect_token(Token::OpenParen)?;
         }
-        let body = self.parse_term_expecting_sort(return_sort.as_sort().unwrap())?;
-        self.state.symbol_table.pop_scope();
+        for (name, params, return_sort) in declarations {
+            self.state.symbol_table.push_scope();
+            for var in &params {
+                self.insert_sorted_var(var.clone());
+            }
+            let body = self.parse_term_expecting_sort(return_sort.as_sort().unwrap())?;
+            self.state.symbol_table.pop_scope();
 
+            self.add_define_fun_rec_premise(name, params, body);
+        }
+        if is_multiple {
+            self.expect_token(Token::CloseParen)?;
+        }
         self.expect_token(Token::CloseParen)?;
 
-        Ok((name, FunctionDef { params, body }))
+        Ok(())
     }
 
     /// Parses a `define-sort` proof command. Returns the sort name and its definition. This method

carcara/src/parser/tests.rs

@@ -475,6 +475,46 @@ fn test_define_fun() {
     assert_eq!(expected, got);
 }
 
+#[test]
+fn test_define_fun_rec() {
+    fn run_test(pool: &mut PrimitivePool, problem: &str, expected_premises: &[&str]) {
+        let mut parser = Parser::new(pool, TEST_CONFIG, problem.as_bytes()).expect(ERROR_MESSAGE);
+        let got = parser.parse_problem().expect(ERROR_MESSAGE).1;
+        assert_eq!(expected_premises.len(), got.len());
+        for p in expected_premises {
+            parser.reset(p.as_bytes()).expect(ERROR_MESSAGE);
+            let expected = parser.parse_term().expect(ERROR_MESSAGE);
+            assert!(got.contains(&expected));
+        }
+    }
+    let mut p = PrimitivePool::new();
+
+    run_test(
+        &mut p,
+        "(define-fun-rec sumr ((x Int)) Int (+ x (ite (> x 0) (sumr (- x 1)) 0)))",
+        &["(forall ((x Int))  (= (sumr x) (+ x (ite (> x 0) (sumr (- x 1)) 0))))"],
+    );
+
+    run_test(&mut p, "(define-fun-rec five () Int 5)", &["(= five 5)"]);
+
+    run_test(
+        &mut p,
+        "(define-funs-rec
+            ((is-even ((n Int)) Bool) (is-odd ((n Int)) Bool) (zero () Int))
+            (
+                (ite (= n zero) true (is-odd (- n 1)))
+                (ite (= n zero) false (is-even (- n 1)))
+                0
+            )
+        )",
+        &[
+            "(forall ((n Int)) (= (is-even n) (ite (= n zero) true (is-odd (- n 1)))))",
+            "(forall ((n Int)) (= (is-odd n) (ite (= n zero) false (is-even (- n 1)))))",
+            "(= zero 0)",
+        ],
+    );
+}
+
 #[test]
 fn test_define_sort() {
     let mut p = PrimitivePool::new();