1 |
|
/****************************************************************************** |
2 |
|
* Top contributors (to current version): |
3 |
|
* Aina Niemetz, Andrew Reynolds, Gereon Kremer |
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 |
|
* Non-clausal simplification preprocessing pass. |
14 |
|
* |
15 |
|
* Run the nonclausal solver and try to solve all assigned theory literals. |
16 |
|
*/ |
17 |
|
|
18 |
|
#include "preprocessing/passes/non_clausal_simp.h" |
19 |
|
|
20 |
|
#include <vector> |
21 |
|
|
22 |
|
#include "context/cdo.h" |
23 |
|
#include "options/smt_options.h" |
24 |
|
#include "preprocessing/assertion_pipeline.h" |
25 |
|
#include "preprocessing/preprocessing_pass_context.h" |
26 |
|
#include "smt/preprocess_proof_generator.h" |
27 |
|
#include "smt/smt_statistics_registry.h" |
28 |
|
#include "theory/booleans/circuit_propagator.h" |
29 |
|
#include "theory/theory.h" |
30 |
|
#include "theory/theory_engine.h" |
31 |
|
#include "theory/theory_model.h" |
32 |
|
#include "theory/trust_substitutions.h" |
33 |
|
|
34 |
|
using namespace cvc5; |
35 |
|
using namespace cvc5::theory; |
36 |
|
|
37 |
|
namespace cvc5 { |
38 |
|
namespace preprocessing { |
39 |
|
namespace passes { |
40 |
|
|
41 |
|
/* -------------------------------------------------------------------------- */ |
42 |
|
|
43 |
9913 |
NonClausalSimp::Statistics::Statistics() |
44 |
9913 |
: d_numConstantProps(smtStatisticsRegistry().registerInt( |
45 |
9913 |
"preprocessing::passes::NonClausalSimp::NumConstantProps")) |
46 |
|
{ |
47 |
9913 |
} |
48 |
|
|
49 |
|
|
50 |
|
/* -------------------------------------------------------------------------- */ |
51 |
|
|
52 |
9913 |
NonClausalSimp::NonClausalSimp(PreprocessingPassContext* preprocContext) |
53 |
|
: PreprocessingPass(preprocContext, "non-clausal-simp"), |
54 |
9913 |
d_pnm(preprocContext->getProofNodeManager()), |
55 |
9913 |
d_llpg(d_pnm ? new smt::PreprocessProofGenerator( |
56 |
7562 |
d_pnm, userContext(), "NonClausalSimp::llpg") |
57 |
|
: nullptr), |
58 |
9913 |
d_llra(d_pnm ? new LazyCDProof( |
59 |
7562 |
d_pnm, nullptr, userContext(), "NonClausalSimp::llra") |
60 |
|
: nullptr), |
61 |
54776 |
d_tsubsList(userContext()) |
62 |
|
{ |
63 |
9913 |
} |
64 |
|
|
65 |
11034 |
PreprocessingPassResult NonClausalSimp::applyInternal( |
66 |
|
AssertionPipeline* assertionsToPreprocess) |
67 |
|
{ |
68 |
11034 |
d_preprocContext->spendResource(Resource::PreprocessStep); |
69 |
|
|
70 |
|
theory::booleans::CircuitPropagator* propagator = |
71 |
11034 |
d_preprocContext->getCircuitPropagator(); |
72 |
|
|
73 |
95041 |
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) |
74 |
|
{ |
75 |
168014 |
Trace("non-clausal-simplify") << "Assertion #" << i << " : " |
76 |
84007 |
<< (*assertionsToPreprocess)[i] << std::endl; |
77 |
|
} |
78 |
|
|
79 |
11034 |
if (propagator->getNeedsFinish()) |
80 |
|
{ |
81 |
4205 |
propagator->finish(); |
82 |
4205 |
propagator->setNeedsFinish(false); |
83 |
|
} |
84 |
11034 |
propagator->initialize(); |
85 |
|
|
86 |
|
// Assert all the assertions to the propagator |
87 |
11034 |
Trace("non-clausal-simplify") << "asserting to propagator" << std::endl; |
88 |
95041 |
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) |
89 |
|
{ |
90 |
84007 |
Assert(rewrite((*assertionsToPreprocess)[i]) |
91 |
|
== (*assertionsToPreprocess)[i]); |
92 |
|
// Don't reprocess substitutions |
93 |
84007 |
if (assertionsToPreprocess->isSubstsIndex(i)) |
94 |
|
{ |
95 |
3039 |
continue; |
96 |
|
} |
97 |
161936 |
Trace("non-clausal-simplify") |
98 |
80968 |
<< "asserting " << (*assertionsToPreprocess)[i] << std::endl; |
99 |
161936 |
Debug("cores") << "propagator->assertTrue: " << (*assertionsToPreprocess)[i] |
100 |
80968 |
<< std::endl; |
101 |
80968 |
propagator->assertTrue((*assertionsToPreprocess)[i]); |
102 |
|
} |
103 |
|
|
104 |
11034 |
Trace("non-clausal-simplify") << "propagating" << std::endl; |
105 |
22068 |
TrustNode conf = propagator->propagate(); |
106 |
11034 |
if (!conf.isNull()) |
107 |
|
{ |
108 |
|
// If in conflict, just return false |
109 |
1882 |
Trace("non-clausal-simplify") |
110 |
941 |
<< "conflict in non-clausal propagation" << std::endl; |
111 |
941 |
assertionsToPreprocess->clear(); |
112 |
941 |
assertionsToPreprocess->pushBackTrusted(conf); |
113 |
941 |
propagator->setNeedsFinish(true); |
114 |
941 |
return PreprocessingPassResult::CONFLICT; |
115 |
|
} |
116 |
|
|
117 |
20186 |
Trace("non-clausal-simplify") |
118 |
20186 |
<< "Iterate through " << propagator->getLearnedLiterals().size() |
119 |
10093 |
<< " learned literals." << std::endl; |
120 |
|
// No conflict, go through the literals and solve them |
121 |
10093 |
context::Context* u = userContext(); |
122 |
10093 |
TrustSubstitutionMap& ttls = d_preprocContext->getTopLevelSubstitutions(); |
123 |
10093 |
CVC5_UNUSED SubstitutionMap& top_level_substs = ttls.get(); |
124 |
|
// constant propagations |
125 |
|
std::shared_ptr<TrustSubstitutionMap> constantPropagations = |
126 |
|
std::make_shared<TrustSubstitutionMap>( |
127 |
20186 |
u, d_pnm, "NonClausalSimp::cprop", PfRule::PREPROCESS_LEMMA); |
128 |
10093 |
SubstitutionMap& cps = constantPropagations->get(); |
129 |
|
// new substitutions |
130 |
|
std::shared_ptr<TrustSubstitutionMap> newSubstitutions = |
131 |
|
std::make_shared<TrustSubstitutionMap>( |
132 |
20186 |
u, d_pnm, "NonClausalSimp::newSubs", PfRule::PREPROCESS_LEMMA); |
133 |
10093 |
SubstitutionMap& nss = newSubstitutions->get(); |
134 |
|
|
135 |
10093 |
size_t j = 0; |
136 |
10093 |
std::vector<TrustNode>& learned_literals = propagator->getLearnedLiterals(); |
137 |
|
// if proofs are enabled, we will need to track the proofs of learned literals |
138 |
10093 |
if (isProofEnabled()) |
139 |
|
{ |
140 |
1803 |
d_tsubsList.push_back(constantPropagations); |
141 |
1803 |
d_tsubsList.push_back(newSubstitutions); |
142 |
30036 |
for (const TrustNode& tll : learned_literals) |
143 |
|
{ |
144 |
28233 |
d_llpg->notifyNewTrustedAssert(tll); |
145 |
|
} |
146 |
|
} |
147 |
124387 |
for (size_t i = 0, size = learned_literals.size(); i < size; ++i) |
148 |
|
{ |
149 |
|
// Simplify the literal we learned wrt previous substitutions |
150 |
228221 |
Node learnedLiteral = learned_literals[i].getNode(); |
151 |
114454 |
Assert(rewrite(learnedLiteral) == learnedLiteral); |
152 |
114454 |
Assert(top_level_substs.apply(learnedLiteral) == learnedLiteral); |
153 |
|
// process the learned literal with substitutions and const propagations |
154 |
114454 |
learnedLiteral = processLearnedLit( |
155 |
|
learnedLiteral, newSubstitutions.get(), constantPropagations.get()); |
156 |
228908 |
Trace("non-clausal-simplify") |
157 |
114454 |
<< "Process learnedLiteral, after constProp : " << learnedLiteral |
158 |
114454 |
<< std::endl; |
159 |
|
// It might just simplify to a constant |
160 |
114454 |
if (learnedLiteral.isConst()) |
161 |
|
{ |
162 |
687 |
if (learnedLiteral.getConst<bool>()) |
163 |
|
{ |
164 |
|
// If the learned literal simplifies to true, it's redundant |
165 |
527 |
continue; |
166 |
|
} |
167 |
|
else |
168 |
|
{ |
169 |
|
// If the learned literal simplifies to false, we're in conflict |
170 |
320 |
Trace("non-clausal-simplify") |
171 |
160 |
<< "conflict with " << learned_literals[i].getNode() << std::endl; |
172 |
160 |
assertionsToPreprocess->clear(); |
173 |
320 |
Node n = NodeManager::currentNM()->mkConst<bool>(false); |
174 |
160 |
assertionsToPreprocess->push_back(n, false, false, d_llpg.get()); |
175 |
160 |
propagator->setNeedsFinish(true); |
176 |
160 |
return PreprocessingPassResult::CONFLICT; |
177 |
|
} |
178 |
|
} |
179 |
|
|
180 |
|
// Solve it with the corresponding theory, possibly adding new |
181 |
|
// substitutions to newSubstitutions |
182 |
113767 |
Trace("non-clausal-simplify") << "solving " << learnedLiteral << std::endl; |
183 |
|
|
184 |
|
TrustNode tlearnedLiteral = |
185 |
227534 |
TrustNode::mkTrustLemma(learnedLiteral, d_llpg.get()); |
186 |
|
Theory::PPAssertStatus solveStatus = |
187 |
341301 |
d_preprocContext->getTheoryEngine()->solve(tlearnedLiteral, |
188 |
227534 |
*newSubstitutions.get()); |
189 |
|
|
190 |
113767 |
switch (solveStatus) |
191 |
|
{ |
192 |
48246 |
case Theory::PP_ASSERT_STATUS_SOLVED: |
193 |
|
{ |
194 |
|
// The literal should rewrite to true |
195 |
96492 |
Trace("non-clausal-simplify") |
196 |
48246 |
<< "solved " << learnedLiteral << std::endl; |
197 |
48246 |
Assert(rewrite(nss.apply(learnedLiteral)).isConst()); |
198 |
|
// else fall through |
199 |
48246 |
break; |
200 |
|
} |
201 |
|
case Theory::PP_ASSERT_STATUS_CONFLICT: |
202 |
|
{ |
203 |
|
// If in conflict, we return false |
204 |
|
Trace("non-clausal-simplify") |
205 |
|
<< "conflict while solving " << learnedLiteral << std::endl; |
206 |
|
assertionsToPreprocess->clear(); |
207 |
|
Node n = NodeManager::currentNM()->mkConst<bool>(false); |
208 |
|
assertionsToPreprocess->push_back(n); |
209 |
|
propagator->setNeedsFinish(true); |
210 |
|
return PreprocessingPassResult::CONFLICT; |
211 |
|
} |
212 |
65521 |
default: |
213 |
131042 |
if (learnedLiteral.getKind() == kind::EQUAL |
214 |
131042 |
&& (learnedLiteral[0].isConst() || learnedLiteral[1].isConst())) |
215 |
|
{ |
216 |
|
// constant propagation |
217 |
11140 |
TNode t; |
218 |
11140 |
TNode c; |
219 |
5570 |
if (learnedLiteral[0].isConst()) |
220 |
|
{ |
221 |
215 |
t = learnedLiteral[1]; |
222 |
215 |
c = learnedLiteral[0]; |
223 |
|
} |
224 |
|
else |
225 |
|
{ |
226 |
5355 |
t = learnedLiteral[0]; |
227 |
5355 |
c = learnedLiteral[1]; |
228 |
|
} |
229 |
5570 |
Assert(!t.isConst()); |
230 |
5570 |
Assert(cps.apply(t, true) == t); |
231 |
5570 |
Assert(top_level_substs.apply(t) == t); |
232 |
5570 |
Assert(nss.apply(t) == t); |
233 |
|
// also add to learned literal |
234 |
11140 |
ProofGenerator* cpg = constantPropagations->addSubstitutionSolved( |
235 |
5570 |
t, c, tlearnedLiteral); |
236 |
|
// We need to justify (= t c) as a literal, since it is reasserted |
237 |
|
// to the assertion pipeline below. We do this with the proof |
238 |
|
// generator returned by the above call. |
239 |
5570 |
if (isProofEnabled()) |
240 |
|
{ |
241 |
1456 |
d_llpg->notifyNewAssert(t.eqNode(c), cpg); |
242 |
|
} |
243 |
|
} |
244 |
|
else |
245 |
|
{ |
246 |
|
// Keep the literal |
247 |
59951 |
learned_literals[j++] = learned_literals[i]; |
248 |
|
// Its a literal that could not be processed as a substitution or |
249 |
|
// conflict. In this case, we notify the context of the learned |
250 |
|
// literal, which will process it with the learned literal manager. |
251 |
59951 |
d_preprocContext->notifyLearnedLiteral(learnedLiteral); |
252 |
|
} |
253 |
65521 |
break; |
254 |
|
} |
255 |
|
} |
256 |
|
|
257 |
|
#ifdef CVC5_ASSERTIONS |
258 |
|
// NOTE: When debugging this code, consider moving this check inside of the |
259 |
|
// loop over propagator->getLearnedLiterals(). This check has been moved |
260 |
|
// outside because it is costly for certain inputs (see bug 508). |
261 |
|
// |
262 |
|
// Check data structure invariants: |
263 |
|
// 1. for each lhs of top_level_substs, does not appear anywhere in rhs of |
264 |
|
// top_level_substs or anywhere in constantPropagations |
265 |
|
// 2. each lhs of constantPropagations rewrites to itself |
266 |
|
// 3. if l -> r is a constant propagation and l is a subterm of l' with l' -> |
267 |
|
// r' another constant propagation, then l'[l/r] -> r' should be a |
268 |
|
// constant propagation too |
269 |
|
// 4. each lhs of constantPropagations is different from each rhs |
270 |
57592 |
for (SubstitutionMap::iterator pos = nss.begin(); pos != nss.end(); ++pos) |
271 |
|
{ |
272 |
47659 |
Assert((*pos).first.isVar()); |
273 |
47659 |
Assert(top_level_substs.apply((*pos).first) == (*pos).first); |
274 |
47659 |
Assert(top_level_substs.apply((*pos).second) == (*pos).second); |
275 |
95318 |
Node app = nss.apply((*pos).second); |
276 |
47659 |
Assert(nss.apply(app) == app); |
277 |
|
} |
278 |
15483 |
for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos) |
279 |
|
{ |
280 |
5550 |
Assert((*pos).second.isConst()); |
281 |
5550 |
Assert(rewrite((*pos).first) == (*pos).first); |
282 |
5550 |
Assert(cps.apply((*pos).second) == (*pos).second); |
283 |
|
} |
284 |
|
#endif /* CVC5_ASSERTIONS */ |
285 |
|
|
286 |
|
// Resize the learnt |
287 |
19866 |
Trace("non-clausal-simplify") |
288 |
9933 |
<< "Resize non-clausal learned literals to " << j << std::endl; |
289 |
9933 |
learned_literals.resize(j); |
290 |
|
|
291 |
19866 |
std::unordered_set<TNode> s; |
292 |
89097 |
for (size_t i = 0, size = assertionsToPreprocess->size(); i < size; ++i) |
293 |
|
{ |
294 |
158328 |
Node assertion = (*assertionsToPreprocess)[i]; |
295 |
158328 |
TrustNode assertionNew = newSubstitutions->applyTrusted(assertion); |
296 |
79164 |
Trace("non-clausal-simplify") << "assertion = " << assertion << std::endl; |
297 |
79164 |
if (!assertionNew.isNull()) |
298 |
|
{ |
299 |
57378 |
Trace("non-clausal-simplify") |
300 |
28689 |
<< "assertionNew = " << assertionNew.getNode() << std::endl; |
301 |
28689 |
assertionsToPreprocess->replaceTrusted(i, assertionNew); |
302 |
28689 |
assertion = assertionNew.getNode(); |
303 |
28689 |
Assert(rewrite(assertion) == assertion); |
304 |
|
} |
305 |
|
for (;;) |
306 |
|
{ |
307 |
81326 |
assertionNew = constantPropagations->applyTrusted(assertion); |
308 |
80245 |
if (assertionNew.isNull()) |
309 |
|
{ |
310 |
79164 |
break; |
311 |
|
} |
312 |
1081 |
Assert(assertionNew.getNode() != assertion); |
313 |
1081 |
assertionsToPreprocess->replaceTrusted(i, assertionNew); |
314 |
1081 |
assertion = assertionNew.getNode(); |
315 |
1081 |
d_statistics.d_numConstantProps += 1; |
316 |
2162 |
Trace("non-clausal-simplify") |
317 |
1081 |
<< "assertionNew = " << assertion << std::endl; |
318 |
|
} |
319 |
79164 |
s.insert(assertion); |
320 |
158328 |
Trace("non-clausal-simplify") |
321 |
79164 |
<< "non-clausal preprocessed: " << assertion << std::endl; |
322 |
|
} |
323 |
|
|
324 |
|
// If necessary, add as assertions if needed (when incremental). This is |
325 |
|
// necessary because certain variables cannot truly be eliminated when |
326 |
|
// we are in incremental mode. For example, say our first call to check-sat |
327 |
|
// is a formula F containing variable x. On the second call to check-sat, |
328 |
|
// say we solve a top-level assertion (= x t). Since the solver already has |
329 |
|
// constraints involving x, we must still keep (= x t) as an assertion. |
330 |
|
// However, notice that we do not retract the substitution { x -> t }. This |
331 |
|
// means that all *subsequent* assertions after (= x t) will replace x by t. |
332 |
9933 |
if (assertionsToPreprocess->storeSubstsInAsserts()) |
333 |
|
{ |
334 |
5469 |
for (const std::pair<const Node, const Node>& pos: nss) |
335 |
|
{ |
336 |
5290 |
Node lhs = pos.first; |
337 |
|
// If using incremental, we must check whether this variable has occurred |
338 |
|
// before now. If it has, we must add as an assertion. |
339 |
2645 |
if (d_preprocContext->getSymsInAssertions().contains(lhs)) |
340 |
|
{ |
341 |
|
// if it has, the substitution becomes an assertion |
342 |
2734 |
TrustNode trhs = newSubstitutions->applyTrusted(lhs); |
343 |
1367 |
Assert(!trhs.isNull()); |
344 |
2734 |
Trace("non-clausal-simplify") |
345 |
1367 |
<< "substitute: will notify SAT layer of substitution: " |
346 |
1367 |
<< trhs.getProven() << std::endl; |
347 |
1367 |
assertionsToPreprocess->addSubstitutionNode(trhs.getProven(), |
348 |
|
trhs.getGenerator()); |
349 |
|
} |
350 |
|
} |
351 |
|
} |
352 |
|
|
353 |
9933 |
Assert(assertionsToPreprocess->getRealAssertionsEnd() |
354 |
|
<= assertionsToPreprocess->size()); |
355 |
|
// Learned literals to conjoin. If proofs are enabled, all these are |
356 |
|
// justified by d_llpg. |
357 |
19866 |
std::vector<Node> learnedLitsToConjoin; |
358 |
|
|
359 |
69345 |
for (size_t i = 0; i < learned_literals.size(); ++i) |
360 |
|
{ |
361 |
97699 |
Node learned = learned_literals[i].getNode(); |
362 |
59412 |
Assert(top_level_substs.apply(learned) == learned); |
363 |
|
// process learned literal |
364 |
59412 |
learned = processLearnedLit( |
365 |
|
learned, newSubstitutions.get(), constantPropagations.get()); |
366 |
59412 |
if (s.find(learned) != s.end()) |
367 |
|
{ |
368 |
21125 |
continue; |
369 |
|
} |
370 |
38287 |
s.insert(learned); |
371 |
38287 |
learnedLitsToConjoin.push_back(learned); |
372 |
76574 |
Trace("non-clausal-simplify") |
373 |
38287 |
<< "non-clausal learned : " << learned << std::endl; |
374 |
|
} |
375 |
9933 |
learned_literals.clear(); |
376 |
|
|
377 |
15483 |
for (SubstitutionMap::iterator pos = cps.begin(); pos != cps.end(); ++pos) |
378 |
|
{ |
379 |
10994 |
Node cProp = (*pos).first.eqNode((*pos).second); |
380 |
5550 |
Assert(top_level_substs.apply(cProp) == cProp); |
381 |
|
// process learned literal (substitutions only) |
382 |
5550 |
cProp = processLearnedLit(cProp, newSubstitutions.get(), nullptr); |
383 |
5550 |
if (s.find(cProp) != s.end()) |
384 |
|
{ |
385 |
106 |
continue; |
386 |
|
} |
387 |
5444 |
s.insert(cProp); |
388 |
5444 |
learnedLitsToConjoin.push_back(cProp); |
389 |
10888 |
Trace("non-clausal-simplify") |
390 |
5444 |
<< "non-clausal constant propagation : " << cProp << std::endl; |
391 |
|
} |
392 |
|
|
393 |
|
// Add new substitutions to topLevelSubstitutions |
394 |
|
// Note that we don't have to keep rhs's in full solved form |
395 |
|
// because SubstitutionMap::apply does a fixed-point iteration when |
396 |
|
// substituting |
397 |
9933 |
ttls.addSubstitutions(*newSubstitutions.get()); |
398 |
|
|
399 |
9933 |
if (!learnedLitsToConjoin.empty()) |
400 |
|
{ |
401 |
2517 |
size_t replIndex = assertionsToPreprocess->getRealAssertionsEnd() - 1; |
402 |
5034 |
Node newConj = NodeManager::currentNM()->mkAnd(learnedLitsToConjoin); |
403 |
5034 |
Trace("non-clausal-simplify") |
404 |
2517 |
<< "non-clausal simplification, reassert: " << newConj << std::endl; |
405 |
2517 |
ProofGenerator* pg = nullptr; |
406 |
2517 |
if (isProofEnabled()) |
407 |
|
{ |
408 |
|
// justify in d_llra |
409 |
15356 |
for (const Node& lit : learnedLitsToConjoin) |
410 |
|
{ |
411 |
14923 |
d_llra->addLazyStep(lit, d_llpg.get()); |
412 |
|
} |
413 |
433 |
if (learnedLitsToConjoin.size() > 1) |
414 |
|
{ |
415 |
320 |
d_llra->addStep(newConj, PfRule::AND_INTRO, learnedLitsToConjoin, {}); |
416 |
320 |
pg = d_llra.get(); |
417 |
|
} |
418 |
|
else |
419 |
|
{ |
420 |
|
// otherwise we ask the learned literal proof generator directly |
421 |
113 |
pg = d_llpg.get(); |
422 |
|
} |
423 |
|
} |
424 |
|
// ------- from d_llpg --------- from d_llpg |
425 |
|
// conj[0] .... d_conj[n] |
426 |
|
// -------------------------------- AND_INTRO |
427 |
|
// newConj |
428 |
|
// where newConj is conjoined at the given index |
429 |
2517 |
assertionsToPreprocess->conjoin(replIndex, newConj, pg); |
430 |
|
} |
431 |
|
|
432 |
9933 |
propagator->setNeedsFinish(true); |
433 |
|
|
434 |
|
// Note that typically ttls.apply(assert)==assert here. |
435 |
|
// However, this invariant is invalidated for cases where we use explicit |
436 |
|
// equality assertions for variables solved in incremental mode that already |
437 |
|
// exist in assertions, as described above. |
438 |
|
|
439 |
9933 |
return PreprocessingPassResult::NO_CONFLICT; |
440 |
|
} |
441 |
|
|
442 |
58977 |
bool NonClausalSimp::isProofEnabled() const { return d_pnm != nullptr; } |
443 |
|
|
444 |
179416 |
Node NonClausalSimp::processLearnedLit(Node lit, |
445 |
|
theory::TrustSubstitutionMap* subs, |
446 |
|
theory::TrustSubstitutionMap* cp) |
447 |
|
{ |
448 |
358832 |
TrustNode tlit; |
449 |
179416 |
if (subs != nullptr) |
450 |
|
{ |
451 |
179416 |
tlit = subs->applyTrusted(lit); |
452 |
179416 |
if (!tlit.isNull()) |
453 |
|
{ |
454 |
40657 |
lit = processRewrittenLearnedLit(tlit); |
455 |
|
} |
456 |
358832 |
Trace("non-clausal-simplify") |
457 |
179416 |
<< "Process learnedLiteral, after newSubs : " << lit << std::endl; |
458 |
|
} |
459 |
|
// apply to fixed point |
460 |
179416 |
if (cp != nullptr) |
461 |
|
{ |
462 |
|
for (;;) |
463 |
|
{ |
464 |
174146 |
tlit = cp->applyTrusted(lit); |
465 |
174006 |
if (tlit.isNull()) |
466 |
|
{ |
467 |
173866 |
break; |
468 |
|
} |
469 |
140 |
Assert(lit != tlit.getNode()); |
470 |
140 |
lit = processRewrittenLearnedLit(tlit); |
471 |
140 |
d_statistics.d_numConstantProps += 1; |
472 |
|
} |
473 |
|
} |
474 |
358832 |
return lit; |
475 |
|
} |
476 |
|
|
477 |
40797 |
Node NonClausalSimp::processRewrittenLearnedLit(TrustNode trn) |
478 |
|
{ |
479 |
40797 |
if (isProofEnabled()) |
480 |
|
{ |
481 |
15127 |
d_llpg->notifyTrustedPreprocessed(trn); |
482 |
|
} |
483 |
|
// return the node |
484 |
40797 |
return trn.getNode(); |
485 |
|
} |
486 |
|
|
487 |
|
} // namespace passes |
488 |
|
} // namespace preprocessing |
489 |
29502 |
} // namespace cvc5 |