1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Andrew Reynolds, Gereon Kremer, Aina Niemetz |
4 |
|
* |
5 |
|
* This file is part of the cvc5 project. |
6 |
|
* |
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 |
|
* **************************************************************************** |
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 "options/base_options.h" |
22 |
|
#include "options/quantifiers_options.h" |
23 |
|
#include "options/smt_options.h" |
24 |
|
#include "options/strings_options.h" |
25 |
|
#include "printer/printer.h" |
26 |
|
#include "proof/conv_proof_generator.h" |
27 |
|
#include "smt/solver_engine_stats.h" |
28 |
|
#include "theory/evaluator.h" |
29 |
|
#include "theory/rewriter.h" |
30 |
|
#include "theory/trust_substitutions.h" |
31 |
|
#include "util/resource_manager.h" |
32 |
|
#include "util/statistics_registry.h" |
33 |
|
|
34 |
|
using namespace cvc5::smt; |
35 |
|
|
36 |
|
namespace cvc5 { |
37 |
|
|
38 |
18655 |
Env::Env(NodeManager* nm, const Options* opts) |
39 |
18655 |
: d_context(new context::Context()), |
40 |
18655 |
d_userContext(new context::UserContext()), |
41 |
|
d_nodeManager(nm), |
42 |
|
d_proofNodeManager(nullptr), |
43 |
18655 |
d_rewriter(new theory::Rewriter()), |
44 |
|
d_evalRew(nullptr), |
45 |
|
d_eval(nullptr), |
46 |
37310 |
d_topLevelSubs(new theory::TrustSubstitutionMap(d_userContext.get())), |
47 |
|
d_logic(), |
48 |
|
d_statisticsRegistry(std::make_unique<StatisticsRegistry>(*this)), |
49 |
|
d_options(), |
50 |
|
d_originalOptions(opts), |
51 |
111930 |
d_resourceManager() |
52 |
|
{ |
53 |
18655 |
if (opts != nullptr) |
54 |
|
{ |
55 |
17767 |
d_options.copyValues(*opts); |
56 |
|
} |
57 |
|
// make the evaluators, which depend on the alphabet of strings |
58 |
37310 |
d_evalRew.reset(new theory::Evaluator(d_rewriter.get(), |
59 |
18655 |
d_options.strings.stringsAlphaCard)); |
60 |
37310 |
d_eval.reset( |
61 |
18655 |
new theory::Evaluator(nullptr, d_options.strings.stringsAlphaCard)); |
62 |
18655 |
d_statisticsRegistry->registerTimer("global::totalTime").start(); |
63 |
18655 |
d_resourceManager = std::make_unique<ResourceManager>(*d_statisticsRegistry, d_options); |
64 |
18655 |
d_rewriter->d_resourceManager = d_resourceManager.get(); |
65 |
18655 |
} |
66 |
|
|
67 |
15906 |
Env::~Env() {} |
68 |
|
|
69 |
7989 |
void Env::setProofNodeManager(ProofNodeManager* pnm) |
70 |
|
{ |
71 |
7989 |
Assert(pnm != nullptr); |
72 |
7989 |
Assert(d_proofNodeManager == nullptr); |
73 |
7989 |
d_proofNodeManager = pnm; |
74 |
7989 |
d_rewriter->setProofNodeManager(pnm); |
75 |
7989 |
d_topLevelSubs->setProofNodeManager(pnm); |
76 |
7989 |
} |
77 |
|
|
78 |
15884 |
void Env::shutdown() |
79 |
|
{ |
80 |
15884 |
d_rewriter.reset(nullptr); |
81 |
|
// d_resourceManager must be destroyed before d_statisticsRegistry |
82 |
15884 |
d_resourceManager.reset(nullptr); |
83 |
15884 |
} |
84 |
|
|
85 |
48691008 |
context::Context* Env::getContext() { return d_context.get(); } |
86 |
|
|
87 |
1819362 |
context::UserContext* Env::getUserContext() { return d_userContext.get(); } |
88 |
|
|
89 |
1310475 |
NodeManager* Env::getNodeManager() const { return d_nodeManager; } |
90 |
|
|
91 |
749194 |
ProofNodeManager* Env::getProofNodeManager() { return d_proofNodeManager; } |
92 |
|
|
93 |
146017 |
bool Env::isSatProofProducing() const |
94 |
|
{ |
95 |
146017 |
return d_proofNodeManager != nullptr |
96 |
176696 |
&& (!d_options.smt.unsatCores |
97 |
62515 |
|| (d_options.smt.unsatCoresMode |
98 |
|
!= options::UnsatCoresMode::ASSUMPTIONS |
99 |
30683 |
&& d_options.smt.unsatCoresMode |
100 |
146017 |
!= options::UnsatCoresMode::PP_ONLY)); |
101 |
|
} |
102 |
|
|
103 |
1342220 |
bool Env::isTheoryProofProducing() const |
104 |
|
{ |
105 |
1342220 |
return d_proofNodeManager != nullptr |
106 |
1612241 |
&& (!d_options.smt.unsatCores |
107 |
524794 |
|| d_options.smt.unsatCoresMode |
108 |
1342220 |
== options::UnsatCoresMode::FULL_PROOF); |
109 |
|
} |
110 |
|
|
111 |
87825380 |
theory::Rewriter* Env::getRewriter() { return d_rewriter.get(); } |
112 |
|
|
113 |
15273 |
theory::Evaluator* Env::getEvaluator(bool useRewriter) |
114 |
|
{ |
115 |
15273 |
return useRewriter ? d_evalRew.get() : d_eval.get(); |
116 |
|
} |
117 |
|
|
118 |
400236 |
theory::TrustSubstitutionMap& Env::getTopLevelSubstitutions() |
119 |
|
{ |
120 |
400236 |
return *d_topLevelSubs.get(); |
121 |
|
} |
122 |
|
|
123 |
8282015 |
const LogicInfo& Env::getLogicInfo() const { return d_logic; } |
124 |
|
|
125 |
6121880 |
StatisticsRegistry& Env::getStatisticsRegistry() |
126 |
|
{ |
127 |
6121880 |
return *d_statisticsRegistry; |
128 |
|
} |
129 |
|
|
130 |
66527139 |
const Options& Env::getOptions() const { return d_options; } |
131 |
|
|
132 |
2 |
const Options& Env::getOriginalOptions() const { return *d_originalOptions; } |
133 |
|
|
134 |
16490958 |
ResourceManager* Env::getResourceManager() const |
135 |
|
{ |
136 |
16490958 |
return d_resourceManager.get(); |
137 |
|
} |
138 |
|
|
139 |
1 |
const Printer& Env::getPrinter() |
140 |
|
{ |
141 |
1 |
return *Printer::getPrinter(d_options.base.outputLanguage); |
142 |
|
} |
143 |
|
|
144 |
336067 |
bool Env::isOutputOn(OutputTag tag) const |
145 |
|
{ |
146 |
336067 |
return d_options.base.outputTagHolder[static_cast<size_t>(tag)]; |
147 |
|
} |
148 |
242434 |
bool Env::isOutputOn(const std::string& tag) const |
149 |
|
{ |
150 |
242434 |
return isOutputOn(options::stringToOutputTag(tag)); |
151 |
|
} |
152 |
27 |
std::ostream& Env::output(const std::string& tag) const |
153 |
|
{ |
154 |
27 |
return output(options::stringToOutputTag(tag)); |
155 |
|
} |
156 |
|
|
157 |
39 |
std::ostream& Env::output(OutputTag tag) const |
158 |
|
{ |
159 |
39 |
if (isOutputOn(tag)) |
160 |
|
{ |
161 |
37 |
return *d_options.base.out; |
162 |
|
} |
163 |
2 |
return cvc5::null_os; |
164 |
|
} |
165 |
|
|
166 |
407094 |
bool Env::isVerboseOn(int64_t level) const |
167 |
|
{ |
168 |
407094 |
return !Configuration::isMuzzledBuild() && d_options.base.verbosity >= level; |
169 |
|
} |
170 |
|
|
171 |
405657 |
std::ostream& Env::verbose(int64_t level) const |
172 |
|
{ |
173 |
405657 |
if (isVerboseOn(level)) |
174 |
|
{ |
175 |
49 |
return *d_options.base.err; |
176 |
|
} |
177 |
405608 |
return cvc5::null_os; |
178 |
|
} |
179 |
|
|
180 |
11 |
std::ostream& Env::warning() const |
181 |
|
{ |
182 |
11 |
return verbose(0); |
183 |
|
} |
184 |
|
|
185 |
986969 |
Node Env::evaluate(TNode n, |
186 |
|
const std::vector<Node>& args, |
187 |
|
const std::vector<Node>& vals, |
188 |
|
bool useRewriter) const |
189 |
|
{ |
190 |
1973938 |
std::unordered_map<Node, Node> visited; |
191 |
1973938 |
return evaluate(n, args, vals, visited, useRewriter); |
192 |
|
} |
193 |
|
|
194 |
1007730 |
Node Env::evaluate(TNode n, |
195 |
|
const std::vector<Node>& args, |
196 |
|
const std::vector<Node>& vals, |
197 |
|
const std::unordered_map<Node, Node>& visited, |
198 |
|
bool useRewriter) const |
199 |
|
{ |
200 |
1007730 |
if (useRewriter) |
201 |
|
{ |
202 |
974436 |
return d_evalRew->eval(n, args, vals, visited); |
203 |
|
} |
204 |
33294 |
return d_eval->eval(n, args, vals, visited); |
205 |
|
} |
206 |
|
|
207 |
1724111 |
Node Env::rewriteViaMethod(TNode n, MethodId idr) |
208 |
|
{ |
209 |
1724111 |
if (idr == MethodId::RW_REWRITE) |
210 |
|
{ |
211 |
1690538 |
return d_rewriter->rewrite(n); |
212 |
|
} |
213 |
33573 |
if (idr == MethodId::RW_EXT_REWRITE) |
214 |
|
{ |
215 |
42 |
return d_rewriter->extendedRewrite(n); |
216 |
|
} |
217 |
33531 |
if (idr == MethodId::RW_REWRITE_EQ_EXT) |
218 |
|
{ |
219 |
237 |
return d_rewriter->rewriteEqualityExt(n); |
220 |
|
} |
221 |
33294 |
if (idr == MethodId::RW_EVALUATE) |
222 |
|
{ |
223 |
33294 |
return evaluate(n, {}, {}, false); |
224 |
|
} |
225 |
|
if (idr == MethodId::RW_IDENTITY) |
226 |
|
{ |
227 |
|
// does nothing |
228 |
|
return n; |
229 |
|
} |
230 |
|
// unknown rewriter |
231 |
|
Unhandled() << "Env::rewriteViaMethod: no rewriter for " << idr |
232 |
|
<< std::endl; |
233 |
|
return n; |
234 |
|
} |
235 |
|
|
236 |
8372256 |
bool Env::isFiniteType(TypeNode tn) const |
237 |
|
{ |
238 |
8372256 |
return isCardinalityClassFinite(tn.getCardinalityClass(), |
239 |
16744512 |
d_options.quantifiers.finiteModelFind); |
240 |
|
} |
241 |
|
|
242 |
31137 |
} // namespace cvc5 |