GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/prop/prop_engine.cpp Lines: 215 299 71.9 %
Date: 2021-03-23 Branches: 303 1030 29.4 %

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
12422
  ScopedBool(bool& reference) :
59
12422
    d_reference(reference) {
60
12422
    d_original = reference;
61
12422
  }
62
63
24844
  ~ScopedBool() {
64
12422
    d_reference = d_original;
65
12422
  }
66
};
67
68
9029
PropEngine::PropEngine(TheoryEngine* te,
69
                       context::Context* satContext,
70
                       context::UserContext* userContext,
71
                       ResourceManager* rm,
72
                       OutputManager& outMgr,
73
9029
                       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
9029
      d_outMgr(outMgr)
86
{
87
9029
  Debug("prop") << "Constructing the PropEngine" << std::endl;
88
89
9029
  d_decisionEngine.reset(new DecisionEngine(satContext, userContext, rm));
90
9029
  d_decisionEngine->init();  // enable appropriate strategies
91
92
9029
  d_satSolver = SatSolverFactory::createCDCLTMinisat(smtStatisticsRegistry());
93
94
  // CNF stream and theory proxy required pointers to each other, make the
95
  // theory proxy first
96
9029
  d_theoryProxy = new TheoryProxy(this,
97
                                  d_theoryEngine,
98
9029
                                  d_decisionEngine.get(),
99
                                  satContext,
100
                                  userContext,
101
9029
                                  pnm);
102
27087
  d_cnfStream = new CnfStream(d_satSolver,
103
9029
                              d_theoryProxy,
104
                              userContext,
105
9029
                              &d_outMgr,
106
                              rm,
107
18058
                              FormulaLitPolicy::TRACK);
108
109
  // connect theory proxy
110
9029
  d_theoryProxy->finishInit(d_cnfStream);
111
  // connect SAT solver
112
9029
  d_satSolver->initialize(d_context, d_theoryProxy, userContext, pnm);
113
114
9029
  d_decisionEngine->setSatSolver(d_satSolver);
115
9029
  d_decisionEngine->setCnfStream(d_cnfStream);
116
9029
  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
8063
  else if (options::unsatCores())
127
  {
128
1826
    ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
129
  }
130
9029
}
131
132
9029
void PropEngine::finishInit()
133
{
134
9029
  NodeManager* nm = NodeManager::currentNM();
135
9029
  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
9029
  if (isProofEnabled())
141
  {
142
966
    static_cast<MinisatSatSolver*>(d_satSolver)
143
        ->getProofManager()
144
966
        ->registerSatAssumptions({nm->mkConst(true)});
145
  }
146
9029
  d_cnfStream->convertAndAssert(nm->mkConst(false).notNode(), false, false);
147
9029
}
148
149
18052
PropEngine::~PropEngine() {
150
9026
  Debug("prop") << "Destructing the PropEngine" << std::endl;
151
9026
  d_decisionEngine->shutdown();
152
9026
  d_decisionEngine.reset(nullptr);
153
9026
  delete d_cnfStream;
154
9026
  delete d_satSolver;
155
9026
  delete d_theoryProxy;
156
9026
}
157
158
92318
theory::TrustNode PropEngine::preprocess(
159
    TNode node,
160
    std::vector<theory::TrustNode>& newLemmas,
161
    std::vector<Node>& newSkolems)
162
{
163
92318
  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
10350
void PropEngine::notifyPreprocessedAssertions(
175
    const std::vector<Node>& assertions)
176
{
177
  // notify the theory proxy of preprocessed assertions
178
10350
  d_theoryProxy->notifyPreprocessedAssertions(assertions);
179
10350
}
180
181
91975
void PropEngine::assertFormula(TNode node) {
182
91975
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
183
91975
  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
184
  // NOTE: we do not notify the theory proxy here, since we've already
185
  // notified the theory proxy during notifyPreprocessedAssertions
186
91979
  assertInternal(node, false, false, true);
187
91971
}
188
189
19549
void PropEngine::assertSkolemDefinition(TNode node, TNode skolem)
190
{
191
19549
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
192
19549
  Debug("prop") << "assertFormula(" << node << ")" << std::endl;
193
19549
  d_theoryProxy->notifyAssertion(node, skolem);
194
19549
  assertInternal(node, false, false, true);
195
19549
}
196
197
461320
void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p)
198
{
199
461320
  bool removable = isLemmaPropertyRemovable(p);
200
201
  // call preprocessor
202
922640
  std::vector<theory::TrustNode> ppLemmas;
203
922640
  std::vector<Node> ppSkolems;
204
  theory::TrustNode tplemma =
205
922640
      d_theoryProxy->preprocessLemma(tlemma, ppLemmas, ppSkolems);
206
207
461318
  Assert(ppSkolems.size() == ppLemmas.size());
208
209
  // do final checks on the lemmas we are about to send
210
9756813
  if (isProofEnabled() && options::proofEagerChecking())
211
  {
212
    Assert(tplemma.getGenerator() != nullptr);
213
    // ensure closed, make the proof node eagerly here to debug
214
    tplemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma");
215
    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
216
    {
217
      Assert(ppLemmas[i].getGenerator() != nullptr);
218
      ppLemmas[i].debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_new");
219
    }
220
  }
221
222
461318
  if (Trace.isOn("te-lemma"))
223
  {
224
    Trace("te-lemma") << "Lemma, output: " << tplemma.getProven() << std::endl;
225
    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
226
    {
227
      Trace("te-lemma") << "Lemma, new lemma: " << ppLemmas[i].getProven()
228
                        << " (skolem is " << ppSkolems[i] << ")" << std::endl;
229
    }
230
  }
231
232
  // now, assert the lemmas
233
461318
  assertLemmasInternal(tplemma, ppLemmas, ppSkolems, removable);
234
461318
}
235
236
471352
void PropEngine::assertTrustedLemmaInternal(theory::TrustNode trn,
237
                                            bool removable)
238
{
239
942704
  Node node = trn.getNode();
240
471352
  Debug("prop::lemmas") << "assertLemma(" << node << ")" << std::endl;
241
471352
  bool negated = trn.getKind() == theory::TrustNodeKind::CONFLICT;
242
471352
  Assert(!isProofEnabled() || trn.getGenerator() != nullptr);
243
471352
  assertInternal(trn.getNode(), negated, removable, false, trn.getGenerator());
244
471352
}
245
246
582876
void PropEngine::assertInternal(
247
    TNode node, bool negated, bool removable, bool input, ProofGenerator* pg)
248
{
249
  // Assert as (possibly) removable
250
582876
  if (isProofEnabled())
251
  {
252
82903
    d_pfCnfStream->convertAndAssert(node, negated, removable, pg);
253
    // if input, register the assertion
254
82903
    if (input)
255
    {
256
17103
      d_ppm->registerAssertion(node);
257
    }
258
  }
259
  else
260
  {
261
499977
    d_cnfStream->convertAndAssert(node, removable, negated, input);
262
  }
263
582872
}
264
647121
void PropEngine::assertLemmasInternal(
265
    theory::TrustNode trn,
266
    const std::vector<theory::TrustNode>& ppLemmas,
267
    const std::vector<Node>& ppSkolems,
268
    bool removable)
269
{
270
647121
  if (!trn.isNull())
271
  {
272
461318
    assertTrustedLemmaInternal(trn, removable);
273
  }
274
657155
  for (const theory::TrustNode& tnl : ppLemmas)
275
  {
276
10034
    assertTrustedLemmaInternal(tnl, removable);
277
  }
278
  // assert to decision engine
279
647121
  if (!removable)
280
  {
281
    // also add to the decision engine, where notice we don't need proofs
282
518968
    if (!trn.isNull())
283
    {
284
      // notify the theory proxy of the lemma
285
333165
      d_theoryProxy->notifyAssertion(trn.getProven());
286
    }
287
518968
    Assert(ppSkolems.size() == ppLemmas.size());
288
529002
    for (size_t i = 0, lsize = ppLemmas.size(); i < lsize; ++i)
289
    {
290
20068
      Node lem = ppLemmas[i].getProven();
291
10034
      d_theoryProxy->notifyAssertion(ppLemmas[i].getProven(), ppSkolems[i]);
292
    }
293
  }
294
647121
}
295
296
82890
void PropEngine::requirePhase(TNode n, bool phase) {
297
82890
  Debug("prop") << "requirePhase(" << n << ", " << phase << ")" << std::endl;
298
299
82890
  Assert(n.getType().isBoolean());
300
82890
  SatLiteral lit = d_cnfStream->getLiteral(n);
301
82890
  d_satSolver->requirePhase(phase ? lit : ~lit);
302
82890
}
303
304
209424
bool PropEngine::isDecision(Node lit) const {
305
209424
  Assert(isSatLiteral(lit));
306
209424
  return d_satSolver->isDecision(d_cnfStream->getLiteral(lit).getSatVariable());
307
}
308
309
void PropEngine::printSatisfyingAssignment(){
310
  const CnfStream::NodeToLiteralMap& transCache =
311
    d_cnfStream->getTranslationCache();
312
  Debug("prop-value") << "Literal | Value | Expr" << std::endl
313
                      << "----------------------------------------"
314
                      << "-----------------" << std::endl;
315
  for(CnfStream::NodeToLiteralMap::const_iterator i = transCache.begin(),
316
      end = transCache.end();
317
      i != end;
318
      ++i) {
319
    std::pair<Node, SatLiteral> curr = *i;
320
    SatLiteral l = curr.second;
321
    if(!l.isNegated()) {
322
      Node n = curr.first;
323
      SatValue value = d_satSolver->modelValue(l);
324
      Debug("prop-value") << "'" << l << "' " << value << " " << n << std::endl;
325
    }
326
  }
327
}
328
329
12422
Result PropEngine::checkSat() {
330
12422
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
331
12422
  Debug("prop") << "PropEngine::checkSat()" << std::endl;
332
333
  // Mark that we are in the checkSat
334
24844
  ScopedBool scopedBool(d_inCheckSat);
335
12422
  d_inCheckSat = true;
336
337
  // TODO This currently ignores conflicts (a dangerous practice).
338
12422
  d_theoryEngine->presolve();
339
340
24850
  if(options::preprocessOnly()) {
341
3
    return Result(Result::SAT_UNKNOWN, Result::REQUIRES_FULL_CHECK);
342
  }
343
344
  // Reset the interrupted flag
345
12419
  d_interrupted = false;
346
347
  // Check the problem
348
12419
  SatValue result = d_satSolver->solve();
349
350
12398
  if( result == SAT_VALUE_UNKNOWN ) {
351
352
    Result::UnknownExplanation why = Result::INTERRUPTED;
353
    if (d_resourceManager->outOfTime())
354
      why = Result::TIMEOUT;
355
    if (d_resourceManager->outOfResources())
356
      why = Result::RESOURCEOUT;
357
358
    return Result(Result::SAT_UNKNOWN, why);
359
  }
360
361
12398
  if( result == SAT_VALUE_TRUE && Debug.isOn("prop") ) {
362
    printSatisfyingAssignment();
363
  }
364
365
12398
  Debug("prop") << "PropEngine::checkSat() => " << result << std::endl;
366
12398
  if(result == SAT_VALUE_TRUE && d_theoryEngine->isIncomplete()) {
367
89
    return Result(Result::SAT_UNKNOWN, Result::INCOMPLETE);
368
  }
369
12309
  return Result(result == SAT_VALUE_TRUE ? Result::SAT : Result::UNSAT);
370
}
371
372
49224
Node PropEngine::getValue(TNode node) const
373
{
374
49224
  Assert(node.getType().isBoolean());
375
49224
  Assert(d_cnfStream->hasLiteral(node));
376
377
49224
  SatLiteral lit = d_cnfStream->getLiteral(node);
378
379
49224
  SatValue v = d_satSolver->value(lit);
380
49224
  if (v == SAT_VALUE_TRUE)
381
  {
382
49194
    return NodeManager::currentNM()->mkConst(true);
383
  }
384
30
  else if (v == SAT_VALUE_FALSE)
385
  {
386
30
    return NodeManager::currentNM()->mkConst(false);
387
  }
388
  else
389
  {
390
    Assert(v == SAT_VALUE_UNKNOWN);
391
    return Node::null();
392
  }
393
}
394
395
28618465
bool PropEngine::isSatLiteral(TNode node) const
396
{
397
28618465
  return d_cnfStream->hasLiteral(node);
398
}
399
400
10814386
bool PropEngine::hasValue(TNode node, bool& value) const
401
{
402
10814386
  Assert(node.getType().isBoolean());
403
10814386
  Assert(d_cnfStream->hasLiteral(node)) << node;
404
405
10814386
  SatLiteral lit = d_cnfStream->getLiteral(node);
406
407
10814386
  SatValue v = d_satSolver->value(lit);
408
10814386
  if (v == SAT_VALUE_TRUE)
409
  {
410
6239850
    value = true;
411
6239850
    return true;
412
  }
413
4574536
  else if (v == SAT_VALUE_FALSE)
414
  {
415
141230
    value = false;
416
141230
    return true;
417
  }
418
  else
419
  {
420
4433306
    Assert(v == SAT_VALUE_UNKNOWN);
421
4433306
    return false;
422
  }
423
}
424
425
18950
void PropEngine::getBooleanVariables(std::vector<TNode>& outputVariables) const
426
{
427
18950
  d_cnfStream->getBooleanVariables(outputVariables);
428
18950
}
429
430
181772
Node PropEngine::ensureLiteral(TNode n)
431
{
432
  // must preprocess
433
181772
  Node preprocessed = getPreprocessedTerm(n);
434
363544
  Trace("ensureLiteral") << "ensureLiteral preprocessed: " << preprocessed
435
181772
                         << std::endl;
436
181772
  if (isProofEnabled())
437
  {
438
18994
    d_pfCnfStream->ensureLiteral(preprocessed);
439
  }
440
  else
441
  {
442
162778
    d_cnfStream->ensureLiteral(preprocessed);
443
  }
444
181772
  return preprocessed;
445
}
446
447
185803
Node PropEngine::getPreprocessedTerm(TNode n)
448
{
449
  // must preprocess
450
371606
  std::vector<theory::TrustNode> newLemmas;
451
371606
  std::vector<Node> newSkolems;
452
371606
  theory::TrustNode tpn = d_theoryProxy->preprocess(n, newLemmas, newSkolems);
453
  // send lemmas corresponding to the skolems introduced by preprocessing n
454
371606
  theory::TrustNode trnNull;
455
185803
  assertLemmasInternal(trnNull, newLemmas, newSkolems, false);
456
371606
  return tpn.isNull() ? Node(n) : tpn.getNode();
457
}
458
459
1731
Node PropEngine::getPreprocessedTerm(TNode n,
460
                                     std::vector<Node>& skAsserts,
461
                                     std::vector<Node>& sks)
462
{
463
  // get the preprocessed form of the term
464
1731
  Node pn = getPreprocessedTerm(n);
465
  // initialize the set of skolems and assertions to process
466
3462
  std::vector<Node> toProcessAsserts;
467
3462
  std::vector<Node> toProcess;
468
1731
  d_theoryProxy->getSkolems(pn, toProcessAsserts, toProcess);
469
1731
  size_t index = 0;
470
  // until fixed point is reached
471
5809
  while (index < toProcess.size())
472
  {
473
3002
    Node ka = toProcessAsserts[index];
474
3002
    Node k = toProcess[index];
475
2039
    index++;
476
2039
    if (std::find(sks.begin(), sks.end(), k) != sks.end())
477
    {
478
      // already added the skolem to the list
479
1076
      continue;
480
    }
481
    // must preprocess lemmas as well
482
1926
    Node kap = getPreprocessedTerm(ka);
483
963
    skAsserts.push_back(kap);
484
963
    sks.push_back(k);
485
    // get the skolems in the preprocessed form of the lemma ka
486
963
    d_theoryProxy->getSkolems(kap, toProcessAsserts, toProcess);
487
  }
488
  // return the preprocessed term
489
3462
  return pn;
490
}
491
492
3190
void PropEngine::push()
493
{
494
3190
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
495
3190
  d_satSolver->push();
496
3190
  Debug("prop") << "push()" << std::endl;
497
3190
}
498
499
3190
void PropEngine::pop()
500
{
501
3190
  Assert(!d_inCheckSat) << "Sat solver in solve()!";
502
3190
  d_satSolver->pop();
503
3190
  Debug("prop") << "pop()" << std::endl;
504
3190
}
505
506
12401
void PropEngine::resetTrail()
507
{
508
12401
  d_satSolver->resetTrail();
509
12401
  Debug("prop") << "resetTrail()" << std::endl;
510
12401
}
511
512
17601
unsigned PropEngine::getAssertionLevel() const
513
{
514
17601
  return d_satSolver->getAssertionLevel();
515
}
516
517
bool PropEngine::isRunning() const { return d_inCheckSat; }
518
void PropEngine::interrupt()
519
{
520
  if (!d_inCheckSat)
521
  {
522
    return;
523
  }
524
525
  d_interrupted = true;
526
  d_satSolver->interrupt();
527
  Debug("prop") << "interrupt()" << std::endl;
528
}
529
530
2312
void PropEngine::spendResource(ResourceManager::Resource r)
531
{
532
2312
  d_resourceManager->spendResource(r);
533
2312
}
534
535
bool PropEngine::properExplanation(TNode node, TNode expl) const
536
{
537
  if (!d_cnfStream->hasLiteral(node))
538
  {
539
    Trace("properExplanation")
540
        << "properExplanation(): Failing because node "
541
        << "being explained doesn't have a SAT literal ?!" << std::endl
542
        << "properExplanation(): The node is: " << node << std::endl;
543
    return false;
544
  }
545
546
  SatLiteral nodeLit = d_cnfStream->getLiteral(node);
547
548
  for (TNode::kinded_iterator i = expl.begin(kind::AND),
549
                              i_end = expl.end(kind::AND);
550
       i != i_end;
551
       ++i)
552
  {
553
    if (!d_cnfStream->hasLiteral(*i))
554
    {
555
      Trace("properExplanation")
556
          << "properExplanation(): Failing because one of explanation "
557
          << "nodes doesn't have a SAT literal" << std::endl
558
          << "properExplanation(): The explanation node is: " << *i
559
          << std::endl;
560
      return false;
561
    }
562
563
    SatLiteral iLit = d_cnfStream->getLiteral(*i);
564
565
    if (iLit == nodeLit)
566
    {
567
      Trace("properExplanation")
568
          << "properExplanation(): Failing because the node" << std::endl
569
          << "properExplanation(): " << node << std::endl
570
          << "properExplanation(): cannot be made to explain itself!"
571
          << std::endl;
572
      return false;
573
    }
574
575
    if (!d_satSolver->properExplanation(nodeLit, iLit))
576
    {
577
      Trace("properExplanation")
578
          << "properExplanation(): SAT solver told us that node" << std::endl
579
          << "properExplanation(): " << *i << std::endl
580
          << "properExplanation(): is not part of a proper explanation node for"
581
          << std::endl
582
          << "properExplanation(): " << node << std::endl
583
          << "properExplanation(): Perhaps it one of the two isn't assigned or "
584
             "the explanation"
585
          << std::endl
586
          << "properExplanation(): node wasn't propagated before the node "
587
             "being explained"
588
          << std::endl;
589
      return false;
590
    }
591
  }
592
593
  return true;
594
}
595
596
void PropEngine::checkProof(context::CDList<Node>* assertions)
597
{
598
  if (!d_pnm)
599
  {
600
    return;
601
  }
602
  return d_ppm->checkProof(assertions);
603
}
604
605
19676
ProofCnfStream* PropEngine::getProofCnfStream() { return d_pfCnfStream.get(); }
606
607
2292
std::shared_ptr<ProofNode> PropEngine::getProof()
608
{
609
2292
  if (!d_pnm)
610
  {
611
    return nullptr;
612
  }
613
2292
  return d_ppm->getProof();
614
}
615
616
1706347
bool PropEngine::isProofEnabled() const { return d_pfCnfStream != nullptr; }
617
618
}  // namespace prop
619
26685
}  // namespace CVC4