src/theory/shared_solver.h

   1 /*********************                                                        */
   2 /*! \file shared_solver.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds
   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  ** \brief Base class for shared solver
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__SHARED_SOLVER__H
  18 #define CVC4__THEORY__SHARED_SOLVER__H
  19
  20 #include "expr/node.h"
  21 #include "theory/ee_setup_info.h"
  22 #include "theory/logic_info.h"
  23 #include "theory/shared_terms_database.h"
  24 #include "theory/term_registration_visitor.h"
  25 #include "theory/valuation.h"
  26
  27 namespace CVC4 {
  28
  29 class TheoryEngine;
  30
  31 namespace theory {
  32
  33 /**
  34  * A base class for shared solver. The shared solver is the component of theory
  35  * engine that behaves like a theory solver, and whose purpose is to ensure the
  36  * main theory combination method can be performed in CombinationEngine.
  37  * Its role is to:
  38  * (1) Notify the individual theories of shared terms via addSharedTerms,
  39  * (2) Be the official interface for equality statuses,
  40  * (3) Propagate equalities to TheoryEngine when necessary and explain them.
  41  */
  42 class SharedSolver
  43 {
  44  public:
  45   SharedSolver(TheoryEngine& te);
  46   virtual ~SharedSolver() {}
  47   //------------------------------------- initialization
  48   /**
  49    * Returns true if we need an equality engine, this has the same contract
  50    * as Theory::needsEqualityEngine.
  51    */
  52   virtual bool needsEqualityEngine(theory::EeSetupInfo& esi);
  53   /**
  54    * Set the equality engine. This should be called by equality engine manager
  55    * during EqEngineManager::initializeTheories.
  56    */
  57   virtual void setEqualityEngine(eq::EqualityEngine* ee) = 0;
  58   //------------------------------------- end initialization
  59   /**
  60    * Called when the given term t is pre-registered in TheoryEngine.
  61    *
  62    * This adds t as an equality to propagate in the shared terms database
  63    * if it is an equality, or adds its shared terms if it involves multiple
  64    * theories.
  65    *
  66    * @param t The term to preregister
  67    * @param multipleTheories Whether multiple theories are present in t.
  68    */
  69   void preRegisterShared(TNode t, bool multipleTheories);
  70   /**
  71    * Pre-notify assertion fact with the given atom. This is called when any
  72    * fact is asserted in TheoryEngine, just before it is dispatched to the
  73    * appropriate theory.
  74    *
  75    * This calls Theory::notifySharedTerm for the shared terms of the atom.
  76    */
  77   void preNotifySharedFact(TNode atom);
  78   /**
  79    * Get the equality status of a and b.
  80    *
  81    * This method is used by theories via Valuation mostly for determining their
  82    * care graph.
  83    */
  84   virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
  85   /**
  86    * Explain literal, which returns a conjunction of literals that entail
  87    * the given one.
  88    */
  89   virtual TrustNode explain(TNode literal, TheoryId id) = 0;
  90   /**
  91    * Assert equality to the shared terms database.
  92    *
  93    * This method is called by TheoryEngine when a fact has been marked to
  94    * send to THEORY_BUILTIN, meaning that shared terms database should
  95    * maintain this fact. This is the case when either an equality is
  96    * asserted from the SAT solver or a theory propagates an equality between
  97    * shared terms.
  98    */
  99   virtual void assertSharedEquality(TNode equality,
 100                                     bool polarity,
 101                                     TNode reason) = 0;
 102   /** Is term t a shared term? */
 103   virtual bool isShared(TNode t) const;
 104
 105   /**
 106    * Method called by equalityEngine when a becomes (dis-)equal to b and a and b
 107    * are shared with the theory. Returns false if there is a direct conflict
 108    * (via rewrite for example).
 109    */
 110   bool propagateSharedEquality(theory::TheoryId theory,
 111                                TNode a,
 112                                TNode b,
 113                                bool value);
 114   /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
 115   void sendLemma(TrustNode trn, TheoryId atomsTo);
 116
 117  protected:
 118   /** Solver-specific pre-register shared */
 119   virtual void preRegisterSharedInternal(TNode t) = 0;
 120   /** Reference to the theory engine */
 121   TheoryEngine& d_te;
 122   /** Logic info of theory engine (cached) */
 123   const LogicInfo& d_logicInfo;
 124   /** The database of shared terms.*/
 125   SharedTermsDatabase d_sharedTerms;
 126   /** Visitor for collecting shared terms */
 127   SharedTermsVisitor d_sharedTermsVisitor;
 128 };
 129
 130 }  // namespace theory
 131 }  // namespace CVC4
 132
 133 #endif /* CVC4__THEORY__SHARED_SOLVER__H */