GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/prop_engine.cpp Lines: 217 301 72.1 %
Date: 2021-03-22 Branches: 308 1038 29.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file prop_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Morgan Deters
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 Implementation of the propositional engine of CVC4
13
 **
14
 ** Implementation of the propositional engine of CVC4.
15
 **/
16
17
#include "prop/prop_engine.h"
18
19
#include <iomanip>
20
#include <map>
21
#include <utility>
22
23
#include "base/check.h"
24
#include "base/output.h"
25
#include "decision/decision_engine.h"
26
#include "options/base_options.h"
27
#include "options/decision_options.h"
28
#include "options/main_options.h"
29
#include "options/options.h"
30
#include "options/proof_options.h"
31
#include "options/smt_options.h"
32
#include "proof/proof_manager.h"
33
#include "prop/cnf_stream.h"
34
#include "prop/minisat/minisat.h"
35
#include "prop/prop_proof_manager.h"
36
#include "prop/sat_solver.h"
37
#include "prop/sat_solver_factory.h"
38
#include "prop/theory_proxy.h"
39
#include "smt/smt_statistics_registry.h"
40
#include "theory/output_channel.h"
41
#include "theory/theory_engine.h"
42
#include "util/resource_manager.h"
43
#include "util/result.h"
44
45
namespace CVC4 {
46
namespace prop {
47
48
/** Keeps a boolean flag scoped */
49
class ScopedBool {
50
51
private:
52
53
  bool d_original;
54
  bool& d_reference;
55
56
public:
57
58
12420
  ScopedBool(bool& reference) :
59
12420
    d_reference(reference) {
60
12420
    d_original = reference;
61
12420
  }
62
63
24840
  ~ScopedBool() {
64
12420
    d_reference = d_original;
65
12420
  }
66
};
67
68
9027
PropEngine::PropEngine(TheoryEngine* te,
69
                       context::Context* satContext,
70
                       context::UserContext* userContext,
71
                       ResourceManager* rm,
72
                       OutputManager& outMgr,
73
9027
                       ProofNodeManager* pnm)
74
    : d_inCheckSat(false),
75
      d_theoryEngine(te),
76
      d_context(satContext),
77
      d_theoryProxy(nullptr),
78
      d_satSolver(nullptr),
79
      d_pnm(pnm),
80
      d_cnfStream(nullptr),
81
      d_pfCnfStream(nullptr),
82
      d_ppm(nullptr),
83
      d_interrupted(false),
84
      d_resourceManager(rm),
85
9027
      d_outMgr(outMgr)
86
{
87
9027
  Debug("prop") << "Constructing the PropEngine" << std::endl;
88
89
9027
  d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
90
9027
  d_decisionEngine->init();  // enable appropriate strategies
91
92
9027
  d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
93
94
  // CNF stream and theory proxy required pointers to each other, make the
95
  // theory proxy first
96
9027
  d_theoryProxy = new TheoryProxy(this,
97
                                  d_theoryEngine,
98
9027
                                  d_decisionEngine.get(),
99
                                  satContext,
100
                                  userContext,
101
9027
                                  pnm);
102
27081
  d_cnfStream = new CnfStream(d_satSolver,
103
9027
                              d_theoryProxy,
104
                              userContext,
105
9027
                              &d_outMgr,
106
                              rm,
107
18054
                              FormulaLitPolicy::TRACK);
108
109
  // connect theory proxy
110
9027
  d_theoryProxy->finishInit(d_cnfStream);
111
  // connect SAT solver
112
9027
  d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
113
114
9027
  d_decisionEngine->setSatSolver(d_satSolver);
115
9027
  d_decisionEngine->setCnfStream(d_cnfStream);
116
9027
  if (pnm)
117
  {
118
1932
    d_pfCnfStream.reset(new ProofCnfStream(
119
        userContext,
120
966
        *d_cnfStream,
121
966
        static_cast<MinisatSatSolver*>(d_satSolver)->getProofManager(),
122
1932
        pnm));
123
1932
    d_ppm.reset(
124
966
        new PropPfManager(userContext, pnm, d_satSolver, d_pfCnfStream.get()));
125
  }
126
8061
  else if (options::unsatCores())
127
  {
128
1826
    ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
129
  }
130
9027
}
131
132
9027
void PropEngine::finishInit()
133
{
134
9027
  NodeManager* nm = NodeManager::currentNM();
135
9027
  d_cnfStream->convertAndAssert(nm->mkConst(true), false, false);
136
  // this is necessary because if True is later asserted to the prop engine the
137
  // CNF stream will ignore it since the SAT solver already had it registered,
138
  // thus not having True as an assumption for the SAT proof. To solve this
139
  // issue we track it directly here
140
9027
  if (isProofEnabled())
141
  {
142
966
    static_cast<MinisatSatSolver*>(d_satSolver)
143
        ->getProofManager()
144
966
        ->registerSatAssumptions({nm->mkConst(true)});
145
  }
146
9027
  d_cnfStream->convertAndAssert(nm->mkConst(false).notNode(), false, false);
147
9027
}
148
149
18048
PropEngine::~PropEngine() {
150
9024
  Debug("prop") << "Destructing the PropEngine" << std::endl;
151
9024
  d_decisionEngine->shutdown();
152
9024
  d_decisionEngine.reset(nullptr);
153
9024
  delete d_cnfStream;
154
9024
  delete d_satSolver;
155
9024
  delete d_theoryProxy;
156
9024
}
157
158
92314
theory::TrustNode PropEngine::preprocess(
159
    TNode node,
160
    std::vector<theory::TrustNode>& newLemmas,
161
    std::vector<Node>& newSkolems)
162
{
163
92314
  return d_theoryProxy->preprocess(node, newLemmas, newSkolems);
164
}
165
166
2
theory::TrustNode PropEngine::removeItes(
167
    TNode node,
168
    std::vector<theory::TrustNode>& newLemmas,
169
    std::vector<Node>& newSkolems)
170
{
171
2
  return d_theoryProxy->removeItes(node, newLemmas, newSkolems);
172
}
173
174
10348
void PropEngine::notifyPreprocessedAssertions(
175
    const std::vector<Node>& assertions)
176
{
177
  // notify the theory engine of preprocessed assertions
178
10348
  d_theoryEngine->notifyPreprocessedAssertions(assertions);
179
120900
  for (const Node& assertion : assertions)
180
  {
181
110552
    d_decisionEngine->addAssertion(assertion);
182
  }
183
10348
}
184
185
91971
void PropEngine::assertFormula(TNode node) {
186
91971
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
187
91971
  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
188
91975
  assertInternal(node, false, false, true);
189
91967
}
190
191
19541
void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
192
{
193
19541
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
194
19541
  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
195
19541
  d_decisionEngine->addSkolemDefinition(node, skolem);
196
19541
  assertInternal(node, false, false, true);
197
19541
}
198
199
461169
void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
200
{
201
461169
  bool removable = isLemmaPropertyRemovable(p);
202
203
  // call preprocessor
204
922338
  std::vector<theory::TrustNode> ppLemmas;
205
922338
  std::vector<Node> ppSkolems;
206
  theory::TrustNode tplemma =
207
922338
      d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems);
208
209
461167
  Assert(ppSkolems.size() == ppLemmas.size());
210
211
  // do final checks on the lemmas we are about to send
212
9756476
  if (isProofEnabled() && options::proofEagerChecking())
213
  {
214
    Assert(tplemma.getGenerator() != nullptr);
215
    // ensure closed, make the proof node eagerly here to debug
216
    tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
217
    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
218
    {
219
      Assert(ppLemmas[i].getGenerator() != nullptr);
220
      ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
221
    }
222
  }
223
224
461167
  if (Trace.isOn("te-lemma"))
225
  {
226
    Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
227
    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
228
    {
229
      Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven()
230
                        << " (skolem is " << ppSkolems[i] << ")" << std::endl;
231
    }
232
  }
233
234
  // now, assert the lemmas
235
461167
  assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable);
236
461167
}
237
238
471189
void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
239
                                            bool removable)
240
{
241
942378
  Node node = trn.getNode();
242
471189
  Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
243
471189
  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
244
471189
  Assert(!isProofEnabled() || trn.getGenerator() != nullptr);
245
471189
  assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
246
471189
}
247
248
582701
void PropEngine::assertInternal(
249
    TNode node, bool negated, bool removable, bool input, ProofGenerator* pg)
250
{
251
  // Assert as (possibly) removable
252
582701
  if (isProofEnabled())
253
  {
254
82889
    d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
255
    // if input, register the assertion
256
82889
    if (input)
257
    {
258
17103
      d_ppm->registerAssertion(node);
259
    }
260
  }
261
  else
262
  {
263
499816
    d_cnfStream->convertAndAssert(node, removable, negated, input);
264
  }
265
582697
}
266
646707
void PropEngine::assertLemmasInternal(
267
    theory::TrustNode trn,
268
    const std::vector<theory::TrustNode>& ppLemmas,
269
    const std::vector<Node>& ppSkolems,
270
    bool removable)
271
{
272
646707
  if (!trn.isNull())
273
  {
274
461167
    assertTrustedLemmaInternal(trn, removable);
275
  }
276
656729
  for (const theory::TrustNode& tnl : ppLemmas)
277
  {
278
10022
    assertTrustedLemmaInternal(tnl, removable);
279
  }
280
  // assert to decision engine
281
646707
  if (!removable)
282
  {
283
    // also add to the decision engine, where notice we don't need proofs
284
518576
    if (!trn.isNull())
285
    {
286
      // notify the theory proxy of the lemma
287
333036
      d_decisionEngine->addAssertion(trn.getProven());
288
    }
289
518576
    Assert(ppSkolems.size() == ppLemmas.size());
290
528598
    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
291
    {
292
20044
      Node lem = ppLemmas[i].getProven();
293
10022
      d_decisionEngine->addSkolemDefinition(lem, ppSkolems[i]);
294
    }
295
  }
296
646707
}
297
298
82860
void PropEngine::requirePhase(TNode n, bool phase) {
299
82860
  Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << std::endl;
300
301
82860
  Assert(n.getType().isBoolean());
302
82860
  SatLiteral lit = d_cnfStream->getLiteral(n);
303
82860
  d_satSolver->requirePhase(phase ? lit : ~lit);
304
82860
}
305
306
209424
bool PropEngine::isDecision(Node lit) const {
307
209424
  Assert(isSatLiteral(lit));
308
209424
  return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable());
