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