src/smt/env.h

   1 /******************************************************************************
   2  * Top contributors (to current version):
   3  *   Andrew Reynolds, Andres Noetzli, Morgan Deters
   4  *
   5  * This file is part of the cvc5 project.
   6  *
   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.
  11  * ****************************************************************************
  12  *
  13  * Smt Environment, main access to global utilities available to
  14  * internal code
  15  */
  16
  17 #include "cvc5_private.h"
  18
  19 #ifndef CVC5__SMT__ENV_H
  20 #define CVC5__SMT__ENV_H
  21
  22 #include <memory>
  23
  24 #include "options/options.h"
  25 #include "theory/logic_info.h"
  26 #include "util/statistics_registry.h"
  27
  28 namespace cvc5 {
  29
  30 class NodeManager;
  31 class StatisticsRegistry;
  32 class ProofNodeManager;
  33 class Printer;
  34 class ResourceManager;
  35
  36 namespace context {
  37 class Context;
  38 class UserContext;
  39 }  // namespace context
  40
  41 namespace smt {
  42 class DumpManager;
  43 }
  44
  45 namespace theory {
  46 class Rewriter;
  47 class TrustSubstitutionMap;
  48 }
  49
  50 /**
  51  * The environment class.
  52  *
  53  * This class lives in the SmtEngine and contains all utilities that are
  54  * globally available to all internal code.
  55  */
  56 class Env
  57 {
  58   friend class SmtEngine;
  59
  60  public:
  61   /**
  62    * Construct an Env with the given node manager.
  63    */
  64   Env(NodeManager* nm, const Options* opts);
  65   /** Destruct the env.  */
  66   ~Env();
  67
  68   /* Access to members------------------------------------------------------- */
  69   /** Get a pointer to the Context owned by this Env. */
  70   context::Context* getContext();
  71
  72   /** Get a pointer to the UserContext owned by this Env. */
  73   context::UserContext* getUserContext();
  74
  75   /** Get a pointer to the underlying NodeManager. */
  76   NodeManager* getNodeManager() const;
  77
  78   /**
  79    * Get the underlying proof node manager. Note since proofs depend on option
  80    * initialization, this is only available after the SmtEngine that owns this
  81    * environment is initialized, and only non-null if proofs are enabled.
  82    */
  83   ProofNodeManager* getProofNodeManager();
  84
  85   /**
  86    * Check whether the SAT solver should produce proofs. Other than whether
  87    * the proof node manager is set, SAT proofs are only generated when the
  88    * unsat core mode is not ASSUMPTIONS.
  89    */
  90   bool isSatProofProducing() const;
  91
  92   /**
  93    * Check whether theories should produce proofs as well. Other than whether
  94    * the proof node manager is set, theory engine proofs are conditioned on the
  95    * relationship between proofs and unsat cores: the unsat cores are in
  96    * FULL_PROOF mode, no proofs are generated on theory engine.
  97    */
  98   bool isTheoryProofProducing() const;
  99
 100   /** Get a pointer to the Rewriter owned by this Env. */
 101   theory::Rewriter* getRewriter();
 102
 103   /** Get a reference to the top-level substitution map */
 104   theory::TrustSubstitutionMap& getTopLevelSubstitutions();
 105
 106   /** Get a pointer to the underlying dump manager. */
 107   smt::DumpManager* getDumpManager();
 108
 109   /** Get the options object (const version only) owned by this Env. */
 110   const Options& getOptions() const;
 111
 112   /** Get the original options object (const version only). */
 113   const Options& getOriginalOptions() const;
 114
 115   /** Get the resource manager owned by this Env. */
 116   ResourceManager* getResourceManager() const;
 117
 118   /** Get the logic information currently set. */
 119   const LogicInfo& getLogicInfo() const;
 120
 121   /** Get a pointer to the StatisticsRegistry. */
 122   StatisticsRegistry& getStatisticsRegistry();
 123
 124   /* Option helpers---------------------------------------------------------- */
 125
 126   /**
 127    * Get the current printer based on the current options
 128    * @return the current printer
 129    */
 130   const Printer& getPrinter();
 131
 132   /**
 133    * Get the output stream that --dump=X should print to
 134    * @return the output stream
 135    */
 136   std::ostream& getDumpOut();
 137
 138  private:
 139   /* Private initialization ------------------------------------------------- */
 140
 141   /** Set proof node manager if it exists */
 142   void setProofNodeManager(ProofNodeManager* pnm);
 143
 144   /* Private shutdown ------------------------------------------------------- */
 145   /**
 146    * Shutdown method, which destroys the non-essential members of this class
 147    * in preparation for destroying SMT engine.
 148    */
 149   void shutdown();
 150   /* Members ---------------------------------------------------------------- */
 151
 152   /** The SAT context owned by this Env */
 153   std::unique_ptr<context::Context> d_context;
 154   /** User level context owned by this Env */
 155   std::unique_ptr<context::UserContext> d_userContext;
 156   /**
 157    * A pointer to the node manager of this environment. A node manager is
 158    * not necessarily unique to an SmtEngine instance.
 159    */
 160   NodeManager* d_nodeManager;
 161   /**
 162    * A pointer to the proof node manager, which is non-null if proofs are
 163    * enabled. This is owned by the proof manager of the SmtEngine that owns
 164    * this environment.
 165    */
 166   ProofNodeManager* d_proofNodeManager;
 167   /**
 168    * The rewriter owned by this Env. We have a different instance
 169    * of the rewriter for each Env instance. This is because rewriters may
 170    * hold references to objects that belong to theory solvers, which are
 171    * specific to an SmtEngine/TheoryEngine instance.
 172    */
 173   std::unique_ptr<theory::Rewriter> d_rewriter;
 174   /** The top level substitutions */
 175   std::unique_ptr<theory::TrustSubstitutionMap> d_topLevelSubs;
 176   /** The dump manager */
 177   std::unique_ptr<smt::DumpManager> d_dumpManager;
 178   /**
 179    * The logic we're in. This logic may be an extension of the logic set by the
 180    * user, which may be different from the user-provided logic due to the
 181    * options we have set.
 182    *
 183    * This is the authorative copy of the logic that internal subsolvers should
 184    * consider during solving and initialization.
 185    */
 186   LogicInfo d_logic;
 187   /**
 188    * The statistics registry owned by this Env.
 189    */
 190   std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
 191   /**
 192    * The options object, which contains the modified version of the options
 193    * provided as input to the SmtEngine that owns this environment. Note
 194    * that d_options may be modified by the options manager, e.g. based
 195    * on the input logic.
 196    *
 197    * This is the authorative copy of the options that internal subsolvers should
 198    * consider during solving and initialization.
 199    */
 200   Options d_options;
 201   /**
 202    * A pointer to the original options object as stored in the api::Solver.
 203    * The referenced objects holds the options as initially parsed before being
 204    * changed, e.g., by setDefaults().
 205    */
 206   const Options* d_originalOptions;
 207   /** Manager for limiting time and abstract resource usage. */
 208   std::unique_ptr<ResourceManager> d_resourceManager;
 209 }; /* class Env */
 210
 211 }  // namespace cvc5
 212
 213 #endif /* CVC5__SMT__ENV_H */