309
}
310
311
void PropEngine::printSatisfyingAssignment(){
312
  const CnfStream::NodeToLiteralMap& transCache =
313
    d_cnfStream->getTranslationCache();
314
  Debug("prop-value") << "Literal | Value | Expr" << std::endl
315
                      << "----------------------------------------"
316
                      << "-----------------" << std::endl;
317
  for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(),
318
      end = transCache.end();
319
      i != end;
320
      ++i) {
321
    std::pair<Node, SatLiteral> curr = *i;
322
    SatLiteral l = curr.second;
323
    if(!l.isNegated()) {
324
      Node n = curr.first;
325
      SatValue value = d_satSolver->modelValue(l);
326
      Debug("prop-value") << "'" << l << "' " << value << " " << n << std::endl;
327
    }
328
  }
329
}
330
331
12420
Result PropEngine::checkSat() {
332
12420
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
333
12420
  Debug("prop") << "PropEngine::checkSat()" << std::endl;
334
335
  // Mark that we are in the checkSat
336
24840
  ScopedBool scopedBool(d_inCheckSat);
337
12420
  d_inCheckSat = true;
338
339
  // TODO This currently ignores conflicts (a dangerous practice).
340
12420
  d_theoryEngine->presolve();
341
342
24846
  if(options::preprocessOnly()) {
343
3
    return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
344
  }
345
346
  // Reset the interrupted flag
347
12417
  d_interrupted = false;
348
349
  // Check the problem
350
12417
  SatValue result = d_satSolver->solve();
351
352
12396
  if( result == SAT_VALUE_UNKNOWN ) {
353
354
    Result::UnknownExplanation why = Result::INTERRUPTED;
355
    if (d_resourceManager->outOfTime())
356
      why = Result::TIMEOUT;
357
    if (d_resourceManager->outOfResources())
358
      why = Result::RESOURCEOUT;
359
360
    return Result(Result::SAT_UNKNOWN, why);
361
  }
362
363
12396
  if( result == SAT_VALUE_TRUE && Debug.isOn("prop") ) {
364
    printSatisfyingAssignment();
365
  }
366
367
12396
  Debug("prop") << "PropEngine::checkSat() => " << result << std::endl;
368
12396
  if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
369
89
    return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
370
  }
