From 0e761324a33a993ae9a268bc2d2ed46f7e86b42d Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 13 Nov 2014 10:43:57 +0100 Subject: [PATCH] More preparation for filtering relevant terms in TermDb. --- .../quantifiers/conjecture_generator.cpp | 8 ++-- .../quantifiers/quant_conflict_find.cpp | 44 +++++++++--------- src/theory/quantifiers/term_database.cpp | 46 +++++++++++++++++-- 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; igetMasterEqualityEngine(); 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::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(){} -- 2.30.2