Move methods from term util to quantifiers registry (#5916)

Towards eliminating dependencies on quantifiers engine, and eliminating the TermUtil class.

Note that QuantifiersModule had to be moved to its own file to avoid circular include dependencies.

1 files changed, 5 insertions, 153 deletions

diff --git a/src/theory/quantifiers/quant_util.h b/src/theory/quantifiers/quant_util.h
index 551143e40..e0cb11712 100644
--- a/src/theory/quantifiers/quant_util.h
+++ b/src/theory/quantifiers/quant_util.h
@@ -21,165 +21,17 @@
 #include <map>
 #include <vector>
 
-#include "theory/quantifiers/quantifiers_inference_manager.h"
-#include "theory/quantifiers/quantifiers_registry.h"
-#include "theory/quantifiers/quantifiers_state.h"
+#include "expr/node.h"
 #include "theory/theory.h"
-#include "theory/uf/equality_engine.h"
 
 namespace CVC4 {
 namespace theory {
 
-class QuantifiersEngine;
-
-namespace quantifiers {
-  class TermDb;
-  class TermUtil;
-}
-
-/** QuantifiersModule class
-*
-* This is the virtual class for defining subsolvers of the quantifiers theory.
-* It has a similar interface to a Theory object.
-*/
-class QuantifiersModule {
- public:
-  /** effort levels for quantifiers modules check */
-  enum QEffort
-  {
-    // conflict effort, for conflict-based instantiation
-    QEFFORT_CONFLICT,
-    // standard effort, for heuristic instantiation
-    QEFFORT_STANDARD,
-    // model effort, for model-based instantiation
-    QEFFORT_MODEL,
-    // last call effort, for last resort techniques
-    QEFFORT_LAST_CALL,
-    // none
-    QEFFORT_NONE,
-  };
-
- public:
-  QuantifiersModule(quantifiers::QuantifiersState& qs,
-                    quantifiers::QuantifiersInferenceManager& qim,
-                    quantifiers::QuantifiersRegistry& qr,
-                    QuantifiersEngine* qe);
-  virtual ~QuantifiersModule(){}
-  /** Presolve.
-   *
-   * Called at the beginning of check-sat call.
-   */
-  virtual void presolve() {}
-  /** Needs check.
-   *
-   * Returns true if this module wishes a call to be made
-   * to check(e) during QuantifiersEngine::check(e).
-   */
-  virtual bool needsCheck( Theory::Effort e ) { return e>=Theory::EFFORT_LAST_CALL; }
-  /** Needs model.
-   *
-   * Whether this module needs a model built during a
-   * call to QuantifiersEngine::check(e)
-   * It returns one of QEFFORT_* from quantifiers_engine.h,
-   * which specifies the quantifiers effort in which it requires the model to
-   * be built.
-   */
-  virtual QEffort needsModel(Theory::Effort e);
-  /** Reset.
-   *
-   * Called at the beginning of QuantifiersEngine::check(e).
-   */
-  virtual void reset_round( Theory::Effort e ){}
-  /** Check.
-   *
-   *   Called during QuantifiersEngine::check(e) depending
-   *   if needsCheck(e) returns true.
-   */
-  virtual void check(Theory::Effort e, QEffort quant_e) = 0;
-  /** Check complete?
-   *
-   * Returns false if the module's reasoning was globally incomplete
-   * (e.g. "sat" must be replaced with "incomplete").
-   *
-   * This is called just before the quantifiers engine will return
-   * with no lemmas added during a LAST_CALL effort check.
-   */
-  virtual bool checkComplete() { return true; }
-  /** Check was complete for quantified formula q
-   *
-   * If for each quantified formula q, some module returns true for
-   * checkCompleteFor( q ),
-   * and no lemmas are added by the quantifiers theory, then we may answer
-   * "sat", unless
-   * we are incomplete for other reasons.
-   */
-  virtual bool checkCompleteFor( Node q ) { return false; }
-  /** Check ownership
-   *
-   * Called once for new quantified formulas that are registered by the
-   * quantifiers theory. The primary purpose of this function is to establish
-   * if this module is the owner of quantified formula q.
-   */
-  virtual void checkOwnership(Node q) {}
-  /** Register quantifier
-   *
-   * Called once for new quantified formulas q that are pre-registered by the
-   * quantifiers theory, after internal ownership of quantified formulas is
-   * finalized. This does context-independent initialization of this module
-   * for quantified formula q.
-   */
-  virtual void registerQuantifier(Node q) {}
-  /** Pre-register quantifier
-   *
-   * Called once for new quantified formulas that are
-   * pre-registered by the quantifiers theory, after
-   * internal ownership of quantified formulas is finalized.
-   */
-  virtual void preRegisterQuantifier(Node q) {}
-  /** Assert node.
-   *
-   * Called when a quantified formula q is asserted to the quantifiers theory
-   */
-  virtual void assertNode(Node q) {}
-  /** Identify this module (for debugging, dynamic configuration, etc..) */
-  virtual std::string identify() const = 0;
-  //----------------------------general queries
-  /** get currently used the equality engine */
-  eq::EqualityEngine* getEqualityEngine() const;
-  /** are n1 and n2 equal in the current used equality engine? */
-  bool areEqual(TNode n1, TNode n2) const;
-  /** are n1 and n2 disequal in the current used equality engine? */
-  bool areDisequal(TNode n1, TNode n2) const;
-  /** get the representative of n in the current used equality engine */
-  TNode getRepresentative(TNode n) const;
-  /** get quantifiers engine that owns this module */
-  QuantifiersEngine* getQuantifiersEngine() const;
-  /** get currently used term database */
-  quantifiers::TermDb* getTermDatabase() const;
-  /** get currently used term utility object */
-  quantifiers::TermUtil* getTermUtil() const;
-  /** get the quantifiers state */
-  quantifiers::QuantifiersState& getState();
-  /** get the quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& getInferenceManager();
-  //----------------------------end general queries
- protected:
-  /** pointer to the quantifiers engine that owns this module */
-  QuantifiersEngine* d_quantEngine;
-  /** The state of the quantifiers engine */
-  quantifiers::QuantifiersState& d_qstate;
-  /** The quantifiers inference manager */
-  quantifiers::QuantifiersInferenceManager& d_qim;
-  /** The quantifiers registry */
-  quantifiers::QuantifiersRegistry& d_qreg;
-};/* class QuantifiersModule */
-
 /** Quantifiers utility
-*
-* This is a lightweight version of a quantifiers module that does not implement
-* methods
-* for checking satisfiability.
-*/
+ *
+ * This is a lightweight version of a quantifiers module that does not implement
+ * methods for checking satisfiability.
+ */
 class QuantifiersUtil {
 public:
   QuantifiersUtil(){}