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