src/theory/shared_terms_database.h

   1 /*********************                                                        */
   2 /*! \file shared_terms_database.h
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Morgan Deters
   6  ** Minor contributors (to current version): Tim King, Andrew Reynolds
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  New York University and The University of Iowa
   9  ** See the file COPYING in the top-level source directory for licensing
  10  ** information.\endverbatim
  11  **
  12  ** [[ Add lengthier description here ]]
  13  ** \todo document this file
  14  **/
  15
  16 #include "cvc4_private.h"
  17
  18 #pragma once
  19
  20 #include "expr/node.h"
  21 #include "theory/theory.h"
  22 #include "theory/uf/equality_engine.h"
  23 #include "util/statistics_registry.h"
  24 #include "context/cdhashset.h"
  25
  26 namespace CVC4 {
  27
  28 class TheoryEngine;
  29
  30 class SharedTermsDatabase : public context::ContextNotifyObj {
  31
  32 public:
  33
  34   /** A container for a list of shared terms */
  35   typedef std::vector<TNode> shared_terms_list;
  36
  37   /** The iterator to go through the shared terms list */
  38   typedef shared_terms_list::const_iterator shared_terms_iterator;
  39
  40 private:
  41
  42   /** Some statistics */
  43   IntStat d_statSharedTerms;
  44
  45   // Needs to be a map from Nodes as after a backtrack they might not exist
  46   typedef std::hash_map<Node, shared_terms_list, TNodeHashFunction> SharedTermsMap;
  47
  48   /** A map from atoms to a list of shared terms */
  49   SharedTermsMap d_atomsToTerms;
  50
  51   /** Each time we add a shared term, we add it's parent to this list */
  52   std::vector<TNode> d_addedSharedTerms;
  53
  54   /** Context-dependent size of the d_addedSharedTerms list */
  55   context::CDO<unsigned> d_addedSharedTermsSize;
  56
  57   /** A map from atoms and subterms to the theories that use it */
  58   typedef context::CDHashMap<std::pair<Node, TNode>, theory::Theory::Set, TNodePairHashFunction> SharedTermsTheoriesMap;
  59   SharedTermsTheoriesMap d_termsToTheories;
  60
  61   /** Map from term to theories that have already been notified about the shared term */
  62   typedef context::CDHashMap<TNode, theory::Theory::Set, TNodeHashFunction> AlreadyNotifiedMap;
  63   AlreadyNotifiedMap d_alreadyNotifiedMap;
  64
  65   /** The registered equalities for propagation */
  66   typedef context::CDHashSet<Node, NodeHashFunction> RegisteredEqualitiesSet;
  67   RegisteredEqualitiesSet d_registeredEqualities;
  68
  69 private:
  70
  71   /** This method removes all the un-necessary stuff from the maps */
  72   void backtrack();
  73
  74   // EENotifyClass: template helper class for d_equalityEngine - handles call-backs
  75   class EENotifyClass : public theory::eq::EqualityEngineNotify {
  76     SharedTermsDatabase& d_sharedTerms;
  77   public:
  78     EENotifyClass(SharedTermsDatabase& shared): d_sharedTerms(shared) {}
  79     bool eqNotifyTriggerEquality(TNode equality, bool value) {
  80       d_sharedTerms.propagateEquality(equality, value);
  81       return true;
  82     }
  83
  84     bool eqNotifyTriggerPredicate(TNode predicate, bool value) {
  85       Unreachable();
  86       return true;
  87     }
  88
  89     bool eqNotifyTriggerTermEquality(theory::TheoryId tag, TNode t1, TNode t2, bool value) {
  90       return d_sharedTerms.propagateSharedEquality(tag, t1, t2, value);
  91     }
  92
  93     void eqNotifyConstantTermMerge(TNode t1, TNode t2) {
  94       d_sharedTerms.conflict(t1, t2, true);
  95     }
  96
  97     void eqNotifyNewClass(TNode t) { }
  98     void eqNotifyPreMerge(TNode t1, TNode t2) { }
  99     void eqNotifyPostMerge(TNode t1, TNode t2) { }
 100     void eqNotifyDisequal(TNode t1, TNode t2, TNode reason) { }
 101   };
 102
 103   /** The notify class for d_equalityEngine */
 104   EENotifyClass d_EENotify;
 105
 106   /** Equality engine */
 107   theory::eq::EqualityEngine d_equalityEngine;
 108
 109   /**
 110    * Method called by equalityEngine when a becomes (dis-)equal to b and a and b are shared with
 111    * the theory. Returns false if there is a direct conflict (via rewrite for example).
 112    */
 113   bool propagateSharedEquality(theory::TheoryId theory, TNode a, TNode b, bool value);
 114
 115   /**
 116    * Called from the equality engine when a trigger equality is deduced.
 117    */
 118   bool propagateEquality(TNode equality, bool polarity);
 119
 120   /** Theory engine */
 121   TheoryEngine* d_theoryEngine;
 122
 123   /** Are we in conflict */
 124   context::CDO<bool> d_inConflict;
 125
 126   /** Conflicting terms, if any */
 127   Node d_conflictLHS, d_conflictRHS;
 128
 129   /** Polarity of the conflict */
 130   bool d_conflictPolarity;
 131
 132   /** Called by the equality engine notify to mark the conflict */
 133   void conflict(TNode lhs, TNode rhs, bool polarity) {
 134     if (!d_inConflict) {
 135       // Only remember it if we're not already in conflict
 136       d_inConflict = true;
 137       d_conflictLHS = lhs;
 138       d_conflictRHS = rhs;
 139       d_conflictPolarity = polarity;
 140     }
 141   }
 142
 143   /**
 144    * Should be called before any public non-const method in order to
 145    * enqueue the conflict to the theory engine.
 146    */
 147   void checkForConflict();
 148
 149 public:
 150
 151   SharedTermsDatabase(TheoryEngine* theoryEngine, context::Context* context);
 152   ~SharedTermsDatabase() throw(AssertionException);
 153
 154   /**
 155    * Asserts the equality to the shared terms database,
 156    */
 157   void assertEquality(TNode equality, bool polarity, TNode reason);
 158
 159   /**
 160    * Return whether the equality is alreday known to the engine
 161    */
 162   bool isKnown(TNode literal) const;
 163
 164   /**
 165    * Returns an explanation of the propagation that came from the database.
 166    */
 167   Node explain(TNode literal) const;
 168
 169   /**
 170    * Add an equality to propagate.
 171    */
 172   void addEqualityToPropagate(TNode equality);
 173
 174   /**
 175    * Add a shared term to the database. The shared term is a subterm of the atom and
 176    * should be associated with the given theory.
 177    */
 178   void addSharedTerm(TNode atom, TNode term, theory::Theory::Set theories);
 179
 180   /**
 181    * Mark that the given theories have been notified of the given shared term.
 182    */
 183   void markNotified(TNode term, theory::Theory::Set theories);
 184
 185   /**
 186    * Returns true if the atom contains any shared terms, false otherwise.
 187    */
 188   bool hasSharedTerms(TNode atom) const;
 189
 190   /**
 191    * Iterator pointing to the first shared term belonging to the given atom.
 192    */
 193   shared_terms_iterator begin(TNode atom) const;
 194
 195   /**
 196    * Iterator pointing to the end of the list of shared terms belonging to the given atom.
 197    */
 198   shared_terms_iterator end(TNode atom) const;
 199
 200   /**
 201    * Get the theories that share the term in a given atom (and have not yet been notified).
 202    */
 203   theory::Theory::Set getTheoriesToNotify(TNode atom, TNode term) const;
 204
 205   /**
 206    * Get the theories that share the term and have been notified already.
 207    */
 208   theory::Theory::Set getNotifiedTheories(TNode term) const;
 209
 210   /**
 211    * Returns true if the term is currently registered as shared with some theory.
 212    */
 213   bool isShared(TNode term) const {
 214     return d_alreadyNotifiedMap.find(term) != d_alreadyNotifiedMap.end();
 215   }
 216
 217   /**
 218    * Returns true if the literal is an (dis-)equality with both sides registered as shared with
 219    * some theory.
 220    */
 221   bool isSharedEquality(TNode literal) const {
 222     TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
 223     return atom.getKind() == kind::EQUAL && isShared(atom[0]) && isShared(atom[1]);
 224   }
 225
 226   /**
 227    * Returns true if the shared terms a and b are known to be equal.
 228    */
 229   bool areEqual(TNode a, TNode b) const;
 230
 231   /**
 232    * Retursn true if the shared terms a and b are known to be dis-equal.
 233    */
 234   bool areDisequal(TNode a, TNode b) const;
 235
 236   /**
 237    * get equality engine
 238    */
 239   theory::eq::EqualityEngine* getEqualityEngine() { return &d_equalityEngine; }
 240
 241 protected:
 242
 243   /**
 244    * This method gets called on backtracks from the context manager.
 245    */
 246   void contextNotifyPop() {
 247     backtrack();
 248   }
 249 };
 250
 251 }