GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/decision/justification_heuristic.cpp Lines: 278 382 72.8 %
Date: 2021-03-22 Branches: 485 1507 32.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file justification_heuristic.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Kshitij Bansal, Andres Noetzli, Gereon Kremer
6
 ** This file is part of the CVC4 project.
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.\endverbatim
11
 **
12
 ** \brief Justification heuristic for decision making
13
 **
14
 ** A ATGP-inspired justification-based decision heuristic. This code is based
15
 ** on the CVC3 implementation of the same heuristic -- note below.
16
 **
17
 ** It needs access to the simplified but non-clausal formula.
18
 **/
19
#include "justification_heuristic.h"
20
21
#include "decision/decision_attributes.h"
22
#include "decision/decision_engine.h"
23
#include "expr/kind.h"
24
#include "expr/node_manager.h"
25
#include "options/decision_options.h"
26
#include "smt/smt_statistics_registry.h"
27
#include "smt/term_formula_removal.h"
28
#include "theory/rewriter.h"
29
#include "util/random.h"
30
31
namespace CVC4 {
32
namespace decision {
33
34
6490
JustificationHeuristic::JustificationHeuristic(CVC4::DecisionEngine* de,
35
                                               context::UserContext* uc,
36
6490
                                               context::Context* c)
37
    : ITEDecisionStrategy(de, c),
38
      d_justified(c),
39
      d_exploredThreshold(c),
40
      d_prvsIndex(c, 0),
41
      d_threshPrvsIndex(c, 0),
42
      d_helpfulness("decision::jh::helpfulness", 0),
43
      d_giveup("decision::jh::giveup", 0),
44
      d_timestat("decision::jh::time"),
45
      d_assertions(uc),
46
      d_skolemAssertions(uc),
47
      d_skolemCache(uc),
48
      d_visited(),
49
      d_visitedComputeSkolems(),
50
      d_curDecision(),
51
      d_curThreshold(0),
52
      d_childCache(uc),
53
      d_weightCache(uc),
54
6490
      d_startIndexCache(c)
55
{
56
6490
  smtStatisticsRegistry()->registerStat(&d_helpfulness);
57
6490
  smtStatisticsRegistry()->registerStat(&d_giveup);
58
6490
  smtStatisticsRegistry()->registerStat(&d_timestat);
59
6490
  Trace("decision") << "Justification heuristic enabled" << std::endl;
60
6490
}
61
62
19467
JustificationHeuristic::~JustificationHeuristic()
63
{
64
6489
  smtStatisticsRegistry()->unregisterStat(&d_helpfulness);
65
6489
  smtStatisticsRegistry()->unregisterStat(&d_giveup);
66
6489
  smtStatisticsRegistry()->unregisterStat(&d_timestat);
67
12978
}
68
69
671375
CVC4::prop::SatLiteral JustificationHeuristic::getNext(bool &stopSearch)
70
{
71
1414855
  if(options::decisionThreshold() > 0) {
72
    bool stopSearchTmp = false;
73
    prop::SatLiteral lit =
74
        getNextThresh(stopSearchTmp, options::decisionThreshold());
75
    if (lit != prop::undefSatLiteral)
76
    {
77
      Assert(stopSearchTmp == false);
78
      return lit;
79
    }
80
    Assert(stopSearchTmp == true);
81
  }
82
671375
  return getNextThresh(stopSearch, 0);
83
}
84
85
671375
CVC4::prop::SatLiteral JustificationHeuristic::getNextThresh(bool &stopSearch, DecisionWeight threshold) {
86
671375
  Trace("decision") << "JustificationHeuristic::getNextThresh(stopSearch, "<<threshold<<")" << std::endl;
87
1342750
  TimerStat::CodeTimer codeTimer(d_timestat);
88
89
671375
  d_visited.clear();
90
671375
  d_curThreshold = threshold;
91
92
671375
  if(Trace.isOn("justified")) {
93
    for(JustifiedSet::key_iterator i = d_justified.key_begin();
94
        i != d_justified.key_end(); ++i) {
95
      TNode n = *i;
96
      prop::SatLiteral l = d_decisionEngine->hasSatLiteral(n)
97
                               ? d_decisionEngine->getSatLiteral(n)
98
                               : -1;
99
      prop::SatValue v = tryGetSatValue(n);
100
      Trace("justified") <<"{ "<<l<<"}" << n <<": "<<v << std::endl;
101
    }
102
  }
103
104
7606917
  for(unsigned i = getPrvsIndex(); i < d_assertions.size(); ++i) {
105
7567762
    Debug("decision") << "---" << std::endl << d_assertions[i] << std::endl;
106
107
    // Sanity check: if it was false, aren't we inconsistent?
108
    // Commenting out. See bug 374. In short, to do with how CNF stream works.
109
    // Assert( tryGetSatValue(d_assertions[i]) != SAT_VALUE_FALSE);
110
111
7567762
    prop::SatValue desiredVal = prop::SAT_VALUE_TRUE;
112
7567762
    prop::SatLiteral litDecision;
113
114
7567762
    litDecision = findSplitter(d_assertions[i], desiredVal);
115
116
7567762
    if (litDecision != prop::undefSatLiteral)
117
    {
118
632220
      setPrvsIndex(i);
119
632220
      Trace("decision") << "jh: splitting on " << litDecision << std::endl;
120
632220
      ++d_helpfulness;
121
632220
      return litDecision;
122
    }
123
  }
124
125
39155
  Trace("decision") << "jh: Nothing to split on " << std::endl;
126
127
#if defined CVC4_DEBUG
128
39155
  bool alljustified = true;
129
6054298
  for(unsigned i = 0 ; i < d_assertions.size() && alljustified ; ++i) {
130
12030286
    TNode curass = d_assertions[i];
131
6216017
    while(curass.getKind() == kind::NOT)
132
100437
      curass = curass[0];
133
6015143
    alljustified &= checkJustified(curass);
134
135
6015143
    if(Debug.isOn("decision")) {
136
      if(!checkJustified(curass))
137
        Debug("decision") << "****** Not justified [i="<<i<<"]: "
138
                          << d_assertions[i] << std::endl;
139
    }
140
  }
141
39155
  Assert(alljustified || d_curThreshold != 0);
142
#endif
143
144
  // SAT solver can stop...
145
39155
  stopSearch = true;
146
39155
  if (d_curThreshold == 0) d_decisionEngine->setResult(prop::SAT_VALUE_TRUE);
147
39155
  return prop::undefSatLiteral;
148
}
149
150
246285
inline void computeXorIffDesiredValues(Kind k,
151
                                       prop::SatValue desiredVal,
152
                                       prop::SatValue& desiredVal1,
153
                                       prop::SatValue& desiredVal2)
154
{
155
246285
  Assert(k == kind::EQUAL || k == kind::XOR);
156
157
246285
  bool shouldInvert =
158
219063
      (desiredVal == prop::SAT_VALUE_TRUE && k == kind::EQUAL)
159
285573
      || (desiredVal == prop::SAT_VALUE_FALSE && k == kind::XOR);
160
161
246285
  if (desiredVal1 == prop::SAT_VALUE_UNKNOWN
162
43594
      && desiredVal2 == prop::SAT_VALUE_UNKNOWN)
163
  {
164
    // CHOICE: pick one of them arbitarily
165
38968
    desiredVal1 = prop::SAT_VALUE_FALSE;
166
  }
167
168
246285
  if(desiredVal2 == SAT_VALUE_UNKNOWN) {
169
46447
    desiredVal2 = shouldInvert ? invertValue(desiredVal1) : desiredVal1;
170
199838
  } else if(desiredVal1 == SAT_VALUE_UNKNOWN) {
171
4626
    desiredVal1 = shouldInvert ? invertValue(desiredVal2) : desiredVal2;
172
  }
173
246285
}
174
175
257064
void JustificationHeuristic::addAssertion(TNode assertion)
176
{
177
  // Save all assertions locally, including the assertions generated by term
178
  // removal. We have to make sure that we assign a value to all the Boolean
179
  // term variables. To illustrate why this is, consider the case where we have
180
  // a single assertion
181
  //
182
  // (or (f a) (f b))
183
  //
184
  // where `f` is a function `Bool -> Bool`. Given an assignment:
185
  //
186
  // (f a) -> true
187
  // (f b) -> false
188
  // a -> false
189
  //
190
  // UF will not complain and the justification heuristic considers the
191
  // assertion to be satisifed. However, we also have to make sure that we pick
192
  // a value for `b` that is not in conflict with the other assignments (we can
193
  // only choose `b` to be `true` otherwise the model is incorrect).
194
257064
  d_assertions.push_back(assertion);
195
257064
}
196
197
20634
void JustificationHeuristic::addSkolemDefinition(TNode lem, TNode skolem)
198
{
199
41268
  Trace("decision::jh::ite")
200
20634
      << " jh-ite: " << skolem << " maps to " << lem << std::endl;
201
20634
  d_skolemAssertions[skolem] = lem;
202
20634
}
203
204
7567762
SatLiteral JustificationHeuristic::findSplitter(TNode node,
205
                                                SatValue desiredVal)
206
{
207
7567762
  d_curDecision = undefSatLiteral;
208
7567762
  findSplitterRec(node, desiredVal);
209
7567762
  return d_curDecision;
210
}
211
212
213
11490034
void JustificationHeuristic::setJustified(TNode n)
214
{
215
11490034
  d_justified.insert(n);
216
11490034
}
217
218
25148337
bool JustificationHeuristic::checkJustified(TNode n)
219
{
220
25148337
  return d_justified.find(n) != d_justified.end();
221
}
222
223
13719462
DecisionWeight JustificationHeuristic::getExploredThreshold(TNode n)
224
{
225
27438924
  return d_exploredThreshold.find(n) == d_exploredThreshold.end()
226
13719462
             ? std::numeric_limits<DecisionWeight>::max()
227
27438924
             : d_exploredThreshold[n];
228
}
229
230
void JustificationHeuristic::setExploredThreshold(TNode n)
231
{
232
  d_exploredThreshold[n] = d_curThreshold;
233
}
234
235
671375
int JustificationHeuristic::getPrvsIndex()
236
{
237
671375
  if(d_curThreshold == 0)
238
671375
    return d_prvsIndex;
239
  else
240
    return d_threshPrvsIndex;
241
}
242
243
632220
void JustificationHeuristic::setPrvsIndex(int prvsIndex)
244
{
245
632220
  if(d_curThreshold == 0)
246
632220
    d_prvsIndex = prvsIndex;
247
  else
248
    d_threshPrvsIndex = prvsIndex;
249
632220
}
250
251
DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, SatValue satValue)
252
{
253
  Assert(satValue == SAT_VALUE_TRUE || satValue == SAT_VALUE_FALSE);
254
  return getWeightPolarized(n, satValue == SAT_VALUE_TRUE);
255
}
256
257
DecisionWeight JustificationHeuristic::getWeightPolarized(TNode n, bool polarity)
258
{
259
  if (options::decisionWeightInternal()
260
      != options::DecisionWeightInternal::USR1)
261
  {
262
    return getWeight(n);
263
  }
264
265
  if(d_weightCache.find(n) == d_weightCache.end()) {
266
    Kind k = n.getKind();
267
    theory::TheoryId tId  = theory::kindToTheoryId(k);
268
    DecisionWeight dW1, dW2;
269
    if(tId != theory::THEORY_BOOL) {
270
      dW1 = dW2 = getWeight(n);
271
    } else {
272
273
      if(k == kind::OR) {
274
        dW1 = std::numeric_limits<DecisionWeight>::max(), dW2 = 0;
275
        for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
276
          dW1 = std::min(dW1, getWeightPolarized(*i, true));
277
          dW2 = std::max(dW2, getWeightPolarized(*i, false));
278
        }
279
      } else if(k == kind::AND) {
280
        dW1 = 0, dW2 = std::numeric_limits<DecisionWeight>::max();
281
        for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
282
          dW1 = std::max(dW1, getWeightPolarized(*i, true));
283
          dW2 = std::min(dW2, getWeightPolarized(*i, false));
284
        }
285
      } else if(k == kind::IMPLIES) {
286
        dW1 = std::min(getWeightPolarized(n[0], false),
287
                       getWeightPolarized(n[1], true));
288
        dW2 = std::max(getWeightPolarized(n[0], true),
289
                       getWeightPolarized(n[1], false));
290
      } else if(k == kind::NOT) {
291
        dW1 = getWeightPolarized(n[0], false);
292
        dW2 = getWeightPolarized(n[0], true);
293
      } else {
294
        dW1 = 0;
295
        for(TNode::iterator i=n.begin(); i != n.end(); ++i) {
296
          dW1 = std::max(dW1, getWeightPolarized(*i, true));
297
          dW1 = std::max(dW1, getWeightPolarized(*i, false));
298
        }
299
        dW2 = dW1;
300
      }
301
302
    }
303
24006
    d_weightCache[n] = std::make_pair(dW1, dW2);
304
  }
