src/theory/uf/theory_uf.h

   1 /*********************                                                        */
   2 /*! \file theory_uf.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Morgan Deters, Tim King
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2016 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief This is the interface to TheoryUF implementations
  13  **
  14  ** This is the interface to TheoryUF implementations.  All
  15  ** implementations of TheoryUF should inherit from this class.
  16  **/
  17
  18 #include "cvc4_private.h"
  19
  20 #ifndef __CVC4__THEORY__UF__THEORY_UF_H
  21 #define __CVC4__THEORY__UF__THEORY_UF_H
  22
  23 #include "expr/node.h"
  24 //#include "expr/attribute.h"
  25
  26 #include "theory/theory.h"
  27 #include "theory/uf/equality_engine.h"
  28 #include "theory/uf/symmetry_breaker.h"
  29
  30 #include "context/cdo.h"
  31 #include "context/cdhashset.h"
  32
  33 namespace CVC4 {
  34 namespace theory {
  35
  36 namespace quantifiers{
  37   class TermArgTrie;
  38 }
  39
  40 namespace uf {
  41
  42 class UfTermDb;
  43 class StrongSolverTheoryUF;
  44
  45 class TheoryUF : public Theory {
  46
  47   friend class StrongSolverTheoryUF;
  48
  49 public:
  50
  51   class NotifyClass : public eq::EqualityEngineNotify {
  52     TheoryUF& d_uf;
  53   public:
  54     NotifyClass(TheoryUF& uf): d_uf(uf) {}
  55
  56     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  57       Debug("uf") << "NotifyClass::eqNotifyTriggerEquality(" << equality << ", " << (value ? "true" : "false" )<< ")" << std::endl;
  58       if (value) {
  59         return d_uf.propagate(equality);
  60       } else {
  61         // We use only literal triggers so taking not is safe
  62         return d_uf.propagate(equality.notNode());
  63       }
  64     }
  65
  66     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  67       Debug("uf") << "NotifyClass::eqNotifyTriggerPredicate(" << predicate << ", " << (value ? "true" : "false") << ")" << std::endl;
  68       if (value) {
  69         return d_uf.propagate(predicate);
  70       } else {
  71        return d_uf.propagate(predicate.notNode());
  72       }
  73     }
  74
  75     bool eqNotifyTriggerTermEquality(TheoryId tag, TNode t1, TNode t2, bool value) {
  76       Debug("uf") << "NotifyClass::eqNotifyTriggerTermMerge(" << tag << ", " << t1 << ", " << t2 << ")" << std::endl;
  77       if (value) {
  78         return d_uf.propagate(t1.eqNode(t2));
  79       } else {
  80         return d_uf.propagate(t1.eqNode(t2).notNode());
  81       }
  82     }
  83
  84     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  85       Debug("uf-notify") << "NotifyClass::eqNotifyConstantTermMerge(" << t1 << ", " << t2 << ")" << std::endl;
  86       d_uf.conflict(t1, t2);
  87     }
  88
  89     void eqNotifyNewClass(TNode t) {
  90       Debug("uf-notify") << "NotifyClass::eqNotifyNewClass(" << t << ")" << std::endl;
  91       d_uf.eqNotifyNewClass(t);
  92     }
  93
  94     void eqNotifyPreMerge(TNode t1, TNode t2) {
  95       Debug("uf-notify") << "NotifyClass::eqNotifyPreMerge(" << t1 << ", " << t2 << ")" << std::endl;
  96       d_uf.eqNotifyPreMerge(t1, t2);
  97     }
  98
  99     void eqNotifyPostMerge(TNode t1, TNode t2) {
 100       Debug("uf-notify") << "NotifyClass::eqNotifyPostMerge(" << t1 << ", " << t2 << ")" << std::endl;
 101       d_uf.eqNotifyPostMerge(t1, t2);
 102     }
 103
 104     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) {
 105       Debug("uf-notify") << "NotifyClass::eqNotifyDisequal(" << t1 << ", " << t2 << ", " << reason << ")" << std::endl;
 106       d_uf.eqNotifyDisequal(t1, t2, reason);
 107     }
 108
 109   };/* class TheoryUF::NotifyClass */
 110
 111 private:
 112
 113   /** The notify class */
 114   NotifyClass d_notify;
 115
 116   /** The associated theory strong solver (or NULL if none) */
 117   StrongSolverTheoryUF* d_thss;
 118
 119   /** Equaltity engine */
 120   eq::EqualityEngine d_equalityEngine;
 121
 122   /** Are we in conflict */
 123   context::CDO<bool> d_conflict;
 124
 125   /** The conflict node */
 126   Node d_conflictNode;
 127
 128   /**
 129    * Should be called to propagate the literal. We use a node here
 130    * since some of the propagated literals are not kept anywhere.
 131    */
 132   bool propagate(TNode literal);
 133
 134   /**
 135    * Explain why this literal is true by adding assumptions
 136    * with proof (if "pf" is non-NULL).
 137    */
 138   void explain(TNode literal, std::vector<TNode>& assumptions, eq::EqProof* pf);
 139
 140   /**
 141    * Explain a literal, with proof (if "pf" is non-NULL).
 142    */
 143   Node explain(TNode literal, eq::EqProof* pf);
 144
 145   /** Literals to propagate */
 146   context::CDList<Node> d_literalsToPropagate;
 147
 148   /** Index of the next literal to propagate */
 149   context::CDO<unsigned> d_literalsToPropagateIndex;
 150
 151   /** All the function terms that the theory has seen */
 152   context::CDList<TNode> d_functionsTerms;
 153
 154   /** Symmetry analyzer */
 155   SymmetryBreaker d_symb;
 156
 157   /** Conflict when merging two constants */
 158   void conflict(TNode a, TNode b);
 159
 160   /** called when a new equivalance class is created */
 161   void eqNotifyNewClass(TNode t);
 162
 163   /** called when two equivalance classes will merge */
 164   void eqNotifyPreMerge(TNode t1, TNode t2);
 165
 166   /** called when two equivalance classes have merged */
 167   void eqNotifyPostMerge(TNode t1, TNode t2);
 168
 169   /** called when two equivalence classes are made disequal */
 170   void eqNotifyDisequal(TNode t1, TNode t2, TNode reason);
 171
 172 public:
 173
 174   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
 175   TheoryUF(context::Context* c, context::UserContext* u, OutputChannel& out,
 176            Valuation valuation, const LogicInfo& logicInfo,
 177            std::string instanceName = "");
 178
 179   ~TheoryUF();
 180
 181   void setMasterEqualityEngine(eq::EqualityEngine* eq);
 182   void finishInit();
 183
 184   void check(Effort);
 185   void preRegisterTerm(TNode term);
 186   Node explain(TNode n);
 187
 188   void collectModelInfo( TheoryModel* m, bool fullModel );
 189
 190   void ppStaticLearn(TNode in, NodeBuilder<>& learned);
 191   void presolve();
 192
 193   void addSharedTerm(TNode n);
 194   void computeCareGraph();
 195
 196   void propagate(Effort effort);
 197   Node getNextDecisionRequest( unsigned& priority );
 198
 199   EqualityStatus getEqualityStatus(TNode a, TNode b);
 200
 201   std::string identify() const {
 202     return "THEORY_UF";
 203   }
 204
 205   eq::EqualityEngine* getEqualityEngine() {
 206     return &d_equalityEngine;
 207   }
 208
 209   StrongSolverTheoryUF* getStrongSolver() {
 210     return d_thss;
 211   }
 212 private:
 213   void addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArgTrie * t2, unsigned arity, unsigned depth );
 214 };/* class TheoryUF */
 215
 216 }/* CVC4::theory::uf namespace */
 217 }/* CVC4::theory namespace */
 218 }/* CVC4 namespace */
 219
 220 #endif /* __CVC4__THEORY__UF__THEORY_UF_H */