Refactor quantifiers engine initialization (#5813)

This is a step towards breaking up the quantifiers engine.

The key change is that QuantifiersEngine will not be passed as a pointer to the modules it contains. This PR makes it so that necessary modules take a QuantifiersState, which will eventually be extended as needed with additional query methods. For now, modules will take both until the dependencies on QuantifersEngine are removed.

This required that QuantifiersEngine now lives in TheoryQuantifiers, instead of in TheoryEngine, since the QuantifiersEngine must be initialized with QuantifiersState, which is a member of TheoryQuantifiers. Now, TheoryEngine retrieves the QuantifiersEngine from TheoryQuantifiers prior to finishing initialization on theories.

1 files changed, 18 insertions, 14 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 0c3bb181e..7ed183342 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -31,6 +31,7 @@
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_util.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
+#include "theory/quantifiers/quantifiers_state.h"
 #include "theory/quantifiers/skolemize.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
@@ -59,20 +60,14 @@ class QuantifiersEngine {
   typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
 
  public:
-  QuantifiersEngine(TheoryEngine* te, DecisionManager& dm,
+  QuantifiersEngine(quantifiers::QuantifiersState& qstate,
                     ProofNodeManager* pnm);
   ~QuantifiersEngine();
-  /** finish initialize */
-  void finishInit();
   //---------------------- external interface
   /** get theory engine */
   TheoryEngine* getTheoryEngine() const;
   /** Get the decision manager */
   DecisionManager* getDecisionManager();
-  /** get default sat context for quantifiers engine */
-  context::Context* getSatContext();
-  /** get default sat context for quantifiers engine */
-  context::UserContext* getUserContext();
   /** get default output channel for the quantifiers engine */
   OutputChannel& getOutputChannel();
   /** get default valuation for the quantifiers engine */
@@ -110,8 +105,19 @@ class QuantifiersEngine {
   //---------------------- end utilities
  private:
   //---------------------- private initialization
-  /** Set the master equality engine */
-  void setMasterEqualityEngine(eq::EqualityEngine* mee);
+  /**
+   * Finish initialize, which passes pointers to the objects that quantifiers
+   * engine needs but were not available when it was created. This is
+   * called after theories have been created but before they have finished
+   * initialization.
+   *
+   * @param te The theory engine
+   * @param dm The decision manager of the theory engine
+   * @param mee The master equality engine of the theory engine
+   */
+  void finishInit(TheoryEngine* te,
+                  DecisionManager* dm,
+                  eq::EqualityEngine* mee);
   //---------------------- end private initialization
   /**
    * Maps quantified formulas to the module that owns them, if any module has
@@ -329,14 +335,12 @@ public:
   Statistics d_statistics;
 
  private:
+  /** The quantifiers state object */
+  quantifiers::QuantifiersState& d_qstate;
   /** Pointer to theory engine object */
   TheoryEngine* d_te;
-  /** The SAT context */
-  context::Context* d_context;
-  /** The user context */
-  context::UserContext* d_userContext;
   /** Reference to the decision manager of the theory engine */
-  DecisionManager& d_decManager;
+  DecisionManager* d_decManager;
   /** Pointer to the master equality engine */
   eq::EqualityEngine* d_masterEqualityEngine;
   /** vector of utilities for quantifiers */