From 29923ecc0467f52a8eb6e318b874269054b956e5 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Wed, 9 Oct 2013 12:26:11 -0500 Subject: [PATCH] More improvements to datatypes, eager selector collapsing, improved collect model info. Also fix bug in model post-processor. --- src/smt/model_postprocessor.cpp | 7 +- src/theory/datatypes/theory_datatypes.cpp | 663 ++++++++++++---------- src/theory/datatypes/theory_datatypes.h | 18 +- 3 files changed, 388 insertions(+), 300 deletions(-) diff --git a/src/smt/model_postprocessor.cpp b/src/smt/model_postprocessor.cpp index cbabc9542..c61a61940 100644 --- a/src/smt/model_postprocessor.cpp +++ b/src/smt/model_postprocessor.cpp @@ -9,9 +9,9 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief + ** \brief + ** ** - ** **/ #include "smt/model_postprocessor.h" @@ -92,6 +92,9 @@ Node ModelPostprocessor::rewriteAs(TNode n, TypeNode asType) { return n; } NodeBuilder<> b(n.getKind()); + if (n.getMetaKind() == kind::metakind::PARAMETERIZED) { + b << n.getOperator(); + } TypeNode::iterator t = asType.begin(); for(TNode::iterator i = n.begin(); i != n.end(); ++i, ++t) { Assert(t != asType.end()); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index fb0ac5923..797445e7e 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -47,8 +47,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, UserContext* u, OutputChannel& out, d_infer_exp(c), d_notify( *this ), d_equalityEngine(d_notify, c, "theory::datatypes::TheoryDatatypes"), - d_selector_apps( c ), d_labels( c ), + d_selector_apps( c ), d_conflict( c, false ), d_collectTermsCache( c ){ @@ -83,6 +83,10 @@ TheoryDatatypes::EqcInfo* TheoryDatatypes::getOrMakeEqcInfo( Node n, bool doMake 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 ); return ei; }else{ return NULL; @@ -201,6 +205,7 @@ void TheoryDatatypes::check(Effort e) { Trace("datatypes-debug") << "Flush pending facts..." << std::endl; addedFact = !d_pending.empty() || !d_pending_merge.empty(); flushPendingFacts(); + /* if( !d_conflict ){ if( options::dtRewriteErrorSel() ){ bool innerAddedFact = false; @@ -211,6 +216,7 @@ void TheoryDatatypes::check(Effort e) { }while( !d_conflict && innerAddedFact ); } } + */ }while( !d_conflict && addedFact ); Trace("datatypes-debug") << "Finished. " << d_conflict << std::endl; if( !d_conflict ){ @@ -467,13 +473,7 @@ void TheoryDatatypes::explain(TNode literal, std::vector& assumptions){ Node TheoryDatatypes::explain( TNode literal ){ std::vector< TNode > assumptions; explain( literal, assumptions ); - if( assumptions.empty() ){ - return NodeManager::currentNM()->mkConst( true ); - }else if( assumptions.size()==1 ){ - return assumptions[0]; - }else{ - return NodeManager::currentNM()->mkNode( kind::AND, assumptions ); - } + return mkAnd( assumptions ); } /** Conflict when merging two constants */ @@ -519,9 +519,6 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ trep2 = eqc2->d_constructor.get(); } EqcInfo* eqc1 = getOrMakeEqcInfo( t1 ); - - - if( eqc1 ){ if( !eqc1->d_constructor.get().isNull() ){ trep1 = eqc1->d_constructor.get(); @@ -529,6 +526,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ //check for clash Node cons1 = eqc1->d_constructor; Node cons2 = eqc2->d_constructor; + //if both have constructor, then either clash or unification if( !cons1.isNull() && !cons2.isNull() ){ Debug("datatypes-debug") << "Constructors : " << cons1 << " " << cons2 << std::endl; if( cons1.getOperator()!=cons2.getOperator() ){ @@ -558,29 +556,11 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ } if( cons1.isNull() && !cons2.isNull() ){ Debug("datatypes-debug") << "Must check if it is okay to set the constructor." << std::endl; - NodeListMap::iterator lbl_i = d_labels.find( t1 ); - if( lbl_i != d_labels.end() ){ - size_t constructorIndex = Datatype::indexOf(cons2.getOperator().toExpr()); - NodeList* lbl = (*lbl_i).second; - for( NodeList::const_iterator i = lbl->begin(); i != lbl->end(); i++ ) { - if( (*i).getKind()==NOT ){ - if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){ - Node n = *i; - std::vector< TNode > assumptions; - explain( *i, assumptions ); - explain( cons2.eqNode( (*i)[0][0] ), assumptions ); - d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_conflict = true; - return; - } - } - } - } - checkInst = true; - eqc1->d_constructor.set( eqc2->d_constructor ); + addConstructor( eqc2->d_constructor.get(), eqc1, t1 ); + if( d_conflict ){ + return; + } } }else{ Debug("datatypes-debug") << "No eqc info for " << t1 << ", must create" << std::endl; @@ -588,10 +568,10 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1 = getOrMakeEqcInfo( t1, true ); eqc1->d_inst.set( eqc2->d_inst ); eqc1->d_constructor.set( eqc2->d_constructor ); + eqc1->d_selectors.set( eqc2->d_selectors ); } - //merge labels NodeListMap::iterator lbl_i = d_labels.find( t2 ); if( lbl_i != d_labels.end() ){ @@ -610,6 +590,14 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ eqc1->d_selectors = true; checkInst = true; } + NodeListMap::iterator sel_i = d_selector_apps.find( t2 ); + if( sel_i != d_selector_apps.end() ){ + Debug("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() ); + } + } if( checkInst ){ instantiate( eqc1, t1 ); if( d_conflict ){ @@ -691,107 +679,184 @@ void TheoryDatatypes::getPossibleCons( EqcInfo* eqc, Node n, std::vector< bool > } void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ - if( !d_conflict ){ - Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; - bool tpolarity = t.getKind()!=NOT; - Node tt = ( t.getKind() == NOT ) ? t[0] : t; - int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); - Node j, jt; - if( hasLabel( eqc, n ) ){ - //if we already know the constructor type, check whether it is in conflict or redundant - int jtindex = getLabelIndex( eqc, n ); - if( (jtindex==ttindex)!=tpolarity ){ - d_conflict = true; - if( !eqc->d_constructor.get().isNull() ){ - //conflict because equivalence class contains a constructor - std::vector< TNode > assumptions; - explain( t, assumptions ); - explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); - d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - return; - }else{ - //conflict because the existing label is contradictory - j = getLabel( n ); - jt = j; - } - }else{ + Debug("datatypes-debug") << "Add tester : " << t << " to eqc(" << n << ")" << std::endl; + Debug("datatypes-labels") << "Add tester " << t << " " << n << " " << eqc << std::endl; + bool tpolarity = t.getKind()!=NOT; + Node tt = ( t.getKind() == NOT ) ? t[0] : t; + int ttindex = Datatype::indexOf( tt.getOperator().toExpr() ); + Node j, jt; + if( hasLabel( eqc, n ) ){ + //if we already know the constructor type, check whether it is in conflict or redundant + int jtindex = getLabelIndex( eqc, n ); + if( (jtindex==ttindex)!=tpolarity ){ + d_conflict = true; + if( !eqc->d_constructor.get().isNull() ){ + //conflict because equivalence class contains a constructor + std::vector< TNode > assumptions; + explain( t, assumptions ); + explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); + d_conflictNode = mkAnd( assumptions ); + Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); return; + }else{ + //conflict because the existing label is contradictory + j = getLabel( n ); + jt = j; } }else{ - //otherwise, scan list of labels - NodeListMap::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; - jt = j[0]; - int jtindex = Datatype::indexOf( jt.getOperator().toExpr() ); - if( jtindex==ttindex ){ - if( tpolarity ){ //we are in conflict - d_conflict = true; - break; - }else{ //it is redundant - return; - } + return; + } + }else{ + //otherwise, scan list of labels + NodeListMap::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; + jt = j[0]; + int jtindex = Datatype::indexOf( jt.getOperator().toExpr() ); + if( jtindex==ttindex ){ + if( tpolarity ){ //we are in conflict + d_conflict = true; + break; + }else{ //it is redundant + return; } } - if( !d_conflict ){ - Debug("datatypes-labels") << "Add to labels " << t << std::endl; - lbl->push_back( t ); - const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype(); - Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << 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 - if( lbl->size()==dt.getNumConstructors()-1 ){ - std::vector< bool > pcons; - getPossibleCons( eqc, n, pcons ); - int testerIndex = -1; - for( int i=0; i<(int)pcons.size(); i++ ) { - if( pcons[i] ){ - testerIndex = i; - break; - } + } + if( !d_conflict ){ + Debug("datatypes-labels") << "Add to labels " << t << std::endl; + lbl->push_back( t ); + const Datatype& dt = ((DatatypeType)(tt[0].getType()).toType()).getDatatype(); + Debug("datatypes-labels") << "Labels at " << lbl->size() << " / " << 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 + if( lbl->size()==dt.getNumConstructors()-1 ){ + std::vector< bool > pcons; + getPossibleCons( eqc, n, pcons ); + int testerIndex = -1; + for( int i=0; i<(int)pcons.size(); i++ ) { + if( pcons[i] ){ + testerIndex = i; + break; } - Assert( testerIndex!=-1 ); - //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); - if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){ - eq_terms.push_back( (*i)[0][0] ); - if( (*i)[0][0]!=tt[0] ){ - nb << (*i)[0][0].eqNode( tt[0] ); - } + } + Assert( testerIndex!=-1 ); + //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); + if( std::find( eq_terms.begin(), eq_terms.end(), (*i)[0][0] )==eq_terms.end() ){ + eq_terms.push_back( (*i)[0][0] ); + if( (*i)[0][0]!=tt[0] ){ + nb << (*i)[0][0].eqNode( tt[0] ); } } - Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] ); - Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; - d_pending.push_back( t_concl ); - d_pending_exp[ t_concl ] = t_concl_exp; - Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; - d_infer.push_back( t_concl ); - d_infer_exp.push_back( t_concl_exp ); - return; } + Node t_concl = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[unsigned(testerIndex)].getTester() ), tt[0] ); + Node t_concl_exp = ( nb.getNumChildren() == 1 ) ? nb.getChild( 0 ) : nb; + d_pending.push_back( t_concl ); + d_pending_exp[ t_concl ] = t_concl_exp; + Trace("datatypes-infer") << "DtInfer : " << t_concl << " by " << t_concl_exp << std::endl; + d_infer.push_back( t_concl ); + d_infer_exp.push_back( t_concl_exp ); + return; } } } - if( d_conflict ){ - std::vector< TNode > assumptions; - explain( j, assumptions ); - explain( t, assumptions ); - explain( jt[0].eqNode( tt[0] ), assumptions ); - d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); + } + if( d_conflict ){ + std::vector< TNode > assumptions; + explain( j, assumptions ); + explain( t, assumptions ); + explain( jt[0].eqNode( tt[0] ), assumptions ); + d_conflictNode = mkAnd( assumptions ); + Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + } +} + +void TheoryDatatypes::addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts ) { + Debug("datatypes-debug") << "Add selector : " << s << " to eqc(" << n << ")" << std::endl; + //check to see if it is redundant + NodeListMap::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; + if( s.getOperator()==ss.getOperator() ){ + return; + } } + //add it to the vector + sel->push_back( s ); + eqc->d_selectors = true; + } + if( assertFacts && !eqc->d_constructor.get().isNull() ){ + //conclude the collapsed merge + collapseSelector( s, eqc->d_constructor.get() ); + } +} + +void TheoryDatatypes::addConstructor( Node c, EqcInfo* eqc, Node n ){ + Debug("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 ); + 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 ){ + if( Datatype::indexOf( (*i)[0].getOperator().toExpr() )==constructorIndex ){ + Node n = *i; + std::vector< TNode > assumptions; + explain( *i, assumptions ); + explain( c.eqNode( (*i)[0][0] ), assumptions ); + d_conflictNode = mkAnd( assumptions ); + Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; + } + } + } + } + //check selectors + NodeListMap::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 ){ + //collapse the selector + collapseSelector( *j, c ); + } + } + eqc->d_constructor.set( c ); +} + +void TheoryDatatypes::collapseSelector( Node s, Node c ) { + Node r = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, s.getOperator(), c ); + Node rr = Rewriter::rewrite( r ); + //if( r!=rr ){ + //Node eq_exp = NodeManager::currentNM()->mkConst(true); + //Node eq = r.getType().isBoolean() ? r.iffNode( rr ) : r.eqNode( rr ); + if( s!=rr ){ + Node eq_exp = c.eqNode( s[0] ); + Node eq = rr.getType().isBoolean() ? s.iffNode( rr ) : s.eqNode( rr ); + + + d_pending.push_back( eq ); + d_pending_exp[ eq ] = eq_exp; + Trace("datatypes-infer") << "DtInfer : " << eq << " by " << eq_exp << " (collapse selector)" << std::endl; + d_infer.push_back( eq ); + d_infer_exp.push_back( eq_exp ); } } @@ -816,12 +881,13 @@ void TheoryDatatypes::computeCareGraph(){ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ Trace("dt-model") << std::endl; printModelDebug( "dt-model" ); + Trace("dt-model") << std::endl; m->assertEqualityEngine( &d_equalityEngine ); - + Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl; +/* std::vector< TypeEnumerator > vec; std::map< TypeNode, int > tes; - Trace("dt-cmi") << "Datatypes : Collect model info " << std::endl; - + */ //get all constructors eq::EqClassesIterator eqccs_i = eq::EqClassesIterator( &d_equalityEngine ); std::vector< Node > cons; @@ -830,90 +896,139 @@ void TheoryDatatypes::collectModelInfo( TheoryModel* m, bool fullModel ){ //for all equivalence classes that are datatypes if( DatatypesRewriter::isTermDatatype( eqc ) ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei ){ - if( !ei->d_constructor.get().isNull() ){ - cons.push_back( ei->d_constructor.get() ); - } + if( !ei->d_constructor.get().isNull() ){ + cons.push_back( ei->d_constructor.get() ); } } ++eqccs_i; } //must choose proper representatives + std::vector< Node > nodes; eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); //for all equivalence classes that are datatypes if( DatatypesRewriter::isTermDatatype( eqc ) ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); - if( ei ){ - if( !ei->d_constructor.get().isNull() ){ - //specify that we should use the constructor as the representative - //m->assertRepresentative( ei->d_constructor.get() ); - }else{ - Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; - Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; - - std::vector< bool > pcons; - getPossibleCons( ei, eqc, pcons ); - Trace("dt-cmi") << "Possible constructors : "; - for( unsigned i=0; id_constructor.get().isNull() ){ + //specify that we should use the constructor as the representative + //m->assertRepresentative( ei->d_constructor.get() ); + }else{ + nodes.push_back( eqc ); + } + } + ++eqcs_i; + } + unsigned index = 0; + while( indexareEqual( cons[i][j], neqc[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; + break; + } } - Trace("dt-cmi") << std::endl; - - if( tes.find( eqc.getType() )==tes.end() ){ - tes[eqc.getType()]=vec.size(); - vec.push_back( TypeEnumerator( eqc.getType() ) ); + } + }while( !success ); + }else{ + Trace("dt-cmi") << "NOTICE : Datatypes: no constructor in equivalence class " << eqc << std::endl; + Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl; + EqcInfo* ei = getOrMakeEqcInfo( eqc ); + std::vector< bool > pcons; + getPossibleCons( ei, eqc, pcons ); + Trace("dt-cmi") << "Possible constructors : "; + for( unsigned i=0; iareEqual( cons[i][j], n[j] ) ){ + diff = true; + break; + } + } + if( !diff ){ + Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; + success = false; + break; + } + } } - bool success; - Node n; - do { - success = true; - Assert( !vec[tes[eqc.getType()]].isFinished() ); - n = *vec[tes[eqc.getType()]]; - ++vec[tes[eqc.getType()]]; - - //applyTypeAscriptions( n, eqc.getType() ); - - Trace("dt-cmi-debug") << "Try " << n << "..." << std::endl; - //check if it is consistent with labels - size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); - if( constructorIndexareEqual( cons[i][j], n[j] ) ){ - diff = true; - break; - } - } - if( !diff ){ - Trace("dt-cmi-debug") << "...Already equivalent modulo equality to " << cons[i] << std::endl; - success = false; - break; - } + }else{ + Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl; + success = false; + } + }while( !success ); + */ + const Datatype& dt = ((DatatypeType)(eqc.getType()).toType()).getDatatype(); + for( unsigned r=0; r<2; r++ ){ + if( neqc.isNull() ){ + for( unsigned i=0; iassertRepresentative( n ); - m->assertEquality( eqc, n, true ); - + } } - }else{ - Trace("model-warn") << "WARNING: Datatypes: no equivalence class info for " << eqc << std::endl; - Trace("model-warn") << " Type : " << eqc.getType() << std::endl; } } - ++eqcs_i; + Assert( !neqc.isNull() ); + Trace("dt-cmi") << "Assign : " << neqc << std::endl; + m->assertEquality( eqc, neqc, true ); + //m->assertRepresentative( neqc ); + cons.push_back( neqc ); + ++index; } + } @@ -932,24 +1047,23 @@ void TheoryDatatypes::collectTerms( Node n ) { Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl; } d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); + //Node r = getRepresentative( n[i] ); + //EqcInfo* eqc = getOrMakeEqcInfo( r, true ); + //eqc->d_selectors = true; } }else if( n.getKind() == APPLY_SELECTOR ){ - if( d_selector_apps.find( n )==d_selector_apps.end() ){ - d_selector_apps[n] = false; - //we must also record which selectors exist - Debug("datatypes") << " Found selector " << n << endl; - if (n.getType().isBoolean()) { - d_equalityEngine.addTriggerPredicate( n ); - }else{ - d_equalityEngine.addTerm( n ); - } - Node rep = getRepresentative( n[0] ); - EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); - if( !eqc->d_selectors ){ - eqc->d_selectors = true; - instantiate( eqc, rep ); - } + //we must also record which selectors exist + Debug("datatypes") << " Found selector " << n << endl; + if (n.getType().isBoolean()) { + d_equalityEngine.addTriggerPredicate( n ); + }else{ + d_equalityEngine.addTerm( n ); } + Node rep = getRepresentative( n[0] ); + //record it in the selectors + EqcInfo* eqc = getOrMakeEqcInfo( rep, true ); + //add it to the eqc info + addSelector( n, eqc, rep ); } } } @@ -967,20 +1081,35 @@ void TheoryDatatypes::processNewTerm( Node n ){ } } -Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index ){ +Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar, bool isActive ){ //if( !d_inst_map[n][index].isNull() ){ // return d_inst_map[n][index]; //}else{ //add constructor to equivalence class + Type tspec; + if( dt.isParametric() ){ + tspec = dt[index].getSpecializedConstructorType(n.getType().toType()); + } std::vector< Node > children; children.push_back( Node::fromExpr( dt[index].getConstructor() ) ); for( int i=0; i<(int)dt[index].getNumArgs(); i++ ){ Node nc = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, Node::fromExpr( dt[index][i].getSelector() ), n ); + if( mkVar ){ + TypeNode tn = nc.getType(); + if( dt.isParametric() ){ + tn = TypeNode::fromType( tspec )[i]; + } + nc = NodeManager::currentNM()->mkSkolem( "m_$$", tn, "created during model gen" ); + } children.push_back( nc ); - processNewTerm( nc ); + if( isActive ){ + processNewTerm( nc ); + } } Node n_ic = NodeManager::currentNM()->mkNode( APPLY_CONSTRUCTOR, children ); - collectTerms( n_ic ); + if( isActive ){ + collectTerms( n_ic ); + } //add type ascription for ambiguous constructor types if(!n_ic.getType().isComparableTo(n.getType())) { Assert( dt.isParametric() ); @@ -994,72 +1123,11 @@ Node TheoryDatatypes::getInstantiateCons( Node n, const Datatype& dt, int index Assert( n_ic.getType()==n.getType() ); } n_ic = Rewriter::rewrite( n_ic ); + Debug("dt-enum") << "Made instantiate cons " << n_ic << std::endl; //d_inst_map[n][index] = n_ic; return n_ic; //} } -/* -Node TheoryDatatypes::applyTypeAscriptions( Node n, TypeNode tn ){ - Debug("dt-ta-debug") << "Apply type ascriptions " << n << " " << tn << std::endl; - if( n.getKind()==APPLY_CONSTRUCTOR ){ - //add type ascription for ambiguous constructor types - if(!n.getType().isComparableTo(tn)) { - size_t constructorIndex = Datatype::indexOf(n.getOperator().toExpr()); - const Datatype& dt = ((DatatypeType)(tn).toType()).getDatatype(); - Assert( dt.isParametric() ); - Debug("dt-ta-debug") << "Ambiguous type for " << n << ", ascribe to " << tn << std::endl; - Debug("dt-ta-debug") << "Constructor is " << dt[constructorIndex] << std::endl; - Type tspec = dt[constructorIndex].getSpecializedConstructorType(tn.toType()); - Debug("dt-ta-debug") << "Type specification is " << tspec << std::endl; - Node op = NodeManager::currentNM()->mkNode(kind::APPLY_TYPE_ASCRIPTION, - NodeManager::currentNM()->mkConst(AscriptionType(tspec)), n.getOperator() ); - std::vector< Node > children; - children.push_back( op ); - for( unsigned i=0; imkNode( APPLY_CONSTRUCTOR, children ) ); - Assert( n.getType()==tn ); - return n; - } - }else{ - if( n.getType()!=tn ){ - Debug("dt-ta-debug") << "Bad type : " << n.getType() << std::endl; - } - } - return n; -} -*/ -void TheoryDatatypes::collapseSelectors(){ - //must check incorrect applications of selectors - for( BoolMap::iterator it = d_selector_apps.begin(); it != d_selector_apps.end(); ++it ){ - if( !(*it).second ){ - Node n = getRepresentative( (*it).first[0] ); - Trace("datatypes-collapse") << "Datatypes collapse selector? : " << n << std::endl; - EqcInfo* ei = getOrMakeEqcInfo( n, true ); - if( ei ){ - if( !ei->d_constructor.get().isNull() ){ - Node op = (*it).first.getOperator(); - Node cons = ei->d_constructor; - Node sn = NodeManager::currentNM()->mkNode( kind::APPLY_SELECTOR, op, cons ); - Node s = Rewriter::rewrite( sn ); - if( sn!=s ){ - Node eq = s.getType().isBoolean() ? s.iffNode( sn ) : s.eqNode( sn ); - d_pending.push_back( eq ); - d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); - Trace("datatypes-infer") << "DtInfer : " << eq << ", by rewrite" << std::endl; - d_infer.push_back( eq ); - } - d_selector_apps[ (*it).first ] = true; - }else{ - Trace("datatypes-collapse") << "No constructor." << std::endl; - } - }else{ - Trace("datatypes-collapse") << "No e info." << std::endl; - } - } - } -} void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ //add constructor to equivalence class if not done so already @@ -1103,7 +1171,7 @@ void TheoryDatatypes::checkCycles() { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - if( eqc.getType().isDatatype() ) { + if( DatatypesRewriter::isTermDatatype( eqc ) ) { map< Node, bool > visited; std::vector< TNode > expl; Node cn = searchForCycle( eqc, eqc, visited, expl ); @@ -1118,11 +1186,7 @@ void TheoryDatatypes::checkCycles() { if( !cn.isNull() ) { Assert( expl.size()>0 ); - if( expl.size() == 1 ){ - d_conflictNode = expl[ 0 ]; - }else{ - d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl ); - } + d_conflictNode = mkAnd( expl ); Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; @@ -1290,30 +1354,45 @@ void TheoryDatatypes::printModelDebug( const char* c ){ EqcInfo* ei = getOrMakeEqcInfo( eqc ); if( ei ){ Trace( c ) << " Instantiated : " << ei->d_inst.get() << std::endl; - if( ei->d_constructor.get().isNull() ){ - Trace("debug-model-warn") << eqc << " has no constructor in equivalence class!" << std::endl; - Trace("debug-model-warn") << " Type : " << eqc.getType() << std::endl; - Trace( c ) << " Constructor : " << std::endl; - Trace( c ) << " Labels : "; - if( hasLabel( ei, eqc ) ){ - Trace( c ) << getLabel( eqc ); - }else{ - NodeListMap::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 << " "; - } + Trace( c ) << " Constructor : "; + if( !ei->d_constructor.get().isNull() ){ + Trace( c )<< ei->d_constructor.get(); + } + Trace( c ) << std::endl << " Labels : "; + if( hasLabel( ei, eqc ) ){ + Trace( c ) << getLabel( eqc ); + }else{ + NodeListMap::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 << " "; } } - Trace( c ) << std::endl; - }else{ - Trace( c ) << " Constructor : " << ei->d_constructor.get() << std::endl; } - Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes" : "no" ) << std::endl; + Trace( c ) << std::endl; + Trace( c ) << " Selectors : " << ( ei->d_selectors ? "yes, " : "no " ); + 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++ ){ + Trace( c ) << *j << " "; + } + } + Trace( c ) << std::endl; } } } ++eqcs_i; } } + +Node TheoryDatatypes::mkAnd( std::vector< TNode >& assumptions ) { + if( assumptions.empty() ){ + return NodeManager::currentNM()->mkConst( true ); + }else if( assumptions.size()==1 ){ + return assumptions[0]; + }else{ + return NodeManager::currentNM()->mkNode( AND, assumptions ); + } +} \ No newline at end of file diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 225139b2d..4f061507c 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -51,6 +51,8 @@ private: NodeList d_infer; NodeList d_infer_exp; + /** mkAnd */ + Node mkAnd( std::vector< TNode >& assumptions ); private: //notification class for equality engine class NotifyClass : public eq::EqualityEngineNotify { @@ -137,7 +139,7 @@ private: /** information necessary for equivalence classes */ std::map< Node, EqcInfo* > d_eqc_info; /** selector applications */ - BoolMap d_selector_apps; + //BoolMap d_selector_apps; /** map from nodes to their instantiated equivalent for each constructor type */ std::map< Node, std::map< int, Node > > d_inst_map; /** which instantiation lemmas we have sent */ @@ -152,6 +154,8 @@ private: * is_[constructor_(n+1)]( t ), each of which is a unique tester. */ NodeListMap d_labels; + /** selector apps for eqch equivalence class */ + NodeListMap d_selector_apps; /** Are we in conflict */ context::CDO d_conflict; /** The conflict node */ @@ -215,8 +219,14 @@ public: private: /** add tester to equivalence class info */ void addTester( Node t, EqcInfo* eqc, Node n ); + /** add selector to equivalence class info */ + void addSelector( Node s, EqcInfo* eqc, Node n, bool assertFacts = true ); + /** add constructor */ + void addConstructor( Node c, EqcInfo* eqc, Node n ); /** merge the equivalence class info of t1 and t2 */ void merge( Node t1, Node t2 ); + /** collapse selector, s is of the form sel( n ) where n = c */ + void collapseSelector( Node s, Node c ); /** for checking if cycles exist */ void checkCycles(); Node searchForCycle( Node n, Node on, @@ -225,15 +235,11 @@ private: /** collect terms */ void collectTerms( Node n ); /** get instantiate cons */ - Node getInstantiateCons( Node n, const Datatype& dt, int index ); - /** apply type ascriptions */ - //Node applyTypeAscriptions( Node n, TypeNode tn ); + Node getInstantiateCons( Node n, const Datatype& dt, int index, bool mkVar = false, bool isActive = true ); /** process new term that was created internally */ void processNewTerm( Node n ); /** check instantiate */ void instantiate( EqcInfo* eqc, Node n ); - /** collapse selectors */ - void collapseSelectors(); /** must specify model * This returns true when the datatypes theory is expected to specify the constructor * type for all equivalence classes. -- 2.30.2