CongruenceClosure implementation; CongruenceClosure white-box test.
New UF theory implementation based on new CC module. This one
supports predicates. The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").
Added type infrastructure for TUPLE.
Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).
Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)
Other minor changes.
if test "$enable_shared" = no -a "$user_specified_enable_or_disable_shared" = yes; then
enable_static=yes
fi
-if test "$enable_shared" = no -a "$enable_static" = yes; then
- enable_static_binary=yes
-fi
# Features requested by the user
AC_MSG_CHECKING([for requested build profile])
if expr "$srcdir" : src/parser >/dev/null; then
definitions=" -D__BUILDING_CVC4PARSERLIB \\
"
- visibility=" -fvisibility=hidden"
+ visibility=' $(FLAG_VISIBILITY_HIDDEN)'
elif expr "$srcdir" : src/main >/dev/null; then
definitions=
visibility=
else
definitions=" -D__BUILDING_CVC4LIB \\
"
- visibility=" -fvisibility=hidden"
+ visibility=' $(FLAG_VISIBILITY_HIDDEN)'
fi
clibname="lib${clibbase}.la"
clibtarget="lib${clibbase}_la"
return get();
}
- CDOmap& operator=(const Data& data) {
+ const Data& operator=(const Data& data) {
set(data);
- return *this;
+ return data;
}
CDOmap* next() const {
return Type(d_nodeManager, new TypeNode(d_nodeManager->mkPredicateType(sortNodes)));
}
+TupleType ExprManager::mkTupleType(const std::vector<Type>& types) {
+ Assert( types.size() >= 2 );
+ NodeManagerScope nms(d_nodeManager);
+ std::vector<TypeNode> typeNodes;
+ for (unsigned i = 0, i_end = types.size(); i < i_end; ++ i) {
+ typeNodes.push_back(*types[i].d_typeNode);
+ }
+ return Type(d_nodeManager, new TypeNode(d_nodeManager->mkTupleType(typeNodes)));
+}
+
BitVectorType ExprManager::mkBitVectorType(unsigned size) const {
NodeManagerScope nms(d_nodeManager);
return Type(d_nodeManager, new TypeNode(d_nodeManager->mkBitVectorType(size)));
*/
FunctionType mkPredicateType(const std::vector<Type>& sorts);
+ /**
+ * Make a tuple type with types from
+ * <code>types[0..types.size()-1]</code>. <code>types</code> must
+ * have at least 2 elements.
+ */
+ TupleType mkTupleType(const std::vector<Type>& types);
+
/** Make a type representing a bit-vector of the given size */
BitVectorType mkBitVectorType(unsigned size) const;
nv->d_rc = 0;
setUsed();
Debug("gc") << "creating node value " << nv
- << " [" << nv->d_id << "]: " << nv->toString() << "\n";
+ << " [" << nv->d_id << "]: " << *nv << "\n";
return nv;
}
case kind::DISTINCT:
typeNode = CVC4::theory::builtin::DistinctTypeRule::computeType(this, n, check);
break;
+ case kind::TUPLE:
+ typeNode = CVC4::theory::builtin::TupleTypeRule::computeType(this, n, check);
+ break;
case kind::CONST_BOOLEAN:
typeNode = CVC4::theory::boolean::BooleanTypeRule::computeType(this, n, check);
break;
*/
inline TypeNode mkPredicateType(const std::vector<TypeNode>& sorts);
+ /**
+ * Make a tuple type with types from
+ * <code>types</code>. <code>types</code> must have at least two
+ * elements.
+ *
+ * @param types a vector of types
+ * @returns the tuple type (types[0], ..., types[n])
+ */
+ inline TypeNode mkTupleType(const std::vector<TypeNode>& types);
+
/** Make the type of bitvectors of size <code>size</code> */
inline TypeNode mkBitVectorType(unsigned size);
return mkTypeNode(kind::FUNCTION_TYPE, sortNodes);
}
+inline TypeNode NodeManager::mkTupleType(const std::vector<TypeNode>& types) {
+ Assert(types.size() >= 2);
+ std::vector<TypeNode> typeNodes;
+ for (unsigned i = 0; i < types.size(); ++ i) {
+ typeNodes.push_back(types[i]);
+ }
+ return mkTypeNode(kind::TUPLE_TYPE, typeNodes);
+}
+
inline TypeNode NodeManager::mkBitVectorType(unsigned size) {
return TypeNode(mkTypeConst<BitVectorSize>(BitVectorSize(size)));
}
return FunctionType(*this);
}
+/** Is this a tuple type? */
+bool Type::isTuple() const {
+ NodeManagerScope nms(d_nodeManager);
+ return d_typeNode->isTuple();
+}
+
+/** Cast to a tuple type */
+Type::operator TupleType() const throw (AssertionException) {
+ NodeManagerScope nms(d_nodeManager);
+ Assert(isTuple());
+ return TupleType(*this);
+}
+
/** Is this an array type? */
bool Type::isArray() const {
NodeManagerScope nms(d_nodeManager);
return makeType(d_typeNode->getRangeType());
}
+std::vector<Type> TupleType::getTypes() const {
+ NodeManagerScope nms(d_nodeManager);
+ std::vector<Type> types;
+ std::vector<TypeNode> typeNodes = d_typeNode->getTupleTypes();
+ std::vector<TypeNode>::iterator it = typeNodes.begin();
+ std::vector<TypeNode>::iterator it_end = typeNodes.end();
+ for(; it != it_end; ++ it) {
+ types.push_back(makeType(*it));
+ }
+ return types;
+}
+
std::string SortType::getName() const {
NodeManagerScope nms(d_nodeManager);
return d_typeNode->getAttribute(expr::VarNameAttr());
Assert(isFunction());
}
+TupleType::TupleType(const Type& t) throw (AssertionException)
+: Type(t)
+{
+ Assert(isTuple());
+}
+
ArrayType::ArrayType(const Type& t) throw (AssertionException)
: Type(t)
{
class BitVectorType;
class ArrayType;
class FunctionType;
+class TupleType;
class KindType;
class SortType;
class Type;
/**
* Is this a function type?
- * @return true if the type is a Boolean type
+ * @return true if the type is a function type
*/
bool isFunction() const;
operator FunctionType() const throw (AssertionException);
/**
- * Is this a function type?
- * @return true if the type is a Boolean type
+ * Is this a tuple type?
+ * @return true if the type is a tuple type
+ */
+ bool isTuple() const;
+
+ /**
+ * Cast this type to a tuple type
+ * @return the TupleType
+ */
+ operator TupleType() const throw (AssertionException);
+
+ /**
+ * Is this an array type?
+ * @return true if the type is a array type
*/
bool isArray() const;
};
/**
- * Class encapsulating a function type.
+ * Class encapsulating a tuple type.
+ */
+class CVC4_PUBLIC TupleType : public Type {
+
+public:
+
+ /** Construct from the base type */
+ TupleType(const Type& type) throw (AssertionException);
+
+ /** Get the constituent types */
+ std::vector<Type> getTypes() const;
+};
+
+/**
+ * Class encapsulating an array type.
*/
class CVC4_PUBLIC ArrayType : public Type {
std::vector<TypeNode> TypeNode::getArgTypes() const {
Assert(isFunction());
std::vector<TypeNode> args;
- for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++ i) {
+ for (unsigned i = 0, i_end = getNumChildren() - 1; i < i_end; ++i) {
args.push_back((*this)[i]);
}
return args;
return (*this)[getNumChildren()-1];
}
+/** Is this a tuple type? */
+bool TypeNode::isTuple() const {
+ return getKind() == kind::TUPLE_TYPE;
+}
+
+/** Is this a tuple type? */
+std::vector<TypeNode> TypeNode::getTupleTypes() const {
+ Assert(isTuple());
+ std::vector<TypeNode> types;
+ for (unsigned i = 0, i_end = getNumChildren(); i < i_end; ++i) {
+ types.push_back((*this)[i]);
+ }
+ return types;
+}
/** Is this a sort kind */
bool TypeNode::isSort() const {
*/
bool isPredicate() const;
+ /** Is this a tuple type? */
+ bool isTuple() const;
+
+ /** Get the constituent types of a tuple type */
+ std::vector<TypeNode> getTupleTypes() const;
+
/** Is this a bit-vector type */
bool isBitVector() const;
SHOW_CONFIG,
STRICT_PARSING,
DEFAULT_EXPR_DEPTH,
- PRINT_EXPR_TYPES
+ PRINT_EXPR_TYPES,
+ UF_THEORY
};/* enum OptionValue */
/**
{ "strict-parsing", no_argument , NULL, STRICT_PARSING },
{ "default-expr-depth", required_argument, NULL, DEFAULT_EXPR_DEPTH },
{ "print-expr-types", no_argument , NULL, PRINT_EXPR_TYPES },
+ { "uf" , required_argument, NULL, UF_THEORY },
{ NULL , no_argument , NULL, '\0' }
};/* if you add things to the above, please remember to update usage.h! */
}
break;
+ case UF_THEORY:
+ {
+ if(!strcmp(optarg, "tim")) {
+ opts->uf_implementation = Options::TIM;
+ } else if(!strcmp(optarg, "morgan")) {
+ opts->uf_implementation = Options::MORGAN;
+ } else if(!strcmp(optarg, "help")) {
+ printf("UF implementations available:\n");
+ printf("tim\n");
+ printf("morgan\n");
+ exit(1);
+ } else {
+ throw OptionException(string("unknown language for --uf: `") +
+ optarg + "'. Try --uf help.");
+ }
+ }
+ break;
+
case SHOW_CONFIG:
fputs(Configuration::about().c_str(), stdout);
printf("\n");
--debug | -d debugging for something (e.g. --debug arith), implies -t\n\
--stats give statistics on exit\n\
--default-expr-depth=N print exprs to depth N (0 == default, -1 == no limit)\n\
- --print-expr-types print types with variables when printing exprs\n"
+ --print-expr-types print types with variables when printing exprs\n\
+ --uf=morgan|tim select uninterpreted function theory implementation\n"
;
}/* CVC4::main namespace */
d_decisionEngine = new DecisionEngine;
// We have mutual dependancy here, so we add the prop engine to the theory
// engine later (it is non-essential there)
- d_theoryEngine = new TheoryEngine(d_ctxt);
+ d_theoryEngine = new TheoryEngine(d_ctxt, opts);
d_propEngine = new PropEngine(opts, d_decisionEngine, d_theoryEngine, d_ctxt);
d_theoryEngine->setPropEngine(d_propEngine);
}
"expr/type_constant.h" \
"basic types"
operator FUNCTION_TYPE 2: "function type"
+operator TUPLE_TYPE 2: "tuple type"
std::stringstream ss;
ss << "Types do not match in equation ";
ss << "[" << lhsType << "<>" << rhsType << "]";
-
+
throw TypeCheckingExceptionPrivate(n, ss.str());
}
}
return booleanType;
}
-};
+};/* class EqualityTypeRule */
+
class DistinctTypeRule {
public:
}
return nodeManager->booleanType();
}
-};
+};/* class DistinctTypeRule */
+
+
+class TupleTypeRule {
+public:
+ inline static TypeNode computeType(NodeManager* nodeManager, TNode n, bool check) {
+ std::vector<TypeNode> types;
+ for(TNode::iterator child_it = n.begin(), child_it_end = n.end();
+ child_it != child_it_end;
+ ++child_it) {
+ types.push_back((*child_it).getType(check));
+ }
+ return nodeManager->mkTupleType(types);
+ }
+};/* class TupleTypeRule */
+
}/* CVC4::theory::builtin namespace */
}/* CVC4::theory namespace */
#include "theory/builtin/theory_builtin.h"
#include "theory/booleans/theory_bool.h"
#include "theory/uf/theory_uf.h"
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "theory/uf/morgan/theory_uf_morgan.h"
#include "theory/arith/theory_arith.h"
#include "theory/arrays/theory_arrays.h"
#include "theory/bv/theory_bv.h"
+#include "util/options.h"
#include "util/stats.h"
namespace CVC4 {
theory::arrays::TheoryArrays* d_arrays;
theory::bv::TheoryBV* d_bv;
+ /**
+ * Debugging flag to ensure that shutdown() is called before the
+ * destructor.
+ */
+ bool d_hasShutDown;
+
/**
* Check whether a node is in the pre-rewrite cache or not.
*/
/**
* Construct a theory engine.
*/
- TheoryEngine(context::Context* ctxt) :
+ TheoryEngine(context::Context* ctxt, const Options* opts) :
d_propEngine(NULL),
d_theoryOut(this, ctxt),
+ d_hasShutDown(false),
d_statistics() {
d_sharedTermManager = new SharedTermManager(this, ctxt);
d_builtin = new theory::builtin::TheoryBuiltin(0, ctxt, d_theoryOut);
d_bool = new theory::booleans::TheoryBool(1, ctxt, d_theoryOut);
- d_uf = new theory::uf::TheoryUF(2, ctxt, d_theoryOut);
+ switch(opts->uf_implementation) {
+ case Options::TIM:
+ d_uf = new theory::uf::tim::TheoryUFTim(2, ctxt, d_theoryOut);
+ break;
+ case Options::MORGAN:
+ d_uf = new theory::uf::morgan::TheoryUFMorgan(2, ctxt, d_theoryOut);
+ break;
+ default:
+ Unhandled(opts->uf_implementation);
+ }
d_arith = new theory::arith::TheoryArith(3, ctxt, d_theoryOut);
d_arrays = new theory::arrays::TheoryArrays(4, ctxt, d_theoryOut);
d_bv = new theory::bv::TheoryBV(5, ctxt, d_theoryOut);
d_theoryOfTable.registerTheory(d_bv);
}
+ ~TheoryEngine() {
+ Assert(d_hasShutDown);
+
+ delete d_bv;
+ delete d_arrays;
+ delete d_arith;
+ delete d_uf;
+ delete d_bool;
+ delete d_builtin;
+
+ delete d_sharedTermManager;
+ }
+
SharedTermManager* getSharedTermManager() {
return d_sharedTermManager;
}
- void setPropEngine(prop::PropEngine* propEngine)
- {
+ void setPropEngine(prop::PropEngine* propEngine) {
Assert(d_propEngine == NULL);
d_propEngine = propEngine;
}
* ordering issues between PropEngine and Theory.
*/
void shutdown() {
+ // Set this first; if a Theory shutdown() throws an exception,
+ // at least the destruction of the TheoryEngine won't confound
+ // matters.
+ d_hasShutDown = true;
+
d_builtin->shutdown();
d_bool->shutdown();
d_uf->shutdown();
d_arith->shutdown();
d_arrays->shutdown();
d_bv->shutdown();
-
- delete d_bv;
- delete d_arrays;
- delete d_arith;
- delete d_uf;
- delete d_bool;
- delete d_builtin;
-
- delete d_sharedTermManager;
}
/**
noinst_LTLIBRARIES = libuf.la
libuf_la_SOURCES = \
- ecdata.h \
- ecdata.cpp \
theory_uf.h \
- theory_uf.cpp \
theory_uf_type_rules.h
+libuf_la_LIBADD = \
+ @builddir@/tim/libuftim.la \
+ @builddir@/morgan/libufmorgan.la
+
+SUBDIRS = tim morgan
+
EXTRA_DIST = kinds
+++ /dev/null
-/********************* */
-/*! \file ecdata.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of equivalence class data for UF theory.
- **
- ** Implementation of equivalence class data for UF theory. This is a
- ** context-dependent object.
- **/
-
-#include "theory/uf/ecdata.h"
-
-using namespace CVC4;
-using namespace context;
-using namespace theory;
-using namespace uf;
-
-ECData::ECData(Context * context, TNode n) :
- ContextObj(context),
- d_find(this),
- d_rep(n),
- d_watchListSize(0),
- d_first(NULL),
- d_last(NULL) {
-}
-
-bool ECData::isClassRep() {
- return this == this->d_find;
-}
-
-void ECData::addPredecessor(TNode n) {
- Assert(isClassRep());
-
- makeCurrent();
-
- Link * newPred = new(getCMM()) Link(getContext(), n, d_first);
- d_first = newPred;
- if(d_last == NULL) {
- d_last = newPred;
- }
-
- ++d_watchListSize;
-}
-
-ContextObj* ECData::save(ContextMemoryManager* pCMM) {
- return new(pCMM) ECData(*this);
-}
-
-void ECData::restore(ContextObj* 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 d_rep;
-}
-
-unsigned ECData::getWatchListSize() {
- return d_watchListSize;
-}
-
-void ECData::setFind(ECData * ec) {
- makeCurrent();
- d_find = ec;
-}
-
-ECData* ECData::getFind() {
- return d_find;
-}
-
-Link* ECData::getFirst() {
- return d_first;
-}
-
-void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) {
- Assert(nslave != nmaster);
- Assert(nslave->getFind() == nmaster);
-
- nmaster->makeCurrent();
-
- nmaster->d_watchListSize += nslave->d_watchListSize;
-
- 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;
- }
-}
+++ /dev/null
-/********************* */
-/*! \file ecdata.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Context dependent equivalence class datastructure for nodes.
- **
- ** Context dependent equivalence class datastructure for nodes.
- ** Currently keeps a context dependent watch list.
- **/
-
-#include "cvc4_private.h"
-
-#ifndef __CVC4__THEORY__UF__ECDATA_H
-#define __CVC4__THEORY__UF__ECDATA_H
-
-#include "expr/node.h"
-#include "context/context.h"
-#include "context/cdo.h"
-#include "context/context_mm.h"
-
-namespace CVC4 {
-namespace theory {
-namespace uf {
-
-/**
- * Link is a context dependent linked list of nodes.
- * Link is intended to be allocated in a Context's memory manager.
- * The next pointer of the list is context dependent, but the node being
- * pointed to is fixed for the life of the Link.
- *
- * Clients of Link are intended not to modify the node that is being pointed
- * to in good faith. This may change in the future.
- */
-struct Link {
- /**
- * Pointer to the next element in linked list.
- * This is context dependent.
- */
- 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 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) :
- d_next(true, context, l),
- d_data(n) {
- Debug("context") << "Link: " << this
- << " so cdo is " << &d_next << std::endl;
- }
-
- /**
- * Allocates a new Link in the region for the provided ContextMemoryManager.
- * This allows for cheap cleanup on pop.
- */
- static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
- return pCMM->newData(size);
- }
-
-private:
-
- /**
- * The destructor isn't actually defined. This declaration keeps
- * the compiler from creating (wastefully) a default definition, and
- * ensures that we get a link error if someone uses Link in a way
- * that requires destruction. Objects of class Link should always
- * be allocated in a ContextMemoryManager, which doesn't call
- * destructors.
- */
- ~Link() throw();
-
- /**
- * Just like the destructor, this is not defined. This ensures no
- * one tries to create a Link on the heap.
- */
- static void* operator new(size_t size);
-
-};/* struct Link */
-
-
-/**
- * ECData is a equivalence class object that is context dependent.
- * It is developed in order to support the congruence closure algorithm
- * in TheoryUF, and is not intended to be used outside of that package.
- *
- * ECData maintains:
- * - find pointer for the equivalence class (disjoint set forest)
- * - the node that represents the equivalence class.
- * - maintains a predecessorlist/watchlist
- *
- * ECData does not have support for the canonical find and union operators
- * for disjoint set forests. Instead it only provides access to the find
- * pointer. The implementation of find is ccFind in TheoryUF.
- * union is broken into 2 phases:
- * 1) setting the find point with setFind
- * 2) taking over the watch list of the other node.
- * This is a technical requirement for the implementation of TheoryUF.
- * (See ccUnion in TheoryUF for more information.)
- *
- * The intended paradigm for iterating over the watch list of ec is:
- * for(Link* i = ec->getFirst(); i != NULL; i = i->next );
- *
- * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses
- * ECData lives.
- */
-class ECData : public context::ContextObj {
-private:
- /**
- * This is the standard disjoint set forest find pointer.
- *
- * Why an ECData pointer instead of a node?
- * This was chosen to be a ECData pointer in order to shortcut at least one
- * table every time the find pointer is examined.
- */
- ECData* d_find;
-
- /**
- * This is pointer back to the node that represents this equivalence class.
- *
- * The following invariant should be maintained:
- * (n.getAttribute(ECAttr()))->rep == n
- * i.e. rep is equal to the node that maps to the ECData using ECAttr.
- *
- * Tricky part: This needs to be a TNode, not a Node.
- * Suppose that rep were a hard link.
- * When a node n maps to an ECData via the ECAttr() there will be a hard
- * link back to n in the ECData. The attribute does not do garbage collection
- * until the node gets garbage collected, which does not happen until its
- * ref count drops to 0. So because of this cycle neither the node and
- * the ECData will never get garbage collected.
- * So this needs to be a soft link.
- */
- TNode d_rep;
-
- // Watch list data structures follow
-
- /**
- * Maintains watch list size for more efficient merging.
- */
- unsigned d_watchListSize;
-
- /**
- * Pointer to the beginning of the watchlist.
- * This value is NULL iff the watch list is empty.
- */
- Link* d_first;
-
- /**
- * Pointer to the end of the watch-list.
- * This is maintained in order to constant time list merging.
- * (This does not give any asymptotic improve as this is currently always
- * preceeded by an O(|watchlist|) operation.)
- * This value is NULL iff the watch list is empty.
- */
- Link* d_last;
-
- /** Context-dependent operation: save this ECData */
- context::ContextObj* save(context::ContextMemoryManager* pCMM);
-
- /** Context-dependent operation: restore this ECData */
- void restore(context::ContextObj* pContextObj);
-
-public:
- /**
- * Returns true if this ECData object is the current representative of
- * the equivalence class.
- */
- bool isClassRep();
-
- /**
- * Adds a node to the watch list of the equivalence class. Does
- * context-dependent memory allocation in the Context with which
- * this ECData was created.
- *
- * @param n the node to be added.
- * @pre isClassRep() == true
- */
- void addPredecessor(TNode n);
-
- /**
- * Creates a EQ with the representative n
- * @param context the context to associate with this ecdata.
- * This is required as ECData is context dependent
- * @param n the node that corresponds to this ECData
- */
- ECData(context::Context* context, TNode n);
-
- /** Destructor for ECDatas */
- ~ECData() {
- Debug("ufgc") << "Calling ECData destructor" << std::endl;
- destroy();
- }
-
- /**
- * An ECData takes over the watch list of another ECData.
- * This is the second step in the union operator for ECData.
- * This should be called after nslave->setFind(nmaster);
- * After this is done nslave's watch list should never be accessed by
- * getLast() or getFirst()
- */
- static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster);
-
- /**
- * Returns the representative of this ECData.
- */
- Node getRep();
-
- /**
- * Returns the size of the equivalence class.
- */
- unsigned getWatchListSize();
-
- /**
- * Returns a pointer the first member of the watch list.
- */
- Link* getFirst();
-
-
- /**
- * Returns the find pointer of the ECData.
- * If isClassRep(), then getFind() == this
- */
- ECData* getFind();
-
- /**
- * Sets the find pointer of the equivalence class to be another ECData object.
- *
- * @pre isClassRep() == true
- * @pre ec->isClassRep() == true
- * @post isClassRep() == false
- * @post ec->isClassRep() == true
- */
- void setFind(ECData * ec);
-
-};/* class ECData */
-
-}/* CVC4::theory::uf namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
-
-#endif /* __CVC4__THEORY__UF__ECDATA_H */
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libufmorgan.la
+
+libufmorgan_la_SOURCES = \
+ theory_uf_morgan.h \
+ theory_uf_morgan.cpp
+
+EXTRA_DIST =
--- /dev/null
+/********************* */
+/*! \file theory_uf_morgan.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the theory of uninterpreted functions.
+ **
+ ** Implementation of the theory of uninterpreted functions.
+ **/
+
+#include "theory/uf/morgan/theory_uf_morgan.h"
+#include "expr/kind.h"
+#include "util/congruence_closure.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::morgan;
+
+TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
+ TheoryUF(id, ctxt, out),
+ d_assertions(ctxt),
+ d_ccChannel(this),
+ d_cc(ctxt, &d_ccChannel),
+ d_unionFind(ctxt),
+ d_disequalities(ctxt),
+ d_disequality(ctxt),
+ d_conflict(),
+ d_trueNode(),
+ d_falseNode() {
+ TypeNode boolType = NodeManager::currentNM()->booleanType();
+ d_trueNode = NodeManager::currentNM()->mkVar("TRUE_UF", boolType);
+ d_falseNode = NodeManager::currentNM()->mkVar("FALSE_UF", boolType);
+ d_cc.addTerm(d_trueNode);
+ d_cc.addTerm(d_falseNode);
+}
+
+TheoryUFMorgan::~TheoryUFMorgan() {
+}
+
+RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
+ if(topLevel) {
+ Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
+ Node ret(n);
+ if(n.getKind() == EQUAL) {
+ if(n[0] == n[1]) {
+ ret = NodeManager::currentNM()->mkConst(true);
+ }
+ }
+ Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
+ return RewriteComplete(ret);
+ } else {
+ return RewriteComplete(n);
+ }
+}
+
+void TheoryUFMorgan::preRegisterTerm(TNode n) {
+ Debug("uf") << "uf: preRegisterTerm(" << n << ")" << std::endl;
+}
+
+void TheoryUFMorgan::registerTerm(TNode n) {
+ Debug("uf") << "uf: registerTerm(" << n << ")" << std::endl;
+}
+
+Node TheoryUFMorgan::constructConflict(TNode diseq) {
+ Debug("uf") << "uf: begin constructConflict()" << std::endl;
+ Debug("uf") << "uf: using diseq == " << diseq << std::endl;
+
+ Node explanation = d_cc.explain(diseq[0], diseq[1]);
+
+ NodeBuilder<> nb(kind::AND);
+ if(explanation.getKind() == kind::AND) {
+ for(Node::iterator i = explanation.begin();
+ i != explanation.end();
+ ++i) {
+ nb << *i;
+ }
+ } else {
+ Assert(explanation.getKind() == kind::EQUAL);
+ nb << explanation;
+ }
+ nb << diseq.notNode();
+
+ // by construction this should be true
+ Assert(nb.getNumChildren() > 1);
+
+ Node conflict = nb;
+ Debug("uf") << "conflict constructed : " << conflict << std::endl;
+
+ Debug("uf") << "uf: ending constructConflict()" << std::endl;
+
+ return conflict;
+}
+
+TNode TheoryUFMorgan::find(TNode a) {
+ UnionFind::iterator i = d_unionFind.find(a);
+ if(i == d_unionFind.end()) {
+ return a;
+ } else {
+ return d_unionFind[a] = find((*i).second);
+ }
+}
+
+// no path compression
+TNode TheoryUFMorgan::debugFind(TNode a) const {
+ UnionFind::iterator i = d_unionFind.find(a);
+ if(i == d_unionFind.end()) {
+ return a;
+ } else {
+ return debugFind((*i).second);
+ }
+}
+
+void TheoryUFMorgan::unionClasses(TNode a, TNode b) {
+ if(a == b) {
+ return;
+ }
+ Assert(d_unionFind.find(a) == d_unionFind.end());
+ Assert(d_unionFind.find(b) == d_unionFind.end());
+ d_unionFind[a] = b;
+}
+
+void TheoryUFMorgan::notifyCongruent(TNode a, TNode b) {
+ Debug("uf") << "uf: notified of merge " << a << std::endl
+ << " and " << b << std::endl;
+ if(!d_conflict.isNull()) {
+ // if already a conflict, we don't care
+ return;
+ }
+
+ // make "a" the one with shorter diseqList
+ DiseqLists::iterator deq_ia = d_disequalities.find(a);
+ DiseqLists::iterator deq_ib = d_disequalities.find(b);
+ if(deq_ia != d_disequalities.end()) {
+ if(deq_ib == d_disequalities.end() ||
+ (*deq_ia).second->size() > (*deq_ib).second->size()) {
+ TNode tmp = a;
+ a = b;
+ b = tmp;
+ Debug("uf") << " swapping to make a shorter diseqList" << std::endl;
+ }
+ }
+ a = find(a);
+ b = find(b);
+ Debug("uf") << "uf: uf reps are " << a << std::endl
+ << " and " << b << std::endl;
+ unionClasses(a, b);
+
+ DiseqLists::iterator deq_i = d_disequalities.find(a);
+ if(deq_i != d_disequalities.end()) {
+ // a set of other trees we are already disequal to
+ // (for the optimization below)
+ std::set<TNode> alreadyDiseqs;
+ DiseqLists::iterator deq_ib = d_disequalities.find(b);
+ if(deq_ib != d_disequalities.end()) {
+ DiseqList* deq = (*deq_i).second;
+ for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
+ TNode deqn = *j;
+ TNode s = deqn[0];
+ TNode t = deqn[1];
+ TNode sp = find(s);
+ TNode tp = find(t);
+ Assert(sp == b || tp == b);
+ if(sp == b) {
+ alreadyDiseqs.insert(tp);
+ } else {
+ alreadyDiseqs.insert(sp);
+ }
+ }
+ }
+
+ DiseqList* deq = (*deq_i).second;
+ Debug("uf") << "a == " << a << std::endl;
+ Debug("uf") << "size of deq(a) is " << deq->size() << std::endl;
+ for(DiseqList::const_iterator j = deq->begin(); j != deq->end(); ++j) {
+ Debug("uf") << " deq(a) ==> " << *j << std::endl;
+ TNode deqn = *j;
+ Assert(deqn.getKind() == kind::EQUAL);
+ TNode s = deqn[0];
+ TNode t = deqn[1];
+ Debug("uf") << " s ==> " << s << std::endl
+ << " t ==> " << t << std::endl
+ << " find(s) ==> " << debugFind(s) << std::endl
+ << " find(t) ==> " << debugFind(t) << std::endl;
+ TNode sp = find(s);
+ TNode tp = find(t);
+ if(sp == tp) {
+ d_conflict = deqn;
+ return;
+ }
+ Assert(sp == b || tp == b);
+ // optimization: don't put redundant diseq's in the list
+ if(sp == b) {
+ if(alreadyDiseqs.find(tp) == alreadyDiseqs.end()) {
+ appendToDiseqList(b, deqn);
+ alreadyDiseqs.insert(tp);
+ }
+ } else {
+ if(alreadyDiseqs.find(sp) == alreadyDiseqs.end()) {
+ appendToDiseqList(b, deqn);
+ alreadyDiseqs.insert(sp);
+ }
+ }
+ }
+ Debug("uf") << "end" << std::endl;
+ }
+}
+
+void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
+ Debug("uf") << "appending " << eq << std::endl
+ << " to diseq list of " << of << std::endl;
+ Assert(eq.getKind() == kind::EQUAL);
+ Assert(of == debugFind(of));
+ DiseqLists::iterator deq_i = d_disequalities.find(of);
+ DiseqList* deq;
+ if(deq_i == d_disequalities.end()) {
+ deq = new(getContext()->getCMM()) DiseqList(true, getContext());
+ d_disequalities.insertDataFromContextMemory(of, deq);
+ } else {
+ deq = (*deq_i).second;
+ }
+ deq->push_back(eq);
+ Debug("uf") << " size is now " << deq->size() << std::endl;
+}
+
+void TheoryUFMorgan::addDisequality(TNode eq) {
+ Assert(eq.getKind() == kind::EQUAL);
+
+ Node a = eq[0];
+ Node b = eq[1];
+
+ appendToDiseqList(find(a), eq);
+ appendToDiseqList(find(b), eq);
+}
+
+void TheoryUFMorgan::check(Effort level) {
+ Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
+
+ while(!done()) {
+ Node assertion = get();
+
+ Debug("uf") << "uf check(): " << assertion << std::endl;
+
+ switch(assertion.getKind()) {
+ case EQUAL:
+ d_cc.addEquality(assertion);
+ if(!d_conflict.isNull()) {
+ Node conflict = constructConflict(d_conflict);
+ d_conflict = Node::null();
+ d_out->conflict(conflict, false);
+ return;
+ }
+ break;
+ case APPLY_UF:
+ { // predicate
+ Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion, d_trueNode);
+ d_cc.addTerm(assertion);
+ d_cc.addEquality(eq);
+ Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+ Assert(find(d_trueNode) != find(d_falseNode));
+ }
+ break;
+ case NOT:
+ if(assertion[0].getKind() == kind::EQUAL) {
+ Node a = assertion[0][0];
+ Node b = assertion[0][1];
+
+ addDisequality(assertion[0]);
+ d_disequality.push_back(assertion[0]);
+
+ d_cc.addTerm(a);
+ d_cc.addTerm(b);
+
+ Debug("uf") << " a ==> " << a << std::endl
+ << " b ==> " << b << std::endl
+ << " find(a) ==> " << debugFind(a) << std::endl
+ << " find(b) ==> " << debugFind(b) << std::endl;
+
+ // There are two ways to get a conflict here.
+ if(!d_conflict.isNull()) {
+ // We get a conflict this way if we weren't watching a, b
+ // before and we were just now notified (via
+ // notifyCongruent()) when we called addTerm() above that
+ // they are congruent. We make this a separate case (even
+ // though the check in the "else if.." below would also
+ // catch it, so that we can clear out d_conflict.
+ Node conflict = constructConflict(d_conflict);
+ d_conflict = Node::null();
+ d_out->conflict(conflict, false);
+ return;
+ } else if(find(a) == find(b)) {
+ // We get a conflict this way if we WERE previously watching
+ // a, b and were notified previously (via notifyCongruent())
+ // that they were congruent.
+ Node conflict = constructConflict(assertion[0]);
+ d_out->conflict(conflict, false);
+ return;
+ }
+
+ // If we get this far, there should be nothing conflicting due
+ // to this disequality.
+ Assert(!d_cc.areCongruent(a, b));
+ } else {
+ Assert(assertion[0].getKind() == kind::APPLY_UF);
+ Node eq = NodeManager::currentNM()->mkNode(kind::EQUAL, assertion[0], d_falseNode);
+ d_cc.addTerm(assertion[0]);
+ d_cc.addEquality(eq);
+ Debug("uf") << "true == false ? " << (find(d_trueNode) == find(d_falseNode)) << std::endl;
+ Assert(find(d_trueNode) != find(d_falseNode));
+ }
+ break;
+ default:
+ Unhandled(assertion.getKind());
+ }
+ }
+ Debug("uf") << "uf check() done = " << (done() ? "true" : "false") << std::endl;
+
+ for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
+ diseqIter != d_disequality.end();
+ ++diseqIter) {
+
+ TNode left = (*diseqIter)[0];
+ TNode right = (*diseqIter)[1];
+ Debug("uf") << "testing left: " << left << std::endl
+ << " right: " << right << std::endl
+ << " find(L): " << debugFind(left) << std::endl
+ << " find(R): " << debugFind(right) << std::endl
+ << " areCong: " << d_cc.areCongruent(left, right) << std::endl;
+ Assert((debugFind(left) == debugFind(right)) == d_cc.areCongruent(left, right));
+ }
+
+ Debug("uf") << "uf: end check(" << level << ")" << std::endl;
+}
+
+void TheoryUFMorgan::propagate(Effort level) {
+ Debug("uf") << "uf: begin propagate(" << level << ")" << std::endl;
+ Debug("uf") << "uf: end propagate(" << level << ")" << std::endl;
+}
--- /dev/null
+/********************* */
+/*! \file theory_uf_morgan.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.
+ **
+ ** This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality. It is based on the Nelson-Oppen algorithm given in
+ ** "Fast Decision Procedures Based on Congruence Closure"
+ ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
+ ** This has been extended to work in a context-dependent way.
+ ** This interacts heavily with the data-structures given in ecdata.h .
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H
+#define __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "theory/theory.h"
+#include "theory/uf/theory_uf.h"
+
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdlist.h"
+#include "util/congruence_closure.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace morgan {
+
+class TheoryUFMorgan : public TheoryUF {
+
+private:
+
+ class CongruenceChannel {
+ TheoryUFMorgan* d_uf;
+
+ public:
+ CongruenceChannel(TheoryUFMorgan* uf) : d_uf(uf) {}
+ void notifyCongruent(TNode a, TNode b) {
+ d_uf->notifyCongruent(a, b);
+ }
+ };/* class CongruenceChannel */
+ friend class CongruenceChannel;
+
+ /**
+ * List of all of the non-negated literals from the assertion queue.
+ * This is used only for conflict generation.
+ * This differs from pending as the program generates new equalities that
+ * are not in this list.
+ * This will probably be phased out in future version.
+ */
+ context::CDList<Node> d_assertions;
+
+ /**
+ * Our channel connected to the congruence closure module.
+ */
+ CongruenceChannel d_ccChannel;
+
+ /**
+ * Instance of the congruence closure module.
+ */
+ CongruenceClosure<CongruenceChannel> d_cc;
+
+ typedef context::CDMap<TNode, TNode, TNodeHashFunction> UnionFind;
+ UnionFind d_unionFind;
+
+ typedef context::CDList<Node> DiseqList;
+ typedef context::CDMap<Node, DiseqList*, NodeHashFunction> DiseqLists;
+
+ /** List of all disequalities this theory has seen. */
+ DiseqLists d_disequalities;
+
+ context::CDList<Node> d_disequality;
+
+ Node d_conflict;
+
+ Node d_trueNode, d_falseNode;
+
+public:
+
+ /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
+ TheoryUFMorgan(int id, context::Context* ctxt, OutputChannel& out);
+
+ /** Destructor for the TheoryUF object. */
+ ~TheoryUFMorgan();
+
+ /**
+ * Registers a previously unseen [in this context] node n.
+ * For TheoryUF, this sets up and maintains invaraints about
+ * equivalence class data-structures.
+ *
+ * Overloads a void registerTerm(TNode n); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void registerTerm(TNode n);
+
+ /**
+ * Currently this does nothing.
+ *
+ * Overloads a void preRegisterTerm(TNode n); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void preRegisterTerm(TNode n);
+
+ /**
+ * Checks whether the set of literals provided to the theory is consistent.
+ *
+ * If this is called at any effort level, it computes the congruence closure
+ * of all of the positive literals in the context.
+ *
+ * If this is called at full effort it checks if any of the negative literals
+ * are inconsistent with the congruence closure.
+ *
+ * Overloads void check(Effort level); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void check(Effort level);
+
+ /**
+ * Rewrites a node in the theory of uninterpreted functions.
+ * This is fairly basic and only ensures that atoms that are
+ * unsatisfiable or a valid are rewritten to false or true respectively.
+ */
+ RewriteResponse postRewrite(TNode n, bool topLevel);
+
+ /**
+ * Propagates theory literals.
+ *
+ * Overloads void propagate(Effort level); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void propagate(Effort level);
+
+ /**
+ * Explains a previously reported conflict. Currently does nothing.
+ *
+ * Overloads void explain(TNode n, Effort level); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void explain(TNode n, Effort level) {}
+
+ std::string identify() const { return std::string("TheoryUFMorgan"); }
+
+private:
+
+ /** Constructs a conflict from an inconsistent disequality. */
+ Node constructConflict(TNode diseq);
+
+ TNode find(TNode a);
+ TNode debugFind(TNode a) const;
+ void unionClasses(TNode a, TNode b);
+
+ void appendToDiseqList(TNode of, TNode eq);
+ void addDisequality(TNode eq);
+
+ /**
+ * Receives a notification from the congruence closure module that
+ * two nodes have been merged into the same congruence class.
+ */
+ void notifyCongruent(TNode a, TNode b);
+
+};/* class TheoryUFMorgan */
+
+}/* CVC4::theory::uf::morgan namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__MORGAN__THEORY_UF_MORGAN_H */
+++ /dev/null
-/********************* */
-/*! \file theory_uf.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief Implementation of the theory of uninterpreted functions.
- **
- ** Implementation of the theory of uninterpreted functions.
- **/
-
-#include "theory/uf/theory_uf.h"
-#include "theory/uf/ecdata.h"
-#include "expr/kind.h"
-
-using namespace CVC4;
-using namespace CVC4::kind;
-using namespace CVC4::context;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
-
-TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) :
- Theory(id, c, out),
- d_assertions(c),
- d_pending(c),
- d_currentPendingIdx(c,0),
- d_disequality(c),
- d_registered(c) {
-}
-
-TheoryUF::~TheoryUF() {
-}
-
-Node TheoryUF::rewrite(TNode n){
- Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
- Node ret(n);
- if(n.getKind() == EQUAL){
- Assert(n.getNumChildren() == 2);
- if(n[0] == n[1]) {
- ret = NodeManager::currentNM()->mkConst(true);
- }
- }
- Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
- return ret;
-}
-void TheoryUF::preRegisterTerm(TNode n) {
- Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
- Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
-}
-
-void TheoryUF::registerTerm(TNode n) {
-
- Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl;
-
- d_registered.push_back(n);
-
- ECData* ecN;
-
- if(n.getAttribute(ECAttr(), ecN)) {
- /* registerTerm(n) is only called when a node has not been seen in the
- * current context. ECAttr() is not a context-dependent attribute.
- * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
- * then it must be the case that this attribute was created in a previous
- * and no longer valid context. Because of this we have to reregister the
- * predecessors lists.
- * Also we do not have to worry about duplicates because all of the Link*
- * setup before are removed when the context n was setup in was popped out
- * of. All we are going to do here are sanity checks.
- */
-
- /*
- * Consider the following chain of events:
- * 1) registerTerm(n) is called on node n where n : f(m) in context level X,
- * 2) A new ECData is created on the heap, ecN,
- * 3) n is added to the predessecor list of m in context level X,
- * 4) We pop out of X,
- * 5) n is removed from the predessecor list of m because this is context
- * dependent, the Link* will be destroyed and pointers to the Link
- * structs in the ECData objects will be updated.
- * 6) registerTerm(n) is called on node n in context level Y,
- * 7) If n.hasAttribute(ECAttr(), &ecN), then ecN is still around,
- * but the predecessor list is not
- *
- * The above assumes that the code is working correctly.
- */
- Assert(ecN->getFirst() == NULL,
- "Equivalence class data exists for the node being registered. "
- "Expected getFirst() == NULL. "
- "This data is either already in use or was not properly maintained "
- "during backtracking");
- /*Assert(ecN->getLast() == NULL,
- "Equivalence class data exists for the node being registered. "
- "Expected getLast() == NULL. "
- "This data is either already in use or was not properly maintained "
- "during backtracking.");*/
- Assert(ecN->isClassRep(),
- "Equivalence class data exists for the node being registered. "
- "Expected isClassRep() to be true. "
- "This data is either already in use or was not properly maintained "
- "during backtracking");
- Assert(ecN->getWatchListSize() == 0,
- "Equivalence class data exists for the node being registered. "
- "Expected getWatchListSize() == 0. "
- "This data is either already in use or was not properly maintained "
- "during backtracking");
- } else {
- //The attribute does not exist, so it is created and set
- ecN = new (true) ECData(getContext(), n);
- n.setAttribute(ECAttr(), ecN);
- }
-
- /* If the node is an APPLY_UF, we need to add it to the predecessor list
- * of its children.
- */
- if(n.getKind() == APPLY_UF) {
- TNode::iterator cIter = n.begin();
-
- for(; cIter != n.end(); ++cIter) {
- TNode child = *cIter;
-
- /* Because this can be called after nodes have been merged, we need
- * to lookup the representative in the UnionFind datastructure.
- */
- ECData* ecChild = ccFind(child.getAttribute(ECAttr()));
-
- /* 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->d_next ) {
- if(equiv(n, Px->d_data)) {
- Node pend = n.eqNode(Px->d_data);
- d_pending.push_back(pend);
- }
- }
-
- ecChild->addPredecessor(n);
- }
- }
- Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;
-
-}
-
-bool TheoryUF::sameCongruenceClass(TNode x, TNode y) {
- return
- ccFind(x.getAttribute(ECAttr())) ==
- ccFind(y.getAttribute(ECAttr()));
-}
-
-bool TheoryUF::equiv(TNode x, TNode y) {
- Assert(x.getKind() == kind::APPLY_UF);
- Assert(y.getKind() == kind::APPLY_UF);
-
- if(x.getNumChildren() != y.getNumChildren()) {
- return false;
- }
-
- if(x.getOperator() != y.getOperator()) {
- return false;
- }
-
- // intentionally don't look at operator
-
- TNode::iterator xIter = x.begin();
- TNode::iterator yIter = y.begin();
-
- while(xIter != x.end()) {
-
- if(!sameCongruenceClass(*xIter, *yIter)) {
- return false;
- }
-
- ++xIter;
- ++yIter;
- }
- return true;
-}
-
-/* This is a very basic, but *obviously correct* find implementation
- * of the classic find algorithm.
- * TODO after we have done some more testing:
- * 1) Add path compression. This is dependent on changes to ccUnion as
- * many better algorithms use eager path compression.
- * 2) Elminate recursion.
- */
-ECData* TheoryUF::ccFind(ECData * x) {
- if(x->getFind() == x) {
- return x;
- } else {
- return ccFind(x->getFind());
- }
- /* Slightly better Find w/ path compression and no recursion*/
- /*
- ECData* start;
- ECData* next = x;
- while(x != x->getFind()) x=x->getRep();
- while( (start = next) != x) {
- next = start->getFind();
- start->setFind(x);
- }
- return x;
- */
-}
-
-void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) {
- ECData* nslave;
- ECData* nmaster;
-
- if(ecX->getWatchListSize() <= ecY->getWatchListSize()) {
- nslave = ecX;
- nmaster = ecY;
- } else {
- nslave = ecY;
- nmaster = ecX;
- }
-
- nslave->setFind(nmaster);
-
- 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);
- }
- }
- }
-
- ECData::takeOverDescendantWatchList(nslave, nmaster);
-}
-
-void TheoryUF::merge() {
- while(d_currentPendingIdx < d_pending.size() ) {
- Node assertion = d_pending[d_currentPendingIdx];
- d_currentPendingIdx = d_currentPendingIdx + 1;
-
- TNode x = assertion[0];
- TNode y = assertion[1];
-
- ECData* tmpX = x.getAttribute(ECAttr());
- ECData* tmpY = y.getAttribute(ECAttr());
-
- ECData* ecX = ccFind(tmpX);
- ECData* ecY = ccFind(tmpY);
- if(ecX == ecY)
- continue;
-
- Debug("uf") << "merging equivalence classes for " << std::endl;
- Debug("uf") << "left equivalence class :" << (ecX->getRep()) << std::endl;
- Debug("uf") << "right equivalence class :" << (ecY->getRep()) << std::endl;
- Debug("uf") << std::endl;
-
- ccUnion(ecX, ecY);
- }
-}
-
-Node TheoryUF::constructConflict(TNode diseq) {
- Debug("uf") << "uf: begin constructConflict()" << std::endl;
-
- NodeBuilder<> nb(kind::AND);
- nb << diseq;
- for(unsigned i = 0; i < d_assertions.size(); ++i) {
- nb << d_assertions[i];
- }
-
- Assert(nb.getNumChildren() > 0);
- Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb;
-
- Debug("uf") << "conflict constructed : " << conflict << std::endl;
-
- Debug("uf") << "uf: ending constructConflict()" << std::endl;
-
- return conflict;
-}
-
-void TheoryUF::check(Effort level) {
-
- Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
-
- while(!done()) {
- Node assertion = get();
- Debug("uf") << "TheoryUF::check(): " << assertion << std::endl;
-
- switch(assertion.getKind()) {
- case EQUAL:
- d_assertions.push_back(assertion);
- d_pending.push_back(assertion);
- merge();
- break;
- case NOT:
- d_disequality.push_back(assertion[0]);
- break;
- default:
- Unhandled(assertion.getKind());
- }
-
- Debug("uf") << "TheoryUF::check(): done = " << (done() ? "true" : "false") << std::endl;
- }
-
- //Make sure all outstanding merges are completed.
- if(d_currentPendingIdx < d_pending.size()) {
- merge();
- }
-
- if(standardEffortOrMore(level)) {
- for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
- diseqIter != d_disequality.end();
- ++diseqIter) {
-
- TNode left = (*diseqIter)[0];
- TNode right = (*diseqIter)[1];
- if(sameCongruenceClass(left, right)) {
- Node remakeNeq = (*diseqIter).notNode();
- Node conflict = constructConflict(remakeNeq);
- d_out->conflict(conflict, false);
- return;
- }
- }
- }
-
- Debug("uf") << "uf: end check(" << level << ")" << std::endl;
-}
/********************* */
/*! \file theory_uf.h
** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
+ ** Original author: mdeters
+ ** Major contributors: none
** Minor contributors (to current version): none
** This file is part of the CVC4 prototype.
** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
** See the file COPYING in the top-level source directory for licensing
** information.\endverbatim
**
- ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality.
- **
- ** This is a basic implementation of the Theory of Uninterpreted Functions
- ** with Equality. It is based on the Nelson-Oppen algorithm given in
- ** "Fast Decision Procedures Based on Congruence Closure"
- ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
- ** This has been extended to work in a context-dependent way.
- ** This interacts heavily with the data-structures given in ecdata.h .
+ ** \brief This is the interface to TheoryUF implementations
**
+ ** This is the interface to TheoryUF implementations. All
+ ** implementations of TheoryUF should inherit from this class.
**/
#include "cvc4_private.h"
#include "theory/theory.h"
#include "context/context.h"
-#include "context/cdo.h"
-#include "context/cdlist.h"
-#include "theory/uf/ecdata.h"
namespace CVC4 {
namespace theory {
namespace uf {
class TheoryUF : public Theory {
-
-private:
-
- /**
- * List of all of the non-negated literals from the assertion queue.
- * This is used only for conflict generation.
- * This differs from pending as the program generates new equalities that
- * are not in this list.
- * This will probably be phased out in future version.
- */
- context::CDList<Node> d_assertions;
-
- /**
- * List of pending equivalence class merges.
- *
- * Tricky part:
- * Must keep a hard link because new equality terms are created and appended
- * to this list.
- */
- context::CDList<Node> d_pending;
-
- /** Index of the next pending equality to merge. */
- context::CDO<unsigned> d_currentPendingIdx;
-
- /** List of all disequalities this theory has seen. */
- context::CDList<Node> d_disequality;
-
- /**
- * List of all of the terms that are registered in the current context.
- * When registerTerm is called on a term we want to guarentee that there
- * is a hard link to the term for the duration of the context in which
- * register term is called.
- * This invariant is enough for us to use soft links where we want is the
- * current implementation as well as making ECAttr() not context dependent.
- * Soft links used both in ECData, and Link.
- */
- context::CDList<Node> d_registered;
-
public:
/** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
- TheoryUF(int id, context::Context* c, OutputChannel& out);
-
- /** Destructor for the TheoryUF object. */
- ~TheoryUF();
-
-
-
- /**
- * Registers a previously unseen [in this context] node n.
- * For TheoryUF, this sets up and maintains invaraints about
- * equivalence class data-structures.
- *
- * Overloads a void registerTerm(TNode n); from theory.h.
- * See theory/theory.h for more information about this method.
- */
- void registerTerm(TNode n);
-
- /**
- * Currently this does nothing.
- *
- * Overloads a void preRegisterTerm(TNode n); from theory.h.
- * See theory/theory.h for more information about this method.
- */
- void preRegisterTerm(TNode n);
-
- /**
- * Checks whether the set of literals provided to the theory is consistent.
- *
- * If this is called at any effort level, it computes the congruence closure
- * of all of the positive literals in the context.
- *
- * If this is called at full effort it checks if any of the negative literals
- * are inconsistent with the congruence closure.
- *
- * Overloads void check(Effort level); from theory.h.
- * See theory/theory.h for more information about this method.
- */
- void check(Effort level);
-
-
- /**
- * Rewrites a node in the theory of uninterpreted functions.
- * This is fairly basic and only ensures that atoms that are
- * unsatisfiable or a valid are rewritten to false or true respectively.
- */
- Node rewrite(TNode n);
-
- /**
- * Plug in old rewrite to the new (pre,post)rewrite interface.
- */
- RewriteResponse postRewrite(TNode n, bool topLevel) {
- return RewriteComplete(topLevel ? rewrite(n) : Node(n));
- }
-
- /**
- * Propagates theory literals. Currently does nothing.
- *
- * Overloads void propagate(Effort level); from theory.h.
- * See theory/theory.h for more information about this method.
- */
- void propagate(Effort level) {}
-
- /**
- * Explains a previously reported conflict. Currently does nothing.
- *
- * Overloads void explain(TNode n, Effort level); from theory.h.
- * See theory/theory.h for more information about this method.
- */
- void explain(TNode n, Effort level) {}
-
- std::string identify() const { return std::string("TheoryUF"); }
-
-private:
- /**
- * Checks whether 2 nodes are already in the same equivalence class tree.
- * This should only be used internally, and it should only be called when
- * the only thing done with the equivalence classes is an equality check.
- *
- * @returns true iff ccFind(x) == ccFind(y);
- */
- bool sameCongruenceClass(TNode x, TNode y);
-
- /**
- * Checks whether Node x and Node y are currently congruent
- * using the equivalence class data structures.
- * @returns true iff
- * |x| = n = |y| and
- * x.getOperator() == y.getOperator() and
- * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
- */
- bool equiv(TNode x, TNode y);
-
- /**
- * Merges 2 equivalence classes, checks wether any predecessors need to
- * be set equal to complete congruence closure.
- * The class with the smaller class size will be merged.
- * @pre ecX->isClassRep()
- * @pre ecY->isClassRep()
- */
- void ccUnion(ECData* ecX, ECData* ecY);
-
- /**
- * Returns the representative of the equivalence class.
- * May modify the find pointers associated with equivalence classes.
- */
- ECData* ccFind(ECData* x);
-
- /** Performs Congruence Closure to reflect the new additions to d_pending. */
- void merge();
-
- /** Constructs a conflict from an inconsistent disequality. */
- Node constructConflict(TNode diseq);
+ TheoryUF(int id, context::Context* ctxt, OutputChannel& out)
+ : Theory(id, ctxt, out) {}
};/* class TheoryUF */
-
-/**
- * Cleanup function for ECData. This will be used for called whenever
- * a ECAttr is being destructed.
- */
-struct ECCleanupStrategy {
- static void cleanup(ECData* ec) {
- Debug("ufgc") << "cleaning up ECData " << ec << "\n";
- ec->deleteSelf();
- }
-};/* struct ECCleanupStrategy */
-
-/** Unique name to use for constructing ECAttr. */
-struct ECAttrTag {};
-
-/**
- * ECAttr is the attribute that maps a node to an equivalence class.
- */
-typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr;
-
}/* CVC4::theory::uf namespace */
}/* CVC4::theory namespace */
}/* CVC4 namespace */
--- /dev/null
+AM_CPPFLAGS = \
+ -D__BUILDING_CVC4LIB \
+ -I@srcdir@/../../../include -I@srcdir@/../../.. -I@builddir@/../../..
+AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN)
+
+noinst_LTLIBRARIES = libuftim.la
+
+libuftim_la_SOURCES = \
+ ecdata.h \
+ ecdata.cpp \
+ theory_uf_tim.h \
+ theory_uf_tim.cpp
+
+EXTRA_DIST =
--- /dev/null
+/********************* */
+/*! \file ecdata.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of equivalence class data for UF theory.
+ **
+ ** Implementation of equivalence class data for UF theory. This is a
+ ** context-dependent object.
+ **/
+
+#include "theory/uf/tim/ecdata.h"
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
+
+ECData::ECData(Context * context, TNode n) :
+ ContextObj(context),
+ d_find(this),
+ d_rep(n),
+ d_watchListSize(0),
+ d_first(NULL),
+ d_last(NULL) {
+}
+
+bool ECData::isClassRep() {
+ return this == this->d_find;
+}
+
+void ECData::addPredecessor(TNode n) {
+ Assert(isClassRep());
+
+ makeCurrent();
+
+ Link * newPred = new(getCMM()) Link(getContext(), n, d_first);
+ d_first = newPred;
+ if(d_last == NULL) {
+ d_last = newPred;
+ }
+
+ ++d_watchListSize;
+}
+
+ContextObj* ECData::save(ContextMemoryManager* pCMM) {
+ return new(pCMM) ECData(*this);
+}
+
+void ECData::restore(ContextObj* 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 d_rep;
+}
+
+unsigned ECData::getWatchListSize() {
+ return d_watchListSize;
+}
+
+void ECData::setFind(ECData * ec) {
+ makeCurrent();
+ d_find = ec;
+}
+
+ECData* ECData::getFind() {
+ return d_find;
+}
+
+Link* ECData::getFirst() {
+ return d_first;
+}
+
+void ECData::takeOverDescendantWatchList(ECData* nslave, ECData* nmaster) {
+ Assert(nslave != nmaster);
+ Assert(nslave->getFind() == nmaster);
+
+ nmaster->makeCurrent();
+
+ nmaster->d_watchListSize += nslave->d_watchListSize;
+
+ 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;
+ }
+}
--- /dev/null
+/********************* */
+/*! \file ecdata.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Context dependent equivalence class datastructure for nodes.
+ **
+ ** Context dependent equivalence class datastructure for nodes.
+ ** Currently keeps a context dependent watch list.
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H
+#define __CVC4__THEORY__UF__TIM__ECDATA_H
+
+#include "expr/node.h"
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/context_mm.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace tim {
+
+/**
+ * Link is a context dependent linked list of nodes.
+ * Link is intended to be allocated in a Context's memory manager.
+ * The next pointer of the list is context dependent, but the node being
+ * pointed to is fixed for the life of the Link.
+ *
+ * Clients of Link are intended not to modify the node that is being pointed
+ * to in good faith. This may change in the future.
+ */
+struct Link {
+ /**
+ * Pointer to the next element in linked list.
+ * This is context dependent.
+ */
+ 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 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) :
+ d_next(true, context, l),
+ d_data(n) {
+ Debug("context") << "Link: " << this
+ << " so cdo is " << &d_next << std::endl;
+ }
+
+ /**
+ * Allocates a new Link in the region for the provided ContextMemoryManager.
+ * This allows for cheap cleanup on pop.
+ */
+ static void* operator new(size_t size, context::ContextMemoryManager* pCMM) {
+ return pCMM->newData(size);
+ }
+
+private:
+
+ /**
+ * The destructor isn't actually defined. This declaration keeps
+ * the compiler from creating (wastefully) a default definition, and
+ * ensures that we get a link error if someone uses Link in a way
+ * that requires destruction. Objects of class Link should always
+ * be allocated in a ContextMemoryManager, which doesn't call
+ * destructors.
+ */
+ ~Link() throw();
+
+ /**
+ * Just like the destructor, this is not defined. This ensures no
+ * one tries to create a Link on the heap.
+ */
+ static void* operator new(size_t size);
+
+};/* struct Link */
+
+
+/**
+ * ECData is a equivalence class object that is context dependent.
+ * It is developed in order to support the congruence closure algorithm
+ * in TheoryUF, and is not intended to be used outside of that package.
+ *
+ * ECData maintains:
+ * - find pointer for the equivalence class (disjoint set forest)
+ * - the node that represents the equivalence class.
+ * - maintains a predecessorlist/watchlist
+ *
+ * ECData does not have support for the canonical find and union operators
+ * for disjoint set forests. Instead it only provides access to the find
+ * pointer. The implementation of find is ccFind in TheoryUF.
+ * union is broken into 2 phases:
+ * 1) setting the find point with setFind
+ * 2) taking over the watch list of the other node.
+ * This is a technical requirement for the implementation of TheoryUF.
+ * (See ccUnion in TheoryUF for more information.)
+ *
+ * The intended paradigm for iterating over the watch list of ec is:
+ * for(Link* i = ec->getFirst(); i != NULL; i = i->next );
+ *
+ * See also ECAttr() in theory_uf.h, and theory_uf.cpp where the codde that uses
+ * ECData lives.
+ */
+class ECData : public context::ContextObj {
+private:
+ /**
+ * This is the standard disjoint set forest find pointer.
+ *
+ * Why an ECData pointer instead of a node?
+ * This was chosen to be a ECData pointer in order to shortcut at least one
+ * table every time the find pointer is examined.
+ */
+ ECData* d_find;
+
+ /**
+ * This is pointer back to the node that represents this equivalence class.
+ *
+ * The following invariant should be maintained:
+ * (n.getAttribute(ECAttr()))->rep == n
+ * i.e. rep is equal to the node that maps to the ECData using ECAttr.
+ *
+ * Tricky part: This needs to be a TNode, not a Node.
+ * Suppose that rep were a hard link.
+ * When a node n maps to an ECData via the ECAttr() there will be a hard
+ * link back to n in the ECData. The attribute does not do garbage collection
+ * until the node gets garbage collected, which does not happen until its
+ * ref count drops to 0. So because of this cycle neither the node and
+ * the ECData will never get garbage collected.
+ * So this needs to be a soft link.
+ */
+ TNode d_rep;
+
+ // Watch list data structures follow
+
+ /**
+ * Maintains watch list size for more efficient merging.
+ */
+ unsigned d_watchListSize;
+
+ /**
+ * Pointer to the beginning of the watchlist.
+ * This value is NULL iff the watch list is empty.
+ */
+ Link* d_first;
+
+ /**
+ * Pointer to the end of the watch-list.
+ * This is maintained in order to constant time list merging.
+ * (This does not give any asymptotic improve as this is currently always
+ * preceeded by an O(|watchlist|) operation.)
+ * This value is NULL iff the watch list is empty.
+ */
+ Link* d_last;
+
+ /** Context-dependent operation: save this ECData */
+ context::ContextObj* save(context::ContextMemoryManager* pCMM);
+
+ /** Context-dependent operation: restore this ECData */
+ void restore(context::ContextObj* pContextObj);
+
+public:
+ /**
+ * Returns true if this ECData object is the current representative of
+ * the equivalence class.
+ */
+ bool isClassRep();
+
+ /**
+ * Adds a node to the watch list of the equivalence class. Does
+ * context-dependent memory allocation in the Context with which
+ * this ECData was created.
+ *
+ * @param n the node to be added.
+ * @pre isClassRep() == true
+ */
+ void addPredecessor(TNode n);
+
+ /**
+ * Creates a EQ with the representative n
+ * @param context the context to associate with this ecdata.
+ * This is required as ECData is context dependent
+ * @param n the node that corresponds to this ECData
+ */
+ ECData(context::Context* context, TNode n);
+
+ /** Destructor for ECDatas */
+ ~ECData() {
+ Debug("ufgc") << "Calling ECData destructor" << std::endl;
+ destroy();
+ }
+
+ /**
+ * An ECData takes over the watch list of another ECData.
+ * This is the second step in the union operator for ECData.
+ * This should be called after nslave->setFind(nmaster);
+ * After this is done nslave's watch list should never be accessed by
+ * getLast() or getFirst()
+ */
+ static void takeOverDescendantWatchList(ECData * nslave, ECData * nmaster);
+
+ /**
+ * Returns the representative of this ECData.
+ */
+ Node getRep();
+
+ /**
+ * Returns the size of the equivalence class.
+ */
+ unsigned getWatchListSize();
+
+ /**
+ * Returns a pointer the first member of the watch list.
+ */
+ Link* getFirst();
+
+
+ /**
+ * Returns the find pointer of the ECData.
+ * If isClassRep(), then getFind() == this
+ */
+ ECData* getFind();
+
+ /**
+ * Sets the find pointer of the equivalence class to be another ECData object.
+ *
+ * @pre isClassRep() == true
+ * @pre ec->isClassRep() == true
+ * @post isClassRep() == false
+ * @post ec->isClassRep() == true
+ */
+ void setFind(ECData * ec);
+
+};/* class ECData */
+
+}/* CVC4::theory::uf::tim namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */
--- /dev/null
+/********************* */
+/*! \file theory_uf_tim.cpp
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Implementation of the theory of uninterpreted functions.
+ **
+ ** Implementation of the theory of uninterpreted functions.
+ **/
+
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "theory/uf/tim/ecdata.h"
+#include "expr/kind.h"
+
+using namespace CVC4;
+using namespace CVC4::kind;
+using namespace CVC4::context;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
+
+TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) :
+ TheoryUF(id, c, out),
+ d_assertions(c),
+ d_pending(c),
+ d_currentPendingIdx(c,0),
+ d_disequality(c),
+ d_registered(c) {
+}
+
+TheoryUFTim::~TheoryUFTim() {
+}
+
+Node TheoryUFTim::rewrite(TNode n){
+ Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
+ Node ret(n);
+ if(n.getKind() == EQUAL){
+ Assert(n.getNumChildren() == 2);
+ if(n[0] == n[1]) {
+ ret = NodeManager::currentNM()->mkConst(true);
+ }
+ }
+ Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
+ return ret;
+}
+void TheoryUFTim::preRegisterTerm(TNode n) {
+ Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
+ Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
+}
+
+void TheoryUFTim::registerTerm(TNode n) {
+
+ Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl;
+
+ d_registered.push_back(n);
+
+ ECData* ecN;
+
+ if(n.getAttribute(ECAttr(), ecN)) {
+ /* registerTerm(n) is only called when a node has not been seen in the
+ * current context. ECAttr() is not a context-dependent attribute.
+ * When n.hasAttribute(ECAttr(),...) is true on a registerTerm(n) call,
+ * then it must be the case that this attribute was created in a previous
+ * and no longer valid context. Because of this we have to reregister the
+ * predecessors lists.
+ * Also we do not have to worry about duplicates because all of the Link*
+ * setup before are removed when the context n was setup in was popped out
+ * of. All we are going to do here are sanity checks.
+ */
+
+ /*
+ * Consider the following chain of events:
+ * 1) registerTerm(n) is called on node n where n : f(m) in context level X,
+ * 2) A new ECData is created on the heap, ecN,
+ * 3) n is added to the predessecor list of m in context level X,
+ * 4) We pop out of X,
+ * 5) n is removed from the predessecor list of m because this is context
+ * dependent, the Link* will be destroyed and pointers to the Link
+ * structs in the ECData objects will be updated.
+ * 6) registerTerm(n) is called on node n in context level Y,
+ * 7) If n.hasAttribute(ECAttr(), &ecN), then ecN is still around,
+ * but the predecessor list is not
+ *
+ * The above assumes that the code is working correctly.
+ */
+ Assert(ecN->getFirst() == NULL,
+ "Equivalence class data exists for the node being registered. "
+ "Expected getFirst() == NULL. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking");
+ /*Assert(ecN->getLast() == NULL,
+ "Equivalence class data exists for the node being registered. "
+ "Expected getLast() == NULL. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking.");*/
+ Assert(ecN->isClassRep(),
+ "Equivalence class data exists for the node being registered. "
+ "Expected isClassRep() to be true. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking");
+ Assert(ecN->getWatchListSize() == 0,
+ "Equivalence class data exists for the node being registered. "
+ "Expected getWatchListSize() == 0. "
+ "This data is either already in use or was not properly maintained "
+ "during backtracking");
+ } else {
+ //The attribute does not exist, so it is created and set
+ ecN = new (true) ECData(getContext(), n);
+ n.setAttribute(ECAttr(), ecN);
+ }
+
+ /* If the node is an APPLY_UF, we need to add it to the predecessor list
+ * of its children.
+ */
+ if(n.getKind() == APPLY_UF) {
+ TNode::iterator cIter = n.begin();
+
+ for(; cIter != n.end(); ++cIter) {
+ TNode child = *cIter;
+
+ /* Because this can be called after nodes have been merged, we need
+ * to lookup the representative in the UnionFind datastructure.
+ */
+ ECData* ecChild = ccFind(child.getAttribute(ECAttr()));
+
+ /* 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->d_next ) {
+ if(equiv(n, Px->d_data)) {
+ Node pend = n.eqNode(Px->d_data);
+ d_pending.push_back(pend);
+ }
+ }
+
+ ecChild->addPredecessor(n);
+ }
+ }
+ Debug("uf") << "uf: end registerTerm(" << n << ")" << std::endl;
+
+}
+
+bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) {
+ return
+ ccFind(x.getAttribute(ECAttr())) ==
+ ccFind(y.getAttribute(ECAttr()));
+}
+
+bool TheoryUFTim::equiv(TNode x, TNode y) {
+ Assert(x.getKind() == kind::APPLY_UF);
+ Assert(y.getKind() == kind::APPLY_UF);
+
+ if(x.getNumChildren() != y.getNumChildren()) {
+ return false;
+ }
+
+ if(x.getOperator() != y.getOperator()) {
+ return false;
+ }
+
+ // intentionally don't look at operator
+
+ TNode::iterator xIter = x.begin();
+ TNode::iterator yIter = y.begin();
+
+ while(xIter != x.end()) {
+
+ if(!sameCongruenceClass(*xIter, *yIter)) {
+ return false;
+ }
+
+ ++xIter;
+ ++yIter;
+ }
+ return true;
+}
+
+/* This is a very basic, but *obviously correct* find implementation
+ * of the classic find algorithm.
+ * TODO after we have done some more testing:
+ * 1) Add path compression. This is dependent on changes to ccUnion as
+ * many better algorithms use eager path compression.
+ * 2) Elminate recursion.
+ */
+ECData* TheoryUFTim::ccFind(ECData * x) {
+ if(x->getFind() == x) {
+ return x;
+ } else {
+ return ccFind(x->getFind());
+ }
+ /* Slightly better Find w/ path compression and no recursion*/
+ /*
+ ECData* start;
+ ECData* next = x;
+ while(x != x->getFind()) x=x->getRep();
+ while( (start = next) != x) {
+ next = start->getFind();
+ start->setFind(x);
+ }
+ return x;
+ */
+}
+
+void TheoryUFTim::ccUnion(ECData* ecX, ECData* ecY) {
+ ECData* nslave;
+ ECData* nmaster;
+
+ if(ecX->getWatchListSize() <= ecY->getWatchListSize()) {
+ nslave = ecX;
+ nmaster = ecY;
+ } else {
+ nslave = ecY;
+ nmaster = ecX;
+ }
+
+ nslave->setFind(nmaster);
+
+ 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);
+ }
+ }
+ }
+
+ ECData::takeOverDescendantWatchList(nslave, nmaster);
+}
+
+void TheoryUFTim::merge() {
+ while(d_currentPendingIdx < d_pending.size() ) {
+ Node assertion = d_pending[d_currentPendingIdx];
+ d_currentPendingIdx = d_currentPendingIdx + 1;
+
+ TNode x = assertion[0];
+ TNode y = assertion[1];
+
+ ECData* tmpX = x.getAttribute(ECAttr());
+ ECData* tmpY = y.getAttribute(ECAttr());
+
+ ECData* ecX = ccFind(tmpX);
+ ECData* ecY = ccFind(tmpY);
+ if(ecX == ecY)
+ continue;
+
+ Debug("uf") << "merging equivalence classes for " << std::endl;
+ Debug("uf") << "left equivalence class :" << (ecX->getRep()) << std::endl;
+ Debug("uf") << "right equivalence class :" << (ecY->getRep()) << std::endl;
+ Debug("uf") << std::endl;
+
+ ccUnion(ecX, ecY);
+ }
+}
+
+Node TheoryUFTim::constructConflict(TNode diseq) {
+ Debug("uf") << "uf: begin constructConflict()" << std::endl;
+
+ NodeBuilder<> nb(kind::AND);
+ nb << diseq;
+ for(unsigned i = 0; i < d_assertions.size(); ++i) {
+ nb << d_assertions[i];
+ }
+
+ Assert(nb.getNumChildren() > 0);
+ Node conflict = nb.getNumChildren() == 1 ? nb[0] : nb;
+
+ Debug("uf") << "conflict constructed : " << conflict << std::endl;
+
+ Debug("uf") << "uf: ending constructConflict()" << std::endl;
+
+ return conflict;
+}
+
+void TheoryUFTim::check(Effort level) {
+
+ Debug("uf") << "uf: begin check(" << level << ")" << std::endl;
+
+ while(!done()) {
+ Node assertion = get();
+ Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl;
+
+ switch(assertion.getKind()) {
+ case EQUAL:
+ d_assertions.push_back(assertion);
+ d_pending.push_back(assertion);
+ merge();
+ break;
+ case NOT:
+ Assert(assertion[0].getKind() == EQUAL,
+ "predicates not supported in this UF implementation");
+ d_disequality.push_back(assertion[0]);
+ break;
+ case APPLY_UF:
+ Unhandled("predicates not supported in this UF implementation");
+ default:
+ Unhandled(assertion.getKind());
+ }
+
+ Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl;
+ }
+
+ //Make sure all outstanding merges are completed.
+ if(d_currentPendingIdx < d_pending.size()) {
+ merge();
+ }
+
+ if(standardEffortOrMore(level)) {
+ for(CDList<Node>::const_iterator diseqIter = d_disequality.begin();
+ diseqIter != d_disequality.end();
+ ++diseqIter) {
+
+ TNode left = (*diseqIter)[0];
+ TNode right = (*diseqIter)[1];
+ if(sameCongruenceClass(left, right)) {
+ Node remakeNeq = (*diseqIter).notNode();
+ Node conflict = constructConflict(remakeNeq);
+ d_out->conflict(conflict, false);
+ return;
+ }
+ }
+ }
+
+ Debug("uf") << "uf: end check(" << level << ")" << std::endl;
+}
--- /dev/null
+/********************* */
+/*! \file theory_uf.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality.
+ **
+ ** This is a basic implementation of the Theory of Uninterpreted Functions
+ ** with Equality. It is based on the Nelson-Oppen algorithm given in
+ ** "Fast Decision Procedures Based on Congruence Closure"
+ ** (http://portal.acm.org/ft_gateway.cfm?id=322198&type=pdf)
+ ** This has been extended to work in a context-dependent way.
+ ** This interacts heavily with the data-structures given in ecdata.h .
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+#define __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H
+
+#include "expr/node.h"
+#include "expr/attribute.h"
+
+#include "theory/theory.h"
+
+#include "context/context.h"
+#include "context/cdo.h"
+#include "context/cdlist.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/tim/ecdata.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+namespace tim {
+
+class TheoryUFTim : public TheoryUF {
+
+private:
+
+ /**
+ * List of all of the non-negated literals from the assertion queue.
+ * This is used only for conflict generation.
+ * This differs from pending as the program generates new equalities that
+ * are not in this list.
+ * This will probably be phased out in future version.
+ */
+ context::CDList<Node> d_assertions;
+
+ /**
+ * List of pending equivalence class merges.
+ *
+ * Tricky part:
+ * Must keep a hard link because new equality terms are created and appended
+ * to this list.
+ */
+ context::CDList<Node> d_pending;
+
+ /** Index of the next pending equality to merge. */
+ context::CDO<unsigned> d_currentPendingIdx;
+
+ /** List of all disequalities this theory has seen. */
+ context::CDList<Node> d_disequality;
+
+ /**
+ * List of all of the terms that are registered in the current context.
+ * When registerTerm is called on a term we want to guarentee that there
+ * is a hard link to the term for the duration of the context in which
+ * register term is called.
+ * This invariant is enough for us to use soft links where we want is the
+ * current implementation as well as making ECAttr() not context dependent.
+ * Soft links used both in ECData, and Link.
+ */
+ context::CDList<Node> d_registered;
+
+public:
+
+ /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
+ TheoryUFTim(int id, context::Context* c, OutputChannel& out);
+
+ /** Destructor for the TheoryUF object. */
+ ~TheoryUFTim();
+
+
+
+ /**
+ * Registers a previously unseen [in this context] node n.
+ * For TheoryUF, this sets up and maintains invaraints about
+ * equivalence class data-structures.
+ *
+ * Overloads a void registerTerm(TNode n); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void registerTerm(TNode n);
+
+ /**
+ * Currently this does nothing.
+ *
+ * Overloads a void preRegisterTerm(TNode n); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void preRegisterTerm(TNode n);
+
+ /**
+ * Checks whether the set of literals provided to the theory is consistent.
+ *
+ * If this is called at any effort level, it computes the congruence closure
+ * of all of the positive literals in the context.
+ *
+ * If this is called at full effort it checks if any of the negative literals
+ * are inconsistent with the congruence closure.
+ *
+ * Overloads void check(Effort level); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void check(Effort level);
+
+
+ /**
+ * Rewrites a node in the theory of uninterpreted functions.
+ * This is fairly basic and only ensures that atoms that are
+ * unsatisfiable or a valid are rewritten to false or true respectively.
+ */
+ Node rewrite(TNode n);
+
+ /**
+ * Plug in old rewrite to the new (pre,post)rewrite interface.
+ */
+ RewriteResponse postRewrite(TNode n, bool topLevel) {
+ return RewriteComplete(topLevel ? rewrite(n) : Node(n));
+ }
+
+ /**
+ * Propagates theory literals. Currently does nothing.
+ *
+ * Overloads void propagate(Effort level); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void propagate(Effort level) {}
+
+ /**
+ * Explains a previously reported conflict. Currently does nothing.
+ *
+ * Overloads void explain(TNode n, Effort level); from theory.h.
+ * See theory/theory.h for more information about this method.
+ */
+ void explain(TNode n, Effort level) {}
+
+ std::string identify() const { return std::string("TheoryUFTim"); }
+
+private:
+ /**
+ * Checks whether 2 nodes are already in the same equivalence class tree.
+ * This should only be used internally, and it should only be called when
+ * the only thing done with the equivalence classes is an equality check.
+ *
+ * @returns true iff ccFind(x) == ccFind(y);
+ */
+ bool sameCongruenceClass(TNode x, TNode y);
+
+ /**
+ * Checks whether Node x and Node y are currently congruent
+ * using the equivalence class data structures.
+ * @returns true iff
+ * |x| = n = |y| and
+ * x.getOperator() == y.getOperator() and
+ * forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
+ */
+ bool equiv(TNode x, TNode y);
+
+ /**
+ * Merges 2 equivalence classes, checks wether any predecessors need to
+ * be set equal to complete congruence closure.
+ * The class with the smaller class size will be merged.
+ * @pre ecX->isClassRep()
+ * @pre ecY->isClassRep()
+ */
+ void ccUnion(ECData* ecX, ECData* ecY);
+
+ /**
+ * Returns the representative of the equivalence class.
+ * May modify the find pointers associated with equivalence classes.
+ */
+ ECData* ccFind(ECData* x);
+
+ /** Performs Congruence Closure to reflect the new additions to d_pending. */
+ void merge();
+
+ /** Constructs a conflict from an inconsistent disequality. */
+ Node constructConflict(TNode diseq);
+
+};/* class TheoryUFTim */
+
+
+/**
+ * Cleanup function for ECData. This will be used for called whenever
+ * a ECAttr is being destructed.
+ */
+struct ECCleanupStrategy {
+ static void cleanup(ECData* ec) {
+ Debug("ufgc") << "cleaning up ECData " << ec << "\n";
+ ec->deleteSelf();
+ }
+};/* struct ECCleanupStrategy */
+
+/** Unique name to use for constructing ECAttr. */
+struct ECAttrTag {};
+
+/**
+ * ECAttr is the attribute that maps a node to an equivalence class.
+ */
+typedef expr::Attribute<ECAttrTag, ECData*, ECCleanupStrategy> ECAttr;
+
+}/* CVC4::theory::uf::tim namespace */
+}/* CVC4::theory::uf namespace */
+}/* CVC4::theory namespace */
+}/* CVC4 namespace */
+
+#endif /* __CVC4__THEORY__UF__TIM__THEORY_UF_TIM_H */
--- /dev/null
+/********************* */
+/*! \file congruence_closure.cpp
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief The congruence closure module implementation
+ **
+ ** The congruence closure module implementation.
+ **/
+
+#include "util/congruence_closure.h"
+#include "util/Assert.h"
+
+#include <string>
+#include <list>
+#include <algorithm>
+#include <utility>
+#include <ext/hash_map>
+
+using namespace std;
+
+namespace CVC4 {
+
+
+}/* CVC4 namespace */
#define __CVC4__UTIL__CONGRUENCE_CLOSURE_H
#include <list>
-#include <algorithm>
-#include <utility>
#include <ext/hash_map>
+#include <ext/hash_set>
+#include <sstream>
#include "expr/node_manager.h"
#include "expr/node.h"
+#include "context/context.h"
#include "context/cdmap.h"
+#include "context/cdset.h"
+#include "context/cdlist.h"
+#include "util/exception.h"
namespace CVC4 {
+template <class OutputChannel>
+class CongruenceClosure;
+
+template <class OutputChannel>
+std::ostream& operator<<(std::ostream& out,
+ const CongruenceClosure<OutputChannel>& cc);
+
+class CVC4_PUBLIC CongruenceClosureException : public Exception {
+public:
+ inline CongruenceClosureException(std::string msg) :
+ Exception(std::string("Congruence closure exception: ") + msg) {}
+ inline CongruenceClosureException(const char* msg) :
+ Exception(std::string("Congruence closure exception: ") + msg) {}
+};/* class CongruenceClosureException */
+
+
/**
* Congruence closure module for CVC4.
*
* OutputChannel is a template argument (it's probably a thin layer,
* and we want to avoid a virtual call hierarchy in this case, and
* enable aggressive inlining). It need only implement one method,
- * merge():
+ * notifyCongruent():
*
* class MyOutputChannel {
* public:
- * void merge(TNode a, TNode b) {
+ * void notifyCongruent(TNode a, TNode b) {
* // CongruenceClosure is notifying us that "a" is now the EC
* // representative for "b" in this context. After a pop, "a"
* // will be its own representative again. Note that "a" and
* // "b" might never have been added with addTerm(). However,
* // something in their equivalence class was (for which a
- * // previous merge() would have notified you of their EC
- * // representative, which is now "a" or "b").
+ * // previous notifyCongruent() would have notified you of
+ * // their EC representative, which is now "a" or "b").
* //
- * // This call is made immediately after the merge is done, and
- * // while other pending merges may be on the queue. In particular,
- * // any exception thrown from this function will immediately
- * // exit the CongruenceClosure call. A subsequent call to
- * // doPendingMerges() is necessary to continue merging;
- * // doPendingMerges() is automatically done at the very beginning
- * // of every call, including find() and areCongruent(), to ensure
- * // consistency. However, if the context pops, the pending merges
- * // up to that level are cleared.
+ * // This call is made while the merge is being done. If you
+ * // throw any exception here, you'll immediately exit the
+ * // CongruenceClosure call and will miss whatever pending
+ * // merges were being performed, leaving the CongruenceClosure
+ * // module in a bad state. Therefore if you throw, you should
+ * // only do so if you are going to backjump, re-establishing a
+ * // good (former) state. Keep this in mind if a
+ * // CVC4::Interrupted that *doesn't* lead to a backjump can
+ * // interrupt you.
* }
* };
*/
template <class OutputChannel>
class CongruenceClosure {
+ /** The context */
+ context::Context* d_context;
+
/** The output channel */
OutputChannel* d_out;
+ // typedef all of these so that iterators are easy to define
+ typedef context::CDMap<Node, Node, NodeHashFunction> RepresentativeMap;
+ typedef context::CDList<Node> ClassList;
+ typedef context::CDMap<Node, ClassList*, NodeHashFunction> ClassLists;
+ typedef context::CDList<Node> UseList;
+ typedef context::CDMap<TNode, UseList*, TNodeHashFunction> UseLists;
+ typedef context::CDMap<Node, Node, NodeHashFunction> LookupMap;
+
+ typedef context::CDMap<TNode, Node, NodeHashFunction> EqMap;
+
+ typedef context::CDMap<Node, Node, NodeHashFunction> ProofMap;
+ typedef context::CDMap<Node, Node, NodeHashFunction> ProofLabel;
+
+ RepresentativeMap d_representative;
+ ClassLists d_classList;
+ UseLists d_useList;
+ LookupMap d_lookup;
+
+ EqMap d_eqMap;
+
+ ProofMap d_proof;
+ ProofLabel d_proofLabel;
+
+ ProofMap d_proofRewrite;
+
+ /**
+ * The set of terms we care about (i.e. those that have been given
+ * us with addTerm() and their representatives).
+ */
+ typedef context::CDSet<Node, NodeHashFunction> CareSet;
+ CareSet d_careSet;
+
public:
/** Construct a congruence closure module instance */
CongruenceClosure(context::Context* ctxt, OutputChannel* out)
- throw(AssertionException);
+ throw(AssertionException) :
+ d_context(ctxt),
+ d_out(out),
+ d_representative(ctxt),
+ d_classList(ctxt),
+ d_useList(ctxt),
+ d_lookup(ctxt),
+ d_eqMap(ctxt),
+ d_proof(ctxt),
+ d_proofLabel(ctxt),
+ d_proofRewrite(ctxt),
+ d_careSet(ctxt) {
+ }
/**
- * Add a term into CC consideration.
+ * Add a term into CC consideration. This is context-dependent.
+ * Calls OutputChannel::notifyCongruent(), so it can throw anything
+ * that that function can.
*/
- void addTerm(TNode trm) throw(AssertionException);
+ void addTerm(TNode trm);
/**
- * Add an equality literal eq into CC consideration.
+ * Add an equality literal eq into CC consideration. This is
+ * context-dependent. Calls OutputChannel::notifyCongruent()
+ * indirectly, so it can throw anything that that function can.
*/
- void addEquality(TNode eq) throw(AssertionException);
+ void addEquality(TNode inputEq) {
+ Debug("cc") << "CC addEquality[" << d_context->getLevel() << "]: " << inputEq << std::endl;
+ Assert(inputEq.getKind() == kind::EQUAL);
+ NodeBuilder<> eqb(kind::EQUAL);
+ if(inputEq[1].getKind() == kind::APPLY_UF &&
+ inputEq[0].getKind() != kind::APPLY_UF) {
+ eqb << flatten(inputEq[1]) << inputEq[0];
+ } else {
+ eqb << flatten(inputEq[0]) << replace(flatten(inputEq[1]));
+ }
+ Node eq = eqb;
+ addEq(eq, inputEq);
+ }
+ void addEq(TNode eq, TNode inputEq);
+
+ Node flatten(TNode t) {
+ if(t.getKind() == kind::APPLY_UF) {
+ NodeBuilder<> appb(kind::APPLY_UF);
+ appb << replace(flatten(t.getOperator()));
+ for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
+ appb << replace(flatten(*i));
+ }
+ return Node(appb);
+ } else {
+ return t;
+ }
+ }
+
+ Node replace(TNode t) {
+ if(t.getKind() == kind::APPLY_UF) {
+ EqMap::iterator i = d_eqMap.find(t);
+ if(i == d_eqMap.end()) {
+ Node v = NodeManager::currentNM()->mkSkolem(t.getType());
+ addEq(NodeManager::currentNM()->mkNode(kind::EQUAL, t, v), TNode::null());
+ d_eqMap.insert(t, v);
+ return v;
+ } else {
+ return (*i).second;
+ }
+ } else {
+ return t;
+ }
+ }
+
+ TNode proofRewrite(TNode pfStep) {
+ ProofMap::const_iterator i = d_proofRewrite.find(pfStep);
+ if(i == d_proofRewrite.end()) {
+ return pfStep;
+ } else {
+ return (*i).second;
+ }
+ }
/**
- * Inquire whether two expressions are congruent.
+ * Inquire whether two expressions are congruent in the current
+ * context.
*/
- bool areCongruent(TNode a, TNode b) throw(AssertionException);
+ inline bool areCongruent(TNode a, TNode b) const throw(AssertionException) {
+ Debug("cc") << "CC areCongruent? " << a << " == " << b << std::endl;
+ Debug("cc") << " a " << a << std::endl;
+ Debug("cc") << " a' " << normalize(a) << std::endl;
+ Debug("cc") << " b " << b << std::endl;
+ Debug("cc") << " b' " << normalize(b) << std::endl;
+
+ Node ap = find(a), bp = find(b);
+
+ // areCongruent() works fine as just find(a) == find(b) _except_
+ // for terms not appearing in equalities. For example, let's say
+ // you have unary f and binary g, h, and
+ //
+ // a == f(b) ; f(a) == b ; g == h
+ //
+ // it's clear that h(f(a),a) == g(b,a), but it's not in the
+ // union-find even if you addTerm() on those two.
+ //
+ // we implement areCongruent() to handle more general
+ // queries---i.e., to check for new congruences---but shortcut a
+ // cheap & common case
+ //
+ return ap == bp || normalize(ap) == normalize(bp);
+ }
/**
- * Find the EC representative for a term t
+ * Find the EC representative for a term t in the current context.
*/
- TNode find(TNode t) throw(AssertionException);
+ inline TNode find(TNode t) const throw(AssertionException) {
+ context::CDMap<Node, Node, NodeHashFunction>::iterator i =
+ d_representative.find(t);
+ return (i == d_representative.end()) ? t : TNode((*i).second);
+ }
+
+ void explainAlongPath(TNode a, TNode c, std::list<std::pair<Node, Node> >& pending, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind, std::list<Node>& pf)
+ throw(AssertionException);
+
+ Node highestNode(TNode a, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind)
+ throw(AssertionException);
+
+ Node nearestCommonAncestor(TNode a, TNode b)
+ throw(AssertionException);
/**
- * Request an explanation for why a and b are in the same EC.
- * Throws a CongruenceClosureException if they aren't in the same
- * EC.
+ * Request an explanation for why a and b are in the same EC in the
+ * current context. Throws a CongruenceClosureException if they
+ * aren't in the same EC.
*/
- Node explain(TNode a, TNode b)
+ Node explain(Node a, Node b)
throw(CongruenceClosureException, AssertionException);
/**
* are in the same EC. Throws a CongruenceClosureException if they
* aren't in the same EC.
*/
- Node explain(TNode eq)
- throw(CongruenceClosureException, AssertionException);
+ inline Node explain(TNode eq)
+ throw(CongruenceClosureException, AssertionException) {
+ Assert(eq.getKind() == kind::EQUAL);
+ return explain(eq[0], eq[1]);
+ }
+
+private:
+
+ friend std::ostream& operator<< <>(std::ostream& out,
+ const CongruenceClosure<OutputChannel>& cc);
/**
- * Request that any pending merges (canceled with an
- * exception thrown from OutputChannel::merge()) be
- * performed and the OutputChannel notified.
+ * Internal propagation of information. Propagation tends to
+ * cascade (this implementation uses an iterative "pending"
+ * worklist), and "seed" is the "seeding" propagation to do (the
+ * first one). Calls OutputChannel::notifyCongruent() indirectly,
+ * so it can throw anything that that function can.
*/
- void doPendingMerges() throw(AssertionException);
-
-private:
+ void propagate(TNode seed);
/**
- * Internal propagation of information.
+ * Internal lookup mapping from tuples to equalities.
*/
- void propagate();
+ inline TNode lookup(TNode a) const {
+ context::CDMap<Node, Node, NodeHashFunction>::iterator i = d_lookup.find(a);
+ if(i == d_lookup.end()) {
+ return TNode::null();
+ } else {
+ TNode l = (*i).second;
+ Assert(l.getKind() == kind::EQUAL);
+ return l;
+ }
+ }
/**
* Internal lookup mapping.
*/
- TNode lookup(TNode a);
+ inline void setLookup(TNode a, TNode b) {
+ Assert(a.getKind() == kind::TUPLE);
+ Assert(b.getKind() == kind::EQUAL);
+ d_lookup[a] = b;
+ }
/**
- * Internal lookup mapping.
+ * Given an apply (f a1 a2...), build a TUPLE expression
+ * (f', a1', a2', ...) suitable for a lookup() key.
*/
- void setLookup(TNode a, TNode b);
+ Node buildRepresentativesOfApply(TNode apply, Kind kindToBuild = kind::TUPLE)
+ throw(AssertionException);
+
+ /**
+ * Append equality "eq" to uselist of "of".
+ */
+ inline void appendToUseList(TNode of, TNode eq) {
+ Debug("cc") << "adding " << eq << " to use list of " << of << std::endl;
+ Assert(eq.getKind() == kind::EQUAL);
+ Assert(of == find(of));
+ UseLists::iterator usei = d_useList.find(of);
+ UseList* ul;
+ if(usei == d_useList.end()) {
+ ul = new(d_context->getCMM()) UseList(true, d_context);
+ d_useList.insertDataFromContextMemory(of, ul);
+ } else {
+ ul = (*usei).second;
+ }
+ ul->push_back(eq);
+ }
+
+ /**
+ * Merge equivalence class ec1 under ec2. ec1's new union-find
+ * representative becomes ec2. Calls
+ * OutputChannel::notifyCongruent(), so it can throw anything that
+ * that function can.
+ */
+ void merge(TNode ec1, TNode ec2);
+ void mergeProof(TNode a, TNode b, TNode e);
/**
* Internal normalization.
*/
- Node normalize(TNode t);
-};
+ Node normalize(TNode t) const throw(AssertionException);
+
+};/* class CongruenceClosure */
+
+
+template <class OutputChannel>
+void CongruenceClosure<OutputChannel>::addTerm(TNode t) {
+ Node trm = replace(flatten(t));
+ Node trmp = find(trm);
+
+ Debug("cc") << "CC addTerm [" << d_careSet.size() << "] " << d_careSet.contains(t) << ": " << t << std::endl
+ << " [" << d_careSet.size() << "] " << d_careSet.contains(trm) << ": " << trm << std::endl
+ << " [" << d_careSet.size() << "] " << d_careSet.contains(trmp) << ": " << trmp << std::endl;
+
+ if(t != trm && !d_careSet.contains(t)) {
+ // we take care to only notify our client once of congruences
+ d_out->notifyCongruent(t, trm);
+ d_careSet.insert(t);
+ }
+
+ if(!d_careSet.contains(trm)) {
+ if(trm != trmp) {
+ // if part of an equivalence class headed by another node,
+ // notify the client of this merge that's already been
+ // performed..
+ d_out->notifyCongruent(trm, trmp);
+ }
+
+ // add its representative to the care set
+ d_careSet.insert(trmp);
+ }
+}
+
+
+template <class OutputChannel>
+void CongruenceClosure<OutputChannel>::addEq(TNode eq, TNode inputEq) {
+ d_proofRewrite[eq] = inputEq;
+
+ Debug("cc") << "CC addEq[" << d_context->getLevel() << "]: " << eq << std::endl;
+ Assert(eq.getKind() == kind::EQUAL);
+ Assert(eq[1].getKind() != kind::APPLY_UF);
+ if(areCongruent(eq[0], eq[1])) {
+ Debug("cc") << "CC -- redundant, ignoring...\n";
+ return;
+ }
+
+ TNode s = eq[0], t = eq[1];
+
+ Assert(s != t);
+
+ Debug("cc:detail") << "CC " << s << " == " << t << std::endl;
+
+ // change from paper: do this whether or not s, t are applications
+ Debug("cc:detail") << "CC propagating the eq" << std::endl;
+
+ if(s.getKind() != kind::APPLY_UF) {
+ // s, t are constants
+ propagate(eq);
+ } else {
+ // s is an apply, t is a constant
+ Node ap = buildRepresentativesOfApply(s);
+
+ Debug("cc:detail") << "CC rewrLHS " << "op_and_args_a == " << t << std::endl;
+ Debug("cc") << "CC ap is " << ap << std::endl;
+
+ TNode l = lookup(ap);
+ Debug("cc:detail") << "CC lookup(ap): " << l << std::endl;
+ if(!l.isNull()) {
+ // ensure a hard Node link exists to this during the call
+ Node pending = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, l);
+ Debug("cc:detail") << "pending1 " << pending << std::endl;
+ propagate(pending);
+ } else {
+ Debug("cc") << "CC lookup(ap) setting to " << eq << std::endl;
+ setLookup(ap, eq);
+ for(Node::iterator i = ap.begin(); i != ap.end(); ++i) {
+ appendToUseList(*i, eq);
+ }
+ }
+ }
+
+ Debug("cc") << *this;
+}/* addEq() */
+
+
+template <class OutputChannel>
+Node CongruenceClosure<OutputChannel>::buildRepresentativesOfApply(TNode apply,
+ Kind kindToBuild)
+ throw(AssertionException) {
+ Assert(apply.getKind() == kind::APPLY_UF);
+ NodeBuilder<> argspb(kindToBuild);
+ argspb << find(apply.getOperator());
+ for(TNode::iterator i = apply.begin(); i != apply.end(); ++i) {
+ argspb << find(*i);
+ }
+ return argspb;
+}/* buildRepresentativesOfApply() */
+
+
+template <class OutputChannel>
+void CongruenceClosure<OutputChannel>::propagate(TNode seed) {
+ Debug("cc:detail") << "=== doing a round of propagation ===" << std::endl
+ << "the \"seed\" propagation is: " << seed << std::endl;
+
+ std::list<Node> pending;
+
+ Debug("cc") << "seed propagation with: " << seed << std::endl;
+ pending.push_back(seed);
+ do { // while(!pending.empty())
+ Node e = pending.front();
+ pending.pop_front();
+
+ Debug("cc") << "=== top of propagate loop ===" << std::endl;
+ Debug("cc") << "=== e is " << e << " ===" << std::endl;
+
+ TNode a, b;
+ if(e.getKind() == kind::EQUAL) {
+ // e is an equality a = b (a, b are constants)
+
+ a = e[0];
+ b = e[1];
+
+ Debug("cc:detail") << "propagate equality: " << a << " == " << b << std::endl;
+ } else {
+ // e is a tuple ( apply f A... = a , apply f B... = b )
+
+ Debug("cc") << "propagate tuple: " << e << "\n";
+
+ Assert(e.getKind() == kind::TUPLE);
+
+ Assert(e.getNumChildren() == 2);
+ Assert(e[0].getKind() == kind::EQUAL);
+ Assert(e[1].getKind() == kind::EQUAL);
+
+ // tuple is (eq, lookup)
+ a = e[0][1];
+ b = e[1][1];
+
+ Assert(a.getKind() != kind::APPLY_UF);
+ Assert(b.getKind() != kind::APPLY_UF);
+
+ Debug("cc") << " ( " << a << " , " << b << " )" << std::endl;
+ }
+
+ Debug("cc:detail") << "=====at start=====" << std::endl
+ << "a :" << a << std::endl
+ << "NORMALIZE a:" << normalize(a) << std::endl
+ << "b :" << b << std::endl
+ << "NORMALIZE b:" << normalize(b) << std::endl
+ << "alreadyCongruent?:" << areCongruent(a,b) << std::endl;
+
+ // change from paper: need to normalize() here since in our
+ // implementation, a and b can be applications
+ Node ap = find(a), bp = find(b);
+ if(ap != bp) {
+
+ Debug("cc:detail") << "EC[a] == " << ap << std::endl
+ << "EC[b] == " << bp << std::endl;
+
+ { // w.l.o.g., |classList ap| <= |classList bp|
+ ClassLists::iterator cl_api = d_classList.find(ap);
+ ClassLists::iterator cl_bpi = d_classList.find(bp);
+ unsigned sizeA = (cl_api == d_classList.end() ? 0 : (*cl_api).second->size());
+ unsigned sizeB = (cl_bpi == d_classList.end() ? 0 : (*cl_bpi).second->size());
+ Debug("cc") << "sizeA == " << sizeA << " sizeB == " << sizeB << std::endl;
+ if(sizeA > sizeB) {
+ Debug("cc") << "swapping..\n";
+ TNode tmp = ap; ap = bp; bp = tmp;
+ tmp = a; a = b; b = tmp;
+ }
+ }
+
+ { // class list handling
+ ClassLists::iterator cl_bpi = d_classList.find(bp);
+ ClassList* cl_bp;
+ if(cl_bpi == d_classList.end()) {
+ cl_bp = new(d_context->getCMM()) ClassList(true, d_context);
+ d_classList.insertDataFromContextMemory(bp, cl_bp);
+ Debug("cc:detail") << "CC in prop alloc classlist for " << bp << std::endl;
+ } else {
+ cl_bp = (*cl_bpi).second;
+ }
+ // we don't store 'ap' in its own class list; so process it here
+ Debug("cc:detail") << "calling mergeproof/merge1 " << ap
+ << " AND " << bp << std::endl;
+ mergeProof(a, b, e);
+ merge(ap, bp);
+
+ Debug("cc") << " adding ap == " << ap << std::endl
+ << " to class list of " << bp << std::endl;
+ cl_bp->push_back(ap);
+ ClassLists::const_iterator cli = d_classList.find(ap);
+ if(cli != d_classList.end()) {
+ const ClassList* cl = (*cli).second;
+ for(ClassList::const_iterator i = cl->begin();
+ i != cl->end();
+ ++i) {
+ TNode c = *i;
+ Debug("cc") << "c is " << c << "\n"
+ << " from cl of " << ap << std::endl;
+ Debug("cc") << " it's find ptr is: " << find(c) << std::endl;
+ Assert(find(c) == ap);
+ Debug("cc:detail") << "calling merge2 " << c << bp << std::endl;
+ merge(c, bp);
+ // move c from classList(ap) to classlist(bp);
+ //i = cl.erase(i);// FIXME do we need to?
+ Debug("cc") << " adding c to class list of " << bp << std::endl;
+ cl_bp->push_back(c);
+ }
+ }
+ Debug("cc:detail") << "bottom\n";
+ }
+
+ { // use list handling
+ Debug("cc:detail") << "ap is " << ap << std::endl;
+ Debug("cc:detail") << "find(ap) is " << find(ap) << std::endl;
+ Debug("cc:detail") << "CC in prop go through useList of " << ap << std::endl;
+ UseLists::iterator usei = d_useList.find(ap);
+ if(usei != d_useList.end()) {
+ UseList* ul = (*usei).second;
+ //for( f(c1,c2)=c in UseList(ap) )
+ for(UseList::const_iterator i = ul->begin();
+ i != ul->end();
+ ++i) {
+ TNode eq = *i;
+ Debug("cc") << "CC -- useList: " << eq << std::endl;
+ Assert(eq.getKind() == kind::EQUAL);
+ // change from paper
+ // use list elts can have form (apply c..) = x OR x = (apply c..)
+ Assert(eq[0].getKind() == kind::APPLY_UF || eq[1].getKind() == kind::APPLY_UF);
+ // do for each side that is an application
+ for(int side = 0; side <= 1; ++side) {
+ if(eq[side].getKind() != kind::APPLY_UF) {
+ continue;
+ }
+
+ Node cp = buildRepresentativesOfApply(eq[side]);
+
+ // if lookup(c1',c2') is some f(d1,d2)=d then
+ TNode n = lookup(cp);
+
+ Debug("cc:detail") << "CC -- c' is " << cp << std::endl;
+
+ if(!n.isNull()) {
+ Debug("cc:detail") << "CC -- lookup(c') is " << n << std::endl;
+ // add (f(c1,c2)=c,f(d1,d2)=d) to pending
+ Node tuple = NodeManager::currentNM()->mkNode(kind::TUPLE, eq, n);
+ Debug("cc") << "CC add tuple to pending: " << tuple << std::endl;
+ pending.push_back(tuple);
+ // remove f(c1,c2)=c from UseList(ap)
+ Debug("cc:detail") << "supposed to remove " << eq << std::endl
+ << " from UseList of " << ap << std::endl;
+ //i = ul.erase(i);// FIXME do we need to?
+ } else {
+ Debug("cc") << "CC -- lookup(c') is null" << std::endl;
+ Debug("cc") << "CC -- setlookup(c') to " << eq << std::endl;
+ // set lookup(c1',c2') to f(c1,c2)=c
+ setLookup(cp, eq);
+ // move f(c1,c2)=c from UseList(ap) to UseList(b')
+ //i = ul.erase(i);// FIXME do we need to remove from UseList(ap) ?
+ appendToUseList(bp, eq);
+ }
+ }
+ }
+ }
+ }/* use lists */
+ Debug("cc:detail") << "CC in prop done with useList of " << ap << std::endl;
+ } else {
+ Debug("cc:detail") << "CCs the same ( == " << ap << "), do nothing."
+ << std::endl;
+ }
+
+ Debug("cc") << "=====at end=====" << std::endl
+ << "a :" << a << std::endl
+ << "NORMALIZE a:" << normalize(a) << std::endl
+ << "b :" << b << std::endl
+ << "NORMALIZE b:" << normalize(b) << std::endl
+ << "alreadyCongruent?:" << areCongruent(a,b) << std::endl;
+ Assert(areCongruent(a, b));
+ } while(!pending.empty());
+}/* propagate() */
+
+
+template <class OutputChannel>
+void CongruenceClosure<OutputChannel>::merge(TNode ec1, TNode ec2) {
+ /*
+ Debug("cc:detail") << " -- merging " << ec1
+ << (d_careSet.find(ec1) == d_careSet.end() ?
+ " -- NOT in care set" : " -- IN CARE SET") << std::endl
+ << " and " << ec2
+ << (d_careSet.find(ec2) == d_careSet.end() ?
+ " -- NOT in care set" : " -- IN CARE SET") << std::endl;
+ */
+
+ Debug("cc") << "CC setting rep of " << ec1 << std::endl;
+ Debug("cc") << "CC to " << ec2 << std::endl;
+
+ /* can now be applications
+ Assert(ec1.getKind() != kind::APPLY_UF);
+ Assert(ec2.getKind() != kind::APPLY_UF);
+ */
+
+ Assert(find(ec1) != ec2);
+ //Assert(find(ec1) == ec1);
+ Assert(find(ec2) == ec2);
+
+ d_representative[ec1] = ec2;
+
+ if(d_careSet.find(ec1) != d_careSet.end()) {
+ d_careSet.insert(ec2);
+ d_out->notifyCongruent(ec1, ec2);
+ }
+}/* merge() */
+
+
+template <class OutputChannel>
+void CongruenceClosure<OutputChannel>::mergeProof(TNode a, TNode b, TNode e) {
+ Debug("cc") << " -- merge-proofing " << a << "\n"
+ << " and " << b << "\n"
+ << " with " << e << "\n";
+
+ // proof forest gets a -> b labeled with e
+
+ // first reverse all the edges in proof forest to root of this proof tree
+ Debug("cc") << "CC PROOF reversing proof tree\n";
+ // c and p are child and parent in (old) proof tree
+ Node c = a, p = d_proof[a], edgePf = d_proofLabel[a];
+ // when we hit null p, we're at the (former) root
+ Debug("cc") << "CC PROOF start at c == " << c << std::endl
+ << " p == " << p << std::endl
+ << " edgePf == " << edgePf << std::endl;
+ while(!p.isNull()) {
+ // in proof forest,
+ // we have edge c --edgePf-> p
+ // turn it into c <-edgePf-- p
+
+ Node pParSave = d_proof[p];
+ Node pLabelSave = d_proofLabel[p];
+ d_proof[p] = c;
+ d_proofLabel[p] = edgePf;
+ c = p;
+ p = pParSave;
+ edgePf = pLabelSave;
+ Debug("cc") << "CC PROOF now at c == " << c << std::endl
+ << " p == " << p << std::endl
+ << " edgePf == " << edgePf << std::endl;
+ }
+
+ // add an edge from a to b
+ d_proof[a] = b;
+ d_proofLabel[a] = e;
+}/* mergeProof() */
+
+
+template <class OutputChannel>
+Node CongruenceClosure<OutputChannel>::normalize(TNode t) const
+ throw(AssertionException) {
+ Debug("cc:detail") << "normalize " << t << std::endl;
+ if(t.getKind() != kind::APPLY_UF) {// t is a constant
+ t = find(t);
+ Debug("cc:detail") << " find " << t << std::endl;
+ return t;
+ } else {// t is an apply
+ NodeBuilder<> apb(kind::TUPLE);
+ TNode op = t.getOperator();
+ Node n = normalize(op);
+ apb << n;
+ bool allConstants = (n.getKind() != kind::APPLY_UF);
+ for(TNode::iterator i = t.begin(); i != t.end(); ++i) {
+ TNode c = *i;
+ n = normalize(c);
+ apb << n;
+ allConstants = (allConstants && n.getKind() != kind::APPLY_UF);
+ }
+
+ Node ap = apb;
+ Debug("cc:detail") << " got ap " << ap << std::endl;
+
+ Node theLookup = lookup(ap);
+ if(allConstants && !theLookup.isNull()) {
+ Assert(theLookup.getKind() == kind::EQUAL);
+ Assert(theLookup[0].getKind() == kind::APPLY_UF);
+ Assert(theLookup[1].getKind() != kind::APPLY_UF);
+ return find(theLookup[1]);
+ } else {
+ NodeBuilder<> fa(kind::APPLY_UF);
+ for(Node::iterator i = ap.begin(); i != ap.end(); ++i) {
+ fa << *i;
+ }
+ // ensure a hard Node link exists during the call
+ Node n = fa;
+ return n;
+ }
+ }
+}/* normalize() */
+
+
+template <class OutputChannel>
+Node CongruenceClosure<OutputChannel>::highestNode(TNode a, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind)
+ throw(AssertionException) {
+ __gnu_cxx::hash_map<Node, Node, NodeHashFunction>::iterator i = unionFind.find(a);
+ if(i == unionFind.end()) {
+ return a;
+ } else {
+ return unionFind[a] = highestNode((*i).second, unionFind);
+ }
+}
+
+
+template <class OutputChannel>
+void CongruenceClosure<OutputChannel>::explainAlongPath(TNode a, TNode c, std::list<std::pair<Node, Node> >& pending, __gnu_cxx::hash_map<Node, Node, NodeHashFunction>& unionFind, std::list<Node>& pf)
+ throw(AssertionException) {
+
+ a = highestNode(a, unionFind);
+ Assert(c == highestNode(c, unionFind));
+
+ while(a != c) {
+ Node b = d_proof[a];
+ Node e = d_proofLabel[a];
+ if(e.getKind() == kind::EQUAL) {
+ pf.push_back(e);
+ } else {
+ Assert(e.getKind() == kind::TUPLE);
+ pf.push_back(e[0]);
+ pf.push_back(e[1]);
+ Assert(e[0][0].getKind() == kind::APPLY_UF);
+ Assert(e[0][1].getKind() != kind::APPLY_UF);
+ Assert(e[1][0].getKind() == kind::APPLY_UF);
+ Assert(e[1][1].getKind() != kind::APPLY_UF);
+ Assert(e[0][0].getNumChildren() == e[1][0].getNumChildren());
+ pending.push_back(std::make_pair(e[0][0].getOperator(), e[1][0].getOperator()));
+ for(int i = 0, nc = e[0][0].getNumChildren(); i < nc; ++i) {
+ pending.push_back(std::make_pair(e[0][0][i], e[1][0][i]));
+ }
+ }
+ unionFind[a] = b;
+ a = highestNode(b, unionFind);
+ }
+}/* explainAlongPath() */
+
+
+template <class OutputChannel>
+Node CongruenceClosure<OutputChannel>::nearestCommonAncestor(TNode a, TNode b)
+ throw(AssertionException) {
+ Assert(find(a) == find(b));
+ return find(a); // FIXME
+}/* nearestCommonAncestor() */
+
+
+template <class OutputChannel>
+Node CongruenceClosure<OutputChannel>::explain(Node a, Node b)
+ throw(CongruenceClosureException, AssertionException) {
+
+ Assert(a != b);
+
+ if(!areCongruent(a, b)) {
+ throw CongruenceClosureException("asked to explain() congruence of nodes "
+ "that aren't congruent");
+ }
+
+ if(a.getKind() == kind::APPLY_UF) {
+ a = replace(flatten(a));
+ }
+ if(b.getKind() == kind::APPLY_UF) {
+ b = replace(flatten(b));
+ }
+
+ std::list<std::pair<Node, Node> > pending;
+ __gnu_cxx::hash_map<Node, Node, NodeHashFunction> unionFind;
+ std::list<Node> terms;
+
+ pending.push_back(std::make_pair(a, b));
+
+ Debug("cc") << "CC EXPLAINING " << a << " == " << b << std::endl;
+
+ do {// while(!pending.empty())
+ std::pair<Node, Node> eq = pending.front();
+ pending.pop_front();
+
+ a = eq.first;
+ b = eq.second;
+
+ Node c = nearestCommonAncestor(a, b);
+
+ explainAlongPath(a, c, pending, unionFind, terms);
+ explainAlongPath(b, c, pending, unionFind, terms);
+ } while(!pending.empty());
+
+ Debug("cc") << "CC EXPLAIN final proof has size " << terms.size() << std::endl;
+
+ NodeBuilder<> pf(kind::AND);
+ while(!terms.empty()) {
+ Node p = terms.front();
+ terms.pop_front();
+ Debug("cc") << "CC EXPLAIN " << p << std::endl;
+ p = proofRewrite(p);
+ Debug("cc") << " rewrite " << p << std::endl;
+ if(!p.isNull()) {
+ pf << p;
+ }
+ }
+
+ Debug("cc") << "CC EXPLAIN done" << std::endl;
+
+ Assert(pf.getNumChildren() > 0);
+
+ if(pf.getNumChildren() == 1) {
+ return pf[0];
+ } else {
+ return pf;
+ }
+}/* explain() */
+
+
+template <class OutputChannel>
+std::ostream& operator<<(std::ostream& out,
+ const CongruenceClosure<OutputChannel>& cc) {
+ out << "==============================================" << std::endl;
+
+ out << "Representatives:" << std::endl;
+ for(typename CongruenceClosure<OutputChannel>::RepresentativeMap::const_iterator i = cc.d_representative.begin(); i != cc.d_representative.end(); ++i) {
+ out << " " << (*i).first << " => " << (*i).second << std::endl;
+ }
+
+ out << "ClassLists:" << std::endl;
+ for(typename CongruenceClosure<OutputChannel>::ClassLists::const_iterator i = cc.d_classList.begin(); i != cc.d_classList.end(); ++i) {
+ if(cc.find((*i).first) == (*i).first) {
+ out << " " << (*i).first << " =>" << std::endl;
+ for(typename CongruenceClosure<OutputChannel>::ClassList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) {
+ out << " " << *j << std::endl;
+ }
+ }
+ }
+
+ out << "UseLists:" << std::endl;
+ for(typename CongruenceClosure<OutputChannel>::UseLists::const_iterator i = cc.d_useList.begin(); i != cc.d_useList.end(); ++i) {
+ if(cc.find((*i).first) == (*i).first) {
+ out << " " << (*i).first << " =>" << std::endl;
+ for(typename CongruenceClosure<OutputChannel>::UseList::const_iterator j = (*i).second->begin(); j != (*i).second->end(); ++j) {
+ out << " " << *j << std::endl;
+ }
+ }
+ }
+
+ out << "Lookup:" << std::endl;
+ for(typename CongruenceClosure<OutputChannel>::LookupMap::const_iterator i = cc.d_lookup.begin(); i != cc.d_lookup.end(); ++i) {
+ TNode n = (*i).second;
+ out << " " << (*i).first << " => " << n << std::endl;
+ }
+
+ out << "==============================================" << std::endl;
+
+ return out;
+}
+
}/* CVC4 namespace */
/** The input language */
parser::InputLanguage lang;
+ /** Enumeration of UF implementation choices */
+ typedef enum { TIM, MORGAN } UfImplementation;
+
+ /** Which implementation of uninterpreted function theory to use */
+ UfImplementation uf_implementation;
+
/** Should we exit after parsing? */
bool parseOnly;
err(0),
verbosity(0),
lang(parser::LANG_AUTO),
+ uf_implementation(MORGAN),
parseOnly(false),
semanticChecks(true),
memoryMap(false),
{}
};/* struct Options */
+inline std::ostream& operator<<(std::ostream& out, Options::UfImplementation uf) {
+ switch(uf) {
+ case Options::TIM:
+ out << "TIM";
+ break;
+ case Options::MORGAN:
+ out << "MORGAN";
+ break;
+ default:
+ out << "UfImplementation:UNKNOWN![" << unsigned(uf) << "]";
+ }
+
+ return out;
+}
+
}/* CVC4 namespace */
#endif /* __CVC4__OPTIONS_H */
blu='\e[1;34m'; \
std='\e[m'; \
}
-subdirs_to_check = unit system regress/regress0 regress/regress1 regress/regress2 regress/regress3
+subdirs_to_check = unit system regress/regress0 regress/regress0/uf regress/regress0/precedence regress/regress1 regress/regress2 regress/regress3
check-recursive: check-pre
.PHONY: check-pre
check-pre:
SUBDIRS = regress0
DIST_SUBDIRS = regress0 regress1 regress2 regress3
+MAKEFLAGS = -k
+
export VERBOSE = 1
.PHONY: regress0 regress1 regress2 regress3
SUBDIRS = . precedence uf
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
euf_simp11.smt \
euf_simp12.smt \
euf_simp13.smt \
+ eq_diamond1.smt \
dead_dnd002.smt \
iso_brn001.smt \
- SEQ032_size2.smt \
simple.01.cvc \
simple.02.cvc \
simple.03.cvc \
SUBDIRS = .
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
SUBDIRS = .
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
SUBDIRS = .
TESTS_ENVIRONMENT = @srcdir@/../run_regression @top_builddir@/src/main/cvc4
+MAKEFLAGS = -k
# These are run for all build profiles.
# If a test shouldn't be run in e.g. competition mode,
theory/shared_term_manager_black \
theory/theory_engine_white \
theory/theory_black \
- theory/theory_uf_white \
+ theory/theory_uf_tim_white \
theory/theory_arith_white \
expr/expr_public \
expr/expr_manager_public \
util/assert_white \
util/bitvector_black \
util/configuration_black \
+ util/congruence_closure_white \
util/output_black \
util/exception_black \
util/integer_black \
else \
echo; \
echo "ERROR:"; \
- echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \
- echo "ERROR: The tests should be generated for the user and included in the tarball,"; \
+ echo "ERROR: You cannot make dist in this build directory, you do not have CxxTest."; \
+ echo "ERROR: The tests should be generated for the user and included in the tarball,"; \
echo "ERROR: otherwise they'll be required to have CxxTest just to test the standard"; \
echo "ERROR: distribution built correctly."; \
echo "ERROR: If you really want to do this, append the following to your make command."; \
echo "ERROR:"; \
- echo "ERROR: I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \
+ echo "ERROR: I_REALLY_WANT_TO_BUILD_CVC4_DIST_WITHOUT_TESTS=1"; \
echo "ERROR:"; \
echo; \
exit 1; \
TS_ASSERT_DIFFERS(VarNameAttr::s_id, TestStringAttr2::s_id);
TS_ASSERT_DIFFERS(TestStringAttr1::s_id, TestStringAttr2::s_id);
- lastId = attr::LastAttributeId<void*, false>::s_id;
- TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
+ //lastId = attr::LastAttributeId<void*, false>::s_id;
+ //TS_ASSERT_LESS_THAN(theory::uf::ECAttr::s_id, lastId);
lastId = attr::LastAttributeId<bool, false>::s_id;
TS_ASSERT_LESS_THAN(theory::Theory::PreRegisteredAttr::s_id, lastId);
#include "context/context.h"
#include "util/rational.h"
#include "util/integer.h"
+#include "util/options.h"
#include "util/Assert.h"
using namespace CVC4;
NodeManager* d_nm;
NodeManagerScope* d_scope;
TheoryEngine* d_theoryEngine;
+ Options d_options;
public:
d_nm = new NodeManager(d_ctxt);
d_scope = new NodeManagerScope(d_nm);
- d_theoryEngine = new TheoryEngine(d_ctxt);
-
+ d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
}
void tearDown() {
+ d_theoryEngine->shutdown();
delete d_theoryEngine;
delete d_scope;
#include "context/context.h"
#include "util/rational.h"
#include "util/integer.h"
+#include "util/options.h"
#include "util/Assert.h"
using namespace CVC4;
FakeOutputChannel *d_nullChannel;
FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv;
TheoryEngine* d_theoryEngine;
+ Options d_options;
public:
d_bv = new FakeTheory(d_ctxt, *d_nullChannel, "BV");
// create the TheoryEngine
- d_theoryEngine = new TheoryEngine(d_ctxt);
+ d_theoryEngine = new TheoryEngine(d_ctxt, &d_options);
// insert our fake versions into the TheoryEngine's theoryOf table
d_theoryEngine->d_theoryOfTable.
}
void tearDown() {
+ d_theoryEngine->shutdown();
delete d_theoryEngine;
delete d_bv;
--- /dev/null
+/********************* */
+/*! \file theory_uf_white.h
+ ** \verbatim
+ ** Original author: taking
+ ** Major contributors: mdeters
+ ** Minor contributors (to current version): dejan
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::theory::uf::tim::TheoryUFTim.
+ **
+ ** White box testing of CVC4::theory::uf::tim::TheoryUFTim.
+ **/
+
+#include <cxxtest/TestSuite.h>
+
+#include "theory/theory.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/tim/theory_uf_tim.h"
+#include "expr/node.h"
+#include "expr/node_manager.h"
+#include "context/context.h"
+
+#include "theory/theory_test_utils.h"
+
+#include <vector>
+
+using namespace CVC4;
+using namespace CVC4::theory;
+using namespace CVC4::theory::uf;
+using namespace CVC4::theory::uf::tim;
+using namespace CVC4::expr;
+using namespace CVC4::context;
+
+using namespace std;
+
+
+class TheoryUFTimWhite : public CxxTest::TestSuite {
+
+ Context* d_ctxt;
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+
+ TestOutputChannel d_outputChannel;
+ Theory::Effort d_level;
+
+ TheoryUFTim* d_euf;
+
+ TypeNode* d_booleanType;
+
+public:
+
+ TheoryUFTimWhite() : d_level(Theory::FULL_EFFORT) {}
+
+ void setUp() {
+ d_ctxt = new Context;
+ d_nm = new NodeManager(d_ctxt);
+ d_scope = new NodeManagerScope(d_nm);
+ d_outputChannel.clear();
+ d_euf = new TheoryUFTim(0, d_ctxt, d_outputChannel);
+
+ d_booleanType = new TypeNode(d_nm->booleanType());
+ }
+
+ void tearDown() {
+ delete d_booleanType;
+ delete d_euf;
+ d_outputChannel.clear();
+ delete d_scope;
+ delete d_nm;
+ delete d_ctxt;
+ }
+
+ void testPushPopSimple() {
+ TypeNode t = d_nm->mkSort();
+ Node x = d_nm->mkVar(t);
+ Node x_eq_x = x.eqNode(x);
+
+ d_ctxt->push();
+ d_ctxt->pop();
+ }
+
+// FIXME: This is broken because of moving registration into theory_engine @CB
+// // void testPushPopChain() {
+// // Node x = d_nm->mkVar(*d_booleanType);
+// // Node f = d_nm->mkVar(*d_booleanType);
+// // Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+// // Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+// // Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
+// // Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
+// // Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, 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 f1_x_neq_x = f_x.eqNode(x).notNode();
+
+// // Node expectedConflict = d_nm->mkNode(kind::AND,
+// // f1_x_neq_x,
+// // f3_x_eq_x,
+// // f5_x_eq_x
+// // );
+
+// // d_euf->assertFact( f3_x_eq_x );
+// // d_euf->assertFact( f1_x_neq_x );
+// // d_euf->check(d_level);
+// // d_ctxt->push();
+
+// // d_euf->assertFact( f5_x_eq_x );
+// // d_euf->check(d_level);
+
+// // TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
+// // TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
+// // Node realConflict = d_outputChannel.getIthNode(0);
+// // TS_ASSERT_EQUALS(expectedConflict, realConflict);
+
+// // d_ctxt->pop();
+// // d_euf->check(d_level);
+
+// // //Test that no additional calls to the output channel occurred.
+// // TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
+
+// // d_euf->assertFact( f5_x_eq_x );
+
+// // d_euf->check(d_level);
+
+// // TS_ASSERT_EQUALS(2u, 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(*d_booleanType);
+// Node f = d_nm->mkVar(*d_booleanType);
+// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+// Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
+
+// Node f_f_x_eq_x = f_f_x.eqNode(x);
+// Node f_f_f_x_neq_f_x = (f_f_f_x.eqNode(f_x)).notNode();
+
+// Node expectedConflict = f_f_f_x_neq_f_x.andNode(f_f_x_eq_x);
+
+// d_euf->assertFact(f_f_x_eq_x);
+// d_euf->assertFact(f_f_f_x_neq_f_x);
+// d_euf->check(d_level);
+
+// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
+// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
+
+// Node realConflict = d_outputChannel.getIthNode(0);
+// TS_ASSERT_EQUALS(expectedConflict, realConflict);
+
+// }
+
+ /* test that !(x == x) is inconsistent */
+// void testSelfInconsistent() {
+// Node x = d_nm->mkVar(*d_booleanType);
+// Node x_neq_x = (x.eqNode(x)).notNode();
+
+// d_euf->assertFact(x_neq_x);
+// d_euf->check(d_level);
+
+// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
+// TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0));
+// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
+// }
+
+// /* test that (x == x) is consistent */
+// void testSelfConsistent() {
+// Node x = d_nm->mkVar(*d_booleanType);
+// Node x_eq_x = x.eqNode(x);
+
+// d_euf->assertFact(x_eq_x);
+// d_euf->check(d_level);
+
+// TS_ASSERT_EQUALS(0u, d_outputChannel.getNumCalls());
+// }
+
+
+// /* test that
+// {f(f(f(x))) == x,
+// f(f(f(f(f(x))))) = x,
+// f(x) != x
+// } is inconsistent */
+// void testChain() {
+// Node x = d_nm->mkVar(*d_booleanType);
+// Node f = d_nm->mkVar(*d_booleanType);
+// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
+// Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
+// Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
+// Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, 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 f1_x_neq_x = f_x.eqNode(x).notNode();
+
+// Node expectedConflict = d_nm->mkNode(kind::AND,
+// f1_x_neq_x,
+// f3_x_eq_x,
+// f5_x_eq_x
+// );
+
+// d_euf->assertFact( f3_x_eq_x );
+// d_euf->assertFact( f5_x_eq_x );
+// d_euf->assertFact( f1_x_neq_x );
+// d_euf->check(d_level);
+
+// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
+// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
+// Node realConflict = d_outputChannel.getIthNode(0);
+// TS_ASSERT_EQUALS(expectedConflict, realConflict);
+// }
+
+
+// void testPushPopA() {
+// Node x = d_nm->mkVar(*d_booleanType);
+// Node x_eq_x = x.eqNode(x);
+
+// d_ctxt->push();
+// d_euf->assertFact( x_eq_x );
+// d_euf->check(d_level);
+// d_ctxt->pop();
+// d_euf->check(d_level);
+// }
+
+// void testPushPopB() {
+// Node x = d_nm->mkVar(*d_booleanType);
+// Node f = d_nm->mkVar(*d_booleanType);
+// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
+// Node f_x_eq_x = f_x.eqNode(x);
+
+// d_euf->assertFact( f_x_eq_x );
+// d_ctxt->push();
+// d_euf->check(d_level);
+// d_ctxt->pop();
+// d_euf->check(d_level);
+// }
+
+};
+++ /dev/null
-/********************* */
-/*! \file theory_uf_white.h
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): dejan
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief White box testing of CVC4::theory::uf::TheoryUF.
- **
- ** White box testing of CVC4::theory::uf::TheoryUF.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "theory/theory.h"
-#include "theory/uf/theory_uf.h"
-#include "expr/node.h"
-#include "expr/node_manager.h"
-#include "context/context.h"
-
-#include "theory/theory_test_utils.h"
-
-#include <vector>
-
-using namespace CVC4;
-using namespace CVC4::theory;
-using namespace CVC4::theory::uf;
-using namespace CVC4::expr;
-using namespace CVC4::context;
-
-using namespace std;
-
-
-class TheoryUFWhite : public CxxTest::TestSuite {
-
- Context* d_ctxt;
- NodeManager* d_nm;
- NodeManagerScope* d_scope;
-
- TestOutputChannel d_outputChannel;
- Theory::Effort d_level;
-
- TheoryUF* d_euf;
-
- TypeNode* d_booleanType;
-
-public:
-
- TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {}
-
- void setUp() {
- d_ctxt = new Context;
- d_nm = new NodeManager(d_ctxt);
- d_scope = new NodeManagerScope(d_nm);
- d_outputChannel.clear();
- d_euf = new TheoryUF(0, d_ctxt, d_outputChannel);
-
- d_booleanType = new TypeNode(d_nm->booleanType());
- }
-
- void tearDown() {
- delete d_booleanType;
- delete d_euf;
- d_outputChannel.clear();
- delete d_scope;
- delete d_nm;
- delete d_ctxt;
- }
-
- void testPushPopSimple() {
- TypeNode t = d_nm->mkSort();
- Node x = d_nm->mkVar(t);
- Node x_eq_x = x.eqNode(x);
-
- d_ctxt->push();
- d_ctxt->pop();
- }
-
-// FIXME: This is broken because of moving registration into theory_engine @CB
-// // void testPushPopChain() {
-// // Node x = d_nm->mkVar(*d_booleanType);
-// // Node f = d_nm->mkVar(*d_booleanType);
-// // Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-// // Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-// // Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
-// // Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
-// // Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, 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 f1_x_neq_x = f_x.eqNode(x).notNode();
-
-// // Node expectedConflict = d_nm->mkNode(kind::AND,
-// // f1_x_neq_x,
-// // f3_x_eq_x,
-// // f5_x_eq_x
-// // );
-
-// // d_euf->assertFact( f3_x_eq_x );
-// // d_euf->assertFact( f1_x_neq_x );
-// // d_euf->check(d_level);
-// // d_ctxt->push();
-
-// // d_euf->assertFact( f5_x_eq_x );
-// // d_euf->check(d_level);
-
-// // TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-// // TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-// // Node realConflict = d_outputChannel.getIthNode(0);
-// // TS_ASSERT_EQUALS(expectedConflict, realConflict);
-
-// // d_ctxt->pop();
-// // d_euf->check(d_level);
-
-// // //Test that no additional calls to the output channel occurred.
-// // TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-
-// // d_euf->assertFact( f5_x_eq_x );
-
-// // d_euf->check(d_level);
-
-// // TS_ASSERT_EQUALS(2u, 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(*d_booleanType);
-// Node f = d_nm->mkVar(*d_booleanType);
-// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-// Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
-
-// Node f_f_x_eq_x = f_f_x.eqNode(x);
-// Node f_f_f_x_neq_f_x = (f_f_f_x.eqNode(f_x)).notNode();
-
-// Node expectedConflict = f_f_f_x_neq_f_x.andNode(f_f_x_eq_x);
-
-// d_euf->assertFact(f_f_x_eq_x);
-// d_euf->assertFact(f_f_f_x_neq_f_x);
-// d_euf->check(d_level);
-
-// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-
-// Node realConflict = d_outputChannel.getIthNode(0);
-// TS_ASSERT_EQUALS(expectedConflict, realConflict);
-
-// }
-
- /* test that !(x == x) is inconsistent */
-// void testSelfInconsistent() {
-// Node x = d_nm->mkVar(*d_booleanType);
-// Node x_neq_x = (x.eqNode(x)).notNode();
-
-// d_euf->assertFact(x_neq_x);
-// d_euf->check(d_level);
-
-// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-// TS_ASSERT_EQUALS(x_neq_x, d_outputChannel.getIthNode(0));
-// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-// }
-
-// /* test that (x == x) is consistent */
-// void testSelfConsistent() {
-// Node x = d_nm->mkVar(*d_booleanType);
-// Node x_eq_x = x.eqNode(x);
-
-// d_euf->assertFact(x_eq_x);
-// d_euf->check(d_level);
-
-// TS_ASSERT_EQUALS(0u, d_outputChannel.getNumCalls());
-// }
-
-
-// /* test that
-// {f(f(f(x))) == x,
-// f(f(f(f(f(x))))) = x,
-// f(x) != x
-// } is inconsistent */
-// void testChain() {
-// Node x = d_nm->mkVar(*d_booleanType);
-// Node f = d_nm->mkVar(*d_booleanType);
-// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-// Node f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_x);
-// Node f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_x);
-// Node f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, f, f_f_f_x);
-// Node f_f_f_f_f_x = d_nm->mkNode(kind::APPLY_UF, 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 f1_x_neq_x = f_x.eqNode(x).notNode();
-
-// Node expectedConflict = d_nm->mkNode(kind::AND,
-// f1_x_neq_x,
-// f3_x_eq_x,
-// f5_x_eq_x
-// );
-
-// d_euf->assertFact( f3_x_eq_x );
-// d_euf->assertFact( f5_x_eq_x );
-// d_euf->assertFact( f1_x_neq_x );
-// d_euf->check(d_level);
-
-// TS_ASSERT_EQUALS(1u, d_outputChannel.getNumCalls());
-// TS_ASSERT_EQUALS(CONFLICT, d_outputChannel.getIthCallType(0));
-// Node realConflict = d_outputChannel.getIthNode(0);
-// TS_ASSERT_EQUALS(expectedConflict, realConflict);
-// }
-
-
-// void testPushPopA() {
-// Node x = d_nm->mkVar(*d_booleanType);
-// Node x_eq_x = x.eqNode(x);
-
-// d_ctxt->push();
-// d_euf->assertFact( x_eq_x );
-// d_euf->check(d_level);
-// d_ctxt->pop();
-// d_euf->check(d_level);
-// }
-
-// void testPushPopB() {
-// Node x = d_nm->mkVar(*d_booleanType);
-// Node f = d_nm->mkVar(*d_booleanType);
-// Node f_x = d_nm->mkNode(kind::APPLY_UF, f, x);
-// Node f_x_eq_x = f_x.eqNode(x);
-
-// d_euf->assertFact( f_x_eq_x );
-// d_ctxt->push();
-// d_euf->check(d_level);
-// d_ctxt->pop();
-// d_euf->check(d_level);
-// }
-
-};
--- /dev/null
+/********************* */
+/*! \file congruence_closure_white.h
+ ** \verbatim
+ ** Original author: mdeters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 prototype.
+ ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys)
+ ** Courant Institute of Mathematical Sciences
+ ** New York University
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief White box testing of CVC4::CongruenceClosure.
+ **
+ ** White box testing of CVC4::CongruenceClosure.
+ **/
+
+#include <cxxtest/TestSuite.h>
+#include <sstream>
+
+#include "context/context.h"
+#include "context/cdset.h"
+#include "context/cdmap.h"
+#include "expr/node.h"
+#include "expr/kind.h"
+#include "expr/node_manager.h"
+#include "util/congruence_closure.h"
+
+
+using namespace CVC4;
+using namespace CVC4::context;
+using namespace std;
+
+
+struct MyOutputChannel {
+ CDSet<Node, NodeHashFunction> d_notifications;
+ CDMap<Node, Node, NodeHashFunction> d_equivalences;
+ NodeManager* d_nm;
+
+ MyOutputChannel(Context* ctxt, NodeManager* nm) :
+ d_notifications(ctxt),
+ d_equivalences(ctxt),
+ d_nm(nm) {
+ }
+
+ bool saw(TNode a, TNode b) {
+ return d_notifications.contains(d_nm->mkNode(kind::EQUAL, a, b)) ||
+ d_notifications.contains(d_nm->mkNode(kind::EQUAL, b, a));
+ }
+
+ TNode find(TNode n) {
+ CDMap<Node, Node, NodeHashFunction>::iterator i = d_equivalences.find(n);
+ if(i == d_equivalences.end()) {
+ return n;
+ } else {
+ // lazy path compression
+ TNode p = (*i).second; // parent
+ TNode f = d_equivalences[n] = find(p); // compress
+ return f;
+ }
+ }
+
+ bool areCongruent(TNode a, TNode b) {
+ Debug("cc") << "=== a is " << a << std::endl
+ << "=== a' is " << find(a) << std::endl
+ << "=== b is " << b << std::endl
+ << "=== b' is " << find(b) << std::endl;
+
+ return find(a) == find(b);
+ }
+
+ void notifyCongruent(TNode a, TNode b) {
+ Debug("cc") << "======OI! I've been notified of: "
+ << a << " == " << b << std::endl;
+
+ Node eq = d_nm->mkNode(kind::EQUAL, a, b);
+ Node eqRev = d_nm->mkNode(kind::EQUAL, b, a);
+
+ TS_ASSERT(!d_notifications.contains(eq));
+ TS_ASSERT(!d_notifications.contains(eqRev));
+
+ d_notifications.insert(eq);
+
+ d_equivalences.insert(a, b);
+ }
+};/* class MyOutputChannel */
+
+
+class CongruenceClosureWhite : public CxxTest::TestSuite {
+ Context* d_context;
+ NodeManager* d_nm;
+ NodeManagerScope* d_scope;
+ MyOutputChannel* d_out;
+ CongruenceClosure<MyOutputChannel>* d_cc;
+
+ TypeNode U;
+ Node a, f, fa, ffa, fffa, ffffa, b, fb, ffb, fffb, ffffb;
+ Node g, gab, gba, gfafb, gfbfa, gfaa, gbfb;
+ Node h, hab, hba, hfaa;
+ Node a_eq_b, fa_eq_b, a_eq_fb, fa_eq_fb, h_eq_g;
+public:
+
+ void setUp() {
+ d_context = new Context;
+ d_nm = new NodeManager(d_context);
+ d_scope = new NodeManagerScope(d_nm);
+ d_out = new MyOutputChannel(d_context, d_nm);
+ d_cc = new CongruenceClosure<MyOutputChannel>(d_context, d_out);
+
+ U = d_nm->mkSort("U");
+
+ f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U));
+ a = d_nm->mkVar("a", U);
+ fa = d_nm->mkNode(kind::APPLY_UF, f, a);
+ ffa = d_nm->mkNode(kind::APPLY_UF, f, fa);
+ fffa = d_nm->mkNode(kind::APPLY_UF, f, ffa);
+ ffffa = d_nm->mkNode(kind::APPLY_UF, f, fffa);
+ b = d_nm->mkVar("b", U);
+ fb = d_nm->mkNode(kind::APPLY_UF, f, b);
+ ffb = d_nm->mkNode(kind::APPLY_UF, f, fb);
+ fffb = d_nm->mkNode(kind::APPLY_UF, f, ffb);
+ ffffb = d_nm->mkNode(kind::APPLY_UF, f, fffb);
+ vector<TypeNode> args(2, U);
+ g = d_nm->mkVar("g", d_nm->mkFunctionType(args, U));
+ gab = d_nm->mkNode(kind::APPLY_UF, g, a, b);
+ gfafb = d_nm->mkNode(kind::APPLY_UF, g, fa, fb);
+ gba = d_nm->mkNode(kind::APPLY_UF, g, b, a);
+ gfbfa = d_nm->mkNode(kind::APPLY_UF, g, fb, fa);
+ gfaa = d_nm->mkNode(kind::APPLY_UF, g, fa, a);
+ gbfb = d_nm->mkNode(kind::APPLY_UF, g, b, fb);
+ h = d_nm->mkVar("h", d_nm->mkFunctionType(args, U));
+ hab = d_nm->mkNode(kind::APPLY_UF, h, a, b);
+ hba = d_nm->mkNode(kind::APPLY_UF, h, b, a);
+ hfaa = d_nm->mkNode(kind::APPLY_UF, h, fa, a);
+
+ a_eq_b = d_nm->mkNode(kind::EQUAL, a, b);
+ fa_eq_b = d_nm->mkNode(kind::EQUAL, fa, b);
+ a_eq_fb = d_nm->mkNode(kind::EQUAL, a, fb);
+ fa_eq_fb = d_nm->mkNode(kind::EQUAL, fa, fb);
+
+ h_eq_g = d_nm->mkNode(kind::EQUAL, h, g);
+ }
+
+ void tearDown() {
+ try {
+ f = a = fa = ffa = fffa = ffffa = Node::null();
+ b = fb = ffb = fffb = ffffb = Node::null();
+ g = gab = gba = gfafb = gfbfa = gfaa = gbfb = Node::null();
+ h = hab = hba = hfaa = Node::null();
+ a_eq_b = fa_eq_b = a_eq_fb = fa_eq_fb = h_eq_g = Node::null();
+ U = TypeNode::null();
+
+ delete d_cc;
+ delete d_out;
+ delete d_scope;
+ delete d_nm;
+ delete d_context;
+
+ } catch(Exception& e) {
+ Warning() << std::endl << e << std::endl;
+ throw;
+ }
+ }
+
+ void testSimple() {
+ //Debug.on("cc");
+ // add terms, then add equalities
+
+ d_cc->addTerm(fa);
+ d_cc->addTerm(fb);
+
+ d_cc->addEquality(a_eq_b);
+
+ TS_ASSERT(d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+ }
+
+ void testSimpleReverse() {
+ // add equalities, then add terms; should get the same as
+ // testSimple()
+
+ d_cc->addEquality(a_eq_b);
+
+ d_cc->addTerm(fa);
+ d_cc->addTerm(fb);
+
+ TS_ASSERT(d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+ }
+
+ void testSimpleContextual() {
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(!d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(!d_cc->areCongruent(a, b));
+
+ {
+ d_context->push();
+
+ d_cc->addTerm(fa);
+ d_cc->addTerm(fb);
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(!d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(!d_cc->areCongruent(a, b));
+
+ {
+ d_context->push();
+
+ d_cc->addEquality(a_eq_b);
+
+ TS_ASSERT(d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(!d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(!d_cc->areCongruent(a, b));
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(!d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(!d_cc->areCongruent(a, b));
+ }
+
+ void testSimpleContextualReverse() {
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(!d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(!d_cc->areCongruent(a, b));
+
+ {
+ d_context->push();
+
+ d_cc->addEquality(a_eq_b);
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+
+ {
+ d_context->push();
+
+ d_cc->addTerm(fa);
+ d_cc->addTerm(fb);
+
+ TS_ASSERT(d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+
+ d_context->pop();
+ }
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(!d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(!d_cc->areCongruent(a, b));
+ }
+
+ void test_f_of_f_of_something() {
+ d_cc->addTerm(ffa);
+ d_cc->addTerm(ffb);
+
+ d_cc->addEquality(a_eq_b);
+
+ TS_ASSERT(d_out->areCongruent(ffa, ffb));
+ TS_ASSERT(d_cc->areCongruent(ffa, ffb));
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+ }
+
+ void test_f4_of_something() {
+ d_cc->addTerm(ffffa);
+ d_cc->addTerm(ffffb);
+
+ d_cc->addEquality(a_eq_b);
+
+ TS_ASSERT(d_out->areCongruent(ffffa, ffffb));
+ TS_ASSERT(d_cc->areCongruent(ffffa, ffffb));
+
+ TS_ASSERT(!d_out->areCongruent(fffa, fffb));
+ TS_ASSERT(d_cc->areCongruent(fffa, fffb));
+
+ TS_ASSERT(!d_out->areCongruent(ffa, ffb));
+ TS_ASSERT(d_cc->areCongruent(ffa, ffb));
+
+ TS_ASSERT(!d_out->areCongruent(fa, fb));
+ TS_ASSERT(d_cc->areCongruent(fa, fb));
+
+ TS_ASSERT(!d_out->areCongruent(a, b));
+ TS_ASSERT(d_cc->areCongruent(a, b));
+ }
+
+ void testSimpleBinaryFunction() {
+ d_cc->addTerm(gab);
+ d_cc->addTerm(gba);
+
+ d_cc->addEquality(a_eq_b);
+
+ TS_ASSERT(d_out->areCongruent(gab, gba));
+ TS_ASSERT(d_cc->areCongruent(gab, gba));
+ }
+
+ void testSimpleBinaryFunction2() {
+
+ //Debug.on("cc");
+ try {
+
+ d_cc->addTerm(gfafb);
+ d_cc->addTerm(gba);
+ d_cc->addTerm(hfaa);
+
+ d_cc->addEquality(a_eq_fb);
+ d_cc->addEquality(fa_eq_b);
+ d_cc->addEquality(h_eq_g);
+
+ TS_ASSERT(d_cc->areCongruent(a, fb));
+ TS_ASSERT(d_cc->areCongruent(b, fa));
+ TS_ASSERT(d_cc->areCongruent(fb, ffa));
+
+ Debug("cc") << "\n\n\n"
+ << "a norm: " << d_cc->normalize(a) << std::endl
+ << "fb norm: " << d_cc->normalize(fb) << std::endl
+ << "b norm: " << d_cc->normalize(b) << std::endl
+ << "fa norm: " << d_cc->normalize(fa) << std::endl
+ << "ffa norm: " << d_cc->normalize(ffa) << std::endl
+ << "ffffa norm " << d_cc->normalize(ffffa) << std::endl
+ << "ffffb norm " << d_cc->normalize(ffffb) << std::endl
+ << "gba norm: " << d_cc->normalize(gba) << std::endl
+ << "gfaa norm: " << d_cc->normalize(gfaa) << std::endl
+ << "gbfb norm: " << d_cc->normalize(gbfb) << std::endl
+ << "gfafb norm: " << d_cc->normalize(gfafb) << std::endl
+ << "hab norm: " << d_cc->normalize(hab) << std::endl
+ << "hba norm: " << d_cc->normalize(hba) << std::endl
+ << "hfaa norm: " << d_cc->normalize(hfaa) << std::endl;
+
+ TS_ASSERT(d_out->areCongruent(gfafb, gba));
+ TS_ASSERT(d_cc->areCongruent(b, fa));
+ TS_ASSERT(d_cc->areCongruent(gfafb, hba));
+ TS_ASSERT(d_cc->areCongruent(gfafb, gba));
+ TS_ASSERT(d_cc->areCongruent(hba, gba));
+ TS_ASSERT(d_cc->areCongruent(hfaa, hba));
+ TS_ASSERT(d_out->areCongruent(hfaa, gba));// fails due to problem with care lists
+ TS_ASSERT(d_cc->areCongruent(hfaa, gba));
+
+ } catch(Exception e) {
+ cout << "\n\n" << e << "\n\n";
+ throw;
+ }
+ }
+
+ void testUF() {
+ //Debug.on("cc");
+ try{
+ Node c_0 = d_nm->mkVar("c_0", U);
+ Node c_1 = d_nm->mkVar("c_1", U);
+ Node c_2 = d_nm->mkVar("c_2", U);
+ Node c2 = d_nm->mkVar("c2", U);
+ Node c3 = d_nm->mkVar("c3", U);
+ Node c4 = d_nm->mkVar("c4", U);
+ Node c5 = d_nm->mkVar("c5", U);
+ Node c6 = d_nm->mkVar("c6", U);
+ Node c7 = d_nm->mkVar("c7", U);
+ Node c8 = d_nm->mkVar("c8", U);
+ Node c9 = d_nm->mkVar("c9", U);
+ vector<TypeNode> args2U(2, U);
+ Node f1 = d_nm->mkVar("f1", d_nm->mkFunctionType(args2U, U));
+
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_2),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_1),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0)))),d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,d_nm->mkNode(kind::APPLY_UF, f1,c_2,d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_2))))));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c2,c8),d_nm->mkNode(kind::APPLY_UF, f1,c4,c9)));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c9,c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c8,c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c4,c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c2,c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c5,c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c7,c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c3,c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, c6,c_1));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_2),c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_1),c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_2,c_0),c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_2),c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_1),c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_1,c_0),c_1));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_1),c_0));
+ d_cc->addEquality(d_nm->mkNode(kind::EQUAL, d_nm->mkNode(kind::APPLY_UF, f1,c_0,c_0),c_0));
+ }catch(Exception &e) { cout << e << "\n"; throw e; }
+ }
+
+ void testUF2() {
+ Node f = d_nm->mkVar("f", d_nm->mkFunctionType(U, U));
+ Node x = d_nm->mkVar("x", U);
+ Node y = d_nm->mkVar("y", U);
+ Node z = d_nm->mkVar("z", U);
+ Node ffx = d_nm->mkNode(kind::APPLY_UF, f, d_nm->mkNode(kind::APPLY_UF, f, x));
+ Node fffx = d_nm->mkNode(kind::APPLY_UF, f, ffx);
+ Node ffffx = d_nm->mkNode(kind::APPLY_UF, f, fffx);
+ Node ffx_eq_fffx = ffx.eqNode(fffx);
+ Node ffx_eq_y = ffx.eqNode(y);
+ Node ffffx_eq_z = ffffx.eqNode(z);
+
+ d_cc->addEquality(ffx_eq_fffx);
+ d_cc->addEquality(ffx_eq_y);
+ d_cc->addEquality(ffffx_eq_z);
+ }
+
+};/* class CongruenceClosureWhite */
projects / cvc5.git / commitdiff