GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory.cpp Lines: 208 247 84.2 %
Date: 2021-03-22 Branches: 391 861 45.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Tim King, Dejan Jovanovic
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 Base for theory interface.
13
 **
14
 ** Base for theory interface.
15
 **/
16
17
#include "theory/theory.h"
18
19
#include <iostream>
20
#include <sstream>
21
#include <string>
22
#include <vector>
23
24
#include "base/check.h"
25
#include "expr/node_algorithm.h"
26
#include "options/smt_options.h"
27
#include "options/theory_options.h"
28
#include "smt/smt_statistics_registry.h"
29
#include "theory/ee_setup_info.h"
30
#include "theory/ext_theory.h"
31
#include "theory/output_channel.h"
32
#include "theory/quantifiers_engine.h"
33
#include "theory/substitutions.h"
34
#include "theory/theory_inference_manager.h"
35
#include "theory/theory_model.h"
36
#include "theory/theory_rewriter.h"
37
#include "theory/theory_state.h"
38
#include "theory/trust_substitutions.h"
39
40
using namespace std;
41
42
namespace CVC4 {
43
namespace theory {
44
45
/** Default value for the uninterpreted sorts is the UF theory */
46
TheoryId Theory::s_uninterpretedSortOwner = THEORY_UF;
47
48
std::ostream& operator<<(std::ostream& os, Theory::Effort level){
49
  switch(level){
50
  case Theory::EFFORT_STANDARD:
51
    os << "EFFORT_STANDARD"; break;
52
  case Theory::EFFORT_FULL:
53
    os << "EFFORT_FULL"; break;
54
  case Theory::EFFORT_LAST_CALL:
55
    os << "EFFORT_LAST_CALL"; break;
56
  default:
57
      Unreachable();
58
  }
59
  return os;
60
}/* ostream& operator<<(ostream&, Theory::Effort) */
61
62
116977
Theory::Theory(TheoryId id,
63
               context::Context* satContext,
64
               context::UserContext* userContext,
65
               OutputChannel& out,
66
               Valuation valuation,
67
               const LogicInfo& logicInfo,
68
               ProofNodeManager* pnm,
69
116977
               std::string name)
70
    : d_id(id),
71
      d_satContext(satContext),
72
      d_userContext(userContext),
73
      d_logicInfo(logicInfo),
74
      d_facts(satContext),
75
      d_factsHead(satContext, 0),
76
      d_sharedTermsIndex(satContext, 0),
77
      d_careGraph(nullptr),
78
      d_decManager(nullptr),
79
      d_instanceName(name),
80
233954
      d_checkTime(getStatsPrefix(id) + name + "::checkTime"),
81
233954
      d_computeCareGraphTime(getStatsPrefix(id) + name
82
233954
                             + "::computeCareGraphTime"),
83
      d_sharedTerms(satContext),
84
      d_out(&out),
85
      d_valuation(valuation),
86
      d_equalityEngine(nullptr),
87
      d_allocEqualityEngine(nullptr),
88
      d_theoryState(nullptr),
89
      d_inferManager(nullptr),
90
      d_quantEngine(nullptr),
91
584885
      d_pnm(pnm)
92
{
93
116977
  smtStatisticsRegistry()->registerStat(&d_checkTime);
94
116977
  smtStatisticsRegistry()->registerStat(&d_computeCareGraphTime);
95
116977
}
96
97
233876
Theory::~Theory() {
98
116938
  smtStatisticsRegistry()->unregisterStat(&d_checkTime);
99
116938
  smtStatisticsRegistry()->unregisterStat(&d_computeCareGraphTime);
100
116938
}
101
102
17990
bool Theory::needsEqualityEngine(EeSetupInfo& esi)
103
{
104
  // by default, this theory does not use an (official) equality engine
105
17990
  return false;
106
}
107
108
116935
void Theory::setEqualityEngine(eq::EqualityEngine* ee)
109
{
110
  // set the equality engine pointer
111
116935
  d_equalityEngine = ee;
112
116935
  if (d_theoryState != nullptr)
113
  {
114
98945
    d_theoryState->setEqualityEngine(ee);
115
  }
116
116935
  if (d_inferManager != nullptr)
117
  {
118
98945
    d_inferManager->setEqualityEngine(ee);
119
  }
120
116935
}
121
122
116935
void Theory::setQuantifiersEngine(QuantifiersEngine* qe)
123
{
124
  // quantifiers engine may be null if not in quantified logic
125
116935
  d_quantEngine = qe;
126
116935
}
127
128
116935
void Theory::setDecisionManager(DecisionManager* dm)
129
{
130
116935
  Assert(d_decManager == nullptr);
131
116935
  Assert(dm != nullptr);
132
116935
  d_decManager = dm;
133
116935
}
134
135
void Theory::finishInitStandalone()
136
{
137
  EeSetupInfo esi;
138
  if (needsEqualityEngine(esi))
139
  {
140
    // always associated with the same SAT context as the theory (d_satContext)
141
    d_allocEqualityEngine.reset(new eq::EqualityEngine(
142
        *esi.d_notify, d_satContext, esi.d_name, esi.d_constantsAreTriggers));
143
    // use it as the official equality engine
144
    setEqualityEngine(d_allocEqualityEngine.get());
145
  }
146
  finishInit();
147
}
148
149
158874271
TheoryId Theory::theoryOf(options::TheoryOfMode mode, TNode node)
150
{
151
158874271
  TheoryId tid = THEORY_BUILTIN;
152
158874271
  switch(mode) {
153
93077638
    case options::TheoryOfMode::THEORY_OF_TYPE_BASED:
154
      // Constants, variables, 0-ary constructors
155
93077638
      if (node.isVar())
156
      {
157
3836608
        if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
158
        {
159
217514
          tid = THEORY_UF;
160
        }
161
        else
162
        {
163
3619094
          tid = Theory::theoryOf(node.getType());
164
        }
165
      }
166
89241030
      else if (node.getKind() == kind::EQUAL)
167
      {
168
        // Equality is owned by the theory that owns the domain
169
5505644
        tid = Theory::theoryOf(node[0].getType());
170
      }
171
      else
172
      {
173
        // Regular nodes are owned by the kind. Notice that constants are a
174
        // special case here, where the theory of the kind of a constant
175
        // always coincides with the type of that constant.
176
83735386
        tid = kindToTheoryId(node.getKind());
177
      }
178
93077638
      break;
179
65796633
    case options::TheoryOfMode::THEORY_OF_TERM_BASED:
180
      // Variables
181
65796633
      if (node.isVar())
182
      {
183
5842568
        if (Theory::theoryOf(node.getType()) != theory::THEORY_BOOL)
184
        {
185
          // We treat the variables as uninterpreted
186
5816227
          tid = s_uninterpretedSortOwner;
187
        }
188
        else
189
        {
190
26341
          if (node.getKind() == kind::BOOLEAN_TERM_VARIABLE)
191
          {
192
            // Boolean vars go to UF
193
18500
            tid = THEORY_UF;
194
          }
195
          else
196
          {
197
            // Except for the Boolean ones
198
7841
            tid = THEORY_BOOL;
199
          }
200
        }
201
      }
202
59954065
      else if (node.getKind() == kind::EQUAL)
203
      {  // Equality
204
        // If one of them is an ITE, it's irelevant, since they will get
205
        // replaced out anyhow
206
6170647
        if (node[0].getKind() == kind::ITE)
207
        {
208
4997
          tid = Theory::theoryOf(node[0].getType());
209
        }
210
6165650
        else if (node[1].getKind() == kind::ITE)
211
        {
212
11613
          tid = Theory::theoryOf(node[1].getType());
213
        }
214
        else
215
        {
216
12308074
          TNode l = node[0];
217
12308074
          TNode r = node[1];
218
12308074
          TypeNode ltype = l.getType();
219
12308074
          TypeNode rtype = r.getType();
220
6154037
          if (ltype != rtype)
221
          {
222
44669
            tid = Theory::theoryOf(l.getType());
223
          }
224
          else
225
          {
226
            // If both sides belong to the same theory the choice is easy
227
6109368
            TheoryId T1 = Theory::theoryOf(l);
228
6109368
            TheoryId T2 = Theory::theoryOf(r);
229
6109368
            if (T1 == T2)
230
            {
231
3215414
              tid = T1;
232
            }
233
            else
234
            {
235
2893954
              TheoryId T3 = Theory::theoryOf(ltype);
236
              // This is a case of
237
              // * x*y = f(z) -> UF
238
              // * x = c      -> UF
239
              // * f(x) = read(a, y) -> either UF or ARRAY
240
              // at least one of the theories has to be parametric, i.e. theory
241
              // of the type is different from the theory of the term
242
2893954
              if (T1 == T3)
243
              {
244
55639
                tid = T2;
245
              }
246
2838315
              else if (T2 == T3)
247
              {
248
2753454
                tid = T1;
249
              }
250
              else
251
              {
252
                // If both are parametric, we take the smaller one (arbitrary)
253
84861
                tid = T1 < T2 ? T1 : T2;
254
              }
255
            }
256
          }
257
        }
258
      }
259
      else
260
      {
261
        // Regular nodes are owned by the kind, which includes constants as a
262
        // special case.
263
53783418
        tid = kindToTheoryId(node.getKind());
264
      }
265
65796633
    break;
266
  default:
267
    Unreachable();
268
  }
269
158874271
  Trace("theory::internal") << "theoryOf(" << mode << ", " << node << ") -> " << tid << std::endl;
270
158874271
  return tid;
271
}
272
273
1182224
void Theory::notifySharedTerm(TNode n)
274
{
275
  // do nothing
276
1182224
}
277
278
5830
void Theory::computeCareGraph() {
279
5830
  Debug("sharing") << "Theory::computeCareGraph<" << getId() << ">()" << endl;
280
6326
  for (unsigned i = 0; i < d_sharedTerms.size(); ++ i) {
281
992
    TNode a = d_sharedTerms[i];
282
992
    TypeNode aType = a.getType();
283
4822
    for (unsigned j = i + 1; j < d_sharedTerms.size(); ++ j) {
284
8196
      TNode b = d_sharedTerms[j];
285
4326
      if (b.getType() != aType) {
286
        // We don't care about the terms of different types
287
456
        continue;
288
      }
289
3870
      switch (d_valuation.getEqualityStatus(a, b)) {
290
3244
      case EQUALITY_TRUE_AND_PROPAGATED:
291
      case EQUALITY_FALSE_AND_PROPAGATED:
292
        // If we know about it, we should have propagated it, so we can skip
293
3244
        break;
294
626
      default:
295
        // Let's split on it
296
626
        addCarePair(a, b);
297
626
        break;
298
      }
299
    }
300
  }
301
5830
}
302
303
void Theory::printFacts(std::ostream& os) const {
304
  unsigned i, n = d_facts.size();
305
  for(i = 0; i < n; i++){
306
    const Assertion& a_i = d_facts[i];
307
    Node assertion  = a_i;
308
    os << d_id << '[' << i << ']' << " " << assertion << endl;
309
  }
310
}
311
312
void Theory::debugPrintFacts() const{
313
  DebugChannel.getStream() << "Theory::debugPrintFacts()" << endl;
314
  printFacts(DebugChannel.getStream());
315
}
316
317
15362
bool Theory::isLegalElimination(TNode x, TNode val)
318
{
319
15362
  Assert(x.isVar());
320
30724
  if (x.getKind() == kind::BOOLEAN_TERM_VARIABLE
321
15362
      || val.getKind() == kind::BOOLEAN_TERM_VARIABLE)
322
  {
323
    return false;
324
  }
325
15362
  if (expr::hasSubterm(val, x))
326
  {
327
4201
    return false;
328
  }
329
11161
  if (!val.getType().isSubtypeOf(x.getType()))
330
  {
331
    return false;
332
  }
333
11161
  if (!options::produceModels())
334
  {
335
    // don't care about the model, we are fine
336
8473
    return true;
337
  }
338
  // if there is a model object
339
2688
  TheoryModel* tm = d_valuation.getModel();
340
2688
  Assert(tm != nullptr);
341
2688
  return tm->isLegalElimination(x, val);
342
}
343
344
17182
std::unordered_set<TNode, TNodeHashFunction> Theory::currentlySharedTerms() const{
345
17182
  std::unordered_set<TNode, TNodeHashFunction> currentlyShared;
346
408804
  for (shared_terms_iterator i = shared_terms_begin(),
347
17182
           i_end = shared_terms_end(); i != i_end; ++i) {
348
391622
    currentlyShared.insert (*i);
349
  }
350
17182
  return currentlyShared;
351
}
352
353
113488
bool Theory::collectModelInfo(TheoryModel* m, const std::set<Node>& termSet)
354
{
355
  // if we are using an equality engine, assert it to the model
356
113488
  if (d_equalityEngine != nullptr)
357
  {
358
75582
    if (!m->assertEqualityEngine(d_equalityEngine, &termSet))
359
    {
360
      return false;
361
    }
362
  }
363
  // now, collect theory-specific value assigments
364
113488
  return collectModelValues(m, termSet);
365
}
366
367
117616
void Theory::computeRelevantTerms(std::set<Node>& termSet)
368
{
369
  // by default, there are no additional relevant terms
370
117616
}
371
372
42440
bool Theory::collectModelValues(TheoryModel* m, const std::set<Node>& termSet)
373
{
374
42440
  return true;
375
}
376
377
57409
Theory::PPAssertStatus Theory::ppAssert(TrustNode tin,
378
                                        TrustSubstitutionMap& outSubstitutions)
379
{
380
114818
  TNode in = tin.getNode();
381
57409
  if (in.getKind() == kind::EQUAL)
382
  {
383
    // (and (= x t) phi) can be replaced by phi[x/t] if
384
    // 1) x is a variable
385
    // 2) x is not in the term t
386
    // 3) x : T and t : S, then S <: T
387
66984
    if (in[0].isVar() && isLegalElimination(in[0], in[1])
388
63166
        && in[0].getKind() != kind::BOOLEAN_TERM_VARIABLE)
389
    {
390
8554
      outSubstitutions.addSubstitutionSolved(in[0], in[1], tin);
391
8554
      return PP_ASSERT_STATUS_SOLVED;
392
    }
393
29221
    if (in[1].isVar() && isLegalElimination(in[1], in[0])
394
29221
        && in[1].getKind() != kind::BOOLEAN_TERM_VARIABLE)
395
    {
396
271
      outSubstitutions.addSubstitutionSolved(in[1], in[0], tin);
397
271
      return PP_ASSERT_STATUS_SOLVED;
398
    }
399
9379
    if (in[0].isConst() && in[1].isConst())
400
    {
401
      if (in[0] != in[1])
402
      {
403
        return PP_ASSERT_STATUS_CONFLICT;
404
      }
405
    }
406
  }
407
408
48584
  return PP_ASSERT_STATUS_UNSOLVED;
409
}
410
411
std::pair<bool, Node> Theory::entailmentCheck(TNode lit)
412
{
413
  return make_pair(false, Node::null());
414
}
415
416
76149
void Theory::addCarePair(TNode t1, TNode t2) {
417
76149
  if (d_careGraph) {
418
76149
    d_careGraph->insert(CarePair(t1, t2, d_id));
419
  }
420
76149
}
421
422
74648
void Theory::getCareGraph(CareGraph* careGraph) {
423
74648
  Assert(careGraph != NULL);
424
425
74648
  Trace("sharing") << "Theory<" << getId() << ">::getCareGraph()" << std::endl;
426
149296
  TimerStat::CodeTimer computeCareGraphTime(d_computeCareGraphTime);
427
74648
  d_careGraph = careGraph;
428
74648
  computeCareGraph();
429
74648
  d_careGraph = NULL;
430
74648
}
431
432
17006
bool Theory::proofsEnabled() const
433
{
434
17006
  return d_pnm != nullptr;
435
}
436
437
18268
EqualityStatus Theory::getEqualityStatus(TNode a, TNode b)
438
{
439
  // if not using an equality engine, then by default we don't know the status
440
18268
  if (d_equalityEngine == nullptr)
441
  {
442
2266
    return EQUALITY_UNKNOWN;
443
  }
444
16002
  Trace("sharing") << "Theory<" << getId() << ">::getEqualityStatus(" << a << ", " << b << ")" << std::endl;
445
16002
  Assert(d_equalityEngine->hasTerm(a) && d_equalityEngine->hasTerm(b));
446
447
  // Check for equality (simplest)
448
16002
  if (d_equalityEngine->areEqual(a, b))
449
  {
450
    // The terms are implied to be equal
451
4953
    return EQUALITY_TRUE;
452
  }
453
454
  // Check for disequality
455
11049
  if (d_equalityEngine->areDisequal(a, b, false))
456
  {
457
    // The terms are implied to be dis-equal
458
3065
    return EQUALITY_FALSE;
459
  }
460
461
  // All other terms are unknown, which is conservative. A theory may override
462
  // this method if it knows more information.
463
7984
  return EQUALITY_UNKNOWN;
464
}
465
466
13996300
void Theory::check(Effort level)
467
{
468
  // see if we are already done (as an optimization)
469
13996300
  if (done() && level < EFFORT_FULL)
470
  {
471
18379101
    return;
472
  }
473
4913759
  Assert(d_theoryState!=nullptr);
474
  // standard calls for resource, stats
475
4913759
  d_out->spendResource(ResourceManager::Resource::TheoryCheckStep);
476
9613499
  TimerStat::CodeTimer checkTimer(d_checkTime);
477
9827518
  Trace("theory-check") << "Theory::preCheck " << level << " " << d_id
478
4913759
                        << std::endl;
479
  // pre-check at level
480
4913759
  if (preCheck(level))
481
  {
482
    // check aborted for a theory-specific reason
483
214019
    return;
484
  }
485
4699740
  Assert(d_theoryState != nullptr);
486
4699740
  Trace("theory-check") << "Theory::process fact queue " << d_id << std::endl;
487
  // process the pending fact queue
488
31941550
  while (!done() && !d_theoryState->isInConflict())
489
  {
490
    // Get the next assertion from the fact queue
491
21153778
    Assertion assertion = get();
492
21153778
    TNode fact = assertion.d_assertion;
493
27241816
    Trace("theory-check") << "Theory::preNotifyFact " << fact << " " << d_id
494
13620908
                          << std::endl;
495
13620908
    bool polarity = fact.getKind() != kind::NOT;
496
21153778
    TNode atom = polarity ? fact : fact[0];
497
    // call the pre-notify method
498
13620908
    if (preNotifyFact(atom, polarity, fact, assertion.d_isPreregistered, false))
499
    {
500
      // handled in theory-specific way that doesn't involve equality engine
501
6088038
      continue;
502
    }
503
15065740
    Trace("theory-check") << "Theory::assert " << fact << " " << d_id
504
7532870
                          << std::endl;
505
    // Theories that don't have an equality engine should always return true
506
    // for preNotifyFact
507
7532870
    Assert(d_equalityEngine != nullptr);
508
    // assert to the equality engine
509
7532870
    if (atom.getKind() == kind::EQUAL)
510
    {
511
5787907
      d_equalityEngine->assertEquality(atom, polarity, fact);
512
    }
513
    else
514
    {
515
1744966
      d_equalityEngine->assertPredicate(atom, polarity, fact);
516
    }
517
15065734
    Trace("theory-check") << "Theory::notifyFact " << fact << " " << d_id
518
7532867
                          << std::endl;
519
    // notify the theory of the new fact, which is not internal
520
7532867
    notifyFact(atom, polarity, fact, false);
521
  }
522
4699737
  Trace("theory-check") << "Theory::postCheck " << d_id << std::endl;
523
  // post-check at level
524
4699737
  postCheck(level);
525
4699736
  Trace("theory-check") << "Theory::finish check " << d_id << std::endl;
526
}
527
528
2083229
bool Theory::preCheck(Effort level) { return false; }
529
530
2
void Theory::postCheck(Effort level) {}
531
532
3003471
bool Theory::preNotifyFact(
533
    TNode atom, bool polarity, TNode fact, bool isPrereg, bool isInternal)
534
{
535
3003471
  return false;
536
}
537
538
1567
void Theory::notifyFact(TNode atom, bool polarity, TNode fact, bool isInternal)
539
{
540
1567
}
541
542
20495
void Theory::preRegisterTerm(TNode node) {}
543
544
2161806
void Theory::addSharedTerm(TNode n)
545
{
546
4323612
  Debug("sharing") << "Theory::addSharedTerm<" << getId() << ">(" << n << ")"
547
2161806
                   << std::endl;
548
4323612
  Debug("theory::assertions")
549
2161806
      << "Theory::addSharedTerm<" << getId() << ">(" << n << ")" << std::endl;
550
2161806
  d_sharedTerms.push_back(n);
551
  // now call theory-specific method notifySharedTerm
552
2161806
  notifySharedTerm(n);
553
  // if we have an equality engine, add the trigger term
554
2161806
  if (d_equalityEngine != nullptr)
555
  {
556
2156975
    d_equalityEngine->addTriggerTerm(n, d_id);
557
  }
558
2161806
}
559
560
274926
eq::EqualityEngine* Theory::getEqualityEngine()
561
{
562
  // get the assigned equality engine, which is a pointer stored in this class
563
274926
  return d_equalityEngine;
564
}
565
566
}/* CVC4::theory namespace */
567
26676
}/* CVC4 namespace */