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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 55bf68b9ff202cd47ea10d144d9a44c6cbb79a6d..3eedfdf5315dc2776b707459e1f5d500a2b89675 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1135,6 +1135,14 @@ Result SmtEngine::checkSynth()
    --------------------------------------------------------------------------
 */
 
+void SmtEngine::declarePool(const Node& p, const std::vector<Node>& initValue)
+{
+  Assert(p.isVar() && p.getType().isSet());
+  finishInit();
+  QuantifiersEngine* qe = getAvailableQuantifiersEngine("declareTermPool");
+  qe->declarePool(p, initValue);
+}
+
 Node SmtEngine::simplify(const Node& ex)
 {
   SmtScope smts(this);

diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 51eed32b2bff5949cd07bf56d122385d1c29e910..3ef1904473dcce73541f82645338d0fb84e96f1e 100644 (file)
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -496,6 +496,17 @@ class CVC4_EXPORT SmtEngine
 
   /*------------------------- end of sygus commands ------------------------*/
 
+  /**
+   * Declare pool whose initial value is the terms in initValue. A pool is
+   * a variable of type (Set T) that is used in quantifier annotations and does
+   * not occur in constraints.
+   *
+   * @param p The pool to declare, which should be a variable of type (Set T)
+   * for some type T.
+   * @param initValue The initial value of p, which should be a vector of terms
+   * of type T.
+   */
+  void declarePool(const Node& p, const std::vector<Node>& initValue);
   /**
    * Simplify a formula without doing "much" work.  Does not involve
    * the SAT Engine in the simplification, but uses the current

diff --git a/src/theory/quantifiers/inst_strategy_pool.h b/src/theory/quantifiers/inst_strategy_pool.h
index e45f08bc2da837018686d1f7abea060685ccd601..8eceaf35a114181a8e4d4c89812d78cde2c16e38 100644 (file)
--- 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 b45380f5e9b99885e23b30e5aaa50a0f953e44f1..5f83578dfd4738d5af7c410b2e415f105b214600 100644 (file)
--- 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 64dc7024644cbffa959c6aa91117fa535acf455f..f89bdf1f2174085d57ac2d4c8214a773c58c0e92 100644 (file)
--- 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 2f3d0bdcfaa41168b3a5d237387c8419aaec826f..0a72945c15014fd658cc2f17282b72fa1c076224 100644 (file)
--- 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 d0825f1f571e932eb1bf24bfc4e87e8588d65d48..0f7c659241e5b762a8c59214d64e4a5f04b01bca 100644 (file)
--- 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 ece2ce568ec72a44bf00d52393b0579b88d1ccf5..90e780c446ba724b4b269055edb14b97767d30a2 100644 (file)
--- 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 f72228c5bd91d45bb0d5d391276f8189760e26f6..148dff1b6475d1ca451969d04b56d9c434df74a6 100644 (file)
--- 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 43eec9499f5e707b43b77c99ed5be980355f6451..aa0fbd06d958e5fe618e0a6de2b46b3c21642eec 100644 (file)
--- 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 4e34d607416b8cb31ae533eea1f9bae74a496668..0664340a7ba037f336e52057eee8b6b27b7eae93 100644 (file)
--- 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 5a582cea83fe80381ec5d1472fd72aef802dfd1c..5916390a64a0329b597ac1ec4499fb2f670a22be 100644 (file)
--- 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 0a54f37eaf61f34d40287bcf1c4ee459349a6dc6..bed73d1fb67a37ea6bd29ec4e538c27b879c7c6e 100644 (file)
--- 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: