GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/preprocess_proof_generator.cpp Lines: 99 107 92.5 %
Date: 2021-03-23 Branches: 209 492 42.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file preprocess_proof_generator.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 The implementation of the module for proofs for preprocessing in an
13
 ** SMT engine.
14
 **/
15
16
#include "smt/preprocess_proof_generator.h"
17
18
#include "expr/proof.h"
19
#include "expr/proof_checker.h"
20
#include "expr/proof_node.h"
21
#include "options/proof_options.h"
22
#include "theory/rewriter.h"
23
24
namespace CVC4 {
25
namespace smt {
26
27
1924
PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
28
                                                   context::Context* c,
29
                                                   std::string name,
30
                                                   PfRule ra,
31
1924
                                                   PfRule rpp)
32
    : d_pnm(pnm),
33
1924
      d_ctx(c ? c : &d_context),
34
      d_src(d_ctx),
35
      d_helperProofs(pnm, d_ctx),
36
      d_inputPf(pnm, nullptr),
37
      d_name(name),
38
      d_ra(ra),
39
3848
      d_rpp(rpp)
40
{
41
1924
}
42
43
13345
void PreprocessProofGenerator::notifyInput(Node n)
44
{
45
13345
  notifyNewAssert(n, &d_inputPf);
46
13345
}
47
48
43861
void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
49
{
50
87722
  Trace("smt-proof-pp-debug")
51
43861
      << "PreprocessProofGenerator::notifyNewAssert: " << n << std::endl;
52
43861
  if (d_src.find(n) == d_src.end())
53
  {
54
    // if no proof generator provided for (non-true) assertion
55
41225
    if (pg == nullptr && (!n.isConst() || !n.getConst<bool>()))
56
    {
57
134
      checkEagerPedantic(d_ra);
58
    }
59
41225
    d_src[n] = theory::TrustNode::mkTrustLemma(n, pg);
60
  }
61
  else
62
  {
63
2636
    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
64
  }
65
43861
}
66
67
24214
void PreprocessProofGenerator::notifyNewTrustedAssert(theory::TrustNode tn)
68
{
69
24214
  notifyNewAssert(tn.getProven(), tn.getGenerator());
70
24214
}
71
72
15258
void PreprocessProofGenerator::notifyPreprocessed(Node n,
73
                                                  Node np,
74
                                                  ProofGenerator* pg)
75
{
76
  // only do anything if indeed it rewrote
77
15258
  if (n == np)
78
  {
79
    return;
80
  }
81
  // call the trusted version
82
15258
  notifyTrustedPreprocessed(theory::TrustNode::mkTrustRewrite(n, np, pg));
83
}
84
85
26165
void PreprocessProofGenerator::notifyTrustedPreprocessed(theory::TrustNode tnp)
86
{
87
26165
  if (tnp.isNull())
88
  {
89
    // no rewrite, nothing to do
90
    return;
91
  }
92
26165
  Assert(tnp.getKind() == theory::TrustNodeKind::REWRITE);
93
52330
  Node np = tnp.getNode();
94
52330
  Trace("smt-proof-pp-debug")
95
52330
      << "PreprocessProofGenerator::notifyPreprocessed: " << tnp.getProven()
96
26165
      << std::endl;
97
26165
  if (d_src.find(np) == d_src.end())
98
  {
99
20732
    if (tnp.getGenerator() == nullptr)
100
    {
101
938
      checkEagerPedantic(d_rpp);
102
    }
103
20732
    d_src[np] = tnp;
104
  }
105
  else
106
  {
107
5433
    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
108
  }
109
}
110
111
32648
std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
112
{
113
32648
  NodeTrustNodeMap::iterator it = d_src.find(f);
114
32648
  if (it == d_src.end())
115
  {
116
    // could be an assumption, return nullptr
117
14832
    return nullptr;
118
  }
119
  // make CDProof to construct the proof below
120
35632
  CDProof cdp(d_pnm);
121
122
35632
  Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
123
17816
                    << ") input " << f << std::endl;
124
35632
  Node curr = f;
125
35632
  std::vector<Node> transChildren;
126
35632
  std::unordered_set<Node, NodeHashFunction> processed;
127
  bool success;
128
  // we connect the proof of f to its source via the map d_src until we
129
  // discover that its source is a preprocessing lemma (a lemma stored in d_src)
130
  // or otherwise it is assumed to be an input assumption.
131
24196
  do
132
  {
133
24196
    success = false;
134
24196
    if (it != d_src.end())
135
    {
136
24196
      Assert((*it).second.getNode() == curr);
137
      // get the proven node
138
48392
      Node proven = (*it).second.getProven();
139
24196
      Assert(!proven.isNull());
140
24196
      Trace("smt-pppg") << "...process proven " << proven << std::endl;
141
24196
      if (processed.find(proven) != processed.end())
142
      {
143
        Unhandled() << "Cyclic steps in preprocess proof generator";
144
        continue;
145
      }
146
24196
      processed.insert(proven);
147
24196
      bool proofStepProcessed = false;
148
149
      // if a generator for the step was provided, it is stored in the proof
150
24196
      Trace("smt-pppg") << "...get provided proof" << std::endl;
151
48392
      std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
152
24196
      if (pfr != nullptr)
153
      {
154
23575
        Trace("smt-pppg") << "...add provided" << std::endl;
155
23575
        Assert(pfr->getResult() == proven);
156
23575
        cdp.addProof(pfr);
157
23575
        proofStepProcessed = true;
158
      }
159
160
24196
      Trace("smt-pppg") << "...update" << std::endl;
161
24196
      theory::TrustNodeKind tnk = (*it).second.getKind();
162
24196
      if (tnk == theory::TrustNodeKind::REWRITE)
163
      {
164
6380
        Trace("smt-pppg") << "...rewritten from " << proven[0] << std::endl;
165
6380
        Assert(proven.getKind() == kind::EQUAL);
166
6380
        if (!proofStepProcessed)
167
        {
168
          // maybe its just a simple rewrite?
169
545
          if (proven[1] == theory::Rewriter::rewrite(proven[0]))
170
          {
171
104
            cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0]});
172
104
            proofStepProcessed = true;
173
          }
174
        }
175
6380
        transChildren.push_back(proven);
176
        // continue with source
177
6380
        curr = proven[0];
178
6380
        success = true;
179
        // find the next node
180
6380
        it = d_src.find(curr);
181
      }
182
      else
183
      {
184
17816
        Trace("smt-pppg") << "...lemma" << std::endl;
185
17816
        Assert(tnk == theory::TrustNodeKind::LEMMA);
186
      }
187
188
24196
      if (!proofStepProcessed)
189
      {
190
517
        Trace("smt-pppg") << "...add missing step" << std::endl;
191
        // add trusted step, the rule depends on the kind of trust node
192
1034
        cdp.addStep(proven,
193
                    tnk == theory::TrustNodeKind::LEMMA ? d_ra : d_rpp,
194
                    {},
195
517
                    {proven});
196
      }
197
    }
