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, 47 insertions, 3 deletions

diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
index 59db1dfe2..b89a2c01b 100644
--- a/src/theory/quantifiers/quantifiers_registry.h
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -18,6 +18,7 @@
 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REGISTRY_H
 
 #include "expr/node.h"
+#include "theory/quantifiers/quant_util.h"
 
 namespace CVC4 {
 namespace theory {
@@ -26,15 +27,29 @@ class QuantifiersModule;
 
 namespace quantifiers {
 
+class Instantiate;
+
 /**
  * The quantifiers registry, which manages basic information about which
- * quantifiers modules have ownership of quantified formulas.
+ * quantifiers modules have ownership of quantified formulas, and manages
+ * the allocation of instantiation constants per quantified formula.
  */
-class QuantifiersRegistry
+class QuantifiersRegistry : public QuantifiersUtil
 {
+  friend class Instantiate;
+
  public:
   QuantifiersRegistry() {}
   ~QuantifiersRegistry() {}
+  /**
+   * Register quantifier, which allocates the instantiation constants for q.
+   */
+  void registerQuantifier(Node q) override;
+  /** reset */
+  bool reset(Theory::Effort e) override;
+  /** identify */
+  std::string identify() const override;
+  //----------------------------- ownership
   /** get the owner of quantified formula q */
   QuantifiersModule* getOwner(Node q) const;
   /**
@@ -47,7 +62,28 @@ class QuantifiersRegistry
    * Return true if module q has no owner registered or if its registered owner is m.
    */
   bool hasOwnership(Node q, QuantifiersModule* m) const;
-
+  //----------------------------- end ownership
+  //----------------------------- instantiation constants
+  /** get the i^th instantiation constant of q */
+  Node getInstantiationConstant(Node q, size_t i) const;
+  /** get number of instantiation constants for q */
+  size_t getNumInstantiationConstants(Node q) const;
+  /** get the ce body q[e/x] */
+  Node getInstConstantBody(Node q);
+  /** returns node n with bound vars of q replaced by instantiation constants of
+     q node n : is the future pattern node q : is the quantifier containing
+     which bind the variable return a pattern where the variable are replaced by
+     variable for instantiation.
+   */
+  Node substituteBoundVariablesToInstConstants(Node n, Node q);
+  /** substitute { instantiation constants of q -> bound variables of q } in n
+   */
+  Node substituteInstConstantsToBoundVariables(Node n, Node q);
+  /** substitute { variables of q -> terms } in n */
+  Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
+  /** substitute { instantiation constants of q -> terms } in n */
+  Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
+  //----------------------------- end instantiation constants
  private:
   /**
    * Maps quantified formulas to the module that owns them, if any module has
@@ -60,6 +96,14 @@ class QuantifiersRegistry
    * precendence.
    */
   std::map<Node, int32_t> d_owner_priority;
+  /** map from universal quantifiers to the list of variables */
+  std::map<Node, std::vector<Node> > d_vars;
+  /** map from universal quantifiers to their inst constant body */
+  std::map<Node, Node> d_inst_const_body;
+  /** instantiation constants to universal quantifiers */
+  std::map<Node, Node> d_inst_constants_map;
+  /** map from universal quantifiers to the list of instantiation constants */
+  std::map<Node, std::vector<Node> > d_inst_constants;
 };
 
 }  // namespace quantifiers