371
12307
  return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
372
}
373
374
49224
Node PropEngine::getValue(TNode node) const
375
{
376
49224
  Assert(node.getType().isBoolean());
377
49224
  Assert(d_cnfStream->hasLiteral(node));
378
379
49224
  SatLiteral lit = d_cnfStream->getLiteral(node);
380
381
49224
  SatValue v = d_satSolver->value(lit);
382
49224
  if (v == SAT_VALUE_TRUE)
383
  {
384
49194
    return NodeManager::currentNM()->mkConst(true);
385
  }
386
30
  else if (v == SAT_VALUE_FALSE)
387
  {
388
30
    return NodeManager::currentNM()->mkConst(false);
389
  }
390
  else
391
  {
392
    Assert(v == SAT_VALUE_UNKNOWN);
393
    return Node::null();
394
  }
395
}
396
397
28617561
bool PropEngine::isSatLiteral(TNode node) const
398
{
399
28617561
  return d_cnfStream->hasLiteral(node);
400
}
401
402
10814087
bool PropEngine::hasValue(TNode node, bool& value) const
403
{
404
10814087
  Assert(node.getType().isBoolean());
405
10814087
  Assert(d_cnfStream->hasLiteral(node)) << node;
406
407
10814087
  SatLiteral lit = d_cnfStream->getLiteral(node);
408
409
10814087
  SatValue v = d_satSolver->value(lit);
410
10814087
  if (v == SAT_VALUE_TRUE)
411
  {
412
6239637
    value = true;
413
6239637
    return true;
414
  }
415
4574450
  else if (v == SAT_VALUE_FALSE)
416
  {
417
141228
    value = false;
418
141228
    return true;
419
  }
420
  else
421
  {
422
4433222
    Assert(v == SAT_VALUE_UNKNOWN);
423
4433222
    return false;
424
  }
425
}
426
427
18942
void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const
428
{
429
18942
  d_cnfStream->getBooleanVariables(outputVariables);
430
18942
}
431
432
181732
Node PropEngine::ensureLiteral(TNode n)
433
{
434
  // must preprocess
435
181732
  Node preprocessed = getPreprocessedTerm(n);
436
363464
  Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
437
181732
                         << std::endl;
438
181732
  if (isProofEnabled())
439
  {
440
18987
    d_pfCnfStream->ensureLiteral(preprocessed);
441
  }
442
  else
443
  {
444
162745
    d_cnfStream->ensureLiteral(preprocessed);
445
  }
446
181732
  return preprocessed;
447
}
448
449
185540
Node PropEngine::getPreprocessedTerm(TNode n)
450
{
451
  // must preprocess
452
371080
  std::vector<theory::TrustNode> newLemmas;
453
371080
  std::vector<Node> newSkolems;
454
371080
  theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
455
  // send lemmas corresponding to the skolems introduced by preprocessing n
456
371080
  theory::TrustNode trnNull;
457
185540
  assertLemmasInternal(trnNull, newLemmas, newSkolems, false);
458
371080
  return tpn.isNull() ? Node(n) : tpn.getNode();
459
}
460
461
1731
Node PropEngine::getPreprocessedTerm(TNode n,
462
                                     std::vector<Node>& skAsserts,
463
                                     std::vector<Node>& sks)
464
{
465
  // get the preprocessed form of the term
466
1731
  Node pn = getPreprocessedTerm(n);
467
  // initialize the set of skolems and assertions to process
468
3462
  std::vector<theory::TrustNode> toProcessAsserts;
469
3462
  std::vector<Node> toProcess;
470
1731
  d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess);
471
1731
  size_t index = 0;
472
  // until fixed point is reached
473
4855
  while (index < toProcess.size())
474
  {
475
2302
    theory::TrustNode ka = toProcessAsserts[index];
476
2302
    Node k = toProcess[index];
477
1562
    index++;
478
1562
    if (std::find(sks.begin(), sks.end(), k) != sks.end())
479
    {
480
      // already added the skolem to the list
481
822
      continue;
482
    }
483
    // must preprocess lemmas as well
484
1480
    Node kap = getPreprocessedTerm(ka.getProven());
485
740
    skAsserts.push_back(kap);
486
740
    sks.push_back(k);
487
    // get the skolems in the preprocessed form of the lemma ka
488
740
    d_theoryProxy->getSkolems(kap, toProcessAsserts, toProcess);
489
  }
