From 6edc4fac0e5c868b6c6bad13ffc9112b16c1d5f5 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 1 Jun 2016 15:51:39 -0500 Subject: [PATCH] Initial infrastructure for bounded set quantification (disabled). Refactoring and fixes for --fmf-bound-int. Fix simple memory leaks in strings and bounded integers. --- src/theory/quantifiers/bounded_integers.cpp | 365 ++++++++++++------ src/theory/quantifiers/bounded_integers.h | 61 ++- src/theory/quantifiers/first_order_model.cpp | 4 +- src/theory/quantifiers/full_model_check.cpp | 13 +- .../quantifiers/inst_strategy_e_matching.cpp | 4 +- src/theory/quantifiers/model_builder.cpp | 26 +- src/theory/quantifiers/model_engine.cpp | 11 +- src/theory/quantifiers/term_database.cpp | 2 + src/theory/quantifiers/term_database.h | 3 + src/theory/quantifiers_engine.cpp | 1 + src/theory/rep_set.cpp | 283 +++++++------- src/theory/rep_set.h | 55 +-- src/theory/strings/theory_strings.cpp | 4 +- test/regress/regress0/fmf/Makefile.am | 3 +- test/regress/regress0/fmf/bound-int-alt.smt2 | 18 + 15 files changed, 543 insertions(+), 310 deletions(-) create mode 100644 test/regress/regress0/fmf/bound-int-alt.smt2 diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index d32ef59a1..7184624da 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -28,7 +28,7 @@ using namespace CVC4::theory::quantifiers; using namespace CVC4::kind; -BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy) : d_bi(bi), +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) { if( options::fmfBoundIntLazy() ){ d_proxy_range = isProxy ? r : NodeManager::currentNM()->mkSkolem( "pbir", r.getType() ); @@ -40,7 +40,7 @@ BoundedIntegers::RangeModel::RangeModel(BoundedIntegers * bi, Node r, context::C } } -void BoundedIntegers::RangeModel::initialize() { +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 ); @@ -55,7 +55,7 @@ void BoundedIntegers::RangeModel::initialize() { d_bi->addLiteralFromRange(ltr_lit, d_range); } -void BoundedIntegers::RangeModel::assertNode(Node n) { +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() ){ @@ -93,7 +93,7 @@ void BoundedIntegers::RangeModel::assertNode(Node n) { } } -void BoundedIntegers::RangeModel::allocateRange() { +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; @@ -110,7 +110,7 @@ void BoundedIntegers::RangeModel::allocateRange() { d_bi->addLiteralFromRange(ltr_lit, d_range); } -Node BoundedIntegers::RangeModel::getNextDecisionRequest() { +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; @@ -129,7 +129,7 @@ Node BoundedIntegers::RangeModel::getNextDecisionRequest() { return Node::null(); } -bool BoundedIntegers::RangeModel::proxyCurrentRange() { +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(); @@ -148,11 +148,24 @@ bool BoundedIntegers::RangeModel::proxyCurrentRange() { } + + + BoundedIntegers::BoundedIntegers(context::Context* c, QuantifiersEngine* qe) : QuantifiersModule(qe), d_assertions(c){ } +BoundedIntegers::~BoundedIntegers() { + for( std::map< Node, RangeModel * >::iterator it = d_rms.begin(); it != d_rms.end(); ++it ){ + delete it->second; + } +} + +void BoundedIntegers::presolve() { + d_bnd_it.clear(); +} + bool BoundedIntegers::isBound( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); } @@ -172,62 +185,79 @@ bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) { return false; } -void BoundedIntegers::processLiteral( Node f, Node lit, bool pol, +void BoundedIntegers::processLiteral( Node q, Node lit, bool pol, + std::map< Node, unsigned >& bound_lit_type_map, std::map< int, std::map< Node, Node > >& bound_lit_map, - std::map< int, std::map< Node, bool > >& bound_lit_pol_map ) { - if( lit.getKind()==GEQ && lit[0].getType().isInteger() ){ - std::map< Node, Node > msum; - if (QuantArith::getMonomialSumLit( lit, msum )){ - Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; - QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" ); - for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ - if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( f, it->first ) ){ - Node veq; - if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){ - Node n1 = veq[0]; - Node n2 = veq[1]; - if(pol){ - //flip - n1 = veq[1]; - n2 = veq[0]; - if( n1.getKind()==BOUND_VARIABLE ){ - n2 = QuantArith::offset( n2, 1 ); + std::map< int, std::map< Node, bool > >& bound_lit_pol_map, + std::map< int, std::map< Node, Node > >& bound_int_range_term ) { + if( lit.getKind()==GEQ ){ + if( lit[0].getType().isInteger() ){ + std::map< Node, Node > msum; + if( QuantArith::getMonomialSumLit( lit, msum ) ){ + Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is monomial sum : " << std::endl; + QuantArith::debugPrintMonomialSum( msum, "bound-int-debug" ); + for( std::map< Node, Node >::iterator it = msum.begin(); it != msum.end(); ++it ){ + if ( !it->first.isNull() && it->first.getKind()==BOUND_VARIABLE && !isBound( q, it->first ) ){ + Node veq; + if( QuantArith::isolate( it->first, msum, veq, GEQ )!=0 ){ + Node n1 = veq[0]; + Node n2 = veq[1]; + if(pol){ + //flip + n1 = veq[1]; + n2 = veq[0]; + if( n1.getKind()==BOUND_VARIABLE ){ + n2 = QuantArith::offset( n2, 1 ); + }else{ + n1 = QuantArith::offset( n1, -1 ); + } + veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 ); + } + Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl; + Node t = n1==it->first ? n2 : n1; + if( !hasNonBoundVar( q, t ) ) { + Trace("bound-int-debug") << "The bound is relevant." << std::endl; + int loru = n1==it->first ? 0 : 1; + bound_lit_type_map[it->first] = BOUND_INT_RANGE; + bound_int_range_term[loru][it->first] = t; + bound_lit_map[loru][it->first] = lit; + bound_lit_pol_map[loru][it->first] = pol; }else{ - n1 = QuantArith::offset( n1, -1 ); + Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl; } - veq = NodeManager::currentNM()->mkNode( GEQ, n1, n2 ); - } - Trace("bound-int-debug") << "Isolated for " << it->first << " : (" << n1 << " >= " << n2 << ")" << std::endl; - Node t = n1==it->first ? n2 : n1; - if( !hasNonBoundVar( f, t ) ) { - Trace("bound-int-debug") << "The bound is relevant." << std::endl; - int loru = n1==it->first ? 0 : 1; - d_bounds[loru][f][it->first] = t; - bound_lit_map[loru][it->first] = lit; - bound_lit_pol_map[loru][it->first] = pol; - }else{ - Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl; } } } } } + }else if( lit.getKind()==MEMBER ){ + //TODO: enable this when sets models are fixed + /* + if( !pol && lit[0].getKind()==BOUND_VARIABLE && !isBound( q, lit[0] ) && !lit[1].hasBoundVar() ){ + Trace("bound-int-debug") << "Literal (polarity = " << pol << ") " << lit << " is membership." << std::endl; + bound_lit_type_map[lit[0]] = BOUND_SET_MEMBER; + bound_lit_map[0][lit[0]] = lit; + bound_lit_pol_map[0][lit[0]] = pol; + } + */ }else if( lit.getKind()==LEQ || lit.getKind()==LT || lit.getKind()==GT ) { Message() << "BoundedIntegers : Bad kind for literal : " << lit << std::endl; } } -void BoundedIntegers::process( Node f, Node n, bool pol, +void BoundedIntegers::process( Node q, Node n, bool pol, + std::map< Node, unsigned >& bound_lit_type_map, std::map< int, std::map< Node, Node > >& bound_lit_map, - std::map< int, std::map< Node, bool > >& bound_lit_pol_map ){ + std::map< int, std::map< Node, bool > >& bound_lit_pol_map, + std::map< int, std::map< Node, Node > >& bound_int_range_term ){ if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){ for( unsigned i=0; i numMap; - for( unsigned i=0; i > bound_lit_map; - std::map< int, std::map< Node, bool > > bound_lit_pol_map; - success = false; - process( f, f[1], true, bound_lit_map, bound_lit_pol_map ); - for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){ - Node v = it->first; - if( !isBound(f,v) ){ - if( d_bounds[1][f].find(v)!=d_bounds[1][f].end() ){ - d_set[f].push_back(v); - d_set_nums[f].push_back(numMap[v]); + + bool success; + do{ + std::map< Node, unsigned > bound_lit_type_map; + std::map< int, std::map< Node, Node > > bound_lit_map; + std::map< int, std::map< Node, bool > > bound_lit_pol_map; + std::map< int, std::map< Node, Node > > bound_int_range_term; + success = false; + process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term ); + //for( std::map< Node, Node >::iterator it = d_bounds[0][f].begin(); it != d_bounds[0][f].end(); ++it ){ + for( std::map< Node, unsigned >::iterator it = bound_lit_type_map.begin(); it != bound_lit_type_map.end(); ++it ){ + Node v = it->first; + if( !isBound( f, v ) ){ + bool setBoundVar = false; + if( it->second==BOUND_INT_RANGE ){ + //must have both + if( bound_lit_map[0].find( v )!=bound_lit_map[0].end() && bound_lit_map[1].find( v )!=bound_lit_map[1].end() ){ + setBoundedVar( f, v, BOUND_INT_RANGE ); + setBoundVar = true; success = true; - //set Attributes on literals for( unsigned b=0; b<2; b++ ){ - Assert( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ); + //set the bounds + Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() ); + d_bounds[b][f][v] = bound_int_range_term[b][v]; + } + Node r = NodeManager::currentNM()->mkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] ); + d_range[f][v] = Rewriter::rewrite( r ); + Trace("bound-int") << "Variable " << v << " is bound because of int range literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl; + } + }else if( it->second==BOUND_SET_MEMBER ){ + setBoundedVar( f, v, BOUND_SET_MEMBER ); + setBoundVar = true; + d_setm_range[f][v] = bound_lit_map[0][v][1]; + Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl; + } + if( setBoundVar ){ + //set Attributes on literals + for( unsigned b=0; b<2; b++ ){ + if( bound_lit_map[b].find( v )!=bound_lit_map[b].end() ){ Assert( bound_lit_pol_map[b].find( v )!=bound_lit_pol_map[b].end() ); BoundIntLitAttribute bila; bound_lit_map[b][v].setAttribute( bila, bound_lit_pol_map[b][v] ? 1 : 0 ); + }else{ + Assert( it->second!=BOUND_INT_RANGE ); } - Trace("bound-int") << "Variable " << v << " is bound because of literals " << bound_lit_map[0][v] << " and " << bound_lit_map[1][v] << std::endl; } } } - }while( success ); - Trace("bound-int") << "Bounds are : " << std::endl; - for( unsigned i=0; imkNode( MINUS, d_bounds[1][f][v], d_bounds[0][f][v] ); - d_range[f][v] = Rewriter::rewrite( r ); + } + }while( success ); + + Trace("bound-int") << "Bounds are : " << std::endl; + for( unsigned i=0; imayComplete( tn ) ){ + Trace("bound-int-warn") << "Warning : Bounded Integers : Due to quantification on " << f[0][i] << ", could not find bounds for " << f << std::endl; + bound_success = false; + break; + } } - if( d_set[f].size()==(f[0].getNumChildren()-finiteTypes) ){ - d_bound_quants.push_back( f ); - for( unsigned i=0; imkNode( CARD, d_setm_range[f][v] ); + } bool isProxy = false; if( r.hasBoundVar() ){ //introduce a new bound @@ -319,18 +390,15 @@ void BoundedIntegers::registerQuantifier( Node f ) { r = new_range; isProxy = true; } - if( r.getKind()!=CONST_RATIONAL ){ + if( !r.isConst() ){ if( std::find(d_ranges.begin(), d_ranges.end(), r)==d_ranges.end() ){ - Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << " " << r.getKind() << std::endl; + Trace("bound-int") << "For " << v << ", bounded Integer Module will try to minimize : " << r << std::endl; d_ranges.push_back( r ); - d_rms[r] = new RangeModel(this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy ); + d_rms[r] = new IntRangeModel( this, r, d_quantEngine->getSatContext(), d_quantEngine->getUserContext(), isProxy ); d_rms[r]->initialize(); } } } - }else{ - Trace("bound-int-warn") << "Warning : Bounded Integers : Could not find bounds for " << f << std::endl; - //Message() << "Bound integers : Cannot infer bounds of " << f << std::endl; } } } @@ -376,39 +444,28 @@ Node BoundedIntegers::getNextDecisionRequest() { 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() ){ + return BOUND_NONE; + }else{ + return it->second; + } +} + void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { l = d_bounds[0][f][v]; u = d_bounds[1][f][v]; if( d_nground_range[f].find(v)!=d_nground_range[f].end() ){ - //must create substitution + //get the substitution std::vector< Node > vars; std::vector< Node > subs; - Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl; - for( unsigned i=0; id_var_order[d_set_nums[f][i]] << std::endl; - Trace("bound-int-rsi") << "term : " << rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]]) << std::endl; - vars.push_back(d_set[f][i]); - subs.push_back(rsi->getTerm(rsi->d_var_order[d_set_nums[f][i]])); - }else{ - break; - } - } - Trace("bound-int-rsi") << "Do substitution..." << std::endl; - //check if it has been instantiated - if (!vars.empty() && !d_bnd_it[f][v].hasInstantiated(subs)){ - //must add the lemma - Node nn = d_nground_range[f][v]; - nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); - Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[f][v] ); - Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; - d_quantEngine->getOutputChannel().lemma(lem, false, true); - l = Node::null(); - u = Node::null(); - return; - }else{ + if( getRsiSubsitution( f, v, vars, subs, rsi ) ){ u = u.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); l = l.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + }else{ + u = Node::null(); + l = Node::null(); } } } @@ -416,12 +473,86 @@ void BoundedIntegers::getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, void BoundedIntegers::getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ) { getBounds( f, v, rsi, l, u ); Trace("bound-int-rsi") << "Get value in model for..." << l << " and " << u << std::endl; - l = d_quantEngine->getModel()->getCurrentModelValue( l ); - u = d_quantEngine->getModel()->getCurrentModelValue( u ); + if( !l.isNull() ){ + l = d_quantEngine->getModel()->getCurrentModelValue( l ); + } + if( !u.isNull() ){ + u = d_quantEngine->getModel()->getCurrentModelValue( u ); + } Trace("bound-int-rsi") << "Value is " << l << " ... " << u << std::endl; return; } -bool BoundedIntegers::isGroundRange(Node f, Node v) { - return isBoundVar(f,v) && !getLowerBound(f,v).hasBoundVar() && !getUpperBound(f,v).hasBoundVar(); +bool BoundedIntegers::isGroundRange( Node q, Node v ) { + if( isBoundVar(q,v) ){ + if( d_bound_type[q][v]==BOUND_INT_RANGE ){ + return !getLowerBound(q,v).hasBoundVar() && !getUpperBound(q,v).hasBoundVar(); + }else if( d_bound_type[q][v]==BOUND_SET_MEMBER ){ + return !d_setm_range[q][v].hasBoundVar(); + } + } + return false; } + +Node BoundedIntegers::getSetRange( Node q, Node v, RepSetIterator * rsi ) { + Node sr = d_setm_range[q][v]; + if( d_nground_range[q].find(v)!=d_nground_range[q].end() ){ + //get the substitution + std::vector< Node > vars; + std::vector< Node > subs; + if( getRsiSubsitution( q, v, vars, subs, rsi ) ){ + sr = sr.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + }else{ + sr = Node::null(); + } + } + return sr; +} + +Node BoundedIntegers::getSetRangeValue( Node q, Node v, RepSetIterator * rsi ) { + Node sr = getSetRange( q, v, rsi ); + if( !sr.isNull() ){ + Trace("bound-int-rsi") << "Get value in model for..." << sr << std::endl; + sr = d_quantEngine->getModel()->getCurrentModelValue( sr ); + Trace("bound-int-rsi") << "Value is " << sr << std::endl; + } + return sr; +} + +bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ) { + + Trace("bound-int-rsi") << "Get bound value in model of variable " << v << std::endl; + Assert( d_set_nums[q].find( v )!=d_set_nums[q].end() ); + int vindex = d_set_nums[q][v]; + Assert( d_set_nums[q][v]==vindex ); + Trace("bound-int-rsi-debug") << " index order is " << vindex << std::endl; + //must take substitution for all variables that are iterating at higher level + for( int i=0; igetVariableOrder( i ); + Assert( q[0][v]==d_set[q][i] ); + Node t = rsi->getCurrentTerm( v ); + Trace("bound-int-rsi") << "term : " << t << std::endl; + vars.push_back( d_set[q][i] ); + subs.push_back( t ); + } + + //check if it has been instantiated + if( !vars.empty() && !d_bnd_it[q][v].hasInstantiated(subs) ){ + if( d_bound_type[q][v]==BOUND_INT_RANGE ){ + //must add the lemma + Node nn = d_nground_range[q][v]; + nn = nn.substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + Node lem = NodeManager::currentNM()->mkNode( LEQ, nn, d_range[q][v] ); + Trace("bound-int-lemma") << "*** Add lemma to minimize instantiated non-ground term " << lem << std::endl; + d_quantEngine->getOutputChannel().lemma(lem, false, true); + }else{ + //TODO : sets + } + return false; + }else{ + return true; + } +} + diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 7d15097bd..ab4bcba96 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -39,31 +39,57 @@ class BoundedIntegers : public QuantifiersModule typedef context::CDHashMap NodeIntMap; typedef context::CDHashMap NodeNodeMap; typedef context::CDHashMap IntBoolMap; +public: + enum { + BOUND_FINITE, + BOUND_INT_RANGE, + BOUND_SET_MEMBER, + BOUND_NONE + }; private: //for determining bounds bool isBound( Node f, Node v ); bool hasNonBoundVar( Node f, Node b ); - std::map< Node, std::map< Node, Node > > d_bounds[2]; + //bound type + std::map< Node, std::map< Node, unsigned > > d_bound_type; std::map< Node, std::vector< Node > > d_set; - std::map< Node, std::vector< int > > d_set_nums; + std::map< Node, std::map< Node, int > > d_set_nums; + //integer lower/upper bounds + std::map< Node, std::map< Node, Node > > d_bounds[2]; std::map< Node, std::map< Node, Node > > d_range; std::map< Node, std::map< Node, Node > > d_nground_range; + //set membership range + std::map< Node, std::map< Node, Node > > d_setm_range; void hasFreeVar( Node f, Node n ); void process( Node f, Node n, bool pol, + std::map< Node, unsigned >& bound_lit_type_map, std::map< int, std::map< Node, Node > >& bound_lit_map, - std::map< int, std::map< Node, bool > >& bound_lit_pol_map ); + std::map< int, std::map< Node, bool > >& bound_lit_pol_map, + std::map< int, std::map< Node, Node > >& bound_int_range_term ); void processLiteral( Node f, Node lit, bool pol, + std::map< Node, unsigned >& bound_lit_type_map, std::map< int, std::map< Node, Node > >& bound_lit_map, - std::map< int, std::map< Node, bool > >& bound_lit_pol_map ); + std::map< int, std::map< Node, bool > >& bound_lit_pol_map, + std::map< int, std::map< Node, Node > >& bound_int_range_term ); std::vector< Node > d_bound_quants; private: class RangeModel { + 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 { private: BoundedIntegers * d_bi; void allocateRange(); Node d_proxy_range; public: - RangeModel(BoundedIntegers * bi, Node r, context::Context* c, context::Context* u, bool isProxy); + 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; @@ -108,27 +134,36 @@ 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: BoundedIntegers( context::Context* c, QuantifiersEngine* qe ); - ~BoundedIntegers() throw() {} - + virtual ~BoundedIntegers(); + + void presolve(); bool needsCheck( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); void registerQuantifier( Node f ); void assertNode( Node n ); Node getNextDecisionRequest(); - bool isBoundVar( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); } - unsigned getNumBoundVars( Node f ) { return d_set[f].size(); } - Node getBoundVar( Node f, int i ) { return d_set[f][i]; } - int getBoundVarNum( Node f, int i ) { return d_set_nums[f][i]; } - Node getLowerBound( Node f, Node v ){ return d_bounds[0][f][v]; } - Node getUpperBound( Node f, Node v ){ return d_bounds[1][f][v]; } + 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(); } + Node getBoundVar( Node q, int i ) { return d_set[q][i]; } + //for integer range + Node getLowerBound( Node q, Node v ){ return d_bounds[0][q][v]; } + Node getUpperBound( Node q, Node v ){ return d_bounds[1][q][v]; } void getBounds( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); void getBoundValues( Node f, Node v, RepSetIterator * rsi, Node & l, Node & u ); bool isGroundRange(Node f, Node v); + //for set range + Node getSetRange( Node q, Node v, RepSetIterator * rsi ); + Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi ); /** Identify this module */ std::string identify() const { return "BoundedIntegers"; } +private: + bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ); }; } diff --git a/src/theory/quantifiers/first_order_model.cpp b/src/theory/quantifiers/first_order_model.cpp index a833f48d2..670f0eff3 100644 --- a/src/theory/quantifiers/first_order_model.cpp +++ b/src/theory/quantifiers/first_order_model.cpp @@ -406,8 +406,8 @@ Node FirstOrderModelIG::evaluateTerm( Node n, int& depIndex, RepSetIterator* ri //check the type of n if( n.getKind()==INST_CONSTANT ){ int v = n.getAttribute(InstVarNumAttribute()); - depIndex = ri->d_var_order[ v ]; - val = ri->getTerm( v ); + depIndex = ri->getIndexOrder( v ); + val = ri->getCurrentTerm( v ); }else if( n.getKind()==ITE ){ int depIndex1, depIndex2; int eval = evaluate( n[0], depIndex1, ri ); diff --git a/src/theory/quantifiers/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 8835d00bc..a0665cb7f 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -764,7 +764,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No Trace("fmc-exh-debug") << "Set element domains..." << std::endl; //set the domains based on the entry for (unsigned i=0; iisInterval(c[i]) || fm->isStar(c[i]) ){ @@ -773,6 +773,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No if (d_rep_ids[tn].find(c[i])!=d_rep_ids[tn].end()) { riter.d_domain[i].clear(); riter.d_domain[i].push_back(d_rep_ids[tn][c[i]]); + riter.d_enum_type[i] = RepSetIterator::ENUM_DOMAIN_ELEMENTS; }else{ Trace("fmc-exh") << "---- Does not have rep : " << c[i] << " for type " << tn << std::endl; return false; @@ -792,7 +793,7 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No std::vector< Node > ev_inst; std::vector< Node > inst; for( int i=0; igetUsedRepresentative( r ); @@ -826,18 +827,18 @@ bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, No int index = riter.increment(); Trace("fmc-exh-debug") << "Incremented index " << index << std::endl; if( !riter.isFinished() ){ - if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_RANGE) { + if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_INT_RANGE) { Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl; riter.increment2( index-1 ); } } } d_addedLemmas += addedLemmas; - Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.d_incomplete << std::endl; - return addedLemmas>0 || !riter.d_incomplete; + Trace("fmc-exh") << "----Finished Exhaustive instantiate, lemmas = " << addedLemmas << ", incomplete=" << riter.isIncomplete() << std::endl; + return addedLemmas>0 || !riter.isIncomplete(); }else{ Trace("fmc-exh") << "----Finished Exhaustive instantiate, failed." << std::endl; - return false; + return !riter.isIncomplete(); } } diff --git a/src/theory/quantifiers/inst_strategy_e_matching.cpp b/src/theory/quantifiers/inst_strategy_e_matching.cpp index 5b5f9fc22..efd765c86 100644 --- a/src/theory/quantifiers/inst_strategy_e_matching.cpp +++ b/src/theory/quantifiers/inst_strategy_e_matching.cpp @@ -278,8 +278,8 @@ void InstStrategyAutoGenTriggers::generateTriggers( Node f ){ Trace("auto-gen-trigger-debug") << "Collected pat terms for " << bd << ", no-patterns : " << d_user_no_gen[f].size() << std::endl; for( unsigned i=0; i terms; for( int k=0; kgetInstantiation( f, vars, terms ); Node val = fm->getValue( n ); @@ -84,7 +84,9 @@ void QModelBuilder::debugModel( FirstOrderModel* fm ){ } Trace("quant-check-model") << "." << std::endl; }else{ - Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl; + if( riter.isIncomplete() ){ + Trace("quant-check-model") << "Warning: Could not test quantifier " << f << std::endl; + } } } } @@ -399,15 +401,19 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i Debug("inst-fmf-ei") << "Begin instantiation..." << std::endl; while( !riter.isFinished() && ( d_addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ d_triedLemmas++; - for( int i=0; i<(int)riter.d_index.size(); i++ ){ - Trace("try") << i << " : " << riter.d_index[i] << " : " << riter.getTerm( i ) << std::endl; + if( Debug.isOn("inst-fmf-ei-debug") ){ + for( int i=0; i<(int)riter.d_index.size(); i++ ){ + Debug("inst-fmf-ei-debug") << i << " : " << riter.d_index[i] << " : " << riter.getCurrentTerm( i ) << std::endl; + } } int eval = 0; int depIndex; //see if instantiation is already true in current model - Debug("fmf-model-eval") << "Evaluating "; - riter.debugPrintSmall("fmf-model-eval"); - Debug("fmf-model-eval") << "Done calculating terms." << std::endl; + if( Debug.isOn("fmf-model-eval") ){ + Debug("fmf-model-eval") << "Evaluating "; + riter.debugPrintSmall("fmf-model-eval"); + Debug("fmf-model-eval") << "Done calculating terms." << std::endl; + } //if evaluate(...)==1, then the instantiation is already true in the model // depIndex is the index of the least significant variable that this evaluation relies upon depIndex = riter.getNumTerms()-1; @@ -425,7 +431,7 @@ bool QModelBuilderIG::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i //instantiation was not shown to be true, construct the match InstMatch m( f ); for( int i=0; igetModel()->d_rep_set) ); if( riter.setQuantifier( f ) ){ - Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.d_incomplete << "..." << std::endl; - if( !riter.d_incomplete ){ + Trace("fmf-exh-inst") << "...exhaustive instantiation set, incomplete=" << riter.isIncomplete() << "..." << std::endl; + if( !riter.isIncomplete() ){ int triedLemmas = 0; int addedLemmas = 0; while( !riter.isFinished() && ( addedLemmas==0 || !options::fmfOneInstPerRound() ) ){ //instantiation was not shown to be true, construct the match InstMatch m( f ); for( int i=0; i& added, bool withinQuant, bool wi } Node op = getMatchOperator( n ); + Trace("term-db-debug") << " match operator is : " << op << std::endl; d_op_map[op].push_back( n ); added.insert( n ); @@ -893,6 +894,7 @@ void TermDb::makeInstantiationConstantsFor( Node q ){ Debug("quantifiers-engine") << "Instantiation constants for " << q << " : " << std::endl; for( unsigned i=0; imkInstConstant( q[0][i].getType() ); d_inst_constants_map[ic] = q; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 3f931014b..7ab3668eb 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -300,6 +300,7 @@ public: private: /** map from universal quantifiers to the list of variables */ std::map< Node, std::vector< Node > > d_vars; + std::map< Node, std::map< Node, unsigned > > d_var_num; /** map from universal quantifiers to the list of instantiation constants */ std::map< Node, std::vector< Node > > d_inst_constants; /** map from universal quantifiers to their inst constant body */ @@ -311,6 +312,8 @@ private: /** make instantiation constants for */ void makeInstantiationConstantsFor( Node q ); public: + /** get variable number */ + unsigned getVariableNum( Node q, Node v ) { return d_var_num[q][v]; } /** get the i^th instantiation constant of q */ Node getInstantiationConstant( Node q, int i ) const; /** get number of instantiation constants for q */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 8b51e94b5..2bebabc5a 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -634,6 +634,7 @@ bool QuantifiersEngine::registerQuantifier( Node f ){ //check whether we should apply a reduction if( reduceQuantifier( f ) ){ + Trace("quant") << "...reduced." << std::endl; d_quants[f] = false; return false; }else{ diff --git a/src/theory/rep_set.cpp b/src/theory/rep_set.cpp index d7178a8c1..184553ba7 100644 --- a/src/theory/rep_set.cpp +++ b/src/theory/rep_set.cpp @@ -127,19 +127,11 @@ int RepSet::getNumRelevantGroundReps( TypeNode t ) { } void RepSet::toStream(std::ostream& out){ -#if 0 - for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ - out << it->first << " : " << std::endl; - for( int i=0; i<(int)it->second.size(); i++ ){ - out << " " << i << ": " << it->second[i] << std::endl; - } - } -#else for( std::map< TypeNode, std::vector< Node > >::iterator it = d_type_reps.begin(); it != d_type_reps.end(); ++it ){ if( !it->first.isFunction() && !it->first.isPredicate() ){ out << "(" << it->first << " " << it->second.size(); out << " ("; - for( int i=0; i<(int)it->second.size(); i++ ){ + for( unsigned i=0; isecond.size(); i++ ){ if( i>0 ){ out << " "; } out << it->second[i]; } @@ -147,7 +139,6 @@ void RepSet::toStream(std::ostream& out){ out << ")" << std::endl; } } -#endif } @@ -157,10 +148,11 @@ RepSetIterator::RepSetIterator( QuantifiersEngine * qe, RepSet* rs ) : d_qe(qe), int RepSetIterator::domainSize( int i ) { Assert(i>=0); - if( d_enum_type[i]==ENUM_DOMAIN_ELEMENTS ){ - return d_domain[i].size(); + int v = d_var_order[i]; + if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){ + return d_domain[v].size(); }else{ - return d_domain[i][0]; + return d_domain[v][0]; } } @@ -188,15 +180,15 @@ bool RepSetIterator::setFunctionDomain( Node op ){ bool RepSetIterator::initialize(){ Trace("rsi") << "Initialize rep set iterator..." << std::endl; - for( size_t i=0; ihasType( tn ) ){ @@ -209,59 +201,59 @@ bool RepSetIterator::initialize(){ Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); } - }else if( tn.isInteger() ){ - bool inc = false; - //check if it is bound + }else{ + bool inc = true; + //check if it is bound by bounded integer module if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ - if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][i] ) ){ + unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] ); + if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){ Trace("rsi") << " variable is bounded integer." << std::endl; - d_enum_type.push_back( ENUM_RANGE ); - }else{ - inc = true; + d_enum_type.push_back( ENUM_INT_RANGE ); + inc = false; + }else if( bvt==quantifiers::BoundedIntegers::BOUND_SET_MEMBER ){ + Trace("rsi") << " variable is bounded by set membership." << std::endl; + d_enum_type.push_back( ENUM_SET_MEMBERS ); + inc = false; } - }else{ - inc = true; } if( inc ){ //check if it is otherwise bound - if( d_bounds[0].find(i)!=d_bounds[0].end() && d_bounds[1].find(i)!=d_bounds[1].end() ){ + if( d_bounds[0].find( v )!=d_bounds[0].end() && d_bounds[1].find( v )!=d_bounds[1].end() ){ Trace("rsi") << " variable is bounded." << std::endl; - d_enum_type.push_back( ENUM_RANGE ); + d_enum_type.push_back( ENUM_INT_RANGE ); + }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ + Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; + d_rep_set->complete( tn ); + //must have succeeded + Assert( d_rep_set->hasType( tn ) ); }else{ Trace("rsi") << " variable cannot be bounded." << std::endl; - Trace("fmf-incomplete") << "Incomplete because of integer quantification of " << d_owner[0][i] << "." << std::endl; + Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; d_incomplete = true; } } - //enumerate if the sort is reasonably small - }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ - Trace("rsi") << " do complete, since cardinality is small (" << tn.getCardinality() << ")..." << std::endl; - d_rep_set->complete( tn ); - //must have succeeded - Assert( d_rep_set->hasType( tn ) ); - }else{ - Trace("rsi") << " variable cannot be bounded." << std::endl; - Trace("fmf-incomplete") << "Incomplete because of quantification of type " << tn << std::endl; - d_incomplete = true; } //if we have yet to determine the type of enumeration - if( d_enum_type.size()<=i ){ + if( d_enum_type.size()<=v ){ d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); if( d_rep_set->hasType( tn ) ){ - for( size_t j=0; jd_type_reps[tn].size(); j++ ){ - d_domain[i].push_back( j ); + for( unsigned j=0; jd_type_reps[tn].size(); j++ ){ + d_domain[v].push_back( j ); } }else{ + Assert( d_incomplete ); return false; } } } //must set a variable index order based on bounded integers - if (d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers()) { + if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ Trace("bound-int-rsi") << "Calculating variable order..." << std::endl; std::vector< int > varOrder; - for( unsigned i=0; igetBoundedIntegers()->getNumBoundVars(d_owner); i++ ){ - varOrder.push_back(d_qe->getBoundedIntegers()->getBoundVarNum(d_owner,i)); + for( unsigned i=0; igetBoundedIntegers()->getNumBoundVars( d_owner ); i++ ){ + Node v = d_qe->getBoundedIntegers()->getBoundVar( d_owner, i ); + Trace("bound-int-rsi") << " bound var #" << i << " is " << v << std::endl; + varOrder.push_back( d_qe->getTermDatabase()->getVariableNum( d_owner, v ) ); } for( unsigned i=0; igetBoundedIntegers()->isBoundVar(d_owner, d_owner[0][i])) { @@ -283,14 +275,10 @@ bool RepSetIterator::initialize(){ Trace("bound-int-rsi") << indexOrder[i] << " "; } Trace("bound-int-rsi") << std::endl; - setIndexOrder(indexOrder); + setIndexOrder( indexOrder ); } //now reset the indices - for (unsigned i=0; i& indexOrder ){ d_index_order.clear(); d_index_order.insert( d_index_order.begin(), indexOrder.begin(), indexOrder.end() ); //make the d_var_order mapping - for( int i=0; i<(int)d_index_order.size(); i++ ){ + for( unsigned i=0; i& domain ){ - d_domain.clear(); - d_domain.insert( d_domain.begin(), domain.begin(), domain.end() ); - //we are done if a domain is empty - for( int i=0; i<(int)d_domain.size(); i++ ){ - if( d_domain[i].empty() ){ - d_index.clear(); - } - } -} -*/ -bool RepSetIterator::resetIndex( int i, bool initial ) { + +int RepSetIterator::resetIndex( int i, bool initial ) { d_index[i] = 0; - int ii = d_index_order[i]; - Trace("bound-int-rsi") << "Reset " << i << " " << ii << " " << initial << std::endl; + int v = d_var_order[i]; + Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl; //determine the current range - if( d_enum_type[ii]==ENUM_RANGE ){ - if( initial || ( d_qe->getBoundedIntegers() && !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][ii] ) ) ){ - Trace("bound-int-rsi") << "Getting range of " << d_owner[0][ii] << std::endl; + if( initial || ( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() && + d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) && + !d_qe->getBoundedIntegers()->isGroundRange( d_owner, d_owner[0][v] ) ) ){ + Trace("bound-int-rsi") << "Getting range of " << d_owner[0][v] << std::endl; + if( d_enum_type[v]==ENUM_INT_RANGE ){ Node actual_l; Node l, u; - if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ - d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][ii], this, l, u ); + if( d_qe->getBoundedIntegers() ){ + unsigned bvt = d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] ); + if( bvt==quantifiers::BoundedIntegers::BOUND_INT_RANGE ){ + d_qe->getBoundedIntegers()->getBoundValues( d_owner, d_owner[0][v], this, l, u ); + } } for( unsigned b=0; b<2; b++ ){ - if( d_bounds[b].find(ii)!=d_bounds[b].end() ){ - Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][ii] << std::endl; - if( b==0 && (l.isNull() || d_bounds[b][ii].getConst() > l.getConst()) ){ + if( d_bounds[b].find(v)!=d_bounds[b].end() ){ + Trace("bound-int-rsi") << "May further limit bound(" << b << ") based on " << d_bounds[b][v] << std::endl; + if( b==0 && (l.isNull() || d_bounds[b][v].getConst() > l.getConst()) ){ if( !l.isNull() ){ //bound was limited externally, record that the value lower bound is not equal to the term lower bound - actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], l ); + actual_l = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v], l ); } - l = d_bounds[b][ii]; - }else if( b==1 && (u.isNull() || d_bounds[b][ii].getConst() <= u.getConst()) ){ - u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][ii], + l = d_bounds[b][v]; + }else if( b==1 && (u.isNull() || d_bounds[b][v].getConst() <= u.getConst()) ){ + u = NodeManager::currentNM()->mkNode( MINUS, d_bounds[b][v], NodeManager::currentNM()->mkConst( Rational(1) ) ); u = Rewriter::rewrite( u ); } @@ -346,73 +328,109 @@ bool RepSetIterator::resetIndex( int i, bool initial ) { if( l.isNull() || u.isNull() ){ //failed, abort the iterator - d_index.clear(); - return false; + return -1; }else{ - Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][ii] << " to " << l << "..." << u << std::endl; + Trace("bound-int-rsi") << "Can limit bounds of " << d_owner[0][v] << " to " << l << "..." << u << std::endl; Node range = Rewriter::rewrite( NodeManager::currentNM()->mkNode( MINUS, u, l ) ); Node ra = Rewriter::rewrite( NodeManager::currentNM()->mkNode( LEQ, range, NodeManager::currentNM()->mkConst( Rational( 9999 ) ) ) ); - d_domain[ii].clear(); + d_domain[v].clear(); Node tl = l; Node tu = u; - if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][ii] ) ){ - d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][ii], this, tl, tu ); + if( d_qe->getBoundedIntegers() && d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){ + d_qe->getBoundedIntegers()->getBounds( d_owner, d_owner[0][v], this, tl, tu ); } - d_lower_bounds[ii] = tl; + d_lower_bounds[v] = tl; if( !actual_l.isNull() ){ //if bound was limited externally, must consider the offset - d_lower_bounds[ii] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) ); + d_lower_bounds[v] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) ); } - if( ra==NodeManager::currentNM()->mkConst(true) ){ + if( ra==d_qe->getTermDatabase()->d_true ){ long rr = range.getConst().getNumerator().getLong()+1; Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; - d_domain[ii].push_back( (int)rr ); + d_domain[v].push_back( (int)rr ); + if( rr<=0 ){ + return 0; + } }else{ - Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][ii] << "." << std::endl; - d_incomplete = true; - d_domain[ii].push_back( 0 ); + Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << d_owner[0][v] << "." << std::endl; + return -1; } } - }else{ - Trace("bound-int-rsi") << d_owner[0][ii] << " has ground range, skip." << std::endl; + }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){ + Assert( d_qe->getBoundedIntegers()->getBoundVarType( d_owner, d_owner[0][v] )==quantifiers::BoundedIntegers::BOUND_SET_MEMBER ); + Node srv = d_qe->getBoundedIntegers()->getSetRangeValue( d_owner, d_owner[0][v], this ); + if( srv.isNull() ){ + return -1; + } + Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl; + d_domain[v].clear(); + d_setm_bounds[v].clear(); + if( srv.getKind()!=EMPTYSET ){ + //TODO: need term model, not value model + while( srv.getKind()==UNION ){ + Assert( srv[1].getKind()==kind::SINGLETON ); + d_setm_bounds[v].push_back( srv[1][0] ); + srv = srv[0]; + } + d_setm_bounds[v].push_back( srv[0] ); + d_domain[v].push_back( d_setm_bounds[v].size() ); + }else{ + d_domain[v].push_back( 0 ); + return 0; + } } } - return true; + return 1; } -int RepSetIterator::increment2( int counter ){ +int RepSetIterator::increment2( int i ){ Assert( !isFinished() ); #ifdef DISABLE_EVAL_SKIP_MULTIPLE - counter = (int)d_index.size()-1; + i = (int)d_index.size()-1; #endif //increment d_index - if( counter>=0){ - Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl; + if( i>=0){ + Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; } - while( counter>=0 && d_index[counter]>=(int)(domainSize(counter)-1) ){ - counter--; - if( counter>=0){ - Trace("rsi-debug") << "domain size of " << counter << " is " << domainSize(counter) << std::endl; + while( i>=0 && d_index[i]>=(int)(domainSize(i)-1) ){ + i--; + if( i>=0){ + Trace("rsi-debug") << "domain size of " << i << " is " << domainSize(i) << std::endl; } } - if( counter==-1 ){ + if( i==-1 ){ d_index.clear(); + return -1; }else{ - d_index[counter]++; - bool emptyDomain = false; - for( int i=(int)d_index.size()-1; i>counter; i-- ){ - if (!resetIndex(i)){ - break; - }else if( domainSize(i)<=0 ){ - emptyDomain = true; - } + Trace("rsi-debug") << "increment " << i << std::endl; + d_index[i]++; + return do_reset_increment( i ); + } +} + +int RepSetIterator::do_reset_increment( int i, bool initial ) { + bool emptyDomain = false; + for( unsigned ii=(i+1); iimkNode(PLUS, d_lower_bounds[index], - NodeManager::currentNM()->mkConst( Rational(d_index[index]) ) ); + Trace("rsi-debug") << "Get, with offset : " << v << " " << d_lower_bounds[v] << " " << curr << std::endl; + Assert( !d_lower_bounds[v].isNull() ); + Node t = NodeManager::currentNM()->mkNode(PLUS, d_lower_bounds[v], NodeManager::currentNM()->mkConst( Rational(curr) ) ); t = Rewriter::rewrite( t ); return t; } } void RepSetIterator::debugPrint( const char* c ){ - for( int i=0; i<(int)d_index.size(); i++ ){ - Debug( c ) << i << " : " << d_index[i] << " : " << getTerm( i ) << std::endl; + for( unsigned v=0; v d_lower_bounds; + //for set ranges + std::map< int, std::vector< Node > > d_setm_bounds; //domain size int domainSize( int i ); //node this is rep set iterator is for Node d_owner; - //reset index - bool resetIndex( int i, bool initial = false ); + //reset index, 1:success, 0:empty, -1:fail + int resetIndex( int i, bool initial = false ); /** set index order */ void setIndexOrder( std::vector< int >& indexOrder ); + /** do reset increment the iterator at index=counter */ + int do_reset_increment( int counter, bool initial = false ); + //ordering for variables we are indexing over + // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, + // then we consider instantiations in this order: + // a/x a/y a/z + // a/x b/y a/z + // b/x a/y a/z + // b/x b/y a/z + // ... + std::vector< int > d_index_order; + //variables to index they are considered at + // for example, if d_index_order = { 2, 0, 1 } + // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } + std::map< int, int > d_var_order; + //are we only considering a strict subset of the domain of the quantifier? + bool d_incomplete; public: RepSetIterator( QuantifiersEngine * qe, RepSet* rs ); ~RepSetIterator(){} @@ -92,43 +112,34 @@ public: RepSet* d_rep_set; //enumeration type? std::vector< int > d_enum_type; - //index we are considering + //current tuple we are considering std::vector< int > d_index; //types we are considering std::vector< TypeNode > d_types; //domain we are considering std::vector< RepDomain > d_domain; - //are we only considering a strict subset of the domain of the quantifier? - bool d_incomplete; - //ordering for variables we are indexing over - // for example, given reps = { a, b } and quantifier forall( x, y, z ) P( x, y, z ) with d_index_order = { 2, 0, 1 }, - // then we consider instantiations in this order: - // a/x a/y a/z - // a/x b/y a/z - // b/x a/y a/z - // b/x b/y a/z - // ... - std::vector< int > d_index_order; - //variables to index they are considered at - // for example, if d_index_order = { 2, 0, 1 } - // then d_var_order = { 0 -> 1, 1 -> 2, 2 -> 0 } - std::map< int, int > d_var_order; //intervals std::map< int, Node > d_bounds[2]; public: /** increment the iterator at index=counter */ - int increment2( int counter ); + int increment2( int i ); /** increment the iterator */ int increment(); /** is the iterator finished? */ bool isFinished(); /** get the i_th term we are considering */ - Node getTerm( int i ); + Node getCurrentTerm( int v ); /** get the number of terms we are considering */ int getNumTerms() { return (int)d_index_order.size(); } /** debug print */ void debugPrint( const char* c ); void debugPrintSmall( const char* c ); + //get index order, returns var # + int getIndexOrder( int v ) { return d_index_order[v]; } + //get variable order, returns index # + int getVariableOrder( int i ) { return d_var_order[i]; } + //is incomplete + bool isIncomplete() { return d_incomplete; } };/* class RepSetIterator */ }/* CVC4::theory namespace */ diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index efb737a29..497ce5f8c 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -127,7 +127,9 @@ TheoryStrings::TheoryStrings(context::Context* c, context::UserContext* u, } TheoryStrings::~TheoryStrings() { - + for( std::map< Node, EqcInfo* >::iterator it = d_eqc_info.begin(); it != d_eqc_info.end(); ++it ){ + delete it->second; + } } Node TheoryStrings::getRepresentative( Node t ) { diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index 6e1c6e918..b7daadfd1 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -56,7 +56,8 @@ TESTS = \ ForElimination-scala-9.smt2 \ agree466.smt2 \ LeftistHeap.scala-8-ncm.smt2 \ - sc-crash-052316.smt2 + sc-crash-052316.smt2 \ + bound-int-alt.smt2 EXTRA_DIST = $(TESTS) diff --git a/test/regress/regress0/fmf/bound-int-alt.smt2 b/test/regress/regress0/fmf/bound-int-alt.smt2 new file mode 100644 index 000000000..146487925 --- /dev/null +++ b/test/regress/regress0/fmf/bound-int-alt.smt2 @@ -0,0 +1,18 @@ +; COMMAND-LINE: --fmf-bound-int +; EXPECT: sat +(set-logic UFLIA) +(set-info :status sat) +(declare-sort U 0) +(declare-sort V 0) +(declare-fun P (U Int V Int U Int) Bool) + +(assert (forall ((x U) (y Int) (z V) (w Int) (v U) (d Int)) (=> (and (<= 0 d 1) (<= 2 y 6) (<= 40 w (+ 37 y))) (P x y z w v d)))) + +(declare-fun a () U) +(declare-fun b () V) + +(assert (not (P a 2 b 40 a 0))) +(assert (not (P a 6 b 39 a 0))) +(assert (not (P a 6 b 44 a 0))) + +(check-sat) -- 2.30.2