GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_engine.cpp Lines: 692 857 80.7 %
Date: 2021-03-23 Branches: 1791 4402 40.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_engine.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Dejan Jovanovic, 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 The theory engine
13
 **
14
 ** The theory engine.
15
 **/
16
17
#include "theory/theory_engine.h"
18
19
#include <sstream>
20
21
#include "base/map_util.h"
22
#include "decision/decision_engine.h"
23
#include "expr/attribute.h"
24
#include "expr/lazy_proof.h"
25
#include "expr/node_builder.h"
26
#include "expr/node_visitor.h"
27
#include "expr/proof_ensure_closed.h"
28
#include "options/quantifiers_options.h"
29
#include "options/smt_options.h"
30
#include "options/theory_options.h"
31
#include "printer/printer.h"
32
#include "prop/prop_engine.h"
33
#include "smt/dump.h"
34
#include "smt/logic_exception.h"
35
#include "smt/output_manager.h"
36
#include "theory/combination_care_graph.h"
37
#include "theory/decision_manager.h"
38
#include "theory/quantifiers/first_order_model.h"
39
#include "theory/quantifiers_engine.h"
40
#include "theory/relevance_manager.h"
41
#include "theory/rewriter.h"
42
#include "theory/shared_solver.h"
43
#include "theory/theory.h"
44
#include "theory/theory_engine_proof_generator.h"
45
#include "theory/theory_id.h"
46
#include "theory/theory_model.h"
47
#include "theory/theory_traits.h"
48
#include "theory/uf/equality_engine.h"
49
#include "util/resource_manager.h"
50
51
using namespace std;
52
53
using namespace CVC4::theory;
54
55
namespace CVC4 {
56
57
/* -------------------------------------------------------------------------- */
58
59
namespace theory {
60
61
/**
62
 * IMPORTANT: The order of the theories is important. For example, strings
63
 *            depends on arith, quantifiers needs to come as the very last.
64
 *            Do not change this order.
65
 */
66
67
#define CVC4_FOR_EACH_THEORY                                     \
68
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BUILTIN)   \
69
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BOOL)      \
70
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_UF)        \
71
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARITH)     \
72
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BV)        \
73
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_FP)        \
74
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_ARRAYS)    \
75
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_DATATYPES) \
76
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SEP)       \
77
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_SETS)      \
78
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_BAGS)      \
79
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_STRINGS)   \
80
  CVC4_FOR_EACH_THEORY_STATEMENT(CVC4::theory::THEORY_QUANTIFIERS)
81
82
}  // namespace theory
83
84
/* -------------------------------------------------------------------------- */
85
86
inline void flattenAnd(Node n, std::vector<TNode>& out){
87
  Assert(n.getKind() == kind::AND);
88
  for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
89
    Node curr = *i;
90
    if(curr.getKind() == kind::AND){
91
      flattenAnd(curr, out);
92
    }else{
93
      out.push_back(curr);
94
    }
95
  }
96
}
97
98
inline Node flattenAnd(Node n){
99
  std::vector<TNode> out;
100
  flattenAnd(n, out);
101
  return NodeManager::currentNM()->mkNode(kind::AND, out);
102
}
103
104
/**
105
 * Compute the string for a given theory id. In this module, we use
106
 * THEORY_SAT_SOLVER as an id, which is not a normal id but maps to
107
 * THEORY_LAST. Thus, we need our own string conversion here.
108
 *
109
 * @param id The theory id
110
 * @return The string corresponding to the theory id
111
 */
112
2148442
std::string getTheoryString(theory::TheoryId id)
113
{
114
2148442
  if (id == theory::THEORY_SAT_SOLVER)
115
  {
116
1435173
    return "THEORY_SAT_SOLVER";
117
  }
118
  else
119
  {
120
1426538
    std::stringstream ss;
121
713269
    ss << id;
122
713269
    return ss.str();
123
  }
124
}
125
126
8997
void TheoryEngine::finishInit()
127
{
128
  // NOTE: This seems to be required since
129
  // theory::TheoryTraits<THEORY>::isParametric cannot be accessed without
130
  // using the CVC4_FOR_EACH_THEORY_STATEMENT macro. -AJR
131
17994
  std::vector<theory::Theory*> paraTheories;
132
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
133
#undef CVC4_FOR_EACH_THEORY_STATEMENT
134
#endif
135
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)   \
136
  if (theory::TheoryTraits<THEORY>::isParametric \
137
      && d_logicInfo.isTheoryEnabled(THEORY))    \
138
  {                                              \
139
    paraTheories.push_back(theoryOf(THEORY));    \
140
  }
141
  // Collect the parametric theories, which are given to the theory combination
142
  // manager below
143
8997
  CVC4_FOR_EACH_THEORY;
144
145
  // Initialize the theory combination architecture
146
17994
  if (options::tcMode() == options::TcMode::CARE_GRAPH)
147
  {
148
8997
    d_tc.reset(new CombinationCareGraph(*this, paraTheories, d_pnm));
149
  }
150
  else
151
  {
152
    Unimplemented() << "TheoryEngine::finishInit: theory combination mode "
153
                    << options::tcMode() << " not supported";
154
  }
155
  // create the relevance filter if any option requires it
156
8997
  if (options::relevanceFilter())
157
  {
158
20
    d_relManager.reset(
159
20
        new RelevanceManager(d_userContext, theory::Valuation(this)));
160
  }
161
162
  // initialize the quantifiers engine
163
8997
  if (d_logicInfo.isQuantified())
164
  {
165
    // get the quantifiers engine, which is initialized by the quantifiers
166
    // theory
167
6054
    d_quantEngine = d_theoryTable[THEORY_QUANTIFIERS]->getQuantifiersEngine();
168
6054
    Assert(d_quantEngine != nullptr);
169
  }
170
  // finish initializing the quantifiers engine, which must come before
171
  // initializing theory combination, since quantifiers engine may have a
172
  // special model builder object
173
8997
  if (d_logicInfo.isQuantified())
174
  {
175
6054
    d_quantEngine->finishInit(this, d_decManager.get());
176
  }
177
  // initialize the theory combination manager, which decides and allocates the
178
  // equality engines to use for all theories.
179
8997
  d_tc->finishInit();
180
  // get pointer to the shared solver
181
8997
  d_sharedSolver = d_tc->getSharedSolver();
182
183
  // finish initializing the theories by linking them with the appropriate
184
  // utilities and then calling their finishInit method.
185
125958
  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
186
116961
    Theory* t = d_theoryTable[theoryId];
187
116961
    if (t == nullptr)
188
    {
189
      continue;
190
    }
191
    // setup the pointers to the utilities
192
116961
    const EeTheoryInfo* eeti = d_tc->getEeTheoryInfo(theoryId);
193
116961
    Assert(eeti != nullptr);
194
    // the theory's official equality engine is the one specified by the
195
    // equality engine manager
196
116961
    t->setEqualityEngine(eeti->d_usedEe);
197
    // set the quantifiers engine
198
116961
    t->setQuantifiersEngine(d_quantEngine);
199
    // set the decision manager for the theory
200
116961
    t->setDecisionManager(d_decManager.get());
201
    // finish initializing the theory
202
116961
    t->finishInit();
203
  }
204
8997
}
205
206
ProofNodeManager* TheoryEngine::getProofNodeManager() const { return d_pnm; }
207
208
8997
TheoryEngine::TheoryEngine(context::Context* context,
209
                           context::UserContext* userContext,
210
                           ResourceManager* rm,
211
                           const LogicInfo& logicInfo,
212
                           OutputManager& outMgr,
213
8997
                           ProofNodeManager* pnm)
214
    : d_propEngine(nullptr),
215
      d_context(context),
216
      d_userContext(userContext),
217
      d_logicInfo(logicInfo),
218
      d_outMgr(outMgr),
219
      d_pnm(pnm),
220
      d_lazyProof(
221
8997
          d_pnm != nullptr
222
              ? new LazyCDProof(
223
962
                    d_pnm, nullptr, d_userContext, "TheoryEngine::LazyCDProof")
224
              : nullptr),
225
8997
      d_tepg(new TheoryEngineProofGenerator(d_pnm, d_userContext)),
226
      d_tc(nullptr),
227
      d_sharedSolver(nullptr),
228
      d_quantEngine(nullptr),
229
8997
      d_decManager(new DecisionManager(userContext)),
230
      d_relManager(nullptr),
231
      d_eager_model_building(false),
232
      d_inConflict(context, false),
233
      d_inSatMode(false),
234
      d_hasShutDown(false),
235
      d_incomplete(context, false),
236
      d_propagationMap(context),
237
      d_propagationMapTimestamp(context, 0),
238
      d_propagatedLiterals(context),
239
      d_propagatedLiteralsIndex(context, 0),
240
      d_atomRequests(context),
241
      d_combineTheoriesTime("TheoryEngine::combineTheoriesTime"),
242
      d_true(),
243
      d_false(),
244
      d_interrupted(false),
245
      d_resourceManager(rm),
246
      d_inPreregister(false),
247
      d_factsAsserted(context, false),
248
36950
      d_attr_handle()
249
{
250
125958
  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST;
251
      ++ theoryId)
252
  {
253
116961
    d_theoryTable[theoryId] = NULL;
254
116961
    d_theoryOut[theoryId] = NULL;
255
  }
256
257
8997
  if (options::sortInference())
258
  {
259
12
    d_sortInfer.reset(new SortInference);
260
  }
261
262
8997
  smtStatisticsRegistry()->registerStat(&d_combineTheoriesTime);
263
8997
  d_true = NodeManager::currentNM()->mkConst<bool>(true);
264
8997
  d_false = NodeManager::currentNM()->mkConst<bool>(false);
265
8997
}
266
267
17988
TheoryEngine::~TheoryEngine() {
268
8994
  Assert(d_hasShutDown);
269
270
125916
  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId != theory::THEORY_LAST; ++ theoryId) {
271
116922
    if(d_theoryTable[theoryId] != NULL) {
272
116874
      delete d_theoryTable[theoryId];
273
116874
      delete d_theoryOut[theoryId];
274
    }
275
  }
276
277
8994
  smtStatisticsRegistry()->unregisterStat(&d_combineTheoriesTime);