490
  // return the preprocessed term
491
3462
  return pn;
492
}
493
494
3190
void PropEngine::push()
495
{
496
3190
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
497
3190
  d_satSolver->push();
498
3190
  Debug("prop") << "push()" << std::endl;
499
3190
}
500
501
3190
void PropEngine::pop()
502
{
503
3190
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
504
3190
  d_satSolver->pop();
505
3190
  Debug("prop") << "pop()" << std::endl;
506
3190
}
507
508
12399
void PropEngine::resetTrail()
509
{
510
12399
  d_satSolver->resetTrail();
511
12399
  Debug("prop") << "resetTrail()" << std::endl;
512
12399
}
513
514
17599
unsigned PropEngine::getAssertionLevel() const
515
{
516
17599
  return d_satSolver->getAssertionLevel();
517
}
518
519
bool PropEngine::isRunning() const { return d_inCheckSat; }
520
void PropEngine::interrupt()
521
{
522
  if (!d_inCheckSat)
523
  {
524
    return;
525
  }
526
527
  d_interrupted = true;
528
  d_satSolver->interrupt();
529
  Debug("prop") << "interrupt()" << std::endl;
530
}
531
532
2312
void PropEngine::spendResource(ResourceManager::Resource r)
533
{
534
2312
  d_resourceManager->spendResource(r);
535
2312
}
536
537
bool PropEngine::properExplanation(TNode node, TNode expl) const
538
{
539
  if (!d_cnfStream->hasLiteral(node))
540
  {
541
    Trace("properExplanation")
542
        << "properExplanation(): Failing because node "
543
        << "being explained doesn't have a SAT literal ?!" << std::endl
544
        << "properExplanation(): The node is: " << node << std::endl;
545
    return false;
546
  }
547
548
  SatLiteral nodeLit = d_cnfStream->getLiteral(node);
549
550
  for (TNode::kinded_iterator i = expl.begin(kind::AND),
551
                              i_end = expl.end(kind::AND);
552
       i != i_end;
553
       ++i)
554
  {
555
    if (!d_cnfStream->hasLiteral(*i))
556
    {
557
      Trace("properExplanation")
558
          << "properExplanation(): Failing because one of explanation "
559
          << "nodes doesn't have a SAT literal" << std::endl
560
          << "properExplanation(): The explanation node is: " << *i
561
          << std::endl;
562
      return false;
563
    }
564
565
    SatLiteral iLit = d_cnfStream->getLiteral(*i);
566
567
    if (iLit == nodeLit)
568
    {
569
      Trace("properExplanation")
570
          << "properExplanation(): Failing because the node" << std::endl
571
          << "properExplanation(): " << node << std::endl
572
          << "properExplanation(): cannot be made to explain itself!"
573
          << std::endl;
574
      return false;
575
    }
576
577
    if (!d_satSolver->properExplanation(nodeLit, iLit))
578
    {
579
      Trace("properExplanation")
580
          << "properExplanation(): SAT solver told us that node" << std::endl
581
          << "properExplanation(): " << *i << std::endl
582
          << "properExplanation(): is not part of a proper explanation node for"
583
          << std::endl
584
          << "properExplanation(): " << node << std::endl
585
          << "properExplanation(): Perhaps it one of the two isn't assigned or "
586
             "the explanation"
587
          << std::endl
588
          << "properExplanation(): node wasn't propagated before the node "
589
             "being explained"
590
          << std::endl;
591
      return false;
592
    }
593
  }
594
595
  return true;
596
}
597
598
void PropEngine::checkProof(context::CDList<Node>* assertions)
599
{
600
  if (!d_pnm)
601
  {
602
    return;
603
  }
604
  return d_ppm->checkProof(assertions);
605
}
606
607
19676
ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); }
608
609
2292
std::shared_ptr<ProofNode> PropEngine::getProof()
610
{
611
2292
  if (!d_pnm)
612
  {
613
    return nullptr;
614
  }
615
2292
  return d_ppm->getProof();
616
}
617
618
1705816
bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
619
620
}  // namespace prop
621
26676
}  // namespace CVC4