diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/quantifiers/candidate_generator.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/model_builder.cpp | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/options | 2 | ||||
-rwxr-xr-x | src/theory/quantifiers/quant_conflict_find.cpp | 5 | ||||
-rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 3 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 29 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.h | 11 | ||||
-rw-r--r-- | src/theory/quantifiers_engine.cpp | 2 |
8 files changed, 42 insertions, 14 deletions
diff --git a/src/theory/quantifiers/candidate_generator.cpp b/src/theory/quantifiers/candidate_generator.cpp index 1b34bc118..9b5e506ea 100644 --- a/src/theory/quantifiers/candidate_generator.cpp +++ b/src/theory/quantifiers/candidate_generator.cpp @@ -63,7 +63,7 @@ CandidateGeneratorQE::CandidateGeneratorQE( QuantifiersEngine* qe, Node op ) : Assert( !d_op.isNull() ); } void CandidateGeneratorQE::resetInstantiationRound(){ - d_term_iter_limit = d_qe->getTermDatabase()->d_op_map[d_op].size(); + d_term_iter_limit = d_qe->getTermDatabase()->getNumGroundTerms( d_op ); } void CandidateGeneratorQE::reset( Node eqc ){ diff --git a/src/theory/quantifiers/model_builder.cpp b/src/theory/quantifiers/model_builder.cpp index 50a0084fc..a12fc7ca2 100644 --- a/src/theory/quantifiers/model_builder.cpp +++ b/src/theory/quantifiers/model_builder.cpp @@ -1039,7 +1039,7 @@ int QModelBuilderInstGen::getSelectionFormulaScore( Node fn ){ if( fn.getKind()==APPLY_UF ){ Node op = fn.getOperator(); //return total number of terms - return d_qe->getTermDatabase()->d_op_count[op]; + return d_qe->getTermDatabase()->d_op_nonred_count[op]; }else{ int score = 0; for( size_t i=0; i<fn.getNumChildren(); i++ ){ diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options index 7ee416c4e..0865f2c0b 100644 --- a/src/theory/quantifiers/options +++ b/src/theory/quantifiers/options @@ -125,7 +125,7 @@ option qcfMode --quant-cf-mode=MODE CVC4::theory::quantifiers::QcfMode :default option qcfWhenMode --quant-cf-when=MODE CVC4::theory::quantifiers::QcfWhenMode :default CVC4::theory::quantifiers::QCF_WHEN_MODE_DEFAULT :include "theory/quantifiers/modes.h" :handler CVC4::theory::quantifiers::stringToQcfWhenMode :handler-include "theory/quantifiers/options_handlers.h" when to invoke conflict find mechanism for quantifiers -option quantRewriteRules --rewrite-rules bool :default false +option quantRewriteRules --rewrite-rules bool :default true use rewrite rules module option rrOneInstPerRound --rr-one-inst-per-round bool :default false add one instance of rewrite rule per round diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 51d69ace4..c0b318f23 100755 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -2194,11 +2194,10 @@ void QuantConflictFind::computeArgReps( TNode n ) { void QuantConflictFind::computeUfTerms( TNode f ) {
if( d_uf_terms.find( f )==d_uf_terms.end() ){
d_uf_terms[f].clear();
- unsigned nt = d_quantEngine->getTermDatabase()->d_op_map[f].size();
+ unsigned nt = d_quantEngine->getTermDatabase()->getNumGroundTerms( f );
for( unsigned i=0; i<nt; i++ ){
Node n = d_quantEngine->getTermDatabase()->d_op_map[f][i];
- if( !n.getAttribute(NoMatchAttribute()) ){
- Assert( getEqualityEngine()->hasTerm( n ) );
+ if( getEqualityEngine()->hasTerm( n ) && !n.getAttribute(NoMatchAttribute()) ){
Node r = getRepresentative( n );
computeArgReps( n );
d_eqc_uf_terms[f].d_children[r].addTerm( n, d_arg_reps[n] );
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 20ab4e55f..914141995 100644 --- a/src/theory/quantifiers/relevant_domain.cpp +++ b/src/theory/quantifiers/relevant_domain.cpp @@ -111,7 +111,8 @@ void RelevantDomain::compute(){ TermDb * db = d_qe->getTermDatabase(); for( std::map< Node, std::vector< Node > >::iterator it = db->d_op_map.begin(); it != db->d_op_map.end(); ++it ){ Node op = it->first; - for( unsigned i=0; i<it->second.size(); i++ ){ + unsigned sz = db->getNumGroundTerms( op ); + for( unsigned i=0; i<sz; i++ ){ Node n = it->second[i]; //if it is a non-redundant term if( !n.getAttribute(NoMatchAttribute()) ){ diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 08a9f5d9f..ea1231e7a 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -46,6 +46,20 @@ bool TermArgTrie::addTerm2( QuantifiersEngine* qe, Node n, int argIndex ){ } } +TermDb::TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ) : d_quantEngine( qe ), d_op_ccount( u ) { + +} + +/** ground terms */ +unsigned TermDb::getNumGroundTerms( Node f ) { + std::map< Node, std::vector< Node > >::iterator it = d_op_map.find( f ); + if( it!=d_op_map.end() ){ + return it->second.size(); + }else{ + return 0; + } + //return d_op_ccount[f]; +} Node TermDb::getOperator( Node n ) { //return n.getOperator(); @@ -89,6 +103,15 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ Trace("term-db") << "register term in db " << n << std::endl; //std::cout << "register trigger term " << n << std::endl; Node op = getOperator( n ); + /* + int occ = d_op_ccount[op]; + if( occ<(int)d_op_map[op].size() ){ + d_op_map[op][occ] = n; + }else{ + d_op_map[op].push_back( n ); + } + d_op_ccount[op].set( occ + 1 ); + */ d_op_map[op].push_back( n ); added.insert( n ); @@ -120,7 +143,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ int alreadyCongruentCount = 0; //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_count[ it->first ] = 0; + d_op_nonred_count[ it->first ] = 0; if( !it->second.empty() ){ if( it->second[0].getType().isBoolean() ){ d_pred_map_trie[ 0 ][ it->first ].d_data.clear(); @@ -138,7 +161,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; - d_op_count[ it->first ]++; + d_op_nonred_count[ it->first ]++; } }else{ congruentCount++; @@ -166,7 +189,7 @@ void TermDb::addTerm( Node n, std::set< Node >& added, bool withinQuant ){ congruentCount++; }else{ nonCongruentCount++; - d_op_count[ op ]++; + d_op_nonred_count[ op ]++; } }else{ alreadyCongruentCount++; diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index b3db6d266..41108bc2a 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -88,6 +88,7 @@ class TermDb { friend class ::CVC4::theory::inst::Trigger; friend class ::CVC4::theory::rrinst::Trigger; friend class ::CVC4::theory::quantifiers::fmcheck::FullModelChecker; + typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; private: /** reference to the quantifiers engine */ QuantifiersEngine* d_quantEngine; @@ -96,13 +97,17 @@ private: private: /** select op map */ std::map< Node, std::map< TypeNode, std::map< TypeNode, Node > > > d_par_op_map; + /** count number of ground terms per operator (user-context dependent) */ + NodeIntMap d_op_ccount; public: - TermDb( QuantifiersEngine* qe ) : d_quantEngine( qe ){} + TermDb( context::Context* c, context::UserContext* u, QuantifiersEngine* qe ); ~TermDb(){} + /** ground terms */ + unsigned getNumGroundTerms( Node f ); + /** count number of non-redundant ground terms per operator */ + std::map< Node, int > d_op_nonred_count; /** map from APPLY_UF operators to ground terms for that operator */ std::map< Node, std::vector< Node > > d_op_map; - /** count number of APPLY_UF terms per operator */ - std::map< Node, int > d_op_count; /** map from APPLY_UF functions to trie */ std::map< Node, TermArgTrie > d_func_map_trie; /** map from APPLY_UF predicates to trie */ diff --git a/src/theory/quantifiers_engine.cpp b/src/theory/quantifiers_engine.cpp index 02423e54d..7fa61477f 100644 --- a/src/theory/quantifiers_engine.cpp +++ b/src/theory/quantifiers_engine.cpp @@ -45,7 +45,7 @@ QuantifiersEngine::QuantifiersEngine(context::Context* c, context::UserContext* d_te( te ), d_lemmas_produced_c(u){ d_eq_query = new EqualityQueryQuantifiersEngine( this ); - d_term_db = new quantifiers::TermDb( this ); + d_term_db = new quantifiers::TermDb( c, u, this ); d_tr_trie = new inst::TriggerTrie; //d_rr_tr_trie = new rrinst::TriggerTrie; //d_eem = new EfficientEMatcher( this ); |