278
8994
}
279
280
void TheoryEngine::interrupt() { d_interrupted = true; }
281
839458
void TheoryEngine::preRegister(TNode preprocessed) {
282
1678916
  Debug("theory") << "TheoryEngine::preRegister( " << preprocessed << ")"
283
839458
                  << std::endl;
284
839458
  d_preregisterQueue.push(preprocessed);
285
286
839458
  if (!d_inPreregister) {
287
    // We're in pre-register
288
784889
    d_inPreregister = true;
289
290
    // Process the pre-registration queue
291
2463797
    while (!d_preregisterQueue.empty()) {
292
      // Get the next atom to pre-register
293
839458
      preprocessed = d_preregisterQueue.front();
294
839458
      d_preregisterQueue.pop();
295
296
      // the atom should not have free variables
297
1678916
      Debug("theory") << "TheoryEngine::preRegister: " << preprocessed
298
839458
                      << std::endl;
299
839458
      Assert(!expr::hasFreeVar(preprocessed));
300
      // should not have witness
301
839458
      Assert(!expr::hasSubtermKind(kind::WITNESS, preprocessed));
302
303
      // pre-register with the shared solver, which handles
304
      // calling prepregister on individual theories, adding shared terms,
305
      // and setting up equalities to propagate in the shared term database.
306
839458
      Assert(d_sharedSolver != nullptr);
307
839462
      d_sharedSolver->preRegister(preprocessed);
308
    }
309
310
    // Leaving pre-register
311
784885
    d_inPreregister = false;
312
  }
313
839454
}
314
315
void TheoryEngine::printAssertions(const char* tag) {
316
  if (Trace.isOn(tag)) {
317
318
    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
319
      Theory* theory = d_theoryTable[theoryId];
320
      if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
321
        Trace(tag) << "--------------------------------------------" << endl;
322
        Trace(tag) << "Assertions of " << theory->getId() << ": " << endl;
323
        {
324
          context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
325
                                                     it_end =
326
                                                         theory->facts_end();
327
          for (unsigned i = 0; it != it_end; ++it, ++i)
328
          {
329
            if ((*it).d_isPreregistered)
330
            {
331
              Trace(tag) << "[" << i << "]: ";
332
            }
333
            else
334
            {
335
              Trace(tag) << "(" << i << "): ";
336
            }
337
            Trace(tag) << (*it).d_assertion << endl;
338
          }
339
        }
340
341
        if (d_logicInfo.isSharingEnabled()) {
342
          Trace(tag) << "Shared terms of " << theory->getId() << ": " << endl;
343
          context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
344
          for (unsigned i = 0; it != it_end; ++ it, ++i) {
345
              Trace(tag) << "[" << i << "]: " << (*it) << endl;
346
          }
347
        }
348
      }
349
    }
350
  }
351
}
352
353
void TheoryEngine::dumpAssertions(const char* tag) {
354
  if (Dump.isOn(tag)) {
355
    const Printer& printer = d_outMgr.getPrinter();
356
    std::ostream& out = d_outMgr.getDumpOut();
357
    printer.toStreamCmdComment(out, "Starting completeness check");
358
    for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
359
      Theory* theory = d_theoryTable[theoryId];
360
      if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
361
        printer.toStreamCmdComment(out, "Completeness check");
362
        printer.toStreamCmdPush(out);
363
364
        // Dump the shared terms
365
        if (d_logicInfo.isSharingEnabled()) {
366
          printer.toStreamCmdComment(out, "Shared terms");
367
          context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
368
          for (unsigned i = 0; it != it_end; ++ it, ++i) {
369
              stringstream ss;
370
              ss << (*it);
371
              printer.toStreamCmdComment(out, ss.str());
372
          }
373
        }
374
375
        // Dump the assertions
376
        printer.toStreamCmdComment(out, "Assertions");
377
        context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
378
        for (; it != it_end; ++ it) {
379
          // Get the assertion
380
          Node assertionNode = (*it).d_assertion;
381
          // Purify all the terms
382
383
          if ((*it).d_isPreregistered)
384
          {
385
            printer.toStreamCmdComment(out, "Preregistered");
386
          }
387
          else
388
          {
389
            printer.toStreamCmdComment(out, "Shared assertion");
390
          }
391
          printer.toStreamCmdAssert(out, assertionNode);
392
        }
393
        printer.toStreamCmdCheckSat(out);
394
395
        printer.toStreamCmdPop(out);
396
      }
397
    }
398
  }
399
}
400
401
/**
402
 * Check all (currently-active) theories for conflicts.
403
 * @param effort the effort level to use
404
 */
405
3630221
void TheoryEngine::check(Theory::Effort effort) {
406
  // spendResource();
407
408
  // Reset the interrupt flag
409
3630221
  d_interrupted = false;
410
411
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
412
#undef CVC4_FOR_EACH_THEORY_STATEMENT
413
#endif
414
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)                      \
415
  if (theory::TheoryTraits<THEORY>::hasCheck                        \
416
      && d_logicInfo.isTheoryEnabled(THEORY))                       \
417
  {                                                                 \
418
    theoryOf(THEORY)->check(effort);                                \
419
    if (d_inConflict)                                               \
420
    {                                                               \
421
      Debug("conflict") << THEORY << " in conflict. " << std::endl; \
422
      break;                                                        \
423
    }                                                               \
424
  }
425
426
  // Do the checking
427
  try {
428
429
    // Mark the output channel unused (if this is FULL_EFFORT, and nothing
430
    // is done by the theories, no additional check will be needed)
431
3630221
    d_outputChannelUsed = false;
432
433
    // Mark the lemmas flag (no lemmas added)
434
3630221
    d_lemmasAdded = false;
435
436
3630221
    Debug("theory") << "TheoryEngine::check(" << effort << "): d_factsAsserted = " << (d_factsAsserted ? "true" : "false") << endl;
437
438
    // If in full effort, we have a fake new assertion just to jumpstart the checking
439
3630221
    if (Theory::fullEffort(effort)) {
440
73166
      d_factsAsserted = true;
441
      // Reset round for the relevance manager, which notice only sets a flag
442
      // to indicate that its information must be recomputed.
443
73166
      if (d_relManager != nullptr)
444
      {
445
54
        d_relManager->resetRound();
446
      }
447
73166
      d_tc->resetRound();
448
    }
449
450
    // Check until done
451
10366899
    while (d_factsAsserted && !d_inConflict && !d_lemmasAdded) {
452
453
3533035
      Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << endl;
454
455
3533035
      Trace("theory::assertions") << endl;
456
3533035
      if (Trace.isOn("theory::assertions")) {
457
        printAssertions("theory::assertions");
458
      }
459
460
3533035
      if(Theory::fullEffort(effort)) {
461
74086
        Trace("theory::assertions::fulleffort") << endl;
462
74086
        if (Trace.isOn("theory::assertions::fulleffort")) {
463
          printAssertions("theory::assertions::fulleffort");
464
        }
465
      }
466
467
      // Note that we've discharged all the facts
468
3533035
      d_factsAsserted = false;
469
470
      // Do the checking
471
3533035
      CVC4_FOR_EACH_THEORY;
472
473
3368339
      Debug("theory") << "TheoryEngine::check(" << effort << "): running propagation after the initial check" << endl;
474
475
      // We are still satisfiable, propagate as much as possible
476
3368339
      propagate(effort);
477
478
      // We do combination if all has been processed and we are in fullcheck
479
6794270
      if (Theory::fullEffort(effort) && d_logicInfo.isSharingEnabled()
480
3420663
          && !d_factsAsserted && !needCheck() && !d_inConflict)
481
      {
482
        // Do the combination
483
29481
        Debug("theory") << "TheoryEngine::check(" << effort << "): running combination" << endl;
484
        {
485
58962
          TimerStat::CodeTimer combineTheoriesTimer(d_combineTheoriesTime);
486
29481
          d_tc->combineTheories();
487
        }
488
29481
        if(d_logicInfo.isQuantified()){
489
15760
          d_quantEngine->notifyCombineTheories();
490
        }
491
      }
492
    }
493
494
    // Must consult quantifiers theory for last call to ensure sat, or otherwise add a lemma
495
3630217
    if( Theory::fullEffort(effort) && ! d_inConflict && ! needCheck() ) {
496
22360
      Trace("theory::assertions-model") << endl;
497
22360
      if (Trace.isOn("theory::assertions-model")) {
498
        printAssertions("theory::assertions-model");
499
      }
500
      // reset the model in the combination engine
501
22360
      d_tc->resetModel();
502
      //checks for theories requiring the model go at last call
503
313020
      for (TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
504
290662
        if( theoryId!=THEORY_QUANTIFIERS ){
505
268304
          Theory* theory = d_theoryTable[theoryId];
506
268304
          if (theory && d_logicInfo.isTheoryEnabled(theoryId)) {
507
139190
            if( theory->needsCheckLastEffort() ){
508
13626
              if (!d_tc->buildModel())
509
              {
510
2
                break;
511
              }
512
13624
              theory->check(Theory::EFFORT_LAST_CALL);
513
            }
514
          }
515
        }
516
      }
517
22360
      if (!d_inConflict)
518
      {
519
22360
        if(d_logicInfo.isQuantified()) {
520
          // quantifiers engine must check at last call effort
521
16809
          d_quantEngine->check(Theory::EFFORT_LAST_CALL);
522
        }
523
      }
524
22347
      if (!d_inConflict && !needCheck())
525
      {
526
        // If d_eager_model_building is false, then we only mark that we
527
        // are in "SAT mode". We build the model later only if the user asks
528
        // for it via getBuiltModel.
529
5955
        d_inSatMode = true;
530
5955
        if (d_eager_model_building)
531
        {
532
4
          d_tc->buildModel();
533
        }
534
      }
535
    }
536
537
3630204
    Debug("theory") << "TheoryEngine::check(" << effort << "): done, we are " << (d_inConflict ? "unsat" : "sat") << (d_lemmasAdded ? " with new lemmas" : " with no new lemmas");
538
3630204
    Debug("theory") << ", need check = " << (needCheck() ? "YES" : "NO") << endl;
539
540
3630204
    if( Theory::fullEffort(effort) && !d_inConflict && !needCheck()) {
541
      // Do post-processing of model from the theories (e.g. used for THEORY_SEP
542
      // to construct heap model)
543
5955
      d_tc->postProcessModel(d_incomplete.get());
544
    }
545
  } catch(const theory::Interrupted&) {
546
    Trace("theory") << "TheoryEngine::check() => interrupted" << endl;
547
  }
