From 4498f55969576927c290b0fd26e0f94726068d03 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Fri, 3 Jun 2016 19:07:05 -0500 Subject: [PATCH] Remove NodeListMap from datatypes and equality inference. Add option --dt-blast-splits. --- src/options/datatypes_options | 2 + src/theory/datatypes/theory_datatypes.cpp | 165 ++++++++++++--------- src/theory/datatypes/theory_datatypes.h | 8 +- src/theory/quantifiers/equality_infer.cpp | 49 +++--- src/theory/quantifiers/equality_infer.h | 8 +- src/theory/quantifiers/symmetry_breaking.h | 2 - 6 files changed, 135 insertions(+), 99 deletions(-) diff --git a/src/options/datatypes_options b/src/options/datatypes_options index e9578f8d7..bb92b4e05 100644 --- a/src/options/datatypes_options +++ b/src/options/datatypes_options @@ -27,5 +27,7 @@ option dtInferAsLemmas --dt-infer-as-lemmas bool :default false always send lemmas out instead of making internal inferences #option dtRExplainLemmas --dt-rexplain-lemmas bool :default true # regression explanations for datatype lemmas +option dtBlastSplits --dt-blast-splits bool :default false + when applicable, blast splitting lemmas for all variables at once endmodule diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 7994351ee..a2f995935 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -94,9 +94,7 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak if( !hasEqcInfo( n ) ){ if( doMake ){ //add to labels - NodeList* lbl = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_labels.insertDataFromContextMemory( n, lbl ); + d_labels[ n ] = 0; std::map< Node, EqcInfo* >::iterator eqc_i = d_eqc_info.find( n ); EqcInfo* ei; @@ -109,10 +107,10 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( TNode n, bool doMak if( n.getKind()==APPLY_CONSTRUCTOR ){ ei->d_constructor = n; } + //add to selectors - NodeList* sel = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator(getSatContext()->getCMM()) ); - d_selector_apps.insertDataFromContextMemory( n, sel ); + d_selector_apps[n] = 0; + return ei; }else{ return NULL; @@ -181,6 +179,7 @@ void TheoryDatatypes::check(Effort e) { Trace("datatypes-debug") << "Check for splits " << e << endl; do { d_addedFact = false; + bool added_split = false; std::map< TypeNode, Node > rec_singletons; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ @@ -314,7 +313,10 @@ void TheoryDatatypes::check(Effort e) { //doSendLemma( lemma ); d_out->lemma( lemma, false, false, true ); } - return; + added_split = true; + if( !options::dtBlastSplits() ){ + return; + } } }else{ Trace("dt-split-debug") << "Do not split constructor for " << n << " : " << n.getType() << " " << dt.getNumConstructors() << std::endl; @@ -326,6 +328,9 @@ void TheoryDatatypes::check(Effort e) { } ++eqcs_i; } + if( added_split ){ + return; + } Trace("datatypes-debug") << "Flush pending facts..." << std::endl; flushPendingFacts(); /* @@ -873,33 +878,36 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //merge labels - NodeListMap::iterator lbl_i = d_labels.find( t2 ); + NodeIntMap::iterator lbl_i = d_labels.find( t2 ); if( lbl_i != d_labels.end() ){ Trace("datatypes-debug") << " merge labels from " << eqc2 << " " << t2 << std::endl; - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); ++j ){ - Node tt = (*j).getKind()==kind::NOT ? (*j)[0] : (*j); + int n_label = (*lbl_i).second; + for( int i=0; id_selectors && eqc2->d_selectors ){ eqc1->d_selectors = true; checkInst = true; } - NodeListMap::iterator sel_i = d_selector_apps.find( t2 ); + NodeIntMap::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; - NodeList* sel = (*sel_i).second; - for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ - addSelector( *j, eqc1, t1, eqc2->d_constructor.get().isNull() ); + int n_sel = (*sel_i).second; + for( int j=0; jd_constructor.get().isNull() ); } } if( checkInst ){ @@ -930,11 +938,11 @@ bool TheoryDatatypes::hasLabel( EqcInfo* eqc, Node n ){ } Node TheoryDatatypes::getLabel( Node n ) { - NodeListMap::iterator lbl_i = d_labels.find( n ); + NodeIntMap::iterator lbl_i = d_labels.find( n ); if( lbl_i != d_labels.end() ){ - NodeList* lbl = (*lbl_i).second; - if( !(*lbl).empty() && (*lbl)[ (*lbl).size() - 1 ].getKind()!=kind::NOT ){ - return (*lbl)[ (*lbl).size() - 1 ]; + unsigned 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 ]; } } return Node::null(); @@ -957,9 +965,9 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ } bool TheoryDatatypes::hasTester( Node n ) { - NodeListMap::iterator lbl_i = d_labels.find( n ); + NodeIntMap::iterator lbl_i = d_labels.find( n ); if( lbl_i != d_labels.end() ){ - return !(*(*lbl_i).second).empty(); + return (*lbl_i).second>0; }else{ return false; } @@ -972,13 +980,14 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > if( lindex!=-1 ){ pcons[ lindex ] = true; }else{ - NodeListMap::iterator lbl_i = d_labels.find( n ); + NodeIntMap::iterator lbl_i = d_labels.find( n ); if( lbl_i != d_labels.end() ){ - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - Assert( (*i).getKind()==NOT ); - //pcons[ Datatype::indexOf( (*i)[0].getOperator().toExpr() ) ] = false; - int tindex = DatatypesRewriter::isTester( (*i)[0] ); + int n_lbl = (*lbl_i).second; + for( int i=0; i } void TheoryDatatypes::getSelectorsForCons( Node r, std::map< int, bool >& sels ) { - NodeListMap::iterator sel_i = d_selector_apps.find( r ); + NodeIntMap::iterator sel_i = d_selector_apps.find( r ); if( sel_i != d_selector_apps.end() ){ - NodeList* sel = (*sel_i).second; - for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){ - int sindex = Datatype::indexOf( (*j).getOperator().toExpr() ); + int n_sel = (*sel_i).second; + for( int j=0; jbegin(); i != lbl->end(); i++ ) { - Assert( (*i).getKind()==NOT ); - j = *i; + int n_lbl = (*lbl_i).second; + for( int i=0; ipush_back( t ); + //lbl->push_back( t ); + d_labels[n] = n_lbl + 1; + if( n_lbl<(int)d_labels_data[n].size() ){ + d_labels_data[n][n_lbl] = t; + }else{ + d_labels_data[n].push_back( t ); + } + n_lbl++; + const Datatype& dt = ((DatatypeType)(t_arg.getType()).toType()).getDatatype(); - Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << dt.getNumConstructors() << std::endl; + Debug("datatypes-labels") << "Labels at " << n_lbl << " / " << dt.getNumConstructors() << std::endl; if( tpolarity ){ instantiate( eqc, n ); }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( lbl->size()==dt.getNumConstructors()-1 && !dt.isSygus() ){ + if( n_lbl==(int)dt.getNumConstructors()-1 && !dt.isSygus() ){ std::vector< bool > pcons; getPossibleCons( eqc, n, pcons ); int testerIndex = -1; @@ -1102,11 +1120,14 @@ 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++ ) { - nb << (*i); - Assert( (*i).getKind()==NOT ); + //for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { + + for( int i=0; ibegin(); j != sel->end(); ++j ){ - Node ss = *j; + int n_sel = (*sel_i).second; + for( int j=0; jpush_back( s ); + //sel->push_back( s ); + d_selector_apps[n] = n_sel + 1; + if( n_sel<(int)d_selector_apps_data[n].size() ){ + d_selector_apps_data[n][n_sel] = s; + }else{ + d_selector_apps_data[n].push_back( s ); + } + eqc->d_selectors = true; } if( assertFacts && !eqc->d_constructor.get().isNull() ){ @@ -1168,19 +1196,19 @@ 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 - NodeListMap::iterator lbl_i = d_labels.find( n ); + NodeIntMap::iterator lbl_i = d_labels.find( n ); if( lbl_i != d_labels.end() ){ size_t constructorIndex = Datatype::indexOf(c.getOperator().toExpr()); - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - if( (*i).getKind()==NOT ){ - int tindex = DatatypesRewriter::isTester( (*i)[0] ); + int n_lbl = (*lbl_i).second; + for( int i=0; i assumptions; - explain( *i, assumptions ); - explainEquality( c, (*i)[0][0], true, assumptions ); + explain( t, assumptions ); + explainEquality( c, t[0][0], true, assumptions ); d_conflictNode = mkAnd( assumptions ); Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); @@ -1191,12 +1219,13 @@ void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ } } //check selectors - NodeListMap::iterator sel_i = d_selector_apps.find( n ); + NodeIntMap::iterator sel_i = d_selector_apps.find( n ); if( sel_i != d_selector_apps.end() ){ - NodeList* sel = (*sel_i).second; - for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ + int n_sel = (*sel_i).second; + for( int j=0; jd_constructor.set( c ); @@ -2098,21 +2127,19 @@ void TheoryDatatypes::printModelDebug( const char* c ){ if( hasLabel( ei, eqc ) ){ Trace( c ) << getLabel( eqc ); }else{ - NodeListMap::iterator lbl_i = d_labels.find( eqc ); + NodeIntMap::iterator lbl_i = d_labels.find( eqc ); if( lbl_i != d_labels.end() ){ - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator j = lbl->begin(); j != lbl->end(); j++ ){ - Trace( c ) << *j << " "; + for( int 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 " ); - NodeListMap::iterator sel_i = d_selector_apps.find( eqc ); + NodeIntMap::iterator sel_i = d_selector_apps.find( eqc ); if( sel_i != d_selector_apps.end() ){ - NodeList* sel = (*sel_i).second; - for( NodeList::const_iterator j = sel->begin(); j != sel->end(); j++ ){ - Trace( c ) << *j << " "; + for( int j=0; j<(*sel_i).second; j++ ){ + Trace( c ) << d_selector_apps_data[eqc][j] << " "; } } Trace( c ) << std::endl; diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index a1882d171..5722e7822 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -42,7 +42,7 @@ namespace datatypes { class TheoryDatatypes : public Theory { private: typedef context::CDChunkList NodeList; - typedef context::CDHashMap NodeListMap; + typedef context::CDHashMap< Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; @@ -162,9 +162,11 @@ private: * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ) followed by * is_[constructor_(n+1)]( t ), each of which is a unique tester. */ - NodeListMap d_labels; + NodeIntMap d_labels; + std::map< Node, std::vector< Node > > d_labels_data; /** selector apps for eqch equivalence class */ - NodeListMap d_selector_apps; + NodeIntMap d_selector_apps; + std::map< Node, std::vector< Node > > d_selector_apps_data; /** constructor terms */ //BoolMap d_consEqc; /** Are we in conflict */ diff --git a/src/theory/quantifiers/equality_infer.cpp b/src/theory/quantifiers/equality_infer.cpp index c3064116f..5190025ee 100644 --- a/src/theory/quantifiers/equality_infer.cpp +++ b/src/theory/quantifiers/equality_infer.cpp @@ -53,10 +53,10 @@ void EqualityInference::addToExplanation( std::vector< Node >& exp, Node e ) { } void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc ) { - NodeListMap::iterator re_i = d_rep_exp.find( eqc ); + NodeIntMap::iterator re_i = d_rep_exp.find( eqc ); if( re_i!=d_rep_exp.end() ){ - for( unsigned i=0; i<(*re_i).second->size(); i++ ){ - addToExplanation( exp, (*(*re_i).second)[i] ); + for( int i=0; i<(*re_i).second; i++ ){ + addToExplanation( exp, d_rep_exp_data[eqc][i] ); } } //for( unsigned i=0; id_rep_exp.size(); i++ ){ @@ -65,16 +65,19 @@ void EqualityInference::addToExplanationEqc( std::vector< Node >& exp, Node eqc } void EqualityInference::addToExplanationEqc( Node eqc, std::vector< Node >& exp_to_add ) { - NodeListMap::iterator re_i = d_rep_exp.find( eqc ); - NodeList* re; + NodeIntMap::iterator re_i = d_rep_exp.find( eqc ); + int n_re = 0; if( re_i != d_rep_exp.end() ){ - re = (*re_i).second; - }else{ - re = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator(d_c->getCMM()) ); - d_rep_exp.insertDataFromContextMemory( eqc, re ); + n_re = (*re_i).second; } + d_rep_exp[eqc] = n_re + exp_to_add.size(); for( unsigned i=0; ipush_back( exp_to_add[i] ); + if( n_re<(int)d_rep_exp_data[eqc].size() ){ + d_rep_exp_data[eqc][n_re] = exp_to_add[i]; + }else{ + d_rep_exp_data[eqc].push_back( exp_to_add[i] ); + } + n_re++; } //for( unsigned i=0; id_rep_exp.push_back( exp_to_add[i] ); @@ -204,16 +207,18 @@ void EqualityInference::eqNotifyNewClass(TNode t) { void EqualityInference::addToUseList( Node used, Node eqc ) { #if 1 - NodeListMap::iterator ul_i = d_uselist.find( used ); - NodeList* ul; + NodeIntMap::iterator ul_i = d_uselist.find( used ); + int n_ul = 0; if( ul_i != d_uselist.end() ){ - ul = (*ul_i).second; - }else{ - ul = new(d_c->getCMM()) NodeList( true, d_c, false, context::ContextMemoryAllocator(d_c->getCMM()) ); - d_uselist.insertDataFromContextMemory( used, ul ); + n_ul = (*ul_i).second; } + d_uselist[ used ] = n_ul + 1; Trace("eq-infer-debug") << " add to use list : " << used << " -> " << eqc << std::endl; - (*ul).push_back( eqc ); + if( n_ul<(int)d_uselist_data[used].size() ){ + d_uselist_data[used][n_ul] = eqc; + }else{ + d_uselist_data[used].push_back( eqc ); + } #else std::map< Node, EqcInfo * >::iterator itu = d_eqci.find( used ); EqcInfo * eqci_used; @@ -356,12 +361,12 @@ void EqualityInference::eqNotifyMerge(TNode t1, TNode t2) { //go through all equivalence classes that may refer to v_solve std::map< Node, bool > processed; processed[v_solve] = true; - NodeListMap::iterator ul_i = d_uselist.find( v_solve ); + NodeIntMap::iterator ul_i = d_uselist.find( v_solve ); if( ul_i != d_uselist.end() ){ - NodeList* ul = (*ul_i).second; - Trace("eq-infer-debug") << " use list size = " << ul->size() << std::endl; - for( unsigned j=0; jsize(); j++ ){ - Node r = (*ul)[j]; + int n_ul = (*ul_i).second; + Trace("eq-infer-debug") << " use list size = " << n_ul << std::endl; + for( int j=0; j