diff options
44 files changed, 2391 insertions, 304 deletions
diff --git a/configure.ac b/configure.ac index 21f2a9a8b..c65dea9dc 100644 --- a/configure.ac +++ b/configure.ac @@ -76,9 +76,6 @@ AC_CANONICAL_TARGET 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]) diff --git a/contrib/addsourcedir b/contrib/addsourcedir index 190864469..ef6aedd15 100644 --- a/contrib/addsourcedir +++ b/contrib/addsourcedir @@ -68,14 +68,14 @@ EOF 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" diff --git a/src/context/cdmap.h b/src/context/cdmap.h index c218d05f3..d9cc5b1a3 100644 --- a/src/context/cdmap.h +++ b/src/context/cdmap.h @@ -247,9 +247,9 @@ public: return get(); } - CDOmap& operator=(const Data& data) { + const Data& operator=(const Data& data) { set(data); - return *this; + return data; } CDOmap* next() const { diff --git a/src/expr/expr_manager_template.cpp b/src/expr/expr_manager_template.cpp index 343f060e9..1eabc9f8a 100644 --- a/src/expr/expr_manager_template.cpp +++ b/src/expr/expr_manager_template.cpp @@ -253,6 +253,16 @@ FunctionType ExprManager::mkPredicateType(const std::vector<Type>& sorts) { 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))); diff --git a/src/expr/expr_manager_template.h b/src/expr/expr_manager_template.h index 3b5b0e0f4..ab7aeace1 100644 --- a/src/expr/expr_manager_template.h +++ b/src/expr/expr_manager_template.h @@ -211,6 +211,13 @@ public: */ 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; diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h index 402116842..4e4d69789 100644 --- a/src/expr/node_builder.h +++ b/src/expr/node_builder.h @@ -874,7 +874,7 @@ expr::NodeValue* NodeBuilder<nchild_thresh>::constructNV() { nv->d_rc = 0; setUsed(); Debug("gc") << "creating node value " << nv - << " [" << nv->d_id << "]: " << nv->toString() << "\n"; + << " [" << nv->d_id << "]: " << *nv << "\n"; return nv; } diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp index fbfffe87d..d017ad799 100644 --- a/src/expr/node_manager.cpp +++ b/src/expr/node_manager.cpp @@ -205,6 +205,9 @@ TypeNode NodeManager::getType(TNode n, bool check) 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; diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h index dcfb14b7a..baa8de5aa 100644 --- a/src/expr/node_manager.h +++ b/src/expr/node_manager.h @@ -523,6 +523,16 @@ public: */ 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); @@ -714,6 +724,15 @@ NodeManager::mkPredicateType(const std::vector<TypeNode>& sorts) { 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))); } diff --git a/src/expr/type.cpp b/src/expr/type.cpp index 225e5f9e0..b111e5604 100644 --- a/src/expr/type.cpp +++ b/src/expr/type.cpp @@ -166,6 +166,19 @@ Type::operator FunctionType() const throw (AssertionException) { 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); @@ -222,6 +235,18 @@ Type FunctionType::getRangeType() const { 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()); @@ -257,6 +282,12 @@ FunctionType::FunctionType(const Type& t) throw (AssertionException) Assert(isFunction()); } +TupleType::TupleType(const Type& t) throw (AssertionException) +: Type(t) +{ + Assert(isTuple()); +} + ArrayType::ArrayType(const Type& t) throw (AssertionException) : Type(t) { diff --git a/src/expr/type.h b/src/expr/type.h index be8a57be3..9ade5e6f5 100644 --- a/src/expr/type.h +++ b/src/expr/type.h @@ -43,6 +43,7 @@ class RealType; class BitVectorType; class ArrayType; class FunctionType; +class TupleType; class KindType; class SortType; class Type; @@ -183,7 +184,7 @@ public: /** * 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; @@ -201,8 +202,20 @@ public: 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; @@ -295,7 +308,21 @@ public: }; /** - * 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 { diff --git a/src/expr/type_node.cpp b/src/expr/type_node.cpp index b32555b9d..491734b35 100644 --- a/src/expr/type_node.cpp +++ b/src/expr/type_node.cpp @@ -63,7 +63,7 @@ bool TypeNode::isPredicate() const { 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; @@ -74,6 +74,20 @@ TypeNode TypeNode::getRangeType() const { 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 { diff --git a/src/expr/type_node.h b/src/expr/type_node.h index 1d5f89c60..811eab54f 100644 --- a/src/expr/type_node.h +++ b/src/expr/type_node.h @@ -333,6 +333,12 @@ public: */ 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; diff --git a/src/main/getopt.cpp b/src/main/getopt.cpp index ed196ac45..b15f4ae66 100644 --- a/src/main/getopt.cpp +++ b/src/main/getopt.cpp @@ -69,7 +69,8 @@ enum OptionValue { SHOW_CONFIG, STRICT_PARSING, DEFAULT_EXPR_DEPTH, - PRINT_EXPR_TYPES + PRINT_EXPR_TYPES, + UF_THEORY };/* enum OptionValue */ /** @@ -115,6 +116,7 @@ static struct option cmdlineOptions[] = { { "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! */ @@ -248,6 +250,24 @@ throw(OptionException) { } 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"); diff --git a/src/main/usage.h b/src/main/usage.h index 9fdc6a67b..2be5f092e 100644 --- a/src/main/usage.h +++ b/src/main/usage.h @@ -45,7 +45,8 @@ CVC4 options:\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 */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 37f6f0657..cdb659760 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -79,7 +79,7 @@ SmtEngine::SmtEngine(ExprManager* em, const Options* opts) throw () : 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); } diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds index dfa94a66d..d3b9d12fb 100644 --- a/src/theory/builtin/kinds +++ b/src/theory/builtin/kinds @@ -127,3 +127,4 @@ constant TYPE_CONSTANT \ "expr/type_constant.h" \ "basic types" operator FUNCTION_TYPE 2: "function type" +operator TUPLE_TYPE 2: "tuple type" diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h index 354bf02bd..42c9902e5 100644 --- a/src/theory/builtin/theory_builtin_type_rules.h +++ b/src/theory/builtin/theory_builtin_type_rules.h @@ -44,7 +44,7 @@ class EqualityTypeRule { std::stringstream ss; ss << "Types do not match in equation "; ss << "[" << lhsType << "<>" << rhsType << "]"; - + throw TypeCheckingExceptionPrivate(n, ss.str()); } @@ -54,7 +54,8 @@ class EqualityTypeRule { } return booleanType; } -}; +};/* class EqualityTypeRule */ + class DistinctTypeRule { public: @@ -71,7 +72,22 @@ 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 */ diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index 54204ae3f..cc0e663fa 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -30,10 +30,13 @@ #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 { @@ -134,6 +137,12 @@ class TheoryEngine { 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. */ static bool inPreRewriteCache(TNode n, bool topLevel) throw() { @@ -193,16 +202,26 @@ public: /** * 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); @@ -222,12 +241,24 @@ public: 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; } @@ -238,21 +269,17 @@ public: * 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; } /** diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index 4e399aeb7..85b41bdbe 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -6,10 +6,13 @@ AM_CXXFLAGS = -Wall -Wno-unknown-pragmas $(FLAG_VISIBILITY_HIDDEN) 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 diff --git a/src/theory/uf/morgan/Makefile.am b/src/theory/uf/morgan/Makefile.am new file mode 100644 index 000000000..e9faa88df --- /dev/null +++ b/src/theory/uf/morgan/Makefile.am @@ -0,0 +1,12 @@ +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 = diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp new file mode 100644 index 000000000..a480a4d21 --- /dev/null +++ b/src/theory/uf/morgan/theory_uf_morgan.cpp @@ -0,0 +1,348 @@ +/********************* */ +/*! \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; +} diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h new file mode 100644 index 000000000..1a1ade250 --- /dev/null +++ b/src/theory/uf/morgan/theory_uf_morgan.h @@ -0,0 +1,186 @@ +/********************* */ +/*! \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 */ diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index f0be0668a..f745cf402 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,8 +1,8 @@ /********************* */ /*! \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) @@ -11,16 +11,10 @@ ** 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" @@ -34,191 +28,20 @@ #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 */ diff --git a/src/theory/uf/tim/Makefile.am b/src/theory/uf/tim/Makefile.am new file mode 100644 index 000000000..647783885 --- /dev/null +++ b/src/theory/uf/tim/Makefile.am @@ -0,0 +1,14 @@ +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 = diff --git a/src/theory/uf/ecdata.cpp b/src/theory/uf/tim/ecdata.cpp index 822f3a95b..52a110ff2 100644 --- a/src/theory/uf/ecdata.cpp +++ b/src/theory/uf/tim/ecdata.cpp @@ -17,12 +17,13 @@ ** context-dependent object. **/ -#include "theory/uf/ecdata.h" +#include "theory/uf/tim/ecdata.h" using namespace CVC4; -using namespace context; -using namespace theory; -using namespace uf; +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), diff --git a/src/theory/uf/ecdata.h b/src/theory/uf/tim/ecdata.h index bff0a67a2..5e72f0042 100644 --- a/src/theory/uf/ecdata.h +++ b/src/theory/uf/tim/ecdata.h @@ -19,8 +19,8 @@ #include "cvc4_private.h" -#ifndef __CVC4__THEORY__UF__ECDATA_H -#define __CVC4__THEORY__UF__ECDATA_H +#ifndef __CVC4__THEORY__UF__TIM__ECDATA_H +#define __CVC4__THEORY__UF__TIM__ECDATA_H #include "expr/node.h" #include "context/context.h" @@ -30,6 +30,7 @@ namespace CVC4 { namespace theory { namespace uf { +namespace tim { /** * Link is a context dependent linked list of nodes. @@ -252,8 +253,9 @@ public: };/* class ECData */ +}/* CVC4::theory::uf::tim namespace */ }/* CVC4::theory::uf namespace */ }/* CVC4::theory namespace */ }/* CVC4 namespace */ -#endif /* __CVC4__THEORY__UF__ECDATA_H */ +#endif /* __CVC4__THEORY__UF__TIM__ECDATA_H */ diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/tim/theory_uf_tim.cpp index 9060568b2..ccc37a24b 100644 --- a/src/theory/uf/theory_uf.cpp +++ b/src/theory/uf/tim/theory_uf_tim.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file theory_uf.cpp +/*! \file theory_uf_tim.cpp ** \verbatim ** Original author: taking ** Major contributors: mdeters @@ -16,8 +16,8 @@ ** Implementation of the theory of uninterpreted functions. **/ -#include "theory/uf/theory_uf.h" -#include "theory/uf/ecdata.h" +#include "theory/uf/tim/theory_uf_tim.h" +#include "theory/uf/tim/ecdata.h" #include "expr/kind.h" using namespace CVC4; @@ -25,9 +25,10 @@ using namespace CVC4::kind; using namespace CVC4::context; using namespace CVC4::theory; using namespace CVC4::theory::uf; +using namespace CVC4::theory::uf::tim; -TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) : - Theory(id, c, out), +TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) : + TheoryUF(id, c, out), d_assertions(c), d_pending(c), d_currentPendingIdx(c,0), @@ -35,10 +36,10 @@ TheoryUF::TheoryUF(int id, Context* c, OutputChannel& out) : d_registered(c) { } -TheoryUF::~TheoryUF() { +TheoryUFTim::~TheoryUFTim() { } -Node TheoryUF::rewrite(TNode n){ +Node TheoryUFTim::rewrite(TNode n){ Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl; Node ret(n); if(n.getKind() == EQUAL){ @@ -50,12 +51,12 @@ Node TheoryUF::rewrite(TNode n){ Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl; return ret; } -void TheoryUF::preRegisterTerm(TNode n) { +void TheoryUFTim::preRegisterTerm(TNode n) { Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl; Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl; } -void TheoryUF::registerTerm(TNode n) { +void TheoryUFTim::registerTerm(TNode n) { Debug("uf") << "uf: begin registerTerm(" << n << ")" << std::endl; @@ -147,13 +148,13 @@ void TheoryUF::registerTerm(TNode n) { } -bool TheoryUF::sameCongruenceClass(TNode x, TNode y) { +bool TheoryUFTim::sameCongruenceClass(TNode x, TNode y) { return ccFind(x.getAttribute(ECAttr())) == ccFind(y.getAttribute(ECAttr())); } -bool TheoryUF::equiv(TNode x, TNode y) { +bool TheoryUFTim::equiv(TNode x, TNode y) { Assert(x.getKind() == kind::APPLY_UF); Assert(y.getKind() == kind::APPLY_UF); @@ -189,7 +190,7 @@ bool TheoryUF::equiv(TNode x, TNode y) { * many better algorithms use eager path compression. * 2) Elminate recursion. */ -ECData* TheoryUF::ccFind(ECData * x) { +ECData* TheoryUFTim::ccFind(ECData * x) { if(x->getFind() == x) { return x; } else { @@ -208,7 +209,7 @@ ECData* TheoryUF::ccFind(ECData * x) { */ } -void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) { +void TheoryUFTim::ccUnion(ECData* ecX, ECData* ecY) { ECData* nslave; ECData* nmaster; @@ -234,7 +235,7 @@ void TheoryUF::ccUnion(ECData* ecX, ECData* ecY) { ECData::takeOverDescendantWatchList(nslave, nmaster); } -void TheoryUF::merge() { +void TheoryUFTim::merge() { while(d_currentPendingIdx < d_pending.size() ) { Node assertion = d_pending[d_currentPendingIdx]; d_currentPendingIdx = d_currentPendingIdx + 1; @@ -259,7 +260,7 @@ void TheoryUF::merge() { } } -Node TheoryUF::constructConflict(TNode diseq) { +Node TheoryUFTim::constructConflict(TNode diseq) { Debug("uf") << "uf: begin constructConflict()" << std::endl; NodeBuilder<> nb(kind::AND); @@ -278,13 +279,13 @@ Node TheoryUF::constructConflict(TNode diseq) { return conflict; } -void TheoryUF::check(Effort level) { +void TheoryUFTim::check(Effort level) { Debug("uf") << "uf: begin check(" << level << ")" << std::endl; while(!done()) { Node assertion = get(); - Debug("uf") << "TheoryUF::check(): " << assertion << std::endl; + Debug("uf") << "TheoryUFTim::check(): " << assertion << std::endl; switch(assertion.getKind()) { case EQUAL: @@ -293,13 +294,17 @@ void TheoryUF::check(Effort level) { 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") << "TheoryUF::check(): done = " << (done() ? "true" : "false") << std::endl; + Debug("uf") << "TheoryUFTim::check(): done = " << (done() ? "true" : "false") << std::endl; } //Make sure all outstanding merges are completed. diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h new file mode 100644 index 000000000..1591cc05c --- /dev/null +++ b/src/theory/uf/tim/theory_uf_tim.h @@ -0,0 +1,229 @@ +/********************* */ +/*! \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 */ diff --git a/src/util/congruence_closure.cpp b/src/util/congruence_closure.cpp new file mode 100644 index 000000000..82e658498 --- /dev/null +++ b/src/util/congruence_closure.cpp @@ -0,0 +1,33 @@ +/********************* */ +/*! \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 */ diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 1727b3b30..058f9c193 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -22,16 +22,36 @@ #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. * @@ -43,67 +63,206 @@ namespace 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); /** @@ -111,38 +270,641 @@ public: * 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 */ diff --git a/src/util/options.h b/src/util/options.h index 7fcf35f00..c79bc93b1 100644 --- a/src/util/options.h +++ b/src/util/options.h @@ -47,6 +47,12 @@ struct CVC4_PUBLIC Options { /** 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; @@ -65,6 +71,7 @@ struct CVC4_PUBLIC Options { err(0), verbosity(0), lang(parser::LANG_AUTO), + uf_implementation(MORGAN), parseOnly(false), semanticChecks(true), memoryMap(false), @@ -72,6 +79,21 @@ struct CVC4_PUBLIC Options { {} };/* 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 */ diff --git a/test/Makefile.am b/test/Makefile.am index 2b79c5045..501f85090 100644 --- a/test/Makefile.am +++ b/test/Makefile.am @@ -26,7 +26,7 @@ test "X$(AM_COLOR_TESTS)" != Xno \ blu='[1;34m'; \ std='[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: diff --git a/test/regress/Makefile.am b/test/regress/Makefile.am index a3808b751..80e8da387 100644 --- a/test/regress/Makefile.am +++ b/test/regress/Makefile.am @@ -1,6 +1,8 @@ SUBDIRS = regress0 DIST_SUBDIRS = regress0 regress1 regress2 regress3 +MAKEFLAGS = -k + export VERBOSE = 1 .PHONY: regress0 regress1 regress2 regress3 diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 09dc52ce4..7f732b17f 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -1,6 +1,7 @@ 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, diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index bf516107e..452024309 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -16,9 +16,9 @@ TESTS = \ 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 \ diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index abc4efcc7..4e4a42a31 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -1,6 +1,7 @@ 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, diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index 51d145859..1651865fd 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -1,6 +1,7 @@ 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, diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 81fb8616e..744ec5775 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -1,6 +1,7 @@ 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, diff --git a/test/unit/Makefile.am b/test/unit/Makefile.am index f25862b54..eb920e6c5 100644 --- a/test/unit/Makefile.am +++ b/test/unit/Makefile.am @@ -3,7 +3,7 @@ UNIT_TESTS = \ 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 \ @@ -29,6 +29,7 @@ UNIT_TESTS = \ util/assert_white \ util/bitvector_black \ util/configuration_black \ + util/congruence_closure_white \ util/output_black \ util/exception_black \ util/integer_black \ @@ -182,13 +183,13 @@ no-cxxtest-available: 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; \ diff --git a/test/unit/expr/attribute_white.h b/test/unit/expr/attribute_white.h index e18aeb975..ea1f40eac 100644 --- a/test/unit/expr/attribute_white.h +++ b/test/unit/expr/attribute_white.h @@ -104,8 +104,8 @@ public: 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); diff --git a/test/unit/theory/shared_term_manager_black.h b/test/unit/theory/shared_term_manager_black.h index 4393d99cd..def2f7049 100644 --- a/test/unit/theory/shared_term_manager_black.h +++ b/test/unit/theory/shared_term_manager_black.h @@ -31,6 +31,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -50,6 +51,7 @@ class SharedTermManagerBlack : public CxxTest::TestSuite { NodeManager* d_nm; NodeManagerScope* d_scope; TheoryEngine* d_theoryEngine; + Options d_options; public: @@ -59,11 +61,11 @@ 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; diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h index ead879336..1ec523148 100644 --- a/test/unit/theory/theory_engine_white.h +++ b/test/unit/theory/theory_engine_white.h @@ -35,6 +35,7 @@ #include "context/context.h" #include "util/rational.h" #include "util/integer.h" +#include "util/options.h" #include "util/Assert.h" using namespace CVC4; @@ -214,6 +215,7 @@ class TheoryEngineWhite : public CxxTest::TestSuite { FakeOutputChannel *d_nullChannel; FakeTheory *d_builtin, *d_bool, *d_uf, *d_arith, *d_arrays, *d_bv; TheoryEngine* d_theoryEngine; + Options d_options; public: @@ -234,7 +236,7 @@ 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. @@ -254,6 +256,7 @@ public: } void tearDown() { + d_theoryEngine->shutdown(); delete d_theoryEngine; delete d_bv; diff --git a/test/unit/theory/theory_uf_white.h b/test/unit/theory/theory_uf_tim_white.h index f273de30f..aec999293 100644 --- a/test/unit/theory/theory_uf_white.h +++ b/test/unit/theory/theory_uf_tim_white.h @@ -11,15 +11,16 @@ ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** - ** \brief White box testing of CVC4::theory::uf::TheoryUF. + ** \brief White box testing of CVC4::theory::uf::tim::TheoryUFTim. ** - ** White box testing of CVC4::theory::uf::TheoryUF. + ** 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" @@ -31,13 +32,14 @@ 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 TheoryUFWhite : public CxxTest::TestSuite { +class TheoryUFTimWhite : public CxxTest::TestSuite { Context* d_ctxt; NodeManager* d_nm; @@ -46,20 +48,20 @@ class TheoryUFWhite : public CxxTest::TestSuite { TestOutputChannel d_outputChannel; Theory::Effort d_level; - TheoryUF* d_euf; + TheoryUFTim* d_euf; TypeNode* d_booleanType; public: - TheoryUFWhite() : d_level(Theory::FULL_EFFORT) {} + 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 TheoryUF(0, d_ctxt, d_outputChannel); + d_euf = new TheoryUFTim(0, d_ctxt, d_outputChannel); d_booleanType = new TypeNode(d_nm->booleanType()); } diff --git a/test/unit/util/congruence_closure_white.h b/test/unit/util/congruence_closure_white.h new file mode 100644 index 000000000..273f9cfa5 --- /dev/null +++ b/test/unit/util/congruence_closure_white.h @@ -0,0 +1,454 @@ +/********************* */ +/*! \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 */ |