GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_engine_proof_generator.cpp Lines: 48 60 80.0 %
Date: 2021-03-23 Branches: 93 264 35.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_engine_proof_generator.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 theory engine proof generator
13
 **/
14
15
#include "theory/theory_engine_proof_generator.h"
16
17
#include <sstream>
18
19
#include "expr/proof_node.h"
20
21
using namespace CVC4::kind;
22
23
namespace CVC4 {
24
25
8997
TheoryEngineProofGenerator::TheoryEngineProofGenerator(ProofNodeManager* pnm,
26
8997
                                                       context::UserContext* u)
27
8997
    : d_pnm(pnm), d_proofs(u)
28
{
29
8997
  d_false = NodeManager::currentNM()->mkConst(false);
30
8997
}
31
32
20273
theory::TrustNode TheoryEngineProofGenerator::mkTrustExplain(
33
    TNode lit, Node exp, std::shared_ptr<LazyCDProof> lpf)
34
{
35
40546
  Node p;
36
20273
  theory::TrustNode trn;
37
20273
  if (lit == d_false)
38
  {
39
    // propagation of false is a conflict
40
111
    trn = theory::TrustNode::mkTrustConflict(exp, this);
41
111
    p = trn.getProven();
42
111
    Assert(p.getKind() == NOT);
43
  }
44
  else
45
  {
46
20162
    trn = theory::TrustNode::mkTrustPropExp(lit, exp, this);
47
20162
    p = trn.getProven();
48
20162
    Assert(p.getKind() == IMPLIES && p.getNumChildren() == 2);
49
  }
50
  // should not already be proven
51
20273
  NodeLazyCDProofMap::iterator it = d_proofs.find(p);
52
20273
  if (it == d_proofs.end())
53
  {
54
    // we will prove the fact p using the proof from lpf.
55
17240
    d_proofs.insert(p, lpf);
56
  }
57
40546
  return trn;
58
}
59
60
13764
std::shared_ptr<ProofNode> TheoryEngineProofGenerator::getProofFor(Node f)
61
{
62
27528
  Trace("tepg-debug") << "TheoryEngineProofGenerator::getProofFor: " << f
63
13764
                      << std::endl;
64
13764
  NodeLazyCDProofMap::iterator it = d_proofs.find(f);
65
13764
  if (it == d_proofs.end())
66
  {
67
    Trace("tepg-debug") << "...null" << std::endl;
68
    return nullptr;
69
  }
70
27528
  std::shared_ptr<LazyCDProof> lcp = (*it).second;
71
  // finalize it via scope
72
27528
  std::vector<Node> scopeAssumps;
73
  // should only ask this generator for proofs of implications, or conflicts
74
27528
  Node exp;
75
27528
  Node conclusion;
76
13764
  if (f.getKind() == IMPLIES && f.getNumChildren() == 2)
77
  {
78
13744
    exp = f[0];
79
13744
    conclusion = f[1];
80
  }
81
20
  else if (f.getKind() == NOT)
82
  {
83
20
    exp = f[0];
84
20
    conclusion = d_false;
85
  }
86
  else
87
  {
88
    Unhandled() << "TheoryEngineProofGenerator::getProofFor: unexpected fact "
89
                << f << std::endl;
90
    return nullptr;
91
  }
92
  // get the assumptions to assume in a scope
93
13764
  if (exp.getKind() == AND)
94
  {
95
116372
    for (const Node& fc : exp)
96
    {
97
103863
      scopeAssumps.push_back(fc);
98
    }
99
  }
100
  else
101
  {
102
1255
    scopeAssumps.push_back(exp);
103
  }
104
13764
  Trace("tepg-debug") << "...get proof body" << std::endl;
105
  // get the proof for conclusion
106
27528
  std::shared_ptr<ProofNode> pfb = lcp->getProofFor(conclusion);
107
13764
  Trace("tepg-debug") << "...mkScope" << std::endl;
108
  // call the scope method of proof node manager
109
27528
  std::shared_ptr<ProofNode> pf = d_pnm->mkScope(pfb, scopeAssumps);
110
111
13764
  if (pf->getResult() != f)
112
  {
113
    std::stringstream serr;
114
    serr << "TheoryEngineProofGenerator::getProofFor: Proof: " << std::endl;
115
    serr << *pf << std::endl;
116
    serr << "TheoryEngineProofGenerator::getProofFor: unexpected return proof"
117
         << std::endl;
118
    serr << "  Expected: " << f << std::endl;
119
    serr << "       Got: " << pf->getResult() << std::endl;
120
    Unhandled() << serr.str();
121
  }
122
13764
  Trace("tepg-debug") << "...finished" << std::endl;
123
13764
  return pf;
124
}
125
126
62077
std::string TheoryEngineProofGenerator::identify() const
127
{
128
62077
  return "TheoryEngineProofGenerator";
129
}
130
131
26685
}  // namespace CVC4