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, 21 insertions, 1 deletions

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index c7a37c007..b1e3313d8 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -65,6 +65,12 @@ class StatisticsRegistry;
 
 /* -------------------------------------------------------------------------- */
 
+namespace api {
+class Solver;
+}  // namespace api
+
+/* -------------------------------------------------------------------------- */
+
 namespace context {
   class Context;
   class UserContext;
@@ -126,6 +132,7 @@ namespace theory {
 
 class CVC4_PUBLIC SmtEngine
 {
+  friend class ::CVC4::api::Solver;
   // TODO (Issue #1096): Remove this friend relationship.
   friend class ::CVC4::preprocessing::PreprocessingPassContext;
   friend class ::CVC4::smt::SmtEnginePrivate;
@@ -207,6 +214,9 @@ class CVC4_PUBLIC SmtEngine
   /** Get the logic information currently set. */
   LogicInfo getLogicInfo() const;
 
+  /** Get the logic information set by the user. */
+  LogicInfo getUserLogicInfo() const;
+
   /**
    * Set information about the script executing.
    * @throw OptionException, ModalException
@@ -875,6 +885,9 @@ class CVC4_PUBLIC SmtEngine
   SmtEngine(const SmtEngine&) = delete;
   SmtEngine& operator=(const SmtEngine&) = delete;
 
+  /** Set solver instance that owns this SmtEngine. */
+  void setSolver(api::Solver* solver) { d_solver = solver; }
+
   /** Get a pointer to the TheoryEngine owned by this SmtEngine. */
   TheoryEngine* getTheoryEngine() { return d_theoryEngine.get(); }
 
@@ -1082,6 +1095,9 @@ class CVC4_PUBLIC SmtEngine
 
   /* Members -------------------------------------------------------------- */
 
+  /** Solver instance that owns this SmtEngine instance. */
+  api::Solver* d_solver = nullptr;
+
   /** Expr manager context */
   std::unique_ptr<context::Context> d_context;
   /** User level context */
@@ -1197,10 +1213,14 @@ class CVC4_PUBLIC SmtEngine
   std::vector<Command*> d_defineCommands;
 
   /**
-   * The logic we're in.
+   * The logic we're in. This logic may be an extension of the logic set by the
+   * user.
    */
   LogicInfo d_logic;
 
+  /** The logic set by the user. */
+  LogicInfo d_userLogic;
+
   /**
    * Keep a copy of the original option settings (for reset()).
    */