src/theory/uf/theory_uf.h

   1 /*********************                                                        */
   2 /** theory_uf.h
   3  ** Original author: taking
   4  ** Major contributors: none
   5  ** Minor contributors (to current version): none
   6  ** This file is part of the CVC4 prototype.
   7  ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
   8  ** Courant Institute of Mathematical Sciences
   9  ** New York University
  10  ** See the file COPYING in the top-level source directory for licensing
  11  ** information.
  12  **
  13  **
  14  **/
  15
  16
  17 #ifndef __CVC4__THEORY__THEORY_UF_H
  18 #define __CVC4__THEORY__THEORY_UF_H
  19
  20 #include "expr/node.h"
  21 #include "expr/attribute.h"
  22
  23 #include "theory/theory.h"
  24
  25 #include "context/context.h"
  26 #include "theory/uf/ecdata.h"
  27
  28 namespace CVC4 {
  29 namespace theory {
  30 namespace uf {
  31
  32 class TheoryUF : public TheoryImpl<TheoryUF> {
  33
  34 private:
  35
  36
  37
  38   /**
  39    * The associated context. Needed for allocating context dependent objects
  40    * and objects in context dependent memory.
  41    */
  42   context::Context* d_context;
  43
  44   /**
  45    * List of pending equivalence class merges.
  46    *
  47    * Tricky part:
  48    * Must keep a hard link because new equality terms are created and appended
  49    * to this list.
  50    */
  51   context::CDList<Node> d_pending;
  52
  53   /** Index of the next pending equality to merge. */
  54   context::CDO<unsigned> d_currentPendingIdx;
  55
  56   /** List of all disequalities this theory has seen. */
  57   context::CDList<Node> d_disequality;
  58
  59   /**
  60    * List of all of the terms that are registered in the current context.
  61    * When registerTerm is called on a term we want to guarentee that there
  62    * is a hard link to the term for the duration of the context in which
  63    * register term is called.
  64    * This invariant is enough for us to use soft links where we want is the
  65    * current implementation as well as making ECAttr() not context dependent.
  66    * Soft links used both in ECData, and Link.
  67    */
  68   context::CDList<Node> d_registered;
  69
  70 public:
  71
  72   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
  73   TheoryUF(context::Context* c, OutputChannel& out);
  74
  75   /** Destructor for the TheoryUF object. */
  76   ~TheoryUF();
  77
  78
  79   //TODO Tim: I am going to delay documenting these functions while Morgan
  80   //has pending changes to the contracts
  81
  82   void registerTerm(TNode n);
  83   void preRegisterTerm(TNode n);
  84
  85   void check(Effort level);
  86
  87   void propagate(Effort level) {}
  88
  89   void explain(TNode n, Effort level) {}
  90
  91 private:
  92   /**
  93    * Checks whether 2 nodes are already in the same equivalence class tree.
  94    * This should only be used internally, and it should only be done when
  95    * the only thing done with the equivalence classes is an equality check.
  96    *
  97    * @returns true iff ccFind(x) == ccFind(y);
  98    */
  99   bool sameCongruenceClass(TNode x, TNode y);
 100
 101   /**
 102    * Checks whether Node x and Node y are currently congruent
 103    * using the equivalence class data structures.
 104    * @returns true iff
 105    *    |x| = n = |y| and
 106    *    x.getOperator() == y.getOperator() and
 107    *    forall 1 <= i < n : ccFind(x[i]) == ccFind(y[i])
 108    */
 109   bool equiv(TNode x, TNode y);
 110
 111   /**
 112    * Merges 2 equivalence classes, checks wether any predecessors need to
 113    * be set equal to complete congruence closure.
 114    * The class with the smaller class size will be merged.
 115    * @pre ecX->isClassRep()
 116    * @pre ecY->isClassRep()
 117    */
 118   void ccUnion(ECData* ecX, ECData* ecY);
 119
 120   /**
 121    * Returns the representative of the equivalence class.
 122    * May modify the find pointers associated with equivalence classes.
 123    */
 124   ECData* ccFind(ECData* x);
 125
 126   /** Performs Congruence Closure to reflect the new additions to d_pending. */
 127   void merge();
 128
 129 };
 130
 131
 132 /**
 133  * Cleanup function for ECData. This will be used for called whenever
 134  * a ECAttr is being destructed.
 135  */
 136 struct ECCleanupFcn{
 137   static void cleanup(ECData* & ec){
 138     ec->deleteSelf();
 139   }
 140 };
 141
 142 /** Unique name to use for constructing ECAttr. */
 143 struct EquivClass;
 144
 145 /**
 146  * ECAttr is the attribute that maps a node to an equivalence class.
 147  */
 148 typedef expr::Attribute<EquivClass, ECData* /*, ECCleanupFcn*/> ECAttr;
 149
 150 } /* CVC4::theory::uf namespace */
 151 } /* CVC4::theory namespace */
 152 } /* CVC4 namespace */
 153
 154
 155 #endif /* __CVC4__THEORY__THEORY_UF_H */