diff options
Diffstat (limited to 'src/theory/quantifiers/term_database.cpp')
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 37 |
1 files changed, 24 insertions, 13 deletions
diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 69271e021..fb28974a9 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -322,15 +322,19 @@ bool TermDb::isEntailed( TNode n, std::map< TNode, TNode >& subs, bool subsRep, return false; } -bool TermDb::hasTermCurrent( Node n ) { - //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE - if( options::termDbMode()==TERM_DB_ALL ){ - return true; - }else if( options::termDbMode()==TERM_DB_RELEVANT ){ +bool TermDb::hasTermCurrent( Node n, bool useMode ) { + if( !useMode ){ return d_has_map.find( n )!=d_has_map.end(); }else{ - Assert( false ); - return false; + //return d_quantEngine->getMasterEqualityEngine()->hasTerm( n ); //some assertions are not sent to EE + if( options::termDbMode()==TERM_DB_ALL ){ + return true; + }else if( options::termDbMode()==TERM_DB_RELEVANT ){ + return d_has_map.find( n )!=d_has_map.end(); + }else{ + Assert( false ); + return false; + } } } @@ -364,7 +368,12 @@ Node TermDb::getHasTermEqc( Node r ) { } } +bool TermDb::isInstClosure( Node r ) { + return d_iclosure_processed.find( r )!=d_iclosure_processed.end(); +} + void TermDb::setHasTerm( Node n ) { + Trace("term-db-debug2") << "hasTerm : " << n << std::endl; //if( inst::Trigger::isAtomicTrigger( n ) ){ if( d_has_map.find( n )==d_has_map.end() ){ d_has_map[n] = true; @@ -391,9 +400,9 @@ void TermDb::reset( Theory::Effort effort ){ d_func_map_trie.clear(); d_func_map_eqc_trie.clear(); - eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); + eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); //compute has map - if( options::termDbMode()==TERM_DB_RELEVANT ){ + if( options::termDbMode()==TERM_DB_RELEVANT || options::lteRestrictInstClosure() ){ d_has_map.clear(); d_has_eqc.clear(); eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( ee ); @@ -423,7 +432,9 @@ void TermDb::reset( Theory::Effort effort ){ 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) { - setHasTerm( (*it).assertion ); + if( (*it).assertion.getKind()!=INST_CLOSURE ){ + setHasTerm( (*it).assertion ); + } } } } @@ -443,7 +454,7 @@ void TermDb::reset( Theory::Effort effort ){ computeModelBasisArgAttribute( n ); } computeArgReps( n ); - + if( Trace.isOn("term-db-debug") ){ Trace("term-db-debug") << "Adding term " << n << " with arg reps : "; for( unsigned i=0; i<d_arg_reps[n].size(); i++ ){ @@ -451,7 +462,7 @@ void TermDb::reset( Theory::Effort effort ){ } Trace("term-db-debug") << std::endl; } - + if( !d_func_map_trie[ it->first ].addTerm( n, d_arg_reps[n] ) ){ NoMatchAttribute nma; n.setAttribute(nma,true); @@ -1157,7 +1168,7 @@ void TermDb::computeAttributes( Node q ) { //not necessarily nested existential //Assert( q[1].getKind()==NOT ); //Assert( q[1][0].getKind()==FORALL ); - + Trace("quant-attr") << "Attribute : sygus : " << q << std::endl; d_qattr_sygus[q] = true; if( d_quantEngine->getCegInstantiation()==NULL ){ |