diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2020-06-18 22:51:50 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2020-06-18 22:51:50 -0700 |
commit | e8884b9b8ba86ce71807887cab87a5188cce4003 (patch) | |
tree | 3b56553ecc3227eafe7aca057c5e29cd8efb63e0 /test | |
parent | 3054cd99db968eb85a9195b12e17e83a334e00cb (diff) |
Add logic check for define-fun(s)-rec (#4577)
This commit adds a logic check for `define-fun-rec`/`define-funs-rec` at
the level of the new API that checks whether the logic is quantified and
includes UF. To make sure that the parser actually executes that check,
this commit converts the `DefineFunctionRecCommand` command to use the
new API instead of the old one. This temporarily breaks the `exportTo`
functionality for `DefineFunctionRecCommand` but this is not currently
used within the CVC4 code base (and it seems unlikely that users use
commands).
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
-rw-r--r-- | test/regress/regress0/smtlib/define-fun-rec-logic.smt2 | 12 | ||||
-rw-r--r-- | test/unit/api/solver_black.h | 32 |
3 files changed, 45 insertions, 0 deletions
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index cdac5fc6c..5ae66f203 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -920,6 +920,7 @@ set(regress_0_tests regress0/simplification_bug2.smtv1.smt2 regress0/smallcnf.cvc regress0/smt2output.smt2 + regress0/smtlib/define-fun-rec-logic.smt2 regress0/smtlib/get-unsat-assumptions.smt2 regress0/smtlib/global-decls.smt2 regress0/smtlib/issue4028.smt2 diff --git a/test/regress/regress0/smtlib/define-fun-rec-logic.smt2 b/test/regress/regress0/smtlib/define-fun-rec-logic.smt2 new file mode 100644 index 000000000..1af16210d --- /dev/null +++ b/test/regress/regress0/smtlib/define-fun-rec-logic.smt2 @@ -0,0 +1,12 @@ +; EXPECT: unsat +; EXPECT: (error "recursive function definitions require a logic with quantifiers") +; EXIT: 1 +(set-logic UFBV) +(define-funs-rec ((f ((b Bool)) Bool) (g ((b Bool)) Bool)) (b b)) +(assert (g false)) +(check-sat) +(reset) +(set-logic QF_BV) +(define-funs-rec ((f ((b Bool)) Bool) (g ((b Bool)) Bool)) (b b)) +(assert (g false)) +(check-sat) diff --git a/test/unit/api/solver_black.h b/test/unit/api/solver_black.h index ff0040024..6faab6075 100644 --- a/test/unit/api/solver_black.h +++ b/test/unit/api/solver_black.h @@ -86,8 +86,10 @@ class SolverBlack : public CxxTest::TestSuite void testDefineFun(); void testDefineFunGlobal(); void testDefineFunRec(); + void testDefineFunRecWrongLogic(); void testDefineFunRecGlobal(); void testDefineFunsRec(); + void testDefineFunsRecWrongLogic(); void testDefineFunsRecGlobal(); void testUFIteration(); @@ -1117,6 +1119,19 @@ void SolverBlack::testDefineFunRec() CVC4ApiException&); } +void SolverBlack::testDefineFunRecWrongLogic() +{ + d_solver->setLogic("QF_BV"); + Sort bvSort = d_solver->mkBitVectorSort(32); + Sort funSort = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); + Term b = d_solver->mkVar(bvSort, "b"); + Term v = d_solver->mkConst(bvSort, "v"); + Term f = d_solver->mkConst(funSort, "f"); + TS_ASSERT_THROWS(d_solver->defineFunRec("f", {}, bvSort, v), + CVC4ApiException&); + TS_ASSERT_THROWS(d_solver->defineFunRec(f, {b, b}, v), CVC4ApiException&); +} + void SolverBlack::testDefineFunRecGlobal() { Sort bSort = d_solver->getBooleanSort(); @@ -1214,6 +1229,23 @@ void SolverBlack::testDefineFunsRec() CVC4ApiException&); } +void SolverBlack::testDefineFunsRecWrongLogic() +{ + d_solver->setLogic("QF_BV"); + Sort uSort = d_solver->mkUninterpretedSort("u"); + Sort bvSort = d_solver->mkBitVectorSort(32); + Sort funSort1 = d_solver->mkFunctionSort({bvSort, bvSort}, bvSort); + Sort funSort2 = d_solver->mkFunctionSort(uSort, d_solver->getIntegerSort()); + Term b = d_solver->mkVar(bvSort, "b"); + Term u = d_solver->mkVar(uSort, "u"); + Term v1 = d_solver->mkConst(bvSort, "v1"); + Term v2 = d_solver->mkConst(d_solver->getIntegerSort(), "v2"); + Term f1 = d_solver->mkConst(funSort1, "f1"); + Term f2 = d_solver->mkConst(funSort2, "f2"); + TS_ASSERT_THROWS(d_solver->defineFunsRec({f1, f2}, {{b, b}, {u}}, {v1, v2}), + CVC4ApiException&); +} + void SolverBlack::testDefineFunsRecGlobal() { Sort bSort = d_solver->getBooleanSort(); |