198
  } while (success);
199
200
  // prove ( curr == f ), which is not necessary if they are the same
201
  // modulo symmetry.
202
17816
  if (!CDProof::isSame(f, curr))
203
  {
204
10340
    Node fullRewrite = curr.eqNode(f);
205
5170
    if (transChildren.size() >= 2)
206
    {
207
789
      Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
208
789
      std::reverse(transChildren.begin(), transChildren.end());
209
789
      cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
210
    }
211
5170
    Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
212
    // prove f
213
5170
    cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
214
5170
    Trace("smt-pppg") << "...finished" << std::endl;
215
  }
216
217
  // overall, proof is:
218
  //        --------- from proof generator       ---------- from proof generator
219
  //        F_1 = F_2          ...               F_{n-1} = F_n
220
  // ---?   -------------------------------------------------- TRANS
221
  // F_1    F_1 = F_n
222
  // ---------------- EQ_RESOLVE
223
  // F_n
224
  // Note F_1 may have been given a proof if it was not an input assumption.
225
226
17816
  return cdp.getProofFor(f);
227
}
228
229
962
ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
230
231
325
LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
232
{
233
325
  return d_helperProofs.allocateProof(nullptr, d_ctx);
234
}
235
236
30594
std::string PreprocessProofGenerator::identify() const { return d_name; }
237
238
1072
void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
239
{
240
1072
  if (options::proofEagerChecking())
241
  {
242
    // catch a pedantic failure now, which otherwise would not be
243
    // triggered since we are doing lazy proof generation
244
    ProofChecker* pc = d_pnm->getChecker();
245
    std::stringstream serr;
246
    if (pc->isPedanticFailure(r, serr))
247
    {
248
      Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
249
                  << serr.str();
250
    }
251
  }
252
1072
}
253
254
}  // namespace smt
255
26685
}  // namespace CVC4