GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/inference_manager_buffered.cpp Lines: 77 83 92.8 %
Date: 2021-03-23 Branches: 55 154 35.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file inference_manager_buffered.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 A buffered inference manager
13
 **/
14
15
#include "theory/inference_manager_buffered.h"
16
17
#include "theory/rewriter.h"
18
#include "theory/theory.h"
19
#include "theory/theory_state.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
namespace theory {
25
26
62979
InferenceManagerBuffered::InferenceManagerBuffered(Theory& t,
27
                                                   TheoryState& state,
28
                                                   ProofNodeManager* pnm,
29
                                                   const std::string& name,
30
62979
                                                   bool cacheLemmas)
31
    : TheoryInferenceManager(t, state, pnm, name, cacheLemmas),
32
62979
      d_processingPendingLemmas(false)
33
{
34
62979
}
35
36
2500820
bool InferenceManagerBuffered::hasPending() const
37
{
38
2500820
  return hasPendingFact() || hasPendingLemma();
39
}
40
41
3005071
bool InferenceManagerBuffered::hasPendingFact() const
42
{
43
3005071
  return !d_pendingFact.empty();
44
}
45
46
3094925
bool InferenceManagerBuffered::hasPendingLemma() const
47
{
48
3094925
  return !d_pendingLem.empty();
49
}
50
51
94676
bool InferenceManagerBuffered::addPendingLemma(Node lem,
52
                                               InferenceId id,
53
                                               LemmaProperty p,
54
                                               ProofGenerator* pg,
55
                                               bool checkCache)
56
{
57
94676
  if (checkCache)
58
  {
59
    // check if it is unique up to rewriting
60
176492
    Node lemr = Rewriter::rewrite(lem);
61
94676
    if (hasCachedLemma(lemr, p))
62
    {
63
12860
      return false;
64
    }
65
  }
66
  // make the simple theory lemma
67
81816
  d_pendingLem.emplace_back(new SimpleTheoryLemma(id, lem, p, pg));
68
81816
  return true;
69
}
70
71
14969
void InferenceManagerBuffered::addPendingLemma(
72
    std::unique_ptr<TheoryInference> lemma)
73
{
74
14969
  d_pendingLem.emplace_back(std::move(lemma));
75
14969
}
76
77
void InferenceManagerBuffered::addPendingFact(Node conc,
78
                                              InferenceId id,
79
                                              Node exp,
80
                                              ProofGenerator* pg)
81
{
82
  // make a simple theory internal fact
83
  Assert(conc.getKind() != AND && conc.getKind() != OR);
84
  d_pendingFact.emplace_back(new SimpleTheoryInternalFact(id, conc, exp, pg));
85
}
86
87
13629
void InferenceManagerBuffered::addPendingFact(
88
    std::unique_ptr<TheoryInference> fact)
89
{
90
13629
  d_pendingFact.emplace_back(std::move(fact));
91
13629
}
92
93
3855
void InferenceManagerBuffered::addPendingPhaseRequirement(Node lit, bool pol)
94
{
95
  // it is the responsibility of the caller to ensure lit is rewritten
96
3855
  d_pendingReqPhase[lit] = pol;
97
3855
}
98
99
3788045
void InferenceManagerBuffered::doPendingFacts()
100
{
101
3788045
  size_t i = 0;
102
4629321
  while (!d_theoryState.isInConflict() && i < d_pendingFact.size())
103
  {
104
    // assert the internal fact, which notice may enqueue more pending facts in
105
    // this loop, or result in a conflict.
106
420638
    assertInternalFactTheoryInference(d_pendingFact[i].get());
107
420638
    i++;
108
  }
109
3788045
  d_pendingFact.clear();
110
3788045
}
111
112
3760874
void InferenceManagerBuffered::doPendingLemmas()
113
{
114
3760874
  if (d_processingPendingLemmas)
115
  {
116
    // already processing
117
6971
    return;
118
  }
119
3753903
  d_processingPendingLemmas = true;
120
3753903
  size_t i = 0;
121
3979909
  while (i < d_pendingLem.size())
122
  {
123
    // process this lemma, which notice may enqueue more pending lemmas in this
124
    // loop, or clear the lemmas.
125
113004
    lemmaTheoryInference(d_pendingLem[i].get());
126
113003
    i++;
127
  }
128
3753902
  d_pendingLem.clear();
129
3753902
  d_processingPendingLemmas = false;
130
}
131
132
210511
void InferenceManagerBuffered::doPendingPhaseRequirements()
133
{
134
  // process the pending require phase calls
135
214365
  for (const std::pair<const Node, bool>& prp : d_pendingReqPhase)
136
  {
137
3854
    requirePhase(prp.first, prp.second);
138
  }
139
210511
  d_pendingReqPhase.clear();
140
210511
}
141
770852
void InferenceManagerBuffered::clearPending()
142
{
143
770852
  d_pendingFact.clear();
144
770852
  d_pendingLem.clear();
145
770852
  d_pendingReqPhase.clear();
146
770852
}
147
1553
void InferenceManagerBuffered::clearPendingFacts() { d_pendingFact.clear(); }
148
17562
void InferenceManagerBuffered::clearPendingLemmas() { d_pendingLem.clear(); }
149
1597
void InferenceManagerBuffered::clearPendingPhaseRequirements()
150
{
151
1597
  d_pendingReqPhase.clear();
152
1597
}
153
154
187998
std::size_t InferenceManagerBuffered::numPendingLemmas() const
155
{
156
187998
  return d_pendingLem.size();
157
}
158
std::size_t InferenceManagerBuffered::numPendingFacts() const
159
{
160
  return d_pendingFact.size();
161
}
162
163
115200
void InferenceManagerBuffered::lemmaTheoryInference(TheoryInference* lem)
164
{
165
  // process this lemma
166
115200
  LemmaProperty p = LemmaProperty::NONE;
167
230400
  TrustNode tlem = lem->processLemma(p);
168
115200
  Assert(!tlem.isNull());
169
  // send the lemma
170
115200
  trustedLemma(tlem, lem->getId(), p);
171
115199
}
172
173
420638
void InferenceManagerBuffered::assertInternalFactTheoryInference(
174
    TheoryInference* fact)
175
{
176
  // process this fact
177
841276
  std::vector<Node> exp;
178
420638
  ProofGenerator* pg = nullptr;
179
841276
  Node lit = fact->processFact(exp, pg);
180
420638
  Assert(!lit.isNull());
181
420638
  bool pol = lit.getKind() != NOT;
182
841276
  TNode atom = pol ? lit : lit[0];
183
  // no double negation or conjunctive conclusions
184
420638
  Assert(atom.getKind() != NOT && atom.getKind() != AND);
185
  // assert the internal fact
186
420638
  assertInternalFact(atom, pol, fact->getId(), exp, pg);
187
420638
}
188
189
}  // namespace theory
190
26685
}  // namespace CVC4