Branch data Line data Source code
1 : : /******************************************************************************
2 : : * This file is part of the cvc5 project.
3 : : *
4 : : * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
5 : : * in the top-level source directory and their institutional affiliations.
6 : : * All rights reserved. See the file COPYING in the top-level source
7 : : * directory for licensing information.
8 : : * ****************************************************************************
9 : : *
10 : : * Smt Environment, main access to global utilities available to
11 : : * internal code.
12 : : */
13 : :
14 : : #include "smt/env.h"
15 : :
16 : : #include "context/context.h"
17 : : #include "expr/node.h"
18 : : #include "expr/node_algorithm.h"
19 : : #include "expr/skolem_manager.h"
20 : : #include "expr/subtype_elim_node_converter.h"
21 : : #include "options/base_options.h"
22 : : #include "options/printer_options.h"
23 : : #include "options/quantifiers_options.h"
24 : : #include "options/smt_options.h"
25 : : #include "options/strings_options.h"
26 : : #include "printer/printer.h"
27 : : #include "proof/conv_proof_generator.h"
28 : : #include "smt/proof_manager.h"
29 : : #include "smt/solver_engine_stats.h"
30 : : #include "theory/evaluator.h"
31 : : #include "theory/quantifiers/oracle_checker.h"
32 : : #include "theory/rewriter.h"
33 : : #include "theory/theory.h"
34 : : #include "theory/trust_substitutions.h"
35 : : #include "util/resource_manager.h"
36 : : #include "util/statistics_registry.h"
37 : :
38 : : using namespace cvc5::internal::smt;
39 : :
40 : : namespace cvc5::internal {
41 : :
42 : 75684 : Env::Env(NodeManager* nm, const Options* opts)
43 : 75684 : : d_nm(nm),
44 : 75684 : d_context(new context::Context()),
45 : 75684 : d_userContext(new context::UserContext()),
46 : 75684 : d_pfManager(nullptr),
47 : 75684 : d_proofNodeManager(nullptr),
48 : 75684 : d_rewriter(new theory::Rewriter(nm)),
49 : 75684 : d_evalRew(nullptr),
50 : 75684 : d_eval(nullptr),
51 : 75684 : d_topLevelSubs(nullptr),
52 : 75684 : d_logic(),
53 : 75684 : d_options(),
54 : 75684 : d_resourceManager(),
55 : 75684 : d_uninterpretedSortOwner(theory::THEORY_UF),
56 : 151368 : d_boolTermSkolems(d_userContext.get())
57 : : {
58 [ + + ]: 75684 : if (opts != nullptr)
59 : : {
60 : 75251 : d_options.copyValues(*opts);
61 : : }
62 : 75684 : d_statisticsRegistry.reset(new StatisticsRegistry(
63 : 75684 : d_options.base.statisticsInternal, d_options.base.statisticsAll));
64 : : // make the evaluators, which depend on the alphabet of strings
65 : 151368 : d_evalRew.reset(new theory::Evaluator(d_rewriter.get(),
66 : 75684 : d_options.strings.stringsAlphaCard));
67 : 75684 : d_eval.reset(
68 : 75684 : new theory::Evaluator(nullptr, d_options.strings.stringsAlphaCard));
69 : 75684 : d_statisticsRegistry->registerTimer("global::totalTime").start();
70 : : d_resourceManager =
71 : 75684 : std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options);
72 : 75684 : d_rewriter->d_resourceManager = d_resourceManager.get();
73 : 75684 : }
74 : :
75 : 70656 : Env::~Env() {}
76 : :
77 : 104009843 : NodeManager* Env::getNodeManager() const { return d_nm; }
78 : :
79 : 50931 : void Env::finishInit(smt::PfManager* pm)
80 : : {
81 [ + + ]: 50931 : if (pm != nullptr)
82 : : {
83 : 19687 : d_pfManager = pm;
84 [ - + ][ - + ]: 19687 : Assert(d_proofNodeManager == nullptr);
[ - - ]
85 : 19687 : d_proofNodeManager = pm->getProofNodeManager();
86 : 19687 : d_rewriter->finishInit(*this);
87 : : }
88 : 101862 : d_topLevelSubs.reset(
89 : 101862 : new theory::TrustSubstitutionMap(*this, d_userContext.get()));
90 : :
91 [ + + ]: 50931 : if (d_options.quantifiers.oracles)
92 : : {
93 : 535 : d_ochecker.reset(new theory::quantifiers::OracleChecker(*this));
94 : : }
95 : 50931 : d_statisticsRegistry->setStatsAll(d_options.base.statisticsAll);
96 : 50931 : d_statisticsRegistry->setStatsInternal(d_options.base.statisticsInternal);
97 : 50931 : }
98 : :
99 : 70636 : void Env::shutdown()
100 : : {
101 : 70636 : d_rewriter.reset(nullptr);
102 : : // d_resourceManager must be destroyed before d_statisticsRegistry
103 : 70636 : d_resourceManager.reset(nullptr);
104 : 70636 : }
105 : :
106 : 54522336 : context::Context* Env::getContext() { return d_context.get(); }
107 : :
108 : 8211810 : context::UserContext* Env::getUserContext() { return d_userContext.get(); }
109 : :
110 : 51624 : smt::PfManager* Env::getProofManager() { return d_pfManager; }
111 : :
112 : 26633 : ProofLogger* Env::getProofLogger()
113 : : {
114 [ + - ]: 26633 : return d_pfManager ? d_pfManager->getProofLogger() : nullptr;
115 : : }
116 : :
117 : 88161284 : ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; }
118 : :
119 : 194284 : bool Env::isProofProducing() const { return d_proofNodeManager != nullptr; }
120 : :
121 : 970727 : bool Env::isSatProofProducing() const
122 : : {
123 : 970727 : return d_proofNodeManager != nullptr
124 [ + + ][ + + ]: 970727 : && d_options.smt.proofMode != options::ProofMode::PP_ONLY;
125 : : }
126 : :
127 : 14903394 : bool Env::isTheoryProofProducing() const
128 : : {
129 : 14903394 : return d_proofNodeManager != nullptr
130 [ + + ][ + + ]: 17114900 : && (d_options.smt.proofMode == options::ProofMode::FULL
131 [ - + ]: 17114900 : || d_options.smt.proofMode == options::ProofMode::FULL_STRICT);
132 : : }
133 : :
134 : 89947678 : theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); }
135 : :
136 : 50937 : theory::Evaluator* Env::getEvaluator(bool useRewriter)
137 : : {
138 [ - + ]: 50937 : return useRewriter ? d_evalRew.get() : d_eval.get();
139 : : }
140 : :
141 : 869100 : theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions()
142 : : {
143 : 869100 : return *d_topLevelSubs.get();
144 : : }
145 : :
146 : 359670084 : const LogicInfo& Env::getLogicInfo() const { return d_logic; }
147 : :
148 : 9652017 : StatisticsRegistry& Env::getStatisticsRegistry()
149 : : {
150 : 9652017 : return *d_statisticsRegistry;
151 : : }
152 : :
153 : 348567756 : const Options& Env::getOptions() const { return d_options; }
154 : :
155 : 43331844 : ResourceManager* Env::getResourceManager() const
156 : : {
157 : 43331844 : return d_resourceManager.get();
158 : : }
159 : :
160 : 5170067 : bool Env::isOutputOn(OutputTag tag) const
161 : : {
162 : 5170067 : return d_options.base.outputTagHolder[static_cast<size_t>(tag)];
163 : : }
164 : 674244 : bool Env::isOutputOn(const std::string& tag) const
165 : : {
166 : 674244 : return isOutputOn(options::stringToOutputTag(tag));
167 : : }
168 : 138070 : std::ostream& Env::output(const std::string& tag) const
169 : : {
170 : 138070 : return output(options::stringToOutputTag(tag));
171 : : }
172 : :
173 : 159630 : std::ostream& Env::output(OutputTag tag) const
174 : : {
175 [ + + ]: 159630 : if (isOutputOn(tag))
176 : : {
177 : 138281 : return *d_options.base.out;
178 : : }
179 : 21349 : return cvc5::internal::null_os;
180 : : }
181 : :
182 : 1973706 : bool Env::isVerboseOn(int64_t level) const
183 : : {
184 [ + - ][ + + ]: 1973706 : return !Configuration::isMuzzledBuild() && d_options.base.verbosity >= level;
185 : : }
186 : :
187 : 1973049 : std::ostream& Env::verbose(int64_t level) const
188 : : {
189 [ + + ]: 1973049 : if (isVerboseOn(level))
190 : : {
191 : 399 : return *d_options.base.err;
192 : : }
193 : 1972650 : return cvc5::internal::null_os;
194 : : }
195 : :
196 : 310 : std::ostream& Env::warning() const { return verbose(0); }
197 : :
198 : 1377518 : Node Env::evaluate(TNode n,
199 : : const std::vector<Node>& args,
200 : : const std::vector<Node>& vals,
201 : : bool useRewriter) const
202 : : {
203 : 1377518 : std::unordered_map<Node, Node> visited;
204 : 2755036 : return evaluate(n, args, vals, visited, useRewriter);
205 : 1377518 : }
206 : :
207 : 1438353 : Node Env::evaluate(TNode n,
208 : : const std::vector<Node>& args,
209 : : const std::vector<Node>& vals,
210 : : const std::unordered_map<Node, Node>& visited,
211 : : bool useRewriter) const
212 : : {
213 [ + + ]: 1438353 : if (useRewriter)
214 : : {
215 : 895891 : return d_evalRew->eval(n, args, vals, visited);
216 : : }
217 : 542462 : return d_eval->eval(n, args, vals, visited);
218 : : }
219 : :
220 : 2034780 : Node Env::rewriteViaMethod(TNode n, MethodId idr)
221 : : {
222 [ + + ]: 2034780 : if (idr == MethodId::RW_REWRITE)
223 : : {
224 : 1482969 : return d_rewriter->rewrite(n);
225 : : }
226 [ + + ]: 551811 : if (idr == MethodId::RW_EXT_REWRITE)
227 : : {
228 : 10752 : return d_rewriter->extendedRewrite(n, false);
229 : : }
230 [ + + ]: 541059 : if (idr == MethodId::RW_EXT_REWRITE_AGG)
231 : : {
232 : 567 : return d_rewriter->extendedRewrite(n, true);
233 : : }
234 [ + + ]: 540492 : if (idr == MethodId::RW_REWRITE_EQ_EXT)
235 : : {
236 : 3034 : return d_rewriter->rewriteEqualityExt(n);
237 : : }
238 [ + - ]: 537458 : if (idr == MethodId::RW_EVALUATE)
239 : : {
240 : 537458 : return evaluate(n, {}, {}, false);
241 : : }
242 [ - - ]: 0 : if (idr == MethodId::RW_IDENTITY)
243 : : {
244 : : // does nothing
245 : 0 : return n;
246 : : }
247 : : // unknown rewriter
248 : 0 : Unhandled() << "Env::rewriteViaMethod: no rewriter for " << idr << std::endl;
249 : : return n;
250 : : }
251 : :
252 : 17082335 : bool Env::isFiniteType(TypeNode tn) const
253 : : {
254 : 17082335 : return isCardinalityClassFinite(tn.getCardinalityClass(),
255 : 34164670 : d_options.quantifiers.finiteModelFind);
256 : : }
257 : :
258 : 261293 : bool Env::isFiniteCardinalityClass(CardinalityClass cc) const
259 : : {
260 : 261293 : return isCardinalityClassFinite(cc, d_options.quantifiers.finiteModelFind);
261 : : }
262 : :
263 : 240124 : bool Env::isFirstClassType(TypeNode tn) const
264 : : {
265 [ + + ]: 240124 : if (tn.isRegExp())
266 : : {
267 : 8 : return d_options.strings.regExpFirstClass;
268 : : }
269 : 240116 : return tn.isFirstClass();
270 : : }
271 : :
272 : 50933 : void Env::setUninterpretedSortOwner(theory::TheoryId theory)
273 : : {
274 : 50933 : d_uninterpretedSortOwner = theory;
275 : 50933 : }
276 : :
277 : 1984904 : theory::TheoryId Env::getUninterpretedSortOwner() const
278 : : {
279 : 1984904 : return d_uninterpretedSortOwner;
280 : : }
281 : :
282 : 8146518 : theory::TheoryId Env::theoryOf(TypeNode typeNode) const
283 : : {
284 : 8146518 : return theory::Theory::theoryOf(typeNode, d_uninterpretedSortOwner);
285 : : }
286 : :
287 : 145374535 : theory::TheoryId Env::theoryOf(TNode node) const
288 : : {
289 : 145374535 : theory::TheoryId tid = theory::Theory::theoryOf(
290 : 145374535 : node, d_options.theory.theoryOfMode, d_uninterpretedSortOwner);
291 : : // Special case: Boolean term skolems belong to THEORY_UF.
292 [ + + ][ + + ]: 145374535 : if (tid == theory::TheoryId::THEORY_BOOL && isBooleanTermSkolem(node))
[ + + ][ + + ]
[ - - ]
293 : : {
294 : 219394 : return theory::TheoryId::THEORY_UF;
295 : : }
296 : 145155141 : return tid;
297 : : }
298 : :
299 : 214648 : bool Env::hasSepHeap() const { return !d_sepLocType.isNull(); }
300 : :
301 : 16054 : TypeNode Env::getSepLocType() const { return d_sepLocType; }
302 : :
303 : 16054 : TypeNode Env::getSepDataType() const { return d_sepDataType; }
304 : :
305 : 1069 : void Env::declareSepHeap(TypeNode locT, TypeNode dataT)
306 : : {
307 [ - + ][ - + ]: 1069 : Assert(!locT.isNull());
[ - - ]
308 [ - + ][ - + ]: 1069 : Assert(!dataT.isNull());
[ - - ]
309 : : // remember the types we have set
310 : 1069 : d_sepLocType = locT;
311 : 1069 : d_sepDataType = dataT;
312 : 1069 : }
313 : :
314 : 28 : void Env::addPlugin(Plugin* p) { d_plugins.push_back(p); }
315 : 910861 : const std::vector<Plugin*>& Env::getPlugins() const { return d_plugins; }
316 : :
317 : 10291 : theory::quantifiers::OracleChecker* Env::getOracleChecker() const
318 : : {
319 : 10291 : return d_ochecker.get();
320 : : }
321 : :
322 : 3482 : void Env::registerBooleanTermSkolem(const Node& k)
323 : : {
324 [ - + ][ - + ]: 3482 : Assert(k.isVar());
[ - - ]
325 : 3482 : d_boolTermSkolems.insert(k);
326 : 3482 : }
327 : :
328 : 14171825 : bool Env::isBooleanTermSkolem(const Node& k) const
329 : : {
330 : : // optimization: check whether k is a variable
331 [ + + ]: 14171825 : if (!k.isVar())
332 : : {
333 : 13839020 : return false;
334 : : }
335 : 332805 : return d_boolTermSkolems.find(k) != d_boolTermSkolems.end();
336 : : }
337 : :
338 : 105 : Node Env::getSharableFormula(const Node& n) const
339 : : {
340 : 105 : Node on = n;
341 [ - + ]: 105 : if (!d_options.base.pluginShareSkolems)
342 : : {
343 : : // note we only remove purify skolems if the above option is disabled
344 : 0 : on = SkolemManager::getOriginalForm(n);
345 : : }
346 : 105 : SkolemManager* skm = d_nm->getSkolemManager();
347 : 105 : std::vector<Node> toProcess;
348 : 105 : toProcess.push_back(on);
349 : : // The set of kinds that we never want to share. Any kind that can appear
350 : : // in lemmas but we don't have API support for should go in this list.
351 : : const std::unordered_set<Kind> excludeKinds = {
352 : : Kind::INST_CONSTANT,
353 : : Kind::DUMMY_SKOLEM,
354 : : Kind::CARDINALITY_CONSTRAINT,
355 : 105 : Kind::COMBINED_CARDINALITY_CONSTRAINT};
356 : 105 : size_t index = 0;
357 : : do
358 : : {
359 : 155 : Node nn = toProcess[index];
360 : 155 : index++;
361 : : // get the symbols contained in nn
362 : 155 : std::unordered_set<Node> syms;
363 : 155 : expr::getSymbols(nn, syms);
364 [ + + ]: 298 : for (const Node& s : syms)
365 : : {
366 : 143 : Kind sk = s.getKind();
367 [ - + ]: 143 : if (excludeKinds.find(sk) != excludeKinds.end())
368 : : {
369 : : // these kinds are never sharable
370 : 0 : return Node::null();
371 : : }
372 [ + + ]: 143 : if (sk == Kind::SKOLEM)
373 : : {
374 [ - + ]: 50 : if (!d_options.base.pluginShareSkolems)
375 : : {
376 : : // not shared if option is false
377 : 0 : return Node::null();
378 : : }
379 : : // must ensure that the indices of the skolem are also legal
380 : : SkolemId id;
381 : 50 : Node cacheVal;
382 [ - + ]: 50 : if (!skm->isSkolemFunction(s, id, cacheVal))
383 : : {
384 : : // kind SKOLEM should imply that it is a skolem function
385 : 0 : DebugUnhandled();
386 : : return Node::null();
387 : : }
388 : 50 : if (!cacheVal.isNull()
389 [ + - ][ + - ]: 150 : && std::find(toProcess.begin(), toProcess.end(), cacheVal)
390 [ + - ]: 150 : == toProcess.end())
391 : : {
392 : : // if we have a cache value, add it to process vector
393 : 50 : toProcess.push_back(cacheVal);
394 : : }
395 [ + - ]: 50 : }
396 : : }
397 [ + - ][ + - ]: 310 : } while (index < toProcess.size());
[ + + ]
398 : : // If we didn't encounter an illegal term, we now eliminate subtyping
399 : 105 : SubtypeElimNodeConverter senc(d_nm);
400 : 105 : on = senc.convert(on);
401 : 105 : return on;
402 : 105 : }
403 : :
404 : : } // namespace cvc5::internal
|
