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