Introduce quantifiers registry utility (#5829)

This is a simple module for determining which quantifiers module has ownership of quantified formulas.

This is work towards eliminating dependencies of quantifiers modules.

Note that quantifiers attributes module (which no longer has a dependency on QuantifiersEngine after this PR) will be embedded into this module in a later PR.

1 files changed, 2 insertions, 23 deletions

diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index f38a43757..b7a1df8a6 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -113,30 +113,7 @@ class QuantifiersEngine {
    */
   void finishInit(TheoryEngine* te, DecisionManager* dm);
   //---------------------- end private initialization
-  /**
-   * Maps quantified formulas to the module that owns them, if any module has
-   * specifically taken ownership of it.
-   */
-  std::map< Node, QuantifiersModule * > d_owner;
-  /**
-   * The priority value associated with the ownership of quantified formulas
-   * in the domain of the above map, where higher values take higher
-   * precendence.
-   */
-  std::map< Node, int > d_owner_priority;
  public:
-  /** get owner */
-  QuantifiersModule * getOwner( Node q );
-  /**
-   * Set owner of quantified formula q to module m with given priority. If
-   * the quantified formula has previously been assigned an owner with
-   * lower priority, that owner is overwritten.
-   */
-  void setOwner( Node q, QuantifiersModule * m, int priority = 0 );
-  /** set owner of quantified formula q based on its attributes qa. */
-  void setOwner(Node q, quantifiers::QAttributes& qa);
-  /** considers */
-  bool hasOwnership( Node q, QuantifiersModule * m = NULL );
   /** does variable v of quantified formula q have a finite bound? */
   bool isFiniteBound(Node q, Node v) const;
   /** get bound var type
@@ -343,6 +320,8 @@ public:
   /** vector of modules for quantifiers */
   std::vector<QuantifiersModule*> d_modules;
   //------------- quantifiers utilities
+  /** The quantifiers registry */
+  quantifiers::QuantifiersRegistry d_qreg;
   /** all triggers will be stored in this trie */
   std::unique_ptr<inst::TriggerTrie> d_tr_trie;
   /** extended model object */