From e8c09abb9165278b13491c83bdcbe17ae535126e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Wed, 7 Dec 2016 12:43:15 -0600 Subject: Refactoring, generalization of bounded inference module. Simplification of rep set iterator. Disable quantifiers dynamic splitting for variables that are inferred bounded. Minor changes to fmc mbqi. Add regressions. --- src/theory/quantifiers/bounded_integers.cpp | 298 ++++++++++++++++++++++------ src/theory/quantifiers/bounded_integers.h | 30 +-- src/theory/quantifiers/full_model_check.cpp | 67 +++---- src/theory/quantifiers/quant_split.cpp | 6 +- src/theory/quantifiers_engine.cpp | 17 +- src/theory/quantifiers_engine.h | 2 + src/theory/rep_set.cpp | 166 ++++------------ src/theory/rep_set.h | 21 +- 8 files changed, 348 insertions(+), 259 deletions(-) (limited to 'src/theory') diff --git a/src/theory/quantifiers/bounded_integers.cpp b/src/theory/quantifiers/bounded_integers.cpp index dc0019383..1112c2ef2 100644 --- a/src/theory/quantifiers/bounded_integers.cpp +++ b/src/theory/quantifiers/bounded_integers.cpp @@ -171,31 +171,110 @@ bool BoundedIntegers::isBound( Node f, Node v ) { return std::find( d_set[f].begin(), d_set[f].end(), v )!=d_set[f].end(); } -bool BoundedIntegers::hasNonBoundVar( Node f, Node b ) { - if( b.getKind()==BOUND_VARIABLE ){ - if( !isBound( f, b ) ){ - return true; - } - }else{ - for( unsigned i=0; i& visited ) { + if( visited.find( b )==visited.end() ){ + visited[b] = true; + if( b.getKind()==BOUND_VARIABLE ){ + if( !isBound( f, b ) ){ return true; } + }else{ + for( unsigned i=0; i visited; + return hasNonBoundVar( f, b, visited ); +} -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, - std::map< int, std::map< Node, Node > >& bound_int_range_term ) { - if( lit.getKind()==GEQ ){ - if( lit[0].getType().isInteger() ){ +bool BoundedIntegers::processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ) { + if( n.getKind()==EQUAL ){ + for( unsigned i=0; i<2; i++ ){ + Node t = n[i]; + if( !hasNonBoundVar( q, n[1-i] ) ){ + if( t==v ){ + v_cases.push_back( n[1-i] ); + return true; + }else if( v.isNull() && t.getKind()==BOUND_VARIABLE ){ + v = t; + v_cases.push_back( n[1-i] ); + return true; + } + } + } + } + return false; +} + +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, Node > >& bound_int_range_term, + std::map< Node, std::vector< Node > >& bound_fixed_set ){ + if( n.getKind()==OR || n.getKind()==AND ){ + if( (n.getKind()==OR)==pol ){ + for( unsigned i=0; i v_cases; + bool success = true; + for( unsigned i=0; i v_cases; + if( processEqDisjunct( q, n, v, v_cases ) ){ + if( !isBound( q, v ) ){ + bound_lit_type_map[v] = BOUND_FIXED_SET; + bound_lit_map[0][v] = n; + bound_lit_pol_map[0][v] = pol; + Assert( v_cases.size()==1 ); + bound_fixed_set[v].clear(); + bound_fixed_set[v].push_back( v_cases[0] ); + } + } + } + }else if( n.getKind()==NOT ){ + process( q, n[0], !pol, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set ); + }else if( n.getKind()==GEQ ){ + if( n[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; + if( QuantArith::getMonomialSumLit( n, msum ) ){ + Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " 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 ) ){ @@ -221,7 +300,7 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol, 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_map[loru][it->first] = n; bound_lit_pol_map[loru][it->first] = pol; }else{ Trace("bound-int-debug") << "The term " << t << " has non-bound variable." << std::endl; @@ -231,32 +310,15 @@ void BoundedIntegers::processLiteral( Node q, Node lit, bool pol, } } } - }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( n.getKind()==MEMBER ){ + if( !pol && n[0].getKind()==BOUND_VARIABLE && !isBound( q, n[0] ) && !hasNonBoundVar( q, n[1] ) ){ + Trace("bound-int-debug") << "literal (polarity = " << pol << ") " << n << " is membership." << std::endl; + bound_lit_type_map[n[0]] = BOUND_SET_MEMBER; + bound_lit_map[0][n[0]] = n; + bound_lit_pol_map[0][n[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 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, Node > >& bound_int_range_term ){ - if( (n.getKind()==OR && pol) || (n.getKind()==AND && !pol) ){ - for( unsigned i=0; i > 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; + std::map< Node, std::vector< Node > > bound_fixed_set; success = false; - process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term ); + process( f, f[1], true, bound_lit_type_map, bound_lit_map, bound_lit_pol_map, bound_int_range_term, bound_fixed_set ); //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; @@ -315,7 +379,6 @@ void BoundedIntegers::registerQuantifier( Node f ) { 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; for( unsigned b=0; b<2; b++ ){ //set the bounds Assert( bound_int_range_term[b].find( v )!=bound_int_range_term[b].end() ); @@ -330,9 +393,23 @@ void BoundedIntegers::registerQuantifier( Node f ) { setBoundVar = true; d_setm_range[f][v] = bound_lit_map[0][v][1]; d_setm_range_lit[f][v] = bound_lit_map[0][v]; + d_range[f][v] = NodeManager::currentNM()->mkNode( CARD, d_setm_range[f][v] ); Trace("bound-int") << "Variable " << v << " is bound because of set membership literal " << bound_lit_map[0][v] << std::endl; + }else if( it->second==BOUND_FIXED_SET ){ + setBoundedVar( f, v, BOUND_FIXED_SET ); + setBoundVar = true; + for( unsigned i=0; imayComplete( tn ) ){ + success = true; + setBoundedVar( f, f[0][i], BOUND_FINITE ); + break; + } + } + } + } }while( success ); Trace("bound-int") << "Bounds are : " << std::endl; @@ -361,12 +451,9 @@ void BoundedIntegers::registerQuantifier( Node f ) { bool bound_success = true; 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; - } + 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; } } @@ -375,17 +462,13 @@ void BoundedIntegers::registerQuantifier( Node f ) { for( unsigned i=0; imkNode( CARD, d_setm_range[f][v] ); - } + Node r = d_range[f][v]; + Assert( !r.isNull() ); bool isProxy = false; if( r.hasBoundVar() ){ //introduce a new bound Node new_range = NodeManager::currentNM()->mkSkolem( "bir", r.getType(), "bound for term" ); - d_nground_range[f][v] = d_range[f][v]; + d_nground_range[f][v] = r; d_range[f][v] = new_range; r = new_range; isProxy = true; @@ -403,6 +486,10 @@ void BoundedIntegers::registerQuantifier( Node f ) { } } +void BoundedIntegers::registerQuantifier( Node q ) { + +} + void BoundedIntegers::assertNode( Node n ) { Trace("bound-int-assert") << "Assert " << n << std::endl; Node nlit = n.getKind()==NOT ? n[0] : n; @@ -490,6 +577,8 @@ bool BoundedIntegers::isGroundRange( Node q, Node v ) { 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(); + }else if( d_bound_type[q][v]==BOUND_FIXED_SET ){ + return !d_fixed_set_ngr_range[q][v].empty(); } } return false; @@ -592,21 +681,23 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va Assert( q[0][v]==d_set[q][i] ); Node t = rsi->getCurrentTerm( v ); Trace("bound-int-rsi") << "term : " << t << std::endl; + if( rsi->d_rep_set->d_values_to_terms.find( t )!=rsi->d_rep_set->d_values_to_terms.end() ){ + t = rsi->d_rep_set->d_values_to_terms[t]; + Trace("bound-int-rsi") << "term (post-rep) : " << 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 ){ + if( d_bound_type[q][v]==BOUND_INT_RANGE || d_bound_type[q][v]==BOUND_SET_MEMBER ){ //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{ @@ -614,3 +705,84 @@ bool BoundedIntegers::getRsiSubsitution( Node q, Node v, std::vector< Node >& va } } +bool BoundedIntegers::getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ) { + if( initial || !isGroundRange( q, v ) ){ + elements.clear(); + unsigned bvt = getBoundVarType( q, v ); + if( bvt==BOUND_INT_RANGE ){ + Node l, u; + getBoundValues( q, v, rsi, l, u ); + if( l.isNull() || u.isNull() ){ + //failed, abort the iterator + return false; + }else{ + Trace("bound-int-rsi") << "Can limit bounds of " << 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 ) ) ) ); + Node tl = l; + Node tu = u; + getBounds( q, v, rsi, tl, tu ); + Assert( !tl.isNull() && !tu.isNull() ); + if( ra==d_quantEngine->getTermDatabase()->d_true ){ + long rr = range.getConst().getNumerator().getLong()+1; + Trace("bound-int-rsi") << "Actual bound range is " << rr << std::endl; + for( unsigned k=0; kmkNode(PLUS, tl, NodeManager::currentNM()->mkConst( Rational(k) ) ); + t = Rewriter::rewrite( t ); + elements.push_back( t ); + } + return true; + }else{ + Trace("fmf-incomplete") << "Incomplete because of integer quantification, bounds are too big for " << v << "." << std::endl; + return false; + } + } + }else if( bvt==BOUND_SET_MEMBER ){ + Node srv = getSetRangeValue( q, v, rsi ); + if( srv.isNull() ){ + return false; + }else{ + Trace("bound-int-rsi") << "Bounded by set membership : " << srv << std::endl; + if( srv.getKind()!=EMPTYSET ){ + while( srv.getKind()==UNION ){ + Assert( srv[1].getKind()==kind::SINGLETON ); + elements.push_back( srv[1][0] ); + srv = srv[0]; + } + Assert( srv.getKind()==kind::SINGLETON ); + elements.push_back( srv[0] ); + } + return true; + } + }else if( bvt==BOUND_FIXED_SET ){ + std::map< Node, std::vector< Node > >::iterator it = d_fixed_set_gr_range[q].find( v ); + if( it!=d_fixed_set_gr_range[q].end() ){ + for( unsigned i=0; isecond.size(); i++ ){ + elements.push_back( it->second[i] ); + } + } + it = d_fixed_set_ngr_range[q].find( v ); + if( it!=d_fixed_set_ngr_range[q].end() ){ + std::vector< Node > vars; + std::vector< Node > subs; + if( getRsiSubsitution( q, v, vars, subs, rsi ) ){ + for( unsigned i=0; isecond.size(); i++ ){ + Node t = it->second[i].substitute( vars.begin(), vars.end(), subs.begin(), subs.end() ); + elements.push_back( t ); + } + return true; + }else{ + return false; + } + }else{ + return true; + } + }else{ + return false; + } + }else{ + //no change required + return true; + } +} + diff --git a/src/theory/quantifiers/bounded_integers.h b/src/theory/quantifiers/bounded_integers.h index 0dfd7eafd..5c5a52855 100644 --- a/src/theory/quantifiers/bounded_integers.h +++ b/src/theory/quantifiers/bounded_integers.h @@ -44,34 +44,36 @@ public: BOUND_FINITE, BOUND_INT_RANGE, BOUND_SET_MEMBER, + BOUND_FIXED_SET, BOUND_NONE }; private: //for determining bounds bool isBound( Node f, Node v ); + bool hasNonBoundVar( Node f, Node b, std::map< Node, bool >& visited ); bool hasNonBoundVar( Node f, Node b ); //bound type std::map< Node, std::map< Node, unsigned > > d_bound_type; std::map< Node, std::vector< Node > > d_set; 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; + //integer lower/upper bounds + std::map< Node, std::map< Node, Node > > d_bounds[2]; //set membership range std::map< Node, std::map< Node, Node > > d_setm_range; std::map< Node, std::map< Node, Node > > d_setm_range_lit; + //fixed finite set range + std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_gr_range; + std::map< Node, std::map< Node, std::vector< Node > > > d_fixed_set_ngr_range; void hasFreeVar( Node f, Node n ); - void process( Node f, Node n, bool pol, + void 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, 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, Node > >& bound_int_range_term ); + std::map< int, std::map< Node, Node > >& bound_int_range_term, + std::map< Node, std::vector< Node > >& bound_fixed_set ); + bool processEqDisjunct( Node q, Node n, Node& v, std::vector< Node >& v_cases ); std::vector< Node > d_bound_quants; private: class RangeModel { @@ -144,13 +146,15 @@ public: void presolve(); bool needsCheck( Theory::Effort e ); void check( Theory::Effort e, unsigned quant_e ); - void registerQuantifier( Node f ); + void registerQuantifier( Node q ); + void preRegisterQuantifier( Node q ); void assertNode( Node n ); Node getNextDecisionRequest( unsigned& priority ); 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]; } +private: //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]; } @@ -160,11 +164,13 @@ public: //for set range Node getSetRange( Node q, Node v, RepSetIterator * rsi ); Node getSetRangeValue( Node q, Node v, RepSetIterator * rsi ); + + bool getRsiSubsitution( Node q, Node v, std::vector< Node >& vars, std::vector< Node >& subs, RepSetIterator * rsi ); +public: + bool getBoundElements( RepSetIterator * rsi, bool initial, Node q, Node v, std::vector< Node >& elements ); /** 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/full_model_check.cpp b/src/theory/quantifiers/full_model_check.cpp index 6b756428b..7e528fef3 100644 --- a/src/theory/quantifiers/full_model_check.cpp +++ b/src/theory/quantifiers/full_model_check.cpp @@ -737,56 +737,37 @@ int FullModelChecker::doExhaustiveInstantiation( FirstOrderModel * fm, Node f, i } } +class RepBoundFmcEntry : public RepBoundExt { +public: + Node d_entry; + FirstOrderModelFmc * d_fm; + bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) { + if( d_fm->isInterval(d_entry[i]) ){ + //explicitly add the interval TODO? + }else if( d_fm->isStar(d_entry[i]) ){ + //add the full range + return false; + }else{ + //only need to consider the single point + elements.push_back( d_entry[i] ); + return true; + } + return false; + } +}; + bool FullModelChecker::exhaustiveInstantiate(FirstOrderModelFmc * fm, Node f, Node c, int c_index) { RepSetIterator riter( d_qe, &(fm->d_rep_set) ); Trace("fmc-exh") << "----Exhaustive instantiate based on index " << c_index << " : " << c << " "; debugPrintCond("fmc-exh", c, true); Trace("fmc-exh")<< std::endl; - Trace("fmc-exh-debug") << "Set interval domains..." << std::endl; - //set the bounds on the iterator based on intervals - for( unsigned i=0; iisInterval(c[i]) ){ - Trace("fmc-exh-debug") << "...set " << i << " based on interval." << std::endl; - for( unsigned b=0; b<2; b++ ){ - if( !fm->isStar(c[i][b]) ){ - riter.d_bounds[b][i] = c[i][b]; - } - } - }else if( !fm->isStar(c[i]) ){ - Trace("fmc-exh-debug") << "...set " << i << " based on point." << std::endl; - riter.d_bounds[0][i] = c[i]; - riter.d_bounds[1][i] = QuantArith::offset( c[i], 1 ); - } - } - } + RepBoundFmcEntry rbfe; + rbfe.d_entry = c; + rbfe.d_fm = fm; Trace("fmc-exh-debug") << "Set quantifier..." << std::endl; //initialize - if( riter.setQuantifier( f ) ){ + if( riter.setQuantifier( f, &rbfe ) ){ 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]) ){ - //add the full range - }else{ - 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; - } - } - }else{ - Trace("fmc-exh") << "---- Does not have type : " << tn << std::endl; - return false; - } - } - } int addedLemmas = 0; //now do full iteration while( !riter.isFinished() ){ @@ -829,7 +810,7 @@ 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_INT_RANGE) { + if (index>=0 && riter.d_index[index]>0 && addedLemmas>0 && riter.d_enum_type[index]==RepSetIterator::ENUM_BOUND_INT ) { Trace("fmc-exh-debug") << "Since this is a range enumeration, skip to the next..." << std::endl; riter.increment2( index-1 ); } diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index c88430dbf..24d26e72f 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -50,7 +50,11 @@ void QuantDSplit::preRegisterQuantifier( Node q ) { if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ score = dt.isInterpretedFinite( tn.toType() ) ? 1 : 0; }else if( options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_DEFAULT ){ - score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1; + //only split if goes from being unhandled -> handled by finite instantiation + // an example is datatypes with uninterpreted sort fields, which are "interpreted finite" but not "finite" + if( !d_quantEngine->isFiniteBound( q, q[0][i] ) ){ + score = dt.isInterpretedFinite( tn.toType() ) ? 1 : -1; + } } Trace("quant-dsplit-debug") << "Datatype " << dt.getName() << " is score " << score << " (" << dt.isInterpretedFinite( tn.toType() ) << " " << dt.isFinite( tn.toType() ) << ")" << std::endl; if( score>max_score ){ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index a3b6293fb..2d79826a6 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -251,8 +251,7 @@ void QuantifiersEngine::finishInit(){ d_lte_part_inst = new quantifiers::LtePartialInst( this, c ); d_modules.push_back( d_lte_part_inst ); } - if( ( options::finiteModelFind() && options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ) || - options::quantDynamicSplit()==quantifiers::QUANT_DSPLIT_MODE_AGG ){ + if( options::quantDynamicSplit()!=quantifiers::QUANT_DSPLIT_MODE_NONE ){ d_qsplit = new quantifiers::QuantDSplit( this, c ); d_modules.push_back( d_qsplit ); } @@ -328,6 +327,20 @@ bool QuantifiersEngine::hasOwnership( Node q, QuantifiersModule * m ) { return mo==m || mo==NULL; } +bool QuantifiersEngine::isFiniteBound( Node q, Node v ) { + if( getBoundedIntegers() && getBoundedIntegers()->isBoundVar( q, v ) ){ + return true; + }else{ + TypeNode tn = v.getType(); + if( tn.isSort() && options::finiteModelFind() ){ + return true; + }else if( getTermDatabase()->mayComplete( tn ) ){ + return true; + } + } + return false; +} + void QuantifiersEngine::presolve() { Trace("quant-engine-proc") << "QuantifiersEngine : presolve " << std::endl; for( unsigned i=0; i=0); int v = d_var_order[i]; - if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){ - return d_domain[v].size(); - }else{ - return d_domain[v][0]; - } + return d_domain_elements[v].size(); } -bool RepSetIterator::setQuantifier( Node f ){ +bool RepSetIterator::setQuantifier( Node f, RepBoundExt* rext ){ Trace("rsi") << "Make rsi for " << f << std::endl; Assert( d_types.empty() ); //store indicies @@ -154,10 +150,10 @@ bool RepSetIterator::setQuantifier( Node f ){ d_types.push_back( f[0][i].getType() ); } d_owner = f; - return initialize(); + return initialize( rext ); } -bool RepSetIterator::setFunctionDomain( Node op ){ +bool RepSetIterator::setFunctionDomain( Node op, RepBoundExt* rext ){ Trace("rsi") << "Make rsi for " << op << std::endl; Assert( d_types.empty() ); TypeNode tn = op.getType(); @@ -165,10 +161,10 @@ bool RepSetIterator::setFunctionDomain( Node op ){ d_types.push_back( tn[i] ); } d_owner = op; - return initialize(); + return initialize( rext ); } -bool RepSetIterator::initialize(){ +bool RepSetIterator::initialize( RepBoundExt* rext ){ Trace("rsi") << "Initialize rep set iterator..." << std::endl; for( unsigned v=0; v() ); TypeNode tn = d_types[v]; Trace("rsi") << "Var #" << v << " is type " << tn << "..." << std::endl; if( tn.isSort() ){ @@ -191,27 +188,27 @@ bool RepSetIterator::initialize(){ Trace("mkVar") << "RepSetIterator:: Make variable " << var << " : " << tn << std::endl; d_rep_set->add( tn, var ); } - }else{ - bool inc = true; - //check if it is bound by bounded integer module - if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ + } + bool inc = true; + //check if it is externally bound + if( rext && rext->setBound( d_owner, v, tn, d_domain_elements[v] ) ){ + d_enum_type.push_back( ENUM_DEFAULT ); + inc = false; + //builtin: check if it is bound by bounded integer module + }else if( d_owner.getKind()==FORALL && d_qe && d_qe->getBoundedIntegers() ){ + if( d_qe->getBoundedIntegers()->isBoundVar( d_owner, d_owner[0][v] ) ){ 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_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 ); + if( bvt!=quantifiers::BoundedIntegers::BOUND_FINITE ){ + d_enum_type.push_back( ENUM_BOUND_INT ); inc = false; + }else{ + //will treat in default way } } + } + if( !tn.isSort() ){ if( inc ){ - //check if it is otherwise bound - 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_INT_RANGE ); - }else if( d_qe->getTermDatabase()->mayComplete( tn ) ){ + 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 @@ -223,12 +220,14 @@ bool RepSetIterator::initialize(){ } } } + //if we have yet to determine the type of enumeration if( d_enum_type.size()<=v ){ - d_enum_type.push_back( ENUM_DOMAIN_ELEMENTS ); if( d_rep_set->hasType( tn ) ){ + d_enum_type.push_back( ENUM_DEFAULT ); for( unsigned j=0; jd_type_reps[tn].size(); j++ ){ - d_domain[v].push_back( j ); + //d_domain[v].push_back( j ); + d_domain_elements[v].push_back( d_rep_set->d_type_reps[tn][j] ); } }else{ Assert( d_incomplete ); @@ -285,92 +284,13 @@ int RepSetIterator::resetIndex( int i, bool initial ) { d_index[i] = 0; int v = d_var_order[i]; Trace("bound-int-rsi") << "Reset " << i << ", var order = " << v << ", initial = " << initial << std::endl; - //determine the current range - 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() ){ - 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(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][v], l ); - } - 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 ); - } - } - } - - if( l.isNull() || u.isNull() ){ - //failed, abort the iterator - return -1; - }else{ - 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[v].clear(); - Node tl = l; - Node tu = u; - 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[v] = tl; - if( !actual_l.isNull() ){ - //if bound was limited externally, must consider the offset - d_lower_bounds[v] = Rewriter::rewrite( NodeManager::currentNM()->mkNode( PLUS, tl, actual_l ) ); - } - 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[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][v] << "." << std::endl; - return -1; - } - } - }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 ){ - while( srv.getKind()==UNION ){ - Assert( srv[1].getKind()==kind::SINGLETON ); - d_setm_bounds[v].push_back( srv[1][0] ); - srv = srv[0]; - } - Assert( srv.getKind()==kind::SINGLETON ); - 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; - } + if( d_enum_type[v]==ENUM_BOUND_INT ){ + Assert( d_owner.getKind()==FORALL ); + if( !d_qe->getBoundedIntegers()->getBoundElements( this, initial, d_owner, d_owner[0][v], d_domain_elements[v] ) ){ + return -1; } } - return 1; + return d_domain_elements[v].empty() ? 0 : 1; } int RepSetIterator::increment2( int i ){ @@ -436,24 +356,12 @@ bool RepSetIterator::isFinished(){ } Node RepSetIterator::getCurrentTerm( int v ){ - Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl; int ii = d_index_order[v]; int curr = d_index[ii]; - if( d_enum_type[v]==ENUM_DOMAIN_ELEMENTS ){ - TypeNode tn = d_types[v]; - Assert( d_rep_set->d_type_reps.find( tn )!=d_rep_set->d_type_reps.end() ); - Assert( 0<=d_domain[v][curr] && d_domain[v][curr]<(int)d_rep_set->d_type_reps[tn].size() ); - return d_rep_set->d_type_reps[tn][d_domain[v][curr]]; - }else if( d_enum_type[v]==ENUM_SET_MEMBERS ){ - Assert( 0<=curr && curr<(int)d_setm_bounds[v].size() ); - return d_setm_bounds[v][curr]; - }else{ - 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; - } + Trace("rsi-debug") << "rsi : get term " << v << ", index order = " << d_index_order[v] << std::endl; + Trace("rsi-debug") << "rsi : curr = " << curr << " / " << d_domain_elements[v].size() << std::endl; + Assert( 0<=curr && curr<(int)d_domain_elements[v].size() ); + return d_domain_elements[v][curr]; } void RepSetIterator::debugPrint( const char* c ){ diff --git a/src/theory/rep_set.h b/src/theory/rep_set.h index a56fba39b..2a2110cfa 100644 --- a/src/theory/rep_set.h +++ b/src/theory/rep_set.h @@ -56,18 +56,23 @@ public: //representative domain typedef std::vector< int > RepDomain; + +class RepBoundExt { +public: + virtual bool setBound( Node owner, int i, TypeNode tn, std::vector< Node >& elements ) = 0; +}; + /** this class iterates over a RepSet */ class RepSetIterator { public: enum { - ENUM_DOMAIN_ELEMENTS, - ENUM_INT_RANGE, - ENUM_SET_MEMBERS, + ENUM_DEFAULT, + ENUM_BOUND_INT, }; private: QuantifiersEngine * d_qe; //initialize function - bool initialize(); + bool initialize( RepBoundExt* rext = NULL ); //for int ranges std::map< int, Node > d_lower_bounds; //for set ranges @@ -101,9 +106,9 @@ public: RepSetIterator( QuantifiersEngine * qe, RepSet* rs ); ~RepSetIterator(){} //set that this iterator will be iterating over instantiations for a quantifier - bool setQuantifier( Node f ); + bool setQuantifier( Node f, RepBoundExt* rext = NULL ); //set that this iterator will be iterating over the domain of a function - bool setFunctionDomain( Node op ); + bool setFunctionDomain( Node op, RepBoundExt* rext = NULL ); public: //pointer to model RepSet* d_rep_set; @@ -114,9 +119,7 @@ public: //types we are considering std::vector< TypeNode > d_types; //domain we are considering - std::vector< RepDomain > d_domain; - //intervals - std::map< int, Node > d_bounds[2]; + std::vector< std::vector< Node > > d_domain_elements; public: /** increment the iterator at index=counter */ int increment2( int i ); -- cgit v1.2.3