diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 10:43:57 +0100 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2014-11-13 10:44:11 +0100 |
commit | 0e761324a33a993ae9a268bc2d2ed46f7e86b42d (patch) | |
tree | d27052ba5aa4520436d8cb6ce059229f2df76ec2 /src/theory | |
parent | 270a5577f9a34c92ee991bff1d047d78a8f6d5ab (diff) |
More preparation for filtering relevant terms in TermDb.
Diffstat (limited to 'src/theory')
-rwxr-xr-x | src/theory/quantifiers/conjecture_generator.cpp | 8 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 44 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 46 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 2 |
4 files changed, 73 insertions, 27 deletions
diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 871d4ddc6..06552196d 100755 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -416,8 +416,10 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { eq::EqClassIterator ieqc_i = eq::EqClassIterator( r, ee );
while( !ieqc_i.isFinished() ){
TNode n = (*ieqc_i);
- if( isHandledTerm( n ) ){
- d_op_arg_index[r].addTerm( this, n );
+ if( getTermDatabase()->hasTermCurrent( n ) ){
+ if( isHandledTerm( n ) ){
+ d_op_arg_index[r].addTerm( this, n );
+ }
}
++ieqc_i;
}
@@ -472,7 +474,7 @@ void ConjectureGenerator::check( Theory::Effort e, unsigned quant_e ) { eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee );
while( !eqc_i.isFinished() ){
TNode n = (*eqc_i);
- if( !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){
+ if( getTermDatabase()->hasTermCurrent( n ) && !n.getAttribute(NoMatchAttribute()) && ( n.getKind()!=EQUAL || isFalse ) ){
if( firstTime ){
Trace("sg-gen-eqc") << "e" << d_em[r] << " : { " << std::endl;
firstTime = false;
diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 768ba63de..d465df4c0 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -458,8 +458,8 @@ bool QuantInfo::isTConstraintSpurious( QuantConflictFind * p, std::vector< Node //check constraints
for( std::map< Node, bool >::iterator it = d_tconstraints.begin(); it != d_tconstraints.end(); ++it ){
//apply substitution to the tconstraint
- Node cons = it->first.substitute( p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].begin(),
- p->getQuantifiersEngine()->getTermDatabase()->d_vars[d_q].end(),
+ Node cons = it->first.substitute( p->getTermDatabase()->d_vars[d_q].begin(),
+ p->getTermDatabase()->d_vars[d_q].end(),
terms.begin(), terms.end() );
cons = it->second ? cons : cons.negate();
if( !entailmentTest( p, cons, p->d_effort==QuantConflictFind::effort_conflict ) ){
@@ -1300,7 +1300,7 @@ bool MatchGen::getNextMatch( QuantConflictFind * p, QuantInfo * qi ) { if( d_type==typ_var && p->d_effort==QuantConflictFind::effort_mc && !d_matched_basis ){
d_matched_basis = true;
Node f = getOperator( d_n );
- TNode mbo = p->getQuantifiersEngine()->getTermDatabase()->getModelBasisOpTerm( f );
+ TNode mbo = p->getTermDatabase()->getModelBasisOpTerm( f );
if( qi->setMatch( p, d_qni_var_num[0], mbo ) ){
success = true;
d_qni_bound[0] = d_qni_var_num[0];
@@ -1662,7 +1662,7 @@ bool MatchGen::isHandledUfTerm( TNode n ) { Node MatchGen::getOperator( QuantConflictFind * p, Node n ) {
if( isHandledUfTerm( n ) ){
- return p->getQuantifiersEngine()->getTermDatabase()->getOperator( n );
+ return p->getTermDatabase()->getOperator( n );
}else{
return Node::null();
}
@@ -2087,26 +2087,28 @@ void QuantConflictFind::computeRelevantEqr() { while( !eqcs_i.isFinished() ){
//nEqc++;
Node r = (*eqcs_i);
- TypeNode rtn = r.getType();
- if( options::qcfMode()==QCF_MC ){
- std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
- if( itt==d_eqcs.end() ){
- Node mb = getQuantifiersEngine()->getTermDatabase()->getModelBasisTerm( rtn );
- if( !getEqualityEngine()->hasTerm( mb ) ){
- Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
- Assert( false );
- }
- Node mbr = getRepresentative( mb );
- if( mbr!=r ){
- d_eqcs[rtn].push_back( mbr );
+ if( getTermDatabase()->hasTermCurrent( r ) ){
+ TypeNode rtn = r.getType();
+ if( options::qcfMode()==QCF_MC ){
+ std::map< TypeNode, std::vector< TNode > >::iterator itt = d_eqcs.find( rtn );
+ if( itt==d_eqcs.end() ){
+ Node mb = getTermDatabase()->getModelBasisTerm( rtn );
+ if( !getEqualityEngine()->hasTerm( mb ) ){
+ Trace("qcf-warn") << "WARNING: Model basis term does not exist!" << std::endl;
+ Assert( false );
+ }
+ Node mbr = getRepresentative( mb );
+ if( mbr!=r ){
+ d_eqcs[rtn].push_back( mbr );
+ }
+ d_eqcs[rtn].push_back( r );
+ d_model_basis[rtn] = mb;
+ }else{
+ itt->second.push_back( r );
}
- d_eqcs[rtn].push_back( r );
- d_model_basis[rtn] = mb;
}else{
- itt->second.push_back( r );
+ d_eqcs[rtn].push_back( r );
}
- }else{
- d_eqcs[rtn].push_back( r );
}
++eqcs_i;
}
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index ee39b55d9..b21494f77 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -322,6 +322,21 @@ bool TermDb::hasTermCurrent( Node n ) { return true; } +void TermDb::setHasTerm( Node n ) { + if( inst::Trigger::isAtomicTrigger( n ) ){ + if( d_has_map.find( n )==d_has_map.end() ){ + d_has_map[n] = true; + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + setHasTerm( n[i] ); + } + } + }else{ + for( unsigned i=0; i<n.getNumChildren(); i++ ){ + setHasTerm( n[i] ); + } + } +} + void TermDb::reset( Theory::Effort effort ){ int nonCongruentCount = 0; int congruentCount = 0; @@ -331,21 +346,45 @@ void TermDb::reset( Theory::Effort effort ){ d_arg_reps.clear(); d_func_map_trie.clear(); d_func_map_eqc_trie.clear(); - /* + //compute has map + /* d_has_map.clear(); eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); while( !eqcs_i.isFinished() ){ TNode r = (*eqcs_i); + bool addedFirst = false; + Node first; eq::EqClassIterator eqc_i = eq::EqClassIterator( r, ee ); while( !eqc_i.isFinished() ){ - d_has_map[(*eqc_i)] = true; + TNode n = (*eqc_i); + if( first.isNull() ){ + first = n; + }else{ + if( !addedFirst ){ + addedFirst = true; + setHasTerm( first ); + } + setHasTerm( n ); + } ++eqc_i; } ++eqcs_i; } + for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) { + Theory* theory = d_quantEngine->getTheoryEngine()->d_theoryTable[theoryId]; + if (theory && d_quantEngine->getTheoryEngine()->d_logicInfo.isTheoryEnabled(theoryId)) { + context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end(); + for (unsigned i = 0; it != it_end; ++ it, ++i) { + Trace("ajr-temp") << "Set has term " << (*it).assertion << std::endl; + setHasTerm( (*it).assertion ); + } + } + } */ + + //rebuild d_func/pred_map_trie for each operation, this will calculate all congruent terms for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ d_op_nonred_count[ it->first ] = 0; @@ -370,6 +409,7 @@ void TermDb::reset( Theory::Effort effort ){ alreadyCongruentCount++; } }else{ + Trace("term-db-stats-debug") << n << " is not relevant." << std::endl; nonRelevantCount++; } } @@ -377,7 +417,7 @@ void TermDb::reset( Theory::Effort effort ){ } Trace("term-db-stats") << "TermDb: Reset" << std::endl; Trace("term-db-stats") << "Congruent/Non-Congruent/Non-Relevant = "; - Trace("term-db-stats") << congruentCount << "(" << alreadyCongruentCount << ") / " << nonCongruentCount << " / " << nonRelevantCount << std::endl; + Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; if( Debug.isOn("term-db") ){ Debug("term-db") << "functions : " << std::endl; for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 3d419ed5c..4dca6b36c 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -128,6 +128,8 @@ private: std::map< Node, std::map< TypeNode, Node > > d_par_op_map; /** count number of ground terms per operator (user-context dependent) */ NodeIntMap d_op_ccount; + /** set has term */ + void setHasTerm( Node n ); public: TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} |