From: Dejan Jovanović Date: Sat, 9 Jul 2011 01:38:48 +0000 (+0000) Subject: surprize surprize X-Git-Tag: cvc5-1.0.0~8519 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=878f71272c06cf605fb3d2f4e66eaea55aa32127;p=cvc5.git surprize surprize --- diff --git a/.cproject b/.cproject index df8183d4e..ac930d8b9 100644 --- a/.cproject +++ b/.cproject @@ -2,319 +2,327 @@ - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - -make - -check -true -true -true - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - - + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + + make + check + true + true + true + + + make + -j2 + + true + true + true + + + + + + + + diff --git a/src/expr/Makefile.am b/src/expr/Makefile.am index 4ed5a3ac7..ced34b8be 100644 --- a/src/expr/Makefile.am +++ b/src/expr/Makefile.am @@ -11,7 +11,7 @@ libexpr_la_SOURCES = \ type_node.h \ type_node.cpp \ node_builder.h \ - convenience_node_builders.h \ + convenience_node_builders.h \ type.h \ type.cpp \ node_value.h \ @@ -27,7 +27,9 @@ libexpr_la_SOURCES = \ declaration_scope.cpp \ expr_manager_scope.h \ node_self_iterator.h \ - expr_stream.h + expr_stream.h \ + kind_map.h + nodist_libexpr_la_SOURCES = \ kind.h \ metakind.h \ diff --git a/src/expr/kind_map.h b/src/expr/kind_map.h new file mode 100644 index 000000000..a02339e5e --- /dev/null +++ b/src/expr/kind_map.h @@ -0,0 +1,275 @@ +/********************* */ +/*! \file kind_map.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, 2011 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 A bitmap of Kinds + ** + ** This is a class representation for a bitmap of Kinds that is + ** iterable, manipulable, and packed. + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__KIND_MAP_H +#define __CVC4__KIND_MAP_H + +#include +#include + +#include "expr/kind.h" + +namespace CVC4 { + +/** A bitmap of Kinds. */ +class KindMap { + static const size_t SIZE = (kind::LAST_KIND + 63) / 64; + + uint64_t d_bitmap[SIZE]; + + /** + * Accessor proxy class used so that things like "map[k] = true" + * will work as expected (we have to return a proxy from + * KindMap::operator[]() in that case, since we can't construct an + * address to the individual *bit* in the packed representation). + */ + class Accessor { + KindMap& d_map; + Kind d_kind; + + Accessor(KindMap& m, Kind k) : + d_map(m), + d_kind(k) { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + } + + friend class KindMap; + + public: + + operator bool() const { + return d_map.tst(d_kind); + } + + Accessor operator=(bool b) const { + if(b) { + d_map.set(d_kind); + } else { + d_map.clr(d_kind); + } + return *this; + } + + };/* class KindMap::Accessor */ + +public: + + /** An iterator over a KindMap. */ + class iterator { + const KindMap* d_map; + Kind d_kind; + + public: + typedef std::input_iterator_tag iterator_category; + typedef Kind value_type; + + iterator() : + d_map(NULL), + d_kind(Kind(0)) { + } + iterator(const KindMap& m, Kind k) : + d_map(&m), + d_kind(k) { + AssertArgument(k >= Kind(0) && k <= kind::LAST_KIND, k, "invalid kind"); + while(d_kind < kind::LAST_KIND && + ! d_map->tst(d_kind)) { + d_kind = Kind(uint64_t(d_kind) + 1); + } + } + iterator& operator++() { + if(d_kind < kind::LAST_KIND) { + d_kind = Kind(uint64_t(d_kind) + 1); + while(d_kind < kind::LAST_KIND && + ! d_map->tst(d_kind)) { + d_kind = Kind(uint64_t(d_kind) + 1); + } + } + return *this; + } + iterator operator++(int) const { + const_iterator i = *this; + ++i; + return i; + } + Kind operator*() const { + return d_kind; + } + bool operator==(iterator i) const { + return d_map == i.d_map && d_kind == i.d_kind; + } + bool operator!=(iterator i) const { + return !(*this == i); + } + };/* class KindMap::iterator */ + typedef iterator const_iterator; + + KindMap() { + clear(); + } + KindMap(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] = m.d_bitmap[i]; + } + } + KindMap(Kind k) { + clear(); + set(k); + } + + /** Empty the map. */ + void clear() { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] = uint64_t(0); + } + } + /** Tests whether the map is empty. */ + bool isEmpty() const { + for(unsigned i = 0; i < SIZE; ++i) { + if(d_bitmap[i] != uint64_t(0)) { + return false; + } + } + return true; + } + /** Test whether k is in the map. */ + bool tst(Kind k) const { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + return (d_bitmap[k / 64] >> (k % 64)) & uint64_t(1); + } + /** Set k in the map. */ + void set(Kind k) { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + d_bitmap[k / 64] |= (uint64_t(1) << (k % 64)); + } + /** Clear k from the map. */ + void clr(Kind k) { + AssertArgument(k >= Kind(0) && k < kind::LAST_KIND, k, "invalid kind"); + d_bitmap[k / 64] &= ~(uint64_t(1) << (k % 64)); + } + + /** Iterate over the map. */ + const_iterator begin() const { + return const_iterator(*this, Kind(0)); + } + const_iterator end() const { + return const_iterator(*this, kind::LAST_KIND); + } + + /** Invert the map. */ + KindMap operator~() const { + KindMap r; + for(unsigned i = 0; i < SIZE; ++i) { + r.d_bitmap[i] = ~d_bitmap[i]; + } + return r; + } + /** Bitwise-AND the map (with assignment). */ + KindMap& operator&=(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] &= m.d_bitmap[i]; + } + return *this; + } + /** Bitwise-AND the map. */ + KindMap operator&(const KindMap& m) const { + KindMap r(*this); + r &= m; + return r; + } + /** Bitwise-OR the map (with assignment). */ + KindMap& operator|=(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] |= m.d_bitmap[i]; + } + return *this; + } + /** Bitwise-OR the map. */ + KindMap operator|(const KindMap& m) const { + KindMap r(*this); + r |= m; + return r; + } + /** Bitwise-XOR the map (with assignment). */ + KindMap& operator^=(const KindMap& m) { + for(unsigned i = 0; i < SIZE; ++i) { + d_bitmap[i] ^= m.d_bitmap[i]; + } + return *this; + } + /** Bitwise-XOR the map. */ + KindMap operator^(const KindMap& m) const { + KindMap r(*this); + r ^= m; + return r; + } + + /** Test whether k is in the map. */ + bool operator[](Kind k) const { + return tst(k); + } + /** Test whether k is in the map (allowing assignment). */ + Accessor operator[](Kind k) { + return Accessor(*this, k); + } + + /** Test equality between two maps. */ + bool operator==(KindMap m) { + for(unsigned i = 0; i < SIZE; ++i) { + if(d_bitmap[i] != m.d_bitmap[i]) { + return false; + } + } + return true; + } + bool operator!=(KindMap m) { + return !(*this == m); + } +};/* class KindMap */ + +inline KindMap operator~(Kind k) { + KindMap m(k); + return ~m; +} +inline KindMap operator&(Kind k1, Kind k2) { + KindMap m(k1); + return m &= k2; +} +inline KindMap operator&(Kind k1, KindMap m2) { + return m2 & k1; +} +inline KindMap operator|(Kind k1, Kind k2) { + KindMap m(k1); + return m |= k2; +} +inline KindMap operator|(Kind k1, KindMap m2) { + return m2 | k1; +} +inline KindMap operator^(Kind k1, Kind k2) { + KindMap m(k1); + return m ^= k2; +} +inline KindMap operator^(Kind k1, KindMap m2) { + return m2 ^ k1; +} + +}/* CVC4 namespace */ + +#endif /* __CVC4__KIND_MAP_H */ diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 7e335a21b..cbec9faea 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -154,6 +154,24 @@ Node PropEngine::getValue(TNode node) { } } +bool PropEngine::hasValue(TNode node, bool& value) { + Assert(node.getType().isBoolean()); + SatLiteral lit = d_cnfStream->getLiteral(node); + + SatLiteralValue v = d_satSolver->value(lit); + if(v == l_True) { + value = true; + return true; + } else if(v == l_False) { + value = false; + return true; + } else { + Assert(v == l_Undef); + return false; + } +} + + void PropEngine::push() { Assert(!d_inCheckSat, "Sat solver in solve()!"); d_satSolver->push(); diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h index e1a1c08d7..f44ad16f7 100644 --- a/src/prop/prop_engine.h +++ b/src/prop/prop_engine.h @@ -114,6 +114,11 @@ public: */ Node getValue(TNode node); + /** + * Check if the node has a value and return it if yes. + */ + bool hasValue(TNode node, bool& value); + /** * Push the context level. */ diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 4185765a8..d85f28b23 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -45,8 +45,6 @@ #include "theory/booleans/theory_bool.h" #include "theory/booleans/circuit_propagator.h" #include "theory/uf/theory_uf.h" -#include "theory/uf/morgan/theory_uf_morgan.h" -#include "theory/uf/tim/theory_uf_tim.h" #include "theory/arith/theory_arith.h" #include "theory/arrays/theory_arrays.h" #include "theory/bv/theory_bv.h" @@ -199,16 +197,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) : d_theoryEngine->addTheory(); d_theoryEngine->addTheory(); d_theoryEngine->addTheory(); - switch(Options::current()->uf_implementation) { - case Options::TIM: - d_theoryEngine->addTheory(); - break; - case Options::MORGAN: - d_theoryEngine->addTheory(); - break; - default: - Unhandled(Options::current()->uf_implementation); - } + d_theoryEngine->addTheory(); d_propEngine = new PropEngine(d_theoryEngine, d_context); d_theoryEngine->setPropEngine(d_propEngine); diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am index e4647b442..3cf53960a 100644 --- a/src/theory/uf/Makefile.am +++ b/src/theory/uf/Makefile.am @@ -11,6 +11,7 @@ nodist_EXTRA_libuf_la_SOURCES = \ libuf_la_SOURCES = \ theory_uf.h \ + theory_uf.cpp \ theory_uf_type_rules.h \ theory_uf_rewriter.h diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h new file mode 100644 index 000000000..ac02fe4db --- /dev/null +++ b/src/theory/uf/equality_engine.h @@ -0,0 +1,555 @@ +/********************* */ +/*! \file equality_engine.h + ** \verbatim + ** Original author: dejan + ** 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#pragma once + +#include +#include +#include +#include + +#include "expr/node.h" +#include "expr/kind_map.h" +#include "context/cdo.h" +#include "util/output.h" +#include "util/stats.h" +#include "theory/rewriter.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +/** Id of the node */ +typedef size_t EqualityNodeId; + +/** Id of the use list */ +typedef size_t UseListNodeId; + +/** The trigger ids */ +typedef size_t TriggerId; + +/** The equality edge ids */ +typedef size_t EqualityEdgeId; + +/** The null node */ +static const EqualityNodeId null_id = (size_t)(-1); + +/** The null use list node */ +static const EqualityNodeId null_uselist_id = (size_t)(-1); + +/** The null trigger */ +static const TriggerId null_trigger = (size_t)(-1); + +/** The null edge id */ +static const EqualityEdgeId null_edge = (size_t)(-1); + +/** + * A reason for a merge. Either an equality x = y, or a merge of two + * function applications f(x1, x2), f(y1, y2) + */ +enum MergeReasonType { + MERGED_THROUGH_CONGRUENCE, + MERGED_THROUGH_EQUALITY +}; + +inline std::ostream& operator << (std::ostream& out, MergeReasonType reason) { + switch (reason) { + case MERGED_THROUGH_CONGRUENCE: + out << "c"; + break; + case MERGED_THROUGH_EQUALITY: + out << "e"; + break; + default: + Unreachable(); + } + return out; +} + +/** A node in the uselist */ +class UseListNode { + +private: + + /** The id of the application node where this representative is at */ + EqualityNodeId d_applicationId; + + /** The next one in the class */ + UseListNodeId d_nextUseListNodeId; + +public: + + /** + * Creates a new node, which is in a list of it's own. + */ + UseListNode(EqualityNodeId nodeId, UseListNodeId nextId) + : d_applicationId(nodeId), d_nextUseListNodeId(nextId) {} + + /** + * Returns the next node in the circular list. + */ + UseListNodeId getNext() const { + return d_nextUseListNodeId; + } + + /** + * Returns the id of the function application. + */ + EqualityNodeId getApplicationId() const { + return d_applicationId; + } +}; + + +class EqualityNode { + +private: + + /** The size of this equivalence class (if it's a representative) */ + size_t d_size; + + /** The id (in the eq-manager) of the representative equality node */ + EqualityNodeId d_findId; + + /** The next equality node in this class */ + EqualityNodeId d_nextId; + + /** The use list of this node */ + UseListNodeId d_useList; + +public: + + /** + * Creates a new node, which is in a list of it's own. + */ + EqualityNode(EqualityNodeId nodeId = null_id) + : d_size(1), d_findId(nodeId), d_nextId(nodeId), d_useList(null_uselist_id) {} + + /** + * Retuerns the uselist. + */ + UseListNodeId getUseList() const { + return d_useList; + } + + /** + * Returns the next node in the class circular list. + */ + EqualityNodeId getNext() const { + return d_nextId; + } + + /** + * Returns the size of this equivalence class (only valid if this is the representative). + */ + size_t getSize() const { + return d_size; + } + + /** + * Merges the two lists. If add size is true the size of this node is increased by the size of + * the other node, otherwise the size is decreased by the size of the other node. + */ + template + void merge(EqualityNode& other) { + EqualityNodeId tmp = d_nextId; d_nextId = other.d_nextId; other.d_nextId = tmp; + if (addSize) { + d_size += other.d_size; + } else { + d_size -= other.d_size; + } + } + + /** + * Returns the class representative. + */ + EqualityNodeId getFind() const { return d_findId; } + + /** + * Set the class representative. + */ + void setFind(EqualityNodeId findId) { d_findId = findId; } + + /** + * Note that this node is used in a function a application funId. + */ + template + void usedIn(EqualityNodeId funId, memory_class& memory) { + UseListNodeId newUseId = memory.size(); + memory.push_back(UseListNode(funId, d_useList)); + d_useList = newUseId; + } + +}; + +template +class EqualityEngine { + +public: + + /** Statistics about the equality engine instance */ + struct Statistics { + /** Total number of merges */ + IntStat mergesCount; + /** Number of terms managed by the system */ + IntStat termsCount; + /** Number of function terms managed by the system */ + IntStat functionTermsCount; + /** Number of times we performed a backtrack */ + IntStat backtracksCount; + + Statistics(std::string name) + : mergesCount(name + "::mergesCount", 0), + termsCount(name + "::termsCount", 0), + functionTermsCount(name + "::functionTermsCount", 0), + backtracksCount(name + "::backtracksCount", 0) + { + StatisticsRegistry::registerStat(&mergesCount); + StatisticsRegistry::registerStat(&termsCount); + StatisticsRegistry::registerStat(&functionTermsCount); + StatisticsRegistry::registerStat(&backtracksCount); + } + + ~Statistics() { + StatisticsRegistry::unregisterStat(&mergesCount); + StatisticsRegistry::unregisterStat(&termsCount); + StatisticsRegistry::unregisterStat(&functionTermsCount); + StatisticsRegistry::unregisterStat(&backtracksCount); + } + }; + + /** + * f(a,b) + */ + struct FunctionApplication { + EqualityNodeId a, b; + FunctionApplication(EqualityNodeId a = null_id, EqualityNodeId b = null_id): + a(a), b(b) {} + bool operator == (const FunctionApplication& other) const { + return a == other.a && b == other.b; + } + bool isApplication() { + return a != null_id && b != null_id; + } + }; + + struct FunctionApplicationHashFunction { + size_t operator () (const FunctionApplication& app) const { + size_t hash = 0; + hash = 0x9e3779b9 + app.a; + hash ^= 0x9e3779b9 + app.b + (hash << 6) + (hash >> 2); + return hash; + } + }; + +private: + + /** The class to notify when a representative changes for a term */ + NotifyClass d_notify; + + /** The map of kinds to be treated as function applications */ + KindMap d_congruenceKinds; + + /** Map from nodes to their ids */ + __gnu_cxx::hash_map d_nodeIds; + + /** Map from function applications to their ids */ + typedef __gnu_cxx::hash_map ApplicationIdsMap; + + /** + * A map from a pair (a', b') to a function application f(a, b), where a' and b' are the current representatives + * of a and b. + */ + ApplicationIdsMap d_applicationLookup; + + /** Map from ids to the nodes */ + std::vector d_nodes; + + /** Map from ids to the nodes */ + std::vector d_applications; + + /** Map from ids to the equality nodes */ + std::vector d_equalityNodes; + + /** Memory for the use-list nodes */ + std::vector d_useListNodes; + + /** Number of asserted equalities we have so far */ + context::CDO d_assertedEqualitiesCount; + + /** + * We keep a list of asserted equalities. Not among original terms, but + * among the class representatives. + */ + struct Equality { + /** Left hand side of the equality */ + EqualityNodeId lhs; + /** Right hand side of the equality */ + EqualityNodeId rhs; + /** Equality constructor */ + Equality(EqualityNodeId lhs = null_id, EqualityNodeId rhs = null_id) + : lhs(lhs), rhs(rhs) {} + }; + + /** The ids of the classes we have merged */ + std::vector d_assertedEqualities; + + /** The reasons for the equalities */ + + /** + * An edge in the equality graph. This graph is an undirected graph (both edges added) + * containing the actual asserted equalities. + */ + class EqualityEdge { + + // The id of the RHS of this equality + EqualityNodeId d_nodeId; + // The next edge + EqualityEdgeId d_nextId; + // Type of reason for this equality + MergeReasonType d_mergeType; + // Reason of this equality + TNode d_reason; + + public: + + EqualityEdge(): + d_nodeId(null_edge), d_nextId(null_edge), d_mergeType(MERGED_THROUGH_CONGRUENCE) {} + + EqualityEdge(EqualityNodeId nodeId, EqualityNodeId nextId, MergeReasonType type, TNode reason): + d_nodeId(nodeId), d_nextId(nextId), d_mergeType(type), d_reason(reason) {} + + /** Returns the id of the next edge */ + EqualityEdgeId getNext() const { return d_nextId; } + + /** Returns the id of the target edge node */ + EqualityNodeId getNodeId() const { return d_nodeId; } + + /** The reason of this edge */ + MergeReasonType getReasonType() const { return d_mergeType; } + + /** The reason of this edge */ + TNode getReason() const { return d_reason; } +}; + + /** + * All the equality edges (twice as many as the number of asserted equalities. If an equality + * t1 = t2 is asserted, the edges added are -> t2, -> t1 (in this order). Hance, having the index + * of one of the edges you can reconstruct the original equality. + */ + std::vector d_equalityEdges; + + /** + * Returns the string representation of the edges. + */ + std::string edgesToString(EqualityEdgeId edgeId) const; + + /** + * Map from a node to it's first edge in the equality graph. Edges are added to the front of the + * list which makes the insertion/backtracking easy. + */ + std::vector d_equalityGraph; + + /** Add an edge to the equality graph */ + void addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason); + + /** Returns the equality node of the given node */ + EqualityNode& getEqualityNode(TNode node); + + /** Returns the equality node of the given node */ + EqualityNode& getEqualityNode(EqualityNodeId nodeId); + + /** Returns the id of the node */ + EqualityNodeId getNodeId(TNode node) const; + + /** Merge the class2 into class1 */ + void merge(EqualityNode& class1, EqualityNode& class2, std::vector& triggers); + + /** Undo the mereg of class2 into class1 */ + void undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id); + + /** Backtrack the information if necessary */ + void backtrack(); + + /** + * Data used in the BFS search through the equality graph. + */ + struct BfsData { + // The current node + EqualityNodeId nodeId; + // The index of the edge we traversed + EqualityEdgeId edgeId; + // Index in the queue of the previous node. Shouldn't be too much of them, at most the size + // of the biggest equivalence class + size_t previousIndex; + + BfsData(EqualityNodeId nodeId = null_id, EqualityEdgeId edgeId = null_edge, size_t prev = 0) + : nodeId(nodeId), edgeId(edgeId), previousIndex(prev) {} + }; + + /** + * Trigger that will be updated + */ + struct Trigger { + /** The current class id of the LHS of the trigger */ + EqualityNodeId classId; + /** Next trigger for class 1 */ + TriggerId nextTrigger; + + Trigger(EqualityNodeId classId, TriggerId nextTrigger) + : classId(classId), nextTrigger(nextTrigger) {} + }; + + /** + * Vector of triggers (persistent and not-backtrackable). Triggers come in pairs for an + * equality trigger (t1, t2): one at position 2k for t1, and one at position 2k + 1 for t2. When + * updating triggers we always know where the other one is (^1). + */ + std::vector d_equalityTriggers; + + /** + * Vector of original equalities of the triggers. + */ + std::vector d_equalityTriggersOriginal; + + /** + * Trigger lists per node. The begin id changes as we merge, but the end always points to + * the actual end of the triggers for this node. + */ + std::vector d_nodeTriggers; + + /** + * Adds the trigger with triggerId to the beginning of the trigger list of the node with id nodeId. + */ + void addTriggerToList(EqualityNodeId nodeId, TriggerId triggerId); + + /** Statistics */ + Statistics d_stats; + + /** Add a new function application node to the database, i.e APP t1 t2 */ + EqualityNodeId newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2); + + /** Add a new node to the database */ + EqualityNodeId newNode(TNode t, bool isApplication); + + struct MergeCandidate { + EqualityNodeId t1Id, t2Id; + MergeReasonType type; + TNode reason; + MergeCandidate(EqualityNodeId x, EqualityNodeId y, MergeReasonType type, TNode reason): + t1Id(x), t2Id(y), type(type), reason(reason) {} + + std::string toString(EqualityEngine& eqEngine) const { + std::stringstream ss; + ss << eqEngine.d_nodes[t1Id] << " = " << eqEngine.d_nodes[t2Id] << ", " << type; + return ss.str(); + } + }; + + /** Propagation queue */ + std::queue d_propagationQueue; + + /** Enqueue to the propagation queue */ + void enqueue(const MergeCandidate& candidate); + + /** Do the propagation (if check is on, congruences are checked again) */ + void propagate(bool check); + + /** + * Get an explanation of the equality t1 = t2. Returns the asserted equalities that + * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere + * else. TODO: mark the phantom equalities (skolems). + */ + void getExplanation(EqualityEdgeId t1Id, EqualityNodeId t2Id, std::vector& equalities) const; + + /** + * Print the equality graph. + */ + void debugPrintGraph(); + +public: + + /** + * Initialize the equality engine, given the owning class. This will initialize the notifier with + * the owner information. + */ + EqualityEngine(NotifyClass& notify, context::Context* context, std::string name) + : d_notify(notify), d_assertedEqualitiesCount(context, 0), d_stats(name) { + Debug("equality") << "EqualityEdge::EqualityEngine(): id_null = " << +null_id << std::endl; + Debug("equality") << "EqualityEdge::EqualityEngine(): edge_null = " << +null_edge << std::endl; + Debug("equality") << "EqualityEdge::EqualityEngine(): trigger_null = " << +null_trigger << std::endl; + } + + /** + * Adds a term to the term database. + */ + void addTerm(TNode t); + + /** + * Add a kind to treat as function applications. + */ + void addFunctionKind(Kind fun) { + d_congruenceKinds |= fun; + } + + /** + * Adds a function application term to the database. + */ + + /** + * Check whether the node is already in the database. + */ + bool hasTerm(TNode t) const; + + /** + * Adds an equality t1 = t2 to the database. + */ + void addEquality(TNode t1, TNode t2, TNode reason); + + /** + * Returns the representative of the term t. + */ + TNode getRepresentative(TNode t) const; + + /** + * Returns true if the two nodes are in the same class. + */ + bool areEqual(TNode t1, TNode t2) const; + + /** + * Get an explanation of the equality t1 = t2. Returns the asserted equalities that + * imply t1 = t2. Returns TNodes as the assertion equalities should be hashed somewhere + * else. TODO: mark the phantom equalities (skolems). + */ + void getExplanation(TNode t1, TNode t2, std::vector& equalities) const; + + /** + * Adds a notify trigger for equality t1 = t2, i.e. when t1 = t2 the notify will be called with + * (t1 = t2). + */ + void addTriggerEquality(TNode t1, TNode t2, TNode trigger); + +}; + +} // Namespace uf +} // Namespace theory +} // Namespace CVC4 + diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h new file mode 100644 index 000000000..292761c46 --- /dev/null +++ b/src/theory/uf/equality_engine_impl.h @@ -0,0 +1,715 @@ +/********************* */ +/*! \file equality_engine_impl.h + ** \verbatim + ** Original author: dejan + ** 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 [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#pragma once + +#include "theory/uf/equality_engine.h" + +namespace CVC4 { +namespace theory { +namespace uf { + +template +void EqualityEngine::enqueue(const MergeCandidate& candidate) { + Debug("equality") << "EqualityEngine::enqueue(" << candidate.toString(*this) << ")" << std::endl; + d_propagationQueue.push(candidate); +} + +template +EqualityNodeId EqualityEngine::newApplicationNode(TNode original, EqualityNodeId t1, EqualityNodeId t2) { + Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ")" << std::endl; + + ++ d_stats.functionTermsCount; + + // Get another id for this + EqualityNodeId funId = newNode(original, true); + FunctionApplication fun(t1, t2); + d_applications[funId] = fun; + + // The function application we're creating + EqualityNodeId t1ClassId = getEqualityNode(t1).getFind(); + EqualityNodeId t2ClassId = getEqualityNode(t2).getFind(); + FunctionApplication funNormalized(t1ClassId, t2ClassId); + + // Add the lookup data, if it's not already there + typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); + if (find == d_applicationLookup.end()) { + // When we backtrack, if the lookup is not there anymore, we'll add it again + Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): no lookup, setting up" << std::endl; + d_applicationLookup[funNormalized] = funId; + } else { + // If it's there, we need to merge these two + Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << "): lookup exists, adding to queue" << std::endl; + enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); + propagate(false); + } + + // Add to the use lists + d_equalityNodes[t1].usedIn(funId, d_useListNodes); + d_equalityNodes[t2].usedIn(funId, d_useListNodes); + + // Return the new id + Debug("equality") << "EqualityEngine::newApplicationNode(" << original << ", " << t1 << ", " << t2 << ") => " << funId << std::endl; + + return funId; +} + +template +EqualityNodeId EqualityEngine::newNode(TNode node, bool isApplication) { + + Debug("equality") << "EqualityEngine::newNode(" << node << ", " << (isApplication ? "function" : "regular") << ")" << std::endl; + + ++ d_stats.termsCount; + + // Register the new id of the term + EqualityNodeId newId = d_nodes.size(); + d_nodeIds[node] = newId; + // Add the node to it's position + d_nodes.push_back(node); + // Note if this is an application or not + d_applications.push_back(FunctionApplication()); + // Add the trigger list for this node + d_nodeTriggers.push_back(+null_trigger); + // Add it to the equality graph + d_equalityGraph.push_back(+null_edge); + // Add the equality node to the nodes + d_equalityNodes.push_back(EqualityNode(newId)); + + Debug("equality") << "EqualityEngine::newNode(" << node << ", " << (isApplication ? "function" : "regular") << ") => " << newId << std::endl; + + return newId; +} + + +template +void EqualityEngine::addTerm(TNode t) { + + Debug("equality") << "EqualityEngine::addTerm(" << t << ")" << std::endl; + + // If there already, we're done + if (hasTerm(t)) { + return; + } + + EqualityNodeId result; + + // If a function application we go in + if (t.getNumChildren() > 0 && d_congruenceKinds[t.getKind()]) + { + // Add the operator + TNode tOp = t.getOperator(); + addTerm(tOp); + // Add all the children and Curryfy + result = getNodeId(tOp); + for (unsigned i = 0; i < t.getNumChildren(); ++ i) { + // Add the child + addTerm(t[i]); + // Add the application + result = newApplicationNode(t, result, getNodeId(t[i])); + } + } else { + // Otherwise we just create the new id + result = newNode(t, false); + } + + Debug("equality") << "EqualityEngine::addTerm(" << t << ") => " << result << std::endl; +} + +template +bool EqualityEngine::hasTerm(TNode t) const { + return d_nodeIds.find(t) != d_nodeIds.end(); +} + +template +EqualityNodeId EqualityEngine::getNodeId(TNode node) const { + Assert(hasTerm(node), node.toString().c_str()); + return (*d_nodeIds.find(node)).second; +} + +template +EqualityNode& EqualityEngine::getEqualityNode(TNode t) { + return getEqualityNode(getNodeId(t)); +} + +template +EqualityNode& EqualityEngine::getEqualityNode(EqualityNodeId nodeId) { + Assert(nodeId < d_equalityNodes.size()); + return d_equalityNodes[nodeId]; +} + +template +void EqualityEngine::addEquality(TNode t1, TNode t2, TNode reason) { + + Debug("equality") << "EqualityEngine::addEquality(" << t1 << "," << t2 << ")" << std::endl; + + // Backtrack if necessary + backtrack(); + + // Add the terms if they are not already in the database + EqualityNodeId t1Id = getNodeId(t1); + EqualityNodeId t2Id = getNodeId(t2); + + // Add to the queue and propagate + enqueue(MergeCandidate(t1Id, t2Id, MERGED_THROUGH_EQUALITY, reason)); + propagate(false); +} + +template +TNode EqualityEngine::getRepresentative(TNode t) const { + + Debug("equality") << "EqualityEngine::getRepresentative(" << t << ")" << std::endl; + + Assert(hasTerm(t)); + + // Both following commands are semantically const + const_cast(this)->backtrack(); + EqualityNodeId representativeId = const_cast(this)->getEqualityNode(t).getFind(); + + Debug("equality") << "EqualityEngine::getRepresentative(" << t << ") => " << d_nodes[representativeId] << std::endl; + + return d_nodes[representativeId]; +} + +template +bool EqualityEngine::areEqual(TNode t1, TNode t2) const { + Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ")" << std::endl; + + Assert(hasTerm(t1)); + Assert(hasTerm(t2)); + + // Both following commands are semantically const + const_cast(this)->backtrack(); + EqualityNodeId rep1 = const_cast(this)->getEqualityNode(t1).getFind(); + EqualityNodeId rep2 = const_cast(this)->getEqualityNode(t2).getFind(); + + Debug("equality") << "EqualityEngine::areEqual(" << t1 << "," << t2 << ") => " << (rep1 == rep2 ? "true" : "false") << std::endl; + + return rep1 == rep2; +} + +template +void EqualityEngine::merge(EqualityNode& class1, EqualityNode& class2, std::vector& triggers) { + + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << ")" << std::endl; + + Assert(triggers.empty()); + + ++ d_stats.mergesCount; + + EqualityNodeId class1Id = class1.getFind(); + EqualityNodeId class2Id = class2.getFind(); + + // Update class2 representative information + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating class " << class2Id << std::endl; + EqualityNodeId currentId = class2Id; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + + // Update it's find to class1 id + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << "->" << class1Id << std::endl; + currentNode.setFind(class1Id); + + // Go through the triggers and inform if necessary + TriggerId currentTrigger = d_nodeTriggers[currentId]; + while (currentTrigger != null_trigger) { + Trigger& trigger = d_equalityTriggers[currentTrigger]; + Trigger& otherTrigger = d_equalityTriggers[currentTrigger ^ 1]; + + // If the two are not already in the same class + if (otherTrigger.classId != trigger.classId) { + trigger.classId = class1Id; + // If they became the same, call the trigger + if (otherTrigger.classId == class1Id) { + // Id of the real trigger is half the internal one + triggers.push_back(currentTrigger); + } + } + + // Go to the next trigger + currentTrigger = trigger.nextTrigger; + } + + // Move to the next node + currentId = currentNode.getNext(); + + } while (currentId != class2Id); + + + // Update class2 table lookup and information + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of " << class2Id << std::endl; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): updating lookups of node " << currentId << std::endl; + + // Go through the uselist and check for congruences + UseListNodeId currentUseId = currentNode.getUseList(); + while (currentUseId != null_uselist_id) { + // Get the node of the use list + UseListNode& useNode = d_useListNodes[currentUseId]; + // Get the function application + EqualityNodeId funId = useNode.getApplicationId(); + Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl; + const FunctionApplication& fun = d_applications[useNode.getApplicationId()]; + // Check if there is an application with find arguments + EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); + EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); + FunctionApplication funNormalized(aNormalized, bNormalized); + typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); + if (find != d_applicationLookup.end()) { + // Applications fun and the funNormalized can be merged due to congruence + if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) { + enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); + } + } else { + // There is no representative, so we can add one, we remove this when backtracking + d_applicationLookup[funNormalized] = funId; + } + // Go to the next one in the use list + currentUseId = useNode.getNext(); + } + + // Move to the next node + currentId = currentNode.getNext(); + } while (currentId != class2Id); + + // Now merge the lists + class1.merge(class2); +} + +template +void EqualityEngine::undoMerge(EqualityNode& class1, EqualityNode& class2, EqualityNodeId class2Id) { + + Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << ")" << std::endl; + + // Now unmerge the lists (same as merge) + class1.merge(class2); + + // First undo the table lookup changes + Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing lookup changes" << std::endl; + EqualityNodeId currentId = class2Id; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + + // Go through the uselist and check for congruences + UseListNodeId currentUseId = currentNode.getUseList(); + while (currentUseId != null_uselist_id) { + // Get the node of the use list + UseListNode& useNode = d_useListNodes[currentUseId]; + // Get the function application + EqualityNodeId funId = useNode.getApplicationId(); + const FunctionApplication& fun = d_applications[useNode.getApplicationId()]; + // Get the application with find arguments + EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); + EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); + FunctionApplication funNormalized(aNormalized, bNormalized); + typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); + // If the id is the one we set, then we undo it + if (find != d_applicationLookup.end() && find->second == funId) { + d_applicationLookup.erase(find); + } + // Go to the next one in the use list + currentUseId = useNode.getNext(); + } + + // Move to the next node + currentId = currentNode.getNext(); + + } while (currentId != class2Id); + + // Update class2 representative information + Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): undoing representative info" << std::endl; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + + // Update it's find to class1 id + currentNode.setFind(class2Id); + + // Go through the trigger list (if any) and undo the class + TriggerId currentTrigger = d_nodeTriggers[currentId]; + while (currentTrigger != null_trigger) { + Trigger& trigger = d_equalityTriggers[currentTrigger]; + trigger.classId = class2Id; + currentTrigger = trigger.nextTrigger; + } + + // Move to the next node + currentId = currentNode.getNext(); + + } while (currentId != class2Id); + + // Now set any missing lookups and check for any congruences on backtrack + std::vector possibleCongruences; + Debug("equality") << "EqualityEngine::undoMerge(" << class1.getFind() << "," << class2Id << "): checking for any unset lookups" << std::endl; + do { + // Get the current node + EqualityNode& currentNode = getEqualityNode(currentId); + + // Go through the uselist and check for congruences + UseListNodeId currentUseId = currentNode.getUseList(); + while (currentUseId != null_uselist_id) { + // Get the node of the use list + UseListNode& useNode = d_useListNodes[currentUseId]; + // Get the function application + EqualityNodeId funId = useNode.getApplicationId(); + const FunctionApplication& fun = d_applications[useNode.getApplicationId()]; + // Get the application with find arguments + EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind(); + EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind(); + FunctionApplication funNormalized(aNormalized, bNormalized); + typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized); + Assert(find != d_applicationLookup.end()); + // If the id doesn't exist, we'll set it + if (find == d_applicationLookup.end()) { + d_applicationLookup[funNormalized] = funId; + } else { + // Otherwise, we might be congruent agaain + if (getEqualityNode(funId).getFind() != getEqualityNode(find->second).getFind()) { + // Damn, we might be merging again, but we'll check this later + enqueue(MergeCandidate(funId, find->second, MERGED_THROUGH_CONGRUENCE, TNode::null())); + } + } + // Go to the next one in the use list + currentUseId = useNode.getNext(); + } + + // Move to the next node + currentId = currentNode.getNext(); + + } while (currentId != class2Id); +} + +template +void EqualityEngine::backtrack() { + + // If we need to backtrack then do it + if (d_assertedEqualitiesCount < d_assertedEqualities.size()) { + + // Clear the propagation queue + while (!d_propagationQueue.empty()) { + d_propagationQueue.pop(); + } + + ++ d_stats.backtracksCount; + + Debug("equality") << "EqualityEngine::backtrack(): nodes" << std::endl; + + for (int i = (int)d_assertedEqualities.size() - 1, i_end = (int)d_assertedEqualitiesCount; i >= i_end; --i) { + // Get the ids of the merged classes + Equality& eq = d_assertedEqualities[i]; + // Undo the merge + undoMerge(d_equalityNodes[eq.lhs], d_equalityNodes[eq.rhs], eq.rhs); + } + + d_assertedEqualities.resize(d_assertedEqualitiesCount); + + Debug("equality") << "EqualityEngine::backtrack(): edges" << std::endl; + + for (int i = (int)d_equalityEdges.size() - 2, i_end = (int)(2*d_assertedEqualitiesCount); i >= i_end; i -= 2) { + EqualityEdge& edge1 = d_equalityEdges[i]; + EqualityEdge& edge2 = d_equalityEdges[i | 1]; + d_equalityGraph[edge2.getNodeId()] = edge1.getNext(); + d_equalityGraph[edge1.getNodeId()] = edge2.getNext(); + } + + d_equalityEdges.resize(2 * d_assertedEqualitiesCount); + + // Now repropagate if something got reenqueued + propagate(true); + } +} + +template +void EqualityEngine::addGraphEdge(EqualityNodeId t1, EqualityNodeId t2, MergeReasonType type, TNode reason) { + Debug("equality") << "EqualityEngine::addGraphEdge(" << d_nodes[t1] << "," << d_nodes[t2] << "," << reason << ")" << std::endl; + EqualityEdgeId edge = d_equalityEdges.size(); + d_equalityEdges.push_back(EqualityEdge(t2, d_equalityGraph[t1], type, reason)); + d_equalityEdges.push_back(EqualityEdge(t1, d_equalityGraph[t2], type, reason)); + d_equalityGraph[t1] = edge; + d_equalityGraph[t2] = edge | 1; + + if (Debug.isOn("equality::internal")) { + const_cast(this)->debugPrintGraph(); + } +} + +template +std::string EqualityEngine::edgesToString(EqualityEdgeId edgeId) const { + std::stringstream out; + bool first = true; + if (edgeId == null_edge) { + out << "null"; + } else { + while (edgeId != null_edge) { + const EqualityEdge& edge = d_equalityEdges[edgeId]; + if (!first) out << ","; + out << d_nodes[edge.getNodeId()]; + edgeId = edge.getNext(); + first = false; + } + } + return out.str(); +} + +template +void EqualityEngine::getExplanation(TNode t1, TNode t2, std::vector& equalities) const { + Assert(getRepresentative(t1) == getRepresentative(t2)); + + Debug("equality") << "EqualityEngine::getExplanation(" << t1 << "," << t2 << ")" << std::endl; + + // Backtrack if necessary + const_cast(this)->backtrack(); + + // Get the explanation + EqualityNodeId t1Id = getNodeId(t1); + EqualityNodeId t2Id = getNodeId(t2); + getExplanation(t1Id, t2Id, equalities); +} + +template +void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, std::vector& equalities) const { + + Debug("equality") << "EqualityEngine::getExplanation(" << d_nodes[t1Id] << "," << d_nodes[t2Id] << ")" << std::endl; + + // If the nodes are the same, we're done + if (t1Id == t2Id) return; + + if (Debug.isOn("equality::internal")) { + const_cast(this)->debugPrintGraph(); + } + + // Queue for the BFS containing nodes + std::vector bfsQueue; + + // Find a path from t1 to t2 in the graph (BFS) + bfsQueue.push_back(BfsData(t1Id, null_id, 0)); + size_t currentIndex = 0; + while (true) { + // There should always be a path, and every node can be visited only once (tree) + Assert(currentIndex < bfsQueue.size()); + + // The next node to visit + BfsData current = bfsQueue[currentIndex]; + EqualityNodeId currentNode = current.nodeId; + + Debug("equality") << "EqualityEngine::getExplanation(): currentNode = " << d_nodes[currentNode] << std::endl; + + // Go through the equality edges of this node + EqualityEdgeId currentEdge = d_equalityGraph[currentNode]; + Debug("equality") << "EqualityEngine::getExplanation(): edgesId = " << currentEdge << std::endl; + Debug("equality") << "EqualityEngine::getExplanation(): edges = " << edgesToString(currentEdge) << std::endl; + + while (currentEdge != null_edge) { + // Get the edge + const EqualityEdge& edge = d_equalityEdges[currentEdge]; + + // If not just the backwards edge + if ((currentEdge | 1u) != (current.edgeId | 1u)) { + + Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = (" << d_nodes[currentNode] << "," << d_nodes[edge.getNodeId()] << ")" << std::endl; + + // Did we find the path + if (edge.getNodeId() == t2Id) { + + Debug("equality") << "EqualityEngine::getExplanation(): path found: " << std::endl; + + // Reconstruct the path + do { + // The current node + currentNode = bfsQueue[currentIndex].nodeId; + EqualityNodeId edgeNode = d_equalityEdges[currentEdge].getNodeId(); + MergeReasonType reasonType = d_equalityEdges[currentEdge].getReasonType(); + + Debug("equality") << "EqualityEngine::getExplanation(): currentEdge = " << currentEdge << ", currentNode = " << currentNode << std::endl; + + // Add the actual equality to the vector + if (reasonType == MERGED_THROUGH_CONGRUENCE) { + // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2 + Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl; + const FunctionApplication& f1 = d_applications[currentNode]; + const FunctionApplication& f2 = d_applications[edgeNode]; + Debug("equality") << push; + getExplanation(f1.a, f2.a, equalities); + getExplanation(f1.b, f2.b, equalities); + Debug("equality") << pop; + } else { + // Construct the equality + Debug("equality") << "EqualityEngine::getExplanation(): adding: " << d_equalityEdges[currentEdge].getReason() << std::endl; + equalities.push_back(d_equalityEdges[currentEdge].getReason()); + } + + // Go to the previous + currentEdge = bfsQueue[currentIndex].edgeId; + currentIndex = bfsQueue[currentIndex].previousIndex; + } while (currentEdge != null_id); + + // Done + return; + } + + // Push to the visitation queue if it's not the backward edge + bfsQueue.push_back(BfsData(edge.getNodeId(), currentEdge, currentIndex)); + } + + // Go to the next edge + currentEdge = edge.getNext(); + } + + // Go to the next node to visit + ++ currentIndex; + } +} + +template +void EqualityEngine::addTriggerEquality(TNode t1, TNode t2, TNode trigger) { + + Debug("equality") << "EqualityEngine::addTrigger(" << t1 << ", " << t2 << ", " << trigger << ")" << std::endl; + + Assert(hasTerm(t1)); + Assert(hasTerm(t2)); + + // Get the information about t1 + EqualityNodeId t1Id = getNodeId(t1); + EqualityNodeId t1classId = getEqualityNode(t1Id).getFind(); + TriggerId t1TriggerId = d_nodeTriggers[t1Id]; + + // Get the information about t2 + EqualityNodeId t2Id = getNodeId(t2); + EqualityNodeId t2classId = getEqualityNode(t2Id).getFind(); + TriggerId t2TriggerId = d_nodeTriggers[t2Id]; + + Debug("equality") << "EqualityEngine::addTrigger(" << trigger << "): " << t1Id << " (" << t1classId << ") = " << t2Id << " (" << t2classId << ")" << std::endl; + + // Create the triggers + TriggerId t1NewTriggerId = d_equalityTriggers.size(); + TriggerId t2NewTriggerId = t1NewTriggerId | 1; + d_equalityTriggers.push_back(Trigger(t1classId, t1TriggerId)); + d_equalityTriggersOriginal.push_back(trigger); + d_equalityTriggers.push_back(Trigger(t2classId, t2TriggerId)); + d_equalityTriggersOriginal.push_back(trigger); + + // Add the trigger to the trigger graph + d_nodeTriggers[t1Id] = t1NewTriggerId; + d_nodeTriggers[t2Id] = t2NewTriggerId; + + // If the trigger is already on, we propagate + if (t1classId == t2classId) { + Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << "): triggered at setup time" << std::endl; + d_notify.notifyEquality(trigger); // Don't care about the return value + } + + Debug("equality") << "EqualityEngine::addTrigger(" << t1 << "," << t2 << ") => (" << t1NewTriggerId << ", " << t2NewTriggerId << ")" << std::endl; +} + +template +void EqualityEngine::propagate(bool check) { + + Debug("equality") << "EqualityEngine::propagate()" << std::endl; + + bool done = false; + while (!d_propagationQueue.empty()) { + + // The current merge candidate + const MergeCandidate current = d_propagationQueue.front(); + d_propagationQueue.pop(); + + if (done) { + // If we're done, just empty the queue + continue; + } + + // Get the representatives + EqualityNodeId t1classId = getEqualityNode(current.t1Id).getFind(); + EqualityNodeId t2classId = getEqualityNode(current.t2Id).getFind(); + + // If already the same, we're done + if (t1classId == t2classId) { + continue; + } + + // If check is on, and a congruence, check the arguments (it might be from a backtrack) + if (check && current.type == MERGED_THROUGH_CONGRUENCE) { + const FunctionApplication& f1 = d_applications[current.t1Id]; + const FunctionApplication& f2 = d_applications[current.t2Id]; + if (getEqualityNode(f1.a).getFind() != getEqualityNode(f2.a).getFind()) continue; + if (getEqualityNode(f1.b).getFind() != getEqualityNode(f2.b).getFind()) continue; + } + + // Get the nodes of the representatives + EqualityNode& node1 = getEqualityNode(t1classId); + EqualityNode& node2 = getEqualityNode(t2classId); + + Assert(node1.getFind() == t1classId); + Assert(node2.getFind() == t2classId); + + // Depending on the merge preference (such as size), merge them + std::vector triggers; + if (node2.getSize() > node1.getSize()) { + Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t1Id]<< " into " << d_nodes[current.t2Id] << std::endl; + merge(node2, node1, triggers); + d_assertedEqualities.push_back(Equality(t2classId, t1classId)); + } else { + Debug("equality") << "EqualityEngine::propagate(): merging " << d_nodes[current.t2Id] << " into " << d_nodes[current.t1Id] << std::endl; + merge(node1, node2, triggers); + d_assertedEqualities.push_back(Equality(t1classId, t2classId)); + } + + // Add the actuall equality to the equality graph + addGraphEdge(current.t1Id, current.t2Id, current.type, current.reason); + + // One more equality added + d_assertedEqualitiesCount = d_assertedEqualitiesCount + 1; + + Assert(2*d_assertedEqualities.size() == d_equalityEdges.size()); + Assert(d_assertedEqualities.size() == d_assertedEqualitiesCount); + + // Notify the triggers + for (size_t trigger = 0, trigger_end = triggers.size(); trigger < trigger_end && !done; ++ trigger) { + // Notify the trigger and exit if it fails + done = !d_notify.notifyEquality(d_equalityTriggersOriginal[triggers[trigger]]); + } + } +} + +template +void EqualityEngine::debugPrintGraph() { + for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) { + + Debug("equality::internal") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):"; + + EqualityEdgeId edgeId = d_equalityGraph[nodeId]; + while (edgeId != null_edge) { + const EqualityEdge& edge = d_equalityEdges[edgeId]; + Debug("equality::internal") << " " << d_nodes[edge.getNodeId()] << ":" << edge.getReason(); + edgeId = edge.getNext(); + } + + Debug("equality::internal") << std::endl; + } +} + +} // Namespace uf +} // Namespace theory +} // Namespace CVC4 + diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp new file mode 100644 index 000000000..0571126e6 --- /dev/null +++ b/src/theory/uf/theory_uf.cpp @@ -0,0 +1,214 @@ +/********************* */ +/*! \file theory_uf.cpp + ** \verbatim + ** Original author: dejan + ** 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 This is the interface to TheoryUF implementations + ** + ** This is the interface to TheoryUF implementations. All + ** implementations of TheoryUF should inherit from this class. + **/ + +#include "theory/uf/theory_uf.h" +#include "theory/uf/equality_engine_impl.h" + +using namespace CVC4; +using namespace CVC4::theory; +using namespace CVC4::theory::uf; + +using namespace std; + +Node mkAnd(const std::vector& conjunctions) { + Assert(conjunctions.size() > 0); + + std::set all; + all.insert(conjunctions.begin(), conjunctions.end()); + + if (all.size() == 1) { + // All the same, or just one + return conjunctions[0]; + } + + NodeBuilder<> conjunction(kind::AND); + std::set::const_iterator it = all.begin(); + std::set::const_iterator it_end = all.end(); + while (it != it_end) { + conjunction << *it; + ++ it; + } + + return conjunction; +} + +void TheoryUF::check(Effort level) { + + while (!done() && !d_conflict) { + // Get all the assertions + TNode assertion = get(); + Debug("uf") << "TheoryUF::check(): processing " << assertion << std::endl; + + // Fo the work + switch (assertion.getKind()) { + case kind::EQUAL: + d_equalityEngine.addEquality(assertion[0], assertion[1], assertion); + break; + case kind::APPLY_UF: + d_equalityEngine.addEquality(assertion, d_true, assertion); + case kind::NOT: + if (assertion[0].getKind() == kind::APPLY_UF) { + d_equalityEngine.addEquality(assertion[0], d_false, assertion); + } + break; + default: + Unreachable(); + } + } + + // If in conflict, output the conflict + if (d_conflict) { + Debug("uf") << "TheoryUF::check(): conflict " << d_conflictNode << std::endl; + d_out->conflict(d_conflictNode); + d_literalsToPropagate.clear(); + } + + // Otherwise we propagate in order to detect a weird conflict like + // p, x = y + // p -> f(x) != f(y) -- f(x) = f(y) gets added to the propagation list at preregistration time + // but when f(x) != f(y) is deduced by the sat solver, so it's asserted, and we don't detect the conflict + // until we go through the propagation list + propagate(level); +} + +void TheoryUF::propagate(Effort level) { + Debug("uf") << "TheoryUF::propagate()" << std::endl; + if (!d_conflict) { + for (unsigned i = 0; i < d_literalsToPropagate.size(); ++ i) { + TNode literal = d_literalsToPropagate[i]; + Debug("uf") << "TheoryUF::propagate(): propagating " << literal << std::endl; + bool satValue; + if (!d_valuation.hasSatValue(literal, satValue)) { + d_out->propagate(literal); + } else { + std::vector assumptions; + if (literal != d_false) { + TNode negatedLiteral = literal.getKind() == kind::NOT ? literal[0] : (TNode) literal.notNode(); + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + break; + } + } + } + d_literalsToPropagate.clear(); +} + +void TheoryUF::preRegisterTerm(TNode node) { + Debug("uf") << "TheoryUF::preRegisterTerm(" << node << ")" << std::endl; + + switch (node.getKind()) { + case kind::EQUAL: + // Add the terms + d_equalityEngine.addTerm(node[0]); + d_equalityEngine.addTerm(node[1]); + // Add the trigger + d_equalityEngine.addTriggerEquality(node[0], node[1], node); + break; + case kind::APPLY_UF: + // Function applications/predicates + d_equalityEngine.addTerm(node); + // Maybe it's a predicate + if (node.getType().isBoolean()) { + // Get triggered for both equal and dis-equal + d_equalityEngine.addTriggerEquality(node, d_true, node); + d_equalityEngine.addTriggerEquality(node, d_false, node.notNode()); + } + default: + // Variables etc + d_equalityEngine.addTerm(node); + break; + } +} + +bool TheoryUF::propagate(TNode atom, bool isTrue) { + Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ")" << std::endl; + + // If already in conflict, no more propagation + if (d_conflict) { + Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << "): already in conflict" << std::endl; + return false; + } + + // The literal + TNode literal = isTrue ? (Node) atom : atom.notNode(); + + // See if the literal has been asserted already + bool satValue = false; + bool isAsserted = literal == d_false || d_valuation.hasSatValue(literal, satValue); + + // If asserted, we're done or in conflict + if (isAsserted) { + if (satValue) { + Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => already known" << std::endl; + return true; + } else { + Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => conflict" << std::endl; + std::vector assumptions; + if (literal != d_false) { + TNode negatedLiteral = isTrue ? atom.notNode() : (Node) atom; + assumptions.push_back(negatedLiteral); + } + explain(literal, assumptions); + d_conflictNode = mkAnd(assumptions); + d_conflict = true; + return false; + } + } + + // Nothing, just enqueue it for propagation and mark it as asserted already + Debug("uf") << "TheoryUF::propagate(" << atom << ", " << (isTrue ? "true" : "false" ) << ") => enqueuing for propagation" << std::endl; + d_literalsToPropagate.push_back(literal); + + return true; +} + +void TheoryUF::explain(TNode literal, std::vector& assumptions) { + TNode lhs, rhs; + switch (literal.getKind()) { + case kind::EQUAL: + lhs = literal[0]; + rhs = literal[1]; + break; + case kind::APPLY_UF: + lhs = literal; + rhs = d_true; + break; + case kind::NOT: + lhs = literal[0]; + rhs = d_false; + case kind::CONST_BOOLEAN: + // we get to explain true = false, since we set false to be the trigger of this + lhs = d_true; + rhs = d_false; + break; + default: + Unreachable(); + } + d_equalityEngine.getExplanation(lhs, rhs, assumptions); +} + +void TheoryUF::explain(TNode literal) { + Debug("uf") << "TheoryUF::explain(" << literal << ")" << std::endl; + std::vector assumptions; + explain(literal, assumptions); + d_out->explanation(mkAnd(assumptions)); +} diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h index 34d6df881..266a1b7b4 100644 --- a/src/theory/uf/theory_uf.h +++ b/src/theory/uf/theory_uf.h @@ -1,7 +1,7 @@ /********************* */ /*! \file theory_uf.h ** \verbatim - ** Original author: mdeters + ** Original author: dejan ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. @@ -26,28 +26,97 @@ #include "expr/attribute.h" #include "theory/theory.h" +#include "theory/uf/equality_engine.h" -#include "context/context.h" +#include "context/cdo.h" +#include "context/cdset.h" namespace CVC4 { namespace theory { namespace uf { class TheoryUF : public Theory { + +public: + + class NotifyClass { + TheoryUF& d_uf; + public: + NotifyClass(TheoryUF& uf): d_uf(uf) {} + + bool notifyEquality(TNode eq) { + Debug("uf") << "NotifyClass::notifyEquality(" << eq << ")" << std::endl; + // Just forward to uf + return d_uf.propagate(eq, true); + } + }; + +private: + + /** The notify class */ + NotifyClass d_notify; + + /** Equaltity engine */ + EqualityEngine d_equalityEngine; + + /** All the literals known to be true */ + context::CDSet d_knownFacts; + + /** Are we in conflict */ + context::CDO d_conflict; + + /** The conflict node */ + Node d_conflictNode; + + /** + * Should be called to propagate the atom. If isTrue is true, the atom should be propagated, + * otherwise the negated atom should be propagated. + */ + bool propagate(TNode atom, bool isTrue); + + /** + * Explain why this literal is true by adding assumptions + */ + void explain(TNode literal, std::vector& assumptions); + + /** Literals to propagate */ + std::vector d_literalsToPropagate; + + /** True node for predicates = true */ + Node d_true; + + /** True node for predicates = false */ + Node d_false; + public: /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/ - TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation) - : Theory(THEORY_UF, ctxt, out, valuation) { } - - // We declare these here (even though it's not terribly useful) for - // documentation reasons, and to keep mktheorytraits from issuing a - // spurious warning. - virtual void check(Effort) = 0; - virtual void propagate(Effort) {} - virtual void staticLearning(TNode in, NodeBuilder<>& learned) {} - virtual void notifyRestart() {} - virtual void presolve() {} + TheoryUF(context::Context* ctxt, OutputChannel& out, Valuation valuation): + Theory(THEORY_UF, ctxt, out, valuation), + d_notify(*this), + d_equalityEngine(d_notify, ctxt, "theory::uf::TheoryUF"), + d_knownFacts(ctxt), + d_conflict(ctxt, false) + { + // The kinds we are treating as function application in congruence + d_equalityEngine.addFunctionKind(kind::APPLY_UF); + + // The boolean constants + d_true = NodeManager::currentNM()->mkConst(true); + d_false = NodeManager::currentNM()->mkConst(false); + d_equalityEngine.addTerm(d_true); + d_equalityEngine.addTerm(d_false); + d_equalityEngine.addTriggerEquality(d_true, d_false, d_false); + } + + void check(Effort); + void propagate(Effort); + void preRegisterTerm(TNode term); + void explain(TNode n); + + std::string identify() const { + return "THEORY_UF"; + } };/* class TheoryUF */ diff --git a/src/theory/valuation.cpp b/src/theory/valuation.cpp index 536255c2d..0aefd7f21 100644 --- a/src/theory/valuation.cpp +++ b/src/theory/valuation.cpp @@ -27,6 +27,10 @@ Node Valuation::getValue(TNode n) const { return d_engine->getValue(n); } +bool Valuation::hasSatValue(TNode n, bool& value) const { + return d_engine->getPropEngine()->hasValue(n, value); +} + Node Valuation::getSatValue(TNode n) const{ if(n.getKind() == kind::NOT) { Node atomRes = d_engine->getPropEngine()->getValue(n[0]); diff --git a/src/theory/valuation.h b/src/theory/valuation.h index 2346b6d32..ea6772ce8 100644 --- a/src/theory/valuation.h +++ b/src/theory/valuation.h @@ -51,6 +51,11 @@ public: */ Node getSatValue(TNode n) const; + /** + * Returns true if the node has a sat value. If yes value is set to it's value. + */ + bool hasSatValue(TNode n, bool& value) const; + };/* class Valuation */ }/* CVC4::theory namespace */ diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 01eaee999..45cf22232 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -19,7 +19,6 @@ TESTS = \ eq_diamond1.smt \ eq_diamond14.reduced.smt \ eq_diamond14.reduced2.smt \ - eq_diamond23.smt \ NEQ016_size5_reduced2a.smt \ NEQ016_size5_reduced2b.smt \ dead_dnd002.smt \