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/base_options.h"
  25 #include "options/options.h"
  26 #include "proof/method_id.h"
  27 #include "theory/logic_info.h"
  28 #include "util/statistics_registry.h"
  29
  30 namespace cvc5 {
  31
  32 class NodeManager;
  33 class StatisticsRegistry;
  34 class ProofNodeManager;
  35 class Printer;
  36 class ResourceManager;
  37
  38 namespace context {
  39 class Context;
  40 class UserContext;
  41 }  // namespace context
  42
  43 namespace smt {
  44 class DumpManager;
  45 class PfManager;
  46 }
  47
  48 namespace theory {
  49 class Evaluator;
  50 class Rewriter;
  51 class TrustSubstitutionMap;
  52 }
  53
  54 /**
  55  * The environment class.
  56  *
  57  * This class lives in the SolverEngine and contains all utilities that are
  58  * globally available to all internal code.
  59  */
  60 class Env
  61 {
  62   friend class SolverEngine;
  63   friend class smt::PfManager;
  64
  65  public:
  66   /**
  67    * Construct an Env with the given node manager.
  68    */
  69   Env(NodeManager* nm, const Options* opts);
  70   /** Destruct the env.  */
  71   ~Env();
  72
  73   /* Access to members------------------------------------------------------- */
  74   /** Get a pointer to the Context owned by this Env. */
  75   context::Context* getContext();
  76
  77   /** Get a pointer to the UserContext owned by this Env. */
  78   context::UserContext* getUserContext();
  79
  80   /** Get a pointer to the underlying NodeManager. */
  81   NodeManager* getNodeManager() const;
  82
  83   /**
  84    * Get the underlying proof node manager. Note since proofs depend on option
  85    * initialization, this is only available after the SolverEngine that owns
  86    * this environment is initialized, and only non-null if proofs are enabled.
  87    */
  88   ProofNodeManager* getProofNodeManager();
  89
  90   /**
  91    * Check whether the SAT solver should produce proofs. Other than whether
  92    * the proof node manager is set, SAT proofs are only generated when the
  93    * unsat core mode is not ASSUMPTIONS.
  94    */
  95   bool isSatProofProducing() const;
  96
  97   /**
  98    * Check whether theories should produce proofs as well. Other than whether
  99    * the proof node manager is set, theory engine proofs are conditioned on the
 100    * relationship between proofs and unsat cores: the unsat cores are in
 101    * FULL_PROOF mode, no proofs are generated on theory engine.
 102    */
 103   bool isTheoryProofProducing() const;
 104
 105   /** Get a pointer to the Rewriter owned by this Env. */
 106   theory::Rewriter* getRewriter();
 107
 108   /** Get a reference to the top-level substitution map */
 109   theory::TrustSubstitutionMap& getTopLevelSubstitutions();
 110
 111   /** Get a pointer to the underlying dump manager. */
 112   smt::DumpManager* getDumpManager();
 113
 114   /** Get the options object (const version only) owned by this Env. */
 115   const Options& getOptions() const;
 116
 117   /** Get the original options object (const version only). */
 118   const Options& getOriginalOptions() const;
 119
 120   /** Get the resource manager owned by this Env. */
 121   ResourceManager* getResourceManager() const;
 122
 123   /** Get the logic information currently set. */
 124   const LogicInfo& getLogicInfo() const;
 125
 126   /** Get a pointer to the StatisticsRegistry. */
 127   StatisticsRegistry& getStatisticsRegistry();
 128
 129   /* Option helpers---------------------------------------------------------- */
 130
 131   /**
 132    * Get the current printer based on the current options
 133    * @return the current printer
 134    */
 135   const Printer& getPrinter();
 136
 137   /**
 138    * Get the output stream that --dump=X should print to
 139    * @return the output stream
 140    */
 141   std::ostream& getDumpOut();
 142
 143   /**
 144    * Check whether the output for the given output tag is enabled. Output tags
 145    * are enabled via the `output` option (or `-o` on the command line).
 146    */
 147   bool isOutputOn(options::OutputTag tag) const;
 148   /**
 149    * Check whether the output for the given output tag (as a string) is enabled.
 150    * Output tags are enabled via the `output` option (or `-o` on the command
 151    * line).
 152    */
 153   bool isOutputOn(const std::string& tag) const;
 154   /**
 155    * Return the output stream for the given output tag. If the output tag is
 156    * enabled, this returns the output stream from the `out` option. Otherwise,
 157    * a null stream (`cvc5::null_os`) is returned.
 158    */
 159   std::ostream& getOutput(options::OutputTag tag) const;
 160   /**
 161    * Return the output stream for the given output tag (as a string). If the
 162    * output tag is enabled, this returns the output stream from the `out`
 163    * option. Otherwise, a null stream (`cvc5::null_os`) is returned.
 164    */
 165   std::ostream& getOutput(const std::string& tag) const;
 166
 167   /* Rewrite helpers--------------------------------------------------------- */
 168   /**
 169    * Evaluate node n under the substitution args -> vals. For details, see
 170    * theory/evaluator.h.
 171    *
 172    * @param n The node to evaluate
 173    * @param args The domain of the substitution
 174    * @param vals The range of the substitution
 175    * @param useRewriter if true, we use this rewriter to rewrite subterms of
 176    * n that cannot be evaluated to a constant.
 177    * @return the rewritten, evaluated form of n under the given substitution.
 178    */
 179   Node evaluate(TNode n,
 180                 const std::vector<Node>& args,
 181                 const std::vector<Node>& vals,
 182                 bool useRewriter) const;
 183   /** Same as above, with a visited cache. */
 184   Node evaluate(TNode n,
 185                 const std::vector<Node>& args,
 186                 const std::vector<Node>& vals,
 187                 const std::unordered_map<Node, Node>& visited,
 188                 bool useRewriter = true) const;
 189   /**
 190    * Apply rewrite on n via the rewrite method identifier idr (see method_id.h).
 191    * This encapsulates the exact behavior of a REWRITE step in a proof.
 192    *
 193    * @param n The node to rewrite,
 194    * @param idr The method identifier of the rewriter, by default RW_REWRITE
 195    * specifying a call to rewrite.
 196    * @return The rewritten form of n.
 197    */
 198   Node rewriteViaMethod(TNode n, MethodId idr = MethodId::RW_REWRITE);
 199
 200  private:
 201   /* Private initialization ------------------------------------------------- */
 202
 203   /** Set proof node manager if it exists */
 204   void setProofNodeManager(ProofNodeManager* pnm);
 205
 206   /* Private shutdown ------------------------------------------------------- */
 207   /**
 208    * Shutdown method, which destroys the non-essential members of this class
 209    * in preparation for destroying SMT engine.
 210    */
 211   void shutdown();
 212   /* Members ---------------------------------------------------------------- */
 213
 214   /** The SAT context owned by this Env */
 215   std::unique_ptr<context::Context> d_context;
 216   /** User level context owned by this Env */
 217   std::unique_ptr<context::UserContext> d_userContext;
 218   /**
 219    * A pointer to the node manager of this environment. A node manager is
 220    * not necessarily unique to an SolverEngine instance.
 221    */
 222   NodeManager* d_nodeManager;
 223   /**
 224    * A pointer to the proof node manager, which is non-null if proofs are
 225    * enabled. This is owned by the proof manager of the SolverEngine that owns
 226    * this environment.
 227    */
 228   ProofNodeManager* d_proofNodeManager;
 229   /**
 230    * The rewriter owned by this Env. We have a different instance
 231    * of the rewriter for each Env instance. This is because rewriters may
 232    * hold references to objects that belong to theory solvers, which are
 233    * specific to an SolverEngine/TheoryEngine instance.
 234    */
 235   std::unique_ptr<theory::Rewriter> d_rewriter;
 236   /** Evaluator that also invokes the rewriter */
 237   std::unique_ptr<theory::Evaluator> d_evalRew;
 238   /** Evaluator that does not invoke the rewriter */
 239   std::unique_ptr<theory::Evaluator> d_eval;
 240   /** The top level substitutions */
 241   std::unique_ptr<theory::TrustSubstitutionMap> d_topLevelSubs;
 242   /** The dump manager */
 243   std::unique_ptr<smt::DumpManager> d_dumpManager;
 244   /**
 245    * The logic we're in. This logic may be an extension of the logic set by the
 246    * user, which may be different from the user-provided logic due to the
 247    * options we have set.
 248    *
 249    * This is the authorative copy of the logic that internal subsolvers should
 250    * consider during solving and initialization.
 251    */
 252   LogicInfo d_logic;
 253   /**
 254    * The statistics registry owned by this Env.
 255    */
 256   std::unique_ptr<StatisticsRegistry> d_statisticsRegistry;
 257   /**
 258    * The options object, which contains the modified version of the options
 259    * provided as input to the SolverEngine that owns this environment. Note
 260    * that d_options may be modified by the options manager, e.g. based
 261    * on the input logic.
 262    *
 263    * This is the authorative copy of the options that internal subsolvers should
 264    * consider during solving and initialization.
 265    */
 266   Options d_options;
 267   /**
 268    * A pointer to the original options object as stored in the api::Solver.
 269    * The referenced objects holds the options as initially parsed before being
 270    * changed, e.g., by setDefaults().
 271    */
 272   const Options* d_originalOptions;
 273   /** Manager for limiting time and abstract resource usage. */
 274   std::unique_ptr<ResourceManager> d_resourceManager;
 275 }; /* class Env */
 276
 277 }  // namespace cvc5
 278
 279 #endif /* CVC5__SMT__ENV_H */