305
  return polarity ? d_weightCache[n].get().first : d_weightCache[n].get().second;
306
}
307
308
DecisionWeight JustificationHeuristic::getWeight(TNode n) {
309
  if(!n.hasAttribute(DecisionWeightAttr()) ) {
310
    options::DecisionWeightInternal combiningFn =
311
        options::decisionWeightInternal();
312
313
    if (combiningFn == options::DecisionWeightInternal::OFF
314
        || n.getNumChildren() == 0)
315
    {
316
      if (options::decisionRandomWeight() != 0)
317
      {
318
        n.setAttribute(DecisionWeightAttr(),
319
            Random::getRandom().pick(0, options::decisionRandomWeight()-1));
320
      }
321
    }
322
    else if (combiningFn == options::DecisionWeightInternal::MAX)
323
    {
324
      DecisionWeight dW = 0;
325
      for (TNode::iterator i = n.begin(); i != n.end(); ++i)
326
        dW = std::max(dW, getWeight(*i));
327
      n.setAttribute(DecisionWeightAttr(), dW);
328
    }
329
    else if (combiningFn == options::DecisionWeightInternal::SUM
330
             || combiningFn == options::DecisionWeightInternal::USR1)
331
    {
332
      DecisionWeight dW = 0;
333
      for (TNode::iterator i = n.begin(); i != n.end(); ++i)
334
        dW = std::max(dW, getWeight(*i));
335
      n.setAttribute(DecisionWeightAttr(), dW);
336
    }
337
    else
338
    {
339
      Unreachable();
340
    }
341
  }
342
  return n.getAttribute(DecisionWeightAttr());
343
}
344
345
typedef std::vector<TNode> ChildList;
346
11338476
TNode JustificationHeuristic::getChildByWeight(TNode n, int i, bool polarity) {
347
24377264
  if(options::decisionUseWeight()) {
348
    // TODO: Optimize storing & access
349
    if(d_childCache.find(n) == d_childCache.end()) {
350
      ChildList list0(n.begin(), n.end()), list1(n.begin(), n.end());
351
      std::sort(list0.begin(), list0.end(), JustificationHeuristic::myCompareClass(this,false));
352
      std::sort(list1.begin(), list1.end(), JustificationHeuristic::myCompareClass(this,true));
353
      d_childCache[n] = make_pair(list0, list1);
354
    }
355
    return polarity ? d_childCache[n].get().second[i] : d_childCache[n].get().first[i];
356
  } else {
357
11338476
    return n[i];
358
  }
359
}
360
361
25895632
SatValue JustificationHeuristic::tryGetSatValue(Node n)
362
{
363
25895632
  Debug("decision") << "   "  << n << " has sat value " << " ";
364
25895632
  if(d_decisionEngine->hasSatLiteral(n) ) {
365
19466018
    Debug("decision") << d_decisionEngine->getSatValue(n) << std::endl;
366
19466018
    return d_decisionEngine->getSatValue(n);
367
  } else {
368
6429614
    Debug("decision") << "NO SAT LITERAL" << std::endl;
369
6429614
    return SAT_VALUE_UNKNOWN;
370
  }//end of else
371
}
372
373
5290502
JustificationHeuristic::SkolemList JustificationHeuristic::getSkolems(TNode n)
374
{
375
5290502
  SkolemCache::iterator it = d_skolemCache.find(n);
376
5290502
  if (it != d_skolemCache.end())
377
  {
378
5019715
    return (*it).second;
379
  }
380
  else
381
  {
382
    // Compute the list of Skolems
383
    // TODO: optimize by avoiding multiple lookup for d_skolemCache[n]
384
270787
    d_visitedComputeSkolems.clear();
385
541574
    SkolemList ilist;
386
270787
    computeSkolems(n, ilist);
387
270787
    d_skolemCache.insert(n, ilist);
388
270787
    return ilist;
389
  }
390
}
391
392
1894586
void JustificationHeuristic::computeSkolems(TNode n, SkolemList& l)
393
{
394
1894586
  Trace("decision::jh::skolems") << " computeSkolems( " << n << ", &l)\n";
395
1894586
  d_visitedComputeSkolems.insert(n);
396
3933646
  for(unsigned i=0; i<n.getNumChildren(); ++i) {
397
2039060
    SkolemMap::iterator it2 = d_skolemAssertions.find(n[i]);
398
2039060
    if (it2 != d_skolemAssertions.end())
399
    {
400
59694
      l.push_back(std::make_pair(n[i], (*it2).second));
401
59694
      Assert(n[i].getNumChildren() == 0);
402
    }
403
2039060
    if (d_visitedComputeSkolems.find(n[i]) == d_visitedComputeSkolems.end())
404
    {
405
1623799
      computeSkolems(n[i], l);
406
    }
407
  }
408
1894586
}
409
410
JustificationHeuristic::SearchResult
411
19133194
JustificationHeuristic::findSplitterRec(TNode node, SatValue desiredVal)
412
{
413
  /**
414
   * Main idea
415
   *
416
   * Given a boolean formula "node", the goal is to try to make it
417
   * evaluate to "desiredVal" (true/false). for instance if "node" is a OR
418
   * formula we want to make it evaluate to true, we'd like one of the
419
   * children to be true. this is done recursively.
420
   */
421
422
38266388
  Trace("decision::jh")
423
19133194
    << "findSplitterRec(" << node << ", "
424
19133194
    << desiredVal << ", .. )" << std::endl;
425
426
  /* Handle NOT as a special case */
427
27568438
  while (node.getKind() == kind::NOT) {
428
4217622
    desiredVal = invertValue(desiredVal);
429
4217622
    node = node[0];
430
  }
431
432
  /* Base case */
433
19133194
  if (checkJustified(node)) {
434
5413732
    Debug("decision::jh") << "  justified, returning" << std::endl;
435
5413732
    return NO_SPLITTER;
436
  }
437
13719462
  if (getExploredThreshold(node) < d_curThreshold) {
438
    Debug("decision::jh") << "  explored, returning" << std::endl;
439
    Assert(d_curThreshold != 0);
440
    return DONT_KNOW;
441
  }
442
443
#if defined CVC4_ASSERTIONS || defined CVC4_DEBUG
444
  // We don't always have a sat literal, so remember that. Will need
445
  // it for some assertions we make.
446
13719462
  bool litPresent = d_decisionEngine->hasSatLiteral(node);
447
13719462
  if(Debug.isOn("decision")) {
448
    if(!litPresent) {
449
      Debug("decision") << "no sat literal for this node" << std::endl;
450
    }
451
  }
452
#endif
453
454
  // Get value of sat literal for the node, if there is one
455
13719462
  SatValue litVal = tryGetSatValue(node);
456
457
  /* You'd better know what you want */
458
13719462
  Assert(desiredVal != SAT_VALUE_UNKNOWN) << "expected known value";
459
460
  /* Good luck, hope you can get what you want */
461
  // See bug 374
462
  // Assert(litVal == desiredVal || litVal == SAT_VALUE_UNKNOWN) <<
463
  //       "invariant violated";
464
465
  /* What type of node is this */
466
13719462
  Kind k = node.getKind();
467
13719462
  theory::TheoryId tId = theory::kindToTheoryId(k);
468
  bool isAtom =
469
32711275
     (k == kind::BOOLEAN_TERM_VARIABLE ) ||
470
19199943
     ( (tId != theory::THEORY_BOOL) &&
471
22283950
       (k != kind::EQUAL || (!node[0].getType().isBoolean())) );
472
473
  /* Some debugging stuff */
474
27438924
  Debug("decision::jh") << "kind = " << k << std::endl
475
13719462
                        << "theoryId = " << tId << std::endl
476
13719462
                        << "node = " << node << std::endl
477
13719462
                        << "litVal = " << litVal << std::endl;
478
479
  /**
480
   * If not in theory of booleans, check if this is something to split-on.
481
   */
482
13719462
  if(isAtom) {
483
    // if node has embedded skolems due to term removal, resolve that first
484
5290502
    if (handleEmbeddedSkolems(node) == FOUND_SPLITTER) return FOUND_SPLITTER;
485
486
5195735
    if(litVal != SAT_VALUE_UNKNOWN) {
487
4563515
      Assert(litVal == desiredVal);
488
4563515
      setJustified(node);
489
4563515
      return NO_SPLITTER;
490
    }
491
    else {
492
632220
      Assert(d_decisionEngine->hasSatLiteral(node));
493
632220
      if(d_curThreshold != 0 && getWeightPolarized(node, desiredVal) >= d_curThreshold)
494
        return DONT_KNOW;
495
      SatVariable v =
496
632220
        d_decisionEngine->getSatLiteral(node).getSatVariable();
497
632220
      d_curDecision = SatLiteral(v, /* negated = */ desiredVal != SAT_VALUE_TRUE );
498
1264440
      Trace("decision-node") << "[decision-node] requesting split on " << d_curDecision
499
632220
                             << ", node: " << node
500
632220
                             << ", polarity: " << (desiredVal == SAT_VALUE_TRUE ? "true" : "false") << std::endl;
501
632220
      return FOUND_SPLITTER;
502
    }
503
  }
504
505
8428960
  SearchResult ret = NO_SPLITTER;
506
8428960
  switch (k) {
507
508
17498
  case kind::CONST_BOOLEAN:
509
17498
    Assert(node.getConst<bool>() == false || desiredVal == SAT_VALUE_TRUE);
510
17498
    Assert(node.getConst<bool>() == true || desiredVal == SAT_VALUE_FALSE);
511
17498
    break;
512
513
1630352
  case kind::AND:
514
1630352
    if (desiredVal == SAT_VALUE_FALSE)
515
837299
      ret = handleAndOrEasy(node, desiredVal);
516
    else
517
793053
      ret = handleAndOrHard(node, desiredVal);
518
1630352
    break;
519
520
4739194
  case kind::OR:
521
4739194
    if (desiredVal == SAT_VALUE_FALSE)
522
82334
      ret = handleAndOrHard(node, desiredVal);
523
    else
524
4656860
      ret = handleAndOrEasy(node, desiredVal);
525
4739194
    break;
526
527
1294853
  case kind::IMPLIES:
528
1294853
    if (desiredVal == SAT_VALUE_FALSE)
529
202783
      ret = handleBinaryHard(node[0], SAT_VALUE_TRUE,
530
                             node[1], SAT_VALUE_FALSE);
531
532
    else
533
1092070
      ret = handleBinaryEasy(node[0], SAT_VALUE_FALSE,
534
                             node[1], SAT_VALUE_TRUE);
535
1294853
    break;
536
537
246285
  case kind::XOR:
538
  case kind::EQUAL: {
539
246285
    SatValue desiredVal1 = tryGetSatValue(node[0]);
540
246285
    SatValue desiredVal2 = tryGetSatValue(node[1]);
541
246285
    computeXorIffDesiredValues(k, desiredVal, desiredVal1, desiredVal2);
542
246285
    ret = handleBinaryHard(node[0], desiredVal1,
543
                           node[1], desiredVal2);
544
246285
    break;
545
  }
546
547
500778
  case kind::ITE:
548
500778
    ret = handleITE(node, desiredVal);
549
500778
    break;
550
551
  default: Assert(false) << "Unexpected Boolean operator"; break;
552
  }//end of switch(k)
553
554
8428960
  if(ret == DONT_KNOW) {
555
    setExploredThreshold(node);
556
  }
557
558
8428960
  if(ret == NO_SPLITTER) {
559
6926519
    Assert(litPresent == false || litVal == desiredVal)
560
        << "Output should be justified";
561
6926519
    setJustified(node);
562
  }
563
8428960
  return ret;
564
}/* findRecSplit method */
565
566
JustificationHeuristic::SearchResult
567
5494159
JustificationHeuristic::handleAndOrEasy(TNode node, SatValue desiredVal)
568
{
569
5494159
  Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_FALSE)
