From 60e8c65407a34d75ccaa88e1ccbb5adb89799330 Mon Sep 17 00:00:00 2001 From: ajreynol Date: Thu, 6 Nov 2014 11:41:35 +0100 Subject: [PATCH] Reenable regression. Add (for now, disabled) changes to datatypes theory combination. Relax communication of dt facts. --- src/theory/datatypes/theory_datatypes.cpp | 103 +++++----------------- src/theory/datatypes/theory_datatypes.h | 4 +- test/regress/regress0/fmf/Makefile.am | 4 +- 3 files changed, 28 insertions(+), 83 deletions(-) diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index f3b8c1ec9..215eb46ca 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -854,6 +854,15 @@ int TheoryDatatypes::getLabelIndex( EqcInfo* eqc, Node n ){ } } +bool TheoryDatatypes::hasTester( Node n ) { + NodeListMap::iterator lbl_i = d_labels.find( n ); + if( lbl_i != d_labels.end() ){ + return !(*(*lbl_i).second).empty(); + }else{ + return false; + } +} + void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& pcons ){ const Datatype& dt = ((DatatypeType)(n.getType()).toType()).getDatatype(); pcons.resize( dt.getNumConstructors(), !hasLabel( eqc, n ) ); @@ -1157,43 +1166,9 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ printModelDebug( "dt-model" ); Trace("dt-model") << std::endl; - /* - bool eq_merged = false; - std::vector< Node > all_eqc; - eq::EqClassesIterator eqcs1_i = eq::EqClassesIterator( &d_equalityEngine ); - while( !eqcs1_i.isFinished() ){ - Node eqc = (*eqcs1_i); - all_eqc.push_back( eqc ); - ++eqcs1_i; - } - //check if equivalence classes have merged - for( unsigned i=0; iareEqual( all_eqc[i], all_eqc[j] ) ){ - Trace("dt-cmi") << "Pre-already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl; - eq_merged = true; - } - } - } - Assert( !eq_merged ); - //*/ - //combine the equality engine m->assertEqualityEngine( &d_equalityEngine ); - /* - //check again if equivalence classes have merged - for( unsigned i=0; iareEqual( all_eqc[i], all_eqc[j] ) ){ - Trace("dt-cmi") << "Already forced equal : " << all_eqc[i] << " = " << all_eqc[j] << std::endl; - eq_merged = true; - } - } - } - Assert( !eq_merged ); - //*/ - //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); std::vector< Node > cons; @@ -1210,18 +1185,21 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ eqc_cons[ eqc ] = c; }else{ //if eqc contains a symbol known to datatypes (a selector), then we must assign - bool containsTSym = false; + bool shouldConsider = false; eq::EqClassIterator eqc_i = eq::EqClassIterator( eqc, &d_equalityEngine ); while( !eqc_i.isFinished() ){ Node n = *eqc_i; Trace("dt-cmi-debug") << n << " has kind " << n.getKind() << ", isVar = " << n.isVar() << std::endl; if( n.isVar() || n.getKind()==APPLY_SELECTOR_TOTAL ){ - containsTSym = true; + shouldConsider = true; break; } ++eqc_i; } - if( containsTSym ){ +/* + bool shouldConsider = ( ei && ei->d_selectors ) || hasTester( eqc ); + */ + if( shouldConsider ){ nodes.push_back( eqc ); } } @@ -1296,22 +1274,6 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-cmi") << pcons[i] << " "; } Trace("dt-cmi") << std::endl; - /* - std::map< int, std::map< int, bool > > sels; - Trace("dt-cmi") << "Existing selectors : "; - NodeListMap::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++ ){ - Expr selectorExpr = (*j).getOperator().toExpr(); - unsigned cindex = Datatype::cindexOf( selectorExpr ); - unsigned index = Datatype::indexOf( selectorExpr ); - sels[cindex][index] = true; - Trace("dt-cmi") << (*j) << " (" << cindex << ", " << index << ") "; - } - } - Trace("dt-cmi") << std::endl; - */ for( unsigned r=0; r<2; r++ ){ if( neqc.isNull() ){ for( unsigned i=0; iassertEquality( eqc, neqc, true ); eqc_cons[ eqc ] = neqc; } - /* - for( unsigned kk=0; kkareEqual( all_eqc[kk], all_eqc[ll] ) ){ - Trace("dt-cmi") << "Forced equal : " << kk << " " << ll << " : " << all_eqc[kk] << " = " << all_eqc[ll] << std::endl; - Node r = m->getRepresentative( all_eqc[kk] ); - Trace("dt-cmi") << " { "; - eq::EqClassIterator eqc_i = eq::EqClassIterator( r, m->d_equalityEngine ); - while( !eqc_i.isFinished() ){ - Trace("dt-cmi") << (*eqc_i) << " "; - ++eqc_i; - } - Trace("dt-cmi") << "} " << std::endl; - } - Assert( !m->areEqual( all_eqc[kk], all_eqc[ll] ) ); - } - } - */ //m->assertRepresentative( neqc ); if( addCons ){ cons.push_back( neqc ); @@ -1810,20 +1754,19 @@ bool TheoryDatatypes::mustCommunicateFact( Node n, Node exp ){ Trace("dt-lemma-debug") << "Compute for " << exp << " => " << n << std::endl; bool addLemma = false; if( n.getKind()==EQUAL || n.getKind()==IFF ){ + /* for( unsigned i=0; i<2; i++ ){ if( n[i].getKind()!=APPLY_SELECTOR_TOTAL && n[i].getKind()!=APPLY_CONSTRUCTOR ){ addLemma = true; } } - - if( !addLemma ){ - TypeNode tn = n[0].getType(); - if( !DatatypesRewriter::isTypeDatatype( tn ) ){ - addLemma = true; - }else{ - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - addLemma = dt.involvesExternalType(); - } + */ + TypeNode tn = n[0].getType(); + if( !DatatypesRewriter::isTypeDatatype( tn ) ){ + addLemma = true; + }else{ + const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); + addLemma = dt.involvesExternalType(); } //for( int j=0; j<(int)n[1].getNumChildren(); j++ ){ // if( !DatatypesRewriter::isTermDatatype( n[1][j] ) ){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 81cbe7523..174117a8f 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -123,12 +123,14 @@ private: //all selectors whose argument is this eqc context::CDO< bool > d_selectors; }; - /** does eqc of n have a label? */ + /** does eqc of n have a label (do we know its constructor)? */ bool hasLabel( EqcInfo* eqc, Node n ); /** get the label associated to n */ Node getLabel( Node n ); /** get the index of the label associated to n */ int getLabelIndex( EqcInfo* eqc, Node n ); + /** does eqc of n have any testers? */ + bool hasTester( Node n ); /** get the possible constructors for n */ void getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool >& cons ); private: diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index cb58ea007..e3e514496 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -34,12 +34,12 @@ TESTS = \ fc-unsat-tot-2.smt2 \ fc-unsat-pent.smt2 \ fc-pigeonhole19.smt2 \ - Hoare-z3.931718.smt + Hoare-z3.931718.smt \ + bug0909.smt2 EXTRA_DIST = $(TESTS) # disabled for now : -# bug0909.smt2 # lst-no-self-rev-exp.smt2 #if CVC4_BUILD_PROFILE_COMPETITION -- 2.30.2