From a2bba0806dab0e0d4728bbba8e4e6b4160335eeb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 27 Nov 2018 15:39:13 -0600 Subject: Make (T)NodeTrie a general utility (#2489) This moves quantifiers::TermArgTrie in src/theory/quantifiers/term_database to (T)NodeTrie in src/expr, and cleans up all references to it. --- .../quantifiers/cegqi/ceg_epr_instantiator.cpp | 10 +-- .../quantifiers/cegqi/ceg_epr_instantiator.h | 5 +- src/theory/quantifiers/conjecture_generator.cpp | 2 +- src/theory/quantifiers/conjecture_generator.h | 7 +- .../quantifiers/ematching/candidate_generator.cpp | 2 +- .../quantifiers/ematching/inst_match_generator.cpp | 23 ++++--- .../quantifiers/ematching/inst_match_generator.h | 6 +- src/theory/quantifiers/inst_propagator.h | 28 ++++---- src/theory/quantifiers/local_theory_ext.cpp | 30 +++++++-- src/theory/quantifiers/local_theory_ext.h | 18 +++-- src/theory/quantifiers/quant_conflict_find.cpp | 8 ++- src/theory/quantifiers/quant_conflict_find.h | 6 +- src/theory/quantifiers/term_database.cpp | 58 +++------------- src/theory/quantifiers/term_database.h | 78 +++------------------- 14 files changed, 104 insertions(+), 177 deletions(-) (limited to 'src/theory/quantifiers') diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp index 3535b57b7..df6690273 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.cpp @@ -107,14 +107,14 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci, Node pv, Node catom, std::vector& arg_reps, - TermArgTrie* tat, + TNodeTrie* tat, unsigned index, std::map& match_score) { if (index == catom.getNumChildren()) { - Assert(tat->hasNodeData()); - Node gcatom = tat->getNodeData(); + Assert(tat->hasData()); + Node gcatom = tat->getData(); Trace("cegqi-epr") << "Matched : " << catom << " and " << gcatom << std::endl; for (unsigned i = 0, nchild = catom.getNumChildren(); i < nchild; i++) @@ -132,7 +132,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci, } return; } - std::map::iterator it = tat->d_data.find(arg_reps[index]); + std::map::iterator it = tat->d_data.find(arg_reps[index]); if (it != tat->d_data.end()) { computeMatchScore( @@ -165,7 +165,7 @@ void EprInstantiator::computeMatchScore(CegInstantiator* ci, TermDb* tdb = ci->getQuantifiersEngine()->getTermDatabase(); Node rep = ee->getRepresentative(eqc); Node op = tdb->getMatchOperator(catom); - TermArgTrie* tat = tdb->getTermArgTrie(rep, op); + TNodeTrie* tat = tdb->getTermArgTrie(rep, op); Trace("cegqi-epr") << "EPR instantiation match term : " << catom << ", check ground terms=" << (tat != NULL) << std::endl; if (tat) diff --git a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h index b4378e1d2..f5057ad86 100644 --- a/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h +++ b/src/theory/quantifiers/cegqi/ceg_epr_instantiator.h @@ -19,14 +19,13 @@ #include #include +#include "expr/node_trie.h" #include "theory/quantifiers/cegqi/ceg_instantiator.h" namespace CVC4 { namespace theory { namespace quantifiers { -class TermArgTrie; - /** Effectively Propositional (EPR) Instantiator * * This implements a selection function for the EPR fragment. @@ -93,7 +92,7 @@ class EprInstantiator : public Instantiator Node pv, Node catom, std::vector& arg_reps, - TermArgTrie* tat, + TNodeTrie* tat, unsigned index, std::map& match_score); void computeMatchScore(CegInstantiator* ci, diff --git a/src/theory/quantifiers/conjecture_generator.cpp b/src/theory/quantifiers/conjecture_generator.cpp index 1d2f9a322..7408678e7 100644 --- a/src/theory/quantifiers/conjecture_generator.cpp +++ b/src/theory/quantifiers/conjecture_generator.cpp @@ -1630,7 +1630,7 @@ bool TermGenerator::getNextMatch( TermGenEnv * s, TNode eqc, std::map< TypeNode, //initial binding TNode f = s->getTgFunc( d_typ, d_status_num ); Assert( !eqc.isNull() ); - TermArgTrie * tat = s->getTermDatabase()->getTermArgTrie( eqc, f ); + TNodeTrie* tat = s->getTermDatabase()->getTermArgTrie(eqc, f); if( tat ){ d_match_children.push_back( tat->d_data.begin() ); d_match_children_end.push_back( tat->d_data.end() ); diff --git a/src/theory/quantifiers/conjecture_generator.h b/src/theory/quantifiers/conjecture_generator.h index 450bd7991..8fff7eafe 100644 --- a/src/theory/quantifiers/conjecture_generator.h +++ b/src/theory/quantifiers/conjecture_generator.h @@ -18,6 +18,7 @@ #define CONJECTURE_GENERATOR_H #include "context/cdhashmap.h" +#include "expr/node_trie.h" #include "theory/quantifiers_engine.h" #include "theory/type_enumerator.h" @@ -25,8 +26,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -class TermArgTrie; - //algorithm for computing candidate subgoals class ConjectureGenerator; @@ -105,8 +104,8 @@ class TermGenerator //2 : variables must map to non-ground terms unsigned d_match_mode; //children - std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children; - std::vector< std::map< TNode, TermArgTrie >::iterator > d_match_children_end; + std::vector::iterator> d_match_children; + std::vector::iterator> d_match_children_end; void reset( TermGenEnv * s, TypeNode tn ); bool getNextTerm( TermGenEnv * s, unsigned depth ); diff --git a/src/theory/quantifiers/ematching/candidate_generator.cpp b/src/theory/quantifiers/ematching/candidate_generator.cpp index 3f404c17f..612a1938a 100644 --- a/src/theory/quantifiers/ematching/candidate_generator.cpp +++ b/src/theory/quantifiers/ematching/candidate_generator.cpp @@ -57,7 +57,7 @@ void CandidateGeneratorQE::reset( Node eqc ){ }else{ eq::EqualityEngine* ee = d_qe->getEqualityQuery()->getEngine(); if( ee->hasTerm( eqc ) ){ - quantifiers::TermArgTrie * tat = d_qe->getTermDatabase()->getTermArgTrie( eqc, d_op ); + TNodeTrie* tat = d_qe->getTermDatabase()->getTermArgTrie(eqc, d_op); if( tat ){ //create an equivalence class iterator in eq class eqc Node rep = ee->getRepresentative( eqc ); diff --git a/src/theory/quantifiers/ematching/inst_match_generator.cpp b/src/theory/quantifiers/ematching/inst_match_generator.cpp index 646208ec6..f26df5b79 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.cpp +++ b/src/theory/quantifiers/ematching/inst_match_generator.cpp @@ -1028,7 +1028,7 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, Trigger* tparent) { int addedLemmas = 0; - quantifiers::TermArgTrie* tat; + TNodeTrie* tat; if( d_eqc.isNull() ){ tat = qe->getTermDatabase()->getTermArgTrie( d_op ); }else{ @@ -1040,10 +1040,12 @@ int InstMatchGeneratorSimple::addInstantiations(Node q, if (tat && !qe->inConflict()) { Node r = qe->getEqualityQuery()->getRepresentative(d_eqc); - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - if( it->first!=r ){ + for (std::pair& t : tat->d_data) + { + if (t.first != r) + { InstMatch m( q ); - addInstantiations( m, qe, addedLemmas, 0, &(it->second) ); + addInstantiations(m, qe, addedLemmas, 0, &(t.second)); if( qe->inConflict() ){ break; } @@ -1066,13 +1068,13 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, QuantifiersEngine* qe, int& addedLemmas, unsigned argIndex, - quantifiers::TermArgTrie* tat) + TNodeTrie* tat) { Debug("simple-trigger-debug") << "Add inst " << argIndex << " " << d_match_pattern << std::endl; if (argIndex == d_match_pattern.getNumChildren()) { Assert( !tat->d_data.empty() ); - TNode t = tat->getNodeData(); + TNode t = tat->getData(); Debug("simple-trigger") << "Actual term is " << t << std::endl; //convert to actual used terms for (std::map::iterator it = d_var_num.begin(); @@ -1096,14 +1098,15 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, if( d_match_pattern[argIndex].getKind()==INST_CONSTANT ){ int v = d_var_num[argIndex]; if( v!=-1 ){ - for( std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.begin(); it != tat->d_data.end(); ++it ){ - Node t = it->first; + for (std::pair& tt : tat->d_data) + { + Node t = tt.first; Node prev = m.get( v ); //using representatives, just check if equal Assert( t.getType().isComparableTo( d_match_pattern_arg_types[argIndex] ) ); if( prev.isNull() || prev==t ){ m.setValue( v, t); - addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); + addInstantiations(m, qe, addedLemmas, argIndex + 1, &(tt.second)); m.setValue( v, prev); if( qe->inConflict() ){ break; @@ -1115,7 +1118,7 @@ void InstMatchGeneratorSimple::addInstantiations(InstMatch& m, //inst constant from another quantified formula, treat as ground term TODO: remove this? } Node r = qe->getEqualityQuery()->getRepresentative( d_match_pattern[argIndex] ); - std::map< TNode, quantifiers::TermArgTrie >::iterator it = tat->d_data.find( r ); + std::map::iterator it = tat->d_data.find(r); if( it!=tat->d_data.end() ){ addInstantiations( m, qe, addedLemmas, argIndex+1, &(it->second) ); } diff --git a/src/theory/quantifiers/ematching/inst_match_generator.h b/src/theory/quantifiers/ematching/inst_match_generator.h index abf269f3e..83d4ce82e 100644 --- a/src/theory/quantifiers/ematching/inst_match_generator.h +++ b/src/theory/quantifiers/ematching/inst_match_generator.h @@ -18,15 +18,13 @@ #define __CVC4__THEORY__QUANTIFIERS__INST_MATCH_GENERATOR_H #include +#include "expr/node_trie.h" #include "theory/quantifiers/inst_match_trie.h" namespace CVC4 { namespace theory { class QuantifiersEngine; -namespace quantifiers{ - class TermArgTrie; -} namespace inst { @@ -662,7 +660,7 @@ class InstMatchGeneratorSimple : public IMGenerator { QuantifiersEngine* qe, int& addedLemmas, unsigned argIndex, - quantifiers::TermArgTrie* tat); + TNodeTrie* tat); };/* class InstMatchGeneratorSimple */ } } diff --git a/src/theory/quantifiers/inst_propagator.h b/src/theory/quantifiers/inst_propagator.h index dc1bf6908..1ba359228 100644 --- a/src/theory/quantifiers/inst_propagator.h +++ b/src/theory/quantifiers/inst_propagator.h @@ -22,9 +22,9 @@ #include #include #include "expr/node.h" +#include "expr/node_trie.h" #include "expr/type_node.h" #include "theory/quantifiers/instantiate.h" -#include "theory/quantifiers/term_database.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -72,17 +72,21 @@ public: TNode getCongruentTermExp( Node f, std::vector< TNode >& args, std::vector< Node >& exp ); private: /** term index */ - std::map< Node, TermArgTrie > d_uf_func_map_trie; - /** union find for terms beyond what is stored in equality engine */ - std::map< Node, Node > d_uf; - std::map< Node, std::vector< Node > > d_uf_exp; - Node getUfRepresentative( Node a, std::vector< Node >& exp ); - /** disequality list, stores explanations */ - std::map< Node, std::map< Node, std::vector< Node > > > d_diseq_list; - /** add arg */ - void addArgument( Node n, std::vector< Node >& args, std::vector< Node >& watch, bool is_watch ); - /** register term */ - void registerUfTerm( TNode n ); + std::map d_uf_func_map_trie; + /** union find for terms beyond what is stored in equality engine */ + std::map d_uf; + std::map > d_uf_exp; + Node getUfRepresentative(Node a, std::vector& exp); + /** disequality list, stores explanations */ + std::map > > d_diseq_list; + /** add arg */ + void addArgument(Node n, + std::vector& args, + std::vector& watch, + bool is_watch); + /** register term */ + void registerUfTerm(TNode n); + public: enum { STATUS_CONFLICT, diff --git a/src/theory/quantifiers/local_theory_ext.cpp b/src/theory/quantifiers/local_theory_ext.cpp index 93b220ea9..752d61489 100644 --- a/src/theory/quantifiers/local_theory_ext.cpp +++ b/src/theory/quantifiers/local_theory_ext.cpp @@ -196,9 +196,17 @@ void LtePartialInst::getInstantiations( std::vector< Node >& lemmas ) { } } -void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& terms, std::vector< TypeNode >& types, TermArgTrie * curr, - unsigned pindex, unsigned paindex, unsigned iindex ){ +void LtePartialInst::getPartialInstantiations(std::vector& conj, + Node q, + Node bvl, + std::vector& vars, + std::vector& terms, + std::vector& types, + TNodeTrie* curr, + unsigned pindex, + unsigned paindex, + unsigned iindex) +{ if( iindex==vars.size() ){ Node body = q[1].substitute( vars.begin(), vars.end(), terms.begin(), terms.end() ); if( bvl.isNull() ){ @@ -231,9 +239,19 @@ void LtePartialInst::getPartialInstantiations( std::vector< Node >& conj, Node q //start traversing term index for the operator curr = d_quantEngine->getTermDatabase()->getTermArgTrie( pat.getOperator() ); } - for( std::map< TNode, TermArgTrie >::iterator it = curr->d_data.begin(); it != curr->d_data.end(); ++it ){ - terms[d_pat_var_order[q][iindex]] = it->first; - getPartialInstantiations( conj, q, bvl, vars, terms, types, &it->second, pindex, paindex+1, iindex+1 ); + for (std::pair& t : curr->d_data) + { + terms[d_pat_var_order[q][iindex]] = t.first; + getPartialInstantiations(conj, + q, + bvl, + vars, + terms, + types, + &t.second, + pindex, + paindex + 1, + iindex + 1); } } }else{ diff --git a/src/theory/quantifiers/local_theory_ext.h b/src/theory/quantifiers/local_theory_ext.h index 63e810645..b8b0e34fa 100644 --- a/src/theory/quantifiers/local_theory_ext.h +++ b/src/theory/quantifiers/local_theory_ext.h @@ -17,15 +17,14 @@ #ifndef __CVC4__THEORY__LOCAL_THEORY_EXT_H #define __CVC4__THEORY__LOCAL_THEORY_EXT_H -#include "theory/quantifiers_engine.h" #include "context/cdo.h" +#include "expr/node_trie.h" +#include "theory/quantifiers_engine.h" namespace CVC4 { namespace theory { namespace quantifiers { -class TermArgTrie; - class LtePartialInst : public QuantifiersModule { private: // was this module invoked @@ -46,9 +45,16 @@ private: void reset(); /** get instantiations */ void getInstantiations( std::vector< Node >& lemmas ); - void getPartialInstantiations( std::vector< Node >& conj, Node q, Node bvl, - std::vector< Node >& vars, std::vector< Node >& inst, std::vector< TypeNode >& types, TermArgTrie * curr, - unsigned pindex, unsigned paindex, unsigned iindex ); + void getPartialInstantiations(std::vector& conj, + Node q, + Node bvl, + std::vector& vars, + std::vector& inst, + std::vector& types, + TNodeTrie* curr, + unsigned pindex, + unsigned paindex, + unsigned iindex); /** get eligible inst variables */ void getEligibleInstVars( Node n, std::map< Node, bool >& vars ); diff --git a/src/theory/quantifiers/quant_conflict_find.cpp b/src/theory/quantifiers/quant_conflict_find.cpp index 95ec24df9..5b57af14c 100644 --- a/src/theory/quantifiers/quant_conflict_find.cpp +++ b/src/theory/quantifiers/quant_conflict_find.cpp @@ -1293,7 +1293,7 @@ void MatchGen::reset( QuantConflictFind * p, bool tgt, QuantInfo * qi ) { Assert( isHandledUfTerm( d_n ) ); TNode f = getMatchOperator( p, d_n ); Debug("qcf-match-debug") << " reset: Var will match operators of " << f << std::endl; - TermArgTrie * qni = p->getTermDatabase()->getTermArgTrie( Node::null(), f ); + TNodeTrie* qni = p->getTermDatabase()->getTermArgTrie(Node::null(), f); if (qni == nullptr || qni->empty()) { //inform irrelevant quantifiers @@ -1672,7 +1672,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { }else{ //binding a variable d_qni_bound[index] = repVar; - std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.begin(); + std::map::iterator it = + d_qn[index]->d_data.begin(); if( it != d_qn[index]->d_data.end() ) { d_qni.push_back( it ); //set the match @@ -1699,7 +1700,8 @@ bool MatchGen::doMatching( QuantConflictFind * p, QuantInfo * qi ) { } if( !val.isNull() ){ //constrained by val - std::map< TNode, TermArgTrie >::iterator it = d_qn[index]->d_data.find( val ); + std::map::iterator it = + d_qn[index]->d_data.find(val); if( it!=d_qn[index]->d_data.end() ){ Debug("qcf-match-debug") << " Match" << std::endl; d_qni.push_back( it ); diff --git a/src/theory/quantifiers/quant_conflict_find.h b/src/theory/quantifiers/quant_conflict_find.h index 0469e958b..9fa37a96c 100644 --- a/src/theory/quantifiers/quant_conflict_find.h +++ b/src/theory/quantifiers/quant_conflict_find.h @@ -22,7 +22,7 @@ #include "context/cdhashmap.h" #include "context/cdlist.h" -#include "theory/quantifiers/term_database.h" +#include "expr/node_trie.h" #include "theory/quantifiers_engine.h" namespace CVC4 { @@ -45,8 +45,8 @@ private: MatchGen * getChild( int i ) { return &d_children[d_children_order[i]]; } //MatchGen * getChild( int i ) { return &d_children[i]; } //current matching information - std::vector< TermArgTrie * > d_qn; - std::vector< std::map< TNode, TermArgTrie >::iterator > d_qni; + std::vector d_qn; + std::vector::iterator> d_qni; bool doMatching( QuantConflictFind * p, QuantInfo * qi ); //for matching : each index is either a variable or a ground term unsigned d_qni_size; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 482acacc2..44c5586c3 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -32,49 +32,6 @@ namespace CVC4 { namespace theory { namespace quantifiers { -TNode TermArgTrie::existsTerm( std::vector< TNode >& reps, int argIndex ) { - if( argIndex==(int)reps.size() ){ - if( d_data.empty() ){ - return Node::null(); - }else{ - return d_data.begin()->first; - } - }else{ - std::map< TNode, TermArgTrie >::iterator it = d_data.find( reps[argIndex] ); - if( it==d_data.end() ){ - return Node::null(); - }else{ - return it->second.existsTerm( reps, argIndex+1 ); - } - } -} - -bool TermArgTrie::addTerm( TNode n, std::vector< TNode >& reps, int argIndex ){ - return addOrGetTerm( n, reps, argIndex )==n; -} - -TNode TermArgTrie::addOrGetTerm( TNode n, std::vector< TNode >& reps, int argIndex ) { - if( argIndex==(int)reps.size() ){ - if( d_data.empty() ){ - //store n in d_data (this should be interpretted as the "data" and not as a reference to a child) - d_data[n].clear(); - return n; - }else{ - return d_data.begin()->first; - } - }else{ - return d_data[reps[argIndex]].addOrGetTerm( n, reps, argIndex+1 ); - } -} - -void TermArgTrie::debugPrint( const char * c, Node n, unsigned depth ) { - for( std::map< TNode, TermArgTrie >::iterator it = d_data.begin(); it != d_data.end(); ++it ){ - for( unsigned i=0; ifirst << std::endl; - it->second.debugPrint( c, n, depth+1 ); - } -} - TermDb::TermDb(context::Context* c, context::UserContext* u, QuantifiersEngine* qe) : d_quantEngine(qe), @@ -1056,12 +1013,13 @@ bool TermDb::reset( Theory::Effort effort ){ return true; } -TermArgTrie * TermDb::getTermArgTrie( Node f ) { +TNodeTrie* TermDb::getTermArgTrie(Node f) +{ if( options::ufHo() ){ f = getOperatorRepresentative( f ); } computeUfTerms( f ); - std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); + std::map::iterator itut = d_func_map_trie.find(f); if( itut!=d_func_map_trie.end() ){ return &itut->second; }else{ @@ -1069,19 +1027,21 @@ TermArgTrie * TermDb::getTermArgTrie( Node f ) { } } -TermArgTrie * TermDb::getTermArgTrie( Node eqc, Node f ) { +TNodeTrie* TermDb::getTermArgTrie(Node eqc, Node f) +{ if( options::ufHo() ){ f = getOperatorRepresentative( f ); } computeUfEqcTerms( f ); - std::map< Node, TermArgTrie >::iterator itut = d_func_map_eqc_trie.find( f ); + std::map::iterator itut = d_func_map_eqc_trie.find(f); if( itut==d_func_map_eqc_trie.end() ){ return NULL; }else{ if( eqc.isNull() ){ return &itut->second; }else{ - std::map< TNode, TermArgTrie >::iterator itute = itut->second.d_data.find( eqc ); + std::map::iterator itute = + itut->second.d_data.find(eqc); if( itute!=itut->second.d_data.end() ){ return &itute->second; }else{ @@ -1096,7 +1056,7 @@ TNode TermDb::getCongruentTerm( Node f, Node n ) { f = getOperatorRepresentative( f ); } computeUfTerms( f ); - std::map< Node, TermArgTrie >::iterator itut = d_func_map_trie.find( f ); + std::map::iterator itut = d_func_map_trie.find(f); if( itut!=d_func_map_trie.end() ){ computeArgReps( n ); return itut->second.existsTerm( d_arg_reps[n] ); diff --git a/src/theory/quantifiers/term_database.h b/src/theory/quantifiers/term_database.h index 7e3806e8c..cc9a24d08 100644 --- a/src/theory/quantifiers/term_database.h +++ b/src/theory/quantifiers/term_database.h @@ -21,9 +21,10 @@ #include #include "expr/attribute.h" +#include "expr/node_trie.h" +#include "theory/quantifiers/quant_util.h" #include "theory/theory.h" #include "theory/type_enumerator.h" -#include "theory/quantifiers/quant_util.h" namespace CVC4 { namespace theory { @@ -37,69 +38,6 @@ namespace inst{ namespace quantifiers { -/** Term arg trie class -* -* This also referred to as a "term index" or a "signature table". -* -* This data structure stores a set expressions, indexed by representatives of -* their arguments. -* -* For example, consider the equivalence classes : -* -* { a, d, f( d, c ), f( a, c ) } -* { b, f( b, d ) } -* { c, f( b, b ) } -* -* where the first elements ( a, b, c ) are the representatives of these classes. -* The TermArgTrie t we may build for f is : -* -* t : -* t.d_data[a] : -* t.d_data[a].d_data[c] : -* t.d_data[a].d_data[c].d_data[f(d,c)] : (leaf) -* t.d_data[b] : -* t.d_data[b].d_data[b] : -* t.d_data[b].d_data[b].d_data[f(b,b)] : (leaf) -* t.d_data[b].d_data[d] : -* t.d_data[b].d_data[d].d_data[f(b,d)] : (leaf) -* -* Leaf nodes store the terms that are indexed by the arguments, for example -* term f(d,c) is indexed by the representative arguments (a,c), and is stored -* as a the (single) key in the data of t.d_data[a].d_data[c]. -*/ -class TermArgTrie { -public: - /** the data */ - std::map< TNode, TermArgTrie > d_data; -public: - /** for leaf nodes : does this trie have data? */ - bool hasNodeData() { return !d_data.empty(); } - /** for leaf nodes : get term corresponding to this leaf */ - TNode getNodeData() { return d_data.begin()->first; } - /** exists term - * Returns the term that is indexed by reps, if one exists, or - * or returns null otherwise. - */ - TNode existsTerm(std::vector& reps, int argIndex = 0); - /** add or get term - * Returns the term that is previously indexed by reps, if one exists, or - * Adds n to the trie, indexed by reps, and returns n. - */ - TNode addOrGetTerm(TNode n, std::vector& reps, int argIndex = 0); - /** add term - * Returns false if a term is previously indexed by reps. - * Returns true if no term is previously indexed by reps, - * and adds n to the trie, indexed by reps, and returns n. - */ - bool addTerm(TNode n, std::vector& reps, int argIndex = 0); - /** debug print this trie */ - void debugPrint(const char* c, Node n, unsigned depth = 0); - /** clear all data from this trie */ - void clear() { d_data.clear(); } - /** is empty */ - bool empty() { return d_data.empty(); } -};/* class TermArgTrie */ - namespace fmcheck { class FullModelChecker; } @@ -121,12 +59,12 @@ class TermGenEnv; * The primary responsibilities for this class are to : * (1) Maintain a list of all ground terms that exist in the quantifier-free * solvers, as notified through the master equality engine. - * (2) Build TermArgTrie objects that index all ground terms, per operator. + * (2) Build TNodeTrie objects that index all ground terms, per operator. * * Like other utilities, its reset(...) function is called * at the beginning of full or last call effort checks. * This initializes the database for the round. However, - * notice that TermArgTrie objects are computed + * notice that TNodeTrie objects are computed * lazily for performance reasons. */ class TermDb : public QuantifiersUtil { @@ -213,10 +151,10 @@ class TermDb : public QuantifiersUtil { */ Node getMatchOperator(Node n); /** get term arg index for all f-applications in the current context */ - TermArgTrie* getTermArgTrie(Node f); + TNodeTrie* getTermArgTrie(Node f); /** get the term arg trie for f-applications in the equivalence class of eqc. */ - TermArgTrie* getTermArgTrie(Node eqc, Node f); + TNodeTrie* getTermArgTrie(Node eqc, Node f); /** get congruent term * If possible, returns a term t such that: * (1) t is a term that is currently indexed by this database, @@ -358,8 +296,8 @@ class TermDb : public QuantifiersUtil { /** mapping from terms to representatives of their arguments */ std::map< TNode, std::vector< TNode > > d_arg_reps; /** map from operators to trie */ - std::map< Node, TermArgTrie > d_func_map_trie; - std::map< Node, TermArgTrie > d_func_map_eqc_trie; + std::map d_func_map_trie; + std::map d_func_map_eqc_trie; /** mapping from operators to their representative relevant domains */ std::map< Node, std::map< unsigned, std::vector< Node > > > d_func_map_rel_dom; /** has map */ -- cgit v1.2.3