src/theory/combination_engine.h

   1 /*********************                                                        */
   2 /*! \file combination_engine.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-2021 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 Abstract interface for theory combination.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__COMBINATION_ENGINE__H
  18 #define CVC4__THEORY__COMBINATION_ENGINE__H
  19
  20 #include <vector>
  21 #include <memory>
  22
  23 #include "theory/ee_manager.h"
  24 #include "theory/valuation.h"
  25
  26 namespace cvc5 {
  27
  28 class TheoryEngine;
  29
  30 namespace theory {
  31
  32 class EagerProofGenerator;
  33 class ModelManager;
  34 class SharedSolver;
  35
  36 /**
  37  * Manager for doing theory combination. This class is responsible for:
  38  * (1) Initializing the various components of theory combination (equality
  39  * engine manager, model manager, shared solver) based on the equality engine
  40  * mode, and
  41  * (2) Implementing the main combination method (combineTheories).
  42  */
  43 class CombinationEngine
  44 {
  45  public:
  46   CombinationEngine(TheoryEngine& te,
  47                     const std::vector<Theory*>& paraTheories,
  48                     ProofNodeManager* pnm);
  49   virtual ~CombinationEngine();
  50
  51   /** Finish initialization */
  52   void finishInit();
  53
  54   /** Get equality engine theory information for theory with identifier tid. */
  55   const EeTheoryInfo* getEeTheoryInfo(TheoryId tid) const;
  56   //-------------------------- model
  57   /**
  58    * Reset the model maintained by this class. This resets all local information
  59    * that is unique to each check.
  60    */
  61   void resetModel();
  62   /**
  63    * Build the model maintained by this class.
  64    *
  65    * @return true if model building was successful.
  66    */
  67   virtual bool buildModel() = 0;
  68   /**
  69    * Post process the model maintained by this class. This is called after
  70    * a successful call to buildModel. This does any theory-specific
  71    * postprocessing of the model.
  72    *
  73    * @param incomplete Whether we are answering "unknown" instead of "sat".
  74    */
  75   void postProcessModel(bool incomplete);
  76   /**
  77    * Get the model object maintained by this class.
  78    */
  79   TheoryModel* getModel();
  80   //-------------------------- end model
  81   /**
  82    * Get the shared solver, which is the active component of theory combination
  83    * that TheoryEngine interacts with prior to calling combineTheories.
  84    */
  85   SharedSolver* getSharedSolver();
  86   /**
  87    * Called at the beginning of full effort
  88    */
  89   virtual void resetRound();
  90   /**
  91    * Combine theories, called after FULL effort passes with no lemmas
  92    * and before LAST_CALL effort is run. This adds necessary lemmas for
  93    * theory combination (e.g. splitting lemmas) to the parent TheoryEngine.
  94    */
  95   virtual void combineTheories() = 0;
  96
  97  protected:
  98   /** Is proof enabled? */
  99   bool isProofEnabled() const;
 100   /**
 101    * Get model equality engine notify. Return the notification object for
 102    * who listens to the model's equality engine (if any).
 103    */
 104   virtual eq::EqualityEngineNotify* getModelEqualityEngineNotify();
 105   /** Send lemma to the theory engine, atomsTo is the theory to send atoms to */
 106   void sendLemma(TrustNode trn, TheoryId atomsTo);
 107   /** Reference to the theory engine */
 108   TheoryEngine& d_te;
 109   /** Valuation for the engine */
 110   Valuation d_valuation;
 111   /** The proof node manager */
 112   ProofNodeManager* d_pnm;
 113   /** Logic info of theory engine (cached) */
 114   const LogicInfo& d_logicInfo;
 115   /** List of parametric theories of theory engine */
 116   const std::vector<Theory*> d_paraTheories;
 117   /**
 118    * The equality engine manager we are using. This class is responsible for
 119    * configuring equality engines for each theory.
 120    */
 121   std::unique_ptr<EqEngineManager> d_eemanager;
 122   /**
 123    * The model manager we are using. This class is responsible for building the
 124    * model.
 125    */
 126   std::unique_ptr<ModelManager> d_mmanager;
 127   /**
 128    * The shared solver. This class is responsible for performing combination
 129    * tasks (e.g. preregistration) during solving.
 130    */
 131   std::unique_ptr<SharedSolver> d_sharedSolver;
 132   /**
 133    * An eager proof generator, if proofs are enabled. This proof generator is
 134    * responsible for proofs of splitting lemmas generated in combineTheories.
 135    */
 136   std::unique_ptr<EagerProofGenerator> d_cmbsPg;
 137 };
 138
 139 }  // namespace theory
 140 }  // namespace cvc5
 141
 142 #endif /* CVC4__THEORY__COMBINATION_DISTRIBUTED__H */