class Expr;
class Type;
-class BooleanType;
-class FunctionType;
+class BooleanType;
+class FunctionType;
class KindType;
class SmtEngine;
class NodeManager;
Expr mkExpr(Kind kind, const std::vector<Expr>& 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<const Type*>& argTypes,
const Type* range);
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){
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) {
}
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;
}
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;
}
}
* 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)
{}
/**
* 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;
/**
* 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.
* preceeded by an O(|watchlist|) operation.)
* This value is NULL iff the watch list is empty.
*/
- Link* last;
+ Link* d_last;
/** Context dependent operations */
/* 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);
}
}
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);
}
}
~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.
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();
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);
+ }
+
+
+
+
};
projects / cvc5.git / commitdiff