570
         or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_TRUE));
571
572
5494159
  int numChildren = node.getNumChildren();
573
5494159
  SatValue desiredValInverted = invertValue(desiredVal);
574
9048824
  for(int i = 0; i < numChildren; ++i) {
575
12603489
    TNode curNode = getChildByWeight(node, i, desiredVal);
576
9048824
    if ( tryGetSatValue(curNode) != desiredValInverted ) {
577
5494159
      SearchResult ret = findSplitterRec(curNode, desiredVal);
578
5494159
      if(ret != DONT_KNOW) {
579
5494159
        return ret;
580
      }
581
    }
582
  }
583
  Assert(d_curThreshold != 0) << "handleAndOrEasy: No controlling input found";
584
  return DONT_KNOW;
585
}
586
587
875387
int JustificationHeuristic::getStartIndex(TNode node) {
588
875387
  return d_startIndexCache[node];
589
}
590
87031
void JustificationHeuristic::saveStartIndex(TNode node, int val) {
591
87031
  d_startIndexCache[node] = val;
592
87031
}
593
594
875387
JustificationHeuristic::SearchResult JustificationHeuristic::handleAndOrHard(TNode node,
595
                                             SatValue desiredVal) {
596
875387
  Assert((node.getKind() == kind::AND and desiredVal == SAT_VALUE_TRUE)
597
         or (node.getKind() == kind::OR and desiredVal == SAT_VALUE_FALSE));
598
599
875387
  int numChildren = node.getNumChildren();
600
875387
  bool noSplitter = true;
601
875387
  int i_st = getStartIndex(node);
602
2845478
  for(int i = i_st; i < numChildren; ++i) {
603
4259743
    TNode curNode = getChildByWeight(node, i, desiredVal);
604
2289652
    SearchResult ret = findSplitterRec(curNode, desiredVal);
605
2289652
    if (ret == FOUND_SPLITTER) {
606
319561
      if(i != i_st) saveStartIndex(node, i);
607
319561
      return FOUND_SPLITTER;
608
    }
609
1970091
    noSplitter = noSplitter && (ret == NO_SPLITTER);
610
  }
611
555826
  return noSplitter ? NO_SPLITTER : DONT_KNOW;
612
}
613
614
1092070
JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryEasy(TNode node1,
615
                                              SatValue desiredVal1,
616
                                              TNode node2,
617
                                              SatValue desiredVal2)
618
{
619
2184140
  if(options::decisionUseWeight() &&
620
1092070
     getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
621
    std::swap(node1, node2);
622
    std::swap(desiredVal1, desiredVal2);
623
  }
624
625
1092070
  if ( tryGetSatValue(node1) != invertValue(desiredVal1) ) {
626
237586
    SearchResult ret = findSplitterRec(node1, desiredVal1);
627
237586
    if(ret != DONT_KNOW)
628
237586
      return ret;
629
  }
630
854484
  if ( tryGetSatValue(node2) != invertValue(desiredVal2) ) {
631
854484
    SearchResult ret = findSplitterRec(node2, desiredVal2);
632
854484
    if(ret != DONT_KNOW)
633
854484
      return ret;
634
  }
635
  Assert(d_curThreshold != 0) << "handleBinaryEasy: No controlling input found";
636
  return DONT_KNOW;
637
}
638
639
449068
JustificationHeuristic::SearchResult JustificationHeuristic::handleBinaryHard(TNode node1,
640
                                              SatValue desiredVal1,
641
                                              TNode node2,
642
                                              SatValue desiredVal2)
643
{
644
898136
  if(options::decisionUseWeight() &&
645
449068
     getWeightPolarized(node1, desiredVal1) > getWeightPolarized(node2, desiredVal2)) {
646
    std::swap(node1, node2);
647
    std::swap(desiredVal1, desiredVal2);
648
  }
649
650
449068
  bool noSplitter = true;
651
  SearchResult ret;
652
653
449068
  ret = findSplitterRec(node1, desiredVal1);
654
449068
  if (ret == FOUND_SPLITTER)
655
56224
    return FOUND_SPLITTER;
656
392844
  noSplitter &= (ret == NO_SPLITTER);
657
658
392844
  ret = findSplitterRec(node2, desiredVal2);
659
392844
  if (ret == FOUND_SPLITTER)
660
197741
    return FOUND_SPLITTER;
661
195103
  noSplitter &= (ret == NO_SPLITTER);
662
663
195103
  return noSplitter ? NO_SPLITTER : DONT_KNOW;
664
}
665
666
500778
JustificationHeuristic::SearchResult JustificationHeuristic::handleITE(TNode node, SatValue desiredVal)
667
{
668
1001556
  Debug("decision::jh") << " handleITE (" << node << ", "
669
500778
                              << desiredVal << std::endl;
670
671
  //[0]: if, [1]: then, [2]: else
672
500778
  SatValue ifVal = tryGetSatValue(node[0]);
673
500778
  if (ifVal == SAT_VALUE_UNKNOWN) {
674
93722
    SatValue trueChildVal = tryGetSatValue(node[1]);
675
93722
    SatValue falseChildVal = tryGetSatValue(node[2]);
676
    SatValue ifDesiredVal;
677
678
93722
    if(trueChildVal == desiredVal || falseChildVal == invertValue(desiredVal)) {
679
3500
      ifDesiredVal = SAT_VALUE_TRUE;
680
269881
    } else if(trueChildVal == invertValue(desiredVal) ||
681
270666
              falseChildVal == desiredVal ||
682
87069
              (options::decisionUseWeight() &&
683
90222
               getWeightPolarized(node[1], true) > getWeightPolarized(node[2], false))
684
              ) {
685
3153
      ifDesiredVal = SAT_VALUE_FALSE;
686
    } else {
687
87069
      ifDesiredVal = SAT_VALUE_TRUE;
688
    }
689
690
93722
    if(findSplitterRec(node[0], ifDesiredVal) == FOUND_SPLITTER)
691
93722
      return FOUND_SPLITTER;
692
693
    Assert(d_curThreshold != 0) << "No controlling input found (6)";
694
    return DONT_KNOW;
695
  } else {
696
    // Try to justify 'if'
697
407056
    if(findSplitterRec(node[0], ifVal) == FOUND_SPLITTER)
698
17060
      return FOUND_SPLITTER;
699
700
    // If that was successful, we need to go into only one of 'then'
701
    // or 'else'
702
389996
    int ch = (ifVal == SAT_VALUE_TRUE) ? 1 : 2;
703
704
389996
    if( findSplitterRec(node[ch], desiredVal) == FOUND_SPLITTER ) {
705
16538
      return FOUND_SPLITTER;
706
    }
707
708
373458
    return NO_SPLITTER;
709
  }// else (...ifVal...)
710
}
711
712
JustificationHeuristic::SearchResult
713
5290502
JustificationHeuristic::handleEmbeddedSkolems(TNode node)
714
{
715
10581004
  const SkolemList l = getSkolems(node);
716
5290502
  Trace("decision::jh::skolems") << " skolems size = " << l.size() << std::endl;
717
718
5290502
  bool noSplitter = true;
719
6399547
  for (SkolemList::const_iterator i = l.begin(); i != l.end(); ++i)
720
  {
721
1203812
    if(d_visited.find((*i).first) == d_visited.end()) {
722
956865
      d_visited.insert((*i).first);
723
956865
      SearchResult ret = findSplitterRec((*i).second, SAT_VALUE_TRUE);
724
956865
      if (ret == FOUND_SPLITTER)
725
94767
        return FOUND_SPLITTER;
726
862098
      noSplitter = noSplitter && (ret == NO_SPLITTER);
727
862098
      d_visited.erase((*i).first);
728
    }
729
  }
730
5195735
  return noSplitter ? NO_SPLITTER : DONT_KNOW;
731
}
732
733
} /* namespace decision */
734
26676
} /* namespace CVC4 */