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 term t is pre-registered in TheoryEngine.
  62    *
  63    * This adds t as an equality to propagate in the shared terms database
  64    * if it is an equality, or adds its shared terms if it involves multiple
  65    * theories.
  66    *
  67    * @param t The term to preregister
  68    * @param multipleTheories Whether multiple theories are present in t.
  69    */
  70   void preRegisterShared(TNode t, bool multipleTheories);
  71   /**
  72    * Pre-notify assertion fact with the given atom. This is called when any
  73    * fact is asserted in TheoryEngine, just before it is dispatched to the
  74    * appropriate theory.
  75    *
  76    * This calls Theory::notifySharedTerm for the shared terms of the atom.
  77    */
  78   void preNotifySharedFact(TNode atom);
  79   /**
  80    * Get the equality status of a and b.
  81    *
  82    * This method is used by theories via Valuation mostly for determining their
  83    * care graph.
  84    */
  85   virtual EqualityStatus getEqualityStatus(TNode a, TNode b);
  86   /**
  87    * Explain literal, which returns a conjunction of literals that entail
  88    * the given one.
  89    */
  90   virtual TrustNode explain(TNode literal, TheoryId id) = 0;
  91   /**
  92    * Assert equality to the shared terms database.
  93    *
  94    * This method is called by TheoryEngine when a fact has been marked to
  95    * send to THEORY_BUILTIN, meaning that shared terms database should
  96    * maintain this fact. This is the case when either an equality is
  97    * asserted from the SAT solver or a theory propagates an equality between
  98    * shared terms.
  99    */
 100   virtual void assertSharedEquality(TNode equality,
 101                                     bool polarity,
 102                                     TNode reason) = 0;
 103   /** Is term t a shared term? */
 104   virtual bool isShared(TNode t) const;
 105
 106   /**
 107    * Method called by equalityEngine when a becomes (dis-)equal to b and a and b
 108    * are shared with the theory. Returns false if there is a direct conflict
 109    * (via rewrite for example).
 110    */
 111   bool propagateSharedEquality(theory::TheoryId theory,
 112                                TNode a,
 113                                TNode b,
 114                                bool value);
 115   /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
 116   void sendLemma(TrustNode trn, TheoryId atomsTo);
 117
 118  protected:
 119   /** Solver-specific pre-register shared */
 120   virtual void preRegisterSharedInternal(TNode t) = 0;
 121   /** Reference to the theory engine */
 122   TheoryEngine& d_te;
 123   /** Logic info of theory engine (cached) */
 124   const LogicInfo& d_logicInfo;
 125   /** The database of shared terms.*/
 126   SharedTermsDatabase d_sharedTerms;
 127   /** Visitor for collecting shared terms */
 128   SharedTermsVisitor d_sharedTermsVisitor;
 129 };
 130
 131 }  // namespace theory
 132 }  // namespace CVC4
 133
 134 #endif /* CVC4__THEORY__SHARED_SOLVER__H */