548
  // If fulleffort, check all theories
549
3630204
  if(Dump.isOn("theory::fullcheck") && Theory::fullEffort(effort)) {
550
    if (!d_inConflict && !needCheck()) {
551
      dumpAssertions("theory::fullcheck");
552
    }
553
  }
554
3630204
}
555
556
3368339
void TheoryEngine::propagate(Theory::Effort effort)
557
{
558
  // Reset the interrupt flag
559
3368339
  d_interrupted = false;
560
561
  // Definition of the statement that is to be run by every theory
562
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
563
#undef CVC4_FOR_EACH_THEORY_STATEMENT
564
#endif
565
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
566
  if (theory::TheoryTraits<THEORY>::hasPropagate && d_logicInfo.isTheoryEnabled(THEORY)) { \
567
    theoryOf(THEORY)->propagate(effort); \
568
  }
569
570
  // Reset the interrupt flag
571
3368339
  d_interrupted = false;
572
573
  // Propagate for each theory using the statement above
574
3368339
  CVC4_FOR_EACH_THEORY;
575
3368339
}
576
577
2565385
Node TheoryEngine::getNextDecisionRequest()
578
{
579
2565385
  return d_decManager->getNextDecisionRequest();
580
}
581
582
128153
bool TheoryEngine::properConflict(TNode conflict) const {
583
  bool value;
584
128153
  if (conflict.getKind() == kind::AND) {
585
1731896
    for (unsigned i = 0; i < conflict.getNumChildren(); ++ i) {
586
1604390
      if (! getPropEngine()->hasValue(conflict[i], value)) {
587
        Debug("properConflict") << "Bad conflict is due to unassigned atom: "
588
                                << conflict[i] << endl;
589
        return false;
590
      }
591
1604390
      if (! value) {
592
        Debug("properConflict") << "Bad conflict is due to false atom: "
593
                                << conflict[i] << endl;
594
        return false;
595
      }
596
1604390
      if (conflict[i] != Rewriter::rewrite(conflict[i])) {
597
        Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
598
                                << conflict[i] << " vs " << Rewriter::rewrite(conflict[i]) << endl;
599
        return false;
600
      }
601
    }
602
  } else {
603
647
    if (! getPropEngine()->hasValue(conflict, value)) {
604
      Debug("properConflict") << "Bad conflict is due to unassigned atom: "
605
                              << conflict << endl;
606
      return false;
607
    }
608
647
    if(! value) {
609
      Debug("properConflict") << "Bad conflict is due to false atom: "
610
                              << conflict << endl;
611
      return false;
612
    }
613
647
    if (conflict != Rewriter::rewrite(conflict)) {
614
      Debug("properConflict") << "Bad conflict is due to atom not in normal form: "
615
                              << conflict << " vs " << Rewriter::rewrite(conflict) << endl;
616
      return false;
617
    }
618
  }
619
128153
  return true;
620
}
621
622
186152
TheoryModel* TheoryEngine::getModel()
623
{
624
186152
  Assert(d_tc != nullptr);
625
186152
  TheoryModel* m = d_tc->getModel();
626
186152
  Assert(m != nullptr);
627
186152
  return m;
628
}
629
630
5743
TheoryModel* TheoryEngine::getBuiltModel()
631
{
632
5743
  Assert(d_tc != nullptr);
633
  // If this method was called, we should be in SAT mode, and produceModels
634
  // should be true.
635
5743
  AlwaysAssert(options::produceModels());
636
5743
  if (!d_inSatMode)
637
  {
638
    // not available, perhaps due to interuption.
639
    return nullptr;
640
  }
641
  // must build model at this point
642
5743
  if (!d_tc->buildModel())
643
  {
644
    return nullptr;
645
  }
646
5742
  return d_tc->getModel();
647
}
648
649
13658
bool TheoryEngine::buildModel()
650
{
651
13658
  Assert(d_tc != nullptr);
652
13658
  return d_tc->buildModel();
653
}
654
655
12422
bool TheoryEngine::presolve() {
656
  // Reset the interrupt flag
657
12422
  d_interrupted = false;
658
659
  // Reset the decision manager. This clears its decision strategies that are
660
  // no longer valid in this user context.
661
12422
  d_decManager->presolve();
662
663
  try {
664
    // Definition of the statement that is to be run by every theory
665
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
666
#undef CVC4_FOR_EACH_THEORY_STATEMENT
667
#endif
668
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
669
    if (theory::TheoryTraits<THEORY>::hasPresolve) {    \
670
      theoryOf(THEORY)->presolve(); \
671
      if(d_inConflict) { \
672
        return true; \
673
      } \
674
    }
675
676
    // Presolve for each theory using the statement above
677
12422
    CVC4_FOR_EACH_THEORY;
678
  } catch(const theory::Interrupted&) {
679
    Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
680
  }
681
  // return whether we have a conflict
682
12418
  return false;
683
}/* TheoryEngine::presolve() */
684
685
12401
void TheoryEngine::postsolve() {
686
  // no longer in SAT mode
687
12401
  d_inSatMode = false;
688
  // Reset the interrupt flag
689
12401
  d_interrupted = false;
690
12401
  bool CVC4_UNUSED wasInConflict = d_inConflict;
691
692
  try {
693
    // Definition of the statement that is to be run by every theory
694
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
695
#undef CVC4_FOR_EACH_THEORY_STATEMENT
696
#endif
697
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY)    \
698
  if (theory::TheoryTraits<THEORY>::hasPostsolve) \
699
  {                                               \
700
    theoryOf(THEORY)->postsolve();                \
701
    Assert(!d_inConflict || wasInConflict)        \
702
        << "conflict raised during postsolve()";  \
703
  }
704
705
    // Postsolve for each theory using the statement above
706
    CVC4_FOR_EACH_THEORY;
707
  } catch(const theory::Interrupted&) {
708
    Trace("theory") << "TheoryEngine::postsolve() => interrupted" << endl;
709
  }
710
12401
}/* TheoryEngine::postsolve() */
711
712
713
2312
void TheoryEngine::notifyRestart() {
714
  // Reset the interrupt flag
715
2312
  d_interrupted = false;
716
717
  // Definition of the statement that is to be run by every theory
718
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
719
#undef CVC4_FOR_EACH_THEORY_STATEMENT
720
#endif
721
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
722
  if (theory::TheoryTraits<THEORY>::hasNotifyRestart && d_logicInfo.isTheoryEnabled(THEORY)) { \
723
    theoryOf(THEORY)->notifyRestart(); \
724
  }
725
726
  // notify each theory using the statement above
727
2312
  CVC4_FOR_EACH_THEORY;
728
2312
}
729
730
92002
void TheoryEngine::ppStaticLearn(TNode in, NodeBuilder<>& learned) {
731
  // Reset the interrupt flag
732
92002
  d_interrupted = false;
733
734
  // Definition of the statement that is to be run by every theory
735
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
736
#undef CVC4_FOR_EACH_THEORY_STATEMENT
737
#endif
738
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
739
  if (theory::TheoryTraits<THEORY>::hasPpStaticLearn) { \
740
    theoryOf(THEORY)->ppStaticLearn(in, learned); \
741
  }
742
743
  // static learning for each theory using the statement above
744
92002
  CVC4_FOR_EACH_THEORY;
745
92002
}
746
747
95938
bool TheoryEngine::isRelevant(Node lit) const
748
{
749
95938
  if (d_relManager != nullptr)
750
  {
751
1096
    return d_relManager->isRelevant(lit);
752
  }
753
  // otherwise must assume its relevant
754
94842
  return true;
755
}
756
757
8994
void TheoryEngine::shutdown() {
758
  // Set this first; if a Theory shutdown() throws an exception,
759
  // at least the destruction of the TheoryEngine won't confound
760
  // matters.
761
8994
  d_hasShutDown = true;
762
763
  // Shutdown all the theories
764
125916
  for(TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST; ++theoryId) {
765
116922
    if(d_theoryTable[theoryId]) {
766
116874
      theoryOf(theoryId)->shutdown();
767
    }
768
  }
769
8994
}
770
771
111080
theory::Theory::PPAssertStatus TheoryEngine::solve(
772
    TrustNode tliteral, TrustSubstitutionMap& substitutionOut)
773
{
774
  // Reset the interrupt flag
775
111080
  d_interrupted = false;
776
777
222160
  TNode literal = tliteral.getNode();
778
222160
  TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
779
111080
  Trace("theory::solve") << "TheoryEngine::solve(" << literal << "): solving with " << theoryOf(atom)->getId() << endl;
780
781
222160
  if(! d_logicInfo.isTheoryEnabled(Theory::theoryOf(atom)) &&
782
111080
     Theory::theoryOf(atom) != THEORY_SAT_SOLVER) {
783
    stringstream ss;
784
    ss << "The logic was specified as " << d_logicInfo.getLogicString()
785
       << ", which doesn't include " << Theory::theoryOf(atom)
786
       << ", but got a preprocessing-time fact for that theory." << endl
787
       << "The fact:" << endl
788
       << literal;
789
    throw LogicException(ss.str());
790
  }
791
792
  Theory::PPAssertStatus solveStatus =
793
111080
      theoryOf(atom)->ppAssert(tliteral, substitutionOut);
794
111080
  Trace("theory::solve") << "TheoryEngine::solve(" << literal << ") => " << solveStatus << endl;
795
222160
  return solveStatus;
796
}
797
798
197598
theory::TrustNode TheoryEngine::ppRewriteEquality(TNode eq)
799
{
800
197598
  Assert(eq.getKind() == kind::EQUAL);
801
395196
  std::vector<SkolemLemma> lems;
802
197598
  TrustNode trn = theoryOf(eq)->ppRewrite(eq, lems);
803
  // should never introduce a skolem to eliminate an equality
804
197598
  Assert(lems.empty());
805
395196
  return trn;
806
}
807
808
10350
void TheoryEngine::notifyPreprocessedAssertions(
809
    const std::vector<Node>& assertions) {
810
  // call all the theories
811
144900
  for (TheoryId theoryId = theory::THEORY_FIRST; theoryId < theory::THEORY_LAST;
812
       ++theoryId) {
813
134550
    if (d_theoryTable[theoryId]) {
814
134550
      theoryOf(theoryId)->ppNotifyAssertions(assertions);
815
    }
816
  }
817
10350
  if (d_relManager != nullptr)
818
  {
819
10
    d_relManager->notifyPreprocessedAssertions(assertions);
820
  }
821
10350
}
822
823
35287877
bool TheoryEngine::markPropagation(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
824
825
  // What and where we are asserting
826
70575754
  NodeTheoryPair toAssert(assertion, toTheoryId, d_propagationMapTimestamp);
827
  // What and where it came from
828
70575754
  NodeTheoryPair toExplain(originalAssertion, fromTheoryId, d_propagationMapTimestamp);
829
830
  // See if the theory already got this literal
831
35287877
  PropagationMap::const_iterator find = d_propagationMap.find(toAssert);
832
35287877
  if (find != d_propagationMap.end()) {
833
    // The theory already knows this
834
10135724
    Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): already there" << endl;
835
10135724
    return false;
836
  }
