GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_inference_manager.cpp Lines: 170 207 82.1 %
Date: 2021-03-23 Branches: 185 456 40.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_inference_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer, Mathias Preiner
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 An inference manager for Theory
13
 **/
14
15
#include "theory/theory_inference_manager.h"
16
17
#include "smt/smt_statistics_registry.h"
18
#include "theory/output_channel.h"
19
#include "theory/rewriter.h"
20
#include "theory/theory.h"
21
#include "theory/theory_state.h"
22
#include "theory/uf/equality_engine.h"
23
#include "theory/uf/proof_equality_engine.h"
24
25
using namespace CVC4::kind;
26
27
namespace CVC4 {
28
namespace theory {
29
30
98967
TheoryInferenceManager::TheoryInferenceManager(Theory& t,
31
                                               TheoryState& state,
32
                                               ProofNodeManager* pnm,
33
                                               const std::string& name,
34
98967
                                               bool cacheLemmas)
35
    : d_theory(t),
36
      d_theoryState(state),
37
98967
      d_out(t.getOutputChannel()),
38
      d_ee(nullptr),
39
      d_pnm(pnm),
40
      d_cacheLemmas(cacheLemmas),
41
      d_keep(t.getSatContext()),
42
98967
      d_lemmasSent(t.getUserContext()),
43
      d_numConflicts(0),
44
      d_numCurrentLemmas(0),
45
      d_numCurrentFacts(0),
46
197934
      d_conflictIdStats(name + "::inferencesConflict"),
47
197934
      d_factIdStats(name + "::inferencesFact"),
48
692769
      d_lemmaIdStats(name + "::inferencesLemma")
49
{
50
  // don't add true lemma
51
197934
  Node truen = NodeManager::currentNM()->mkConst(true);
52
98967
  d_lemmasSent.insert(truen);
53
98967
  smtStatisticsRegistry()->registerStat(&d_conflictIdStats);
54
98967
  smtStatisticsRegistry()->registerStat(&d_factIdStats);
55
98967
  smtStatisticsRegistry()->registerStat(&d_lemmaIdStats);
56
98967
}
57
58
197868
TheoryInferenceManager::~TheoryInferenceManager()
59
{
60
98934
  smtStatisticsRegistry()->unregisterStat(&d_conflictIdStats);
61
98934
  smtStatisticsRegistry()->unregisterStat(&d_factIdStats);
62
98934
  smtStatisticsRegistry()->unregisterStat(&d_lemmaIdStats);
63
98934
}
64
65
98967
void TheoryInferenceManager::setEqualityEngine(eq::EqualityEngine* ee)
66
{
67
98967
  d_ee = ee;
68
  // if proofs are enabled, also make a proof equality engine to wrap ee
69
  // if it is non-null
70
98967
  if (d_pnm != nullptr && d_ee != nullptr)
71
  {
72
12406
    d_pfee.reset(new eq::ProofEqEngine(d_theoryState.getSatContext(),
73
6203
                                       d_theoryState.getUserContext(),
74
6203
                                       *d_ee,
75
12406
                                       d_pnm));
76
  }
77
98967
}
78
79
20186
bool TheoryInferenceManager::isProofEnabled() const { return d_pnm != nullptr; }
80
81
995996
void TheoryInferenceManager::reset()
82
{
83
995996
  d_numConflicts = 0;
84
995996
  d_numCurrentLemmas = 0;
85
995996
  d_numCurrentFacts = 0;
86
995996
}
87
88
133791
bool TheoryInferenceManager::hasSent() const
89
{
90
267582
  return d_theoryState.isInConflict() || d_numCurrentLemmas > 0
91
259823
         || d_numCurrentFacts > 0;
92
}
93
94
8997
eq::ProofEqEngine* TheoryInferenceManager::getProofEqEngine()
95
{
96
8997
  return d_pfee.get();
97
}
98
99
10267
void TheoryInferenceManager::conflictEqConstantMerge(TNode a, TNode b)
100
{
101
10267
  if (!d_theoryState.isInConflict())
102
  {
103
19896
    TrustNode tconf = explainConflictEqConstantMerge(a, b);
104
9948
    d_theoryState.notifyInConflict();
105
9948
    d_out.trustedConflict(tconf);
106
  }
107
10267
}
108
109
88007
void TheoryInferenceManager::conflict(TNode conf, InferenceId id)
110
{
111
88007
  d_conflictIdStats << id;
112
88007
  d_theoryState.notifyInConflict();
113
88007
  d_out.conflict(conf);
114
88007
  ++d_numConflicts;
115
88007
}
116
117
17421
void TheoryInferenceManager::trustedConflict(TrustNode tconf, InferenceId id)
118
{
119
17421
  d_conflictIdStats << id;
120
17421
  d_theoryState.notifyInConflict();
121
17421
  d_out.trustedConflict(tconf);
122
17421
}
123
124
void TheoryInferenceManager::conflictExp(InferenceId id,
125
                                         PfRule pfr,
126
                                         const std::vector<Node>& exp,
127
                                         const std::vector<Node>& args)
128
{
129
  if (!d_theoryState.isInConflict())
130
  {
131
    // make the trust node
132
    TrustNode tconf = mkConflictExp(pfr, exp, args);
133
    // send it on the output channel
134
    trustedConflict(tconf, id);
135
  }
136
}
137
138
TrustNode TheoryInferenceManager::mkConflictExp(PfRule id,
139
                                                const std::vector<Node>& exp,
140
                                                const std::vector<Node>& args)
141
{
142
  if (d_pfee != nullptr)
143
  {
144
    // use proof equality engine to construct the trust node
145
    return d_pfee->assertConflict(id, exp, args);
146
  }
147
  // version without proofs
148
  Node conf = mkExplainPartial(exp, {});
149
  return TrustNode::mkTrustConflict(conf, nullptr);
150
}
151
152
5362
void TheoryInferenceManager::conflictExp(InferenceId id,
153
                                         const std::vector<Node>& exp,
154
                                         ProofGenerator* pg)
155
{
156
5362
  if (!d_theoryState.isInConflict())
157
  {
158
    // make the trust node
159
10366
    TrustNode tconf = mkConflictExp(exp, pg);
160
    // send it on the output channel
161
5183
    trustedConflict(tconf, id);
162
  }
163
5362
}
164
165
6211
TrustNode TheoryInferenceManager::mkConflictExp(const std::vector<Node>& exp,
166
                                                ProofGenerator* pg)
167
{
168
6211
  if (d_pfee != nullptr)
169
  {
170
931
    Assert(pg != nullptr);
171
    // use proof equality engine to construct the trust node
172
931
    return d_pfee->assertConflict(exp, pg);
173
  }
174
  // version without proofs
175
10560
  Node conf = mkExplainPartial(exp, {});
176
5280
  return TrustNode::mkTrustConflict(conf, nullptr);
177
}
178
179
10715006
bool TheoryInferenceManager::propagateLit(TNode lit)
180
{
181
  // If already in conflict, no more propagation
182
10715006
  if (d_theoryState.isInConflict())
183
  {
184
3212
    return false;
185
  }
186
  // Propagate out
187
10711794
  bool ok = d_out.propagate(lit);
188
10711794
  if (!ok)
189
  {
190
69314
    d_theoryState.notifyInConflict();
191
  }
192
10711794
  return ok;
193
}
194
195
260289
TrustNode TheoryInferenceManager::explainLit(TNode lit)
196
{
197
260289
  if (d_pfee != nullptr)
198
  {
199
43519
    return d_pfee->explain(lit);
200
  }
201
216770
  if (d_ee != nullptr)
202
  {
203
433540
    Node exp = d_ee->mkExplainLit(lit);
204
216770
    return TrustNode::mkTrustPropExp(lit, exp, nullptr);
205
  }
206
  Unimplemented() << "Inference manager for " << d_theory.getId()
207
                  << " was asked to explain a propagation but doesn't have an "
208
                     "equality engine or implement the "
209
                     "TheoryInferenceManager::explainLit interface!";
210
}
211
212
9948
TrustNode TheoryInferenceManager::explainConflictEqConstantMerge(TNode a,
213
                                                                 TNode b)
214
{
215
19896
  Node lit = a.eqNode(b);
216
9948
  if (d_pfee != nullptr)
217
  {
218
1568
    return d_pfee->assertConflict(lit);
219
  }
220
8380
  if (d_ee != nullptr)
221
  {
222
16760
    Node conf = d_ee->mkExplainLit(lit);
223
8380
    return TrustNode::mkTrustConflict(conf, nullptr);
224
  }
225
  Unimplemented() << "Inference manager for " << d_theory.getId()
226
                  << " mkTrustedConflictEqConstantMerge";
227
}
228
229
669002
bool TheoryInferenceManager::lemma(TNode lem, InferenceId id, LemmaProperty p)
230
{
231
1338003
  TrustNode tlem = TrustNode::mkTrustLemma(lem, nullptr);
232
1338003
  return trustedLemma(tlem, id, p);
233
}
234
235
872340
bool TheoryInferenceManager::trustedLemma(const TrustNode& tlem,
236
                                          InferenceId id,
237
                                          LemmaProperty p)
238
{
239
  // if the policy says to cache lemmas, check the cache and return false if
240
  // we are a duplicate
241
872340
  if (d_cacheLemmas)
242
  {
243
829150
    if (!cacheLemma(tlem.getNode(), p))
244
    {
245
593937
      return false;
246
    }
247
  }
248
278403
  d_lemmaIdStats << id;
249
278403
  d_numCurrentLemmas++;
250
278405
  d_out.trustedLemma(tlem, p);
251
278401
  return true;
252
}
253
254
bool TheoryInferenceManager::lemmaExp(Node conc,
255
                                      InferenceId id,
256
                                      PfRule pfr,
257
                                      const std::vector<Node>& exp,
258
                                      const std::vector<Node>& noExplain,
259
                                      const std::vector<Node>& args,
260
                                      LemmaProperty p)
261
{
262
  // make the trust node
263
  TrustNode trn = mkLemmaExp(conc, pfr, exp, noExplain, args);
264
  // send it on the output channel
265
  return trustedLemma(trn, id, p);
266
}
267
268
TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
269
                                             PfRule id,
270
                                             const std::vector<Node>& exp,
271
                                             const std::vector<Node>& noExplain,
272
                                             const std::vector<Node>& args)
273
{
274
  if (d_pfee != nullptr)
275
  {
276
    // make the trust node from the proof equality engine
277
    return d_pfee->assertLemma(conc, id, exp, noExplain, args);
278
  }
279
  // otherwise, not using proofs, explain and make trust node
280
  Node ant = mkExplainPartial(exp, noExplain);
281
  Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
282
  return TrustNode::mkTrustLemma(lem, nullptr);
283
}
284
285
bool TheoryInferenceManager::lemmaExp(Node conc,
286
                                      InferenceId id,
287
                                      const std::vector<Node>& exp,
288
                                      const std::vector<Node>& noExplain,
289
                                      ProofGenerator* pg,
290
                                      LemmaProperty p)
291
{
292
  // make the trust node
293
  TrustNode trn = mkLemmaExp(conc, exp, noExplain, pg);
294
  // send it on the output channel
295
  return trustedLemma(trn, id, p);
296
}
297
298
15272
TrustNode TheoryInferenceManager::mkLemmaExp(Node conc,
299
                                             const std::vector<Node>& exp,
300
                                             const std::vector<Node>& noExplain,
301
                                             ProofGenerator* pg)
302
{
303
15272
  if (d_pfee != nullptr)
304
  {
305
    // make the trust node from the proof equality engine
306
803
    return d_pfee->assertLemma(conc, exp, noExplain, pg);
307
  }
308
  // otherwise, not using proofs, explain and make trust node
309
28938
  Node ant = mkExplainPartial(exp, noExplain);
310
28938
  Node lem = NodeManager::currentNM()->mkNode(kind::IMPLIES, ant, conc);
311
14469
  return TrustNode::mkTrustLemma(lem, nullptr);
312
}
313
314
103393
bool TheoryInferenceManager::hasCachedLemma(TNode lem, LemmaProperty p)
315
{
316
206786
  Node rewritten = Rewriter::rewrite(lem);
317
206786
  return d_lemmasSent.find(rewritten) != d_lemmasSent.end();
318
}
319
320
uint32_t TheoryInferenceManager::numSentLemmas() const
321
{
322
  return d_numCurrentLemmas;
323
}
324
325
511900
bool TheoryInferenceManager::hasSentLemma() const
326
{
327
511900
  return d_numCurrentLemmas != 0;
328
}
329
330
15184
bool TheoryInferenceManager::assertInternalFact(TNode atom,
331
                                                bool pol,
332
                                                InferenceId id,
333
                                                TNode exp)
334
{
335
15184
  d_factIdStats << id;
336
15184
  return processInternalFact(atom, pol, PfRule::UNKNOWN, {exp}, {}, nullptr);
337
}
338
339
2131
bool TheoryInferenceManager::assertInternalFact(TNode atom,
340
                                                bool pol,
341
                                                InferenceId id,
342
                                                PfRule pfr,
343
                                                const std::vector<Node>& exp,
344
                                                const std::vector<Node>& args)
345
{
346
2131
  Assert(pfr != PfRule::UNKNOWN);
347
2131
  d_factIdStats << id;
348
2131
  return processInternalFact(atom, pol, pfr, exp, args, nullptr);
349
}
350
351
420638
bool TheoryInferenceManager::assertInternalFact(TNode atom,
352
                                                bool pol,
353
                                                InferenceId id,
354
                                                const std::vector<Node>& exp,
355
                                                ProofGenerator* pg)
356
{
357
420638
  d_factIdStats << id;
358
420638
  return processInternalFact(atom, pol, PfRule::ASSUME, exp, {}, pg);
359
}
360
361
437953
bool TheoryInferenceManager::processInternalFact(TNode atom,
362
                                                 bool pol,
363
                                                 PfRule id,
364
                                                 const std::vector<Node>& exp,
365
                                                 const std::vector<Node>& args,
366
                                                 ProofGenerator* pg)
367
{
368
  // make the node corresponding to the explanation
369
875906
  Node expn = NodeManager::currentNM()->mkAnd(exp);
370
  // call the pre-notify fact method with preReg = false, isInternal = true
371
437953
  if (d_theory.preNotifyFact(atom, pol, expn, false, true))
372
  {
373
    // Handled in a theory-specific way that doesn't require equality engine,
374
    // notice we return true, indicating that the fact was processed.
375
    return true;
376
  }
377
437953
  Assert(d_ee != nullptr);
378
875906
  Trace("infer-manager") << "TheoryInferenceManager::assertInternalFact: "
379
437953
                         << expn << std::endl;
380
437953
  d_numCurrentFacts++;
381
  // Now, assert the fact. How to do so depends on whether proofs are enabled.
382
  // If no proof production, or no proof rule was given
383
437953
  bool ret = false;
384
437953
  if (d_pfee == nullptr || id == PfRule::UNKNOWN)
385
  {
386
422533
    if (atom.getKind() == kind::EQUAL)
387
    {
388
346018
      ret = d_ee->assertEquality(atom, pol, expn);
389
    }
390
    else
391
    {
392
76515
      ret = d_ee->assertPredicate(atom, pol, expn);
393
    }
394
    // Must reference count the equality and its explanation, which is not done
395
    // by the equality engine. Notice that we do *not* need to do this for
396
    // external assertions, which enter as facts in theory check. This is also
397
    // not done if we are asserting to the proof equality engine, which does
398
    // this caching itself within ProofEqEngine::assertFact.
399
422533
    d_keep.insert(atom);
400
422533
    d_keep.insert(expn);
401
  }
402
  else
403
  {
404
    // Note that we reconstruct the original literal lit here, since both the
405
    // original literal is needed for bookkeeping proofs. It is possible to
406
    // optimize this so that a few less nodes are created, but at the cost
407
    // of a more verbose interface to proof equality engine.
408
30840
    Node lit = pol ? Node(atom) : atom.notNode();
409
15420
    if (pg != nullptr)
410
    {
411
      // use the proof generator interface
412
14029
      ret = d_pfee->assertFact(lit, expn, pg);
413
    }
414
    else
415
    {
416
      // use the explict proof step interface
417
1391
      ret = d_pfee->assertFact(lit, id, expn, args);
418
    }
419
  }
420
  // call the notify fact method with isInternal = true
421
437953
  d_theory.notifyFact(atom, pol, expn, true);
422
875906
  Trace("infer-manager")
423
437953
      << "TheoryInferenceManager::finished assertInternalFact" << std::endl;
424
437953
  return ret;
425
}
426
427
38423
void TheoryInferenceManager::explain(TNode n, std::vector<TNode>& assumptions)
428
{
429
38423
  if (n.getKind() == kind::AND)
430
  {
431
    for (const Node& nc : n)
432
    {
433
      d_ee->explainLit(nc, assumptions);
434
    }
435
  }
436
  else
437
  {
438
38423
    d_ee->explainLit(n, assumptions);
439
  }
440
38423
}
441
442
Node TheoryInferenceManager::mkExplain(TNode n)
443
{
444
  std::vector<TNode> assumptions;
445
  explain(n, assumptions);
446
  return NodeManager::currentNM()->mkAnd(assumptions);
447
}
448
449
19749
Node TheoryInferenceManager::mkExplainPartial(
450
    const std::vector<Node>& exp, const std::vector<Node>& noExplain)
451
{
452
39498
  std::vector<TNode> assumps;
453
60534
  for (const Node& e : exp)
454
  {
455
43147
    if (std::find(noExplain.begin(), noExplain.end(), e) != noExplain.end())
456
    {
457
2362
      if (std::find(assumps.begin(), assumps.end(), e) == assumps.end())
458
      {
459
        // a non-explained literal
460
2362
        assumps.push_back(e);
461
      }
462
2362
      continue;
463
    }
464
    // otherwise, explain it
465
38423
    explain(e, assumps);
466
  }
467
39498
  return NodeManager::currentNM()->mkAnd(assumps);
468
}
469
470
uint32_t TheoryInferenceManager::numSentFacts() const
471
{
472
  return d_numCurrentFacts;
473
}
474
475
63043
bool TheoryInferenceManager::hasSentFact() const
476
{
477
63043
  return d_numCurrentFacts != 0;
478
}
479
480
829150
bool TheoryInferenceManager::cacheLemma(TNode lem, LemmaProperty p)
481
{
482
1658300
  Node rewritten = Rewriter::rewrite(lem);
483
829150
  if (d_lemmasSent.find(rewritten) != d_lemmasSent.end())
484
  {
485
593937
    return false;
486
  }
487
235213
  d_lemmasSent.insert(rewritten);
488
235213
  return true;
489
}
490
491
23746
void TheoryInferenceManager::requirePhase(TNode n, bool pol)
492
{
493
23746
  return d_out.requirePhase(n, pol);
494
}
495
496
660380
void TheoryInferenceManager::spendResource(ResourceManager::Resource r)
497
{
498
660380
  d_out.spendResource(r);
499
660380
}
500
501
21232002
void TheoryInferenceManager::safePoint(ResourceManager::Resource r)
502
{
503
21232002
  d_out.safePoint(r);
504
21232002
}
505
506
3039
void TheoryInferenceManager::setIncomplete() { d_out.setIncomplete(); }
507
508
}  // namespace theory
509
26685
}  // namespace CVC4