1 /******************************************************************************
2 * Top contributors (to current version):
3 * Andrew Reynolds, Andres Noetzli, Morgan Deters
5 * This file is part of the cvc5 project.
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 * ****************************************************************************
13 * Smt Environment, main access to global utilities available to
17 #include "cvc5_private.h"
19 #ifndef CVC5__SMT__ENV_H
20 #define CVC5__SMT__ENV_H
24 #include "options/options.h"
25 #include "theory/logic_info.h"
26 #include "util/statistics_registry.h"
31 class StatisticsRegistry
;
32 class ProofNodeManager
;
34 class ResourceManager
;
39 } // namespace context
48 class TrustSubstitutionMap
;
52 * The environment class.
54 * This class lives in the SmtEngine and contains all utilities that are
55 * globally available to all internal code.
59 friend class SmtEngine
;
60 friend class smt::PfManager
;
64 * Construct an Env with the given node manager.
66 Env(NodeManager
* nm
, const Options
* opts
);
67 /** Destruct the env. */
70 /* Access to members------------------------------------------------------- */
71 /** Get a pointer to the Context owned by this Env. */
72 context::Context
* getContext();
74 /** Get a pointer to the UserContext owned by this Env. */
75 context::UserContext
* getUserContext();
77 /** Get a pointer to the underlying NodeManager. */
78 NodeManager
* getNodeManager() const;
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.
85 ProofNodeManager
* getProofNodeManager();
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.
92 bool isSatProofProducing() const;
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.
100 bool isTheoryProofProducing() const;
102 /** Get a pointer to the Rewriter owned by this Env. */
103 theory::Rewriter
* getRewriter();
105 /** Get a reference to the top-level substitution map */
106 theory::TrustSubstitutionMap
& getTopLevelSubstitutions();
108 /** Get a pointer to the underlying dump manager. */
109 smt::DumpManager
* getDumpManager();
111 /** Get the options object (const version only) owned by this Env. */
112 const Options
& getOptions() const;
114 /** Get the original options object (const version only). */
115 const Options
& getOriginalOptions() const;
117 /** Get the resource manager owned by this Env. */
118 ResourceManager
* getResourceManager() const;
120 /** Get the logic information currently set. */
121 const LogicInfo
& getLogicInfo() const;
123 /** Get a pointer to the StatisticsRegistry. */
124 StatisticsRegistry
& getStatisticsRegistry();
126 /* Option helpers---------------------------------------------------------- */
129 * Get the current printer based on the current options
130 * @return the current printer
132 const Printer
& getPrinter();
135 * Get the output stream that --dump=X should print to
136 * @return the output stream
138 std::ostream
& getDumpOut();
141 /* Private initialization ------------------------------------------------- */
143 /** Set proof node manager if it exists */
144 void setProofNodeManager(ProofNodeManager
* pnm
);
146 /* Private shutdown ------------------------------------------------------- */
148 * Shutdown method, which destroys the non-essential members of this class
149 * in preparation for destroying SMT engine.
152 /* Members ---------------------------------------------------------------- */
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
;
159 * A pointer to the node manager of this environment. A node manager is
160 * not necessarily unique to an SmtEngine instance.
162 NodeManager
* d_nodeManager
;
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
168 ProofNodeManager
* d_proofNodeManager
;
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.
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
;
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.
185 * This is the authorative copy of the logic that internal subsolvers should
186 * consider during solving and initialization.
190 * The statistics registry owned by this Env.
192 std::unique_ptr
<StatisticsRegistry
> d_statisticsRegistry
;
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.
199 * This is the authorative copy of the options that internal subsolvers should
200 * consider during solving and initialization.
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().
208 const Options
* d_originalOptions
;
209 /** Manager for limiting time and abstract resource usage. */
210 std::unique_ptr
<ResourceManager
> d_resourceManager
;
215 #endif /* CVC5__SMT__ENV_H */