837
838
25152153
  Trace("theory::assertToTheory") << "TheoryEngine::markPropagation(): marking [" << d_propagationMapTimestamp << "] " << assertion << ", " << toTheoryId << " from " << originalAssertion << ", " << fromTheoryId << endl;
839
840
  // Mark the propagation
841
25152153
  d_propagationMap[toAssert] = toExplain;
842
25152153
  d_propagationMapTimestamp = d_propagationMapTimestamp + 1;
843
844
25152153
  return true;
845
}
846
847
848
40601667
void TheoryEngine::assertToTheory(TNode assertion, TNode originalAssertion, theory::TheoryId toTheoryId, theory::TheoryId fromTheoryId) {
849
850
40601667
  Trace("theory::assertToTheory") << "TheoryEngine::assertToTheory(" << assertion << ", " << originalAssertion << "," << toTheoryId << ", " << fromTheoryId << ")" << endl;
851
852
40601667
  Assert(toTheoryId != fromTheoryId);
853
67663717
  if(toTheoryId != THEORY_SAT_SOLVER &&
854
27062050
     ! d_logicInfo.isTheoryEnabled(toTheoryId)) {
855
    stringstream ss;
856
    ss << "The logic was specified as " << d_logicInfo.getLogicString()
857
       << ", which doesn't include " << toTheoryId
858
       << ", but got an asserted fact to that theory." << endl
859
       << "The fact:" << endl
860
       << assertion;
861
    throw LogicException(ss.str());
862
  }
863
864
40601667
  if (d_inConflict) {
865
68070
    return;
866
  }
867
868
  // If sharing is disabled, things are easy
869
40533597
  if (!d_logicInfo.isSharingEnabled()) {
870
5245720
    Assert(assertion == originalAssertion);
871
5245720
    if (fromTheoryId == THEORY_SAT_SOLVER) {
872
      // Send to the apropriate theory
873
3348926
      theory::Theory* toTheory = theoryOf(toTheoryId);
874
      // We assert it, and we know it's preregistereed
875
3348926
      toTheory->assertFact(assertion, true);
876
      // Mark that we have more information
877
3348926
      d_factsAsserted = true;
878
    } else {
879
1896794
      Assert(toTheoryId == THEORY_SAT_SOLVER);
880
      // Check for propositional conflict
881
      bool value;
882
1896794
      if (d_propEngine->hasValue(assertion, value)) {
883
815899
        if (!value) {
884
40908
          Trace("theory::propagate") << "TheoryEngine::assertToTheory(" << assertion << ", " << toTheoryId << ", " << fromTheoryId << "): conflict (no sharing)" << endl;
885
81816
          Trace("dtview::conflict")
886
40908
              << ":THEORY-CONFLICT: " << assertion << std::endl;
887
40908
          d_inConflict = true;
888
        } else {
889
774991
          return;
890
        }
891
      }
892
1121803
      d_propagatedLiterals.push_back(assertion);
893
    }
894
4470729
    return;
895
  }
896
897
  // If sending to the shared terms database, it's also simple
898
35287877
  if (toTheoryId == THEORY_BUILTIN) {
899
22652930
    Assert(assertion.getKind() == kind::EQUAL
900
           || (assertion.getKind() == kind::NOT
901
               && assertion[0].getKind() == kind::EQUAL))
902
11326465
        << "atom should be an EQUALity, not `" << assertion << "'";
903
11326465
    if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
904
      // assert to the shared solver
905
6289637
      bool polarity = assertion.getKind() != kind::NOT;
906
12579274
      TNode atom = polarity ? assertion : assertion[0];
907
6289637
      d_sharedSolver->assertSharedEquality(atom, polarity, assertion);
908
    }
909
11326465
    return;
910
  }
911
912
  // Things from the SAT solver are already normalized, so they go
913
  // directly to the apropriate theory
914
23961412
  if (fromTheoryId == THEORY_SAT_SOLVER) {
915
    // We know that this is normalized, so just send it off to the theory
916
8761555
    if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
917
      // Is it preregistered
918
8677510
      bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
919
      // We assert it
920
8677510
      theoryOf(toTheoryId)->assertFact(assertion, preregistered);
921
      // Mark that we have more information
922
8677510
      d_factsAsserted = true;
923
    }
924
8761555
    return;
925
  }
926
927
  // Propagations to the SAT solver are just enqueued for pickup by
928
  // the SAT solver later
929
15199857
  if (toTheoryId == THEORY_SAT_SOLVER) {
930
11598680
    if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
931
      // Enqueue for propagation to the SAT solver
932
7054127
      d_propagatedLiterals.push_back(assertion);
933
      // Check for propositional conflicts
934
      bool value;
935
7054127
      if (d_propEngine->hasValue(assertion, value) && !value) {
936
74742
        Trace("theory::propagate")
937
37371
            << "TheoryEngine::assertToTheory(" << assertion << ", "
938
37371
            << toTheoryId << ", " << fromTheoryId << "): conflict (sharing)"
939
37371
            << endl;
940
74742
        Trace("dtview::conflict")
941
37371
            << ":THEORY-CONFLICT: " << assertion << std::endl;
942
37371
        d_inConflict = true;
943
      }
944
    }
945
11598680
    return;
946
  }
947
948
3601177
  Assert(assertion.getKind() == kind::EQUAL
949
         || (assertion.getKind() == kind::NOT
950
             && assertion[0].getKind() == kind::EQUAL));
951
952
  // Normalize
953
7202354
  Node normalizedLiteral = Rewriter::rewrite(assertion);
954
955
  // See if it rewrites false directly -> conflict
956
3601177
  if (normalizedLiteral.isConst()) {
957
22625
    if (!normalizedLiteral.getConst<bool>()) {
958
      // Mark the propagation for explanations
959
387
      if (markPropagation(normalizedLiteral, originalAssertion, toTheoryId, fromTheoryId)) {
960
        // special case, trust node has no proof generator
961
774
        TrustNode trnn = TrustNode::mkTrustConflict(normalizedLiteral);
962
        // Get the explanation (conflict will figure out where it came from)
963
387
        conflict(trnn, toTheoryId);
964
      } else {
965
        Unreachable();
966
      }
967
387
      return;
968
    }
969
  }
970
971
  // Try and assert (note that we assert the non-normalized one)
972
3600790
  if (markPropagation(assertion, originalAssertion, toTheoryId, fromTheoryId)) {
973
    // Check if has been pre-registered with the theory
974
3130492
    bool preregistered = d_propEngine->isSatLiteral(assertion) && Theory::theoryOf(assertion) == toTheoryId;
975
    // Assert away
976
3130492
    theoryOf(toTheoryId)->assertFact(assertion, preregistered);
977
3130492
    d_factsAsserted = true;
978
  }
979
980
3600790
  return;
981
}
982
983
12078584
void TheoryEngine::assertFact(TNode literal)
984
{
985
12078584
  Trace("theory") << "TheoryEngine::assertFact(" << literal << ")" << endl;
986
987
  // spendResource();
988
989
  // If we're in conflict, nothing to do
990
12078584
  if (d_inConflict) {
991
20877
    return;
992
  }
993
994
  // Get the atom
995
12057707
  bool polarity = literal.getKind() != kind::NOT;
996
24115414
  TNode atom = polarity ? literal : literal[0];
997
998
12057707
  if (d_logicInfo.isSharingEnabled()) {
999
    // If any shared terms, it's time to do sharing work
1000
8708781
    d_sharedSolver->preNotifySharedFact(atom);
1001
1002
    // If it's an equality, assert it to the shared term manager, even though the terms are not
1003
    // yet shared. As the terms become shared later, the shared terms manager will then add them
1004
    // to the assert the equality to the interested theories
1005
8708781
    if (atom.getKind() == kind::EQUAL) {
1006
      // Assert it to the the owning theory
1007
4644330
      assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1008
      // Shared terms manager will assert to interested theories directly, as
1009
      // the terms become shared
1010
4644330
      assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ THEORY_SAT_SOLVER);
1011
1012
      // Now, let's check for any atom triggers from lemmas
1013
4644330
      AtomRequests::atom_iterator it = d_atomRequests.getAtomIterator(atom);
1014
4654500
      while (!it.done()) {
1015
5085
        const AtomRequests::Request& request = it.get();
1016
        Node toAssert =
1017
10170
            polarity ? (Node)request.d_atom : request.d_atom.notNode();
1018
5085
        Debug("theory::atoms") << "TheoryEngine::assertFact(" << literal << "): sending requested " << toAssert << endl;
1019
5085
        assertToTheory(
1020
5085
            toAssert, literal, request.d_toTheory, THEORY_SAT_SOLVER);
1021
5085
        it.next();
1022
      }
1023
1024
    } else {
1025
      // Not an equality, just assert to the appropriate theory
1026
4064451
      assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1027
    }
1028
  } else {
1029
    // Assert the fact to the appropriate theory directly
1030
3348926
    assertToTheory(literal, literal, /* to */ Theory::theoryOf(atom), /* from */ THEORY_SAT_SOLVER);
1031
  }
1032
}
1033
1034
15674248
bool TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
1035
15674248
  Debug("theory::propagate") << "TheoryEngine::propagate(" << literal << ", " << theory << ")" << endl;
1036
1037
31348496
  Trace("dtview::prop") << std::string(d_context->getLevel(), ' ')
