GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/eager_proof_generator.cpp Lines: 59 63 93.7 %
Date: 2021-03-22 Branches: 81 198 40.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file eager_proof_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Alex Ozdemir
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 the abstract proof generator class
13
 **/
14
15
#include "theory/eager_proof_generator.h"
16
17
#include "expr/proof.h"
18
#include "expr/proof_node.h"
19
#include "expr/proof_node_manager.h"
20
21
namespace CVC4 {
22
namespace theory {
23
24
58875
EagerProofGenerator::EagerProofGenerator(ProofNodeManager* pnm,
25
                                         context::Context* c,
26
58875
                                         std::string name)
27
58875
    : d_pnm(pnm), d_name(name), d_proofs(c == nullptr ? &d_context : c)
28
{
29
58875
}
30
31
330101
void EagerProofGenerator::setProofFor(Node f, std::shared_ptr<ProofNode> pf)
32
{
33
  // pf should prove f
34
660202
  Assert(pf->getResult() == f)
35
      << "EagerProofGenerator::setProofFor: unexpected result" << std::endl
36
330101
      << "Expected: " << f << std::endl
37
330101
      << "Actual: " << pf->getResult() << std::endl;
38
330101
  d_proofs[f] = pf;
39
330101
}
40
15304
void EagerProofGenerator::setProofForConflict(Node conf,
41
                                              std::shared_ptr<ProofNode> pf)
42
{
43
  // Normalize based on key
44
30608
  Node ckey = TrustNode::getConflictProven(conf);
45
15304
  setProofFor(ckey, pf);
46
15304
}
47
48
201912
void EagerProofGenerator::setProofForLemma(Node lem,
49
                                           std::shared_ptr<ProofNode> pf)
50
{
51
  // Normalize based on key
52
403824
  Node lkey = TrustNode::getLemmaProven(lem);
53
201912
  setProofFor(lkey, pf);
54
201912
}
55
56
71757
void EagerProofGenerator::setProofForPropExp(TNode lit,
57
                                             Node exp,
58
                                             std::shared_ptr<ProofNode> pf)
59
{
60
  // Normalize based on key
61
143514
  Node pekey = TrustNode::getPropExpProven(lit, exp);
62
71757
  setProofFor(pekey, pf);
63
71757
}
64
65
123531
std::shared_ptr<ProofNode> EagerProofGenerator::getProofFor(Node f)
66
{
67
123531
  NodeProofNodeMap::iterator it = d_proofs.find(f);
68
123531
  if (it == d_proofs.end())
69
  {
70
1105
    return nullptr;
71
  }
72
122426
  return (*it).second;
73
}
74
75
743484
bool EagerProofGenerator::hasProofFor(Node f)
76
{
77
743484
  return d_proofs.find(f) != d_proofs.end();
78
}
79
80
212315
TrustNode EagerProofGenerator::mkTrustNode(Node n,
81
                                           std::shared_ptr<ProofNode> pf,
82
                                           bool isConflict)
83
{
84
212315
  if (pf == nullptr)
85
  {
86
    return TrustNode::null();
87
  }
88
212315
  if (isConflict)
89
  {
90
    // this shouldnt modify the key
91
11206
    setProofForConflict(n, pf);
92
    // we can now return the trust node
93
11206
    return TrustNode::mkTrustConflict(n, this);
94
  }
95
  // this shouldnt modify the key
96
201109
  setProofForLemma(n, pf);
97
  // we can now return the trust node
98
201109
  return TrustNode::mkTrustLemma(n, this);
99
}
100
101
11827
TrustNode EagerProofGenerator::mkTrustNode(Node conc,
102
                                           PfRule id,
103
                                           const std::vector<Node>& exp,
104
                                           const std::vector<Node>& args,
105
                                           bool isConflict)
106
{
107
  // if no children, its easy
108
11827
  if (exp.empty())
109
  {
110
22774
    std::shared_ptr<ProofNode> pf = d_pnm->mkNode(id, {}, args, conc);
111
11387
    return mkTrustNode(conc, pf, isConflict);
112
  }
113
  // otherwise, we use CDProof + SCOPE
114
880
  CDProof cdp(d_pnm);
115
440
  cdp.addStep(conc, id, exp, args);
116
880
  std::shared_ptr<ProofNode> pf = cdp.getProofFor(conc);
117
  // We use mkNode instead of mkScope, since there is no reason to check
118
  // whether the free assumptions of pf are in exp, since they are by the
119
  // construction above.
120
880
  std::shared_ptr<ProofNode> pfs = d_pnm->mkNode(PfRule::SCOPE, {pf}, exp);
121
440
  return mkTrustNode(pfs->getResult(), pfs, isConflict);
122
}
123
124
2645
TrustNode EagerProofGenerator::mkTrustedRewrite(
125
    Node a, Node b, std::shared_ptr<ProofNode> pf)
126
{
127
2645
  if (pf == nullptr)
128
  {
129
    return TrustNode::null();
130
  }
131
5290
  Node eq = a.eqNode(b);
132
2645
  setProofFor(eq, pf);
133
2645
  return TrustNode::mkTrustRewrite(a, b, this);
134
}
135
136
1958
TrustNode EagerProofGenerator::mkTrustedPropagation(
137
    Node n, Node exp, std::shared_ptr<ProofNode> pf)
138
{
139
1958
  if (pf == nullptr)
140
  {
141
    return TrustNode::null();
142
  }
143
1958
  setProofForPropExp(n, exp, pf);
144
1958
  return TrustNode::mkTrustPropExp(n, exp, this);
145
}
146
147
9890
TrustNode EagerProofGenerator::mkTrustNodeSplit(Node f)
148
{
149
  // make the lemma
150
19780
  Node lem = f.orNode(f.notNode());
151
19780
  return mkTrustNode(lem, PfRule::SPLIT, {}, {f}, false);
152
}
153
154
263406
std::string EagerProofGenerator::identify() const { return d_name; }
155
156
}  // namespace theory
157
26676
}  // namespace CVC4