diff options
Diffstat (limited to 'src/theory/uf/theory_uf.h')
| -rw-r--r-- | src/theory/uf/theory_uf.h | 191 |
1 files changed, 7 insertions, 184 deletions
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 */ |