From: Andrew Reynolds Date: Mon, 16 Sep 2019 20:02:06 +0000 (-0500) Subject: Move virtual term substitution utilities to own file and document (#3278) X-Git-Tag: cvc5-1.0.0~3951 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f6cfc98f37bf92ccbf11aad20c1419071d8704f8;p=cvc5.git Move virtual term substitution utilities to own file and document (#3278) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index db92d2b3f..20458219e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -463,6 +463,8 @@ libcvc4_add_sources( theory/quantifiers/cegqi/ceg_instantiator.h theory/quantifiers/cegqi/inst_strategy_cegqi.cpp theory/quantifiers/cegqi/inst_strategy_cegqi.h + theory/quantifiers/cegqi/vts_term_cache.cpp + theory/quantifiers/cegqi/vts_term_cache.h theory/quantifiers/conjecture_generator.cpp theory/quantifiers/conjecture_generator.h theory/quantifiers/dynamic_rewrite.cpp diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp index e71f2b157..0a3775807 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.cpp @@ -32,7 +32,8 @@ namespace CVC4 { namespace theory { namespace quantifiers { -ArithInstantiator::ArithInstantiator(TypeNode tn) : Instantiator(tn) +ArithInstantiator::ArithInstantiator(TypeNode tn, VtsTermCache* vtc) + : Instantiator(tn), d_vtc(vtc) { d_zero = NodeManager::currentNM()->mkConst(Rational(0)); d_one = NodeManager::currentNM()->mkConst(Rational(1)); @@ -43,10 +44,8 @@ void ArithInstantiator::reset(CegInstantiator* ci, Node pv, CegInstEffort effort) { - d_vts_sym[0] = ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity( - d_type, false, false); - d_vts_sym[1] = - ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(false, false); + d_vts_sym[0] = d_vtc->getVtsInfinity(d_type, false, false); + d_vts_sym[1] = d_vtc->getVtsDelta(false, false); for (unsigned i = 0; i < 2; i++) { d_mbp_bounds[i].clear(); @@ -288,7 +287,7 @@ bool ArithInstantiator::processAssertion(CegInstantiator* ci, } else { - Node delta = ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta(); + Node delta = d_vtc->getVtsDelta(); uval = nm->mkNode( uires == CEG_TT_UPPER_STRICT ? PLUS : MINUS, uval, delta); uval = Rewriter::rewrite(uval); @@ -357,8 +356,7 @@ bool ArithInstantiator::processAssertions(CegInstantiator* ci, << "No " << (rr == 0 ? "lower" : "upper") << " bounds for " << pv << " (type=" << d_type << ")" << std::endl; // no bounds, we do +- infinity - Node val = - ci->getQuantifiersEngine()->getTermUtil()->getVtsInfinity(d_type); + Node val = d_vtc->getVtsInfinity(d_type); // could get rho value for infinity here if (rr == 0) { @@ -1034,11 +1032,7 @@ Node ArithInstantiator::getModelBasedProjectionValue(CegInstantiator* ci, { // create delta here if necessary val = nm->mkNode( - PLUS, - val, - nm->mkNode(MULT, - delta_coeff, - ci->getQuantifiersEngine()->getTermUtil()->getVtsDelta())); + PLUS, val, nm->mkNode(MULT, delta_coeff, d_vtc->getVtsDelta())); val = Rewriter::rewrite(val); } return val; diff --git a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h index 8ae5383a5..94e674687 100644 --- a/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_arith_instantiator.h @@ -20,6 +20,7 @@ #include #include "expr/node.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/cegqi/vts_term_cache.h" namespace CVC4 { namespace theory { @@ -42,7 +43,7 @@ namespace quantifiers { class ArithInstantiator : public Instantiator { public: - ArithInstantiator(TypeNode tn); + ArithInstantiator(TypeNode tn, VtsTermCache* vtc); virtual ~ArithInstantiator() {} /** reset */ void reset(CegInstantiator* ci, @@ -129,6 +130,8 @@ class ArithInstantiator : public Instantiator std::string identify() const override { return "Arith"; } private: + /** pointer to the virtual term substitution term cache class */ + VtsTermCache* d_vtc; /** zero/one */ Node d_zero; Node d_one; diff --git a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp index 1713c21e2..63736b53c 100644 --- a/src/theory/quantifiers/cegqi/ceg_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_instantiator.cpp @@ -477,7 +477,7 @@ void CegInstantiator::activateInstantiationVariable(Node v, unsigned index) TypeNode tn = v.getType(); Instantiator * vinst; if( tn.isReal() ){ - vinst = new ArithInstantiator(tn); + vinst = new ArithInstantiator(tn, d_parent->getVtsTermCache()); }else if( tn.isSort() ){ Assert( options::quantEpr() ); vinst = new EprInstantiator(tn); diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp index 7ad7e6996..7f9c21a65 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.cpp @@ -57,6 +57,7 @@ InstStrategyCegqi::InstStrategyCegqi(QuantifiersEngine* qe) d_incomplete_check(false), d_added_cbqi_lemma(qe->getUserContext()), d_elim_quants(qe->getSatContext()), + d_vtsCache(new VtsTermCache(qe)), d_bv_invert(nullptr), d_nested_qe_waitlist_size(qe->getUserContext()), d_nested_qe_waitlist_proc(qe->getUserContext()) @@ -460,7 +461,7 @@ Node InstStrategyCegqi::rewriteInstantiation(Node q, // do virtual term substitution inst = Rewriter::rewrite(inst); Trace("quant-vts-debug") << "Rewrite vts symbols in " << inst << std::endl; - inst = d_quantEngine->getTermUtil()->rewriteVtsSymbols(inst); + inst = d_vtsCache->rewriteVtsSymbols(inst); Trace("quant-vts-debug") << "...got " << inst << std::endl; } if (options::cbqiNestedQE()) @@ -499,7 +500,7 @@ Node InstStrategyCegqi::doNestedQENode( if( doVts ){ //do virtual term substitution ret = Rewriter::rewrite( ret ); - ret = d_quantEngine->getTermUtil()->rewriteVtsSymbols( ret ); + ret = d_vtsCache->rewriteVtsSymbols(ret); } Trace("cbqi-nqe") << "Nested quantifier elimination: " << std::endl; Trace("cbqi-nqe") << " " << n << std::endl; @@ -631,14 +632,14 @@ void InstStrategyCegqi::process( Node q, Theory::Effort effort, int e ) { d_small_const = NodeManager::currentNM()->mkNode( MULT, d_small_const, d_small_const ); d_small_const = Rewriter::rewrite( d_small_const ); //heuristic for now, until we know how to do nested quantification - Node delta = d_quantEngine->getTermUtil()->getVtsDelta( true, false ); + Node delta = d_vtsCache->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 ); d_quantEngine->getOutputChannel().lemma( delta_lem_ub ); } std::vector< Node > inf; - d_quantEngine->getTermUtil()->getVtsTerms( inf, true, false, false ); + d_vtsCache->getVtsTerms(inf, true, false, false); for( unsigned i=0; imkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst() ) ); @@ -674,7 +675,7 @@ bool InstStrategyCegqi::doAddInstantiation( std::vector< Node >& subs ) { return true; }else{ //check if we need virtual term substitution (if used delta or infinity) - bool used_vts = d_quantEngine->getTermUtil()->containsVtsTerm( subs, false ); + bool used_vts = d_vtsCache->containsVtsTerm(subs, false); if (d_quantEngine->getInstantiate()->addInstantiation( d_curr_quant, subs, false, false, used_vts)) { @@ -704,6 +705,11 @@ CegInstantiator * InstStrategyCegqi::getInstantiator( Node q ) { return it->second.get(); } +VtsTermCache* InstStrategyCegqi::getVtsTermCache() const +{ + return d_vtsCache.get(); +} + BvInverter* InstStrategyCegqi::getBvInverter() const { return d_bv_invert.get(); diff --git a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h index f3624d834..7abdf7d6d 100644 --- a/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h +++ b/src/theory/quantifiers/cegqi/inst_strategy_cegqi.h @@ -21,6 +21,7 @@ #include "theory/decision_manager.h" #include "theory/quantifiers/bv_inverter.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" +#include "theory/quantifiers/cegqi/vts_term_cache.h" #include "theory/quantifiers/instantiate.h" #include "theory/quantifiers/quant_util.h" #include "util/statistics_registry.h" @@ -89,6 +90,8 @@ class InstStrategyCegqi : public QuantifiersModule std::string identify() const override { return std::string("Cegqi"); } /** get instantiator for quantifier */ CegInstantiator* getInstantiator(Node q); + /** get the virtual term substitution term cache utility */ + VtsTermCache* getVtsTermCache() const; /** get the BV inverter utility */ BvInverter* getBvInverter() const; /** pre-register quantifier */ @@ -149,6 +152,8 @@ 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; /** diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.cpp b/src/theory/quantifiers/cegqi/vts_term_cache.cpp new file mode 100644 index 000000000..11c126eaf --- /dev/null +++ b/src/theory/quantifiers/cegqi/vts_term_cache.cpp @@ -0,0 +1,298 @@ +/********************* */ +/*! \file vts_term_cache.cpp + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Implementation of virtual term substitution term cache. + **/ + +#include "theory/quantifiers/cegqi/vts_term_cache.h" + +#include "expr/node_algorithm.h" +#include "theory/arith/arith_msum.h" +#include "theory/quantifiers_engine.h" + +using namespace CVC4::kind; + +namespace CVC4 { +namespace theory { +namespace quantifiers { + +VtsTermCache::VtsTermCache(QuantifiersEngine* qe) : d_qe(qe) +{ + d_zero = NodeManager::currentNM()->mkConst(Rational(0)); +} + +void VtsTermCache::getVtsTerms(std::vector& t, + bool isFree, + bool create, + bool inc_delta) +{ + if (inc_delta) + { + Node delta = getVtsDelta(isFree, create); + if (!delta.isNull()) + { + t.push_back(delta); + } + } + NodeManager* nm = NodeManager::currentNM(); + for (unsigned r = 0; r < 2; r++) + { + TypeNode tn = r == 0 ? nm->realType() : nm->integerType(); + Node inf = getVtsInfinity(tn, isFree, create); + if (!inf.isNull()) + { + t.push_back(inf); + } + } +} + +Node VtsTermCache::getVtsDelta(bool isFree, bool create) +{ + if (create) + { + NodeManager* nm = NodeManager::currentNM(); + if (d_vts_delta_free.isNull()) + { + d_vts_delta_free = + nm->mkSkolem("delta_free", + nm->realType(), + "free delta for virtual term substitution"); + Node delta_lem = nm->mkNode(GT, d_vts_delta_free, d_zero); + d_qe->getOutputChannel().lemma(delta_lem); + } + if (d_vts_delta.isNull()) + { + d_vts_delta = nm->mkSkolem( + "delta", nm->realType(), "delta for virtual term substitution"); + // mark as a virtual term + VirtualTermSkolemAttribute vtsa; + d_vts_delta.setAttribute(vtsa, true); + } + } + return isFree ? d_vts_delta_free : d_vts_delta; +} + +Node VtsTermCache::getVtsInfinity(TypeNode tn, bool isFree, bool create) +{ + if (create) + { + NodeManager* nm = NodeManager::currentNM(); + if (d_vts_inf_free[tn].isNull()) + { + d_vts_inf_free[tn] = nm->mkSkolem( + "inf_free", tn, "free infinity for virtual term substitution"); + } + if (d_vts_inf[tn].isNull()) + { + d_vts_inf[tn] = + nm->mkSkolem("inf", tn, "infinity for virtual term substitution"); + // mark as a virtual term + VirtualTermSkolemAttribute vtsa; + d_vts_inf[tn].setAttribute(vtsa, true); + } + } + return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn]; +} + +Node VtsTermCache::substituteVtsFreeTerms(Node n) +{ + std::vector vars; + getVtsTerms(vars, false, false); + std::vector vars_free; + getVtsTerms(vars_free, true, false); + Assert(vars.size() == vars_free.size()); + if (vars.empty()) + { + return n; + } + return n.substitute( + vars.begin(), vars.end(), vars_free.begin(), vars_free.end()); +} + +Node VtsTermCache::rewriteVtsSymbols(Node n) +{ + NodeManager* nm = NodeManager::currentNM(); + if ((n.getKind() == EQUAL || n.getKind() == GEQ)) + { + Trace("quant-vts-debug") << "VTS : process " << n << std::endl; + Node rew_vts_inf; + bool rew_delta = false; + // rewriting infinity always takes precedence over rewriting delta + for (unsigned r = 0; r < 2; r++) + { + TypeNode tn = r == 0 ? nm->realType() : nm->integerType(); + Node inf = getVtsInfinity(tn, false, false); + if (!inf.isNull() && expr::hasSubterm(n, inf)) + { + if (rew_vts_inf.isNull()) + { + rew_vts_inf = inf; + } + else + { + // for mixed int/real with multiple infinities + Trace("quant-vts-debug") << "Multiple infinities...equate " << inf + << " = " << rew_vts_inf << std::endl; + std::vector subs_lhs; + subs_lhs.push_back(inf); + std::vector subs_rhs; + subs_lhs.push_back(rew_vts_inf); + n = n.substitute(subs_lhs.begin(), + subs_lhs.end(), + subs_rhs.begin(), + subs_rhs.end()); + n = Rewriter::rewrite(n); + // may have cancelled + if (!expr::hasSubterm(n, rew_vts_inf)) + { + rew_vts_inf = Node::null(); + } + } + } + } + if (rew_vts_inf.isNull()) + { + if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta)) + { + rew_delta = true; + } + } + if (!rew_vts_inf.isNull() || rew_delta) + { + std::map msum; + if (ArithMSum::getMonomialSumLit(n, msum)) + { + if (Trace.isOn("quant-vts-debug")) + { + Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; + ArithMSum::debugPrintMonomialSum(msum, "quant-vts-debug"); + } + Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta; + Assert(!vts_sym.isNull()); + Node iso_n; + Node nlit; + int res = ArithMSum::isolate(vts_sym, msum, iso_n, n.getKind(), true); + if (res != 0) + { + Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n + << ", res = " << res << std::endl; + Node slv = iso_n[res == 1 ? 1 : 0]; + // ensure the vts terms have been eliminated + if (containsVtsTerm(slv)) + { + Trace("quant-vts-warn") + << "Bad vts literal : " << n << ", contains " << vts_sym + << " but bad solved form " << slv << "." << std::endl; + // safe case: just convert to free symbols + nlit = substituteVtsFreeTerms(n); + Trace("quant-vts-debug") << "...return " << nlit << std::endl; + return nlit; + } + else + { + if (!rew_vts_inf.isNull()) + { + nlit = nm->mkConst(n.getKind() == GEQ && res == 1); + } + else + { + Assert(iso_n[res == 1 ? 0 : 1] == d_vts_delta); + if (n.getKind() == EQUAL) + { + nlit = nm->mkConst(false); + } + else if (res == 1) + { + nlit = nm->mkNode(GEQ, d_zero, slv); + } + else + { + nlit = nm->mkNode(GT, slv, d_zero); + } + } + } + Trace("quant-vts-debug") << "Return " << nlit << std::endl; + return nlit; + } + else + { + Trace("quant-vts-warn") + << "Bad vts literal : " << n << ", contains " << vts_sym + << " but could not isolate." << std::endl; + // safe case: just convert to free symbols + nlit = substituteVtsFreeTerms(n); + Trace("quant-vts-debug") << "...return " << nlit << std::endl; + return nlit; + } + } + } + return n; + } + else if (n.getKind() == FORALL) + { + // cannot traverse beneath quantifiers + return substituteVtsFreeTerms(n); + } + bool childChanged = false; + std::vector children; + for (const Node& nc : n) + { + Node nn = rewriteVtsSymbols(nc); + children.push_back(nn); + childChanged = childChanged || nn != nc; + } + if (childChanged) + { + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) + { + children.insert(children.begin(), n.getOperator()); + } + Node ret = nm->mkNode(n.getKind(), children); + Trace("quant-vts-debug") << "...make node " << ret << std::endl; + return ret; + } + return n; +} + +bool VtsTermCache::containsVtsTerm(Node n, bool isFree) +{ + std::vector t; + getVtsTerms(t, isFree, false); + return expr::hasSubterm(n, t); +} + +bool VtsTermCache::containsVtsTerm(std::vector& n, bool isFree) +{ + std::vector t; + getVtsTerms(t, isFree, false); + if (!t.empty()) + { + for (const Node& nc : n) + { + if (expr::hasSubterm(nc, t)) + { + return true; + } + } + } + return false; +} + +bool VtsTermCache::containsVtsInfinity(Node n, bool isFree) +{ + std::vector t; + getVtsTerms(t, isFree, false, false); + return expr::hasSubterm(n, t); +} + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/quantifiers/cegqi/vts_term_cache.h b/src/theory/quantifiers/cegqi/vts_term_cache.h new file mode 100644 index 000000000..1c3ec0801 --- /dev/null +++ b/src/theory/quantifiers/cegqi/vts_term_cache.h @@ -0,0 +1,145 @@ +/********************* */ +/*! \file vts_term_cache.h + ** \verbatim + ** Top contributors (to current version): + ** Andrew Reynolds + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Virtual term substitution term cache. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H +#define CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H + +#include +#include "expr/attribute.h" +#include "expr/node.h" + +namespace CVC4 { +namespace theory { + +class QuantifiersEngine; + +/** Attribute to mark Skolems as virtual terms */ +struct VirtualTermSkolemAttributeId +{ +}; +typedef expr::Attribute + VirtualTermSkolemAttribute; + +namespace quantifiers { + +/** Virtual term substitution term cache + * + * This class stores skolems corresponding to virtual terms (e.g. delta and + * infinity) and has methods for performing virtual term substitution. + * + * In detail, there are three kinds of virtual terms: + * (1) delta, of Real type, representing a infinitesimally small real value, + * (2) infinity, of Real type, representing an infinitely large real value, + * (3) infinity, of Int type, representing an infinitely large integer value. + * + * For each of the above three virtual terms, we have 2 variants. + * + * The first variant we simply call "virtual terms". These terms are intended + * to never appear in assertions and are simply used by algorithms e.g. CEGQI + * for specifying instantiations. They are eliminated by the standard rules of + * virtual term substitution, e.g.: + * t < s + delta ---> t <=s + * t <= s + delta ---> t <= s + * t < s - delta ----> t < s + * t <= s - delta -----> t < s + * t <= s + inf ----> true + * t <= s - inf ----> false + * + * The second variant we call "free virtual terms". These terms are intended + * to appear in assertions and are constrained to have the semantics of the + * above virtual terms, e.g.: + * 0 < delta_free + * forall x. x < inf_free + * We use free virtual terms for some instantiation strategies, e.g. those + * that combine instantiating quantified formulas with nested quantifiers + * with terms containing virtual terms. + */ +class VtsTermCache +{ + public: + VtsTermCache(QuantifiersEngine* qe); + ~VtsTermCache() {} + /** + * 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 + * if the requested delta has not already been created. + */ + Node getVtsDelta(bool isFree = false, bool create = true); + /** + * Get vts infinity of type tn, where tn should be Int or Real. + * The argument isFree indicates if we are getting the free variant of + * infinity. If create is false, this method returns Node::null if the + * requested infinity has not already been created. + */ + Node getVtsInfinity(TypeNode tn, bool isFree = false, bool create = true); + /** + * Get all vts terms and add them to vector t. + * If the argument isFree is true, we return the free variant of all virtual + * terms. If create is false, we do not add virtual terms that have not + * already been created. If inc_delta is false, we do not include delta. + */ + void getVtsTerms(std::vector& t, + bool isFree = false, + bool create = true, + bool inc_delta = true); + /** + * Rewrite virtual terms in node n. This returns the rewritten form of n + * after virtual term substitution. + * + * This method ensures that the returned node is equivalent to n and does + * not contain free occurrences of the virtual terms. + */ + Node rewriteVtsSymbols(Node n); + /** + * This method returns true iff n contains a virtual term. If isFree is true, + * if returns true iff n contains a free virtual term. + */ + bool containsVtsTerm(Node n, bool isFree = false); + /** + * This method returns true iff any term in vector n contains a virtual term. + * If isFree is true, if returns true iff any term in vector n contains a + * free virtual term. + */ + bool containsVtsTerm(std::vector& n, bool isFree = false); + /** + * This method returns true iff n contains an occurence of the virtual term + * infinity. If isFree is true, if returns true iff n contains the free + * virtual term infinity. + */ + bool containsVtsInfinity(Node n, bool isFree = false); + + private: + /** pointer to the quantifiers engine */ + QuantifiersEngine* d_qe; + /** constants */ + Node d_zero; + /** The virtual term substitution delta */ + Node d_vts_delta; + /** The virtual term substitution "free delta" */ + Node d_vts_delta_free; + /** The virtual term substitution infinities for int/real types */ + std::map d_vts_inf; + /** The virtual term substitution "free infinities" for int/real types */ + std::map d_vts_inf_free; + /** substitute vts terms with their corresponding vts free terms */ + Node substituteVtsFreeTerms(Node n); +}; /* class TermUtil */ + +} // namespace quantifiers +} // namespace theory +} // namespace CVC4 + +#endif /* CVC4__THEORY__QUANTIFIERS__CEGQI__VTS_TERM_CACHE_H */ diff --git a/src/theory/quantifiers/term_util.cpp b/src/theory/quantifiers/term_util.cpp index 6ffc50c97..c9c738eb3 100644 --- a/src/theory/quantifiers/term_util.cpp +++ b/src/theory/quantifiers/term_util.cpp @@ -304,215 +304,6 @@ void TermUtil::computeInstConstContainsForQuant(Node q, } } -void TermUtil::getVtsTerms( std::vector< Node >& t, bool isFree, bool create, bool inc_delta ) { - if( inc_delta ){ - Node delta = getVtsDelta( isFree, create ); - if( !delta.isNull() ){ - t.push_back( delta ); - } - } - for( unsigned r=0; r<2; r++ ){ - Node inf = getVtsInfinityIndex( r, isFree, create ); - if( !inf.isNull() ){ - t.push_back( inf ); - } - } -} - -Node TermUtil::getVtsDelta( bool isFree, bool create ) { - if( create ){ - if( d_vts_delta_free.isNull() ){ - d_vts_delta_free = NodeManager::currentNM()->mkSkolem( "delta_free", NodeManager::currentNM()->realType(), "free delta for virtual term substitution" ); - Node delta_lem = NodeManager::currentNM()->mkNode( GT, d_vts_delta_free, d_zero ); - d_quantEngine->getOutputChannel().lemma( delta_lem ); - } - if( d_vts_delta.isNull() ){ - d_vts_delta = NodeManager::currentNM()->mkSkolem( "delta", NodeManager::currentNM()->realType(), "delta for virtual term substitution" ); - //mark as a virtual term - VirtualTermSkolemAttribute vtsa; - d_vts_delta.setAttribute(vtsa,true); - } - } - return isFree ? d_vts_delta_free : d_vts_delta; -} - -Node TermUtil::getVtsInfinity( TypeNode tn, bool isFree, bool create ) { - if( create ){ - if( d_vts_inf_free[tn].isNull() ){ - d_vts_inf_free[tn] = NodeManager::currentNM()->mkSkolem( "inf_free", tn, "free infinity for virtual term substitution" ); - } - if( d_vts_inf[tn].isNull() ){ - d_vts_inf[tn] = NodeManager::currentNM()->mkSkolem( "inf", tn, "infinity for virtual term substitution" ); - //mark as a virtual term - VirtualTermSkolemAttribute vtsa; - d_vts_inf[tn].setAttribute(vtsa,true); - } - } - return isFree ? d_vts_inf_free[tn] : d_vts_inf[tn]; -} - -Node TermUtil::getVtsInfinityIndex( int i, bool isFree, bool create ) { - if( i==0 ){ - return getVtsInfinity( NodeManager::currentNM()->realType(), isFree, create ); - }else if( i==1 ){ - return getVtsInfinity( NodeManager::currentNM()->integerType(), isFree, create ); - }else{ - Assert( false ); - return Node::null(); - } -} - -Node TermUtil::substituteVtsFreeTerms( Node n ) { - std::vector< Node > vars; - getVtsTerms( vars, false, false ); - std::vector< Node > vars_free; - getVtsTerms( vars_free, true, false ); - Assert( vars.size()==vars_free.size() ); - if( !vars.empty() ){ - return n.substitute( vars.begin(), vars.end(), vars_free.begin(), vars_free.end() ); - }else{ - return n; - } -} - -Node TermUtil::rewriteVtsSymbols( Node n ) { - if( ( n.getKind()==EQUAL || n.getKind()==GEQ ) ){ - Trace("quant-vts-debug") << "VTS : process " << n << std::endl; - Node rew_vts_inf; - bool rew_delta = false; - //rewriting infinity always takes precedence over rewriting delta - for( unsigned r=0; r<2; r++ ){ - Node inf = getVtsInfinityIndex( r, false, false ); - if (!inf.isNull() && expr::hasSubterm(n, inf)) - { - if( rew_vts_inf.isNull() ){ - rew_vts_inf = inf; - }else{ - //for mixed int/real with multiple infinities - Trace("quant-vts-debug") << "Multiple infinities...equate " << inf << " = " << rew_vts_inf << std::endl; - std::vector< Node > subs_lhs; - subs_lhs.push_back( inf ); - std::vector< Node > subs_rhs; - subs_lhs.push_back( rew_vts_inf ); - n = n.substitute( subs_lhs.begin(), subs_lhs.end(), subs_rhs.begin(), subs_rhs.end() ); - n = Rewriter::rewrite( n ); - // may have cancelled - if (!expr::hasSubterm(n, rew_vts_inf)) - { - rew_vts_inf = Node::null(); - } - } - } - } - if (rew_vts_inf.isNull()) - { - if (!d_vts_delta.isNull() && expr::hasSubterm(n, d_vts_delta)) - { - rew_delta = true; - } - } - if( !rew_vts_inf.isNull() || rew_delta ){ - std::map< Node, Node > msum; - if (ArithMSum::getMonomialSumLit(n, msum)) - { - if( Trace.isOn("quant-vts-debug") ){ - Trace("quant-vts-debug") << "VTS got monomial sum : " << std::endl; - ArithMSum::debugPrintMonomialSum(msum, "quant-vts-debug"); - } - Node vts_sym = !rew_vts_inf.isNull() ? rew_vts_inf : d_vts_delta; - Assert( !vts_sym.isNull() ); - Node iso_n; - Node nlit; - int res = ArithMSum::isolate(vts_sym, msum, iso_n, n.getKind(), true); - if( res!=0 ){ - Trace("quant-vts-debug") << "VTS isolated : -> " << iso_n << ", res = " << res << std::endl; - Node slv = iso_n[res==1 ? 1 : 0]; - //ensure the vts terms have been eliminated - if( containsVtsTerm( slv ) ){ - Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but bad solved form " << slv << "." << std::endl; - nlit = substituteVtsFreeTerms( n ); - Trace("quant-vts-debug") << "...return " << nlit << std::endl; - //Assert( false ); - //safe case: just convert to free symbols - return nlit; - }else{ - if( !rew_vts_inf.isNull() ){ - nlit = ( n.getKind()==GEQ && res==1 ) ? d_true : d_false; - }else{ - Assert( iso_n[res==1 ? 0 : 1]==d_vts_delta ); - if( n.getKind()==EQUAL ){ - nlit = d_false; - }else if( res==1 ){ - nlit = NodeManager::currentNM()->mkNode( GEQ, d_zero, slv ); - }else{ - nlit = NodeManager::currentNM()->mkNode( GT, slv, d_zero ); - } - } - } - Trace("quant-vts-debug") << "Return " << nlit << std::endl; - return nlit; - }else{ - Trace("quant-vts-warn") << "Bad vts literal : " << n << ", contains " << vts_sym << " but could not isolate." << std::endl; - //safe case: just convert to free symbols - nlit = substituteVtsFreeTerms( n ); - Trace("quant-vts-debug") << "...return " << nlit << std::endl; - //Assert( false ); - return nlit; - } - } - } - return n; - }else if( n.getKind()==FORALL ){ - //cannot traverse beneath quantifiers - return substituteVtsFreeTerms( n ); - }else{ - bool childChanged = false; - std::vector< Node > children; - for( unsigned i=0; imkNode( n.getKind(), children ); - Trace("quant-vts-debug") << "...make node " << ret << std::endl; - return ret; - }else{ - return n; - } - } -} - -bool TermUtil::containsVtsTerm( Node n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false ); - return expr::hasSubterm(n, t); -} - -bool TermUtil::containsVtsTerm( std::vector< Node >& n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false ); - if( !t.empty() ){ - for (const Node& nc : n) - { - if (expr::hasSubterm(nc, t)) - { - return true; - } - } - } - return false; -} - -bool TermUtil::containsVtsInfinity( Node n, bool isFree ) { - std::vector< Node > t; - getVtsTerms( t, isFree, false, false ); - return expr::hasSubterm(n, t); -} - Node TermUtil::ensureType( Node n, TypeNode tn ) { TypeNode ntn = n.getType(); Assert( ntn.isComparableTo( tn ) ); diff --git a/src/theory/quantifiers/term_util.h b/src/theory/quantifiers/term_util.h index 52965d2fa..9906eef2f 100644 --- a/src/theory/quantifiers/term_util.h +++ b/src/theory/quantifiers/term_util.h @@ -76,10 +76,6 @@ typedef expr::Attribute AbsTypeFunDefAttribute; struct QuantIdNumAttributeId {}; typedef expr::Attribute< QuantIdNumAttributeId, uint64_t > QuantIdNumAttribute; -/** Attribute to mark Skolems as virtual terms */ -struct VirtualTermSkolemAttributeId {}; -typedef expr::Attribute< VirtualTermSkolemAttributeId, bool > VirtualTermSkolemAttribute; - class QuantifiersEngine; namespace inst{ @@ -188,31 +184,7 @@ public: Node n, std::vector& vars); -//for virtual term substitution -private: - Node d_vts_delta; - std::map< TypeNode, Node > d_vts_inf; - Node d_vts_delta_free; - std::map< TypeNode, Node > d_vts_inf_free; - /** get vts infinity index */ - Node getVtsInfinityIndex( int i, bool isFree = false, bool create = true ); - /** substitute vts free terms */ - Node substituteVtsFreeTerms( Node n ); public: - /** get vts delta */ - Node getVtsDelta( bool isFree = false, bool create = true ); - /** get vts infinity */ - Node getVtsInfinity( TypeNode tn, bool isFree = false, bool create = true ); - /** get all vts terms */ - void getVtsTerms( std::vector< Node >& t, bool isFree = false, bool create = true, bool inc_delta = true ); - /** rewrite delta */ - Node rewriteVtsSymbols( Node n ); - /** simple check for contains term */ - bool containsVtsTerm( Node n, bool isFree = false ); - /** simple check for contains term */ - bool containsVtsTerm( std::vector< Node >& n, bool isFree = false ); - /** simple check for contains term */ - bool containsVtsInfinity( Node n, bool isFree = false ); /** ensure type */ static Node ensureType( Node n, TypeNode tn );