From 62b20b4983d7f6cdea4a1814fc331199303a1092 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Mon, 17 Sep 2018 16:50:19 -0500 Subject: [PATCH] Decision strategy: incorporate bounded integers (#2481) --- .../quantifiers/fmf/bounded_integers.cpp | 247 +++++------------- src/theory/quantifiers/fmf/bounded_integers.h | 84 +++--- 2 files changed, 113 insertions(+), 218 deletions(-) diff --git a/src/theory/quantifiers/fmf/bounded_integers.cpp b/src/theory/quantifiers/fmf/bounded_integers.cpp index e28489b1a..307ffeeed 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.cpp +++ b/src/theory/quantifiers/fmf/bounded_integers.cpp @@ -31,9 +31,14 @@ using namespace CVC4::theory; using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; - -BoundedIntegers::IntRangeModel::IntRangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi), - d_range(r), d_curr_max(-1), d_lit_to_range(u), d_range_assertions(c), d_has_range(c,false), d_curr_range(c,-1), d_ranges_proxied(u) { +BoundedIntegers::IntRangeDecisionHeuristic::IntRangeDecisionHeuristic( + Node r, + context::Context* c, + context::Context* u, + Valuation valuation, + bool isProxy) + : DecisionStrategyFmf(c, valuation), d_range(r), d_ranges_proxied(u) +{ if( options::fmfBoundLazy() ){ d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() ); }else{ @@ -43,128 +48,46 @@ BoundedIntegers::IntRangeModel::IntRangeModel(BoundedIntegers * bi, Node r, cont Trace("bound-int") << "Introduce proxy " << d_proxy_range << " for " << d_range << std::endl; } } - -void BoundedIntegers::IntRangeModel::initialize() { - //add initial split lemma - Node ltr = NodeManager::currentNM()->mkNode( LT, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(0) ) ); - ltr = Rewriter::rewrite( ltr ); - Trace("bound-int-lemma") << " *** bound int: initial split on " << ltr << std::endl; - d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); - Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr; - d_range_literal[-1] = ltr_lit; - d_lit_to_range[ltr_lit] = -1; - d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT; - //register with bounded integers - Trace("bound-int-debug") << "Literal " << ltr_lit << " is literal for " << d_range << std::endl; - d_bi->addLiteralFromRange(ltr_lit, d_range); +Node BoundedIntegers::IntRangeDecisionHeuristic::mkLiteral(unsigned n) +{ + NodeManager* nm = NodeManager::currentNM(); + Node cn = nm->mkConst(Rational(n == 0 ? 0 : n - 1)); + return nm->mkNode(n == 0 ? LT : LEQ, d_proxy_range, cn); } -void BoundedIntegers::IntRangeModel::assertNode(Node n) { - bool pol = n.getKind()!=NOT; - Node nlit = n.getKind()==NOT ? n[0] : n; - if( d_lit_to_range.find( nlit )!=d_lit_to_range.end() ){ - int vrange = d_lit_to_range[nlit]; - Trace("bound-int-assert") << "With polarity = " << pol << " (req "<< d_lit_to_pol[nlit] << ")"; - Trace("bound-int-assert") << ", found literal " << nlit; - Trace("bound-int-assert") << ", it is bound literal " << vrange << " for " << d_range << std::endl; - d_range_assertions[nlit] = (pol==d_lit_to_pol[nlit]); - if( pol!=d_lit_to_pol[nlit] ){ - //check if we need a new split? - if( !d_has_range ){ - bool needsRange = true; - for( NodeIntMap::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ - if( d_range_assertions.find( (*it).first )==d_range_assertions.end() ){ - Trace("bound-int-debug") << "Does not need range because of " << (*it).first << std::endl; - needsRange = false; - break; - } - } - if( needsRange ){ - allocateRange(); - } - } - }else{ - if (!d_has_range || vrangemkNode( LEQ, d_proxy_range, NodeManager::currentNM()->mkConst( Rational(newBound) ) ); - ltr = Rewriter::rewrite( ltr ); - Trace("bound-int-lemma") << " *** bound int: split on " << ltr << std::endl; - d_bi->getQuantifiersEngine()->getOutputChannel().split( ltr ); - Node ltr_lit = ltr.getKind()==NOT ? ltr[0] : ltr; - d_range_literal[newBound] = ltr_lit; - d_lit_to_range[ltr_lit] = newBound; - d_lit_to_pol[ltr_lit] = ltr.getKind()!=NOT; - //register with bounded integers - d_bi->addLiteralFromRange(ltr_lit, d_range); -} - -Node BoundedIntegers::IntRangeModel::getNextDecisionRequest() { - //request the current cardinality as a decision literal, if not already asserted - for( NodeIntMap::iterator it = d_lit_to_range.begin(); it != d_lit_to_range.end(); ++it ){ - int i = (*it).second; - if( !d_has_range || imkNode( EQUAL, d_range_literal[curr].negate(), - NodeManager::currentNM()->mkNode( LEQ, d_range, NodeManager::currentNM()->mkConst( Rational(curr) ) ) ); - Trace("bound-int-lemma") << "*** bound int : proxy lemma : " << lem << std::endl; - d_bi->getQuantifiersEngine()->addLemma( lem ); - return true; - } + if (d_ranges_proxied.find(curr) != d_ranges_proxied.end()) + { + return Node::null(); } - return false; + d_ranges_proxied[curr] = true; + NodeManager* nm = NodeManager::currentNM(); + Node currLit = getLiteral(curr); + Node lem = + nm->mkNode(EQUAL, + currLit, + nm->mkNode(curr == 0 ? LT : LEQ, + d_range, + nm->mkConst(Rational(curr == 0 ? 0 : curr - 1)))); + return lem; } - - - - -BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) : -QuantifiersModule(qe), d_assertions(c){ - +BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) + : QuantifiersModule(qe) +{ } -BoundedIntegers::~BoundedIntegers() { - for( std::map< Node, RangeModel * >::iterator it = d_rms.begin(); it != d_rms.end(); ++it ){ - delete it->second; - } -} +BoundedIntegers::~BoundedIntegers() {} void BoundedIntegers::presolve() { d_bnd_it.clear(); @@ -356,29 +279,26 @@ bool BoundedIntegers::needsCheck( Theory::Effort e ) { void BoundedIntegers::check(Theory::Effort e, QEffort quant_e) { - if (quant_e == QEFFORT_STANDARD) + if (quant_e != QEFFORT_STANDARD) { - Trace("bint-engine") << "---Bounded Integers---" << std::endl; - bool addedLemma = false; - //make sure proxies are up-to-date with range - for( unsigned i=0; iproxyCurrentRange() ){ - addedLemma = true; - } - } - Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl; + return; } -} - - -void BoundedIntegers::addLiteralFromRange( Node lit, Node r ) { - d_lit_to_ranges[lit].push_back(r); - //check if it is already asserted? - if(d_assertions.find(lit)!=d_assertions.end()){ - d_rms[r]->assertNode( d_assertions[lit] ? lit : lit.negate() ); + Trace("bint-engine") << "---Bounded Integers---" << std::endl; + bool addedLemma = false; + // make sure proxies are up-to-date with range + for (const Node& r : d_ranges) + { + Node prangeLem = d_rms[r]->proxyCurrentRangeLemma(); + if (!prangeLem.isNull()) + { + Trace("bound-int-lemma") + << "*** bound int : proxy lemma : " << prangeLem << std::endl; + d_quantEngine->addLemma(prangeLem); + addedLemma = true; + } } + Trace("bint-engine") << " addedLemma = " << addedLemma << std::endl; } - void BoundedIntegers::setBoundedVar( Node q, Node v, unsigned bound_type ) { d_bound_type[q][v] = bound_type; d_set_nums[q][v] = d_set[q].size(); @@ -564,11 +484,20 @@ void BoundedIntegers::checkOwnership(Node f) isProxy = true; } if( !r.isConst() ){ - if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){ + if (d_rms.find(r) == d_rms.end()) + { Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl; d_ranges.push_back( r ); - d_rms[r] = new IntRangeModel( this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy ); - d_rms[r]->initialize(); + d_rms[r].reset( + new IntRangeDecisionHeuristic(r, + d_quantEngine->getSatContext(), + d_quantEngine->getUserContext(), + d_quantEngine->getValuation(), + isProxy)); + d_quantEngine->getTheoryEngine() + ->getDecisionManager() + ->registerStrategy(DecisionManager::STRAT_QUANT_BOUND_INT_SIZE, + d_rms[r].get()); } } } @@ -576,48 +505,6 @@ void BoundedIntegers::checkOwnership(Node f) } } -void BoundedIntegers::assertNode( Node n ) { - Trace("bound-int-assert") << "Assert " << n << std::endl; - Node nlit = n.getKind()==NOT ? n[0] : n; - if( d_lit_to_ranges.find(nlit)!=d_lit_to_ranges.end() ){ - Trace("bound-int-assert") << "This is the bounding literal for " << d_lit_to_ranges[nlit].size() << " ranges." << std::endl; - for( unsigned i=0; iassertNode( n ); - } - } - d_assertions[nlit] = n.getKind()!=NOT; -} - -Node BoundedIntegers::getNextDecisionRequest( unsigned& priority ) { - Trace("bound-int-dec-debug") << "bi: Get next decision request?" << std::endl; - for( unsigned i=0; igetNextDecisionRequest(); - if (!d.isNull()) { - bool polLit = d.getKind()!=NOT; - Node lit = d.getKind()==NOT ? d[0] : d; - bool value; - if( d_quantEngine->getValuation().hasSatValue( lit, value ) ) { - if( value==polLit ){ - Trace("bound-int-dec-debug") << "...already asserted properly." << std::endl; - //already true, we're already fine - }else{ - Trace("bound-int-dec-debug") << "...already asserted with wrong polarity, re-assert." << std::endl; - assertNode( d.negate() ); - i--; - } - }else{ - priority = 1; - Trace("bound-int-dec") << "Bounded Integers : Decide " << d << std::endl; - return d; - } - } - } - Trace("bound-int-dec-debug") << "No decision request." << std::endl; - return Node::null(); -} - unsigned BoundedIntegers::getBoundVarType( Node q, Node v ) { std::map< Node, unsigned >::iterator it = d_bound_type[q].find( v ); if( it==d_bound_type[q].end() ){ diff --git a/src/theory/quantifiers/fmf/bounded_integers.h b/src/theory/quantifiers/fmf/bounded_integers.h index 8cb530a62..b3132a4a7 100644 --- a/src/theory/quantifiers/fmf/bounded_integers.h +++ b/src/theory/quantifiers/fmf/bounded_integers.h @@ -83,47 +83,58 @@ private: void processMatchBoundVars( Node q, Node n, std::vector< Node >& bvs, std::map< Node, bool >& visited ); std::vector< Node > d_bound_quants; private: - class RangeModel { + /** + * This decision strategy is used for minimizing the value of an integer + * arithmetic term t. It decides positively on literals of the form + * t < 0, t <= 0, t <= 1, t <=2, and so on. + */ + class IntRangeDecisionHeuristic : public DecisionStrategyFmf + { public: - RangeModel(){} - virtual ~RangeModel(){} - virtual void initialize() = 0; - virtual void assertNode(Node n) = 0; - virtual Node getNextDecisionRequest() = 0; - virtual bool proxyCurrentRange() = 0; - }; - class IntRangeModel : public RangeModel { + IntRangeDecisionHeuristic(Node r, + context::Context* c, + context::Context* u, + Valuation valuation, + bool isProxy); + /** make the n^th literal of this strategy */ + Node mkLiteral(unsigned n) override; + /** identify */ + std::string identify() const override + { + return std::string("bound_int_range"); + } + /** Returns the current proxy lemma if one exists (see below). */ + Node proxyCurrentRangeLemma(); + private: - BoundedIntegers * d_bi; - void allocateRange(); - Node d_proxy_range; - public: - IntRangeModel( BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy); - virtual ~IntRangeModel(){} - Node d_range; - int d_curr_max; - std::map< int, Node > d_range_literal; - std::map< Node, bool > d_lit_to_pol; - NodeIntMap d_lit_to_range; - NodeBoolMap d_range_assertions; - context::CDO< bool > d_has_range; - context::CDO< int > d_curr_range; - IntBoolMap d_ranges_proxied; - void initialize() override; - void assertNode(Node n) override; - Node getNextDecisionRequest() override; - bool proxyCurrentRange() override; + /** The range we are minimizing */ + Node d_range; + /** a proxy of the range + * + * When option::fmfBoundLazy is enabled, this class uses a lazy strategy + * for enforcing the bounds on term t by using a fresh variable x of type + * integer. The point of this variable is to serve as a proxy for t, so + * that we can decide on literals of the form x <= c instead of t <= c. The + * advantage of this is that we avoid unfairness, say, if t is constrained + * to be strictly greater c. Then, at full effort check, we add "proxy + * lemmas" of the form: (t <= c) <=> (x <= c) for the current minimal + * upper bound c for x. + */ + Node d_proxy_range; + /** ranges that have been proxied + * + * This is a user-context-dependent cache that stores which value we have + * added proxy lemmas for. + */ + IntBoolMap d_ranges_proxied; }; private: //information for minimizing ranges std::vector< Node > d_ranges; - //map to range model objects - std::map< Node, RangeModel * > d_rms; - //literal to range - std::map< Node, std::vector< Node > > d_lit_to_ranges; - //list of currently asserted arithmetic literals - NodeBoolMap d_assertions; -private: + /** Decision heuristics for each integer range */ + std::map> d_rms; + + private: //class to store whether bounding lemmas have been added class BoundInstTrie { @@ -143,7 +154,6 @@ private: }; std::map< Node, std::map< Node, BoundInstTrie > > d_bnd_it; private: - void addLiteralFromRange( Node lit, Node r ); void setBoundedVar( Node f, Node v, unsigned bound_type ); public: @@ -154,8 +164,6 @@ public: bool needsCheck(Theory::Effort e) override; void check(Theory::Effort e, QEffort quant_e) override; void checkOwnership(Node q) override; - void assertNode(Node n) override; - Node getNextDecisionRequest(unsigned& priority) override; bool isBoundVar( Node q, Node v ) { return std::find( d_set[q].begin(), d_set[q].end(), v )!=d_set[q].end(); } unsigned getBoundVarType( Node q, Node v ); unsigned getNumBoundVars( Node q ) { return d_set[q].size(); } -- 2.30.2