diff options
| -rw-r--r-- | src/theory/datatypes/datatypes_sygus.cpp | 7 | ||||
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 145 | ||||
| -rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 42 |
3 files changed, 113 insertions, 81 deletions
diff --git a/src/theory/datatypes/datatypes_sygus.cpp b/src/theory/datatypes/datatypes_sygus.cpp index 2fee4f48d..526ca2d4a 100644 --- a/src/theory/datatypes/datatypes_sygus.cpp +++ b/src/theory/datatypes/datatypes_sygus.cpp @@ -538,9 +538,10 @@ Node SygusSymBreakNew::getSimpleSymBreakPred(Node e, // enumerator is only specific to variable agnostic symmetry breaking e = Node::null(); } - std::map<unsigned, Node>::iterator it = - d_simple_sb_pred[e][tn][tindex][optHashVal].find(depth); - if (it != d_simple_sb_pred[e][tn][tindex][optHashVal].end()) + std::map<unsigned, Node>& ssbCache = + d_simple_sb_pred[e][tn][tindex][optHashVal]; + std::map<unsigned, Node>::iterator it = ssbCache.find(depth); + if (it != ssbCache.end()) { return it->second; } diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 6aed1514c..77579489a 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -488,7 +488,8 @@ void TheoryDatatypes::assertFact( Node fact, Node exp ){ //add to tester if applicable Node t_arg; int tindex = DatatypesRewriter::isTester( atom, t_arg ); - if( tindex!=-1 ){ + if (tindex >= 0) + { Trace("dt-tester") << "Assert tester : " << atom << " for " << t_arg << std::endl; Node rep = getRepresentative( t_arg ); EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); @@ -863,17 +864,16 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //merge labels - NodeIntMap::iterator lbl_i = d_labels.find( t2 ); + NodeUIntMap::iterator lbl_i = d_labels.find(t2); if( lbl_i != d_labels.end() ){ Trace("datatypes-debug") << " merge labels from " << eqc2 << " " << t2 << std::endl; - int n_label = (*lbl_i).second; - for( int i=0; i<n_label; i++ ){ - Assert( i<(int)d_labels_data[ t2 ].size() ); + size_t n_label = (*lbl_i).second; + for (size_t i = 0; i < n_label; i++) + { + Assert(i < d_labels_data[t2].size()); Node t = d_labels_data[ t2 ][i]; - Node tt = t.getKind()==kind::NOT ? t[0] : t; - Node t_arg; - int tindex = DatatypesRewriter::isTester( tt, t_arg ); - Assert( tindex!=-1 ); + Node t_arg = d_labels_args[t2][i]; + unsigned tindex = d_labels_tindex[t2][i]; addTester( tindex, t, eqc1, t1, t_arg ); if( d_conflict ){ Trace("datatypes-debug") << " conflict!" << std::endl; @@ -887,11 +887,12 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1->d_selectors = true; checkInst = true; } - NodeIntMap::iterator sel_i = d_selector_apps.find( t2 ); + NodeUIntMap::iterator sel_i = d_selector_apps.find(t2); if( sel_i != d_selector_apps.end() ){ Trace("datatypes-debug") << " merge selectors from " << eqc2 << " " << t2 << std::endl; - int n_sel = (*sel_i).second; - for( int j=0; j<n_sel; j++ ){ + size_t n_sel = (*sel_i).second; + for (size_t j = 0; j < n_sel; j++) + { addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() ); } } @@ -923,9 +924,9 @@ bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){ } Node TheoryDatatypes::getLabel( Node n ) { - NodeIntMap::iterator lbl_i = d_labels.find( n ); + NodeUIntMap::iterator lbl_i = d_labels.find(n); if( lbl_i != d_labels.end() ){ - unsigned n_lbl = (*lbl_i).second; + size_t n_lbl = (*lbl_i).second; if( n_lbl>0 && d_labels_data[n][ n_lbl-1 ].getKind()!=kind::NOT ){ return d_labels_data[n][ n_lbl-1 ]; } @@ -949,7 +950,7 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ } bool TheoryDatatypes::hasTester( Node n ) { - NodeIntMap::iterator lbl_i = d_labels.find( n ); + NodeUIntMap::iterator lbl_i = d_labels.find(n); if( lbl_i != d_labels.end() ){ return (*lbl_i).second>0; }else{ @@ -965,14 +966,13 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > if( lindex!=-1 ){ pcons[ lindex ] = true; }else{ - NodeIntMap::iterator lbl_i = d_labels.find( n ); + NodeUIntMap::iterator lbl_i = d_labels.find(n); if( lbl_i != d_labels.end() ){ - int n_lbl = (*lbl_i).second; - for( int i=0; i<n_lbl; i++ ){ - Node t = d_labels_data[n][i]; - Assert( t.getKind()==NOT ); - int tindex = DatatypesRewriter::isTester( t[0] ); - Assert( tindex!=-1 ); + size_t n_lbl = (*lbl_i).second; + for (size_t i = 0; i < n_lbl; i++) + { + Assert(d_labels_data[n][i].getKind() == NOT); + unsigned tindex = d_labels_tindex[n][i]; pcons[ tindex ] = false; } } @@ -1009,16 +1009,21 @@ Node TheoryDatatypes::getTermSkolemFor( Node n ) { } } -void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg ){ +void TheoryDatatypes::addTester( + unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg) +{ Trace("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl; Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; bool tpolarity = t.getKind()!=NOT; Node j, jt; bool makeConflict = false; - int jtindex0 = getLabelIndex( eqc, n ); - if( jtindex0!=-1 ){ + int prevTIndex = getLabelIndex(eqc, n); + if (prevTIndex >= 0) + { + unsigned ptu = static_cast<unsigned>(prevTIndex); //if we already know the constructor type, check whether it is in conflict or redundant - if( (jtindex0==ttindex)!=tpolarity ){ + if ((ptu == ttindex) != tpolarity) + { if( !eqc->d_constructor.get().isNull() ){ //conflict because equivalence class contains a constructor std::vector< TNode > assumptions; @@ -1040,19 +1045,18 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node } }else{ //otherwise, scan list of labels - NodeIntMap::iterator lbl_i = d_labels.find( n ); + NodeUIntMap::iterator lbl_i = d_labels.find(n); Assert( lbl_i != d_labels.end() ); - int n_lbl = (*lbl_i).second; + size_t n_lbl = (*lbl_i).second; std::map< int, bool > neg_testers; - for( int i=0; i<n_lbl; i++ ){ - Node ti = d_labels_data[n][i]; - Assert( ti.getKind()==NOT ); - j = ti; - jt = j[0]; - int jtindex = DatatypesRewriter::isTester( jt ); - Assert( jtindex!=-1 ); + for (size_t i = 0; i < n_lbl; i++) + { + Assert(d_labels_data[n][i].getKind() == NOT); + unsigned jtindex = d_labels_tindex[n][i]; if( jtindex==ttindex ){ if( tpolarity ){ //we are in conflict + j = d_labels_data[n][i]; + jt = j[0]; makeConflict = true; break; }else{ //it is redundant @@ -1064,12 +1068,17 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node } if( !makeConflict ){ Debug("datatypes-labels") << "Add to labels " << t << std::endl; - //lbl->push_back( t ); d_labels[n] = n_lbl + 1; - if( n_lbl<(int)d_labels_data[n].size() ){ + if (n_lbl < d_labels_data[n].size()) + { + // reuse spot in the vector d_labels_data[n][n_lbl] = t; + d_labels_args[n][n_lbl] = t_arg; + d_labels_tindex[n][n_lbl] = ttindex; }else{ - d_labels_data[n].push_back( t ); + d_labels_data[n].push_back(t); + d_labels_args[n].push_back(t_arg); + d_labels_tindex[n].push_back(ttindex); } n_lbl++; @@ -1077,8 +1086,8 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl; if( tpolarity ){ instantiate( eqc, n ); - //TODO : and it is not the other testers FIXME - for( int i=0; i<(int)dt.getNumConstructors(); i++ ){ + for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++) + { if( i!=ttindex && neg_testers.find( i )==neg_testers.end() ){ Assert( n.getKind()!=APPLY_CONSTRUCTOR ); Node infer = DatatypesRewriter::mkTester( n, i, dt ).negate(); @@ -1090,8 +1099,8 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node }else{ //check if we have reached the maximum number of testers // in this case, add the positive tester - //this should not be done for sygus, since cases may be limited - if( n_lbl==(int)dt.getNumConstructors()-1 ){ + if (n_lbl == dt.getNumConstructors() - 1) + { std::vector< bool > pcons; getPossibleCons( eqc, n, pcons ); int testerIndex = -1; @@ -1105,15 +1114,12 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node //we must explain why each term in the set of testers for this equivalence class is equal std::vector< Node > eq_terms; NodeBuilder<> nb(kind::AND); - //for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - - for( int i=0; i<n_lbl; i++ ){ + for (unsigned i = 0; i < n_lbl; i++) + { Node ti = d_labels_data[n][i]; nb << ti; Assert( ti.getKind()==NOT ); - Node t_arg2; - DatatypesRewriter::isTester( ti[0], t_arg2 ); - //Assert( tindex!=-1 ); + Node t_arg2 = d_labels_args[n][i]; if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){ eq_terms.push_back( t_arg2 ); if( t_arg2!=t_arg ){ @@ -1149,11 +1155,12 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) { Trace("dt-collapse-sel") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl; //check to see if it is redundant - NodeIntMap::iterator sel_i = d_selector_apps.find( n ); + NodeUIntMap::iterator sel_i = d_selector_apps.find(n); Assert( sel_i != d_selector_apps.end() ); if( sel_i != d_selector_apps.end() ){ - int n_sel = (*sel_i).second; - for( int j=0; j<n_sel; j++ ){ + size_t n_sel = (*sel_i).second; + for (size_t j = 0; j < n_sel; j++) + { Node ss = d_selector_apps_data[n][j]; if( s.getOperator()==ss.getOperator() && ( s.getKind()!=DT_HEIGHT_BOUND || s[1]==ss[1] ) ){ Trace("dt-collapse-sel") << "...redundant." << std::endl; @@ -1163,7 +1170,8 @@ void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFact //add it to the vector //sel->push_back( s ); d_selector_apps[n] = n_sel + 1; - if( n_sel<(int)d_selector_apps_data[n].size() ){ + if (n_sel < d_selector_apps_data[n].size()) + { d_selector_apps_data[n][n_sel] = s; }else{ d_selector_apps_data[n].push_back( s ); @@ -1181,16 +1189,18 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ Trace("datatypes-debug") << "Add constructor : " << c << " to eqc(" << n << ")" << std::endl; Assert( eqc->d_constructor.get().isNull() ); //check labels - NodeIntMap::iterator lbl_i = d_labels.find( n ); + NodeUIntMap::iterator lbl_i = d_labels.find(n); if( lbl_i != d_labels.end() ){ size_t constructorIndex = DatatypesRewriter::indexOf(c.getOperator()); - int n_lbl = (*lbl_i).second; - for( int i=0; i<n_lbl; i++ ){ + size_t n_lbl = (*lbl_i).second; + for (size_t i = 0; i < n_lbl; i++) + { Node t = d_labels_data[n][i]; - if( t.getKind()==NOT ){ - int tindex = DatatypesRewriter::isTester( t[0] ); - Assert( tindex!=-1 ); - if( tindex==(int)constructorIndex ){ + if (d_labels_data[n][i].getKind() == NOT) + { + unsigned tindex = d_labels_tindex[n][i]; + if (tindex == constructorIndex) + { std::vector< TNode > assumptions; explain( t, assumptions ); explainEquality( c, t[0][0], true, assumptions ); @@ -1204,10 +1214,11 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } } //check selectors - NodeIntMap::iterator sel_i = d_selector_apps.find( n ); + NodeUIntMap::iterator sel_i = d_selector_apps.find(n); if( sel_i != d_selector_apps.end() ){ - int n_sel = (*sel_i).second; - for( int j=0; j<n_sel; j++ ){ + size_t n_sel = (*sel_i).second; + for (size_t j = 0; j < n_sel; j++) + { Node s = d_selector_apps_data[n][j]; //collapse the selector collapseSelector( s, c ); @@ -2121,18 +2132,20 @@ void TheoryDatatypes::printModelDebug( const char* c ){ if( hasLabel( ei, eqc ) ){ Trace( c ) << getLabel( eqc ); }else{ - NodeIntMap::iterator lbl_i = d_labels.find( eqc ); + NodeUIntMap::iterator lbl_i = d_labels.find(eqc); if( lbl_i != d_labels.end() ){ - for( int j=0; j<(*lbl_i).second; j++ ){ + for (size_t j = 0; j < (*lbl_i).second; j++) + { Trace( c ) << d_labels_data[eqc][j] << " "; } } } Trace( c ) << std::endl; Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes, " : "no " ); - NodeIntMap::iterator sel_i = d_selector_apps.find( eqc ); + NodeUIntMap::iterator sel_i = d_selector_apps.find(eqc); if( sel_i != d_selector_apps.end() ){ - for( int j=0; j<(*sel_i).second; j++ ){ + for (size_t j = 0; j < (*sel_i).second; j++) + { Trace( c ) << d_selector_apps_data[eqc][j] << " "; } } diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index de2863718..0a3017058 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -42,7 +42,8 @@ namespace datatypes { class TheoryDatatypes : public Theory { private: typedef context::CDList<Node> NodeList; - typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; + /** maps nodes to an index in a vector */ + typedef context::CDHashMap<Node, size_t, NodeHashFunction> NodeUIntMap; typedef context::CDHashMap<Node, bool, NodeHashFunction> BoolMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeMap; @@ -159,21 +160,38 @@ private: std::map< Node, EqcInfo* > d_eqc_info; /** map from nodes to their instantiated equivalent for each constructor type */ std::map< Node, std::map< int, Node > > d_inst_map; - /** which instantiation lemmas we have sent */ - //std::map< Node, std::vector< Node > > d_inst_lemmas; + //---------------------------------labels /** labels for each equivalence class - * for each eqc n, d_labels[n] is testers that hold for this equivalence class, either: + * + * For each eqc r, d_labels[r] is testers that hold for this equivalence + * class, either: * a list of equations of the form - * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers - * and n is less than the number of possible constructors for t minus one, + * NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ), each of + * which are unique testers, n is less than the number of possible + * constructors for t minus one, * or a list of equations of the form - * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ) followed by - * is_[constructor_(n+1)]( t ), each of which is a unique tester. - */ - NodeIntMap d_labels; + * NOT is_[constructor_1]( t1 )...NOT is_[constructor_n]( tn ) followed by + * is_[constructor_(n+1)]( t{n+1} ), each of which is a unique tester. + * In both cases, t1, ..., tn, t{n+1} are terms in the equivalence class of r. + * + * We store this list in a context-dependent way, using the four data + * structures below. The three vectors d_labels_data, d_labels_args, and + * d_labels_tindex store the tester applications, their arguments and the + * tester index of the application. The map d_labels stores the number of + * values in these vectors that is valid in the current context (this is an + * optimization that ensures we don't need to pop data when changing SAT + * contexts). + */ + NodeUIntMap d_labels; + /** the tester applications */ std::map< Node, std::vector< Node > > d_labels_data; + /** the argument of each node in d_labels_data */ + std::map<Node, std::vector<Node> > d_labels_args; + /** the tester index of each node in d_labels_data */ + std::map<Node, std::vector<unsigned> > d_labels_tindex; + //---------------------------------end labels /** selector apps for eqch equivalence class */ - NodeIntMap d_selector_apps; + NodeUIntMap d_selector_apps; std::map< Node, std::vector< Node > > d_selector_apps_data; /** Are we in conflict */ context::CDO<bool> d_conflict; @@ -300,7 +318,7 @@ private: private: /** add tester to equivalence class info */ - void addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg ); + void addTester(unsigned ttindex, Node t, EqcInfo* eqc, Node n, Node t_arg); /** add selector to equivalence class info */ void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true ); /** add constructor */ |