src/theory/model_manager.h

   1 /*********************                                                        */
   2 /*! \file model_manager.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 management of models for TheoryEngine.
  13  **/
  14
  15 #include "cvc4_private.h"
  16
  17 #ifndef CVC4__THEORY__MODEL_MANAGER__H
  18 #define CVC4__THEORY__MODEL_MANAGER__H
  19
  20 #include <memory>
  21
  22 #include "theory/ee_manager.h"
  23 #include "theory/logic_info.h"
  24 #include "theory/theory_model.h"
  25 #include "theory/theory_model_builder.h"
  26
  27 namespace CVC4 {
  28
  29 class TheoryEngine;
  30
  31 namespace theory {
  32
  33 /**
  34  * A base class for managing models. Its main feature is to implement a
  35  * buildModel command. Overall, its behavior is specific to the kind of equality
  36  * engine management mode we are using. In particular, the prepare model
  37  * method is a manager-specific way for setting up the equality engine of the
  38  * model in preparation for model building.
  39  */
  40 class ModelManager
  41 {
  42  public:
  43   ModelManager(TheoryEngine& te, EqEngineManager& eem);
  44   virtual ~ModelManager();
  45   /**
  46    * Finish initializing this class, which allocates the model, the model
  47    * builder as well as the equality engine of the model. The equality engine
  48    * to use is determined by the virtual method initializeModelEqEngine.
  49    *
  50    * @param notify The object that wants to be notified for callbacks occurring
  51    */
  52   void finishInit(eq::EqualityEngineNotify* notify);
  53   /** Reset model, called during full effort check before the model is built */
  54   void resetModel();
  55   /**
  56    * Build the model. If we have yet to build the model on this round, this
  57    * method calls the (manager-specific) prepareModel method and then calls
  58    * finishBuildModel.
  59    *
  60    * @return true if model building was successful.
  61    */
  62   bool buildModel();
  63   /**
  64    * Have we called buildModel this round? Note this returns true whether or
  65    * not the model building was successful.
  66    */
  67   bool isModelBuilt() const;
  68   /**
  69    * Post process model, which is used as a way of each theory adding additional
  70    * information to the model after successfully building a model.
  71    */
  72   void postProcessModel(bool incomplete);
  73   /** Get a pointer to model object maintained by this class. */
  74   theory::TheoryModel* getModel();
  75   //------------------------ finer grained control over model building
  76   /**
  77    * Prepare model, which is the manager-specific method for setting up the
  78    * equality engine of the model. This should assert all relevant information
  79    * about the model into the equality engine of d_model.
  80    *
  81    * @return true if we are in conflict (i.e. the equality engine of the model
  82    * equality engine is inconsistent).
  83    */
  84   virtual bool prepareModel() = 0;
  85   /**
  86    * Finish build model, which calls the theory model builder to assign values
  87    * to all equivalence classes. This should be run after prepareModel.
  88    *
  89    * @return true if model building was successful.
  90    */
  91   virtual bool finishBuildModel() const = 0;
  92   //------------------------ end finer grained control over model building
  93  protected:
  94   /**
  95    * Initialize model equality engine. This is called at the end of finish
  96    * init, after we have created a model object but before we have assigned it
  97    * an equality engine.
  98    */
  99   virtual void initializeModelEqEngine(eq::EqualityEngineNotify* notify) = 0;
 100   /**
 101    * Collect model Boolean variables.
 102    * This asserts the values of all boolean variables to the equality engine of
 103    * the model, based on their value in the prop engine.
 104    *
 105    * @return true if we are in conflict.
 106    */
 107   bool collectModelBooleanVariables();
 108   /**
 109    * Collect asserted terms for theory with the given identifier, add to
 110    * termSet.
 111    *
 112    * @param tid The theory whose assertions we are collecting
 113    * @param termSet The set to add terms to
 114    * @param includeShared Whether to include the shared terms of the theory
 115    */
 116   void collectAssertedTerms(TheoryId tid,
 117                             std::set<Node>& termSet,
 118                             bool includeShared = true) const;
 119   /**
 120    * Helper function for collectAssertedTerms, adds all subterms
 121    * belonging to theory tid to termSet.
 122    */
 123   void collectTerms(TheoryId tid, TNode n, std::set<Node>& termSet) const;
 124   /** Reference to the theory engine */
 125   TheoryEngine& d_te;
 126   /** Logic info of theory engine (cached) */
 127   const LogicInfo& d_logicInfo;
 128   /** The equality engine manager */
 129   EqEngineManager& d_eem;
 130   /**
 131    * A dummy context for the model equality engine, so we can clear it
 132    * independently of search context.
 133    */
 134   context::Context d_modelEeContext;
 135   /** Pointer to the equality engine of the model */
 136   eq::EqualityEngine* d_modelEqualityEngine;
 137   /** The equality engine of the model, if we allocated it */
 138   std::unique_ptr<eq::EqualityEngine> d_modelEqualityEngineAlloc;
 139   /** The model object we are using */
 140   theory::TheoryModel* d_model;
 141   /** The model object we have allocated (if one exists) */
 142   std::unique_ptr<theory::TheoryModel> d_alocModel;
 143   /** The model builder object we are using */
 144   theory::TheoryEngineModelBuilder* d_modelBuilder;
 145   /** The model builder object we have allocated (if one exists) */
 146   std::unique_ptr<theory::TheoryEngineModelBuilder> d_alocModelBuilder;
 147   /** whether we have tried to build this model in the current context */
 148   bool d_modelBuilt;
 149   /** whether this model has been built successfully */
 150   bool d_modelBuiltSuccess;
 151 };
 152
 153 }  // namespace theory
 154 }  // namespace CVC4
 155
 156 #endif /* CVC4__THEORY__MODEL_MANAGER__H */