summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/smt/model_postprocessor.cpp7
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp663
-rw-r--r--src/theory/datatypes/theory_datatypes.h18
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<TNode>(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<TNode>& 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; i<pcons.size(); i++ ){
- Trace("dt-cmi") << pcons[i] << " ";
+ if( !ei->d_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( index<nodes.size() ){
+ Node eqc = nodes[index];
+ Node neqc;
+ if( !d_equalityEngine.hasTerm( eqc ) ){
+ Trace("dt-cmi") << "NOTICE : Datatypes: need to assign constructor for " << eqc << std::endl;
+ Trace("dt-cmi") << " Type : " << eqc.getType() << std::endl;
+ //can assign arbitrary term
+ TypeEnumerator te(eqc.getType());
+ bool success;
+ do{
+ success = true;
+ Assert( !te.isFinished() );
+ neqc = *te;
+ Trace("dt-cmi-debug") << "Try " << neqc << " ... " << std::endl;
+ ++te;
+ for( unsigned i=0; i<cons.size(); i++ ){
+ //check if it is modulo equality the same
+ if( cons[i].getOperator()==neqc.getOperator() ){
+ bool diff = false;
+ for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
+ if( !m->areEqual( 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; i<pcons.size(); i++ ){
+ Trace("dt-cmi") << pcons[i] << " ";
+ }
+ Trace("dt-cmi") << std::endl;
+ /*
+ if( tes.find( eqc.getType() )==tes.end() ){
+ tes[eqc.getType()]=vec.size();
+ vec.push_back( TypeEnumerator( eqc.getType() ) );
+ }
+ bool success;
+ Node n;
+ do {
+ success = true;
+ Assert( !vec[tes[eqc.getType()]].isFinished() );
+ n = *vec[tes[eqc.getType()]];
+ ++vec[tes[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( constructorIndex<pcons.size() && pcons[constructorIndex] ){
+ for( unsigned i=0; i<cons.size(); i++ ){
+ //check if it is modulo equality the same
+ if( cons[i].getOperator()==n.getOperator() ){
+ bool diff = false;
+ for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
+ if( !m->areEqual( 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( constructorIndex<pcons.size() && pcons[constructorIndex] ){
- for( unsigned i=0; i<cons.size(); i++ ){
- //check if it is modulo equality the same
- if( cons[i].getOperator()==n.getOperator() ){
- bool diff = false;
- for( unsigned j=0; j<cons[i].getNumChildren(); j++ ){
- if( !m->areEqual( 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; i<pcons.size(); i++ ){
+ if( pcons[i] && (r==1)==dt[ i ].isFinite() ){
+ neqc = getInstantiateCons( eqc, dt, i, false, false );
+ for( unsigned j=0; j<neqc.getNumChildren(); j++ ){
+ if( !d_equalityEngine.hasTerm( neqc[j] ) && DatatypesRewriter::isTermDatatype( neqc[j] ) ){
+ nodes.push_back( neqc[j] );
}
}
- }else{
- Trace("dt-cmi-debug") << "...Not consistent with labels" << std::endl;
- success = false;
+ break;
}
- }while( !success );
- Trace("dt-cmi") << "Assign : " << n << std::endl;
- //m->assertRepresentative( 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; i<n.getNumChildren(); i++ ){
- children.push_back( applyTypeAscriptions( n[i], TypeNode::fromType( tspec )[i] ) );
- }
- n = Rewriter::rewrite( NodeManager::currentNM()->mkNode( 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<bool> 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.
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback