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).

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();