Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Gereon Kremer, Mathias Preiner
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 "smt/env.h"
18 : :
19 : : #include "context/context.h"
20 : : #include "expr/node.h"
21 : : #include "expr/node_algorithm.h"
22 : : #include "expr/skolem_manager.h"
23 : : #include "expr/subtype_elim_node_converter.h"
24 : : #include "options/base_options.h"
25 : : #include "options/printer_options.h"
26 : : #include "options/quantifiers_options.h"
27 : : #include "options/smt_options.h"
28 : : #include "options/strings_options.h"
29 : : #include "printer/printer.h"
30 : : #include "proof/conv_proof_generator.h"
31 : : #include "smt/proof_manager.h"
32 : : #include "smt/solver_engine_stats.h"
33 : : #include "theory/evaluator.h"
34 : : #include "theory/quantifiers/oracle_checker.h"
35 : : #include "theory/rewriter.h"
36 : : #include "theory/theory.h"
37 : : #include "theory/trust_substitutions.h"
38 : : #include "util/resource_manager.h"
39 : : #include "util/statistics_registry.h"
40 : :
41 : : using namespace cvc5::internal::smt;
42 : :
43 : : namespace cvc5::internal {
44 : :
45 : 70493 : Env::Env(NodeManager* nm, const Options* opts)
46 : : : d_nm(nm),
47 : 70493 : d_context(new context::Context()),
48 : 70493 : d_userContext(new context::UserContext()),
49 : : d_pfManager(nullptr),
50 : : d_proofNodeManager(nullptr),
51 : 70493 : d_rewriter(new theory::Rewriter(nm)),
52 : : d_evalRew(nullptr),
53 : : d_eval(nullptr),
54 : : d_topLevelSubs(nullptr),
55 : : d_logic(),
56 : : d_options(),
57 : : d_resourceManager(),
58 : : d_uninterpretedSortOwner(theory::THEORY_UF),
59 : 281972 : d_boolTermSkolems(d_userContext.get())
60 : : {
61 [ + + ]: 70493 : if (opts != nullptr)
62 : : {
63 : 70061 : d_options.copyValues(*opts);
64 : : }
65 : 70493 : d_statisticsRegistry.reset(new StatisticsRegistry(
66 : 70493 : d_options.base.statisticsInternal, d_options.base.statisticsAll));
67 : : // make the evaluators, which depend on the alphabet of strings
68 : 140986 : d_evalRew.reset(new theory::Evaluator(d_rewriter.get(),
69 : 70493 : d_options.strings.stringsAlphaCard));
70 : 70493 : d_eval.reset(
71 : 70493 : new theory::Evaluator(nullptr, d_options.strings.stringsAlphaCard));
72 : 70493 : d_statisticsRegistry->registerTimer("global::totalTime").start();
73 : 70493 : d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
74 : 70493 : d_rewriter->d_resourceManager = d_resourceManager.get();
75 : 70493 : }
76 : :
77 : 66038 : Env::~Env() {}
78 : :
79 : 76648600 : NodeManager* Env::getNodeManager() const { return d_nm; }
80 : :
81 : 49988 : void Env::finishInit(smt::PfManager* pm)
82 : : {
83 [ + + ]: 49988 : if (pm != nullptr)
84 : : {
85 : 19327 : d_pfManager = pm;
86 [ - + ][ - + ]: 19327 : Assert(d_proofNodeManager == nullptr);
[ - - ]
87 : 19327 : d_proofNodeManager = pm->getProofNodeManager();
88 : 19327 : d_rewriter->finishInit(*this);
89 : : }
90 : 99976 : d_topLevelSubs.reset(
91 : 99976 : new theory::TrustSubstitutionMap(*this, d_userContext.get()));
92 : :
93 [ + + ]: 49988 : if (d_options.quantifiers.oracles)
94 : : {
95 : 466 : d_ochecker.reset(new theory::quantifiers::OracleChecker(*this));
96 : : }
97 : 49988 : }
98 : :
99 : 66018 : void Env::shutdown()
100 : : {
101 : 66018 : d_rewriter.reset(nullptr);
102 : : // d_resourceManager must be destroyed before d_statisticsRegistry
103 : 66018 : d_resourceManager.reset(nullptr);
104 : 66018 : }
105 : :
106 : 78200400 : context::Context* Env::getContext() { return d_context.get(); }
107 : :
108 : 7633340 : context::UserContext* Env::getUserContext() { return d_userContext.get(); }
109 : :
110 : 50591 : smt::PfManager* Env::getProofManager() { return d_pfManager; }
111 : :
112 : 97449500 : ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
113 : :
114 : 294065 : bool Env::isSatProofProducing() const
115 : : {
116 : 294065 : return d_proofNodeManager != nullptr
117 [ + + ][ + + ]: 294065 : && d_options.smt.proofMode != options::ProofMode::PP_ONLY;
118 : : }
119 : :
120 : 12660400 : bool Env::isTheoryProofProducing() const
121 : : {
122 : 12660400 : return d_proofNodeManager != nullptr
123 [ + + ][ + + ]: 14636700 : && (d_options.smt.proofMode == options::ProofMode::FULL
124 [ - + ]: 14636700 : || d_options.smt.proofMode == options::ProofMode::FULL_STRICT);
125 : : }
126 : :
127 : 85385300 : theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
128 : :
129 : 49994 : theory::Evaluator* Env::getEvaluator(bool useRewriter)
130 : : {
131 [ - + ]: 49994 : return useRewriter ? d_evalRew.get() : d_eval.get();
132 : : }
133 : :
134 : 860122 : theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
135 : : {
136 : 860122 : return *d_topLevelSubs.get();
137 : : }
138 : :
139 : 465569000 : const LogicInfo& Env::getLogicInfo() const { return d_logic; }
140 : :
141 : 9259770 : StatisticsRegistry& Env::getStatisticsRegistry()
142 : : {
143 : 9259770 : return *d_statisticsRegistry;
144 : : }
145 : :
146 : 360082000 : const Options& Env::getOptions() const { return d_options; }
147 : :
148 : 60745600 : ResourceManager* Env::getResourceManager() const
149 : : {
150 : 60745600 : return d_resourceManager.get();
151 : : }
152 : :
153 : 11196200 : bool Env::isOutputOn(OutputTag tag) const
154 : : {
155 : 11196200 : return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
156 : : }
157 : 698338 : bool Env::isOutputOn(const std::string& tag) const
158 : : {
159 : 698338 : return isOutputOn(options::stringToOutputTag(tag));
160 : : }
161 : 134620 : std::ostream& Env::output(const std::string& tag) const
162 : : {
163 : 134620 : return output(options::stringToOutputTag(tag));
164 : : }
165 : :
166 : 157400 : std::ostream& Env::output(OutputTag tag) const
167 : : {
168 [ + + ]: 157400 : if (isOutputOn(tag))
169 : : {
170 : 134829 : return *d_options.base.out;
171 : : }
172 : 22571 : return cvc5::internal::null_os;
173 : : }
174 : :
175 : 2054950 : bool Env::isVerboseOn(int64_t level) const
176 : : {
177 [ + - ][ + + ]: 2054950 : return !Configuration::isMuzzledBuild() && d_options.base.verbosity >= level;
178 : : }
179 : :
180 : 2054300 : std::ostream& Env::verbose(int64_t level) const
181 : : {
182 [ + + ]: 2054300 : if (isVerboseOn(level))
183 : : {
184 : 350 : return *d_options.base.err;
185 : : }
186 : 2053950 : return cvc5::internal::null_os;
187 : : }
188 : :
189 : 262 : std::ostream& Env::warning() const
190 : : {
191 : 262 : return verbose(0);
192 : : }
193 : :
194 : 742082 : Node Env::evaluate(TNode n,
195 : : const std::vector<Node>& args,
196 : : const std::vector<Node>& vals,
197 : : bool useRewriter) const
198 : : {
199 : 742082 : std::unordered_map<Node, Node> visited;
200 : 1484160 : return evaluate(n, args, vals, visited, useRewriter);
201 : : }
202 : :
203 : 802677 : Node Env::evaluate(TNode n,
204 : : const std::vector<Node>& args,
205 : : const std::vector<Node>& vals,
206 : : const std::unordered_map<Node, Node>& visited,
207 : : bool useRewriter) const
208 : : {
209 [ + + ]: 802677 : if (useRewriter)
210 : : {
211 : 351940 : return d_evalRew->eval(n, args, vals, visited);
212 : : }
213 : 450737 : return d_eval->eval(n, args, vals, visited);
214 : : }
215 : :
216 : 3721020 : Node Env::rewriteViaMethod(TNode n, MethodId idr)
217 : : {
218 [ + + ]: 3721020 : if (idr == MethodId::RW_REWRITE)
219 : : {
220 : 3266620 : return d_rewriter->rewrite(n);
221 : : }
222 [ + + ]: 454403 : if (idr == MethodId::RW_EXT_REWRITE)
223 : : {
224 : 787 : return d_rewriter->extendedRewrite(n);
225 : : }
226 [ + + ]: 453616 : if (idr == MethodId::RW_EXT_REWRITE_AGG)
227 : : {
228 : 634 : return d_rewriter->extendedRewrite(n, true);
229 : : }
230 [ + + ]: 452982 : if (idr == MethodId::RW_REWRITE_EQ_EXT)
231 : : {
232 : 2245 : return d_rewriter->rewriteEqualityExt(n);
233 : : }
234 [ + - ]: 450737 : if (idr == MethodId::RW_EVALUATE)
235 : : {
236 : 450737 : return evaluate(n, {}, {}, false);
237 : : }
238 [ - - ]: 0 : if (idr == MethodId::RW_IDENTITY)
239 : : {
240 : : // does nothing
241 : 0 : return n;
242 : : }
243 : : // unknown rewriter
244 : 0 : Unhandled() << "Env::rewriteViaMethod: no rewriter for " << idr
245 : 0 : << std::endl;
246 : : return n;
247 : : }
248 : :
249 : 15257900 : bool Env::isFiniteType(TypeNode tn) const
250 : : {
251 : 15257900 : return isCardinalityClassFinite(tn.getCardinalityClass(),
252 : 30515800 : d_options.quantifiers.finiteModelFind);
253 : : }
254 : :
255 : 49990 : void Env::setUninterpretedSortOwner(theory::TheoryId theory)
256 : : {
257 : 49990 : d_uninterpretedSortOwner = theory;
258 : 49990 : }
259 : :
260 : 2017400 : theory::TheoryId Env::getUninterpretedSortOwner() const
261 : : {
262 : 2017400 : return d_uninterpretedSortOwner;
263 : : }
264 : :
265 : 8375300 : theory::TheoryId Env::theoryOf(TypeNode typeNode) const
266 : : {
267 : 8375300 : return theory::Theory::theoryOf(typeNode, d_uninterpretedSortOwner);
268 : : }
269 : :
270 : 157321000 : theory::TheoryId Env::theoryOf(TNode node) const
271 : : {
272 : 157321000 : theory::TheoryId tid = theory::Theory::theoryOf(node,
273 : 157321000 : d_options.theory.theoryOfMode,
274 : 157321000 : d_uninterpretedSortOwner);
275 : : // Special case: Boolean term skolems belong to THEORY_UF.
276 [ + + ][ + + ]: 157321000 : if (tid==theory::TheoryId::THEORY_BOOL && isBooleanTermSkolem(node))
[ + + ][ + + ]
[ - - ]
277 : : {
278 : 228714 : return theory::TheoryId::THEORY_UF;
279 : : }
280 : 157092000 : return tid;
281 : : }
282 : :
283 : 212822 : bool Env::hasSepHeap() const { return !d_sepLocType.isNull(); }
284 : :
285 : 16581 : TypeNode Env::getSepLocType() const { return d_sepLocType; }
286 : :
287 : 16581 : TypeNode Env::getSepDataType() const { return d_sepDataType; }
288 : :
289 : 1276 : void Env::declareSepHeap(TypeNode locT, TypeNode dataT)
290 : : {
291 [ - + ][ - + ]: 1276 : Assert(!locT.isNull());
[ - - ]
292 [ - + ][ - + ]: 1276 : Assert(!dataT.isNull());
[ - - ]
293 : : // remember the types we have set
294 : 1276 : d_sepLocType = locT;
295 : 1276 : d_sepDataType = dataT;
296 : 1276 : }
297 : :
298 : 28 : void Env::addPlugin(Plugin* p) { d_plugins.push_back(p); }
299 : 1012860 : const std::vector<Plugin*>& Env::getPlugins() const { return d_plugins; }
300 : :
301 : 11082 : theory::quantifiers::OracleChecker* Env::getOracleChecker() const
302 : : {
303 : 11082 : return d_ochecker.get();
304 : : }
305 : :
306 : 2674 : void Env::registerBooleanTermSkolem(const Node& k)
307 : : {
308 [ - + ][ - + ]: 2674 : Assert(k.isVar());
[ - - ]
309 : 2674 : d_boolTermSkolems.insert(k);
310 : 2674 : }
311 : :
312 : 13838400 : bool Env::isBooleanTermSkolem(const Node& k) const
313 : : {
314 : : // optimization: check whether k is a variable
315 [ + + ]: 13838400 : if (!k.isVar())
316 : : {
317 : 13490800 : return false;
318 : : }
319 : 347630 : return d_boolTermSkolems.find(k) != d_boolTermSkolems.end();
320 : : }
321 : :
322 : 105 : Node Env::getSharableFormula(const Node& n) const
323 : : {
324 : 210 : Node on = n;
325 [ - + ]: 105 : if (!d_options.base.pluginShareSkolems)
326 : : {
327 : : // note we only remove purify skolems if the above option is disabled
328 : 0 : on = SkolemManager::getOriginalForm(n);
329 : : }
330 : 105 : SkolemManager * skm = d_nm->getSkolemManager();
331 : 210 : std::vector<Node> toProcess;
332 : 105 : toProcess.push_back(on);
333 : : // The set of kinds that we never want to share. Any kind that can appear
334 : : // in lemmas but we don't have API support for should go in this list.
335 : : const std::unordered_set<Kind> excludeKinds = {
336 : : Kind::INST_CONSTANT,
337 : : Kind::DUMMY_SKOLEM,
338 : : Kind::CARDINALITY_CONSTRAINT,
339 : 210 : Kind::COMBINED_CARDINALITY_CONSTRAINT};
340 : 105 : size_t index = 0;
341 : 50 : do
342 : : {
343 : 155 : Node nn = toProcess[index];
344 : 155 : index++;
345 : : // get the symbols contained in nn
346 : 155 : std::unordered_set<Node> syms;
347 : 155 : expr::getSymbols(nn, syms);
348 [ + + ]: 298 : for (const Node& s : syms)
349 : : {
350 : 143 : Kind sk = s.getKind();
351 [ - + ]: 143 : if (excludeKinds.find(sk) != excludeKinds.end())
352 : : {
353 : : // these kinds are never sharable
354 : 0 : return Node::null();
355 : : }
356 [ + + ]: 143 : if (sk == Kind::SKOLEM)
357 : : {
358 [ - + ]: 50 : if (!d_options.base.pluginShareSkolems)
359 : : {
360 : : // not shared if option is false
361 : 0 : return Node::null();
362 : : }
363 : : // must ensure that the indices of the skolem are also legal
364 : : SkolemId id;
365 : 50 : Node cacheVal;
366 [ - + ]: 50 : if (!skm->isSkolemFunction(s, id, cacheVal))
367 : : {
368 : : // kind SKOLEM should imply that it is a skolem function
369 : 0 : Assert(false);
370 : : return Node::null();
371 : : }
372 : 50 : if (!cacheVal.isNull()
373 [ + - ][ + - ]: 150 : && std::find(toProcess.begin(), toProcess.end(), cacheVal)
374 [ + - ]: 150 : == toProcess.end())
375 : : {
376 : : // if we have a cache value, add it to process vector
377 : 50 : toProcess.push_back(cacheVal);
378 : : }
379 : : }
380 : : }
381 [ + + ]: 155 : } while (index < toProcess.size());
382 : : // If we didn't encounter an illegal term, we now eliminate subtyping
383 : 210 : SubtypeElimNodeConverter senc(d_nm);
384 : 105 : on = senc.convert(on);
385 : 105 : return on;
386 : : }
387 : :
388 : : } // namespace cvc5::internal
|