1038
15674248
                        << ":THEORY-PROP: " << literal << endl;
1039
1040
  // spendResource();
1041
1042
  // Get the atom
1043
15674248
  bool polarity = literal.getKind() != kind::NOT;
1044
31348496
  TNode atom = polarity ? literal : literal[0];
1045
1046
15674248
  if (d_logicInfo.isSharingEnabled() && atom.getKind() == kind::EQUAL) {
1047
11511647
    if (d_propEngine->isSatLiteral(literal)) {
1048
      // We propagate SAT literals to SAT
1049
9377016
      assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1050
    }
1051
11511647
    if (theory != THEORY_BUILTIN) {
1052
      // Assert to the shared terms database
1053
6703722
      assertToTheory(literal, literal, /* to */ THEORY_BUILTIN, /* from */ theory);
1054
    }
1055
  } else {
1056
    // Just send off to the SAT solver
1057
4162601
    Assert(d_propEngine->isSatLiteral(literal));
1058
4162601
    assertToTheory(literal, literal, /* to */ THEORY_SAT_SOLVER, /* from */ theory);
1059
  }
1060
1061
31348496
  return !d_inConflict;
1062
}
1063
1064
54015
const LogicInfo& TheoryEngine::getLogicInfo() const { return d_logicInfo; }
1065
1066
840
bool TheoryEngine::getSepHeapTypes(TypeNode& locType, TypeNode& dataType) const
1067
{
1068
840
  if (d_sepLocType.isNull())
1069
  {
1070
819
    return false;
1071
  }
1072
21
  locType = d_sepLocType;
1073
21
  dataType = d_sepDataType;
1074
21
  return true;
1075
}
1076
1077
121
void TheoryEngine::declareSepHeap(TypeNode locT, TypeNode dataT)
1078
{
1079
121
  Theory* tsep = theoryOf(THEORY_SEP);
1080
121
  if (tsep == nullptr)
1081
  {
1082
    Assert(false) << "TheoryEngine::declareSepHeap called without the "
1083
                     "separation logic theory enabled";
1084
    return;
1085
  }
1086
1087
  // Definition of the statement that is to be run by every theory
1088
#ifdef CVC4_FOR_EACH_THEORY_STATEMENT
1089
#undef CVC4_FOR_EACH_THEORY_STATEMENT
1090
#endif
1091
#define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
1092
  theoryOf(THEORY)->declareSepHeap(locT, dataT);
1093
1094
  // notify each theory using the statement above
1095
121
  CVC4_FOR_EACH_THEORY;
1096
1097
  // remember the types we have set
1098
119
  d_sepLocType = locT;
1099
119
  d_sepDataType = dataT;
1100
}
1101
1102
1558001
theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
1103
1558001
  Assert(a.getType().isComparableTo(b.getType()));
1104
1558001
  return d_sharedSolver->getEqualityStatus(a, b);
