diff --git a/carcara/src/parser/lexer.rs b/carcara/src/parser/lexer.rs index bc933660..69734a64 100644 --- a/carcara/src/parser/lexer.rs +++ b/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", diff --git a/carcara/src/parser/mod.rs b/carcara/src/parser/mod.rs index 3789c653..67c88ac3 100644 --- a/carcara/src/parser/mod.rs +++ b/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 `( (*) )`. 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, Rc)> { + 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 ¶ms { + 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, body: Rc) { + 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 ¶ms { - 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 ¶ms { + 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 diff --git a/carcara/src/parser/tests.rs b/carcara/src/parser/tests.rs index cb57a897..968e7995 100644 --- a/carcara/src/parser/tests.rs +++ b/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();