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{
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 || vrange<d_curr_range ){
- Trace("bound-int-bound") << "Successfully bound " << d_range << " to " << vrange << std::endl;
- d_curr_range = vrange;
- }
- //set the range
- d_has_range = true;
- }
- }else{
- Message() << "Could not find literal " << nlit << " for range " << d_range << std::endl;
- AlwaysAssert(false);
+Node BoundedIntegers::IntRangeDecisionHeuristic::proxyCurrentRangeLemma()
+{
+ if (d_range == d_proxy_range)
+ {
+ return Node::null();
}
-}
-
-void BoundedIntegers::IntRangeModel::allocateRange() {
- d_curr_max++;
- int newBound = d_curr_max;
- Trace("bound-int-proc") << "Allocate range bound " << newBound << " for " << d_range << std::endl;
- //TODO: newBound should be chosen in a smarter way
- Node ltr = NodeManager::currentNM()->mkNode( 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 || i<d_curr_range ){
- Node rn = (*it).first;
- Assert( !rn.isNull() );
- if( d_range_assertions.find( rn )==d_range_assertions.end() ){
- if (!d_lit_to_pol[rn]) {
- rn = rn.negate();
- }
- Trace("bound-int-dec-debug") << "For " << d_range << ", make decision " << rn << " to make range " << i << std::endl;
- return rn;
- }
- }
+ unsigned curr = 0;
+ if (!getAssertedLiteralIndex(curr))
+ {
+ return Node::null();
}
- return Node::null();
-}
-
-bool BoundedIntegers::IntRangeModel::proxyCurrentRange() {
- //Trace("model-engine") << "Range(" << d_range << ") currently is " << d_curr_max.get() << std::endl;
- if( d_range!=d_proxy_range ){
- //int curr = d_curr_range.get();
- int curr = d_curr_max;
- if( d_ranges_proxied.find( curr )==d_ranges_proxied.end() ){
- d_ranges_proxied[curr] = true;
- Assert( d_range_literal.find( curr )!=d_range_literal.end() );
- Node lem = NodeManager::currentNM()->mkNode( 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();
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; i<d_ranges.size(); i++) {
- if( d_rms[d_ranges[i]]->proxyCurrentRange() ){
- 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();
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());
}
}
}
}
}
-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; i<d_lit_to_ranges[nlit].size(); i++) {
- Node r = d_lit_to_ranges[nlit][i];
- Trace("bound-int-assert") << " ...this is a bounding literal for " << r << std::endl;
- d_rms[r]->assertNode( 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; i<d_ranges.size(); i++) {
- Node d = d_rms[d_ranges[i]]->getNextDecisionRequest();
- 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() ){
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<Node, std::unique_ptr<IntRangeDecisionHeuristic>> d_rms;
+
+ private:
//class to store whether bounding lemmas have been added
class BoundInstTrie
{
};
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:
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(); }
projects / cvc5.git / commitdiff