1105
}
1106
1107
7095
Node TheoryEngine::getModelValue(TNode var) {
1108
7095
  if (var.isConst())
1109
  {
1110
    // the model value of a constant must be itself
1111
    return var;
1112
  }
1113
7095
  Assert(d_sharedSolver->isShared(var));
1114
7095
  return theoryOf(Theory::theoryOf(var.getType()))->getModelValue(var);
1115
}
1116
1117
135138
TrustNode TheoryEngine::getExplanation(TNode node)
1118
{
1119
270276
  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
1120
135138
                           << "): current propagation index = "
1121
135138
                           << d_propagationMapTimestamp << endl;
1122
135138
  bool polarity = node.getKind() != kind::NOT;
1123
270276
  TNode atom = polarity ? node : node[0];
1124
1125
  // If we're not in shared mode, explanations are simple
1126
135138
  if (!d_logicInfo.isSharingEnabled())
1127
  {
1128
120252
    Debug("theory::explain")
1129
60126
        << "TheoryEngine::getExplanation: sharing is NOT enabled. "
1130
60126
        << " Responsible theory is: " << theoryOf(atom)->getId() << std::endl;
1131
1132
120252
    TrustNode texplanation = theoryOf(atom)->explain(node);
1133
120252
    Node explanation = texplanation.getNode();
1134
120252
    Debug("theory::explain") << "TheoryEngine::getExplanation(" << node
1135
60126
                             << ") => " << explanation << endl;
1136
60126
    if (isProofEnabled())
1137
    {
1138
13423
      texplanation.debugCheckClosed(
1139
          "te-proof-exp", "texplanation no share", false);
1140
      // check if no generator, if so, add THEORY_LEMMA
1141
13423
      if (texplanation.getGenerator() == nullptr)
1142
      {
1143
856
        Node proven = texplanation.getProven();
1144
428
        TheoryId tid = theoryOf(atom)->getId();
1145
856
        Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(tid);
1146
428
        d_lazyProof->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
1147
428
        texplanation =
1148
856
            TrustNode::mkTrustPropExp(node, explanation, d_lazyProof.get());
1149
      }
1150
    }
1151
60126
    return texplanation;
1152
  }
1153
1154
150024
  Debug("theory::explain") << "TheoryEngine::getExplanation: sharing IS enabled"
1155
75012
                           << std::endl;
1156
1157
  // Initial thing to explain
1158
150024
  NodeTheoryPair toExplain(node, THEORY_SAT_SOLVER, d_propagationMapTimestamp);
1159
75012
  Assert(d_propagationMap.find(toExplain) != d_propagationMap.end());
1160
1161
150024
  NodeTheoryPair nodeExplainerPair = d_propagationMap[toExplain];
1162
150024
  Debug("theory::explain")
1163
75012
      << "TheoryEngine::getExplanation: explainer for node "
1164
75012
      << nodeExplainerPair.d_node
1165
75012
      << " is theory: " << nodeExplainerPair.d_theory << std::endl;
1166
1167
  // Create the workplace for explanations
1168
150024
  std::vector<NodeTheoryPair> vec{d_propagationMap[toExplain]};
1169
  // Process the explanation
1170
150024
  TrustNode texplanation = getExplanation(vec);
1171
150024
  Debug("theory::explain") << "TheoryEngine::getExplanation(" << node << ") => "
1172
75012
                           << texplanation.getNode() << endl;
1173
75012
  return texplanation;
1174
}
1175
1176
110294
struct AtomsCollect {
1177
1178
  std::vector<TNode> d_atoms;
1179
  std::unordered_set<TNode, TNodeHashFunction> d_visited;
1180
1181
public:
1182
1183
  typedef void return_type;
1184
1185
679080
  bool alreadyVisited(TNode current, TNode parent) {
1186
    // Check if already visited
1187
679080
    if (d_visited.find(current) != d_visited.end()) return true;
1188
    // Don't visit non-boolean
1189
625419
    if (!current.getType().isBoolean()) return true;
1190
    // New node
1191
510053
    return false;
1192
  }
1193
1194
170513
  void visit(TNode current, TNode parent) {
1195
170513
    if (Theory::theoryOf(current) != theory::THEORY_BOOL) {
1196
61705
      d_atoms.push_back(current);
1197
    }
1198
170513
    d_visited.insert(current);
1199
170513
  }
1200
1201
55147
  void start(TNode node) {}
1202
55147
  void done(TNode node) {}
1203
1204
55147
  std::vector<TNode> getAtoms() const {
1205
55147
    return d_atoms;
1206
  }
1207
};
1208
1209
55147
void TheoryEngine::ensureLemmaAtoms(const std::vector<TNode>& atoms, theory::TheoryId atomsTo) {
1210
116852
  for (unsigned i = 0; i < atoms.size(); ++ i) {
1211
1212
    // Non-equality atoms are either owned by theory or they don't make sense
1213
61705
    if (atoms[i].getKind() != kind::EQUAL) {
1214
64369
      continue;
1215
    }
1216
1217
    // The equality
1218
59041
    Node eq = atoms[i];
1219
    // Simple normalization to not repeat stuff
1220
53661
    if (eq[0] > eq[1]) {
1221
      eq = eq[1].eqNode(eq[0]);
1222
    }
1223
1224
    // Rewrite the equality
1225
59041
    Node eqNormalized = Rewriter::rewrite(atoms[i]);
1226
1227
53661
    Debug("theory::atoms") << "TheoryEngine::ensureLemmaAtoms(): " << eq << " with nf " << eqNormalized << endl;
1228
1229
    // If the equality is a boolean constant, we send immediately
1230
53661
    if (eqNormalized.isConst()) {
1231
      if (eqNormalized.getConst<bool>()) {
1232
        assertToTheory(eq, eqNormalized, /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1233
      } else {
1234
        assertToTheory(eq.notNode(), eqNormalized.notNode(), /** to */ atomsTo, /** Sat solver */ theory::THEORY_SAT_SOLVER);
1235
      }
1236
      continue;
1237
53661
    }else if( eqNormalized.getKind() != kind::EQUAL){
1238
      Assert(eqNormalized.getKind() == kind::BOOLEAN_TERM_VARIABLE
1239
             || (eqNormalized.getKind() == kind::NOT
1240
                 && eqNormalized[0].getKind() == kind::BOOLEAN_TERM_VARIABLE));
1241
      // this happens for Boolean term equalities V = true that are rewritten to V, we should skip
1242
      //  TODO : revisit this
1243
      continue;
1244
    }
1245
1246
    // If the normalization did the just flips, keep the flip
1247
53661
    if (eqNormalized[0] == eq[1] && eqNormalized[1] == eq[0]) {
1248
1818
      eq = eqNormalized;
1249
    }
1250
1251
    // Check if the equality is already known by the sat solver
1252
53661
    if (d_propEngine->isSatLiteral(eqNormalized)) {
1253
      bool value;
1254
48856
      if (d_propEngine->hasValue(eqNormalized, value)) {
1255
96562
        if (value) {
1256
48281
          assertToTheory(eq, eqNormalized, atomsTo, theory::THEORY_SAT_SOLVER);
1257
96562
          continue;
1258
        } else {
1259
          assertToTheory(eq.notNode(), eqNormalized.notNode(), atomsTo, theory::THEORY_SAT_SOLVER);
1260
          continue;
1261
        }
1262
      }
1263
    }
1264
1265
    // If the theory is asking about a different form, or the form is ok but if will go to a different theory
1266
    // then we must figure it out
1267
5380
    if (eqNormalized != eq || Theory::theoryOf(eq) != atomsTo) {
1268
      // If you get eqNormalized, send atoms[i] to atomsTo
1269
4457
      d_atomRequests.add(eqNormalized, eq, atomsTo);
1270
    }
1271
  }
1272
55147
}
1273
1274
461320
void TheoryEngine::lemma(theory::TrustNode tlemma,
1275
                         theory::LemmaProperty p,
1276
                         theory::TheoryId atomsTo,
1277
                         theory::TheoryId from)
1278
{
1279
  // For resource-limiting (also does a time check).
1280
  // spendResource();
1281
461320
  Assert(tlemma.getKind() == TrustNodeKind::LEMMA
1282
         || tlemma.getKind() == TrustNodeKind::CONFLICT);
1283
  // get the node
1284
922640
  Node node = tlemma.getNode();
1285
922640
  Node lemma = tlemma.getProven();
1286
1287
461320
  Assert(!expr::hasFreeVar(lemma));
1288
1289
  // when proofs are enabled, we ensure the trust node has a generator by
1290
  // adding a trust step to the lazy proof maintained by this class
1291
461320
  if (isProofEnabled())
1292
  {
1293
    // ensure proof: set THEORY_LEMMA if no generator is provided
1294
64280
    if (tlemma.getGenerator() == nullptr)
1295
    {
1296
      // internal lemmas should have generators
1297
7464
      Assert(from != THEORY_LAST);
1298
      // add theory lemma step to proof
1299
14928
      Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(from);
1300
7464
      d_lazyProof->addStep(lemma, PfRule::THEORY_LEMMA, {}, {lemma, tidn});
1301
      // update the trust node
1302
7464
      tlemma = TrustNode::mkTrustLemma(lemma, d_lazyProof.get());
1303
    }
1304
    // ensure closed
1305
64280
    tlemma.debugCheckClosed("te-proof-debug", "TheoryEngine::lemma_initial");
1306
  }
1307
1308
  // Do we need to check atoms
1309
461320
  if (atomsTo != theory::THEORY_LAST) {
1310
55147
    Debug("theory::atoms") << "TheoryEngine::lemma(" << node << ", " << atomsTo << ")" << endl;
1311
110294
    AtomsCollect collectAtoms;
1312
55147
    NodeVisitor<AtomsCollect>::run(collectAtoms, node);
1313
55147
    ensureLemmaAtoms(collectAtoms.getAtoms(), atomsTo);
1314
  }
1315
1316
461320
  if(Dump.isOn("t-lemmas")) {
1317
    // we dump the negation of the lemma, to show validity of the lemma
1318
    Node n = lemma.negate();
1319
    const Printer& printer = d_outMgr.getPrinter();
1320
    std::ostream& out = d_outMgr.getDumpOut();
1321
    printer.toStreamCmdComment(out, "theory lemma: expect valid");
1322
    printer.toStreamCmdCheckSat(out, n);
1323
  }
1324
1325
  // assert the lemma
1326
461322
  d_propEngine->assertLemma(tlemma, p);
1327
1328
  // If specified, we must add this lemma to the set of those that need to be
1329
  // justified, where note we pass all auxiliary lemmas in skAsserts as well,
1330
  // since these by extension must be justified as well.
1331
461318
  if (d_relManager != nullptr && isLemmaPropertyNeedsJustify(p))
1332
  {
1333
    std::vector<Node> skAsserts;
1334
    std::vector<Node> sks;
1335
    Node retLemma =
1336
        d_propEngine->getPreprocessedTerm(tlemma.getProven(), skAsserts, sks);
1337
    d_relManager->notifyPreprocessedAssertion(retLemma);
1338
    d_relManager->notifyPreprocessedAssertions(skAsserts);
1339
  }
1340
1341
  // Mark that we added some lemmas
1342
461318
  d_lemmasAdded = true;
1343
461318
}
1344
1345
128153
void TheoryEngine::conflict(theory::TrustNode tconflict, TheoryId theoryId)
1346
{
1347
128153
  Assert(tconflict.getKind() == TrustNodeKind::CONFLICT);
1348
256306
  TNode conflict = tconflict.getNode();
1349
256306
  Trace("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", "
1350
128153
                            << theoryId << ")" << endl;
1351
128153
  Trace("te-proof-debug") << "Check closed conflict" << std::endl;
1352
  // doesn't require proof generator, yet, since THEORY_LEMMA is added below
1353
128153
  tconflict.debugCheckClosed(
1354
      "te-proof-debug", "TheoryEngine::conflict_initial", false);
1355
1356
128153
  Trace("dtview::conflict") << ":THEORY-CONFLICT: " << conflict << std::endl;
1357
1358
  // Mark that we are in conflict
1359
128153
  d_inConflict = true;
1360
1361
128153
  if(Dump.isOn("t-conflicts")) {
1362
    const Printer& printer = d_outMgr.getPrinter();
1363
    std::ostream& out = d_outMgr.getDumpOut();
1364
    printer.toStreamCmdComment(out, "theory conflict: expect unsat");
1365
    printer.toStreamCmdCheckSat(out, conflict);
1366
  }
1367
1368
  // In the multiple-theories case, we need to reconstruct the conflict
1369
128153
  if (d_logicInfo.isSharingEnabled()) {
1370
    // Create the workplace for explanations
1371
207306
    std::vector<NodeTheoryPair> vec;
1372
103653
    vec.push_back(
1373
207306
        NodeTheoryPair(conflict, theoryId, d_propagationMapTimestamp));
1374
1375
    // Process the explanation
1376
207306
    TrustNode tncExp = getExplanation(vec);
1377
207306
    Trace("te-proof-debug")
1378
103653
        << "Check closed conflict explained with sharing" << std::endl;
1379
103653
    tncExp.debugCheckClosed("te-proof-debug",
1380
                            "TheoryEngine::conflict_explained_sharing");
1381
207306
    Node fullConflict = tncExp.getNode();
1382
1383
103653
    if (isProofEnabled())
1384
    {
1385
14020
      Trace("te-proof-debug") << "Process conflict: " << conflict << std::endl;
1386
28040
      Trace("te-proof-debug") << "Conflict " << tconflict << " from "
1387
14020
                              << tconflict.identifyGenerator() << std::endl;
1388
28040
      Trace("te-proof-debug") << "Explanation " << tncExp << " from "
1389
14020
                              << tncExp.identifyGenerator() << std::endl;
1390
14020
      Assert(d_lazyProof != nullptr);
1391
14020
      if (tconflict.getGenerator() != nullptr)
1392
      {
1393
12661
        d_lazyProof->addLazyStep(tconflict.getProven(),
1394
                                 tconflict.getGenerator());
1395
      }
1396
      else
1397
      {
1398
        // add theory lemma step
1399
2718
        Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
1400
2718
        Node conf = tconflict.getProven();
1401
1359
        d_lazyProof->addStep(conf, PfRule::THEORY_LEMMA, {}, {conf, tidn});
1402
      }
1403
      // store the explicit step, which should come from a different
1404
      // generator, e.g. d_tepg.
1405
28040
      Node proven = tncExp.getProven();
1406
14020
      Assert(tncExp.getGenerator() != d_lazyProof.get());
1407
28040
      Trace("te-proof-debug") << "add lazy step " << tncExp.identifyGenerator()
1408
14020
                              << " for " << proven << std::endl;
1409
14020
      d_lazyProof->addLazyStep(proven, tncExp.getGenerator());
1410
14020
      pfgEnsureClosed(proven,
1411
14020
                      d_lazyProof.get(),
1412
                      "te-proof-debug",
1413
                      "TheoryEngine::conflict_during");
1414
28040
      Node fullConflictNeg = fullConflict.notNode();
1415
28040
      std::vector<Node> children;
1416
14020
      children.push_back(proven);
1417
28040
      std::vector<Node> args;
1418
14020
      args.push_back(fullConflictNeg);
1419
14020
      if (conflict == d_false)
1420
      {
1421
111
        AlwaysAssert(proven == fullConflictNeg);
1422
      }
1423
      else
1424
      {
1425
13909
        if (fullConflict != conflict)
1426
        {
1427
          // ------------------------- explained  ---------- from theory
1428
          // fullConflict => conflict              ~conflict
1429
          // ------------------------------------------ MACRO_SR_PRED_TRANSFORM
1430
          // ~fullConflict
1431
13433
          children.push_back(conflict.notNode());
1432
13433
          args.push_back(mkMethodId(MethodId::SB_LITERAL));
1433
13433
          d_lazyProof->addStep(
1434
              fullConflictNeg, PfRule::MACRO_SR_PRED_TRANSFORM, children, args);
1435
        }
1436
      }
1437
    }
1438
    // pass the processed trust node
1439
    TrustNode tconf =
1440
207306
        TrustNode::mkTrustConflict(fullConflict, d_lazyProof.get());
1441
103653
    Debug("theory::conflict") << "TheoryEngine::conflict(" << conflict << ", " << theoryId << "): full = " << fullConflict << endl;
1442
103653
    Assert(properConflict(fullConflict));
1443
207306
    Trace("te-proof-debug")
1444
103653
        << "Check closed conflict with sharing" << std::endl;
1445
103653
    tconf.debugCheckClosed("te-proof-debug", "TheoryEngine::conflict:sharing");
1446
103653
    lemma(tconf, LemmaProperty::REMOVABLE);
1447
  } else {
1448
    // When only one theory, the conflict should need no processing
1449
24500
    Assert(properConflict(conflict));
1450
    // pass the trust node that was sent from the theory
1451
24500
    lemma(tconflict, LemmaProperty::REMOVABLE, THEORY_LAST, theoryId);
1452
  }
1453
128153
}
1454
1455
178665
theory::TrustNode TheoryEngine::getExplanation(
1456
    std::vector<NodeTheoryPair>& explanationVector)
1457
{
1458
178665
  Assert(explanationVector.size() == 1);
1459
357330
  Node conclusion = explanationVector[0].d_node;
1460
357330
  std::shared_ptr<LazyCDProof> lcp;
1461
178665
  if (isProofEnabled())
1462
  {
1463
40546
    Trace("te-proof-exp") << "=== TheoryEngine::getExplanation " << conclusion
1464
20273
                          << std::endl;
1465
40546
    lcp.reset(new LazyCDProof(
1466
20273
        d_pnm, nullptr, nullptr, "TheoryEngine::LazyCDProof::getExplanation"));
1467
  }
1468
178665
  unsigned i = 0; // Index of the current literal we are processing
1469
1470
357330
  std::unique_ptr<std::set<Node>> inputAssertions = nullptr;
1471
  // the overall explanation
1472
357330
  std::set<TNode> exp;
1473
  // vector of trust nodes to explain at the end
1474
357330
  std::vector<std::pair<TheoryId, TrustNode>> texplains;
1475
  // cache of nodes we have already explained by some theory
1476
357330
  std::unordered_map<Node, size_t, NodeHashFunction> cache;
1477
1478
8738957
  while (i < explanationVector.size()) {
1479
    // Get the current literal to explain
1480
4686567
    NodeTheoryPair toExplain = explanationVector[i];
1481
1482
8560292
    Debug("theory::explain")
1483
4280146
        << "[i=" << i << "] TheoryEngine::explain(): processing ["
1484
4280146
        << toExplain.d_timestamp << "] " << toExplain.d_node << " sent from "
1485
4280146
        << toExplain.d_theory << endl;
1486
1487
8735046
    if (cache.find(toExplain.d_node) != cache.end()
1488
4280146
        && cache[toExplain.d_node] < toExplain.d_timestamp)
1489
    {
1490
174754
      ++i;
1491
174754
      continue;
1492
    }
1493
4105392
    cache[toExplain.d_node] = toExplain.d_timestamp;
1494
1495
    // If a true constant or a negation of a false constant we can ignore it
1496
8223589
    if ((toExplain.d_node.isConst() && toExplain.d_node.getConst<bool>())
1497
12316176
        || (toExplain.d_node.getKind() == kind::NOT
1498
4569121
            && toExplain.d_node[0].isConst()
1499
4105392
            && !toExplain.d_node[0].getConst<bool>()))
1500
    {
1501
12418
      ++ i;
1502
      // if we are building a proof
1503
12418
      if (lcp != nullptr)
1504
      {
1505
2884
        Trace("te-proof-exp")
1506
1442
            << "- explain " << toExplain.d_node << " trivially..." << std::endl;
1507
        // ------------------MACRO_SR_PRED_INTRO
1508
        // toExplain.d_node
1509
2884
        std::vector<Node> children;
1510
2884
        std::vector<Node> args;
1511
1442
        args.push_back(toExplain.d_node);
1512
1442
        lcp->addStep(
1513
            toExplain.d_node, PfRule::MACRO_SR_PRED_INTRO, children, args);
1514
      }
1515
12418
      continue;
1516
    }
1517
1518
    // If from the SAT solver, keep it
1519
5502793
    if (toExplain.d_theory == THEORY_SAT_SOLVER)
1520
    {
1521
1409819
      Debug("theory::explain") << "\tLiteral came from THEORY_SAT_SOLVER. Kepping it." << endl;
1522
1409819
      exp.insert(explanationVector[i++].d_node);
1523
      // it will be a free assumption in the proof
1524
1409819
      Trace("te-proof-exp") << "- keep " << toExplain.d_node << std::endl;
1525
1409819
      continue;
1526
    }
1527
1528
    // If an and, expand it
1529
2683155
    if (toExplain.d_node.getKind() == kind::AND)
1530
    {
1531
817128
      Debug("theory::explain")
1532
408564
          << "TheoryEngine::explain(): expanding " << toExplain.d_node
1533
408564
          << " got from " << toExplain.d_theory << endl;
1534
408564
      size_t nchild = toExplain.d_node.getNumChildren();
1535
2235454
      for (size_t k = 0; k < nchild; ++k)
1536
      {
1537
        NodeTheoryPair newExplain(
1538
3653780
            toExplain.d_node[k], toExplain.d_theory, toExplain.d_timestamp);
1539
1826890
        explanationVector.push_back(newExplain);
1540
      }
1541
408564
      if (lcp != nullptr)
1542
      {
1543
114912
        Trace("te-proof-exp")
1544
57456
            << "- AND expand " << toExplain.d_node << std::endl;
1545
        // delay explanation, use a dummy trust node
1546
        TrustNode tnAndExp = TrustNode::mkTrustPropExp(
1547
114912
            toExplain.d_node, toExplain.d_node, nullptr);
1548
57456
        texplains.push_back(
1549
114912
            std::pair<TheoryId, TrustNode>(THEORY_LAST, tnAndExp));
1550
      }
1551
408564
      ++ i;
1552
408564
      continue;
1553
    }
1554
1555
    // See if it was sent to the theory by another theory
1556
2274591
    PropagationMap::const_iterator find = d_propagationMap.find(toExplain);
1557
2274591
    if (find != d_propagationMap.end()) {
1558
4296884
      Debug("theory::explain")
1559
2148442
          << "\tTerm was propagated by another theory (theory = "
1560
2148442
          << getTheoryString((*find).second.d_theory) << ")" << std::endl;
1561
      // There is some propagation, check if its a timely one
1562
2148442
      if ((*find).second.d_timestamp < toExplain.d_timestamp)
1563
      {
1564
3736340
        Debug("theory::explain")
1565
1868170
            << "\tRelevant timetsamp, pushing " << (*find).second.d_node
1566
1868170
            << "to index = " << explanationVector.size() << std::endl;
1567
1868170
        explanationVector.push_back((*find).second);
1568
1868170
        ++i;
1569
1570
1868170
        if (lcp != nullptr)
1571
        {
1572
248405
          if (!CDProof::isSame(toExplain.d_node, (*find).second.d_node))
1573
          {
1574
6736
            Trace("te-proof-exp")
1575
3368
                << "- t-explained cached: " << toExplain.d_node << " by "
1576
3368
                << (*find).second.d_node << std::endl;
1577
            // delay explanation, use a dummy trust node that says that
1578
            // (*find).second.d_node explains toExplain.d_node.
1579
            TrustNode tnRewExp = TrustNode::mkTrustPropExp(
1580
6736
                toExplain.d_node, (*find).second.d_node, nullptr);
1581
3368
            texplains.push_back(
1582
6736
                std::pair<TheoryId, TrustNode>(THEORY_LAST, tnRewExp));
1583
          }
1584
        }
1585
1868170
        continue;
1586
      }
1587
    }
1588
    // It was produced by the theory, so ask for an explanation
1589
    TrustNode texplanation =
1590
812842
        d_sharedSolver->explain(toExplain.d_node, toExplain.d_theory);
1591
406421
    if (lcp != nullptr)
1592
    {
1593
60296
      texplanation.debugCheckClosed("te-proof-exp", "texplanation", false);
1594
120592
      Trace("te-proof-exp")
1595
60296
          << "- t-explained[" << toExplain.d_theory << "]: " << toExplain.d_node
1596
60296
          << " by " << texplanation.getNode() << std::endl;
1597
      // should prove the propagation we asked for
1598
60296
      Assert(texplanation.getKind() == TrustNodeKind::PROP_EXP
1599
             && texplanation.getProven()[1] == toExplain.d_node);
1600
      // if not a trivial explanation
1601
60296
      if (!CDProof::isSame(texplanation.getNode(), toExplain.d_node))
1602
      {
1603
        // We add it to the list of theory explanations, to be processed at
1604
        // the end of this method. We wait to explain here because it may
1605
        // be that a later explanation may preempt the need for proving this
1606
        // step. For instance, if the conclusion lit is later added as an
1607
        // assumption in the final explanation. This avoids cyclic proofs.
1608
54334
        texplains.push_back(
1609
108668
            std::pair<TheoryId, TrustNode>(toExplain.d_theory, texplanation));
1610
      }
1611
    }
1612
812842
    Node explanation = texplanation.getNode();
1613
1614
812842
    Debug("theory::explain")
1615
406421
        << "TheoryEngine::explain(): got explanation " << explanation
1616
406421
        << " got from " << toExplain.d_theory << endl;
1617
406421
    Assert(explanation != toExplain.d_node)
1618
        << "wasn't sent to you, so why are you explaining it trivially";
1619
    // Mark the explanation
1620
    NodeTheoryPair newExplain(
1621
812842
        explanation, toExplain.d_theory, toExplain.d_timestamp);
1622
406421
    explanationVector.push_back(newExplain);
1623
1624
406421
    ++ i;
1625
  }
1626
1627
  // make the explanation node
1628
357330
  Node expNode;
1629
178665
  if (exp.size() == 0)
1630
  {
1631
    // Normalize to true
1632
21
    expNode = NodeManager::currentNM()->mkConst<bool>(true);
1633
  }
1634
178644
  else if (exp.size() == 1)
1635
  {
1636
    // All the same, or just one
1637
5484
    expNode = *exp.begin();
1638
  }
1639
  else
1640
  {
1641
346320
    NodeBuilder<> conjunction(kind::AND);
1642
173160
    std::set<TNode>::const_iterator it = exp.begin();
1643
173160
    std::set<TNode>::const_iterator it_end = exp.end();
1644
2894064
    while (it != it_end)
1645
    {
1646
1360452
      conjunction << *it;
1647
1360452
      ++it;
1648
    }
1649
173160
    expNode = conjunction;
1650
  }
1651
  // if we are building a proof, go back through the explanations and
1652
  // build the proof
1653
178665
  if (lcp != nullptr)
1654
  {
1655
20273
    if (Trace.isOn("te-proof-exp"))
1656
    {
1657
      Trace("te-proof-exp") << "Explanation is:" << std::endl;
1658
      for (TNode e : exp)
1659
      {
1660
        Trace("te-proof-exp") << "  " << e << std::endl;
1661
      }
1662
      Trace("te-proof-exp") << "=== Replay explanations..." << std::endl;
1663
    }
1664
    // Now, go back and add the necessary steps of theory explanations, i.e.
1665
    // add those that prove things that aren't in the final explanation. We
1666
    // iterate in reverse order so that most recent steps take priority. This
1667
    // avoids cyclic proofs in the lazy proof we are building (lcp).
1668
115158
    for (std::vector<std::pair<TheoryId, TrustNode>>::reverse_iterator
1669
20273
             it = texplains.rbegin(),
1670
20273
             itEnd = texplains.rend();
1671
135431
         it != itEnd;
1672
         ++it)
1673
    {
1674
167284
      TrustNode trn = it->second;
1675
115158
      Assert(trn.getKind() == TrustNodeKind::PROP_EXP);
1676
167284
      Node proven = trn.getProven();
1677
115158
      Assert(proven.getKind() == kind::IMPLIES);
1678
167284
      Node tConc = proven[1];
1679
115158
      Trace("te-proof-exp") << "- Process " << trn << std::endl;
1680
120351
      if (exp.find(tConc) != exp.end())
1681
      {
1682
        // already added to proof
1683
5193
        Trace("te-proof-exp") << "...already added" << std::endl;
1684
5193
        continue;
1685
      }
1686
162091
      Node symTConc = CDProof::getSymmFact(tConc);
1687
109965
      if (!symTConc.isNull())
1688
      {
1689
51943
        if (exp.find(symTConc) != exp.end())
1690
        {
1691
          // symmetric direction
1692
32
          Trace("te-proof-exp") << "...already added (SYMM)" << std::endl;
1693
32
          continue;
1694
        }
1695
      }
1696
      // remember that we've explained this formula, to avoid cycles in lcp
1697
109933
      exp.insert(tConc);
1698
109933
      TheoryId ttid = it->first;
1699
162059
      Node tExp = proven[0];
1700
109933
      if (ttid == THEORY_LAST)
1701
      {
1702
57807
        if (tConc == tExp)
1703
        {
1704
          // dummy trust node, do AND expansion
1705
55673
          Assert(tConc.getKind() == kind::AND);
1706
          // tConc[0] ... tConc[n]
1707
          // ---------------------- AND_INTRO
1708
          // tConc
1709
111346
          std::vector<Node> pfChildren;
1710
55673
          pfChildren.insert(pfChildren.end(), tConc.begin(), tConc.end());
1711
55673
          lcp->addStep(tConc, PfRule::AND_INTRO, pfChildren, {});
1712
55673
          Trace("te-proof-exp") << "...via AND_INTRO" << std::endl;
1713
55673
          continue;
1714
        }
1715
        // otherwise should hold by rewriting
1716
2134
        Assert(Rewriter::rewrite(tConc) == Rewriter::rewrite(tExp));
1717
        // tExp
1718
        // ---- MACRO_SR_PRED_TRANSFORM
1719
        // tConc
1720
2134
        lcp->addStep(tConc, PfRule::MACRO_SR_PRED_TRANSFORM, {tExp}, {tConc});
1721
2134
        Trace("te-proof-exp") << "...via MACRO_SR_PRED_TRANSFORM" << std::endl;
1722
2134
        continue;
1723
      }
1724
52126
      if (tExp == tConc)
1725
      {
1726
        // trivial
1727
        Trace("te-proof-exp") << "...trivial" << std::endl;
1728
        continue;
1729
      }
1730
      //       ------------- Via theory
1731
      // tExp  tExp => tConc
1732
      // ---------------------------------MODUS_PONENS
1733
      // tConc
1734
52126
      if (trn.getGenerator() != nullptr)
1735
      {
1736
49260
        Trace("te-proof-exp") << "...via theory generator" << std::endl;
1737
49260
        lcp->addLazyStep(proven, trn.getGenerator());
1738
      }
1739
      else
1740
      {
1741
2866
        Trace("te-proof-exp") << "...via trust THEORY_LEMMA" << std::endl;
1742
        // otherwise, trusted theory lemma
1743
5732
        Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(it->first);
1744
2866
        lcp->addStep(proven, PfRule::THEORY_LEMMA, {}, {proven, tidn});
1745
      }
1746
104252
      std::vector<Node> pfChildren;
1747
52126
      pfChildren.push_back(trn.getNode());
1748
52126
      pfChildren.push_back(proven);
1749
52126
      lcp->addStep(tConc, PfRule::MODUS_PONENS, pfChildren, {});
1750
    }
1751
    // store in the proof generator
1752
40546
    TrustNode trn = d_tepg->mkTrustExplain(conclusion, expNode, lcp);
1753
    // return the trust node
1754
20273
    return trn;
1755
  }
1756
1757
158392
  return theory::TrustNode::mkTrustLemma(expNode, nullptr);
1758
}
1759
1760
803764
bool TheoryEngine::isProofEnabled() const { return d_pnm != nullptr; }
1761
1762
109
void TheoryEngine::setUserAttribute(const std::string& attr,
1763
                                    Node n,
1764
                                    const std::vector<Node>& node_values,
1765
                                    const std::string& str_value)
1766
{
1767
109
  Trace("te-attr") << "set user attribute " << attr << " " << n << endl;
1768
109
  if( d_attr_handle.find( attr )!=d_attr_handle.end() ){
1769
218
    for( size_t i=0; i<d_attr_handle[attr].size(); i++ ){
1770
109
      d_attr_handle[attr][i]->setUserAttribute(attr, n, node_values, str_value);
1771
    }
1772
  } else {
1773
    //unhandled exception?
1774
  }
1775
109
}
1776
1777
44985
void TheoryEngine::handleUserAttribute(const char* attr, Theory* t) {
1778
44985
  Trace("te-attr") << "Handle user attribute " << attr << " " << t << endl;
1779
89970
  std::string str( attr );
1780
44985
  d_attr_handle[ str ].push_back( t );
1781
44985
}
1782
1783
1942
void TheoryEngine::checkTheoryAssertionsWithModel(bool hardFailure) {
1784
27188
  for(TheoryId theoryId = THEORY_FIRST; theoryId < THEORY_LAST; ++theoryId) {
1785
25246
    Theory* theory = d_theoryTable[theoryId];
1786
25246
    if(theory && d_logicInfo.isTheoryEnabled(theoryId)) {
1787
105877
      for(context::CDList<Assertion>::const_iterator it = theory->facts_begin(),
1788
11035
            it_end = theory->facts_end();
1789
105877
          it != it_end;
1790
          ++it) {
1791
189684
        Node assertion = (*it).d_assertion;
1792
94842
        if (!isRelevant(assertion))
1793
        {
1794
          // not relevant, skip
1795
          continue;
1796
        }
1797
189684
        Node val = d_tc->getModel()->getValue(assertion);
1798
94842
        if (val != d_true)
1799
        {
1800
10
          std::stringstream ss;
1801
10
          ss << " " << theoryId
1802
10
             << " has an asserted fact that the model doesn't satisfy." << endl
1803
10
             << "The fact: " << assertion << endl
1804
5
             << "Model value: " << val << endl;
1805
5
          if (hardFailure)
1806
          {
1807
5
            if (val == d_false)
1808
            {
1809
              // Always an error if it is false
1810
              InternalError() << ss.str();
1811
            }
1812
            else
1813
            {
1814
              // Otherwise just a warning. Notice this case may happen for
1815
              // assertions with unevaluable operators, e.g. transcendental
1816
              // functions. It also may happen for separation logic, where
1817
              // check-model support is limited.
1818
5
              Warning() << ss.str();
1819
            }
1820
          }
1821
        }
1822
      }
1823
    }
1824
  }
1825
1942
}
1826
1827
5250
std::pair<bool, Node> TheoryEngine::entailmentCheck(options::TheoryOfMode mode,
1828
                                                    TNode lit)
1829
{
1830
10500
  TNode atom = (lit.getKind() == kind::NOT) ? lit[0] : lit;
1831
5250
  if( atom.getKind()==kind::AND || atom.getKind()==kind::OR || atom.getKind()==kind::IMPLIES ){
1832
    //Boolean connective, recurse
1833
    std::vector< Node > children;
1834
    bool pol = (lit.getKind()!=kind::NOT);
1835
    bool is_conjunction = pol==(lit.getKind()==kind::AND);
1836
    for( unsigned i=0; i<atom.getNumChildren(); i++ ){
1837
      Node ch = atom[i];
1838
      if( pol==( lit.getKind()==kind::IMPLIES && i==0 ) ){
1839
        ch = atom[i].negate();
1840
      }
1841
      std::pair<bool, Node> chres = entailmentCheck(mode, ch);
1842
      if( chres.first ){
1843
        if( !is_conjunction ){
1844
          return chres;
1845
        }else{
1846
          children.push_back( chres.second );
1847
        }
1848
      }else if( !chres.first && is_conjunction ){
1849
        return std::pair<bool, Node>(false, Node::null());
1850
      }
1851
    }
1852
    if( is_conjunction ){
1853
      return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, children));
1854
    }else{
1855
      return std::pair<bool, Node>(false, Node::null());
1856
    }
1857
5250
  }else if( atom.getKind()==kind::ITE || ( atom.getKind()==kind::EQUAL && atom[0].getType().isBoolean() ) ){
1858
    bool pol = (lit.getKind()!=kind::NOT);
1859
    for( unsigned r=0; r<2; r++ ){
1860
      Node ch = atom[0];
1861
      if( r==1 ){
1862
        ch = ch.negate();
1863
      }
1864
      std::pair<bool, Node> chres = entailmentCheck(mode, ch);
1865
      if( chres.first ){
1866
        Node ch2 = atom[ atom.getKind()==kind::ITE ? r+1 : 1 ];
1867
        if( pol==( atom.getKind()==kind::ITE ? true : r==1 ) ){
1868
          ch2 = ch2.negate();
1869
        }
1870
        std::pair<bool, Node> chres2 = entailmentCheck(mode, ch2);
1871
        if( chres2.first ){
1872
          return std::pair<bool, Node>(true, NodeManager::currentNM()->mkNode(kind::AND, chres.second, chres2.second));
1873
        }else{
1874
          break;
1875
        }
1876
      }
1877
    }
1878
    return std::pair<bool, Node>(false, Node::null());
1879
  }else{
1880
    //it is a theory atom
1881
5250
    theory::TheoryId tid = theory::Theory::theoryOf(mode, atom);
1882
5250
    theory::Theory* th = theoryOf(tid);
1883
1884
5250
    Assert(th != NULL);
1885
5250
    Trace("theory-engine-entc") << "Entailment check : " << lit << std::endl;
1886
1887
10500
    std::pair<bool, Node> chres = th->entailmentCheck(lit);
1888
5250
    return chres;
1889
  }
1890
}
1891
1892
29844534
void TheoryEngine::spendResource(ResourceManager::Resource r)
1893
{
1894
29844534
  d_resourceManager->spendResource(r);
1895
29844534
}
1896
1897
26685
}/* CVC4 namespace */