From c7b4826b817abfb605884181e22ebac75afd5024 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 25 Apr 2022 15:07:51 -0500 Subject: [PATCH] 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. --- .../cegqi/ceg_arith_instantiator.cpp | 4 +- .../quantifiers/cegqi/inst_strategy_cegqi.cpp | 57 +++++++++++++------ .../quantifiers/cegqi/inst_strategy_cegqi.h | 5 +- .../quantifiers/cegqi/vts_term_cache.cpp | 14 ++--- src/theory/quantifiers/cegqi/vts_term_cache.h | 12 +++- src/theory/quantifiers/term_registry.cpp | 3 + src/theory/quantifiers/term_registry.h | 5 ++ 7 files changed, 70 insertions(+), 30 deletions(-) diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index e468ae001..d8119e45f 100644 --- 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 cffe42ae2..37aeaedcb 100644 --- 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; igetVtsTerms(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())); 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 b9412c54c..6b81141ea 100644 --- 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> d_cinst; - /** virtual term substitution term cache for arithmetic instantiation */ - std::unique_ptr d_vtsCache; /** inversion utility for BV instantiation */ std::unique_ptr 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 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 c0cb2d79f..4ba42d5ad 100644 --- 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& 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 99aad4410..fbd1ffa8f 100644 --- 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 c86b7aef9..c08815c43 100644 --- 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 0af712985..94964ac28 100644 --- 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 d_sygusTdb; /** oracle checker */ std::unique_ptr d_ochecker; + /** virtual term substitution term cache for arithmetic instantiation */ + std::unique_ptr d_vtsCache; /** extended model object */ FirstOrderModel* d_qmodel; }; -- 2.30.2