summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/theory/datatypes/explanation_manager.cpp3
-rw-r--r--src/theory/datatypes/explanation_manager.h8
-rw-r--r--src/theory/datatypes/theory_datatypes.cpp113
-rw-r--r--src/theory/datatypes/theory_datatypes.h2
-rw-r--r--src/util/trans_closure.cpp13
-rw-r--r--src/util/trans_closure.h7
6 files changed, 67 insertions, 79 deletions
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 <map>
-//#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<Node>(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<Node>(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 ) );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback