From 29cc307cdf2c42bebf4f5615874a864783f47fd0 Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 4 Mar 2010 20:10:46 +0000 Subject: [PATCH] Committing a bug fix from Dejan. This resolves an issue with restoring ECData. --- src/expr/expr_manager.h | 10 ++-- src/theory/uf/ecdata.cpp | 55 ++++++++++--------- src/theory/uf/ecdata.h | 16 +++--- src/theory/uf/theory_uf.cpp | 14 ++--- src/theory/uf/theory_uf.h | 2 - test/unit/theory/theory_uf_white.h | 87 ++++++++++++++++++++++++++++++ 6 files changed, 137 insertions(+), 47 deletions(-) diff --git a/src/expr/expr_manager.h b/src/expr/expr_manager.h index 67fa0664a..f5edc5464 100644 --- a/src/expr/expr_manager.h +++ b/src/expr/expr_manager.h @@ -24,8 +24,8 @@ namespace CVC4 { class Expr; class Type; -class BooleanType; -class FunctionType; +class BooleanType; +class FunctionType; class KindType; class SmtEngine; class NodeManager; @@ -91,12 +91,12 @@ public: Expr mkExpr(Kind kind, const std::vector& children); /** Make a function type from domain to range. */ - const FunctionType* - mkFunctionType(const Type* domain, + const FunctionType* + mkFunctionType(const Type* domain, const Type* range); /** Make a function type with input types from argTypes. */ - const FunctionType* + const FunctionType* mkFunctionType(const std::vector& argTypes, const Type* range); diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/ecdata.cpp index 5a89a4939..22db1e6d0 100644 --- a/src/theory/uf/ecdata.cpp +++ b/src/theory/uf/ecdata.cpp @@ -23,16 +23,16 @@ using namespace uf; ECData::ECData(Context * context, TNode n) : ContextObj(context), - find(this), - rep(n), - watchListSize(0), - first(NULL), - last(NULL) + d_find(this), + d_rep(n), + d_watchListSize(0), + d_first(NULL), + d_last(NULL) {} bool ECData::isClassRep(){ - return this == this->find; + return this == this->d_find; } void ECData::addPredecessor(TNode n, Context* context){ @@ -40,13 +40,13 @@ void ECData::addPredecessor(TNode n, Context* context){ makeCurrent(); - Link * newPred = new (context->getCMM()) Link(context, n, first); - first = newPred; - if(last == NULL){ - last = newPred; + Link * newPred = new (context->getCMM()) Link(context, n, d_first); + d_first = newPred; + if(d_last == NULL){ + d_last = newPred; } - ++watchListSize; + ++d_watchListSize; } ContextObj* ECData::save(ContextMemoryManager* pCMM) { @@ -54,30 +54,35 @@ ContextObj* ECData::save(ContextMemoryManager* pCMM) { } void ECData::restore(ContextObj* pContextObj) { - *this = *((ECData*)pContextObj); + ECData* data = (ECData*)pContextObj; + d_find = data->d_find; + d_first = data->d_first; + d_last = data->d_last; + d_rep = data->d_rep; + d_watchListSize = data->d_watchListSize; } Node ECData::getRep(){ - return rep; + return d_rep; } unsigned ECData::getWatchListSize(){ - return watchListSize; + return d_watchListSize; } void ECData::setFind(ECData * ec){ makeCurrent(); - find = ec; + d_find = ec; } ECData * ECData::getFind(){ - return find; + return d_find; } Link* ECData::getFirst(){ - return first; + return d_first; } @@ -87,14 +92,14 @@ void ECData::takeOverDescendantWatchList(ECData * nslave, ECData * nmaster){ nmaster->makeCurrent(); - nmaster->watchListSize += nslave->watchListSize; + nmaster->d_watchListSize += nslave->d_watchListSize; - if(nmaster->first == NULL){ - nmaster->first = nslave->first; - nmaster->last = nslave->last; - }else if(nslave->first != NULL){ - Link * currLast = nmaster->last; - currLast->next = nslave->first; - nmaster->last = nslave->last; + if(nmaster->d_first == NULL){ + nmaster->d_first = nslave->d_first; + nmaster->d_last = nslave->d_last; + }else if(nslave->d_first != NULL){ + Link * currLast = nmaster->d_last; + currLast->d_next = nslave->d_first; + nmaster->d_last = nslave->d_last; } } diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/ecdata.h index 5bb3a57bd..735712cdc 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/ecdata.h @@ -41,21 +41,21 @@ struct Link { * Pointer to the next element in linked list. * This is context dependent. */ - context::CDO< Link* > next; + context::CDO< Link* > d_next; /* Link is supposed to be allocated in a region of a ContextMemoryManager. * In order to avoid having to decrement the ref count at deletion time, * it is preferrable for the user of Link to maintain the invariant that * data will survival for the entire scope of the TNode. */ - TNode data; + TNode d_data; /** * Creates a new Link w.r.t. a context for the node n. * An optional parameter is to specify the next element in the link. */ Link(context::Context* context, TNode n, Link * l = NULL): - next(context, l), data(n) + d_next(context, l), d_data(n) {} /** @@ -103,7 +103,7 @@ private: * This was chosen to be a ECData pointer in order to shortcut at least one * table every time the find pointer is examined. */ - ECData* find; + ECData* d_find; /** @@ -122,17 +122,17 @@ private: * the ECData will never get garbage collected. * So this needs to be a soft link. */ - TNode rep; + TNode d_rep; /* Watch list datastructures. */ /** Maintains watch list size for more efficient merging */ - unsigned watchListSize; + unsigned d_watchListSize; /** *Pointer to the beginning of the watchlist. *This value is NULL iff the watch list is empty. */ - Link* first; + Link* d_first; /** * Pointer to the end of the watch-list. @@ -141,7 +141,7 @@ private: * preceeded by an O(|watchlist|) operation.) * This value is NULL iff the watch list is empty. */ - Link* last; + Link* d_last; /** Context dependent operations */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp index 485f5f6d3..b4597c7c7 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/theory_uf.cpp @@ -122,9 +122,9 @@ void TheoryUF::registerTerm(TNode n){ /* Because this can be called after nodes have been merged we may need * to be merged with other predecessors of the equivalence class. */ - for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->next ){ - if(equiv(n, Px->data)){ - Node pend = n.eqNode(Px->data); + for(Link* Px = ecChild->getFirst(); Px != NULL; Px = Px->d_next ){ + if(equiv(n, Px->d_data)){ + Node pend = n.eqNode(Px->d_data); d_pending.push_back(pend); } } @@ -210,10 +210,10 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY){ nslave->setFind(nmaster); - for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->next ){ - for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->next ){ - if(equiv(Px->data,Py->data)){ - Node pendingEq = (Px->data).eqNode(Py->data); + for(Link* Px = nmaster->getFirst(); Px != NULL; Px = Px->d_next ){ + for(Link* Py = nslave->getFirst(); Py != NULL; Py = Py->d_next ){ + if(equiv(Px->d_data,Py->d_data)){ + Node pendingEq = (Px->d_data).eqNode(Py->d_data); d_pending.push_back(pendingEq); } } diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 5ac5e3001..d432d733f 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -84,8 +84,6 @@ public: ~TheoryUF(); - //TODO Tim: I am going to delay documenting these functions while Morgan - //has pending changes to the contracts /** * Registers a previously unseen [in this context] node n. diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_white.h index 5aeb5f8a5..fe2c8d821 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_white.h @@ -115,6 +115,64 @@ public: delete d_nm; } + void testPushPopChain(){ + Node x = d_nm->mkVar(); + Node f = d_nm->mkVar(); + Node f_x = d_nm->mkNode(kind::APPLY, f, x); + Node f_f_x = d_nm->mkNode(kind::APPLY, f, f_x); + Node f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_x); + Node f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_x); + Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY, f, f_f_f_f_x); + + Node f3_x_eq_x = f_f_f_x.eqNode(x); + Node f5_x_eq_x = f_f_f_f_f_x.eqNode(x); + Node f5_x_eq_f5_x = f_f_f_f_f_x.eqNode(f_f_f_f_f_x); + Node f1_x_neq_x = f_x.eqNode(x).notNode(); + + Node expectedConflict = d_nm->mkNode(kind::AND, + f1_x_neq_x, + f5_x_eq_f5_x, + f3_x_eq_x, + f5_x_eq_x + ); + + d_euf->assertFact( f5_x_eq_f5_x ); + + d_euf->assertFact( f3_x_eq_x ); + d_euf->assertFact( f1_x_neq_x ); + d_euf->check(level); + d_context->push(); + + d_euf->assertFact( f5_x_eq_x ); + d_euf->check(level); + + TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); + Node realConflict = d_outputChannel.getIthNode(0); + TS_ASSERT_EQUALS(expectedConflict, realConflict); + + d_context->pop(); + d_euf->check(level); + + //Test that no additional calls to the output channel occurred. + TS_ASSERT_EQUALS(1, d_outputChannel.getNumCalls()); + + d_euf->assertFact( f5_x_eq_x ); + + d_euf->check(level); + + TS_ASSERT_EQUALS(2, d_outputChannel.getNumCalls()); + TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0)); + TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(1)); + Node firstConflict = d_outputChannel.getIthNode(0); + Node secondConflict = d_outputChannel.getIthNode(1); + TS_ASSERT_EQUALS(expectedConflict, firstConflict); + TS_ASSERT_EQUALS(expectedConflict, secondConflict); + + } + + + /* test that {f(f(x)) == x, f(f(f(x))) != f(x)} is inconsistent */ void testSimpleChain(){ Node x = d_nm->mkVar(); @@ -200,4 +258,33 @@ public: Node realConflict = d_outputChannel.getIthNode(0); TS_ASSERT_EQUALS(expectedConflict, realConflict); } + + + void testPushPopA(){ + Node x = d_nm->mkVar(); + Node x_eq_x = x.eqNode(x); + + d_context->push(); + d_euf->assertFact( x_eq_x ); + d_euf->check(level); + d_context->pop(); + d_euf->check(level); + } + + void testPushPopB(){ + Node x = d_nm->mkVar(); + Node f = d_nm->mkVar(); + Node f_x = d_nm->mkNode(kind::APPLY, f, x); + Node f_x_eq_x = f_x.eqNode(x); + + d_euf->assertFact( f_x_eq_x ); + d_context->push(); + d_euf->check(level); + d_context->pop(); + d_euf->check(level); + } + + + + }; -- 2.30.2