Minor cleaning of instantiation utilities (#7334)

Also fixes a bug in the quantifiers macro utility which did not compute the instantiation constant body of a quantified formula properly.

This is work towards a major refactoring of conflict-based instantiation / entailment checks.

9 files changed, 61 insertions, 50 deletions

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index 0337d8959..339524d94 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -40,10 +40,8 @@ InstRewriterCegqi::InstRewriterCegqi(InstStrategyCegqi* p)
 {
 }
 
-TrustNode InstRewriterCegqi::rewriteInstantiation(Node q,
-                                                  std::vector<Node>& terms,
-                                                  Node inst,
-                                                  bool doVts)
+TrustNode InstRewriterCegqi::rewriteInstantiation(
+    Node q, const std::vector<Node>& terms, Node inst, bool doVts)
 {
   return d_parent->rewriteInstantiation(q, terms, inst, doVts);
 }
@@ -344,10 +342,8 @@ void InstStrategyCegqi::preRegisterQuantifier(Node q)
     }
   }
 }
-TrustNode InstStrategyCegqi::rewriteInstantiation(Node q,
-                                                  std::vector<Node>& terms,
-                                                  Node inst,
-                                                  bool doVts)
+TrustNode InstStrategyCegqi::rewriteInstantiation(
+    Node q, const std::vector<Node>& terms, Node inst, bool doVts)
 {
   Node prevInst = inst;
   if (doVts)
diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index a568b0b4d..5a886e28d 100644
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -49,7 +49,7 @@ class InstRewriterCegqi : public InstantiationRewriter
    * corresponding to the rewrite and its proof generator.
    */
   TrustNode rewriteInstantiation(Node q,
-                                 std::vector<Node>& terms,
+                                 const std::vector<Node>& terms,
                                  Node inst,
                                  bool doVts) override;
 
@@ -116,7 +116,7 @@ class InstStrategyCegqi : public QuantifiersModule
    * proof generator.
    */
   TrustNode rewriteInstantiation(Node q,
-                                 std::vector<Node>& terms,
+                                 const std::vector<Node>& terms,
                                  Node inst,
                                  bool doVts);
   /** get the instantiation rewriter object */
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index 0807188d5..f756fcfd1 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -485,7 +485,7 @@ bool Instantiate::addInstantiationExpFail(Node q,
 }
 
 void Instantiate::recordInstantiation(Node q,
-                                      std::vector<Node>& terms,
+                                      const std::vector<Node>& terms,
                                       bool doVts)
 {
   Trace("inst-debug") << "Record instantiation for " << q << std::endl;
@@ -497,7 +497,7 @@ void Instantiate::recordInstantiation(Node q,
 }
 
 bool Instantiate::existsInstantiation(Node q,
-                                      std::vector<Node>& terms,
+                                      const std::vector<Node>& terms,
                                       bool modEq)
 {
   if (options::incrementalSolving())
@@ -520,8 +520,8 @@ bool Instantiate::existsInstantiation(Node q,
 }
 
 Node Instantiate::getInstantiation(Node q,
-                                   std::vector<Node>& vars,
-                                   std::vector<Node>& terms,
+                                   const std::vector<Node>& vars,
+                                   const std::vector<Node>& terms,
                                    InferenceId id,
                                    Node pfArg,
                                    bool doVts,
@@ -576,14 +576,17 @@ Node Instantiate::getInstantiation(Node q,
   return body;
 }
 
-Node Instantiate::getInstantiation(Node q, std::vector<Node>& terms, bool doVts)
+Node Instantiate::getInstantiation(Node q,
+                                   const std::vector<Node>& terms,
+                                   bool doVts)
 {
   Assert(d_qreg.d_vars.find(q) != d_qreg.d_vars.end());
   return getInstantiation(
       q, d_qreg.d_vars[q], terms, InferenceId::UNKNOWN, Node::null(), doVts);
 }
 
-bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms)
+bool Instantiate::recordInstantiationInternal(Node q,
+                                              const std::vector<Node>& terms)
 {
   if (options::incrementalSolving())
   {
@@ -601,7 +604,8 @@ bool Instantiate::recordInstantiationInternal(Node q, std::vector<Node>& terms)
   return d_inst_match_trie[q].addInstMatch(d_qstate, q, terms);
 }
 
-bool Instantiate::removeInstantiationInternal(Node q, std::vector<Node>& terms)
+bool Instantiate::removeInstantiationInternal(Node q,
+                                              const std::vector<Node>& terms)
 {
   if (options::incrementalSolving())
   {
diff --git a/src/theory/quantifiers/instantiate.h b/src/theory/quantifiers/instantiate.h
index 753213f35..b4972a7b6 100644
--- a/src/theory/quantifiers/instantiate.h
+++ b/src/theory/quantifiers/instantiate.h
@@ -65,7 +65,7 @@ class InstantiationRewriter
    * and its proof generator.
    */
   virtual TrustNode rewriteInstantiation(Node q,
-                                         std::vector<Node>& terms,
+                                         const std::vector<Node>& terms,
                                          Node inst,
                                          bool doVts) = 0;
 };
@@ -203,7 +203,7 @@ class Instantiate : public QuantifiersUtil
    * but does not enqueue an instantiation lemma.
    */
   void recordInstantiation(Node q,
-                           std::vector<Node>& terms,
+                           const std::vector<Node>& terms,
                            bool doVts = false);
   /** exists instantiation
    *
@@ -212,7 +212,7 @@ class Instantiate : public QuantifiersUtil
    *   modEq : whether to check for duplication modulo equality
    */
   bool existsInstantiation(Node q,
-                           std::vector<Node>& terms,
+                           const std::vector<Node>& terms,
                            bool modEq = false);
   //--------------------------------------general utilities
   /** get instantiation
@@ -225,8 +225,8 @@ class Instantiate : public QuantifiersUtil
    * single INSTANTIATE step concluding the instantiated body of q from q.
    */
   Node getInstantiation(Node q,
-                        std::vector<Node>& vars,
-                        std::vector<Node>& terms,
+                        const std::vector<Node>& vars,
+                        const std::vector<Node>& terms,
                         InferenceId id = InferenceId::UNKNOWN,
                         Node pfArg = Node::null(),
                         bool doVts = false,
@@ -235,7 +235,9 @@ class Instantiate : public QuantifiersUtil
    *
    * Same as above but with vars equal to the bound variables of q.
    */
-  Node getInstantiation(Node q, std::vector<Node>& terms, bool doVts = false);
+  Node getInstantiation(Node q,
+                        const std::vector<Node>& terms,
+                        bool doVts = false);
   //--------------------------------------end general utilities
 
   /**
@@ -297,9 +299,9 @@ class Instantiate : public QuantifiersUtil
 
  private:
   /** record instantiation, return true if it was not a duplicate */
-  bool recordInstantiationInternal(Node q, std::vector<Node>& terms);
+  bool recordInstantiationInternal(Node q, const std::vector<Node>& terms);
   /** remove instantiation from the cache */
-  bool removeInstantiationInternal(Node q, std::vector<Node>& terms);
+  bool removeInstantiationInternal(Node q, const std::vector<Node>& terms);
   /**
    * Ensure that n has type tn, return a term equivalent to it for that type
    * if possible.
diff --git a/src/theory/quantifiers/quant_module.cpp b/src/theory/quantifiers/quant_module.cpp
index 8fb37c548..db4eb9d34 100644
--- a/src/theory/quantifiers/quant_module.cpp
+++ b/src/theory/quantifiers/quant_module.cpp
@@ -76,5 +76,10 @@ quantifiers::QuantifiersRegistry& QuantifiersModule::getQuantifiersRegistry()
   return d_qreg;
 }
 
+quantifiers::TermRegistry& QuantifiersModule::getTermRegistry()
+{
+  return d_treg;
+}
+
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers/quant_module.h b/src/theory/quantifiers/quant_module.h
index 639f9c2b4..ce6c1b04c 100644
--- a/src/theory/quantifiers/quant_module.h
+++ b/src/theory/quantifiers/quant_module.h
@@ -167,6 +167,8 @@ class QuantifiersModule : protected EnvObj
   quantifiers::QuantifiersInferenceManager& getInferenceManager();
   /** get the quantifiers registry */
   quantifiers::QuantifiersRegistry& getQuantifiersRegistry();
+  /** get the term registry */
+  quantifiers::TermRegistry& getTermRegistry();
   //----------------------------end general queries
  protected:
   /** Reference to the state of the quantifiers engine */
diff --git a/src/theory/quantifiers/quantifiers_macros.cpp b/src/theory/quantifiers/quantifiers_macros.cpp
index a3bdf10ad..9b9580b02 100644
--- a/src/theory/quantifiers/quantifiers_macros.cpp
+++ b/src/theory/quantifiers/quantifiers_macros.cpp
@@ -88,7 +88,7 @@ Node QuantifiersMacros::solve(Node lit, bool reqGround)
             << "...does not contain bad (recursive) operator." << std::endl;
         // must be ground UF term if mode is GROUND_UF
         if (options::macrosQuantMode() != options::MacrosQuantMode::GROUND_UF
-            || preservesTriggerVariables(body, n_def))
+            || preservesTriggerVariables(lit, n_def))
         {
           Trace("macros-debug")
               << "...respects ground-uf constraint." << std::endl;
@@ -139,6 +139,7 @@ bool QuantifiersMacros::containsBadOp(Node n, Node op, bool reqGround)
 
 bool QuantifiersMacros::preservesTriggerVariables(Node q, Node n)
 {
+  Assert(q.getKind() == FORALL) << "Expected quantified formula, got " << q;
   Node icn = d_qreg.substituteBoundVariablesToInstConstants(n, q);
   Trace("macros-debug2") << "Get free variables in " << icn << std::endl;
   std::vector<Node> var;
diff --git a/src/theory/quantifiers/quantifiers_registry.cpp b/src/theory/quantifiers/quantifiers_registry.cpp
index 6d5e00363..487bcc0fe 100644
--- a/src/theory/quantifiers/quantifiers_registry.cpp
+++ b/src/theory/quantifiers/quantifiers_registry.cpp
@@ -38,6 +38,7 @@ void QuantifiersRegistry::registerQuantifier(Node q)
   {
     return;
   }
+  Assert(q.getKind() == kind::FORALL);
   NodeManager* nm = NodeManager::currentNM();
   Debug("quantifiers-engine")
       << "Instantiation constants for " << q << " : " << std::endl;
@@ -144,42 +145,42 @@ Node QuantifiersRegistry::substituteBoundVariablesToInstConstants(Node n,
                                                                   Node q)
 {
   registerQuantifier(q);
-  return n.substitute(d_vars[q].begin(),
-                      d_vars[q].end(),
-                      d_inst_constants[q].begin(),
-                      d_inst_constants[q].end());
+  std::vector<Node>& vars = d_vars.at(q);
+  std::vector<Node>& consts = d_inst_constants.at(q);
+  Assert(vars.size() == q[0].getNumChildren());
+  Assert(vars.size() == consts.size());
+  return n.substitute(vars.begin(), vars.end(), consts.begin(), consts.end());
 }
 
 Node QuantifiersRegistry::substituteInstConstantsToBoundVariables(Node n,
                                                                   Node q)
 {
   registerQuantifier(q);
-  return n.substitute(d_inst_constants[q].begin(),
-                      d_inst_constants[q].end(),
-                      d_vars[q].begin(),
-                      d_vars[q].end());
+  std::vector<Node>& vars = d_vars.at(q);
+  std::vector<Node>& consts = d_inst_constants.at(q);
+  Assert(vars.size() == q[0].getNumChildren());
+  Assert(vars.size() == consts.size());
+  return n.substitute(consts.begin(), consts.end(), vars.begin(), vars.end());
 }
 
-Node QuantifiersRegistry::substituteBoundVariables(Node n,
-                                                   Node q,
-                                                   std::vector<Node>& terms)
+Node QuantifiersRegistry::substituteBoundVariables(
+    Node n, Node q, const std::vector<Node>& terms)
 {
   registerQuantifier(q);
-  Assert(d_vars[q].size() == terms.size());
-  return n.substitute(
-      d_vars[q].begin(), d_vars[q].end(), terms.begin(), terms.end());
+  std::vector<Node>& vars = d_vars.at(q);
+  Assert(vars.size() == q[0].getNumChildren());
+  Assert(vars.size() == terms.size());
+  return n.substitute(vars.begin(), vars.end(), terms.begin(), terms.end());
 }
 
-Node QuantifiersRegistry::substituteInstConstants(Node n,
-                                                  Node q,
-                                                  std::vector<Node>& terms)
+Node QuantifiersRegistry::substituteInstConstants(
+    Node n, Node q, const std::vector<Node>& terms)
 {
   registerQuantifier(q);
-  Assert(d_inst_constants[q].size() == terms.size());
-  return n.substitute(d_inst_constants[q].begin(),
-                      d_inst_constants[q].end(),
-                      terms.begin(),
-                      terms.end());
+  std::vector<Node>& consts = d_inst_constants.at(q);
+  Assert(consts.size() == q[0].getNumChildren());
+  Assert(consts.size() == terms.size());
+  return n.substitute(consts.begin(), consts.end(), terms.begin(), terms.end());
 }
 
 QuantAttributes& QuantifiersRegistry::getQuantAttributes()
diff --git a/src/theory/quantifiers/quantifiers_registry.h b/src/theory/quantifiers/quantifiers_registry.h
index 559939bbe..858a85cae 100644
--- a/src/theory/quantifiers/quantifiers_registry.h
+++ b/src/theory/quantifiers/quantifiers_registry.h
@@ -84,9 +84,9 @@ class QuantifiersRegistry : public QuantifiersUtil
    */
   Node substituteInstConstantsToBoundVariables(Node n, Node q);
   /** substitute { variables of q -> terms } in n */
-  Node substituteBoundVariables(Node n, Node q, std::vector<Node>& terms);
+  Node substituteBoundVariables(Node n, Node q, const std::vector<Node>& terms);
   /** substitute { instantiation constants of q -> terms } in n */
-  Node substituteInstConstants(Node n, Node q, std::vector<Node>& terms);
+  Node substituteInstConstants(Node n, Node q, const std::vector<Node>& terms);
   //----------------------------- end instantiation constants
   /** Get quantifiers attributes utility class */
   QuantAttributes& getQuantAttributes();