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-2025 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 : 74499 : Env::Env(NodeManager* nm, const Options* opts)
46 : : : d_nm(nm),
47 : 74499 : d_context(new context::Context()),
48 : 74499 : d_userContext(new context::UserContext()),
49 : : d_pfManager(nullptr),
50 : : d_proofNodeManager(nullptr),
51 : 74499 : 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 : 297996 : d_boolTermSkolems(d_userContext.get())
60 : : {
61 [ + + ]: 74499 : if (opts != nullptr)
62 : : {
63 : 74066 : d_options.copyValues(*opts);
64 : : }
65 : 74499 : d_statisticsRegistry.reset(new StatisticsRegistry(
66 : 74499 : d_options.base.statisticsInternal, d_options.base.statisticsAll));
67 : : // make the evaluators, which depend on the alphabet of strings
68 : 148998 : d_evalRew.reset(new theory::Evaluator(d_rewriter.get(),
69 : 74499 : d_options.strings.stringsAlphaCard));
70 : 74499 : d_eval.reset(
71 : 74499 : new theory::Evaluator(nullptr, d_options.strings.stringsAlphaCard));
72 : 74499 : d_statisticsRegistry->registerTimer("global::totalTime").start();
73 : 74499 : d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
74 : 74499 : d_rewriter->d_resourceManager = d_resourceManager.get();
75 : 74499 : }
76 : :
77 : 69525 : Env::~Env() {}
78 : :
79 : 102683000 : NodeManager* Env::getNodeManager() const { return d_nm; }
80 : :
81 : 49893 : void Env::finishInit(smt::PfManager* pm)
82 : : {
83 [ + + ]: 49893 : if (pm != nullptr)
84 : : {
85 : 18860 : d_pfManager = pm;
86 [ - + ][ - + ]: 18860 : Assert(d_proofNodeManager == nullptr);
[ - - ]
87 : 18860 : d_proofNodeManager = pm->getProofNodeManager();
88 : 18860 : d_rewriter->finishInit(*this);
89 : : }
90 : 99786 : d_topLevelSubs.reset(
91 : 99786 : new theory::TrustSubstitutionMap(*this, d_userContext.get()));
92 : :
93 [ + + ]: 49893 : if (d_options.quantifiers.oracles)
94 : : {
95 : 535 : d_ochecker.reset(new theory::quantifiers::OracleChecker(*this));
96 : : }
97 : 49893 : d_statisticsRegistry->setStatsAll(d_options.base.statisticsAll);
98 : 49893 : d_statisticsRegistry->setStatsInternal(d_options.base.statisticsInternal);
99 : 49893 : }
100 : :
101 : 69505 : void Env::shutdown()
102 : : {
103 : 69505 : d_rewriter.reset(nullptr);
104 : : // d_resourceManager must be destroyed before d_statisticsRegistry
105 : 69505 : d_resourceManager.reset(nullptr);
106 : 69505 : }
107 : :
108 : 54064000 : context::Context* Env::getContext() { return d_context.get(); }
109 : :
110 : 8024080 : context::UserContext* Env::getUserContext() { return d_userContext.get(); }
111 : :
112 : 50586 : smt::PfManager* Env::getProofManager() { return d_pfManager; }
113 : :
114 : 25800 : ProofLogger* Env::getProofLogger()
115 : : {
116 [ + - ]: 25800 : return d_pfManager ? d_pfManager->getProofLogger() : nullptr;
117 : : }
118 : :
119 : 88273800 : ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
120 : :
121 : 193139 : bool Env::isProofProducing() const { return d_proofNodeManager != nullptr; }
122 : :
123 : 951487 : bool Env::isSatProofProducing() const
124 : : {
125 : 951487 : return d_proofNodeManager != nullptr
126 [ + + ][ + + ]: 951487 : && d_options.smt.proofMode != options::ProofMode::PP_ONLY;
127 : : }
128 : :
129 : 14569700 : bool Env::isTheoryProofProducing() const
130 : : {
131 : 14569700 : return d_proofNodeManager != nullptr
132 [ + + ][ + + ]: 16730100 : && (d_options.smt.proofMode == options::ProofMode::FULL
133 [ - + ]: 16730100 : || d_options.smt.proofMode == options::ProofMode::FULL_STRICT);
134 : : }
135 : :
136 : 88421300 : theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
137 : :
138 : 49899 : theory::Evaluator* Env::getEvaluator(bool useRewriter)
139 : : {
140 [ - + ]: 49899 : return useRewriter ? d_evalRew.get() : d_eval.get();
141 : : }
142 : :
143 : 844879 : theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
144 : : {
145 : 844879 : return *d_topLevelSubs.get();
146 : : }
147 : :
148 : 347209000 : const LogicInfo& Env::getLogicInfo() const { return d_logic; }
149 : :
150 : 9448740 : StatisticsRegistry& Env::getStatisticsRegistry()
151 : : {
152 : 9448740 : return *d_statisticsRegistry;
153 : : }
154 : :
155 : 338651000 : const Options& Env::getOptions() const { return d_options; }
156 : :
157 : 42101600 : ResourceManager* Env::getResourceManager() const
158 : : {
159 : 42101600 : return d_resourceManager.get();
160 : : }
161 : :
162 : 5091400 : bool Env::isOutputOn(OutputTag tag) const
163 : : {
164 : 5091400 : return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
165 : : }
166 : 672317 : bool Env::isOutputOn(const std::string& tag) const
167 : : {
168 : 672317 : return isOutputOn(options::stringToOutputTag(tag));
169 : : }
170 : 137792 : std::ostream& Env::output(const std::string& tag) const
171 : : {
172 : 137792 : return output(options::stringToOutputTag(tag));
173 : : }
174 : :
175 : 159161 : std::ostream& Env::output(OutputTag tag) const
176 : : {
177 [ + + ]: 159161 : if (isOutputOn(tag))
178 : : {
179 : 137995 : return *d_options.base.out;
180 : : }
181 : 21166 : return cvc5::internal::null_os;
182 : : }
183 : :
184 : 1941820 : bool Env::isVerboseOn(int64_t level) const
185 : : {
186 [ + - ][ + + ]: 1941820 : return !Configuration::isMuzzledBuild() && d_options.base.verbosity >= level;
187 : : }
188 : :
189 : 1941160 : std::ostream& Env::verbose(int64_t level) const
190 : : {
191 [ + + ]: 1941160 : if (isVerboseOn(level))
192 : : {
193 : 399 : return *d_options.base.err;
194 : : }
195 : 1940760 : return cvc5::internal::null_os;
196 : : }
197 : :
198 : 310 : std::ostream& Env::warning() const
199 : : {
200 : 310 : return verbose(0);
201 : : }
202 : :
203 : 1366790 : Node Env::evaluate(TNode n,
204 : : const std::vector<Node>& args,
205 : : const std::vector<Node>& vals,
206 : : bool useRewriter) const
207 : : {
208 : 1366790 : std::unordered_map<Node, Node> visited;
209 : 2733580 : return evaluate(n, args, vals, visited, useRewriter);
210 : : }
211 : :
212 : 1427620 : Node Env::evaluate(TNode n,
213 : : const std::vector<Node>& args,
214 : : const std::vector<Node>& vals,
215 : : const std::unordered_map<Node, Node>& visited,
216 : : bool useRewriter) const
217 : : {
218 [ + + ]: 1427620 : if (useRewriter)
219 : : {
220 : 896184 : return d_evalRew->eval(n, args, vals, visited);
221 : : }
222 : 531440 : return d_eval->eval(n, args, vals, visited);
223 : : }
224 : :
225 : 1972030 : Node Env::rewriteViaMethod(TNode n, MethodId idr)
226 : : {
227 [ + + ]: 1972030 : if (idr == MethodId::RW_REWRITE)
228 : : {
229 : 1432770 : return d_rewriter->rewrite(n);
230 : : }
231 [ + + ]: 539263 : if (idr == MethodId::RW_EXT_REWRITE)
232 : : {
233 : 9616 : return d_rewriter->extendedRewrite(n, false);
234 : : }
235 [ + + ]: 529647 : if (idr == MethodId::RW_EXT_REWRITE_AGG)
236 : : {
237 : 567 : return d_rewriter->extendedRewrite(n, true);
238 : : }
239 [ + + ]: 529080 : if (idr == MethodId::RW_REWRITE_EQ_EXT)
240 : : {
241 : 2628 : return d_rewriter->rewriteEqualityExt(n);
242 : : }
243 [ + - ]: 526452 : if (idr == MethodId::RW_EVALUATE)
244 : : {
245 : 526452 : return evaluate(n, {}, {}, false);
246 : : }
247 [ - - ]: 0 : if (idr == MethodId::RW_IDENTITY)
248 : : {
249 : : // does nothing
250 : 0 : return n;
251 : : }
252 : : // unknown rewriter
253 : 0 : Unhandled() << "Env::rewriteViaMethod: no rewriter for " << idr
254 : 0 : << std::endl;
255 : : return n;
256 : : }
257 : :
258 : 16993500 : bool Env::isFiniteType(TypeNode tn) const
259 : : {
260 : 16993500 : return isCardinalityClassFinite(tn.getCardinalityClass(),
261 : 33987000 : d_options.quantifiers.finiteModelFind);
262 : : }
263 : :
264 : 277913 : bool Env::isFiniteCardinalityClass(CardinalityClass cc) const
265 : : {
266 : 277913 : return isCardinalityClassFinite(cc, d_options.quantifiers.finiteModelFind);
267 : : }
268 : :
269 : 231943 : bool Env::isFirstClassType(TypeNode tn) const
270 : : {
271 [ + + ]: 231943 : if (tn.isRegExp())
272 : : {
273 : 8 : return d_options.strings.regExpFirstClass;
274 : : }
275 : 231935 : return tn.isFirstClass();
276 : : }
277 : :
278 : 49895 : void Env::setUninterpretedSortOwner(theory::TheoryId theory)
279 : : {
280 : 49895 : d_uninterpretedSortOwner = theory;
281 : 49895 : }
282 : :
283 : 1995890 : theory::TheoryId Env::getUninterpretedSortOwner() const
284 : : {
285 : 1995890 : return d_uninterpretedSortOwner;
286 : : }
287 : :
288 : 8209430 : theory::TheoryId Env::theoryOf(TypeNode typeNode) const
289 : : {
290 : 8209430 : return theory::Theory::theoryOf(typeNode, d_uninterpretedSortOwner);
291 : : }
292 : :
293 : 142540000 : theory::TheoryId Env::theoryOf(TNode node) const
294 : : {
295 : 142540000 : theory::TheoryId tid = theory::Theory::theoryOf(node,
296 : 142540000 : d_options.theory.theoryOfMode,
297 : 142540000 : d_uninterpretedSortOwner);
298 : : // Special case: Boolean term skolems belong to THEORY_UF.
299 [ + + ][ + + ]: 142540000 : if (tid==theory::TheoryId::THEORY_BOOL && isBooleanTermSkolem(node))
[ + + ][ + + ]
[ - - ]
300 : : {
301 : 222798 : return theory::TheoryId::THEORY_UF;
302 : : }
303 : 142318000 : return tid;
304 : : }
305 : :
306 : 210108 : bool Env::hasSepHeap() const { return !d_sepLocType.isNull(); }
307 : :
308 : 15409 : TypeNode Env::getSepLocType() const { return d_sepLocType; }
309 : :
310 : 15409 : TypeNode Env::getSepDataType() const { return d_sepDataType; }
311 : :
312 : 1069 : void Env::declareSepHeap(TypeNode locT, TypeNode dataT)
313 : : {
314 [ - + ][ - + ]: 1069 : Assert(!locT.isNull());
[ - - ]
315 [ - + ][ - + ]: 1069 : Assert(!dataT.isNull());
[ - - ]
316 : : // remember the types we have set
317 : 1069 : d_sepLocType = locT;
318 : 1069 : d_sepDataType = dataT;
319 : 1069 : }
320 : :
321 : 28 : void Env::addPlugin(Plugin* p) { d_plugins.push_back(p); }
322 : 905813 : const std::vector<Plugin*>& Env::getPlugins() const { return d_plugins; }
323 : :
324 : 10268 : theory::quantifiers::OracleChecker* Env::getOracleChecker() const
325 : : {
326 : 10268 : return d_ochecker.get();
327 : : }
328 : :
329 : 3521 : void Env::registerBooleanTermSkolem(const Node& k)
330 : : {
331 [ - + ][ - + ]: 3521 : Assert(k.isVar());
[ - - ]
332 : 3521 : d_boolTermSkolems.insert(k);
333 : 3521 : }
334 : :
335 : 13831600 : bool Env::isBooleanTermSkolem(const Node& k) const
336 : : {
337 : : // optimization: check whether k is a variable
338 [ + + ]: 13831600 : if (!k.isVar())
339 : : {
340 : 13495500 : return false;
341 : : }
342 : 336155 : return d_boolTermSkolems.find(k) != d_boolTermSkolems.end();
343 : : }
344 : :
345 : 105 : Node Env::getSharableFormula(const Node& n) const
346 : : {
347 : 210 : Node on = n;
348 [ - + ]: 105 : if (!d_options.base.pluginShareSkolems)
349 : : {
350 : : // note we only remove purify skolems if the above option is disabled
351 : 0 : on = SkolemManager::getOriginalForm(n);
352 : : }
353 : 105 : SkolemManager * skm = d_nm->getSkolemManager();
354 : 210 : std::vector<Node> toProcess;
355 : 105 : toProcess.push_back(on);
356 : : // The set of kinds that we never want to share. Any kind that can appear
357 : : // in lemmas but we don't have API support for should go in this list.
358 : : const std::unordered_set<Kind> excludeKinds = {
359 : : Kind::INST_CONSTANT,
360 : : Kind::DUMMY_SKOLEM,
361 : : Kind::CARDINALITY_CONSTRAINT,
362 : 210 : Kind::COMBINED_CARDINALITY_CONSTRAINT};
363 : 105 : size_t index = 0;
364 : 50 : do
365 : : {
366 : 155 : Node nn = toProcess[index];
367 : 155 : index++;
368 : : // get the symbols contained in nn
369 : 155 : std::unordered_set<Node> syms;
370 : 155 : expr::getSymbols(nn, syms);
371 [ + + ]: 298 : for (const Node& s : syms)
372 : : {
373 : 143 : Kind sk = s.getKind();
374 [ - + ]: 143 : if (excludeKinds.find(sk) != excludeKinds.end())
375 : : {
376 : : // these kinds are never sharable
377 : 0 : return Node::null();
378 : : }
379 [ + + ]: 143 : if (sk == Kind::SKOLEM)
380 : : {
381 [ - + ]: 50 : if (!d_options.base.pluginShareSkolems)
382 : : {
383 : : // not shared if option is false
384 : 0 : return Node::null();
385 : : }
386 : : // must ensure that the indices of the skolem are also legal
387 : : SkolemId id;
388 : 50 : Node cacheVal;
389 [ - + ]: 50 : if (!skm->isSkolemFunction(s, id, cacheVal))
390 : : {
391 : : // kind SKOLEM should imply that it is a skolem function
392 : 0 : DebugUnhandled();
393 : : return Node::null();
394 : : }
395 : 50 : if (!cacheVal.isNull()
396 [ + - ][ + - ]: 150 : && std::find(toProcess.begin(), toProcess.end(), cacheVal)
397 [ + - ]: 150 : == toProcess.end())
398 : : {
399 : : // if we have a cache value, add it to process vector
400 : 50 : toProcess.push_back(cacheVal);
401 : : }
402 : : }
403 : : }
404 [ + + ]: 155 : } while (index < toProcess.size());
405 : : // If we didn't encounter an illegal term, we now eliminate subtyping
406 : 210 : SubtypeElimNodeConverter senc(d_nm);
407 : 105 : on = senc.convert(on);
408 : 105 : return on;
409 : : }
410 : :
411 : : } // namespace cvc5::internal
|
