GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_node_manager.cpp Lines: 115 158 72.8 %
Date: 2021-03-23 Branches: 207 722 28.7 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_node_manager.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, 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 Implementation of proof node manager
13
 **/
14
15
#include "expr/proof_node_manager.h"
16
17
#include "expr/proof.h"
18
#include "expr/proof_checker.h"
19
#include "expr/proof_node.h"
20
#include "expr/proof_node_algorithm.h"
21
#include "options/proof_options.h"
22
#include "theory/rewriter.h"
23
24
using namespace CVC4::kind;
25
26
namespace CVC4 {
27
28
962
ProofNodeManager::ProofNodeManager(ProofChecker* pc)
29
962
    : d_checker(pc)
30
{
31
962
  d_true = NodeManager::currentNM()->mkConst(true);
32
962
}
33
34
13996231
std::shared_ptr<ProofNode> ProofNodeManager::mkNode(
35
    PfRule id,
36
    const std::vector<std::shared_ptr<ProofNode>>& children,
37
    const std::vector<Node>& args,
38
    Node expected)
39
{
40
27992462
  Trace("pnm") << "ProofNodeManager::mkNode " << id << " {" << expected.getId()
41
13996231
               << "} " << expected << "\n";
42
27992462
  Node res = checkInternal(id, children, args, expected);
43
13996231
  if (res.isNull())
44
  {
45
    // if it was invalid, then we return the null node
46
    return nullptr;
47
  }
48
  // otherwise construct the proof node and set its proven field
49
  std::shared_ptr<ProofNode> pn =
50
27992462
      std::make_shared<ProofNode>(id, children, args);
51
13996231
  pn->d_proven = res;
52
13996231
  return pn;
53
}
54
55
7964044
std::shared_ptr<ProofNode> ProofNodeManager::mkAssume(Node fact)
56
{
57
7964044
  Assert(!fact.isNull());
58
7964044
  Assert(fact.getType().isBoolean());
59
7964044
  return mkNode(PfRule::ASSUME, {}, {fact}, fact);
60
}
61
62
220
std::shared_ptr<ProofNode> ProofNodeManager::mkTrans(
63
    const std::vector<std::shared_ptr<ProofNode>>& children, Node expected)
64
{
65
220
  Assert(!children.empty());
66
220
  if (children.size() == 1)
67
  {
68
    Assert(expected.isNull() || children[0]->getResult() == expected);
69
    return children[0];
70
  }
71
220
  return mkNode(PfRule::TRANS, children, {}, expected);
72
}
73
74
177259
std::shared_ptr<ProofNode> ProofNodeManager::mkScope(
75
    std::shared_ptr<ProofNode> pf,
76
    std::vector<Node>& assumps,
77
    bool ensureClosed,
78
    bool doMinimize,
79
    Node expected)
80
{
81
177259
  if (!ensureClosed)
82
  {
83
43828
    return mkNode(PfRule::SCOPE, {pf}, assumps, expected);
84
  }
85
133431
  Trace("pnm-scope") << "ProofNodeManager::mkScope " << assumps << std::endl;
86
  // we first ensure the assumptions are flattened
87
266862
  std::unordered_set<Node, NodeHashFunction> ac{assumps.begin(), assumps.end()};
88
  // map from the rewritten form of assumptions to the original. This is only
89
  // computed in the rare case when we need rewriting to match the
90
  // assumptions. An example of this is for Boolean constant equalities in
91
  // scoped proofs from the proof equality engine.
92
266862
  std::unordered_map<Node, Node, NodeHashFunction> acr;
93
  // whether we have compute the map above
94
133431
  bool computedAcr = false;
95
96
  // The free assumptions of the proof
97
266862
  std::map<Node, std::vector<std::shared_ptr<ProofNode>>> famap;
98
133431
  expr::getFreeAssumptionsMap(pf, famap);
99
266862
  std::unordered_set<Node, NodeHashFunction> acu;
100
593180
  for (const std::pair<const Node, std::vector<std::shared_ptr<ProofNode>>>&
101
133431
           fa : famap)
102
  {
103
1186360
    Node a = fa.first;
104
1033942
    if (ac.find(a) != ac.end())
105
    {
106
      // already covered by an assumption
107
440762
      acu.insert(a);
108
440762
      continue;
109
    }
110
    // trivial assumption
111
152418
    if (a == d_true)
112
    {
113
      Trace("pnm-scope") << "- justify trivial True assumption\n";
114
      for (std::shared_ptr<ProofNode> pfs : fa.second)
115
      {
116
        Assert(pfs->getResult() == a);
117
        updateNode(pfs.get(), PfRule::MACRO_SR_PRED_INTRO, {}, {a});
118
      }
119
      Trace("pnm-scope") << "...finished" << std::endl;
120
      acu.insert(a);
121
      continue;
122
    }
123
152418
    Trace("pnm-scope") << "- try matching free assumption " << a << "\n";
124
    // otherwise it may be due to symmetry?
125
304836
    Node aeqSym = CDProof::getSymmFact(a);
126
152418
    Trace("pnm-scope") << "  - try sym " << aeqSym << "\n";
127
304836
    Node aMatch;
128
152418
    if (!aeqSym.isNull() && ac.count(aeqSym))
129
    {
130
303270
      Trace("pnm-scope") << "- reorient assumption " << aeqSym << " via " << a
131
303270
                         << " for " << fa.second.size() << " proof nodes"
132
151635
                         << std::endl;
133
151635
      aMatch = aeqSym;
134
    }
135
    else
136
    {
137
      // Otherwise, may be derivable by rewriting. Note this is used in
138
      // ensuring that proofs from the proof equality engine that involve
139
      // equality with Boolean constants are closed.
140
783
      if (!computedAcr)
141
      {
142
292
        computedAcr = true;
143
4328
        for (const Node& acc : ac)
144
        {
145
8072
          Node accr = theory::Rewriter::rewrite(acc);
146
4036
          if (accr != acc)
147
          {
148
1634
            acr[accr] = acc;
149
          }
150
        }
151
      }
152
1566
      Node ar = theory::Rewriter::rewrite(a);
153
      std::unordered_map<Node, Node, NodeHashFunction>::iterator itr =
154
783
          acr.find(ar);
155
783
      if (itr != acr.end())
156
      {
157
783
        aMatch = itr->second;
158
      }
159
    }
160
161
    // if we found a match either by symmetry or rewriting, then we connect
162
    // the assumption here.
163
152418
    if (!aMatch.isNull())
164
    {
165
304836
      std::shared_ptr<ProofNode> pfaa = mkAssume(aMatch);
166
      // must correct the orientation on this leaf
167
304836
      std::vector<std::shared_ptr<ProofNode>> children;
168
152418
      children.push_back(pfaa);
169
416136
      for (std::shared_ptr<ProofNode> pfs : fa.second)
170
      {
171
263718
        Assert(pfs->getResult() == a);
172
        // use SYMM if possible
173
263718
        if (aMatch == aeqSym)
174
        {
175
262720
          updateNode(pfs.get(), PfRule::SYMM, children, {});
176
        }
177
        else
178
        {
179
998
          updateNode(pfs.get(), PfRule::MACRO_SR_PRED_TRANSFORM, children, {a});
180
        }
181
      }
182
152418
      Trace("pnm-scope") << "...finished" << std::endl;
183
152418
      acu.insert(aMatch);
184
152418
      continue;
185
    }
186
    // If we did not find a match, it is an error, since all free assumptions
187
    // should be arguments to SCOPE.
188
    std::stringstream ss;
189
190
    bool dumpProofTraceOn = Trace.isOn("dump-proof-error");
191
    if (dumpProofTraceOn)
192
    {
193
      ss << "The proof : " << *pf << std::endl;
194
    }
195
    ss << std::endl << "Free assumption: " << a << std::endl;
196
    for (const Node& aprint : ac)
197
    {
198
      ss << "- assumption: " << aprint << std::endl;
199
    }
200
    if (!dumpProofTraceOn)
201
    {
202
      ss << "Use -t dump-proof-error for details on proof" << std::endl;
203
    }
204
    Unreachable() << "Generated a proof that is not closed by the scope: "
205
                  << ss.str() << std::endl;
206
  }
207
133431
  if (acu.size() < ac.size())
208
  {
209
    // All assumptions should match a free assumption; if one does not, then
210
    // the explanation could have been smaller.
211
36409
    for (const Node& a : ac)
212
    {
213
30465
      if (acu.find(a) == acu.end())
214
      {
215
16006
        Notice() << "ProofNodeManager::mkScope: assumption " << a
216
                 << " does not match a free assumption in proof" << std::endl;
217
      }
218
    }
219
  }
220
133431
  if (doMinimize && acu.size() < ac.size())
221
  {
222
5492
    assumps.clear();
223
5492
    assumps.insert(assumps.end(), acu.begin(), acu.end());
224
  }
225
127939
  else if (ac.size() < assumps.size())
226
  {
227
    // remove duplicates to avoid redundant literals in clauses
228
82
    assumps.clear();
229
82
    assumps.insert(assumps.end(), ac.begin(), ac.end());
230
  }
231
266862
  Node minExpected;
232
133431
  NodeManager* nm = NodeManager::currentNM();
233
266862
  Node exp;
234
133431
  if (assumps.empty())
235
  {
236
    // SCOPE with no arguments is a no-op, just return original
237
1919
    return pf;
238
  }
239
263024
  Node conc = pf->getResult();
240
131512
  exp = assumps.size() == 1 ? assumps[0] : nm->mkNode(AND, assumps);
241
131512
  if (conc.isConst() && !conc.getConst<bool>())
242
  {
243
37483
    minExpected = exp.notNode();
244
  }
245
  else
246
  {
247
94029
    minExpected = nm->mkNode(IMPLIES, exp, conc);
248
  }
249
131512
  return mkNode(PfRule::SCOPE, {pf}, assumps, minExpected);
250
}
251
252
314224
bool ProofNodeManager::updateNode(
253
    ProofNode* pn,
254
    PfRule id,
255
    const std::vector<std::shared_ptr<ProofNode>>& children,
256
    const std::vector<Node>& args)
257
{
258
314224
  return updateNodeInternal(pn, id, children, args, true);
259
}
260
261
1861419
bool ProofNodeManager::updateNode(ProofNode* pn, ProofNode* pnr)
262
{
263
1861419
  Assert(pn != nullptr);
264
1861419
  Assert(pnr != nullptr);
265
1861419
  if (pn->getResult() != pnr->getResult())
266
  {
267
    return false;
268
  }
269
  // can shortcut re-check of rule
270
1861419
  return updateNodeInternal(
271
1861419
      pn, pnr->getRule(), pnr->getChildren(), pnr->getArguments(), false);
272
}
273
274
14310455
Node ProofNodeManager::checkInternal(
275
    PfRule id,
276
    const std::vector<std::shared_ptr<ProofNode>>& children,
277
    const std::vector<Node>& args,
278
    Node expected)
279
{
280
14310455
  Node res;
281
14310455
  if (d_checker)
282
  {
283
    // check with the checker, which takes expected as argument
284
14310455
    res = d_checker->check(id, children, args, expected);
285
14310455
    Assert(!res.isNull())
286
        << "ProofNodeManager::checkInternal: failed to check proof";
287
  }
288
  else
289
  {
290
    // otherwise we trust the expected value, if it exists
291
    Assert(!expected.isNull()) << "ProofNodeManager::checkInternal: no checker "
292
                                  "or expected value provided";
293
    res = expected;
294
  }
295
14310455
  return res;
296
}
297
298
6200337
ProofChecker* ProofNodeManager::getChecker() const { return d_checker; }
299
300
2175643
bool ProofNodeManager::updateNodeInternal(
301
    ProofNode* pn,
302
    PfRule id,
303
    const std::vector<std::shared_ptr<ProofNode>>& children,
304
    const std::vector<Node>& args,
305
    bool needsCheck)
306
{
307
2175643
  Assert(pn != nullptr);
308
  // ---------------- check for cyclic
309
2175643
  if (options::proofEagerChecking())
310
  {
311
    std::unordered_set<const ProofNode*> visited;
312
    for (const std::shared_ptr<ProofNode>& cpc : children)
313
    {
314
      if (expr::containsSubproof(cpc.get(), pn, visited))
315
      {
316
        std::stringstream ss;
317
        ss << "ProofNodeManager::updateNode: attempting to make cyclic proof! "
318
           << id << " " << pn->getResult() << ", children = " << std::endl;
319
        for (const std::shared_ptr<ProofNode>& cp : children)
320
        {
321
          ss << "  " << cp->getRule() << " " << cp->getResult() << std::endl;
322
        }
323
        ss << "Full children:" << std::endl;
324
        for (const std::shared_ptr<ProofNode>& cp : children)
325
        {
326
          ss << "  - ";
327
          cp->printDebug(ss);
328
          ss << std::endl;
329
        }
330
        Unreachable() << ss.str();
331
      }
332
    }
333
  }
334
  // ---------------- end check for cyclic
335
336
  // should have already computed what is proven
337
2175643
  Assert(!pn->d_proven.isNull())
338
      << "ProofNodeManager::updateProofNode: invalid proof provided";
339
2175643
  if (needsCheck)
340
  {
341
    // We expect to prove the same thing as before
342
628448
    Node res = checkInternal(id, children, args, pn->d_proven);
343
314224
    if (res.isNull())
344
    {
345
      // if it was invalid, then we do not update
346
      return false;
347
    }
348
    // proven field should already be the same as the result
349
314224
    Assert(res == pn->d_proven);
350
  }
351
352
  // we update its value
353
2175643
  pn->setValue(id, children, args);
354
2175643
  return true;
355
}
356
357
26685
}  // namespace CVC4