src/theory/shared_terms_database.h

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