Add internal API methods for pool-based instantiation (#6350)

11 files changed, 41 insertions, 14 deletions

diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h
index e45f08bc2..8eceaf35a 100644
--- a/src/theory/quantifiers/inst_strategy_pool.h
+++ b/src/theory/quantifiers/inst_strategy_pool.h
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
-#define CVC4__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
+#ifndef CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
+#define CVC5__THEORY__QUANTIFIERS__INST_STRATEGY_POOL_H
 
 #include "theory/quantifiers/quant_module.h"
 
diff --git a/src/theory/quantifiers/instantiate.cpp b/src/theory/quantifiers/instantiate.cpp
index b45380f5e..5f83578df 100644
--- a/src/theory/quantifiers/instantiate.cpp
+++ b/src/theory/quantifiers/instantiate.cpp
@@ -378,6 +378,7 @@ bool Instantiate::addInstantiation(Node q,
           orig_body, q[1], maxInstLevel + 1);
     }
   }
+  d_treg.processInstantiation(q, terms);
   Trace("inst-add-debug") << " --> Success." << std::endl;
   ++(d_statistics.d_instantiations);
   return true;
diff --git a/src/theory/quantifiers/quantifiers_attributes.cpp b/src/theory/quantifiers/quantifiers_attributes.cpp
index 64dc70246..f89bdf1f2 100644
--- a/src/theory/quantifiers/quantifiers_attributes.cpp
+++ b/src/theory/quantifiers/quantifiers_attributes.cpp
@@ -186,10 +186,20 @@ void QuantAttributes::computeQuantAttributes( Node q, QAttributes& qa ){
   if( q.getNumChildren()==3 ){
     qa.d_ipl = q[2];
     for( unsigned i=0; i<q[2].getNumChildren(); i++ ){
-      Trace("quant-attr-debug") << "Check : " << q[2][i] << " " << q[2][i].getKind() << std::endl;
-      if( q[2][i].getKind()==INST_PATTERN || q[2][i].getKind()==INST_NO_PATTERN ){
+      Kind k = q[2][i].getKind();
+      Trace("quant-attr-debug")
+          << "Check : " << q[2][i] << " " << k << std::endl;
+      if (k == INST_PATTERN || k == INST_NO_PATTERN)
+      {
         qa.d_hasPattern = true;
-      }else if( q[2][i].getKind()==INST_ATTRIBUTE ){
+      }
+      else if (k == INST_POOL || k == INST_ADD_TO_POOL
+               || k == SKOLEM_ADD_TO_POOL)
+      {
+        qa.d_hasPool = true;
+      }
+      else if (k == INST_ATTRIBUTE)
+      {
         Node avar = q[2][i][0];
         if( avar.getAttribute(FunDefAttribute()) ){
           Trace("quant-attr") << "Attribute : function definition : " << q << std::endl;
diff --git a/src/theory/quantifiers/quantifiers_attributes.h b/src/theory/quantifiers/quantifiers_attributes.h
index 2f3d0bdcf..0a72945c1 100644
--- a/src/theory/quantifiers/quantifiers_attributes.h
+++ b/src/theory/quantifiers/quantifiers_attributes.h
@@ -119,6 +119,7 @@ struct QAttributes
  public:
   QAttributes()
       : d_hasPattern(false),
+        d_hasPool(false),
         d_sygus(false),
         d_qinstLevel(-1),
         d_quant_elim(false),
@@ -129,6 +130,8 @@ struct QAttributes
   ~QAttributes(){}
   /** does the quantified formula have a pattern? */
   bool d_hasPattern;
+  /** does the quantified formula have a pool? */
+  bool d_hasPool;
   /** if non-null, this quantified formula is a function definition for function
    * d_fundef_f */
   Node d_fundef_f;
diff --git a/src/theory/quantifiers/quantifiers_inference_manager.cpp b/src/theory/quantifiers/quantifiers_inference_manager.cpp
index d0825f1f5..0f7c65924 100644
--- a/src/theory/quantifiers/quantifiers_inference_manager.cpp
+++ b/src/theory/quantifiers/quantifiers_inference_manager.cpp
@@ -30,7 +30,7 @@ QuantifiersInferenceManager::QuantifiersInferenceManager(
     ProofNodeManager* pnm)
     : InferenceManagerBuffered(t, state, pnm, "theory::quantifiers"),
       d_instantiate(new Instantiate(state, *this, qr, tr, pnm)),
-      d_skolemize(new Skolemize(state, pnm))
+      d_skolemize(new Skolemize(state, tr, pnm))
 {
 }
 
diff --git a/src/theory/quantifiers/skolemize.cpp b/src/theory/quantifiers/skolemize.cpp
index ece2ce568..90e780c44 100644
--- a/src/theory/quantifiers/skolemize.cpp
+++ b/src/theory/quantifiers/skolemize.cpp
@@ -24,6 +24,7 @@
 #include "options/smt_options.h"
 #include "theory/quantifiers/quantifiers_attributes.h"
 #include "theory/quantifiers/quantifiers_state.h"
+#include "theory/quantifiers/term_registry.h"
 #include "theory/quantifiers/term_util.h"
 #include "theory/rewriter.h"
 #include "theory/sort_inference.h"
@@ -34,8 +35,11 @@ namespace cvc5 {
 namespace theory {
 namespace quantifiers {
 
-Skolemize::Skolemize(QuantifiersState& qs, ProofNodeManager* pnm)
+Skolemize::Skolemize(QuantifiersState& qs,
+                     TermRegistry& tr,
+                     ProofNodeManager* pnm)
     : d_qstate(qs),
+      d_treg(tr),
       d_skolemized(qs.getUserContext()),
       d_pnm(pnm),
       d_epg(pnm == nullptr ? nullptr
@@ -91,6 +95,8 @@ TrustNode Skolemize::process(Node q)
     lem = nb;
   }
   d_skolemized[q] = lem;
+  // triggered when skolemizing
+  d_treg.processSkolemization(q, d_skolem_constants[q]);
   return TrustNode::mkTrustLemma(lem, pg);
 }
 
diff --git a/src/theory/quantifiers/skolemize.h b/src/theory/quantifiers/skolemize.h
index f72228c5b..148dff1b6 100644
--- a/src/theory/quantifiers/skolemize.h
+++ b/src/theory/quantifiers/skolemize.h
@@ -32,12 +32,10 @@ namespace cvc5 {
 class DTypeConstructor;
 
 namespace theory {
-
-class SortInference;
-
 namespace quantifiers {
 
 class QuantifiersState;
+class TermRegistry;
 
 /** Skolemization utility
  *
@@ -70,7 +68,7 @@ class Skolemize
   typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap;
 
  public:
-  Skolemize(QuantifiersState& qs, ProofNodeManager* pnm);
+  Skolemize(QuantifiersState& qs, TermRegistry& tr, ProofNodeManager* pnm);
   ~Skolemize() {}
   /** skolemize quantified formula q
    * If the return value ret of this function is non-null, then ret is a trust
@@ -143,6 +141,8 @@ class Skolemize
                          std::vector<Node>& selfSel);
   /** Reference to the quantifiers state */
   QuantifiersState& d_qstate;
+  /** Reference to the term registry */
+  TermRegistry& d_treg;
   /** quantified formulas that have been skolemized */
   NodeNodeMap d_skolemized;
   /** map from quantified formulas to the list of skolem constants */
diff --git a/src/theory/quantifiers/term_pools.cpp b/src/theory/quantifiers/term_pools.cpp
index 43eec9499..aa0fbd06d 100644
--- a/src/theory/quantifiers/term_pools.cpp
+++ b/src/theory/quantifiers/term_pools.cpp
@@ -81,6 +81,7 @@ void TermPools::registerPool(Node p, const std::vector<Node>& initValue)
   d.initialize();
   for (const Node& i : initValue)
   {
+    Assert(i.getType().isComparableTo(p.getType().getSetElementType()));
     d.add(i);
   }
 }
@@ -156,4 +157,4 @@ void TermPools::processInternal(Node q,
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace cvc5
diff --git a/src/theory/quantifiers/term_pools.h b/src/theory/quantifiers/term_pools.h
index 4e34d6074..0664340a7 100644
--- a/src/theory/quantifiers/term_pools.h
+++ b/src/theory/quantifiers/term_pools.h
@@ -103,6 +103,6 @@ class TermPools : public QuantifiersUtil
 
 }  // namespace quantifiers
 }  // namespace theory
-}  // namespace CVC5
+}  // namespace cvc5
 
 #endif /* CVC5__THEORY__QUANTIFIERS__TERM_POOLS_H */
diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp
index 5a582cea8..5916390a6 100644
--- a/src/theory/quantifiers_engine.cpp
+++ b/src/theory/quantifiers_engine.cpp
@@ -65,6 +65,7 @@ QuantifiersEngine::QuantifiersEngine(
   d_util.push_back(&d_qreg);
   d_util.push_back(tr.getTermDatabase());
   d_util.push_back(qim.getInstantiate());
+  d_util.push_back(tr.getTermPools());
 }
 
 QuantifiersEngine::~QuantifiersEngine() {}
@@ -653,6 +654,10 @@ bool QuantifiersEngine::getSynthSolutions(
 {
   return d_qmodules->d_synth_e->getSynthSolutions(sol_map);
 }
+void QuantifiersEngine::declarePool(Node p, const std::vector<Node>& initValue)
+{
+  d_treg.declarePool(p, initValue);
+}
 
 }  // namespace theory
 }  // namespace cvc5
diff --git a/src/theory/quantifiers_engine.h b/src/theory/quantifiers_engine.h
index 0a54f37ea..bed73d1fb 100644
--- a/src/theory/quantifiers_engine.h
+++ b/src/theory/quantifiers_engine.h
@@ -172,7 +172,8 @@ public:
   * SynthConjecture::getSynthSolutions.
   */
  bool getSynthSolutions(std::map<Node, std::map<Node, Node> >& sol_map);
-
+ /** Declare pool */
+ void declarePool(Node p, const std::vector<Node>& initValue);
  //----------end user interface for instantiations
 
  private: