Add logic check for define-fun(s)-rec (#4577)
authorAndres Noetzli <andres.noetzli@gmail.com>
Fri, 19 Jun 2020 05:51:50 +0000 (22:51 -0700)
committerGitHub <noreply@github.com>
Fri, 19 Jun 2020 05:51:50 +0000 (22:51 -0700)
commite8884b9b8ba86ce71807887cab87a5188cce4003
tree3b56553ecc3227eafe7aca057c5e29cd8efb63e0
parent3054cd99db968eb85a9195b12e17e83a334e00cb
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).
src/api/cvc4cpp.cpp
src/parser/cvc/Cvc.g
src/parser/smt2/Smt2.g
src/printer/smt2/smt2_printer.cpp
src/smt/command.cpp
src/smt/command.h
src/smt/smt_engine.cpp
src/smt/smt_engine.h
test/regress/CMakeLists.txt
test/regress/regress0/smtlib/define-fun-rec-logic.smt2 [new file with mode: 0644]
test/unit/api/solver_black.h