From: Andrew Reynolds Date: Mon, 2 May 2011 21:40:06 +0000 (+0000) Subject: minor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure modul... X-Git-Tag: cvc5-1.0.0~8559 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f04cbfc62ae22d00b1a37af29f86258a902770e4;p=cvc5.git minor updates to exp manager, fixed 32bit vs 64bit issues in transitive closure module, theory datatypes now uses transitive closure for cycle detection, bug 261 fixed --- diff --git a/src/theory/datatypes/explanation_manager.cpp b/src/theory/datatypes/explanation_manager.cpp index 424ca8fac..3594037a6 100644 --- a/src/theory/datatypes/explanation_manager.cpp +++ b/src/theory/datatypes/explanation_manager.cpp @@ -9,6 +9,7 @@ using namespace CVC4::theory::datatypes; void ProofManager::setExplanation( Node n, Node jn, unsigned r ) { + Assert( n!=jn ); d_exp[n] = std::pair< Node, unsigned >( jn, r ); } @@ -35,7 +36,7 @@ void ExplanationManager::process( Node n, NodeBuilder<>& nb, ProofManager* pm ) if( r.d_e ){ Debug("emanager") << "Em::process: Consult externally for " << n << std::endl; exp = r.d_e->explain( n, pm ); - //trivial case, r says that n is an input + //trivial case, explainer says that n is an input if( exp==n ){ r.d_isInput = true; } diff --git a/src/theory/datatypes/explanation_manager.h b/src/theory/datatypes/explanation_manager.h index d16f48b01..aaf0e06e9 100644 --- a/src/theory/datatypes/explanation_manager.h +++ b/src/theory/datatypes/explanation_manager.h @@ -111,10 +111,10 @@ public: application or rule ri, i.e. applying proof rule ri to jni derives ni. - If pm->getEffort() = STANDARD, then for each ( ni, jni, ri ), jni is the (at least informal) justification for ni. - - Return value should be a conjunction of nodes n'1...n'k, where each n'i occurs + - Return value should be a (possibly empty) conjunction of nodes n'1...n'k, where each n'i occurs (as a conjunct) in jn1...jnk, but not in n1...nk. - For each of these literals n'i, assert( n'i ) was called previously, - - either pm->setExplanation( n, ... ) is called, or n is the return value + For each of these literals n'i, assert( n'i ) was called. + - either pm->setExplanation( n, ... ) is called, or n is the return value. */ virtual Node explain( Node n, ProofManager* pm ) = 0; }; @@ -179,7 +179,7 @@ public: bool hasNode( Node n ) { return d_drv_map.find( n )!=d_drv_map.end(); } /** n is explained */ bool hasConflict() { return d_hasConflict.get() || hasNode( NodeManager::currentNM()->mkConst(false) ); } - /** jn is why n is true, by reason r */ + /** jn is why n is true, by rule r */ void addNode( Node n, Node jn, unsigned r = 0 ) { if( !hasNode( n ) ){ Assert( n!=jn ); diff --git a/src/theory/datatypes/theory_datatypes.cpp b/src/theory/datatypes/theory_datatypes.cpp index 1c901f38e..7b5319267 100644 --- a/src/theory/datatypes/theory_datatypes.cpp +++ b/src/theory/datatypes/theory_datatypes.cpp @@ -25,8 +25,6 @@ #include -//#define USE_TRANSITIVE_CLOSURE - using namespace std; using namespace CVC4; using namespace CVC4::kind; @@ -78,8 +76,8 @@ TheoryDatatypes::TheoryDatatypes(Context* c, OutputChannel& out, Valuation valua ////bug test for transitive closure //TransitiveClosure tc( c ); - //Debug("datatypes-tc") << "1 -> 0 : " << tc.addEdge( 1, 0 ) << std::endl; - //Debug("datatypes-tc") << "32 -> 1 : " << tc.addEdge( 32, 1 ) << std::endl; + //Debug("datatypes-tc") << "33 -> 32 : " << tc.addEdge( 33, 32 ) << std::endl; + //Debug("datatypes-tc") << "32 -> 33 : " << tc.addEdge( 32, 33 ) << std::endl; //tc.debugPrintMatrix(); } @@ -206,6 +204,7 @@ void TheoryDatatypes::check(Effort e) { d_inCheck = false; if( hasConflict() ) { Debug("datatypes-conflict") << "Constructing conflict..." << endl; + Debug("datatypes-conflict") << d_cc << std::endl; Node conflict = d_em.getConflict(); if( Debug.isOn("datatypes") || Debug.isOn("datatypes-split") || Debug.isOn("datatypes-cycles") || Debug.isOn("datatypes-conflict") ){ @@ -215,6 +214,7 @@ void TheoryDatatypes::check(Effort e) { // conflict = NodeManager::currentNM()->mkNode(kind::AND, conflict, conflict); //} d_out->conflict( conflict, false ); + //Assert( false ); return; } } @@ -406,7 +406,7 @@ void TheoryDatatypes::addTester( Node assertion ){ if( hasConflict() ) { return; } - //test all selectors whose arguments are in the equivalence class of tRep + //update all selectors whose arguments are in the equivalence class of tRep updateSelectors( tRep ); } }else if( !conflict.isNull() ){ @@ -517,7 +517,7 @@ void TheoryDatatypes::merge(TNode a, TNode b) { if( a == b) { return; } - Debug("datatypes-cycles") << "Merge "<< a << " " << b << endl; + Debug("datatypes") << "Merge "<< a << " " << b << endl; // make "a" the one with shorter diseqList EqLists::iterator deq_ia = d_disequalities.find(a); @@ -568,10 +568,10 @@ void TheoryDatatypes::merge(TNode a, TNode b) { d_unionFind.setCanon(a, b); d_reps[a] = false; d_reps[b] = true; -#ifdef USE_TRANSITIVE_CLOSURE + //add this to the transitive closure module bool result = d_cycle_check.addEdgeNode( a, b ); d_hasSeenCycle.set( d_hasSeenCycle.get() || result ); -#endif + //merge equivalence classes initializeEqClass( a ); @@ -647,30 +647,23 @@ void TheoryDatatypes::merge(TNode a, TNode b) { } } - //Debug("datatypes-debug") << "Done clash" << endl; -#ifdef USE_TRANSITIVE_CLOSURE Debug("datatypes-cycles") << "Equal " << a << " -> " << b << " " << d_hasSeenCycle.get() << endl; if( d_hasSeenCycle.get() ){ checkCycles(); if( hasConflict() ){ return; } - }else{ - checkCycles(); - if( hasConflict() ){ - for( int i=0; i<(int)d_currEqualities.size(); i++ ) { - Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; - } - d_cycle_check.debugPrint(); - Assert( false ); - } - } -#else - checkCycles(); - if( hasConflict() ){ - return; } -#endif + //else{ + // checkCycles(); + // if( hasConflict() ){ + // for( int i=0; i<(int)d_currEqualities.size(); i++ ) { + // Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; + // } + // d_cycle_check.debugPrint(); + // Assert( false ); + // } + //} Debug("datatypes-debug") << "Done cycles" << endl; //merge selector lists @@ -814,6 +807,7 @@ void TheoryDatatypes::updateSelectors( Node a ) { if( b != s[0] ) { Node t = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, s.getOperator(), b ); d_cc.addTerm( t ); + collectTerms( t ); } s = collapseSelector( s ); if( hasConflict() ) { @@ -866,52 +860,45 @@ void TheoryDatatypes::collectTerms( Node n ) { collectTerms( n[i] ); } if( n.getKind() == APPLY_CONSTRUCTOR ){ -#ifdef USE_TRANSITIVE_CLOSURE for( int i=0; i<(int)n.getNumChildren(); i++ ) { Debug("datatypes-cycles") << "Subterm " << n << " -> " << n[i] << endl; bool result = d_cycle_check.addEdgeNode( n, n[i] ); - //if( result ){ - // for( int i=0; i<(int)d_currEqualities.size(); i++ ) { - // Debug("datatypes-cycles") << "currEqualities[" << i << "] = " << d_currEqualities[i] << endl; - // } - // d_cycle_check.debugPrint(); - //} Assert( !result ); //this should not create any new cycles (relevant terms should have been recorded before) } -#endif - } - if( n.getKind() == APPLY_SELECTOR ) { - if( d_selectors.find( n ) == d_selectors.end() ) { - Debug("datatypes") << " Found selector " << n << endl; - d_selectors[ n ] = true; - d_cc.addTerm( n ); - Node tmp = find( n[0] ); - checkInstantiate( tmp ); - - Node s = n; - if( tmp != n[0] ) { - s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, n.getOperator(), tmp ); - } - s = collapseSelector( s ); - if( s.getKind() == APPLY_SELECTOR ) { - //add selector to selector eq list - Debug("datatypes") << " Add selector to list " << tmp << " " << n << endl; - EqListsN::iterator sel_i = d_selector_eq.find( tmp ); - EqListN* sel; - if( sel_i == d_selector_eq.end() ) { - sel = new(getContext()->getCMM()) EqListN(true, getContext(), false, - ContextMemoryAllocator(getContext()->getCMM())); - d_selector_eq.insertDataFromContextMemory(tmp, sel); + }else{ + if( n.getKind() == APPLY_SELECTOR ) { + if( d_selectors.find( n ) == d_selectors.end() ) { + Debug("datatypes") << " Found selector " << n << endl; + d_selectors[ n ] = true; + d_cc.addTerm( n ); + Node tmp = find( n[0] ); + checkInstantiate( tmp ); + + Node s = n; + if( tmp != n[0] ) { + s = NodeManager::currentNM()->mkNode( APPLY_SELECTOR, n.getOperator(), tmp ); + } + s = collapseSelector( s ); + if( s.getKind() == APPLY_SELECTOR ) { + //add selector to selector eq list + Debug("datatypes") << " Add selector to list " << tmp << " " << n << endl; + EqListsN::iterator sel_i = d_selector_eq.find( tmp ); + EqListN* sel; + if( sel_i == d_selector_eq.end() ) { + sel = new(getContext()->getCMM()) EqListN(true, getContext(), false, + ContextMemoryAllocator(getContext()->getCMM())); + d_selector_eq.insertDataFromContextMemory(tmp, sel); + } else { + sel = (*sel_i).second; + } + sel->push_back( s ); } else { - sel = (*sel_i).second; + Debug("datatypes") << " collapsed selector to " << s << endl; } - sel->push_back( s ); - } else { - Debug("datatypes") << " collapsed selector to " << s << endl; } } + addTermToLabels( n ); } - addTermToLabels( n ); } void TheoryDatatypes::appendToDiseqList(TNode of, TNode eq) { @@ -1021,11 +1008,11 @@ bool TheoryDatatypes::searchForCycle( Node n, Node on, if( visited.find( nn ) == visited.end() ) { visited[nn] = true; if( nn == on || searchForCycle( nn, on, visited, explanation ) ) { - if( !d_cycle_check.isConnectedNode( n, n[i] ) ){ + if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n, n[i] ) ){ Debug("datatypes-cycles") << "Cycle subterm: " << n << " is not -> " << n[i] << "!!!!" << std::endl; } if( nn != n[i] ) { - if( !d_cycle_check.isConnectedNode( n[i], nn ) ){ + if( Debug.isOn("datatypes-cycles") && !d_cycle_check.isConnectedNode( n[i], nn ) ){ Debug("datatypes-cycles") << "Cycle equality: " << n[i] << " is not -> " << nn << "!!!!" << std::endl; } Node ccEq = NodeManager::currentNM()->mkNode( EQUAL, nn, n[i] ); diff --git a/src/theory/datatypes/theory_datatypes.h b/src/theory/datatypes/theory_datatypes.h index 1e715b4e4..23345ef8d 100644 --- a/src/theory/datatypes/theory_datatypes.h +++ b/src/theory/datatypes/theory_datatypes.h @@ -72,7 +72,7 @@ private: * map from terms to testers asserted for that term * for each t, this is either a list of equations of the form * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ), each of which are unique testers - * and n is less than the number of possible constructors for t, + * and n is less than the number of possible constructors for t minus one, * or a list of equations of the form * NOT is_[constructor_1]( t )...NOT is_[constructor_n]( t ) followed by * is_[constructor_(n+1)]( t ), each of which is a unique tester. diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 43c8735ad..61c48fa8d 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -89,11 +89,11 @@ void TransitiveClosure::debugPrintMatrix() for (i = 0; i < adjMatrix.size(); ++i) { for (j = 0; j < adjMatrix.size(); ++j) { if (adjMatrix[i] != NULL && adjMatrix[i]->read(j)) { - cout << "1 "; + Debug("trans-closure") << "1 "; } - else cout << "0 "; + else Debug("trans-closure") << "0 "; } - cout << endl; + Debug("trans-closure") << endl; } } @@ -110,10 +110,9 @@ unsigned TransitiveClosureNode::getId( Node i ){ void TransitiveClosureNode::debugPrint(){ for( int i=0; i<(int)currEdges.size(); i++ ){ - cout << "currEdges[ " << i << " ] = " - << currEdges[i].first << " -> " << currEdges[i].second; - //<< "(" << getId( currEdges[i].first ) << " -> " << getId( currEdges[i].second ) << ")"; - cout << std::endl; + Debug("trans-closure") << "currEdges[ " << i << " ] = " + << currEdges[i].first << " -> " << currEdges[i].second; + Debug("trans-closure") << std::endl; } } diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index af16d2e13..c7538bc41 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -76,7 +76,7 @@ public: void write(unsigned index) { if (index < 64) { - unsigned mask = uint64_t(1) << index; + uint64_t mask = uint64_t(1) << index; if ((d_data & mask) != 0) return; makeCurrent(); d_data = d_data | mask; @@ -127,7 +127,6 @@ public: class TransitiveClosureNode : public TransitiveClosure{ context::CDO< unsigned > d_counter; context::CDMap< Node, unsigned, NodeHashFunction > nodeMap; - unsigned getId( Node i ); //for debugging context::CDList< std::pair< Node, Node > > currEdges; public: @@ -135,7 +134,9 @@ public: TransitiveClosure(context), d_counter( context, 0 ), nodeMap( context ), currEdges(context) {} ~TransitiveClosureNode(){} - /* Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */ + /** get id for node */ + unsigned getId( Node i ); + /** Add an edge from node i to node j. Return false if successful, true if this edge would create a cycle */ bool addEdgeNode(Node i, Node j) { currEdges.push_back( std::pair< Node, Node >( i, j ) ); return addEdge( getId( i ), getId( j ) );