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