Branch data Line data Source code
1 : : /******************************************************************************
2 : : * Top contributors (to current version):
3 : : * Andrew Reynolds, Aina Niemetz, Gereon Kremer
4 : : *
5 : : * This file is part of the cvc5 project.
6 : : *
7 : : * Copyright (c) 2009-2024 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 : : * Implementation of the justification SAT decision strategy
14 : : */
15 : :
16 : : #include "decision/justification_strategy.h"
17 : :
18 : : #include "expr/node_algorithm.h"
19 : : #include "prop/skolem_def_manager.h"
20 : :
21 : : using namespace cvc5::internal::kind;
22 : : using namespace cvc5::internal::prop;
23 : :
24 : : namespace cvc5::internal {
25 : : namespace decision {
26 : :
27 : 39518 : JustificationStrategy::JustificationStrategy(Env& env,
28 : : prop::CDCLTSatSolver* ss,
29 : 39518 : prop::CnfStream* cs)
30 : : : DecisionEngine(env, ss, cs),
31 : : d_assertions(
32 : 79036 : userContext(),
33 : : context(),
34 : 79036 : options()
35 : 39518 : .decision.jhRlvOrder), // assertions are user-context dependent
36 : : d_localAssertions(
37 : : context(), context()), // local assertions are SAT-context dependent
38 : : d_jcache(context(), ss, cs),
39 : : d_stack(context()),
40 : : d_lastDecisionLit(context()),
41 : : d_currStatusDec(false),
42 : 79036 : d_useRlvOrder(options().decision.jhRlvOrder),
43 : 79036 : d_decisionStopOnly(options().decision.decisionMode
44 : 39518 : == options::DecisionMode::STOPONLY),
45 : 79036 : d_jhSkMode(options().decision.jhSkolemMode),
46 : 79036 : d_jhSkRlvMode(options().decision.jhSkolemRlvMode),
47 : 39518 : d_stats(statisticsRegistry())
48 : : {
49 : 39518 : }
50 : :
51 : 37133 : void JustificationStrategy::presolve()
52 : : {
53 : 37133 : d_lastDecisionLit = Node::null();
54 : 37133 : d_currUnderStatus = Node::null();
55 : 37133 : d_currStatusDec = false;
56 : : // reset the dynamic assertion list data
57 : 37133 : d_assertions.presolve();
58 : 37133 : d_localAssertions.presolve();
59 : : // clear the stack
60 : 37133 : d_stack.clear();
61 : 37133 : }
62 : :
63 : 8365200 : SatLiteral JustificationStrategy::getNextInternal(bool& stopSearch)
64 : : {
65 : : // ensure we have an assertion
66 [ + + ]: 8365200 : if (!refreshCurrentAssertion())
67 : : {
68 [ + - ]: 13662 : Trace("jh-process") << "getNext, already finished" << std::endl;
69 : 13662 : stopSearch = true;
70 : 13662 : return undefSatLiteral;
71 : : }
72 [ - + ][ - + ]: 8351540 : Assert(d_stack.hasCurrentAssertion());
[ - - ]
73 : : // temporary information in the loop below
74 : : JustifyInfo* ji;
75 : 16703100 : JustifyNode next;
76 : : // we start with the value implied by the last decision, if it exists
77 : 8351540 : SatValue lastChildVal = SAT_VALUE_UNKNOWN;
78 [ + - ]: 8351540 : Trace("jh-process") << "getNext" << std::endl;
79 : : // If we had just sent a decision, then we lookup its value here. This may
80 : : // correspond to a context where the decision was carried out, or
81 : : // alternatively it may correspond to a case where we have backtracked and
82 : : // propagated that literal with opposite polarity. Thus, we do not assume we
83 : : // know the value of d_lastDecisionLit and look it up again here. The value
84 : : // of lastChildVal will be used to update the justify info in the current
85 : : // stack below.
86 [ + + ]: 8351540 : if (!d_lastDecisionLit.get().isNull())
87 : : {
88 [ + - ]: 16583400 : Trace("jh-process") << "last decision = " << d_lastDecisionLit.get()
89 : 8291720 : << std::endl;
90 : 8291720 : lastChildVal = d_jcache.lookupValue(d_lastDecisionLit.get());
91 [ + + ]: 8291720 : if (lastChildVal == SAT_VALUE_UNKNOWN)
92 : : {
93 : : // if the value is now unknown, we must reprocess the assertion, since
94 : : // we have backtracked
95 : 184689 : TNode curr = d_stack.getCurrentAssertion();
96 : 184689 : d_stack.clear();
97 : 184689 : d_stack.reset(curr);
98 : : }
99 : : }
100 : 8351540 : d_lastDecisionLit = TNode::null();
101 : : // while we are trying to satisfy assertions
102 : 43698800 : do
103 : : {
104 [ - + ][ - + ]: 52050400 : Assert(d_stack.getCurrent() != nullptr);
[ - - ]
105 : : // We get the next justify node, if it can be found.
106 : 29743800 : do
107 : : {
108 : : // get the current justify info, which should be ready
109 : 81794200 : ji = d_stack.getCurrent();
110 [ + + ]: 81794200 : if (ji == nullptr)
111 : : {
112 : 19917800 : break;
113 : : }
114 : : // get the next child to process from the current justification info
115 : : // based on the fact that its last child processed had value lastChildVal.
116 : 61876400 : next = getNextJustifyNode(ji, lastChildVal);
117 : : // if the current node is finished, we pop the stack
118 [ + + ]: 61876400 : if (next.first.isNull())
119 : : {
120 : 29743800 : d_stack.popStack();
121 : : }
122 [ + + ]: 61876400 : } while (next.first.isNull());
123 : :
124 [ + + ]: 52050400 : if (ji == nullptr)
125 : : {
126 : : // the assertion we just processed should have value true
127 [ - + ][ - + ]: 19917800 : Assert(lastChildVal == SAT_VALUE_TRUE);
[ - - ]
128 [ + + ]: 19917800 : if (!d_currUnderStatus.isNull())
129 : : {
130 : : // notify status if we are watching it
131 : : DecisionStatus ds;
132 [ + + ]: 18616500 : if (d_currStatusDec)
133 : : {
134 : 2038340 : ds = DecisionStatus::DECISION;
135 : 2038340 : ++(d_stats.d_numStatusDecision);
136 : : }
137 : : else
138 : : {
139 : 16578100 : ds = DecisionStatus::NO_DECISION;
140 : 16578100 : ++(d_stats.d_numStatusNoDecision);
141 : : }
142 : 18616500 : d_assertions.notifyStatus(d_currUnderStatus, ds);
143 : : }
144 : : // we did not find a next node for current, refresh current assertion
145 : 19917800 : d_stack.clear();
146 : 19917800 : refreshCurrentAssertion();
147 : 19917800 : lastChildVal = SAT_VALUE_UNKNOWN;
148 [ + - ]: 39835600 : Trace("jh-process") << "...exhausted assertion, now "
149 [ - + ][ - - ]: 19917800 : << d_stack.getCurrentAssertion() << std::endl;
150 : : }
151 : : else
152 : : {
153 : : // must have requested a next child to justify
154 [ - + ][ - + ]: 32132500 : Assert(!next.first.isNull());
[ - - ]
155 [ - + ][ - + ]: 32132500 : Assert(next.second != SAT_VALUE_UNKNOWN);
[ - - ]
156 : : // Look up whether the next child already has a value
157 : 32132500 : lastChildVal = d_jcache.lookupValue(next.first);
158 [ + + ]: 32132500 : if (lastChildVal == SAT_VALUE_UNKNOWN)
159 : : {
160 : 18344700 : bool nextPol = next.first.getKind() != Kind::NOT;
161 [ + + ]: 18344700 : TNode nextAtom = nextPol ? next.first : next.first[0];
162 [ + + ]: 18344700 : if (expr::isTheoryAtom(nextAtom))
163 : : {
164 : : // should be assigned a literal
165 [ - + ][ - + ]: 8258260 : Assert(d_cnfStream->hasLiteral(nextAtom));
[ - - ]
166 : : // get the SAT literal
167 : 8258260 : SatLiteral nsl = d_cnfStream->getLiteral(nextAtom);
168 : : // flip if the atom was negated
169 : : // store the last decision value here, which will be used at the
170 : : // starting value on the next call to this method
171 [ + + ]: 8258260 : lastChildVal = nextPol ? next.second : invertValue(next.second);
172 : : // (1) atom with unassigned value, return it as the decision, possibly
173 : : // inverted
174 [ + - ]: 16516500 : Trace("jh-process")
175 : 8258260 : << "...return " << nextAtom << " " << lastChildVal << std::endl;
176 : : // Note that the last child of the current node we looked at does
177 : : // *not* yet have a value. Although we are returning it as a decision,
178 : : // we cannot set its value in d_jcache, because we have yet to
179 : : // push a decision level. Thus, we remember the literal we decided
180 : : // on. The value of d_lastDecisionLit will be processed at the
181 : : // beginning of the next call to getNext above.
182 : 8258260 : d_lastDecisionLit = next.first;
183 : : // record that we made a decision
184 : 8258260 : d_currStatusDec = true;
185 [ + + ]: 8258260 : if (d_decisionStopOnly)
186 : : {
187 : : // only doing stop-only, return undefSatLiteral.
188 : 82078 : return undefSatLiteral;
189 : : }
190 [ + + ]: 8176180 : return lastChildVal == SAT_VALUE_FALSE ? ~nsl : nsl;
191 : : }
192 : : else
193 : : {
194 : : // NOTE: it may be the case that we have yet to justify this node,
195 : : // as indicated by the return of d_jcache.lookupValue. We may have a
196 : : // value assigned to next.first by the SAT solver, but we ignore it
197 : : // here.
198 : : // (2) unprocessed non-atom, push to the stack
199 : 10086400 : d_stack.pushToStack(next.first, next.second);
200 : 10086400 : d_stats.d_maxStackSize.maxAssign(d_stack.size());
201 : : // we have yet to process children for the next node, so lastChildVal
202 : : // remains set to SAT_VALUE_UNKNOWN.
203 : : }
204 : : }
205 : : else
206 : : {
207 [ + - ]: 27575700 : Trace("jh-debug") << "in main loop, " << next.first << " has value "
208 : 13787800 : << lastChildVal << std::endl;
209 : : }
210 : : // (3) otherwise, next already has a value lastChildVal which will be
211 : : // processed in the next iteration of the loop.
212 : : }
213 [ + + ]: 43792100 : } while (d_stack.hasCurrentAssertion());
214 : : // we exhausted all assertions
215 [ + - ]: 93278 : Trace("jh-process") << "...exhausted all assertions" << std::endl;
216 : 93278 : stopSearch = true;
217 : 93278 : return undefSatLiteral;
218 : : }
219 : :
220 : 61876400 : JustifyNode JustificationStrategy::getNextJustifyNode(
221 : : JustifyInfo* ji, prop::SatValue& lastChildVal)
222 : : {
223 : : // get the node we are trying to justify and its desired value
224 : 123753000 : JustifyNode jc = ji->getNode();
225 [ - + ][ - + ]: 61876400 : Assert(!jc.first.isNull());
[ - - ]
226 [ - + ][ - + ]: 61876400 : Assert(jc.second != SAT_VALUE_UNKNOWN);
[ - - ]
227 : : // extract the non-negated formula we are trying to justify
228 : 61876400 : bool currPol = jc.first.getKind() != Kind::NOT;
229 [ + + ]: 123753000 : TNode curr = currPol ? jc.first : jc.first[0];
230 : 61876400 : Kind ck = curr.getKind();
231 : : // the current node should be a non-theory literal and not have double
232 : : // negation, due to our invariants of what is pushed onto the stack
233 [ - + ][ - + ]: 61876400 : Assert(!expr::isTheoryAtom(curr));
[ - - ]
234 [ - + ][ - + ]: 61876400 : Assert(ck != Kind::NOT);
[ - - ]
235 : : // get the next child index to process
236 : 61876400 : size_t i = ji->getNextChildIndex();
237 [ + - ]: 123753000 : Trace("jh-debug") << "getNextJustifyNode " << curr << " / " << currPol
238 : 0 : << ", index = " << i
239 : 61876400 : << ", last child value = " << lastChildVal << std::endl;
240 : : // NOTE: if i>0, we just computed the value of the (i-1)^th child
241 : : // i.e. i == 0 || lastChildVal != SAT_VALUE_UNKNOWN,
242 : : // however this does not hold when backtracking has occurred.
243 : : // if i=0, we shouldn't have a last child value
244 [ + + ][ - + ]: 61876400 : Assert(i > 0 || lastChildVal == SAT_VALUE_UNKNOWN)
[ - + ][ - - ]
245 : 0 : << "in getNextJustifyNode, value given for non-existent last child";
246 : : // we are trying to make the value of curr equal to currDesiredVal
247 [ + + ]: 61876400 : SatValue currDesiredVal = currPol ? jc.second : invertValue(jc.second);
248 : : // value is set to TRUE/FALSE if the value of curr can be determined.
249 : 61876400 : SatValue value = SAT_VALUE_UNKNOWN;
250 : : // if we require processing the next child of curr, we set desiredVal to
251 : : // value which we want that child to be to make curr's value equal to
252 : : // currDesiredVal.
253 : 61876400 : SatValue desiredVal = SAT_VALUE_UNKNOWN;
254 [ + + ][ + + ]: 61876400 : if (ck == Kind::AND || ck == Kind::OR)
255 : : {
256 [ + + ]: 31663700 : if (i == 0)
257 : : {
258 : : // See if a single child with currDesiredVal forces value, which is the
259 : : // case if ck / currDesiredVal in { and / false, or / true }.
260 [ + + ]: 18949100 : if ((ck == Kind::AND) == (currDesiredVal == SAT_VALUE_FALSE))
261 : : {
262 : : // lookahead to determine if already satisfied
263 : : // we scan only once, when processing the first child
264 [ + + ]: 75573600 : for (const Node& c : curr)
265 : : {
266 : 72465800 : SatValue v = d_jcache.lookupValue(c);
267 [ + + ]: 72465800 : if (v == currDesiredVal)
268 : : {
269 [ + - ]: 14718100 : Trace("jh-debug") << "already forcing child " << c << std::endl;
270 : 14718100 : value = currDesiredVal;
271 : 14718100 : break;
272 : : }
273 : : // NOTE: if v == SAT_VALUE_UNKNOWN, then we can add this to a watch
274 : : // list and short circuit processing in the children of this node.
275 : : }
276 : : }
277 : 18949100 : desiredVal = currDesiredVal;
278 : : }
279 [ + + ]: 8725390 : else if ((ck == Kind::AND && lastChildVal == SAT_VALUE_FALSE)
280 [ + + ][ + + ]: 12327200 : || (ck == Kind::OR && lastChildVal == SAT_VALUE_TRUE)
281 [ + + ][ + + ]: 25429200 : || i == curr.getNumChildren())
[ + + ]
282 : : {
283 [ + - ]: 4012620 : Trace("jh-debug") << "current is forcing child" << std::endl;
284 : : // forcing or exhausted case
285 : 4012620 : value = lastChildVal;
286 : : }
287 : : else
288 : : {
289 : : // otherwise, no forced value, value of child should match the parent
290 : 8702000 : desiredVal = currDesiredVal;
291 : 31663700 : }
292 : : }
293 [ + + ]: 30212700 : else if (ck == Kind::IMPLIES)
294 : : {
295 [ + + ]: 5360180 : if (i == 0)
296 : : {
297 : : // lookahead to second child to determine if value already forced
298 [ + + ]: 2808340 : if (d_jcache.lookupValue(curr[1]) == SAT_VALUE_TRUE)
299 : : {
300 : 1163850 : value = SAT_VALUE_TRUE;
301 : : }
302 : : else
303 : : {
304 : : // otherwise, we request the opposite of what parent wants
305 : 1644500 : desiredVal = invertValue(currDesiredVal);
306 : : }
307 : : }
308 [ + + ]: 2551840 : else if (i == 1)
309 : : {
310 : : // forcing case
311 [ + + ]: 1635640 : if (lastChildVal == SAT_VALUE_FALSE)
312 : : {
313 : 713001 : value = SAT_VALUE_TRUE;
314 : : }
315 : : else
316 : : {
317 : 922641 : desiredVal = currDesiredVal;
318 : : }
319 : : }
320 : : else
321 : : {
322 : : // exhausted case
323 : 916196 : value = lastChildVal;
324 : : }
325 : : }
326 [ + + ]: 24852500 : else if (ck == Kind::ITE)
327 : : {
328 [ + + ]: 4636580 : if (i == 0)
329 : : {
330 : : // lookahead on branches
331 : 1590040 : SatValue val1 = d_jcache.lookupValue(curr[1]);
332 : 1590040 : SatValue val2 = d_jcache.lookupValue(curr[2]);
333 [ + + ]: 1590040 : if (val1 == val2)
334 : : {
335 : : // branches have no difference, value is that of branches, which may
336 : : // be unknown
337 : 580950 : value = val1;
338 : : }
339 : : // if first branch is already wrong or second branch is already correct,
340 : : // try to make condition false. Note that we arbitrarily choose true here
341 : : // if both children are unknown. If both children have the same value
342 : : // and that value is not unknown, desiredVal will be ignored, since
343 : : // value is set above.
344 : 1590040 : desiredVal =
345 [ + + ]: 2723010 : (val1 == invertValue(currDesiredVal) || val2 == currDesiredVal)
346 [ + + ]: 2723010 : ? SAT_VALUE_FALSE
347 : : : SAT_VALUE_TRUE;
348 : : }
349 [ + + ]: 3046540 : else if (i == 1)
350 : : {
351 [ - + ][ - + ]: 1525970 : Assert(lastChildVal != SAT_VALUE_UNKNOWN);
[ - - ]
352 : : // we just computed the value of the condition, check if the condition
353 : : // was false
354 [ + + ]: 1525970 : if (lastChildVal == SAT_VALUE_FALSE)
355 : : {
356 : : // this increments to the else branch
357 : 665034 : i = ji->getNextChildIndex();
358 : : }
359 : : // make the branch equal to the desired value
360 : 1525970 : desiredVal = currDesiredVal;
361 : : }
362 : : else
363 : : {
364 : : // return the branch value
365 : 1520570 : value = lastChildVal;
366 : : }
367 : : }
368 [ + + ][ + - ]: 20215900 : else if (ck == Kind::XOR || ck == Kind::EQUAL)
369 : : {
370 [ - + ][ - + ]: 20215900 : Assert(curr[0].getType().isBoolean());
[ - - ]
371 [ + + ]: 20215900 : if (i == 0)
372 : : {
373 : : // check if the rhs forces a value
374 : 6808000 : SatValue val1 = d_jcache.lookupValue(curr[1]);
375 [ + + ]: 6808000 : if (val1 == SAT_VALUE_UNKNOWN)
376 : : {
377 : : // not forced, arbitrarily choose true
378 : 6124370 : desiredVal = SAT_VALUE_TRUE;
379 : : }
380 : : else
381 : : {
382 : : // if the RHS of the XOR/EQUAL already had a value val1, then:
383 : : // ck / currDesiredVal
384 : : // equal / true ... LHS should have same value as RHS
385 : : // equal / false ... LHS should have opposite value as RHS
386 : : // xor / true ... LHS should have opposite value as RHS
387 : : // xor / false ... LHS should have same value as RHS
388 : 683626 : desiredVal = ((ck == Kind::EQUAL) == (currDesiredVal == SAT_VALUE_TRUE))
389 [ + + ]: 683626 : ? val1
390 : 135312 : : invertValue(val1);
391 : : }
392 : : }
393 [ + + ]: 13407900 : else if (i == 1)
394 : : {
395 [ - + ][ - + ]: 6735940 : Assert(lastChildVal != SAT_VALUE_UNKNOWN);
[ - - ]
396 : : // same as above, choosing a value for RHS based on the value of LHS,
397 : : // which is stored in lastChildVal.
398 : 6735940 : desiredVal = ((ck == Kind::EQUAL) == (currDesiredVal == SAT_VALUE_TRUE))
399 [ + + ]: 6735940 : ? lastChildVal
400 : 5753720 : : invertValue(lastChildVal);
401 : : }
402 : : else
403 : : {
404 : : // recompute the value of the first child
405 : 6671970 : SatValue val0 = d_jcache.lookupValue(curr[0]);
406 [ - + ][ - + ]: 6671970 : Assert(val0 != SAT_VALUE_UNKNOWN);
[ - - ]
407 [ - + ][ - + ]: 6671970 : Assert(lastChildVal != SAT_VALUE_UNKNOWN);
[ - - ]
408 : : // compute the value of the equal/xor. The values for LHS/RHS are
409 : : // stored in val0 and lastChildVal.
410 : : // (val0 == lastChildVal) / ck
411 : : // true / equal ... value of curr is true
412 : : // true / xor ... value of curr is false
413 : : // false / equal ... value of curr is false
414 : : // false / xor ... value of curr is true
415 [ + + ]: 6671970 : value = ((val0 == lastChildVal) == (ck == Kind::EQUAL)) ? SAT_VALUE_TRUE
416 : : : SAT_VALUE_FALSE;
417 : 20215900 : }
418 : : }
419 : : else
420 : : {
421 : : // curr should not be an atom
422 : 0 : Assert(false);
423 : : }
424 : : // we return null if we have determined the value of the current node
425 [ + + ]: 61876400 : if (value != SAT_VALUE_UNKNOWN)
426 : : {
427 [ - + ][ - + ]: 29743800 : Assert(!expr::isTheoryAtom(curr));
[ - - ]
428 : : // add to justify if so
429 : 29743800 : d_jcache.setValue(curr, value);
430 : : // update the last child value, which will be used by the parent of the
431 : : // current node, if it exists.
432 [ + + ]: 29743800 : lastChildVal = currPol ? value : invertValue(value);
433 [ + - ]: 59487700 : Trace("jh-debug") << "getJustifyNode: return null with value "
434 : 29743800 : << lastChildVal << std::endl;
435 : : // return null, indicating there is nothing left to do for current
436 : 59487700 : return JustifyNode(TNode::null(), SAT_VALUE_UNKNOWN);
437 : : }
438 [ + - ][ - + ]: 64265100 : Trace("jh-debug") << "getJustifyNode: return " << curr[i]
[ - - ]
439 : 32132500 : << " with desired value " << desiredVal << std::endl;
440 : : // The next child should be a valid argument in curr. Otherwise, we did not
441 : : // recognize when its value could be inferred above.
442 [ - + ][ - + ]: 32132500 : Assert(i < curr.getNumChildren()) << curr.getKind() << " had no value";
[ - - ]
443 : : // should set a desired value
444 [ - + ][ - + ]: 32132500 : Assert(desiredVal != SAT_VALUE_UNKNOWN)
[ - - ]
445 : 0 : << "Child " << i << " of " << curr.getKind() << " had no desired value";
446 : : // return the justify node
447 : 32132500 : return JustifyNode(curr[i], desiredVal);
448 : : }
449 : :
450 : 93895 : bool JustificationStrategy::isDone() { return !refreshCurrentAssertion(); }
451 : :
452 : 835102 : void JustificationStrategy::addAssertions(const std::vector<TNode>& lems)
453 : : {
454 [ + - ]: 835102 : Trace("jh-assert") << "addAssertions " << lems << std::endl;
455 : 835102 : insertToAssertionList(lems, false);
456 : 835102 : }
457 : :
458 : 621142 : void JustificationStrategy::addLocalAssertions(const std::vector<TNode>& lems)
459 : : {
460 [ + - ]: 621142 : Trace("jh-assert") << "addLocalAssertions: " << lems << std::endl;
461 : 621142 : insertToAssertionList(lems, true);
462 : 621142 : }
463 : :
464 : 1456240 : void JustificationStrategy::insertToAssertionList(const std::vector<TNode>& lems,
465 : : bool local)
466 : : {
467 : 2912490 : std::vector<TNode> toProcess(lems.begin(), lems.end());
468 [ + + ]: 1456240 : AssertionList& al = local ? d_localAssertions : d_assertions;
469 [ + + ]: 1456240 : IntStat& sizeStat =
470 : : local ? d_stats.d_maxSkolemDefsSize : d_stats.d_maxAssertionsSize;
471 : : // always miniscope AND and negated OR immediately
472 : 1456240 : size_t index = 0;
473 : : // must keep some intermediate nodes below around for ref counting
474 : 2912490 : std::vector<Node> keep;
475 [ + + ]: 3114140 : while (index < toProcess.size())
476 : : {
477 : 3315790 : TNode curr = toProcess[index];
478 : 1657890 : bool pol = curr.getKind() != Kind::NOT;
479 [ + + ]: 3315790 : TNode currAtom = pol ? curr : curr[0];
480 : 1657890 : index++;
481 : 1657890 : Kind k = currAtom.getKind();
482 [ + + ][ + + ]: 1657890 : if (k == Kind::AND && pol)
483 : : {
484 : 30517 : toProcess.insert(toProcess.begin() + index, curr.begin(), curr.end());
485 : : }
486 [ + + ][ + + ]: 1627380 : else if (k == Kind::OR && !pol)
487 : : {
488 : 356 : std::vector<Node> negc;
489 [ + + ]: 5555 : for (TNode c : currAtom)
490 : : {
491 : 10398 : Node cneg = c.negate();
492 : 5199 : negc.push_back(cneg);
493 : : // ensure ref counted
494 : 5199 : keep.push_back(cneg);
495 : : }
496 : 356 : toProcess.insert(toProcess.begin() + index, negc.begin(), negc.end());
497 : : }
498 [ + + ]: 1627020 : else if (!expr::isTheoryAtom(currAtom))
499 : : {
500 : 1229570 : al.addAssertion(curr);
501 : : // take stats
502 : 1229570 : sizeStat.maxAssign(al.size());
503 : : }
504 : : else
505 : : {
506 : : // we skip (top-level) theory literals, since these are always propagated
507 : : // NOTE: skolem definitions that are always relevant should be added to
508 : : // assertions, for uniformity via a method notifyJustified(currAtom)
509 : : }
510 : : }
511 : : // clear since toProcess may contain nodes with 0 ref count after returning
512 : : // otherwise
513 : 1456240 : toProcess.clear();
514 : 1456240 : }
515 : :
516 : 28376900 : bool JustificationStrategy::refreshCurrentAssertion()
517 : : {
518 [ + - ]: 28376900 : Trace("jh-process") << "refreshCurrentAssertion" << std::endl;
519 : : // if we already have a current assertion, nothing to be done
520 : 56753800 : TNode curr = d_stack.getCurrentAssertion();
521 [ + + ]: 28376900 : if (!curr.isNull())
522 : : {
523 [ + + ][ + + ]: 8377980 : if (curr != d_currUnderStatus && !d_currUnderStatus.isNull())
[ + + ]
524 : : {
525 : 83426 : ++(d_stats.d_numStatusBacktrack);
526 : 83426 : d_assertions.notifyStatus(d_currUnderStatus, DecisionStatus::BACKTRACK);
527 : : // we've backtracked to another assertion which may be partially
528 : : // processed. don't track its status?
529 : 83426 : d_currUnderStatus = Node::null();
530 : : // NOTE: could reset the stack here to preserve other invariants,
531 : : // currently we do not.
532 : : }
533 : 8377980 : return true;
534 : : }
535 : 19998900 : bool skFirst = (d_jhSkMode != options::JutificationSkolemMode::LAST);
536 : : // use main assertions first
537 [ + + ]: 19998900 : if (refreshCurrentAssertionFromList(skFirst))
538 : : {
539 : 1165600 : return true;
540 : : }
541 : : // if satisfied all main assertions, use the skolem assertions, which may
542 : : // fail
543 : 18833300 : return refreshCurrentAssertionFromList(!skFirst);
544 : : }
545 : :
546 : 38832200 : bool JustificationStrategy::refreshCurrentAssertionFromList(bool local)
547 : : {
548 [ + + ]: 38832200 : AssertionList& al = local ? d_localAssertions : d_assertions;
549 : 38832200 : bool doWatchStatus = !local;
550 : 38832200 : d_currUnderStatus = Node::null();
551 : 77664500 : TNode curr = al.getNextAssertion();
552 : : SatValue currValue;
553 [ + + ]: 39045300 : while (!curr.isNull())
554 : : {
555 [ + - ]: 20083900 : Trace("jh-process") << "Check assertion " << curr << std::endl;
556 : : // we never add theory literals to our assertions lists
557 [ - + ][ - + ]: 20083900 : Assert(!isTheoryLiteral(curr));
[ - - ]
558 : 20083900 : currValue = d_jcache.lookupValue(curr);
559 [ + + ]: 20083900 : if (currValue == SAT_VALUE_UNKNOWN)
560 : : {
561 : : // if not already justified, we reset the stack and push to it
562 : 19870800 : d_stack.reset(curr);
563 : 19870800 : d_lastDecisionLit = TNode::null();
564 : : // for activity
565 [ + + ]: 19870800 : if (doWatchStatus)
566 : : {
567 : : // initially, mark that we have not found a decision in this
568 : 18705200 : d_currUnderStatus = d_stack.getCurrentAssertion();
569 : 18705200 : d_currStatusDec = false;
570 : : }
571 : 19870800 : return true;
572 : : }
573 : : // assertions should all be satisfied, otherwise we are in conflict
574 [ - + ][ - + ]: 213024 : Assert(currValue == SAT_VALUE_TRUE);
[ - - ]
575 [ + + ]: 213024 : if (doWatchStatus)
576 : : {
577 : : // mark that we did not find a decision in it
578 : 212766 : ++(d_stats.d_numStatusNoDecision);
579 : 212766 : d_assertions.notifyStatus(curr, DecisionStatus::NO_DECISION);
580 : : }
581 : : // already justified, immediately skip
582 : 213024 : curr = al.getNextAssertion();
583 : : }
584 : 18961400 : return false;
585 : : }
586 : :
587 : 20083900 : bool JustificationStrategy::isTheoryLiteral(TNode n)
588 : : {
589 [ + + ]: 20083900 : return expr::isTheoryAtom(n.getKind() == Kind::NOT ? n[0] : n);
590 : : }
591 : :
592 : : } // namespace decision
593 : : } // namespace cvc5::internal
|
