Add define rec fun to cvc parser (#1738)

7 files changed, 129 insertions, 8 deletions

diff --git a/src/parser/cvc/Cvc.g b/src/parser/cvc/Cvc.g
index 47bee5740..a4333c81d 100644
--- a/src/parser/cvc/Cvc.g
+++ b/src/parser/cvc/Cvc.g
@@ -81,7 +81,7 @@ tokens {
   ARITH_VAR_ORDER_TOK = 'ARITH_VAR_ORDER';
   CONTINUE_TOK = 'CONTINUE';
   RESTART_TOK = 'RESTART';
-
+  RECURSIVE_FUNCTION_TOK = 'REC-FUN';
   /* operators */
 
   AND_TOK = 'AND';
@@ -116,7 +116,7 @@ tokens {
   EXISTS_TOK = 'EXISTS';
   PATTERN_TOK = 'PATTERN';
 
-  LAMBDA = 'LAMBDA';
+  LAMBDA_TOK = 'LAMBDA';
 
   // Symbols
 
@@ -707,6 +707,15 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
   std::vector<CVC4::Datatype> dts;
   Debug("parser-extra") << "command: " << AntlrInput::tokenText(LT(1)) << std::endl;
   std::string s;
+  Expr func;
+  std::vector<Expr> bvs;
+  std::vector<Expr> funcs;
+  std::vector<Expr> formulas;
+  std::vector<std::vector<Expr>> formals;
+  std::vector<std::string> ids;
+  std::vector<CVC4::Type> types;
+  bool idCommaFlag = true;
+  bool formCommaFlag = true;
 }
     /* our bread & butter */
   : ASSERT_TOK formula[f] { cmd->reset(new AssertCommand(f)); }
@@ -880,6 +889,66 @@ mainCommand[std::unique_ptr<CVC4::Command>* cmd]
   | CONTINUE_TOK
     { UNSUPPORTED("CONTINUE command"); }
   | RESTART_TOK formula[f] { UNSUPPORTED("RESTART command"); }
+  | RECURSIVE_FUNCTION_TOK (identifier[id,CHECK_NONE,SYM_VARIABLE] 
+    {
+      if(idCommaFlag){
+        idCommaFlag=false;
+      }
+      else{
+        PARSER_STATE->parseError("Identifiers need to be comma separated");
+      }
+    }
+    COLON type[t,CHECK_DECLARED] (COMMA {
+      idCommaFlag=true;
+      })? 
+    {
+      func = PARSER_STATE->mkVar(id, t, ExprManager::VAR_FLAG_NONE, true);
+      ids.push_back(id);
+      types.push_back(t);
+      funcs.push_back(func);
+    })+
+    EQUAL_TOK (formula[f]
+    {
+      if(formCommaFlag){
+        formCommaFlag=false;
+      }
+      else{
+        PARSER_STATE->parseError("Function definitions need to be comma separated");
+      }
+    }
+    (COMMA{
+      formCommaFlag=true;
+    })?
+    {
+      if( f.getKind()==kind::LAMBDA ){
+        bvs.insert(bvs.end(), f[0].begin(), f[0].end());
+        formals.push_back(bvs);
+        bvs.clear();
+        f = f[1];
+        formulas.push_back(f);
+      }
+      else {
+        formals.push_back(bvs);
+        formulas.push_back(f);
+      }
+    })+
+    {
+      if(idCommaFlag){
+        PARSER_STATE->parseError("Cannot end function list with comma");
+      }
+      if(formCommaFlag){
+        PARSER_STATE->parseError("Cannot end function definition list with comma");
+      }
+      if(funcs.size()!=formulas.size()){
+        PARSER_STATE->parseError("Number of functions doesn't match number of function definitions");
+      }
+      for(unsigned int i = 0, size = funcs.size(); i < size; i++){
+        if(!funcs[i].getType().isSubtypeOf(types[i])){
+          PARSER_STATE->parseError("Type mismatch in definition");
+        }
+      }
+      cmd->reset(new DefineFunctionRecCommand(funcs,formals,formulas));
+    }
   | toplevelDeclaration[cmd]
   ;
 
@@ -1074,6 +1143,10 @@ declareVariables[std::unique_ptr<CVC4::Command>* cmd, CVC4::Type& t,
         }
       } else {
         // f is not null-- meaning this is a definition not a declaration
+        //Check if the formula f has the correct type, declared as t.
+        if(!f.getType().isSubtypeOf(t)){
+          PARSER_STATE->parseError("Type mismatch in definition");
+        }
         if(!topLevel) {
           // must be top-level; doesn't make sense to write something
           // like e.g. FORALL(x:INT = 4): [...]
@@ -1434,16 +1507,13 @@ prefixFormula[CVC4::Expr& f]
     IN_TOK formula[f] { PARSER_STATE->popScope(); }
 
    /* lambda */
-  | LAMBDA { PARSER_STATE->pushScope(); } LPAREN
+  | LAMBDA_TOK { PARSER_STATE->pushScope(); } LPAREN
     boundVarDeclsReturn[terms,types]
     RPAREN COLON formula[f]
     { PARSER_STATE->popScope();
       Type t = EXPR_MANAGER->mkFunctionType(types, f.getType());
-      std::string name = "lambda";
-      Expr func = PARSER_STATE->mkAnonymousFunction(name, t, ExprManager::VAR_FLAG_DEFINED);
-      Command* cmd = new DefineFunctionCommand(name, func, terms, f);
-      PARSER_STATE->preemptCommand(cmd);
-      f = func;
+      Expr bvl = EXPR_MANAGER->mkExpr( kind::BOUND_VAR_LIST, terms );
+      f = EXPR_MANAGER->mkExpr( kind::LAMBDA, bvl, f );
     }
   ;
 
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index de80368a4..c5b38dcd8 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -1222,6 +1222,8 @@ REG1_TESTS = \
 	regress1/quantifiers/burns4.smt2 \
 	regress1/quantifiers/cbqi-sdlx-fixpoint-3-dd.smt2 \
 	regress1/quantifiers/cdt-0208-to.smt2 \
+	regress1/quantifiers/const.cvc \
+	regress1/quantifiers/constfunc.cvc \
 	regress1/quantifiers/ext-ex-deq-trigger.smt2 \
 	regress1/quantifiers/extract-nproc.smt2 \
 	regress1/quantifiers/florian-case-ax.smt2 \
@@ -1233,6 +1235,7 @@ REG1_TESTS = \
 	regress1/quantifiers/javafe.ast.StmtVec.009.smt2 \
 	regress1/quantifiers/mix-coeff.smt2 \
 	regress1/quantifiers/model_6_1_bv.smt2 \
+	regress1/quantifiers/mutualrec2.cvc \
 	regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 \
 	regress1/quantifiers/opisavailable-12.smt2 \
 	regress1/quantifiers/parametric-lists.smt2 \
@@ -1257,6 +1260,7 @@ REG1_TESTS = \
 	regress1/quantifiers/qcft-javafe.filespace.TreeWalker.006.smt2 \
 	regress1/quantifiers/qcft-smtlib3dbc51.smt2 \
 	regress1/quantifiers/quaternion_ds1_symm_0428.fof.smt2 \
+	regress1/quantifiers/recfact.cvc \
 	regress1/quantifiers/rew-to-0211-dd.smt2 \
 	regress1/quantifiers/ricart-agrawala6.smt2 \
 	regress1/quantifiers/set3.smt2 \
@@ -1535,6 +1539,7 @@ REG2_TESTS = \
 	regress2/quantifiers/javafe.ast.WhileStmt.447.smt2 \
 	regress2/quantifiers/javafe.tc.CheckCompilationUnit.001.smt2 \
 	regress2/quantifiers/javafe.tc.FlowInsensitiveChecks.682.smt2 \
+	regress2/quantifiers/mutualrec2.cvc \
 	regress2/quantifiers/nunchaku2309663.nun.min.smt2 \
 	regress2/simplify.javafe.ast.ArrayInit.35_without_quantification2.smt2 \
 	regress2/strings/cmu-dis-0707-3.smt2 \
diff --git a/test/regress/regress1/quantifiers/const.cvc b/test/regress/regress1/quantifiers/const.cvc
new file mode 100644
index 000000000..41b13434a
--- /dev/null
+++ b/test/regress/regress1/quantifiers/const.cvc
@@ -0,0 +1,4 @@
+% EXPECT: unsat
+REC-FUN five : INT = 5;
+ASSERT five = 6;
+CHECKSAT;
diff --git a/test/regress/regress1/quantifiers/constfunc.cvc b/test/regress/regress1/quantifiers/constfunc.cvc
new file mode 100644
index 000000000..3b563cdad
--- /dev/null
+++ b/test/regress/regress1/quantifiers/constfunc.cvc
@@ -0,0 +1,7 @@
+% EXPECT: unsat
+OPTION "fmf-fun";
+REC-FUN f : INT -> INT = LAMBDA (x : INT) : 1;
+x : INT;
+ASSERT NOT (f(7) = x);
+ASSERT f(8) = x;
+CHECKSAT;
diff --git a/test/regress/regress1/quantifiers/mutualrec2.cvc b/test/regress/regress1/quantifiers/mutualrec2.cvc
new file mode 100644
index 000000000..66da896ae
--- /dev/null
+++ b/test/regress/regress1/quantifiers/mutualrec2.cvc
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+OPTION "fmf-fun";
+REC-FUN iseven : (INT) -> INT, isodd : (INT) -> INT, fact : INT -> INT =
+LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE (IF (isodd(x - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF,
+LAMBDA (y : INT): IF (y = 0) THEN 0 ELSE (IF (iseven(y - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF,
+LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE x * fact(x - 1) ENDIF;
+a,b,x,y,z : INT;
+ASSERT 1 = isodd(4);
+ASSERT 0 = iseven(4);
+ASSERT 0 = isodd(3);
+ASSERT 1 = iseven(3);
+ASSERT NOT (24 = fact(4));
+CHECKSAT;
+
diff --git a/test/regress/regress1/quantifiers/recfact.cvc b/test/regress/regress1/quantifiers/recfact.cvc
new file mode 100644
index 000000000..b2ea3304f
--- /dev/null
+++ b/test/regress/regress1/quantifiers/recfact.cvc
@@ -0,0 +1,7 @@
+% EXPECT: unsat
+OPTION "fmf-fun";
+x : INT;
+REC-FUN fact : (INT) -> INT = LAMBDA (x : INT) : IF (x > 0) THEN x * fact (x - 1) ELSE 1 ENDIF;
+ASSERT fact(0) = 2;
+ASSERT x = fact(3);
+CHECKSAT;
diff --git a/test/regress/regress2/quantifiers/mutualrec2.cvc b/test/regress/regress2/quantifiers/mutualrec2.cvc
new file mode 100644
index 000000000..66da896ae
--- /dev/null
+++ b/test/regress/regress2/quantifiers/mutualrec2.cvc
@@ -0,0 +1,14 @@
+% EXPECT: unsat
+OPTION "fmf-fun";
+REC-FUN iseven : (INT) -> INT, isodd : (INT) -> INT, fact : INT -> INT =
+LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE (IF (isodd(x - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF,
+LAMBDA (y : INT): IF (y = 0) THEN 0 ELSE (IF (iseven(y - 1) = 0) THEN 1 ELSE 0 ENDIF) ENDIF,
+LAMBDA (x : INT): IF (x = 0) THEN 1 ELSE x * fact(x - 1) ENDIF;
+a,b,x,y,z : INT;
+ASSERT 1 = isodd(4);
+ASSERT 0 = iseven(4);
+ASSERT 0 = isodd(3);
+ASSERT 1 = iseven(3);
+ASSERT NOT (24 = fact(4));
+CHECKSAT;
+