diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-08-17 22:24:26 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-08-17 22:24:26 +0000 |
| commit | 08a57829cdd0ef4c02fee349b4b721d3e4a3f6d1 (patch) | |
| tree | 9ea214ffb5a5a03e3c71c09814f17787be6d022b /src | |
| parent | daf715e2ccb53bd88c6f374840b5d41e72c61c90 (diff) | |
Merge from "cc" branch:
CongruenceClosure implementation; CongruenceClosure white-box test.
New UF theory implementation based on new CC module. This one
supports predicates. The two UF implementations exist in parallel
(they can be selected at runtime via the new command line option
"--uf").
Added type infrastructure for TUPLE.
Fixes to unit tests that failed in 16-August-2010 regressions.
Needed to instantiate TheoryEngine with an Options structure, and
explicitly call ->shutdown() on it before destruction (like the
SMTEngine does).
Fixed test makefiles to (1) perform all tests even in the presence of
failures, (2) give proper summaries of subdirectory tests
(e.g. regress0/uf and regress0/precedence)
Other minor changes.
Diffstat (limited to 'src')
29 files changed, 1904 insertions, 282 deletions
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 */ |