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
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));
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();
}
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);
<< "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)
{
{
// 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;
#include <vector>
#include "expr/node.h"
#include "theory/quantifiers/cegqi/ceg_instantiator.h"
+#include "theory/quantifiers/cegqi/vts_term_cache.h"
namespace CVC4 {
namespace theory {
class ArithInstantiator : public Instantiator
{
public:
- ArithInstantiator(TypeNode tn);
+ ArithInstantiator(TypeNode tn, VtsTermCache* vtc);
virtual ~ArithInstantiator() {}
/** reset */
void reset(CegInstantiator* ci,
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;
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);
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())
// 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())
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;
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; i<inf.size(); i++ ){
Trace("quant-vts-debug") << "Infinity lemma for " << inf[i] << " " << d_small_const << std::endl;
Node inf_lem_lb = NodeManager::currentNM()->mkNode( GT, inf[i], NodeManager::currentNM()->mkConst( Rational(1)/d_small_const.getConst<Rational>() ) );
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))
{
return it->second.get();
}
+VtsTermCache* InstStrategyCegqi::getVtsTermCache() const
+{
+ return d_vtsCache.get();
+}
+
BvInverter* InstStrategyCegqi::getBvInverter() const
{
return d_bv_invert.get();
#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"
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 */
* 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;
/**
--- /dev/null
+/********************* */
+/*! \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<Node>& 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<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;
+ }
+ 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<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;
+ // 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<Node> 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<Node> t;
+ getVtsTerms(t, isFree, false);
+ return expr::hasSubterm(n, t);
+}
+
+bool VtsTermCache::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 VtsTermCache::containsVtsInfinity(Node n, bool isFree)
+{
+ std::vector<Node> t;
+ getVtsTerms(t, isFree, false, false);
+ return expr::hasSubterm(n, t);
+}
+
+} // namespace quantifiers
+} // namespace theory
+} // namespace CVC4
--- /dev/null
+/********************* */
+/*! \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 <map>
+#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<VirtualTermSkolemAttributeId, bool>
+ 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<Node>& 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<Node>& 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<TypeNode, Node> d_vts_inf;
+ /** The virtual term substitution "free infinities" for int/real types */
+ std::map<TypeNode, Node> 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 */
}
}
-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; i<n.getNumChildren(); i++ ){
- Node nn = rewriteVtsSymbols( n[i] );
- children.push_back( nn );
- childChanged = childChanged || nn!=n[i];
- }
- if( childChanged ){
- if( n.getMetaKind() == kind::metakind::PARAMETERIZED ){
- children.insert( children.begin(), n.getOperator() );
- }
- Node ret = NodeManager::currentNM()->mkNode( 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 ) );
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{
Node n,
std::vector<Node>& 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 );
projects / cvc5.git / commitdiff