Add define rec fun to cvc parser (#1738)

6 files changed, 51 insertions, 0 deletions

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;
+