From d8994e79a67778b99e03dbe5a9437c4eb75c6c06 Mon Sep 17 00:00:00 2001 From: Arjun Viswanathan Date: Fri, 6 Apr 2018 17:50:48 -0500 Subject: Add define rec fun to cvc parser (#1738) --- test/regress/Makefile.tests | 5 +++++ test/regress/regress1/quantifiers/const.cvc | 4 ++++ test/regress/regress1/quantifiers/constfunc.cvc | 7 +++++++ test/regress/regress1/quantifiers/mutualrec2.cvc | 14 ++++++++++++++ test/regress/regress1/quantifiers/recfact.cvc | 7 +++++++ test/regress/regress2/quantifiers/mutualrec2.cvc | 14 ++++++++++++++ 6 files changed, 51 insertions(+) create mode 100644 test/regress/regress1/quantifiers/const.cvc create mode 100644 test/regress/regress1/quantifiers/constfunc.cvc create mode 100644 test/regress/regress1/quantifiers/mutualrec2.cvc create mode 100644 test/regress/regress1/quantifiers/recfact.cvc create mode 100644 test/regress/regress2/quantifiers/mutualrec2.cvc (limited to 'test/regress') 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; + -- cgit v1.2.3