diff options
author | Guy <katz911@gmail.com> | 2016-06-08 15:24:44 -0700 |
---|---|---|
committer | Guy <katz911@gmail.com> | 2016-06-08 15:24:44 -0700 |
commit | f948414b8b9979f3e680abdedf8e3e6fbbbdd226 (patch) | |
tree | 73592bb1c62f16a269bfa0983db93d2f204ea860 | |
parent | 2db4844c1f0c307071ea94d0d58d1f322a0b1a6b (diff) | |
parent | c60db311c3e1ccd7b311fcea444865d1d5d32031 (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
-rw-r--r-- | src/options/datatypes_options | 2 | ||||
-rw-r--r-- | src/smt/smt_engine.cpp | 14 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.cpp | 167 | ||||
-rw-r--r-- | src/theory/datatypes/theory_datatypes.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/equality_infer.cpp | 49 | ||||
-rw-r--r-- | src/theory/quantifiers/equality_infer.h | 8 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.cpp | 35 | ||||
-rw-r--r-- | src/theory/quantifiers/inst_match_generator.h | 10 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 480 | ||||
-rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.h | 9 | ||||
-rw-r--r-- | src/theory/quantifiers/symmetry_breaking.h | 2 | ||||
-rw-r--r-- | src/theory/quantifiers/term_database.cpp | 44 | ||||
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 2 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/regexp_operation.h | 1 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.cpp | 179 | ||||
-rw-r--r-- | src/theory/strings/theory_strings.h | 12 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.cpp | 4 | ||||
-rw-r--r-- | src/theory/strings/theory_strings_preprocess.h | 1 |
19 files changed, 448 insertions, 583 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/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 63afb0b72..d5874c52f 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -552,10 +552,10 @@ class SmtEnginePrivate : public NodeManagerListener { */ unsigned d_simplifyAssertionsDepth; - /** whether certain preprocess steps are necessary */ - bool d_needsExpandDefs; - bool d_needsRewriteBoolTerms; - bool d_needsConstrainSubTypes; + /** TODO: whether certain preprocess steps are necessary */ + //bool d_needsExpandDefs; + //bool d_needsRewriteBoolTerms; + //bool d_needsConstrainSubTypes; public: /** @@ -684,9 +684,9 @@ public: d_abstractValueMap(&d_fakeContext), d_abstractValues(), d_simplifyAssertionsDepth(0), - d_needsExpandDefs(true), - d_needsRewriteBoolTerms(true), - d_needsConstrainSubTypes(true), //TODO + //d_needsExpandDefs(true), + //d_needsRewriteBoolTerms(true), + //d_needsConstrainSubTypes(true), //TODO d_iteSkolemMap(), d_iteRemover(smt.d_userContext), d_pbsProcessor(smt.d_userContext), diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 95d704a0e..a2f995935 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -82,6 +82,8 @@ TheoryDatatypes::~TheoryDatatypes() { Assert(current != NULL); delete current; } + delete d_sygus_split; + delete d_sygus_sym_break; } void TheoryDatatypes::setMasterEqualityEngine(eq::EqualityEngine* eq) { @@ -92,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<TNode>(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; @@ -107,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<TNode>(getSatContext()->getCMM()) ); - d_selector_apps.insertDataFromContextMemory( n, sel ); + d_selector_apps[n] = 0; + return ei; }else{ return NULL; @@ -179,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() ){ @@ -312,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; @@ -324,6 +328,9 @@ void TheoryDatatypes::check(Effort e) { } ++eqcs_i; } + if( added_split ){ + return; + } Trace("datatypes-debug") << "Flush pending facts..." << std::endl; flushPendingFacts(); /* @@ -871,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; i<n_label; i++ ){ + Assert( i<(int)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 ); - addTester( tindex, *j, eqc1, t1, t_arg ); + addTester( tindex, t, eqc1, t1, t_arg ); if( d_conflict ){ Trace("datatypes-debug") << " conflict!" << std::endl; return; } } + } //merge selectors if( !eqc1->d_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; j<n_sel; j++ ){ + addSelector( d_selector_apps_data[t2][j], eqc1, t1, eqc2->d_constructor.get().isNull() ); } } if( checkInst ){ @@ -928,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(); @@ -955,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; } @@ -970,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<n_lbl; i++ ){ + Node t = d_labels_data[n][i]; + Assert( t.getKind()==NOT ); + //pcons[ Datatype::indexOf( t[0].getOperator().toExpr() ) ] = false; + int tindex = DatatypesRewriter::isTester( t[0] ); Assert( tindex!=-1 ); pcons[ tindex ] = false; } @@ -985,11 +996,11 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > } 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; j<n_sel; j++ ){ + int sindex = Datatype::indexOf( d_selector_apps_data[r][j].getOperator().toExpr() ); sels[sindex] = true; } } @@ -1056,12 +1067,13 @@ void TheoryDatatypes::addTester( int ttindex, Node t, EqcInfo* eqc, Node n, Node } }else{ //otherwise, scan list of labels - NodeListMap::iterator lbl_i = d_labels.find( n ); + NodeIntMap::iterator lbl_i = d_labels.find( n ); Assert( 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 ); - j = *i; + int n_lbl = (*lbl_i).second; + 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 = Datatype::indexOf( jt.getOperator().toExpr() ); int jtindex = DatatypesRewriter::isTester( jt ); @@ -1077,16 +1089,24 @@ 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 ); + //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; @@ -1100,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; i<n_lbl; i++ ){ + Node ti = d_labels_data[n][i]; + nb << ti; + Assert( ti.getKind()==NOT ); Node t_arg2; - DatatypesRewriter::isTester( (*i)[0], t_arg2 ); + DatatypesRewriter::isTester( ti[0], t_arg2 ); //Assert( tindex!=-1 ); if( std::find( eq_terms.begin(), eq_terms.end(), t_arg2 )==eq_terms.end() ){ eq_terms.push_back( t_arg2 ); @@ -1141,19 +1164,26 @@ 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 - NodeListMap::iterator sel_i = d_selector_apps.find( n ); + NodeIntMap::iterator sel_i = d_selector_apps.find( n ); Assert( sel_i != d_selector_apps.end() ); if( sel_i != d_selector_apps.end() ){ - NodeList* sel = (*sel_i).second; - for( NodeList::const_iterator j = sel->begin(); j != sel->end(); ++j ){ - Node ss = *j; + int n_sel = (*sel_i).second; + for( int 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; return; } } //add it to the vector - sel->push_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() ){ @@ -1166,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<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 ){ - Node n = *i; std::vector< TNode > 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 ); @@ -1189,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; j<n_sel; j++ ){ + Node s = d_selector_apps_data[n][j]; //collapse the selector - collapseSelector( *j, c ); + collapseSelector( s, c ); } } eqc->d_constructor.set( c ); @@ -2096,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<Node> NodeList; - typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> 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; i<d_eqci[n]->d_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<TNode>(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; i<exp_to_add.size(); i++ ){ - re->push_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; i<exp_to_add.size(); i++ ){ // eqci->d_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<TNode>(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; j<ul->size(); 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<n_ul; j++ ){ + Node r = d_uselist_data[v_solve][j]; //Trace("eq-infer-debug") << " use list size = " << eqci_solved->d_uselist.size() << std::endl; //for( unsigned j=0; j<eqci_solved->d_uselist.size(); j++ ){ // Node r = eqci_solved->d_uselist[j]; diff --git a/src/theory/quantifiers/equality_infer.h b/src/theory/quantifiers/equality_infer.h index 93c7bd080..80d6ef98b 100644 --- a/src/theory/quantifiers/equality_infer.h +++ b/src/theory/quantifiers/equality_infer.h @@ -39,7 +39,7 @@ class EqualityInference typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap; typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap; typedef context::CDChunkList<Node> NodeList; - typedef context::CDHashMap< Node, NodeList *, NodeHashFunction > NodeListMap; + typedef context::CDHashMap< Node, int, NodeHashFunction > NodeIntMap; private: context::Context * d_c; Node d_one; @@ -67,11 +67,13 @@ private: BoolMap d_elim_vars; std::map< Node, EqcInfo * > d_eqci; NodeMap d_rep_to_eqc; - NodeListMap d_rep_exp; + NodeIntMap d_rep_exp; + std::map< Node, std::vector< Node > > d_rep_exp_data; /** set eqc rep */ void setEqcRep( Node t, Node r, std::vector< Node >& exp_to_add, EqcInfo * eqci ); /** use list */ - NodeListMap d_uselist; + NodeIntMap d_uselist; + std::map< Node, std::vector< Node > > d_uselist_data; void addToUseList( Node used, Node eqc ); /** pending merges */ NodeList d_pending_merges; diff --git a/src/theory/quantifiers/inst_match_generator.cpp b/src/theory/quantifiers/inst_match_generator.cpp index bd5100a2e..2d3bf76f6 100644 --- a/src/theory/quantifiers/inst_match_generator.cpp +++ b/src/theory/quantifiers/inst_match_generator.cpp @@ -32,6 +32,7 @@ namespace theory { namespace inst { InstMatchGenerator::InstMatchGenerator( Node pat ){ + d_cg = NULL; d_needsReset = true; d_active_add = false; Assert( quantifiers::TermDb::hasInstConstAttr(pat) ); @@ -43,12 +44,20 @@ InstMatchGenerator::InstMatchGenerator( Node pat ){ } InstMatchGenerator::InstMatchGenerator() { + d_cg = NULL; d_needsReset = true; d_active_add = false; d_next = NULL; d_matchPolicy = MATCH_GEN_DEFAULT; } +InstMatchGenerator::~InstMatchGenerator() throw() { + for( unsigned i=0; i<d_children.size(); i++ ){ + delete d_children[i]; + } + delete d_cg; +} + void InstMatchGenerator::setActiveAdd(bool val){ d_active_add = val; if( d_next!=NULL ){ @@ -249,7 +258,7 @@ bool InstMatchGenerator::getMatch( Node f, Node t, InstMatch& m, QuantifiersEngi Trace("matching-debug2") << "Reset children..." << std::endl; //now, fit children into match //we will be requesting candidates for matching terms for each child - for( int i=0; i<(int)d_children.size(); i++ ){ + for( unsigned i=0; i<d_children.size(); i++ ){ d_children[i]->reset( t[ d_children_index[i] ], qe ); } Trace("matching-debug2") << "Continue next " << d_next << std::endl; @@ -484,7 +493,7 @@ d_f( q ){ } Debug("smart-multi-trigger") << std::endl; } - for( int i=0; i<(int)pats.size(); i++ ){ + for( unsigned i=0; i<pats.size(); i++ ){ Node n = pats[i]; //make the match generator d_children.push_back( InstMatchGenerator::mkInstMatchGenerator(q, n, qe ) ); @@ -492,7 +501,7 @@ d_f( q ){ std::vector< int > unique_vars; std::map< int, bool > shared_vars; int numSharedVars = 0; - for( int j=0; j<(int)d_var_contains[n].size(); j++ ){ + for( unsigned j=0; j<d_var_contains[n].size(); j++ ){ if( d_var_to_node[ d_var_contains[n][j] ].size()==1 ){ Debug("smart-multi-trigger") << "Var " << d_var_contains[n][j] << " is unique to " << pats[i] << std::endl; unique_vars.push_back( d_var_contains[n][j] ); @@ -503,7 +512,7 @@ d_f( q ){ } //we use the latest shared variables, then unique variables std::vector< int > vars; - int index = i==0 ? (int)(pats.size()-1) : (i-1); + unsigned index = i==0 ? pats.size()-1 : (i-1); while( numSharedVars>0 && index!=i ){ for( std::map< int, bool >::iterator it = shared_vars.begin(); it != shared_vars.end(); ++it ){ if( it->second ){ @@ -519,16 +528,24 @@ d_f( q ){ } vars.insert( vars.end(), unique_vars.begin(), unique_vars.end() ); Debug("smart-multi-trigger") << " Index[" << i << "]: "; - for( int i=0; i<(int)vars.size(); i++ ){ - Debug("smart-multi-trigger") << vars[i] << " "; + for( unsigned j=0; j<vars.size(); j++ ){ + Debug("smart-multi-trigger") << vars[j] << " "; } Debug("smart-multi-trigger") << std::endl; //make ordered inst match trie - InstMatchTrie::ImtIndexOrder* imtio = new InstMatchTrie::ImtIndexOrder; - imtio->d_order.insert( imtio->d_order.begin(), vars.begin(), vars.end() ); - d_children_trie.push_back( InstMatchTrieOrdered( imtio ) ); + d_imtio[i] = new InstMatchTrie::ImtIndexOrder; + d_imtio[i]->d_order.insert( d_imtio[i]->d_order.begin(), vars.begin(), vars.end() ); + d_children_trie.push_back( InstMatchTrieOrdered( d_imtio[i] ) ); } +} +InstMatchGeneratorMulti::~InstMatchGeneratorMulti() throw() { + for( unsigned i=0; i<d_children.size(); i++ ){ + delete d_children[i]; + } + for( std::map< unsigned, InstMatchTrie::ImtIndexOrder* >::iterator it = d_imtio.begin(); it != d_imtio.end(); ++it ){ + delete it->second; + } } /** reset instantiation round (call this whenever equivalence classes have changed) */ diff --git a/src/theory/quantifiers/inst_match_generator.h b/src/theory/quantifiers/inst_match_generator.h index 49e3c1ec5..096774c51 100644 --- a/src/theory/quantifiers/inst_match_generator.h +++ b/src/theory/quantifiers/inst_match_generator.h @@ -91,7 +91,7 @@ public: InstMatchGenerator( Node pat ); InstMatchGenerator(); /** destructor */ - ~InstMatchGenerator() throw() {} + virtual ~InstMatchGenerator() throw(); /** The pattern we are producing matches for. If null, this is a multi trigger that is merging matches from d_children. */ @@ -125,7 +125,7 @@ public: class VarMatchGeneratorBooleanTerm : public InstMatchGenerator { public: VarMatchGeneratorBooleanTerm( Node var, Node comp ); - ~VarMatchGeneratorBooleanTerm() throw() {} + virtual ~VarMatchGeneratorBooleanTerm() throw() {} Node d_comp; bool d_rm_prev; /** reset instantiation round (call this at beginning of instantiation round) */ @@ -142,7 +142,7 @@ public: class VarMatchGeneratorTermSubs : public InstMatchGenerator { public: VarMatchGeneratorTermSubs( Node var, Node subs ); - ~VarMatchGeneratorTermSubs() throw() {} + virtual ~VarMatchGeneratorTermSubs() throw() {} TNode d_var; TypeNode d_var_type; Node d_subs; @@ -183,6 +183,8 @@ private: int d_matchPolicy; /** children generators */ std::vector< InstMatchGenerator* > d_children; + /** order */ + std::map< unsigned, InstMatchTrie::ImtIndexOrder* > d_imtio; /** inst match tries for each child */ std::vector< InstMatchTrieOrdered > d_children_trie; /** calculate matches */ @@ -191,7 +193,7 @@ public: /** constructors */ InstMatchGeneratorMulti( Node q, std::vector< Node >& pats, QuantifiersEngine* qe ); /** destructor */ - ~InstMatchGeneratorMulti() throw() {} + virtual ~InstMatchGeneratorMulti() throw(); /** reset instantiation round (call this whenever equivalence classes have changed) */ void resetInstantiationRound( QuantifiersEngine* qe ); /** reset, eqc is the equivalence class to search in (any if eqc=null) */ diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index 511337b40..68f824c57 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -48,7 +48,7 @@ bool QuantifiersRewriter::isClause( Node n ){ bool QuantifiersRewriter::isLiteral( Node n ){ switch( n.getKind() ){ case NOT: - return isLiteral( n[0] ); + return n[0].getKind()!=NOT && isLiteral( n[0] ); break; case OR: case AND: @@ -59,7 +59,8 @@ bool QuantifiersRewriter::isLiteral( Node n ){ return false; break; case EQUAL: - return n[0].getType()!=NodeManager::currentNM()->booleanType(); + //for boolean terms + return !n[0].getType().isBoolean(); break; default: break; @@ -259,121 +260,98 @@ RewriteResponse QuantifiersRewriter::postRewrite(TNode in) { return RewriteResponse( status, ret ); } -Node QuantifiersRewriter::computeElimSymbols( Node body ) { - if( isLiteral( body ) ){ - return body; - }else{ - bool childrenChanged = false; - Kind k = body.getKind(); - if( body.getKind()==IMPLIES ){ - k = OR; - childrenChanged = true; - }else if( body.getKind()==XOR ){ - k = IFF; +bool QuantifiersRewriter::addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ){ + if( ( k==OR || k==AND ) && options::elimTautQuant() ){ + Node lit = c.getKind()==NOT ? c[0] : c; + bool pol = c.getKind()!=NOT; + std::map< Node, bool >::iterator it = lit_pol.find( lit ); + if( it==lit_pol.end() ){ + lit_pol[lit] = pol; + children.push_back( c ); + }else{ childrenChanged = true; - } - std::vector< Node > children; - std::map< Node, bool > lit_pol; - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - Node c = computeElimSymbols( body[i] ); - if( i==0 && ( body.getKind()==IMPLIES || body.getKind()==XOR ) ){ - c = c.negate(); - } - if( ( k==OR || k==AND ) && options::elimTautQuant() ){ - Node lit = c.getKind()==NOT ? c[0] : c; - bool pol = c.getKind()!=NOT; - std::map< Node, bool >::iterator it = lit_pol.find( lit ); - if( it==lit_pol.end() ){ - lit_pol[lit] = pol; - children.push_back( c ); - }else{ - childrenChanged = true; - if( it->second!=pol ){ - return NodeManager::currentNM()->mkConst( k==OR ); - } - } - }else{ - children.push_back( c ); + if( it->second!=pol ){ + return false; } - childrenChanged = childrenChanged || c!=body[i]; - } - //if( body.getKind()==ITE && isLiteral( body[0] ) ){ - // ret = NodeManager::currentNM()->mkNode( AND, NodeManager::currentNM()->mkNode( OR, body[0].negate(), body[1] ), - // NodeManager::currentNM()->mkNode( OR, body[0], body[2] ) ); - //} - if( childrenChanged ){ - return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children ); - }else{ - return body; } + }else{ + children.push_back( c ); } + return true; } -Node QuantifiersRewriter::computeNNF( Node body ){ - if( body.getKind()==NOT ){ +// eliminates IMPLIES/XOR, removes duplicates/infers tautologies of AND/OR, and computes NNF +Node QuantifiersRewriter::computeElimSymbols( Node body ) { + Kind ok = body.getKind(); + Kind k = ok; + bool negAllCh = false; + bool negCh1 = false; + if( ok==IMPLIES ){ + k = OR; + negCh1 = true; + }else if( ok==XOR ){ + k = IFF; + negCh1 = true; + }else if( ok==NOT ){ if( body[0].getKind()==NOT ){ - return computeNNF( body[0][0] ); - }else if( isLiteral( body[0] ) ){ - return body; + return computeElimSymbols( body[0][0] ); + }else if( body[0].getKind()==OR || body[0].getKind()==IMPLIES ){ + k = AND; + negAllCh = true; + negCh1 = body[0].getKind()==IMPLIES; + body = body[0]; + }else if( body[0].getKind()==AND ){ + k = OR; + negAllCh = true; + body = body[0]; + }else if( body[0].getKind()==XOR || body[0].getKind()==IFF ){ + k = IFF; + negCh1 = ( body[0].getKind()==IFF ); + body = body[0]; + }else if( body[0].getKind()==ITE ){ + k = body[0].getKind(); + negAllCh = true; + negCh1 = true; + body = body[0]; }else{ - std::vector< Node > children; - Kind k = body[0].getKind(); - - if( body[0].getKind()==OR || body[0].getKind()==AND ){ - k = body[0].getKind()==AND ? OR : AND; - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - Node nc = computeNNF( body[0][i].notNode() ); - if( nc.getKind()==k ){ - for( unsigned j=0; j<nc.getNumChildren(); j++ ){ - children.push_back( nc[j] ); - } - }else{ - children.push_back( nc ); - } - } - }else if( body[0].getKind()==IFF ){ - for( int i=0; i<2; i++ ){ - Node nn = i==0 ? body[0][i] : body[0][i].notNode(); - children.push_back( computeNNF( nn ) ); - } - }else if( body[0].getKind()==ITE ){ - for( int i=0; i<3; i++ ){ - Node nn = i==0 ? body[0][i] : body[0][i].notNode(); - children.push_back( computeNNF( nn ) ); - } - }else{ - Notice() << "Unhandled Quantifiers NNF: " << body << std::endl; - return body; - } - return NodeManager::currentNM()->mkNode( k, children ); + return body; } - }else if( isLiteral( body ) ){ + }else if( ok!=IFF && ok!=ITE && ok!=AND && ok!=OR ){ + //a literal return body; - }else{ - std::vector< Node > children; - bool childrenChanged = false; - bool isAssoc = body.getKind()==AND || body.getKind()==OR; - for( int i=0; i<(int)body.getNumChildren(); i++ ){ - Node nc = computeNNF( body[i] ); - if( isAssoc && nc.getKind()==body.getKind() ){ - for( unsigned j=0; j<nc.getNumChildren(); j++ ){ - children.push_back( nc[j] ); + } + bool childrenChanged = false; + std::vector< Node > children; + std::map< Node, bool > lit_pol; + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node c = computeElimSymbols( ( i==0 && negCh1 )!=negAllCh ? body[i].negate() : body[i] ); + bool success = true; + if( c.getKind()==k && ( k==OR || k==AND ) ){ + //flatten + childrenChanged = true; + for( unsigned j=0; j<c.getNumChildren(); j++ ){ + if( !addCheckElimChild( children, c[j], k, lit_pol, childrenChanged ) ){ + success = false; + break; } - childrenChanged = true; - }else{ - children.push_back( nc ); - childrenChanged = childrenChanged || nc!=body[i]; } - } - if( childrenChanged ){ - return NodeManager::currentNM()->mkNode( body.getKind(), children ); }else{ - return body; + success = addCheckElimChild( children, c, k, lit_pol, childrenChanged ); + } + if( !success ){ + // tautology + Assert( k==OR || k==AND ); + return NodeManager::currentNM()->mkConst( k==OR ); } + childrenChanged = childrenChanged || c!=body[i]; + } + if( childrenChanged || k!=ok ){ + return ( children.size()==1 && k!=NOT ) ? children[0] : NodeManager::currentNM()->mkNode( k, children ); + }else{ + return body; } } - void QuantifiersRewriter::computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ){ if( n.getKind()==ITE && n[0].getKind()==APPLY_TESTER && n[1].getType().isBoolean() ){ @@ -1036,144 +1014,6 @@ Node QuantifiersRewriter::computeVarElimination( Node body, std::vector< Node >& return body; } -Node QuantifiersRewriter::computeClause( Node n ){ - Assert( isClause( n ) ); - if( isLiteral( n ) ){ - return n; - }else{ - NodeBuilder<> t(OR); - if( n.getKind()==NOT ){ - if( n[0].getKind()==NOT ){ - return computeClause( n[0][0] ); - }else{ - //De-Morgan's law - Assert( n[0].getKind()==AND ); - for( int i=0; i<(int)n[0].getNumChildren(); i++ ){ - Node nn = computeClause( n[0][i].notNode() ); - addNodeToOrBuilder( nn, t ); - } - } - }else{ - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node nn = computeClause( n[i] ); - addNodeToOrBuilder( nn, t ); - } - } - return t.constructNode(); - } -} - -Node QuantifiersRewriter::computeCNF( Node n, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ){ - if( isLiteral( n ) ){ - return n; - }else if( !forcePred && isClause( n ) ){ - return computeClause( n ); - }else{ - Kind k = n.getKind(); - NodeBuilder<> t(k); - for( int i=0; i<(int)n.getNumChildren(); i++ ){ - Node nc = n[i]; - Node ncnf = computeCNF( nc, args, defs, k!=OR ); - if( k==OR ){ - addNodeToOrBuilder( ncnf, t ); - }else{ - t << ncnf; - } - } - if( !forcePred && k==OR ){ - return t.constructNode(); - }else{ - //compute the free variables - Node nt = t; - std::vector< Node > activeArgs; - computeArgVec( args, activeArgs, nt ); - std::vector< TypeNode > argTypes; - for( int i=0; i<(int)activeArgs.size(); i++ ){ - argTypes.push_back( activeArgs[i].getType() ); - } - //create the predicate - Assert( argTypes.size()>0 ); - TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, NodeManager::currentNM()->booleanType() ); - std::stringstream ss; - ss << "cnf_" << n.getKind() << "_" << n.getId(); - Node op = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "was created by the quantifiers rewriter" ); - std::vector< Node > predArgs; - predArgs.push_back( op ); - predArgs.insert( predArgs.end(), activeArgs.begin(), activeArgs.end() ); - Node pred = NodeManager::currentNM()->mkNode( APPLY_UF, predArgs ); - Trace("quantifiers-rewrite-cnf-debug") << "Made predicate " << pred << " for " << nt << std::endl; - //create the bound var list - Node bvl = NodeManager::currentNM()->mkNode( BOUND_VAR_LIST, activeArgs ); - //now, look at the structure of nt - if( nt.getKind()==NOT ){ - //case for NOT - for( int i=0; i<2; i++ ){ - NodeBuilder<> tt(OR); - tt << ( i==0 ? nt[0].notNode() : nt[0] ); - tt << ( i==0 ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - }else if( nt.getKind()==OR ){ - //case for OR - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - NodeBuilder<> tt(OR); - tt << nt[i].notNode() << pred; - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - NodeBuilder<> tt(OR); - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - tt << nt[i]; - } - tt << pred.notNode(); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - }else if( nt.getKind()==AND ){ - //case for AND - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - NodeBuilder<> tt(OR); - tt << nt[i] << pred.notNode(); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - NodeBuilder<> tt(OR); - for( int i=0; i<(int)nt.getNumChildren(); i++ ){ - tt << nt[i].notNode(); - } - tt << pred; - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - }else if( nt.getKind()==IFF ){ - //case for IFF - for( int i=0; i<4; i++ ){ - NodeBuilder<> tt(OR); - tt << ( ( i==0 || i==3 ) ? nt[0].notNode() : nt[0] ); - tt << ( ( i==1 || i==3 ) ? nt[1].notNode() : nt[1] ); - tt << ( ( i==0 || i==1 ) ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - }else if( nt.getKind()==ITE ){ - //case for ITE - for( int j=1; j<=2; j++ ){ - for( int i=0; i<2; i++ ){ - NodeBuilder<> tt(OR); - tt << ( ( j==1 ) ? nt[0].notNode() : nt[0] ); - tt << ( ( i==1 ) ? nt[j].notNode() : nt[j] ); - tt << ( ( i==0 ) ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - } - for( int i=0; i<2; i++ ){ - NodeBuilder<> tt(OR); - tt << ( i==0 ? nt[1].notNode() : nt[1] ); - tt << ( i==0 ? nt[2].notNode() : nt[2] ); - tt << ( i==1 ? pred.notNode() : pred ); - defs << NodeManager::currentNM()->mkNode( FORALL, bvl, tt.constructNode() ); - } - }else{ - Notice() << "Unhandled Quantifiers CNF: " << nt << std::endl; - } - return pred; - } - } -} - Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, bool pol ){ if( body.getKind()==FORALL ){ if( pol && ( options::prenexQuant()==PRENEX_ALL || body.getNumChildren()==2 ) ){ @@ -1181,15 +1021,13 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b std::vector< Node > subs; //for doing prenexing of same-signed quantifiers //must rename each variable that already exists - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - //if( std::find( args.begin(), args.end(), body[0][i] )!=args.end() ){ + for( unsigned i=0; i<body[0].getNumChildren(); i++ ){ terms.push_back( body[0][i] ); subs.push_back( NodeManager::currentNM()->mkBoundVar( body[0][i].getType() ) ); } args.insert( args.end(), subs.begin(), subs.end() ); Node newBody = body[1]; newBody = newBody.substitute( terms.begin(), terms.end(), subs.begin(), subs.end() ); - Debug("quantifiers-substitute-debug") << "Did substitute have an effect" << (body[1] != newBody) << body[1] << " became " << newBody << endl; return newBody; }else{ return body; @@ -1198,7 +1036,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b Assert( body.getKind()!=EXISTS ); bool childrenChanged = false; std::vector< Node > newChildren; - for( int i=0; i<(int)body.getNumChildren(); i++ ){ + for( unsigned i=0; i<body.getNumChildren(); i++ ){ bool newHasPol; bool newPol; QuantPhaseReq::getPolarity( body, i, true, pol, newHasPol, newPol ); @@ -1224,7 +1062,7 @@ Node QuantifiersRewriter::computePrenex( Node body, std::vector< Node >& args, b } } -Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node body ) { +Node QuantifiersRewriter::computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ) { Assert( body.getKind()==OR ); size_t var_found_count = 0; size_t eqc_count = 0; @@ -1240,8 +1078,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node Node n = body[i]; std::vector< Node > lit_args; computeArgVec( args, lit_args, n ); - if (lit_args.empty()) { - lits.push_back(n); + if( lit_args.empty() ){ + lits.push_back( n ); }else { //collect the equivalence classes this literal belongs to, and the new variables it contributes std::vector< int > eqcs; @@ -1293,8 +1131,8 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node eqc_to_lit[eqcz].push_back(n); } } - if ( eqc_active>1 || !lits.empty() ){ - Trace("clause-split-debug") << "Split clause " << f << std::endl; + if ( eqc_active>1 || !lits.empty() || var_to_eqc.size()!=args.size() ){ + Trace("clause-split-debug") << "Split quantified formula with body " << body << std::endl; Trace("clause-split-debug") << " Ground literals: " << std::endl; for( size_t i=0; i<lits.size(); i++) { Trace("clause-split-debug") << " " << lits[i] << std::endl; @@ -1317,27 +1155,21 @@ Node QuantifiersRewriter::computeSplit( Node f, std::vector< Node >& args, Node Node fa = NodeManager::currentNM()->mkNode( FORALL, bvl, body ); lits.push_back(fa); } - Assert( lits.size()>1 ); - Node nf = NodeManager::currentNM()->mkNode(OR,lits); + Assert( !lits.empty() ); + Node nf = lits.size()==1 ? lits[0] : NodeManager::currentNM()->mkNode(OR,lits); Trace("clause-split-debug") << "Made node : " << nf << std::endl; return nf; + }else{ + return mkForAll( args, body, qa ); } - return f; } Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ){ - std::vector< Node > activeArgs; - //if cegqi is on, may be synthesis conjecture, in which case we want to keep all variables - if( options::ceGuidedInst() && qa.d_sygus ){ - activeArgs.insert( activeArgs.end(), args.begin(), args.end() ); - }else{ - computeArgVec2( args, activeArgs, body, qa.d_ipl ); - } - if( activeArgs.empty() ){ + if( args.empty() ){ return body; }else{ std::vector< Node > children; - children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, activeArgs ) ); + children.push_back( NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, args ) ); children.push_back( body ); if( !qa.d_ipl.isNull() ){ children.push_back( qa.d_ipl ); @@ -1346,82 +1178,59 @@ Node QuantifiersRewriter::mkForAll( std::vector< Node >& args, Node body, QAttri } } -Node QuantifiersRewriter::computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ){ +//computes miniscoping, also eliminates variables that do not occur free in body +Node QuantifiersRewriter::computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ){ if( body.getKind()==FORALL ){ - //combine arguments + //combine prenex std::vector< Node > newArgs; - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ + newArgs.insert( newArgs.end(), args.begin(), args.end() ); + for( unsigned i=0; i<body[0].getNumChildren(); i++ ){ newArgs.push_back( body[0][i] ); } - newArgs.insert( newArgs.end(), args.begin(), args.end() ); - return mkForAll( newArgs, body[ 1 ], qa ); - }else{ - if( body.getKind()==NOT ){ - //push not downwards - if( body[0].getKind()==NOT ){ - return computeMiniscoping( f, args, body[0][0], qa ); - }else if( body[0].getKind()==AND ){ - if( options::miniscopeQuantFreeVar() ){ - NodeBuilder<> t(kind::OR); - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - t << ( body[0][i].getKind()==NOT ? body[0][i][0] : body[0][i].notNode() ); - } - return computeMiniscoping( f, args, t.constructNode(), qa ); - } - }else if( body[0].getKind()==OR ){ - if( options::miniscopeQuant() ){ - NodeBuilder<> t(kind::AND); - for( int i=0; i<(int)body[0].getNumChildren(); i++ ){ - Node trm = body[0][i].negate(); - t << computeMiniscoping( f, args, trm, qa ); - } - return t.constructNode(); + return mkForAll( newArgs, body[1], qa ); + }else if( body.getKind()==AND ){ + if( options::miniscopeQuant() ){ + //break apart + NodeBuilder<> t(kind::AND); + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + t << computeMiniscoping( args, body[i], qa ); + } + Node retVal = t; + return retVal; + } + }else if( body.getKind()==OR ){ + if( options::quantSplit() ){ + //splitting subsumes free variable miniscoping, apply it with higher priority + return computeSplit( args, body, qa ); + }else if( options::miniscopeQuantFreeVar() ){ + Node newBody = body; + NodeBuilder<> body_split(kind::OR); + NodeBuilder<> tb(kind::OR); + for( unsigned i=0; i<body.getNumChildren(); i++ ){ + Node trm = body[i]; + if( TermDb::containsTerms( body[i], args ) ){ + tb << trm; + }else{ + body_split << trm; } } - }else if( body.getKind()==AND ){ - if( options::miniscopeQuant() ){ - //break apart - NodeBuilder<> t(kind::AND); - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - t << computeMiniscoping( f, args, body[i], qa ); - } - Node retVal = t; - return retVal; - } - }else if( body.getKind()==OR ){ - if( options::quantSplit() ){ - //splitting subsumes free variable miniscoping, apply it with higher priority - Node nf = computeSplit( f, args, body ); - if( nf!=f ){ - return nf; - } - }else if( options::miniscopeQuantFreeVar() ){ - Node newBody = body; - NodeBuilder<> body_split(kind::OR); - NodeBuilder<> tb(kind::OR); - for( unsigned i=0; i<body.getNumChildren(); i++ ){ - Node trm = body[i]; - if( TermDb::containsTerms( body[i], args ) ){ - tb << trm; - }else{ - body_split << trm; - } - } - if( tb.getNumChildren()==0 ){ - return body_split; - }else if( body_split.getNumChildren()>0 ){ - newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; - body_split << mkForAll( args, newBody, qa ); - return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split; - } + if( tb.getNumChildren()==0 ){ + return body_split; + }else if( body_split.getNumChildren()>0 ){ + newBody = tb.getNumChildren()==1 ? tb.getChild( 0 ) : tb; + std::vector< Node > activeArgs; + computeArgVec2( args, activeArgs, newBody, qa.d_ipl ); + body_split << mkForAll( activeArgs, newBody, qa ); + return body_split.getNumChildren()==1 ? body_split.getChild( 0 ) : body_split; } } + }else if( body.getKind()==NOT ){ + Assert( isLiteral( body[0] ) ); } - //if( body==f[1] ){ - // return f; - //}else{ - return mkForAll( args, body, qa ); - //} + //remove variables that don't occur + std::vector< Node > activeArgs; + computeArgVec2( args, activeArgs, body, qa.d_ipl ); + return mkForAll( activeArgs, body, qa ); } Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& args, Node body ){ @@ -1539,8 +1348,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q return is_std; }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return options::aggressiveMiniscopeQuant() && is_std; - }else if( computeOption==COMPUTE_NNF ){ - return true; }else if( computeOption==COMPUTE_PROCESS_TERMS ){ return options::condRewriteQuant(); }else if( computeOption==COMPUTE_COND_SPLIT ){ @@ -1549,8 +1356,6 @@ bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& q return options::prenexQuant()!=PRENEX_NONE && !options::aggressiveMiniscopeQuant() && is_std; }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ return ( options::varElimQuant() || options::dtVarExpandQuant() || options::purifyQuant() ) && is_std; - //}else if( computeOption==COMPUTE_CNF ){ - // return options::cnfQuant(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ return options::purifyQuant() && is_std; }else{ @@ -1570,11 +1375,9 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut n = computeElimSymbols( n ); }else if( computeOption==COMPUTE_MINISCOPING ){ //return directly - return computeMiniscoping( f, args, n, qa ); + return computeMiniscoping( args, n, qa ); }else if( computeOption==COMPUTE_AGGRESSIVE_MINISCOPING ){ return computeAggressiveMiniscoping( args, n ); - }else if( computeOption==COMPUTE_NNF ){ - n = computeNNF( n ); }else if( computeOption==COMPUTE_PROCESS_TERMS ){ std::vector< Node > new_conds; n = computeProcessTerms( n, args, new_conds, f, qa ); @@ -1588,9 +1391,6 @@ Node QuantifiersRewriter::computeOperation( Node f, int computeOption, QAttribut n = computePrenex( n, args, true ); }else if( computeOption==COMPUTE_VAR_ELIMINATION ){ n = computeVarElimination( n, args, qa ); - //}else if( computeOption==COMPUTE_CNF ){ - //n = computeCNF( n, args, defs, false ); - //ipl = Node::null(); }else if( computeOption==COMPUTE_PURIFY_EXPAND ){ std::vector< Node > conj; computePurifyExpand( n, conj, args, qa ); @@ -1724,15 +1524,15 @@ struct ContainsQuantAttributeId {}; typedef expr::Attribute<ContainsQuantAttributeId, uint64_t> ContainsQuantAttribute; // check if the given node contains a universal quantifier -bool QuantifiersRewriter::containsQuantifiers(Node n) { +bool QuantifiersRewriter::containsQuantifiers( Node n ){ if( n.hasAttribute(ContainsQuantAttribute()) ){ return n.getAttribute(ContainsQuantAttribute())==1; - } else if(n.getKind() == kind::FORALL) { + }else if( n.getKind() == kind::FORALL ){ return true; - } else { + }else{ bool cq = false; for( unsigned i = 0; i < n.getNumChildren(); ++i ){ - if( containsQuantifiers(n[i]) ){ + if( containsQuantifiers( n[i] ) ){ cq = true; break; } diff --git a/src/theory/quantifiers/quantifiers_rewriter.h b/src/theory/quantifiers/quantifiers_rewriter.h index 2071d1793..776517109 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.h +++ b/src/theory/quantifiers/quantifiers_rewriter.h @@ -38,6 +38,7 @@ public: static int getPurifyId( Node n ); static int getPurifyIdLit( Node n ); private: + static bool addCheckElimChild( std::vector< Node >& children, Node c, Kind k, std::map< Node, bool >& lit_pol, bool& childrenChanged ); static void addNodeToOrBuilder( Node n, NodeBuilder<>& t ); static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa ); static void computeArgs( std::vector< Node >& args, std::map< Node, bool >& activeMap, Node n, std::map< Node, bool >& visited ); @@ -46,7 +47,6 @@ private: static Node computeProcessTerms2( Node body, bool hasPol, bool pol, std::map< Node, bool >& currCond, int nCurrCond, std::map< Node, Node >& cache, std::map< Node, Node >& icache, std::vector< Node >& new_vars, std::vector< Node >& new_conds ); - static Node computeClause( Node n ); static void computeDtTesterIteSplit( Node n, std::map< Node, Node >& pcons, std::map< Node, std::map< int, Node > >& ncons, std::vector< Node >& conj ); static bool isConditionalVariableElim( Node n, int pol=0 ); static bool isVariableElim( Node v, Node s, std::map< Node, std::vector< int > >& var_parent ); @@ -57,15 +57,13 @@ private: static Node computeVarElimination2( Node body, std::vector< Node >& args, QAttributes& qa, std::map< Node, std::vector< int > >& var_parent ); private: static Node computeElimSymbols( Node body ); - static Node computeMiniscoping( Node f, std::vector< Node >& args, Node body, QAttributes& qa ); + static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body ); - static Node computeNNF( Node body ); //cache is dependent upon currCond, icache is not, new_conds are negated conditions static Node computeProcessTerms( Node body, std::vector< Node >& new_vars, std::vector< Node >& new_conds, Node q, QAttributes& qa ); static Node computeCondSplit( Node body, QAttributes& qa ); - static Node computeCNF( Node body, std::vector< Node >& args, NodeBuilder<>& defs, bool forcePred ); static Node computePrenex( Node body, std::vector< Node >& args, bool pol ); - static Node computeSplit( Node f, std::vector< Node >& args, Node body ); + static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa ); static Node computeVarElimination( Node body, std::vector< Node >& args, QAttributes& qa ); static Node computePurify( Node body, std::vector< Node >& args, std::map< Node, std::vector< int > >& var_parent ); static void computePurifyExpand( Node body, std::vector< Node >& conj, std::vector< Node >& args, QAttributes& qa ); @@ -74,7 +72,6 @@ private: COMPUTE_ELIM_SYMBOLS = 0, COMPUTE_MINISCOPING, COMPUTE_AGGRESSIVE_MINISCOPING, - COMPUTE_NNF, COMPUTE_PROCESS_TERMS, COMPUTE_PRENEX, COMPUTE_VAR_ELIMINATION, diff --git a/src/theory/quantifiers/symmetry_breaking.h b/src/theory/quantifiers/symmetry_breaking.h index 38fea4f45..e682955e7 100644 --- a/src/theory/quantifiers/symmetry_breaking.h +++ b/src/theory/quantifiers/symmetry_breaking.h @@ -42,9 +42,7 @@ class SubsortSymmetryBreaker { typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; - //typedef context::CDChunkList<int> IntList; typedef context::CDList<Node> NodeList; - typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; private: /** quantifiers engine */ QuantifiersEngine* d_qe; diff --git a/src/theory/quantifiers/term_database.cpp b/src/theory/quantifiers/term_database.cpp index 5645c3401..c34d86497 100644 --- a/src/theory/quantifiers/term_database.cpp +++ b/src/theory/quantifiers/term_database.cpp @@ -238,10 +238,15 @@ void TermDb::computeUfTerms( TNode f ) { if( it!=d_op_map.end() ){ eq::EqualityEngine* ee = d_quantEngine->getMasterEqualityEngine(); Trace("term-db-debug") << "Adding terms for operator " << f << std::endl; + unsigned congruentCount = 0; + unsigned nonCongruentCount = 0; + unsigned alreadyCongruentCount = 0; + unsigned relevantCount = 0; for( unsigned i=0; i<it->second.size(); i++ ){ Node n = it->second[i]; //to be added to term index, term must be relevant, and exist in EE if( hasTermCurrent( n ) && ee->hasTerm( n ) ){ + relevantCount++; if( isTermActive( n ) ){ computeArgReps( n ); @@ -260,7 +265,7 @@ void TermDb::computeUfTerms( TNode f ) { if( at!=n && ee->areEqual( at, n ) ){ setTermInactive( n ); Trace("term-db-debug") << n << " is redundant." << std::endl; - //congruentCount++; + congruentCount++; }else{ if( at!=n && ee->areDisequal( at, n, false ) ){ std::vector< Node > lits; @@ -282,29 +287,22 @@ void TermDb::computeUfTerms( TNode f ) { d_consistent_ee = false; return; } - //nonCongruentCount++; + nonCongruentCount++; d_op_nonred_count[ f ]++; } }else{ Trace("term-db-debug") << n << " is already redundant." << std::endl; - //congruentCount++; - //alreadyCongruentCount++; + alreadyCongruentCount++; } }else{ Trace("term-db-debug") << n << " is not relevant." << std::endl; - //nonRelevantCount++; } } - - /* - if( Trace.isOn("term-db-index") ){ - Trace("term-db-index") << "Term index for " << f << " : " << std::endl; - Trace("term-db-index") << "- " << it->first << std::endl; - d_func_map_trie[ f ].debugPrint("term-db-index", it->second[0]); - Trace("term-db-index") << "Non-Congruent/Congruent/Non-Relevant = "; - Trace("term-db-index") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; + if( Trace.isOn("tdb") ){ + Trace("tdb") << "Term db size [" << f << "] : " << nonCongruentCount << " / "; + Trace("tdb") << ( nonCongruentCount + congruentCount ) << " / " << ( nonCongruentCount + congruentCount + alreadyCongruentCount ) << " / "; + Trace("tdb") << relevantCount << " / " << it->second.size() << std::endl; } - */ } } } @@ -676,10 +674,6 @@ void TermDb::presolve() { } bool TermDb::reset( Theory::Effort effort ){ - //int nonCongruentCount = 0; - //int congruentCount = 0; - //int alreadyCongruentCount = 0; - //int nonRelevantCount = 0; d_op_nonred_count.clear(); d_arg_reps.clear(); d_func_map_trie.clear(); @@ -743,20 +737,6 @@ bool TermDb::reset( Theory::Effort effort ){ } } */ - /* - Trace("term-db-stats") << "TermDb: Reset" << std::endl; - Trace("term-db-stats") << "Non-Congruent/Congruent/Non-Relevant = "; - Trace("term-db-stats") << nonCongruentCount << " / " << congruentCount << " (" << alreadyCongruentCount << ") / " << nonRelevantCount << std::endl; - if( Trace.isOn("term-db-index") ){ - Trace("term-db-index") << "functions : " << std::endl; - for( std::map< Node, std::vector< Node > >::iterator it = d_op_map.begin(); it != d_op_map.end(); ++it ){ - if( it->second.size()>0 ){ - Trace("term-db-index") << "- " << it->first << std::endl; - d_func_map_trie[ it->first ].debugPrint("term-db-index", it->second[0]); - } - } - } - */ return true; } diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 214a4d055..802acc089 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -86,7 +86,7 @@ Trigger::Trigger( QuantifiersEngine* qe, Node f, std::vector< Node >& nodes ) } Trigger::~Trigger() { - if(d_mg != NULL) { delete d_mg; } + delete d_mg; } void Trigger::resetInstantiationRound(){ diff --git a/src/theory/strings/regexp_operation.cpp b/src/theory/strings/regexp_operation.cpp index 53344dd6c..a665a02c1 100644 --- a/src/theory/strings/regexp_operation.cpp +++ b/src/theory/strings/regexp_operation.cpp @@ -39,6 +39,10 @@ RegExpOpr::RegExpOpr() d_sigma_star = NodeManager::currentNM()->mkNode( kind::REGEXP_STAR, d_sigma ); } +RegExpOpr::~RegExpOpr(){ + +} + int RegExpOpr::gcd ( int a, int b ) { int c; while ( a != 0 ) { diff --git a/src/theory/strings/regexp_operation.h b/src/theory/strings/regexp_operation.h index c537553f2..075391370 100644 --- a/src/theory/strings/regexp_operation.h +++ b/src/theory/strings/regexp_operation.h @@ -99,6 +99,7 @@ private: public: RegExpOpr(); + ~RegExpOpr(); bool checkConstRegExp( Node r ); void simplify(Node t, std::vector< Node > &new_nodes, bool polarity); diff --git a/src/theory/strings/theory_strings.cpp b/src/theory/strings/theory_strings.cpp index 497ce5f8c..57344236e 100644 --- a/src/theory/strings/theory_strings.cpp +++ b/src/theory/strings/theory_strings.cpp @@ -2726,23 +2726,17 @@ int TheoryStrings::processSimpleDeq( std::vector< Node >& nfi, std::vector< Node void TheoryStrings::addNormalFormPair( Node n1, Node n2 ){ if( !isNormalFormPair( n1, n2 ) ){ - //Assert( !isNormalFormPair( n1, n2 ) ); - NodeList* lst; - NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); - if( nf_i == d_nf_pairs.end() ){ - if( d_nf_pairs.find( n2 )!=d_nf_pairs.end() ){ - addNormalFormPair( n2, n1 ); - return; - } - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_nf_pairs.insertDataFromContextMemory( n1, lst ); - Trace("strings-nf") << "Create cache for " << n1 << std::endl; - } else { - lst = (*nf_i).second; - } - Trace("strings-nf") << "Add normal form pair : " << n1 << " " << n2 << std::endl; - lst->push_back( n2 ); + int index = 0; + NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + } + d_nf_pairs[n1] = index + 1; + if( index<(int)d_nf_pairs_data[n1].size() ){ + d_nf_pairs_data[n1][index] = n2; + }else{ + d_nf_pairs_data[n1].push_back( n2 ); + } Assert( isNormalFormPair( n1, n2 ) ); } else { Trace("strings-nf-debug") << "Already a normal form pair " << n1 << " " << n2 << std::endl; @@ -2755,15 +2749,14 @@ bool TheoryStrings::isNormalFormPair( Node n1, Node n2 ) { } bool TheoryStrings::isNormalFormPair2( Node n1, Node n2 ) { - //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; - NodeList* lst; - NodeListMap::iterator nf_i = d_nf_pairs.find( n1 ); - if( nf_i != d_nf_pairs.end() ) { - lst = (*nf_i).second; - for( NodeList::const_iterator i = lst->begin(); i != lst->end(); ++i ) { - Node n = *i; - if( n==n2 ) { - return true; + //Trace("strings-debug") << "is normal form pair. " << n1 << " " << n2 << std::endl; + NodeIntMap::const_iterator it = d_nf_pairs.find( n1 ); + if( it!=d_nf_pairs.end() ){ + Assert( d_nf_pairs_data.find( n1 )!=d_nf_pairs_data.end() ); + for( int i=0; i<(*it).second; i++ ){ + Assert( i<(int)d_nf_pairs_data[n1].size() ); + if( d_nf_pairs_data[n1][i]==n2 ){ + return true; } } } @@ -3428,6 +3421,26 @@ void TheoryStrings::updateMpl( Node n, int b ) { } */ + +unsigned TheoryStrings::getNumMemberships( Node n, bool isPos ) { + if( isPos ){ + NodeIntMap::const_iterator it = d_pos_memberships.find( n ); + if( it!=d_pos_memberships.end() ){ + return (*it).second; + } + }else{ + NodeIntMap::const_iterator it = d_neg_memberships.find( n ); + if( it!=d_neg_memberships.end() ){ + return (*it).second; + } + } + return 0; +} + +Node TheoryStrings::getMembership( Node n, bool isPos, unsigned i ) { + return isPos ? d_pos_memberships_data[n][i] : d_neg_memberships_data[n][i]; +} + //// Regular Expressions Node TheoryStrings::mkRegExpAntec(Node atom, Node ant) { if(d_regexp_ant.find(atom) == d_regexp_ant.end()) { @@ -3505,10 +3518,8 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > Trace("regexp-check") << "Normalizing Positive Memberships ... " << std::endl; - for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); - itr_xr != d_pos_memberships.end(); ++itr_xr ) { + for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){ Node x = (*itr_xr).first; - NodeList* lst = (*itr_xr).second; Node nf_x = x; std::vector< Node > nf_x_exp; if(d_normal_forms.find( x ) != d_normal_forms.end()) { @@ -3522,10 +3533,11 @@ bool TheoryStrings::normalizePosMemberships(std::map< Node, std::vector< Node > std::vector< Node > vec_x; std::vector< Node > vec_r; - for(NodeList::const_iterator itr_lst = lst->begin(); - itr_lst != lst->end(); ++itr_lst) { - Node r = *itr_lst; - Node nf_r = normalizeRegexp((*lst)[0]); + unsigned n_pmem = (*itr_xr).second; + Assert( getNumMemberships( x, true )==n_pmem ); + for( unsigned k=0; k<n_pmem; k++ ){ + Node r = getMembership( x, true, k ); + Node nf_r = normalizeRegexp( r ); //AJR: fixed (was normalizing mem #0 always) Node memb = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, nf_x, nf_r); if(d_processed_memberships.find(memb) == d_processed_memberships.end()) { if(d_regexp_opr.checkConstRegExp(nf_r)) { @@ -3755,46 +3767,43 @@ void TheoryStrings::checkMemberships() { Trace("regexp-debug") << "Checking Memberships ... " << std::endl; //if(options::stringEIT()) { //TODO: Opt for normal forms - for(NodeListMap::const_iterator itr_xr = d_pos_memberships.begin(); - itr_xr != d_pos_memberships.end(); ++itr_xr ) { + for( NodeIntMap::const_iterator itr_xr = d_pos_memberships.begin(); itr_xr != d_pos_memberships.end(); ++itr_xr ){ bool spflag = false; Node x = (*itr_xr).first; - NodeList* lst = (*itr_xr).second; Trace("regexp-debug") << "Checking Memberships for " << x << std::endl; if(d_inter_index.find(x) == d_inter_index.end()) { d_inter_index[x] = 0; } int cur_inter_idx = d_inter_index[x]; - if(cur_inter_idx != (int)lst->size()) { - if(lst->size() == 1) { - d_inter_cache[x] = (*lst)[0]; + unsigned n_pmem = (*itr_xr).second; + Assert( getNumMemberships( x, true )==n_pmem ); + if( cur_inter_idx != (int)n_pmem ) { + if( n_pmem == 1) { + d_inter_cache[x] = getMembership( x, true, 0 ); d_inter_index[x] = 1; Trace("regexp-debug") << "... only one choice " << std::endl; - } else if(lst->size() > 1) { + } else if(n_pmem > 1) { Node r; if(d_inter_cache.find(x) != d_inter_cache.end()) { r = d_inter_cache[x]; } if(r.isNull()) { - r = (*lst)[0]; + r = getMembership( x, true, 0 ); cur_inter_idx = 1; } - NodeList::const_iterator itr_lst = lst->begin(); - for(int i=0; i<cur_inter_idx; i++) { - ++itr_lst; - } - Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << lst->size() << std::endl; - for(;itr_lst != lst->end(); ++itr_lst) { - Node r2 = *itr_lst; + + unsigned k_start = cur_inter_idx; + Trace("regexp-debug") << "... staring from : " << cur_inter_idx << ", we have " << n_pmem << std::endl; + for(unsigned k = k_start; k<n_pmem; k++) { + Node r2 = getMembership( x, true, k ); r = d_regexp_opr.intersect(r, r2, spflag); if(spflag) { break; } else if(r == d_emptyRegexp) { std::vector< Node > vec_nodes; - ++itr_lst; - for(NodeList::const_iterator itr2 = lst->begin(); - itr2 != itr_lst; ++itr2) { - Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, *itr2); + for( unsigned kk=0; kk<=k; kk++ ){ + Node rr = getMembership( x, true, kk ); + Node n = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, rr); vec_nodes.push_back( n ); } Node conc; @@ -3809,7 +3818,7 @@ void TheoryStrings::checkMemberships() { //updates if(!d_conflict && !spflag) { d_inter_cache[x] = r; - d_inter_index[x] = (int)lst->size(); + d_inter_index[x] = (int)n_pmem; } } } @@ -4432,44 +4441,52 @@ void TheoryStrings::addMembership(Node assertion) { Node x = atom[0]; Node r = atom[1]; if(polarity) { - NodeList* lst; - NodeListMap::iterator itr_xr = d_pos_memberships.find( x ); - if( itr_xr == d_pos_memberships.end() ){ - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_pos_memberships.insertDataFromContextMemory( x, lst ); - } else { - lst = (*itr_xr).second; - } - //check - for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { - if( r == *itr ) { - return; + int index = 0; + NodeIntMap::const_iterator it = d_pos_memberships.find( x ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + for( int k=0; k<index; k++ ){ + if( k<(int)d_pos_memberships_data[x].size() ){ + if( d_pos_memberships_data[x][k]==r ){ + return; + } + }else{ + break; + } } } - lst->push_back( r ); + d_pos_memberships[x] = index + 1; + if( index<(int)d_pos_memberships_data[x].size() ){ + d_pos_memberships_data[x][index] = r; + }else{ + d_pos_memberships_data[x].push_back( r ); + } } else if(!options::stringIgnNegMembership()) { /*if(options::stringEIT() && d_regexp_opr.checkConstRegExp(r)) { int rt; Node r2 = d_regexp_opr.complement(r, rt); Node a = NodeManager::currentNM()->mkNode(kind::STRING_IN_REGEXP, x, r2); }*/ - NodeList* lst; - NodeListMap::iterator itr_xr = d_neg_memberships.find( x ); - if( itr_xr == d_neg_memberships.end() ){ - lst = new(getSatContext()->getCMM()) NodeList( true, getSatContext(), false, - ContextMemoryAllocator<TNode>(getSatContext()->getCMM()) ); - d_neg_memberships.insertDataFromContextMemory( x, lst ); - } else { - lst = (*itr_xr).second; - } - //check - for( NodeList::const_iterator itr = lst->begin(); itr != lst->end(); ++itr ) { - if( r == *itr ) { - return; + int index = 0; + NodeIntMap::const_iterator it = d_neg_memberships.find( x ); + if( it!=d_nf_pairs.end() ){ + index = (*it).second; + for( int k=0; k<index; k++ ){ + if( k<(int)d_neg_memberships_data[x].size() ){ + if( d_neg_memberships_data[x][k]==r ){ + return; + } + }else{ + break; + } } } - lst->push_back( r ); + d_neg_memberships[x] = index + 1; + if( index<(int)d_neg_memberships_data[x].size() ){ + d_neg_memberships_data[x][index] = r; + }else{ + d_neg_memberships_data[x].push_back( r ); + } } // old if(polarity || !options::stringIgnNegMembership()) { diff --git a/src/theory/strings/theory_strings.h b/src/theory/strings/theory_strings.h index c9e0a29bf..2deb09654 100644 --- a/src/theory/strings/theory_strings.h +++ b/src/theory/strings/theory_strings.h @@ -50,7 +50,6 @@ typedef expr::Attribute< StringsProxyVarAttributeId, bool > StringsProxyVarAttri class TheoryStrings : public Theory { typedef context::CDChunkList<Node> NodeList; - typedef context::CDHashMap<Node, NodeList*, NodeHashFunction> NodeListMap; typedef context::CDHashMap<Node, bool, NodeHashFunction> NodeBoolMap; typedef context::CDHashMap<Node, int, NodeHashFunction> NodeIntMap; typedef context::CDHashMap<Node, Node, NodeHashFunction> NodeNodeMap; @@ -165,7 +164,8 @@ private: std::map< Node, std::vector< Node > > d_normal_forms_exp; std::map< Node, std::map< Node, std::map< bool, int > > > d_normal_forms_exp_depend; //map of pairs of terms that have the same normal form - NodeListMap d_nf_pairs; + NodeIntMap d_nf_pairs; + std::map< Node, std::vector< Node > > d_nf_pairs_data; void addNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair( Node n1, Node n2 ); bool isNormalFormPair2( Node n1, Node n2 ); @@ -421,8 +421,12 @@ private: NodeSet d_regexp_ucached; NodeSet d_regexp_ccached; // stored assertions - NodeListMap d_pos_memberships; - NodeListMap d_neg_memberships; + NodeIntMap d_pos_memberships; + std::map< Node, std::vector< Node > > d_pos_memberships_data; + NodeIntMap d_neg_memberships; + std::map< Node, std::vector< Node > > d_neg_memberships_data; + unsigned getNumMemberships( Node n, bool isPos ); + Node getMembership( Node n, bool isPos, unsigned i ); // semi normal forms for symbolic expression std::map< Node, Node > d_nf_regexps; std::map< Node, std::vector< Node > > d_nf_regexps_exp; diff --git a/src/theory/strings/theory_strings_preprocess.cpp b/src/theory/strings/theory_strings_preprocess.cpp index a4f42bddd..ba811644a 100644 --- a/src/theory/strings/theory_strings_preprocess.cpp +++ b/src/theory/strings/theory_strings_preprocess.cpp @@ -33,6 +33,10 @@ StringsPreprocess::StringsPreprocess( context::UserContext* u ) : d_cache( u ){ d_zero = NodeManager::currentNM()->mkConst( ::CVC4::Rational(0) ); } +StringsPreprocess::~StringsPreprocess(){ + +} + /* int StringsPreprocess::checkFixLenVar( Node t ) { int ret = 2; diff --git a/src/theory/strings/theory_strings_preprocess.h b/src/theory/strings/theory_strings_preprocess.h index 5bc9667ea..abc7b5a91 100644 --- a/src/theory/strings/theory_strings_preprocess.h +++ b/src/theory/strings/theory_strings_preprocess.h @@ -40,6 +40,7 @@ private: Node simplify( Node t, std::vector< Node > &new_nodes ); public: StringsPreprocess( context::UserContext* u ); + ~StringsPreprocess(); Node decompose( Node t, std::vector< Node > &new_nodes ); void simplify(std::vector< Node > &vec_node); |