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

1 files changed, 12 insertions, 0 deletions

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)