Move VTS term cache to term registry (#8656)

This is in preparation for simplifying the interface to Instantiate::addInstantiation, where the VTS cache can be consulted to ask if VTS is necessary.

diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
index e468ae0019cf8b93a4bef788f2be4f14f1be65c9..d8119e45f90bca70595cb6ca209774b05f4f3868 100644 (file)
--- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
+++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp
@@ -1010,7 +1010,9 @@ Node ArithInstantiator::mkVtsSum(const Node& val,
   {
     // create delta here if necessary
     vval = nm->mkNode(
-        ADD, vval, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta()));
+        ADD,
+        vval,
+        nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta(false, true)));
   }
   vval = rewrite(vval);
   return vval;

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
index cffe42ae27294f09a8f72b05f57e218ddf73ed37..37aeaedcb07acb04f3f7cef7219a5481af57ab04 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp
@@ -56,11 +56,11 @@ InstStrategyCegqi::InstStrategyCegqi(Env& env,
       d_cbqi_set_quant_inactive(false),
       d_incomplete_check(false),
       d_added_cbqi_lemma(userContext()),
-      d_vtsCache(new VtsTermCache(env, qim)),
       d_bv_invert(nullptr),
       d_small_const_multiplier(NodeManager::currentNM()->mkConstReal(
           Rational(1) / Rational(1000000))),
-      d_small_const(d_small_const_multiplier)
+      d_small_const(d_small_const_multiplier),
+      d_freeDeltaLb(false, userContext())
 {
   d_check_vts_lemma_lc = false;
   if (options().quantifiers.cegqiBv)
@@ -355,7 +355,8 @@ TrustNode InstStrategyCegqi::rewriteInstantiation(
     // do virtual term substitution
     inst = rewrite(inst);
     Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl;
-    inst = d_vtsCache->rewriteVtsSymbols(inst);
+    VtsTermCache* vtc = d_treg.getVtsTermCache();
+    inst = vtc->rewriteVtsSymbols(inst);
     Trace("quant-vts-debug") << "...got " << inst << std::endl;
   }
   if (prevInst != inst)
@@ -424,38 +425,61 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) {
     // don't need to process this, since it has been reduced
     return;
   }
+  // run the check
   if( e==0 ){
     CegInstantiator * cinst = getInstantiator( q );
     Trace("inst-alg") << "-> Run cegqi for " << q << std::endl;
     d_curr_quant = q;
     if( !cinst->check() ){
       d_incomplete_check = true;
-      d_check_vts_lemma_lc = true;
     }
     d_curr_quant = Node::null();
-  }else if( e==1 ){
-    NodeManager* nm = NodeManager::currentNM();
+  }
+
+  // now, process the bounding lemmas for virtual terms
+  NodeManager* nm = NodeManager::currentNM();
+  VtsTermCache* vtc = d_treg.getVtsTermCache();
+  if (e == 0)
+  {
+    // if the check was incomplete, process bounds at next effort level
+    d_check_vts_lemma_lc = d_incomplete_check;
+    // process the lower bound for free delta immediately
+    Node delta = vtc->getVtsDelta(true, false);
+    if (!delta.isNull())
+    {
+      if (!d_freeDeltaLb.get())
+      {
+        d_freeDeltaLb = true;
+        Node zero = nm->mkConstReal(Rational(0));
+        Node delta_lem = nm->mkNode(GT, delta, zero);
+        d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
+      }
+    }
+  }
+  else if (e == 1)
+  {
     //minimize the free delta heuristically on demand
     if( d_check_vts_lemma_lc ){
       Trace("inst-alg") << "-> Minimize delta heuristic, for " << q << std::endl;
       d_check_vts_lemma_lc = false;
-      d_small_const = NodeManager::currentNM()->mkNode(
-          MULT, d_small_const, d_small_const_multiplier);
+      d_small_const = nm->mkNode(MULT, d_small_const, d_small_const_multiplier);
       d_small_const = rewrite(d_small_const);
       //heuristic for now, until we know how to do nested quantification
-      Node delta = d_vtsCache->getVtsDelta(true, false);
+      Node delta = vtc->getVtsDelta(true, false);
       if( !delta.isNull() ){
         Trace("quant-vts-debug") << "Delta lemma for " << d_small_const << std::endl;
-        Node delta_lem_ub = NodeManager::currentNM()->mkNode( LT, delta, d_small_const );
+        Node delta_lem_ub = nm->mkNode(LT, delta, d_small_const);
         d_qim.lemma(delta_lem_ub, InferenceId::QUANTIFIERS_CEGQI_VTS_UB_DELTA);
       }
       std::vector< Node > inf;
-      d_vtsCache->getVtsTerms(inf, true, false, false);
-      for( unsigned i=0; i<inf.size(); i++ ){
-        Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
+      vtc->getVtsTerms(inf, true, false, false);
+      for (const Node& i : inf)
+      {
+        Trace("quant-vts-debug")
+            << "Infinity lemma for " << i << " " << d_small_const << std::endl;
         Node inf_lem_lb = nm->mkNode(
             GT,
-            inf[i],
+            i,
             nm->mkConstReal(Rational(1) / d_small_const.getConst<Rational>()));
         d_qim.lemma(inf_lem_lb, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_INF);
       }
@@ -482,7 +506,8 @@ Node InstStrategyCegqi::getCounterexampleLiteral(Node q)
 bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) {
   Assert(!d_curr_quant.isNull());
   // check if we need virtual term substitution (if used delta or infinity)
-  bool usedVts = d_vtsCache->containsVtsTerm(subs, false);
+  VtsTermCache* vtc = d_treg.getVtsTermCache();
+  bool usedVts = vtc->containsVtsTerm(subs, false);
   Instantiate* inst = d_qim.getInstantiate();
   //if doing partial quantifier elimination, record the instantiation and set the incomplete flag instead of sending instantiation lemma
   if (d_qreg.getQuantAttributes().isQuantElimPartial(d_curr_quant))
@@ -518,7 +543,7 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) {
 
 VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
 {
-  return d_vtsCache.get();
+  return d_treg.getVtsTermCache();
 }
 
 BvInverter* InstStrategyCegqi::getBvInverter() const

diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
index b9412c54cb3f87cad902a44e8b116953c0df7f92..6b81141eae5c4dd4dfb9d0b839973b735bb94355 100644 (file)
--- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
+++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h
@@ -23,7 +23,6 @@
 #include "theory/quantifiers/bv_inverter.h"
 #include "theory/quantifiers/cegqi/ceg_instantiator.h"
 #include "theory/quantifiers/cegqi/nested_qe.h"
-#include "theory/quantifiers/cegqi/vts_term_cache.h"
 #include "theory/quantifiers/instantiate.h"
 #include "theory/quantifiers/quant_module.h"
 #include "util/statistics_stats.h"
@@ -156,8 +155,6 @@ class InstStrategyCegqi : public QuantifiersModule
    * This object is responsible for finding instantiatons for q.
    */
   std::map<Node, std::unique_ptr<CegInstantiator>> d_cinst;
-  /** virtual term substitution term cache for arithmetic instantiation */
-  std::unique_ptr<VtsTermCache> d_vtsCache;
   /** inversion utility for BV instantiation */
   std::unique_ptr<BvInverter> d_bv_invert;
   /**
@@ -182,6 +179,8 @@ class InstStrategyCegqi : public QuantifiersModule
   const Node d_small_const_multiplier;
   /** a small constant, used as a coefficient above */
   Node d_small_const;
+  /** whether we have initialized the lower bound on the free delta */
+  context::CDO<bool> d_freeDeltaLb;
   //---------------------- end for vts delta minimization
   /** register ce lemma */
   bool registerCbqiLemma( Node q );

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
index c0cb2d79f1706860fa9c7c2a9ca0df16afd4a741..4ba42d5ad6daf46d92be376ffdec90fc248679a7 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.cpp
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp
@@ -28,10 +28,9 @@ namespace cvc5::internal {
 namespace theory {
 namespace quantifiers {
 
-VtsTermCache::VtsTermCache(Env& env, QuantifiersInferenceManager& qim)
-    : EnvObj(env), d_qim(qim)
-{
-}
+VtsTermCache::VtsTermCache(Env& env) : EnvObj(env), d_hasAllocated(false) {}
+
+bool VtsTermCache::hasAllocated() const { return d_hasAllocated; }
 
 void VtsTermCache::getVtsTerms(std::vector<Node>& t,
                                bool isFree,
@@ -66,16 +65,15 @@ Node VtsTermCache::getVtsDelta(bool isFree, bool create)
     SkolemManager* sm = nm->getSkolemManager();
     if (d_vts_delta_free.isNull())
     {
+      d_hasAllocated = true;
       d_vts_delta_free =
           sm->mkDummySkolem("delta_free",
                             nm->realType(),
                             "free delta for virtual term substitution");
-      Node zero = nm->mkConstReal(Rational(0));
-      Node delta_lem = nm->mkNode(GT, d_vts_delta_free, zero);
-      d_qim.lemma(delta_lem, InferenceId::QUANTIFIERS_CEGQI_VTS_LB_DELTA);
     }
     if (d_vts_delta.isNull())
     {
+      d_hasAllocated = true;
       d_vts_delta = sm->mkDummySkolem(
           "delta", nm->realType(), "delta for virtual term substitution");
       // mark as a virtual term
@@ -94,11 +92,13 @@ Node VtsTermCache::getVtsInfinity(TypeNode tn, bool isFree, bool create)
     SkolemManager* sm = nm->getSkolemManager();
     if (d_vts_inf_free[tn].isNull())
     {
+      d_hasAllocated = true;
       d_vts_inf_free[tn] = sm->mkDummySkolem(
           "inf_free", tn, "free infinity for virtual term substitution");
     }
     if (d_vts_inf[tn].isNull())
     {
+      d_hasAllocated = true;
       d_vts_inf[tn] = sm->mkDummySkolem(
           "inf", tn, "infinity for virtual term substitution");
       // mark as a virtual term

diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h
index 99aad441035dd7704cd1f25c59b7ccc89ad11359..fbd1ffa8fb663f17eba7688fafe85edeb34df204 100644 (file)
--- a/src/theory/quantifiers/cegqi/vts_term_cache.h
+++ b/src/theory/quantifiers/cegqi/vts_term_cache.h
@@ -73,8 +73,14 @@ class QuantifiersInferenceManager;
 class VtsTermCache : protected EnvObj
 {
  public:
-  VtsTermCache(Env& env, QuantifiersInferenceManager& qim);
+  VtsTermCache(Env& env);
   ~VtsTermCache() {}
+  /**
+   * Have we allocated any VTS symbol? This impacts quantifier instantiation.
+   * In particular we use virtual term substitution for all instantiations
+   * when this is true.
+   */
+  bool hasAllocated() const;
   /**
    * Get vts delta. The argument isFree indicates if we are getting the
    * free variant of delta. If create is false, this method returns Node::null
@@ -125,8 +131,8 @@ class VtsTermCache : protected EnvObj
   bool containsVtsInfinity(Node n, bool isFree = false);
 
  private:
-  /** Reference to the quantifiers inference manager */
-  QuantifiersInferenceManager& d_qim;
+  /** Have we allocated any vts symbol? */
+  bool d_hasAllocated;
   /** The virtual term substitution delta */
   Node d_vts_delta;
   /** The virtual term substitution "free delta" */

diff --git a/src/theory/quantifiers/term_registry.cpp b/src/theory/quantifiers/term_registry.cpp
index c86b7aef95a85d8e608de4284acb27460e97d9d0..c08815c43eda9c2abfa4b0b55748a478a316e660 100644 (file)
--- a/src/theory/quantifiers/term_registry.cpp
+++ b/src/theory/quantifiers/term_registry.cpp
@@ -44,6 +44,7 @@ TermRegistry::TermRegistry(Env& env,
       d_echeck(new EntailmentCheck(env, qs, *d_termDb.get())),
       d_sygusTdb(nullptr),
       d_ochecker(nullptr),
+      d_vtsCache(new VtsTermCache(env)),
       d_qmodel(nullptr)
 {
   if (options().quantifiers.oracles)
@@ -161,6 +162,8 @@ TermEnumeration* TermRegistry::getTermEnumeration() const
 
 TermPools* TermRegistry::getTermPools() const { return d_termPools.get(); }
 
+VtsTermCache* TermRegistry::getVtsTermCache() const { return d_vtsCache.get(); }
+
 FirstOrderModel* TermRegistry::getModel() const { return d_qmodel; }
 
 }  // namespace quantifiers

diff --git a/src/theory/quantifiers/term_registry.h b/src/theory/quantifiers/term_registry.h
index 0af7129851d309924d80c916feb94f283f749ad8..94964ac284be8502af262239554d44aca2b78f8f 100644 (file)
--- a/src/theory/quantifiers/term_registry.h
+++ b/src/theory/quantifiers/term_registry.h
@@ -23,6 +23,7 @@
 
 #include "context/cdhashset.h"
 #include "smt/env_obj.h"
+#include "theory/quantifiers/cegqi/vts_term_cache.h"
 #include "theory/quantifiers/entailment_check.h"
 #include "theory/quantifiers/sygus/term_database_sygus.h"
 #include "theory/quantifiers/term_database.h"
@@ -93,6 +94,8 @@ class TermRegistry : protected EnvObj
   TermEnumeration* getTermEnumeration() const;
   /** get the term pools utility */
   TermPools* getTermPools() const;
+  /** get the virtual term substitution term cache utility */
+  VtsTermCache* getVtsTermCache() const;
   /** get the model utility */
   FirstOrderModel* getModel() const;
 
@@ -115,6 +118,8 @@ class TermRegistry : protected EnvObj
   std::unique_ptr<TermDbSygus> d_sygusTdb;
   /** oracle checker */
   std::unique_ptr<OracleChecker> d_ochecker;
+  /** virtual term substitution term cache for arithmetic instantiation */
+  std::unique_ptr<VtsTermCache> d_vtsCache;
   /** extended model object */
   FirstOrderModel* d_qmodel;
 };