GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/smt/preprocess_proof_generator.cpp Lines: 110 118 93.2 %
Date: 2021-11-05 Branches: 245 552 44.4 %

Line Exec Source
1
/******************************************************************************
2
 * Top contributors (to current version):
3
 *   Andrew Reynolds, Gereon Kremer
4
 *
5
 * This file is part of the cvc5 project.
6
 *
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.
11
 * ****************************************************************************
12
 *
13
 * The implementation of the module for proofs for preprocessing in an
14
 * SMT engine.
15
 */
16
17
#include "smt/preprocess_proof_generator.h"
18
19
#include <sstream>
20
21
#include "options/proof_options.h"
22
#include "proof/method_id.h"
23
#include "proof/proof.h"
24
#include "proof/proof_checker.h"
25
#include "proof/proof_node.h"
26
#include "theory/quantifiers/extended_rewrite.h"
27
#include "theory/rewriter.h"
28
29
namespace cvc5 {
30
namespace smt {
31
32
15990
PreprocessProofGenerator::PreprocessProofGenerator(ProofNodeManager* pnm,
33
                                                   context::Context* c,
34
                                                   std::string name,
35
                                                   PfRule ra,
36
15990
                                                   PfRule rpp)
37
    : d_pnm(pnm),
38
15990
      d_ctx(c ? c : &d_context),
39
      d_src(d_ctx),
40
      d_helperProofs(pnm, d_ctx),
41
      d_inputPf(pnm, c, "InputProof"),
42
      d_name(name),
43
      d_ra(ra),
44
31980
      d_rpp(rpp)
45
{
46
15990
}
47
48
43539
void PreprocessProofGenerator::notifyInput(Node n)
49
{
50
43539
  notifyNewAssert(n, &d_inputPf);
51
43539
}
52
53
100906
void PreprocessProofGenerator::notifyNewAssert(Node n, ProofGenerator* pg)
54
{
55
100906
  if (n.isConst() && n.getConst<bool>())
56
  {
57
    // ignore true assertions
58
9714
    return;
59
  }
60
182384
  Trace("smt-proof-pp-debug")
61
182384
      << "PreprocessProofGenerator::notifyNewAssert: " << identify() << " " << n
62
91192
      << " from " << (pg == nullptr ? "null" : pg->identify()) << std::endl;
63
91192
  if (d_src.find(n) == d_src.end())
64
  {
65
    // if no proof generator provided for (non-true) assertion
66
88186
    if (pg == nullptr)
67
    {
68
583
      checkEagerPedantic(d_ra);
69
    }
70
88186
    d_src[n] = TrustNode::mkTrustLemma(n, pg);
71
  }
72
  else
73
  {
74
3006
    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
75
  }
76
}
77
78
32058
void PreprocessProofGenerator::notifyNewTrustedAssert(TrustNode tn)
79
{
80
32058
  notifyNewAssert(tn.getProven(), tn.getGenerator());
81
32058
}
82
83
38324
void PreprocessProofGenerator::notifyPreprocessed(Node n,
84
                                                  Node np,
85
                                                  ProofGenerator* pg)
86
{
87
  // only do anything if indeed it rewrote
88
38324
  if (n == np)
89
  {
90
    return;
91
  }
92
  // call the trusted version
93
38324
  notifyTrustedPreprocessed(TrustNode::mkTrustRewrite(n, np, pg));
94
}
95
96
54204
void PreprocessProofGenerator::notifyTrustedPreprocessed(TrustNode tnp)
97
{
98
54204
  if (tnp.isNull())
99
  {
100
    // no rewrite, nothing to do
101
    return;
102
  }
103
54204
  Assert(tnp.getKind() == TrustNodeKind::REWRITE);
104
108408
  Node np = tnp.getNode();
105
108408
  Trace("smt-proof-pp-debug")
106
54204
      << "PreprocessProofGenerator::notifyPreprocessed: " << tnp << std::endl;
107
54204
  if (d_src.find(np) == d_src.end())
108
  {
109
45398
    if (tnp.getGenerator() == nullptr)
110
    {
111
2444
      checkEagerPedantic(d_rpp);
112
    }
113
45398
    d_src[np] = tnp;
114
  }
115
  else
116
  {
117
8806
    Trace("smt-proof-pp-debug") << "...already proven" << std::endl;
118
  }
119
}
120
121
70091
std::shared_ptr<ProofNode> PreprocessProofGenerator::getProofFor(Node f)
122
{
123
140182
  Trace("smt-pppg") << "PreprocessProofGenerator::getProofFor: (" << d_name
124
70091
                    << ") input " << f << std::endl;
125
70091
  NodeTrustNodeMap::iterator it = d_src.find(f);
126
70091
  if (it == d_src.end())
127
  {
128
39638
    Trace("smt-pppg") << "...no proof for " << identify() << " " << f
129
19819
                      << std::endl;
130
    // could be an assumption, return nullptr
131
19819
    return nullptr;
132
  }
133
  // make CDProof to construct the proof below
134
100544
  CDProof cdp(d_pnm);
135
136
100544
  Node curr = f;
137
100544
  std::vector<Node> transChildren;
138
100544
  std::unordered_set<Node> processed;
139
  bool success;
140
  // we connect the proof of f to its source via the map d_src until we
141
  // discover that its source is a preprocessing lemma (a lemma stored in d_src)
142
  // or otherwise it is assumed to be an input assumption.
143
66553
  do
144
  {
145
66553
    success = false;
146
66553
    if (it != d_src.end())
147
    {
148
66553
      Assert((*it).second.getNode() == curr);
149
      // get the proven node
150
133106
      Node proven = (*it).second.getProven();
151
66553
      Assert(!proven.isNull());
152
66553
      Trace("smt-pppg") << "...process proven " << proven << std::endl;
153
66553
      if (processed.find(proven) != processed.end())
154
      {
155
        Unhandled() << "Cyclic steps in preprocess proof generator";
156
        continue;
157
      }
158
66553
      processed.insert(proven);
159
66553
      bool proofStepProcessed = false;
160
161
      // if a generator for the step was provided, it is stored in the proof
162
133106
      Trace("smt-pppg-debug")
163
66553
          << "...get provided proof " << (*it).second << std::endl;
164
133106
      std::shared_ptr<ProofNode> pfr = (*it).second.toProofNode();
165
66553
      if (pfr != nullptr)
166
      {
167
65585
        Trace("smt-pppg-debug") << "...add provided " << *pfr << std::endl;
168
65585
        Assert(pfr->getResult() == proven);
169
65585
        cdp.addProof(pfr);
170
65585
        proofStepProcessed = true;
171
      }
172
173
66553
      Trace("smt-pppg-debug") << "...update" << std::endl;
174
66553
      TrustNodeKind tnk = (*it).second.getKind();
175
66553
      if (tnk == TrustNodeKind::REWRITE)
176
      {
177
32562
        Trace("smt-pppg-debug")
178
16281
            << "...rewritten from " << proven[0] << std::endl;
179
16281
        Assert(proven.getKind() == kind::EQUAL);
180
16281
        if (!proofStepProcessed)
181
        {
182
          // maybe its just an (extended) rewrite?
183
1586
          Node pr = theory::Rewriter::callExtendedRewrite(proven[0]);
184
793
          if (proven[1] == pr)
185
          {
186
16
            Node idr = mkMethodId(MethodId::RW_EXT_REWRITE);
187
8
            Trace("smt-pppg-debug") << "...add simple rewrite" << std::endl;
188
8
            cdp.addStep(proven, PfRule::REWRITE, {}, {proven[0], idr});
189
8
            proofStepProcessed = true;
190
          }
191
        }
192
16281
        transChildren.push_back(proven);
193
        // continue with source
194
16281
        curr = proven[0];
195
16281
        success = true;
196
        // find the next node
197
16281
        Trace("smt-pppg") << "...continue " << curr << std::endl;
198
16281
        it = d_src.find(curr);
199
      }
200
      else
201
      {
202
50272
        Trace("smt-pppg") << "...lemma" << std::endl;
203
50272
        Assert(tnk == TrustNodeKind::LEMMA);
204
      }
205
206
66553
      if (!proofStepProcessed)
207
      {
208
1920
        Trace("smt-pppg-debug")
209
960
            << "...justify missing step with "
210
960
            << (tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp) << std::endl;
211
        // add trusted step, the rule depends on the kind of trust node
212
1920
        cdp.addStep(
213
960
            proven, tnk == TrustNodeKind::LEMMA ? d_ra : d_rpp, {}, {proven});
214
      }
215
    }
216
  } while (success);
217
218
  // prove ( curr == f ), which is not necessary if they are the same
219
  // modulo symmetry.
220
50272
  if (!CDProof::isSame(f, curr))
221
  {
222
27448
    Node fullRewrite = curr.eqNode(f);
223
13724
    if (transChildren.size() >= 2)
224
    {
225
1829
      Trace("smt-pppg") << "...apply trans to get " << fullRewrite << std::endl;
226
1829
      std::reverse(transChildren.begin(), transChildren.end());
227
1829
      cdp.addStep(fullRewrite, PfRule::TRANS, transChildren, {});
228
    }
229
13724
    Trace("smt-pppg") << "...eq_resolve to prove" << std::endl;
230
    // prove f
231
13724
    cdp.addStep(f, PfRule::EQ_RESOLVE, {curr, fullRewrite}, {});
232
13724
    Trace("smt-pppg") << "...finished" << std::endl;
233
  }
234
235
  // overall, proof is:
236
  //        --------- from proof generator       ---------- from proof generator
237
  //        F_1 = F_2          ...               F_{n-1} = F_n
238
  // ---?   -------------------------------------------------- TRANS
239
  // F_1    F_1 = F_n
240
  // ---------------- EQ_RESOLVE
241
  // F_n
242
  // Note F_1 may have been given a proof if it was not an input assumption.
243
244
50272
  return cdp.getProofFor(f);
245
}
246
247
7987
ProofNodeManager* PreprocessProofGenerator::getManager() { return d_pnm; }
248
249
413
LazyCDProof* PreprocessProofGenerator::allocateHelperProof()
250
{
251
413
  return d_helperProofs.allocateProof(nullptr, d_ctx);
252
}
253
254
164056
std::string PreprocessProofGenerator::identify() const { return d_name; }
255
256
3027
void PreprocessProofGenerator::checkEagerPedantic(PfRule r)
257
{
258
3027
  if (options::proofCheck() == options::ProofCheckMode::EAGER)
259
  {
260
    // catch a pedantic failure now, which otherwise would not be
261
    // triggered since we are doing lazy proof generation
262
    ProofChecker* pc = d_pnm->getChecker();
263
    std::stringstream serr;
264
    if (pc->isPedanticFailure(r, serr))
265
    {
266
      Unhandled() << "PreprocessProofGenerator::checkEagerPedantic: "
267
                  << serr.str();
268
    }
269
  }
270
3027
}
271
272
}  // namespace smt
273
31125
}  // namespace cvc5