From: Andrew Reynolds Date: Tue, 8 Oct 2013 14:01:13 +0000 (-0500) Subject: Optimizations for datatypes theory. There seems to be a bug in trans_closure, curren... X-Git-Tag: cvc5-1.0.0~7275^2~28 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=59c96a073e34f51b415863ece51c3242c953acc4;p=cvc5.git Optimizations for datatypes theory. There seems to be a bug in trans_closure, currently implemented a work around. --- diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index c827a8f07..fb0ac5923 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -118,6 +118,12 @@ void TheoryDatatypes::check(Effort e) { } if( e == EFFORT_FULL ) { + //check for cycles + checkCycles(); + if( d_conflict ){ + return; + } + //check for splits Debug("datatypes-split") << "Check for splits " << e << endl; bool addedFact = false; do { @@ -159,20 +165,19 @@ void TheoryDatatypes::check(Effort e) { } } } + /* if( !needSplit && mustSpecifyAssignment() ){ - // && //for the sake of termination, we must choose the constructor of a ground term //NEED GUARENTEE: groundTerm should not contain any subterms of the same type - //** TODO: this is probably not good enough, actually need fair enumeration strategy - /* + // TODO: this is probably not good enough, actually need fair enumeration strategy Node groundTerm = n.getType().mkGroundTerm(); int index = Datatype::indexOf( groundTerm.getOperator().toExpr() ); if( pcons[index] ){ consIndex = index; } needSplit = true; - */ } + */ if( needSplit && consIndex!=-1 ) { Node test = NodeManager::currentNM()->mkNode( APPLY_TESTER, Node::fromExpr( dt[consIndex].getTester() ), n ); Trace("dt-split") << "*************Split for possible constructor " << dt[consIndex] << " for " << n << endl; @@ -446,10 +451,16 @@ void TheoryDatatypes::explain(TNode literal, std::vector& assumptions){ Debug("datatypes-explain") << "Explain " << literal << std::endl; bool polarity = literal.getKind() != kind::NOT; TNode atom = polarity ? literal : literal[0]; + std::vector tassumptions; if (atom.getKind() == kind::EQUAL || atom.getKind() == kind::IFF) { - d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions); + d_equalityEngine.explainEquality(atom[0], atom[1], polarity, tassumptions); } else { - d_equalityEngine.explainPredicate(atom, polarity, assumptions); + d_equalityEngine.explainPredicate(atom, polarity, tassumptions); + } + for( unsigned i=0; iconflict( d_conflictNode ); d_conflict = true; } @@ -523,7 +534,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ if( cons1.getOperator()!=cons2.getOperator() ){ //check for clash d_conflictNode = explain( cons1.eqNode( cons2 ) ); - Debug("datatypes-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Clash conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; return; @@ -559,8 +570,7 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ explain( *i, assumptions ); explain( cons2.eqNode( (*i)[0][0] ), assumptions ); d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Debug("datatypes-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; - Debug("datatypes-conflict-temp") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Tester merge eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); d_conflict = true; return; @@ -615,12 +625,16 @@ void TheoryDatatypes::merge( Node t1, Node t2 ){ newRep = trep2; } bool result = d_cycle_check.addEdgeNode( oldRep, newRep ); - d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); - Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << d_hasSeenCycle.get() << endl; - if( d_hasSeenCycle.get() ){ + //d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); + Debug("datatypes-cycles") << "DtCyc: Equal " << oldRep << " -> " << newRep << " " << result << " " << d_hasSeenCycle.get() << endl; + if( result ){ checkCycles(); if( d_conflict ){ + Debug("datatypes-cycles-find") << "Cycle found." << std::endl; return; + }else{ + Debug("datatypes-cycles-find") << "WARNING : no cycle found." << std::endl; + d_cycle_check.debugPrint(); } } } @@ -694,7 +708,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ explain( t, assumptions ); explain( eqc->d_constructor.get().eqNode( tt[0] ), assumptions ); d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Debug("datatypes-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Tester eq conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); return; }else{ @@ -775,7 +789,7 @@ void TheoryDatatypes::addTester( Node t, EqcInfo* eqc, Node n ){ explain( t, assumptions ); explain( jt[0].eqNode( tt[0] ), assumptions ); d_conflictNode = NodeManager::currentNM()->mkNode( AND, assumptions ); - Debug("datatypes-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; + Trace("dt-conflict") << "CONFLICT: Tester conflict : " << d_conflictNode << std::endl; d_out->conflict( d_conflictNode ); } } @@ -912,8 +926,11 @@ void TheoryDatatypes::collectTerms( Node n ) { if( n.getKind() == APPLY_CONSTRUCTOR ){ //we must take into account subterm relation when checking for cycles for( int i=0; i<(int)n.getNumChildren(); i++ ) { - Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << endl; bool result = d_cycle_check.addEdgeNode( n, n[i] ); + Debug("datatypes-cycles") << "DtCyc: Subterm " << n << " -> " << n[i] << " " << result << endl; + if( result && !d_hasSeenCycle.get() ){ + Debug("datatypes-cycles") << "FOUND CYCLE" << std::endl; + } d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); } }else if( n.getKind() == APPLY_SELECTOR ){ @@ -941,7 +958,7 @@ void TheoryDatatypes::processNewTerm( Node n ){ Trace("dt-terms") << "Created term : " << n << std::endl; //see if it is rewritten to be something different Node rn = Rewriter::rewrite( n ); - if( rn!=n ){ + if( rn!=n && !areEqual( rn, n ) ){ Node eq = n.getType().isBoolean() ? rn.iffNode( n ) : rn.eqNode( n ); d_pending.push_back( eq ); d_pending_exp[ eq ] = NodeManager::currentNM()->mkConst( true ); @@ -1059,21 +1076,21 @@ void TheoryDatatypes::instantiate( EqcInfo* eqc, Node n ){ int index = getLabelIndex( eqc, n ); const Datatype& dt = ((DatatypeType)(tt.getType()).toType()).getDatatype(); //must be finite or have a selector - //if( eqc->d_selectors || dt[ index ].isFinite() || mustSpecifyAssignment() ){ - //instantiate this equivalence class - eqc->d_inst = true; - Node tt_cons = getInstantiateCons( tt, dt, index ); - Node eq; - if( tt!=tt_cons ){ - eq = tt.eqNode( tt_cons ); - Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; - d_pending.push_back( eq ); - d_pending_exp[ eq ] = exp; - Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; - //eqc->d_inst.set( eq ); - d_infer.push_back( eq ); - d_infer_exp.push_back( exp ); - } + //if( eqc->d_selectors || dt[ index ].isFinite() ){ // || mustSpecifyAssignment() + //instantiate this equivalence class + eqc->d_inst = true; + Node tt_cons = getInstantiateCons( tt, dt, index ); + Node eq; + if( tt!=tt_cons ){ + eq = tt.eqNode( tt_cons ); + Debug("datatypes-inst") << "DtInstantiate : " << eqc << " " << eq << std::endl; + d_pending.push_back( eq ); + d_pending_exp[ eq ] = exp; + Trace("datatypes-infer") << "DtInfer : " << eq << " by " << exp << std::endl; + //eqc->d_inst.set( eq ); + d_infer.push_back( eq ); + d_infer_exp.push_back( exp ); + } //} //else{ // Debug("datatypes-inst") << "Do not instantiate" << std::endl; @@ -1086,26 +1103,38 @@ void TheoryDatatypes::checkCycles() { eq::EqClassesIterator eqcs_i = eq::EqClassesIterator( &d_equalityEngine ); while( !eqcs_i.isFinished() ){ Node eqc = (*eqcs_i); - map< Node, bool > visited; - std::vector< TNode > expl; - if( searchForCycle( eqc, eqc, visited, expl ) ) { - Assert( expl.size()>0 ); - if( expl.size() == 1 ){ - d_conflictNode = expl[ 0 ]; - }else{ - d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl ); + if( eqc.getType().isDatatype() ) { + map< Node, bool > visited; + std::vector< TNode > expl; + Node cn = searchForCycle( eqc, eqc, visited, expl ); + //if we discovered a different cycle while searching this one + if( !cn.isNull() && cn!=eqc ){ + visited.clear(); + expl.clear(); + Node prev = cn; + cn = searchForCycle( cn, cn, visited, expl ); + Assert( prev==cn ); + } + + if( !cn.isNull() ) { + Assert( expl.size()>0 ); + if( expl.size() == 1 ){ + d_conflictNode = expl[ 0 ]; + }else{ + d_conflictNode = NodeManager::currentNM()->mkNode( AND, expl ); + } + Trace("dt-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; + d_out->conflict( d_conflictNode ); + d_conflict = true; + return; } - Debug("datatypes-conflict") << "CONFLICT: Cycle conflict : " << d_conflictNode << std::endl; - d_out->conflict( d_conflictNode ); - d_conflict = true; - return; } ++eqcs_i; } } //postcondition: if cycle detected, explanation is why n is a subterm of on -bool TheoryDatatypes::searchForCycle( Node n, Node on, +Node TheoryDatatypes::searchForCycle( Node n, Node on, map< Node, bool >& visited, std::vector< TNode >& explanation, bool firstTime ) { Debug("datatypes-cycle-check") << "Search for cycle " << n << " " << on << endl; @@ -1116,19 +1145,20 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, if( nn==on ){ Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, nn ); explain( lit, explanation ); - return true; + return on; } }else{ nn = n; } if( visited.find( nn ) == visited.end() ) { visited[nn] = true; - EqcInfo* eqc = getOrMakeEqcInfo( nn ); + EqcInfo* eqc = getOrMakeEqcInfo( nn, false ); if( eqc ){ Node ncons = eqc->d_constructor.get(); if( !ncons.isNull() ) { for( int i=0; i<(int)ncons.getNumChildren(); i++ ) { - if( searchForCycle( ncons[i], on, visited, explanation, false ) ) { + Node cn = searchForCycle( ncons[i], on, visited, explanation, false ); + if( cn==on ) { if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, ncons[i] ) ){ Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << ncons[i] << "!!!!" << std::endl; } @@ -1137,13 +1167,18 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, Node lit = NodeManager::currentNM()->mkNode( EQUAL, n, ncons ); explain( lit, explanation ); } - return true; + return on; + }else if( !cn.isNull() ){ + return cn; } } } } + visited.erase( nn ); + return Node::null(); + }else{ + return nn; } - return false; } bool TheoryDatatypes::mustSpecifyAssignment(){ diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 203782a79..225139b2d 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -219,7 +219,7 @@ private: void merge( Node t1, Node t2 ); /** for checking if cycles exist */ void checkCycles(); - bool searchForCycle( Node n, Node on, + Node searchForCycle( Node n, Node on, std::map< Node, bool >& visited, std::vector< TNode >& explanation, bool firstTime = true ); /** collect terms */ diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 96e8692f5..8db91da69 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -107,6 +107,7 @@ void Datatype::resolve(ExprManager* em, Node::fromExpr((*i).d_tester).setAttribute(DatatypeIndexAttr(), index++); } d_self = self; + //d_card = getCardinality(); } void Datatype::addConstructor(const DatatypeConstructor& c) { @@ -125,6 +126,10 @@ Cardinality Datatype::getCardinality() const throw(IllegalArgumentException) { for(const_iterator i = begin(), i_end = end(); i != i_end; ++i) { c += (*i).getCardinality(); } + //if( d_card!=c ){ + //std::cout << "Bad card " << std::endl; + //} + return c; } diff --git a/src/util/datatype.h b/src/util/datatype.h index c46c10c97..01558fd30 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -404,6 +404,7 @@ private: std::vector d_constructors; bool d_resolved; Type d_self; + Cardinality d_card; /** * Datatypes refer to themselves, recursively, and we have a @@ -616,7 +617,8 @@ inline Datatype::Datatype(std::string name) : d_params(), d_constructors(), d_resolved(false), - d_self() { + d_self(), + d_card(1) { } inline Datatype::Datatype(std::string name, const std::vector& params) : @@ -624,7 +626,8 @@ inline Datatype::Datatype(std::string name, const std::vector& params) : d_params(params), d_constructors(), d_resolved(false), - d_self() { + d_self(), + d_card(1) { } inline std::string Datatype::getName() const throw() { diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 90b069485..970d2542e 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -37,16 +37,22 @@ TransitiveClosure::~TransitiveClosure() { bool TransitiveClosure::addEdge(unsigned i, unsigned j) { + Debug("trans-closure") << "Add edge " << i << " -> " << j << std::endl; // Check for loops Assert(i != j, "Cannot add self-loop"); - if (adjMatrix.size() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) { + if (adjIndex.get() > j && adjMatrix[j] != NULL && adjMatrix[j]->read(i)) { return true; } // Grow matrix if necessary unsigned maxSize = ((i > j) ? i : j) + 1; - while (maxSize > adjMatrix.size()) { - adjMatrix.push_back(NULL); + while (maxSize > adjIndex.get()) { + if( maxSize > adjMatrix.size() ){ + adjMatrix.push_back(NULL); + }else if( adjMatrix[adjIndex.get()]!=NULL ){ + adjMatrix[adjIndex.get()]->clear(); + } + adjIndex.set( adjIndex.get() + 1 ); } // Add edge from i to j and everything j can reach @@ -60,7 +66,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j) // Add edges from everything that can reach i to j and everything that j can reach unsigned k; - for (k = 0; k < adjMatrix.size(); ++k) { + for (k = 0; k < adjIndex.get(); ++k) { if (adjMatrix[k] != NULL && adjMatrix[k]->read(i)) { adjMatrix[k]->write(j); if (adjMatrix[j] != NULL) { @@ -74,7 +80,7 @@ bool TransitiveClosure::addEdge(unsigned i, unsigned j) bool TransitiveClosure::isConnected(unsigned i, unsigned j) { - if( i>=adjMatrix.size() || j>adjMatrix.size() ){ + if( i>=adjIndex.get() || j>adjIndex.get() ){//adjMatrix.size() ){ return false; }else{ return adjMatrix[i] != NULL && adjMatrix[i]->read(j); @@ -84,15 +90,15 @@ bool TransitiveClosure::isConnected(unsigned i, unsigned j) void TransitiveClosure::debugPrintMatrix() { unsigned i,j; - for (i = 0; i < adjMatrix.size(); ++i) { - for (j = 0; j < adjMatrix.size(); ++j) { + for (i = 0; i < adjIndex.get(); ++i) { + for (j = 0; j < adjIndex.get(); ++j) { if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) { Debug("trans-closure") << "1 "; } else Debug("trans-closure") << "0 "; } Debug("trans-closure") << endl; - } + } } unsigned TransitiveClosureNode::getId( Node i ){ @@ -108,10 +114,14 @@ unsigned TransitiveClosureNode::getId( Node i ){ void TransitiveClosureNode::debugPrint(){ for( int i=0; i<(int)currEdges.size(); i++ ){ - Debug("trans-closure") << "currEdges[ " << i << " ] = " + Debug("trans-closure") << "currEdges[ " << i << " ] = " << currEdges[i].first << " -> " << currEdges[i].second; + int id1 = getId( currEdges[i].first ); + int id2 = getId( currEdges[i].second ); + Debug("trans-closure") << " { " << id1 << " -> " << id2 << " } "; Debug("trans-closure") << std::endl; } + debugPrintMatrix(); } diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index ce846637d..14e7ab95f 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -57,17 +57,17 @@ protected: CDBV* next() { return d_next; } public: - CDBV(context::Context* context) : + CDBV(context::Context* context) : ContextObj(context), d_data(0), d_next(NULL) {} - ~CDBV() { + ~CDBV() { if (d_next != NULL) { d_next->deleteSelf(); } destroy(); } - + void clear() { d_data = 0; if( d_next ) d_next->clear(); } bool read(unsigned index) { if (index < 64) return (d_data & (uint64_t(1) << index)) != 0; else if (d_next == NULL) return false; @@ -88,7 +88,7 @@ public: makeCurrent(); d_next = new(true) CDBV(getContext()); d_next->write(index - 64); - } + } } void merge(CDBV* pcdbv) { @@ -108,9 +108,10 @@ public: class TransitiveClosure { context::Context* d_context; std::vector adjMatrix; + context::CDO adjIndex; public: - TransitiveClosure(context::Context* context) : d_context(context) {} + TransitiveClosure(context::Context* context) : d_context(context), adjIndex(context,0) {} virtual ~TransitiveClosure(); /* Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */ @@ -130,7 +131,7 @@ class TransitiveClosureNode : public TransitiveClosure{ //for debugging context::CDList< std::pair< Node, Node > > currEdges; public: - TransitiveClosureNode(context::Context* context) : + TransitiveClosureNode(context::Context* context) : TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {} ~TransitiveClosureNode(){}