src/theory/shared_terms_database.h

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