GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/preprocessing/assertion_pipeline.cpp Lines: 90 90 100.0 %
Date: 2021-03-22 Branches: 151 380 39.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file assertion_pipeline.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, Haniel Barbosa
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 AssertionPipeline stores a list of assertions modified by
13
 ** preprocessing passes
14
 **/
15
16
#include "preprocessing/assertion_pipeline.h"
17
18
#include "expr/node_manager.h"
19
#include "options/smt_options.h"
20
#include "expr/lazy_proof.h"
21
#include "proof/proof_manager.h"
22
#include "smt/preprocess_proof_generator.h"
23
#include "theory/builtin/proof_checker.h"
24
#include "theory/rewriter.h"
25
26
namespace CVC4 {
27
namespace preprocessing {
28
29
9626
AssertionPipeline::AssertionPipeline()
30
    : d_realAssertionsEnd(0),
31
      d_storeSubstsInAsserts(false),
32
      d_substsIndex(0),
33
      d_assumptionsStart(0),
34
      d_numAssumptions(0),
35
9626
      d_pppg(nullptr)
36
{
37
9626
}
38
39
14455
void AssertionPipeline::clear()
40
{
41
14455
  d_nodes.clear();
42
14455
  d_realAssertionsEnd = 0;
43
14455
  d_assumptionsStart = 0;
44
14455
  d_numAssumptions = 0;
45
14455
}
46
47
115194
void AssertionPipeline::push_back(Node n,
48
                                  bool isAssumption,
49
                                  bool isInput,
50
                                  ProofGenerator* pgen)
51
{
52
115194
  d_nodes.push_back(n);
53
115194
  if (isAssumption)
54
  {
55
2149
    Assert(pgen == nullptr);
56
2149
    if (d_numAssumptions == 0)
57
    {
58
2129
      d_assumptionsStart = d_nodes.size() - 1;
59
    }
60
    // Currently, we assume that assumptions are all added one after another
61
    // and that we store them in the same vector as the assertions. Once we
62
    // split the assertions up into multiple vectors (see issue #2473), we will
63
    // not have this limitation anymore.
64
2149
    Assert(d_assumptionsStart + d_numAssumptions == d_nodes.size() - 1);
65
2149
    d_numAssumptions++;
66
  }
67
230388
  Trace("assert-pipeline") << "Assertions: ...new assertion " << n
68
115194
                           << ", isInput=" << isInput << std::endl;
69
115194
  if (isProofEnabled())
70
  {
71
18099
    if (!isInput)
72
    {
73
      // notice this is always called, regardless of whether pgen is nullptr
74
4754
      d_pppg->notifyNewAssert(n, pgen);
75
    }
76
    else
77
    {
78
13345
      Assert(pgen == nullptr);
79
      // n is an input assertion, whose proof should be ASSUME.
80
13345
      d_pppg->notifyInput(n);
81
    }
82
  }
83
115194
}
84
85
20355
void AssertionPipeline::pushBackTrusted(theory::TrustNode trn)
86
{
87
20355
  Assert(trn.getKind() == theory::TrustNodeKind::LEMMA);
88
  // push back what was proven
89
20355
  push_back(trn.getProven(), false, false, trn.getGenerator());
90
20355
}
91
92
267644
void AssertionPipeline::replace(size_t i, Node n, ProofGenerator* pgen)
93
{
94
267644
  if (n == d_nodes[i])
95
  {
96
    // no change, skip
97
189359
    return;
98
  }
99
156570
  Trace("assert-pipeline") << "Assertions: Replace " << d_nodes[i] << " with "
100
78285
                           << n << std::endl;
101
78285
  if (isProofEnabled())
102
  {
103
15258
    d_pppg->notifyPreprocessed(d_nodes[i], n, pgen);
104
  }
105
63027
  else if (options::unsatCores())
106
  {
107
12110
    ProofManager::currentPM()->addDependence(n, d_nodes[i]);
108
  }
109
78285
  d_nodes[i] = n;
110
}
111
112
128255
void AssertionPipeline::replaceTrusted(size_t i, theory::TrustNode trn)
113
{
114
128255
  if (trn.isNull())
115
  {
116
    // null trust node denotes no change, nothing to do
117
54280
    return;
118
  }
119
73975
  Assert(trn.getKind() == theory::TrustNodeKind::REWRITE);
120
73975
  Assert(trn.getProven()[0] == d_nodes[i]);
121
73975
  replace(i, trn.getNode(), trn.getGenerator());
122
}
123
124
962
void AssertionPipeline::setProofGenerator(smt::PreprocessProofGenerator* pppg)
125
{
126
962
  d_pppg = pppg;
127
962
}
128
129
212327
bool AssertionPipeline::isProofEnabled() const { return d_pppg != nullptr; }
130
131
2323
void AssertionPipeline::enableStoreSubstsInAsserts()
132
{
133
2323
  d_storeSubstsInAsserts = true;
134
2323
  d_substsIndex = d_nodes.size();
135
2323
  d_nodes.push_back(NodeManager::currentNM()->mkConst<bool>(true));
136
2323
}
137
138
9000
void AssertionPipeline::disableStoreSubstsInAsserts()
139
{
140
9000
  d_storeSubstsInAsserts = false;
141
9000
}
142
143
1204
void AssertionPipeline::addSubstitutionNode(Node n, ProofGenerator* pg)
144
{
145
1204
  Assert(d_storeSubstsInAsserts);
146
1204
  Assert(n.getKind() == kind::EQUAL);
147
1204
  conjoin(d_substsIndex, n, pg);
148
1204
}
149
150
3572
void AssertionPipeline::conjoin(size_t i, Node n, ProofGenerator* pg)
151
{
152
3572
  NodeManager* nm = NodeManager::currentNM();
153
6904
  Node newConj = nm->mkNode(kind::AND, d_nodes[i], n);
154
6904
  Node newConjr = theory::Rewriter::rewrite(newConj);
155
7144
  Trace("assert-pipeline") << "Assertions: conjoin " << n << " to "
156
3572
                           << d_nodes[i] << std::endl;
157
7144
  Trace("assert-pipeline-debug") << "conjoin " << n << " to " << d_nodes[i]
158
3572
                                 << ", got " << newConjr << std::endl;
159
3572
  if (newConjr == d_nodes[i])
160
  {
161
    // trivial, skip
162
240
    return;
163
  }
164
3332
  if (isProofEnabled())
165
  {
166
725
    if (newConjr == n)
167
    {
168
      // don't care about the previous proof and can simply plug in the
169
      // proof from pg if the resulting assertion is the same as n.
170
400
      d_pppg->notifyNewAssert(newConjr, pg);
171
    }
172
    else
173
    {
174
      // ---------- from pppg   --------- from pg
175
      // d_nodes[i]                n
176
      // -------------------------------- AND_INTRO
177
      //      d_nodes[i] ^ n
178
      // -------------------------------- MACRO_SR_PRED_TRANSFORM
179
      //   rewrite( d_nodes[i] ^ n )
180
      // allocate a fresh proof which will act as the proof generator
181
325
      LazyCDProof* lcp = d_pppg->allocateHelperProof();
182
325
      lcp->addLazyStep(n, pg, PfRule::PREPROCESS);
183
325
      if (d_nodes[i].isConst() && d_nodes[i].getConst<bool>())
184
      {
185
        // skip the AND_INTRO if the previous d_nodes[i] was true
186
152
        newConj = n;
187
      }
188
      else
189
      {
190
173
        lcp->addLazyStep(d_nodes[i], d_pppg);
191
173
        lcp->addStep(newConj, PfRule::AND_INTRO, {d_nodes[i], n}, {});
192
      }
193
325
      if (newConjr != newConj)
194
      {
195
972
        lcp->addStep(
196
648
            newConjr, PfRule::MACRO_SR_PRED_TRANSFORM, {newConj}, {newConjr});
197
      }
198
      // Notice we have constructed a proof of a new assertion, where d_pppg
199
      // is referenced in the lazy proof above. If alternatively we had
200
      // constructed a proof of d_nodes[i] = rewrite( d_nodes[i] ^ n ), we would
201
      // have used notifyPreprocessed. However, it is simpler to make the
202
      // above proof.
203
325
      d_pppg->notifyNewAssert(newConjr, lcp);
204
    }
205
  }
206
3332
  if (options::unsatCores() && !isProofEnabled())
207
  {
208
4
    ProofManager::currentPM()->addDependence(newConjr, d_nodes[i]);
209
  }
210
3332
  d_nodes[i] = newConjr;
211
3332
  Assert(theory::Rewriter::rewrite(newConjr) == newConjr);
212
}
213
214
}  // namespace preprocessing
215
26676
}  // namespace CVC4