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