e3a34cf4ab2585422f7cbbb6d3f0f7facf2bdec9
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/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"
33 class StatisticsRegistry
;
34 class ProofNodeManager
;
36 class ResourceManager
;
41 } // namespace context
51 class TrustSubstitutionMap
;
55 * The environment class.
57 * This class lives in the SolverEngine and contains all utilities that are
58 * globally available to all internal code.
62 friend class SolverEngine
;
63 friend class smt::PfManager
;
67 * Construct an Env with the given node manager.
69 Env(NodeManager
* nm
, const Options
* opts
);
70 /** Destruct the env. */
73 /* Access to members------------------------------------------------------- */
74 /** Get a pointer to the Context owned by this Env. */
75 context::Context
* getContext();
77 /** Get a pointer to the UserContext owned by this Env. */
78 context::UserContext
* getUserContext();
80 /** Get a pointer to the underlying NodeManager. */
81 NodeManager
* getNodeManager() const;
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.
88 ProofNodeManager
* getProofNodeManager();
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.
95 bool isSatProofProducing() const;
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.
103 bool isTheoryProofProducing() const;
105 /** Get a pointer to the Rewriter owned by this Env. */
106 theory::Rewriter
* getRewriter();
108 /** Get a reference to the top-level substitution map */
109 theory::TrustSubstitutionMap
& getTopLevelSubstitutions();
111 /** Get a pointer to the underlying dump manager. */
112 smt::DumpManager
* getDumpManager();
114 /** Get the options object (const version only) owned by this Env. */
115 const Options
& getOptions() const;
117 /** Get the original options object (const version only). */
118 const Options
& getOriginalOptions() const;
120 /** Get the resource manager owned by this Env. */
121 ResourceManager
* getResourceManager() const;
123 /** Get the logic information currently set. */
124 const LogicInfo
& getLogicInfo() const;
126 /** Get a pointer to the StatisticsRegistry. */
127 StatisticsRegistry
& getStatisticsRegistry();
129 /* Option helpers---------------------------------------------------------- */
132 * Get the current printer based on the current options
133 * @return the current printer
135 const Printer
& getPrinter();
138 * Get the output stream that --dump=X should print to
139 * @return the output stream
141 std::ostream
& getDumpOut();
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).
147 bool isOutputOn(options::OutputTag tag
) const;
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
153 bool isOutputOn(const std::string
& tag
) const;
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.
159 std::ostream
& getOutput(options::OutputTag tag
) const;
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.
165 std::ostream
& getOutput(const std::string
& tag
) const;
167 /* Rewrite helpers--------------------------------------------------------- */
169 * Evaluate node n under the substitution args -> vals. For details, see
170 * theory/evaluator.h.
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.
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;
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.
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.
198 Node
rewriteViaMethod(TNode n
, MethodId idr
= MethodId::RW_REWRITE
);
201 /* Private initialization ------------------------------------------------- */
203 /** Set proof node manager if it exists */
204 void setProofNodeManager(ProofNodeManager
* pnm
);
206 /* Private shutdown ------------------------------------------------------- */
208 * Shutdown method, which destroys the non-essential members of this class
209 * in preparation for destroying SMT engine.
212 /* Members ---------------------------------------------------------------- */
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
;
219 * A pointer to the node manager of this environment. A node manager is
220 * not necessarily unique to an SolverEngine instance.
222 NodeManager
* d_nodeManager
;
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
228 ProofNodeManager
* d_proofNodeManager
;
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.
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
;
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.
249 * This is the authorative copy of the logic that internal subsolvers should
250 * consider during solving and initialization.
254 * The statistics registry owned by this Env.
256 std::unique_ptr
<StatisticsRegistry
> d_statisticsRegistry
;
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.
263 * This is the authorative copy of the options that internal subsolvers should
264 * consider during solving and initialization.
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().
272 const Options
* d_originalOptions
;
273 /** Manager for limiting time and abstract resource usage. */
274 std::unique_ptr
<ResourceManager
> d_resourceManager
;
279 #endif /* CVC5__SMT__ENV_H */