GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_node.cpp Lines: 31 34 91.2 %
Date: 2021-03-23 Branches: 15 30 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_node.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 Implementation of proof node utility
13
 **/
14
15
#include "expr/proof_node.h"
16
17
#include "expr/proof_node_algorithm.h"
18
#include "expr/proof_node_to_sexpr.h"
19
20
namespace CVC4 {
21
22
16262766
ProofNode::ProofNode(PfRule id,
23
                     const std::vector<std::shared_ptr<ProofNode>>& children,
24
16262766
                     const std::vector<Node>& args)
25
{
26
16262766
  setValue(id, children, args);
27
16262766
}
28
29
52811729
PfRule ProofNode::getRule() const { return d_rule; }
30
31
24475280
const std::vector<std::shared_ptr<ProofNode>>& ProofNode::getChildren() const
32
{
33
24475280
  return d_children;
34
}
35
36
24013113
const std::vector<Node>& ProofNode::getArguments() const { return d_args; }
37
38
51795334
Node ProofNode::getResult() const { return d_proven; }
39
40
94376
bool ProofNode::isClosed()
41
{
42
188752
  std::vector<Node> assumps;
43
94376
  expr::getFreeAssumptions(this, assumps);
44
188752
  return assumps.empty();
45
}
46
47
2171160
std::shared_ptr<ProofNode> ProofNode::clone() const
48
{
49
4342320
  std::vector<std::shared_ptr<ProofNode>> cchildren;
50
4267620
  for (const std::shared_ptr<ProofNode>& cp : d_children)
51
  {
52
2096460
    cchildren.push_back(cp->clone());
53
  }
54
  std::shared_ptr<ProofNode> thisc =
55
2171160
      std::make_shared<ProofNode>(d_rule, cchildren, d_args);
56
2171160
  thisc->d_proven = d_proven;
57
4342320
  return thisc;
58
}
59
60
18438409
void ProofNode::setValue(
61
    PfRule id,
62
    const std::vector<std::shared_ptr<ProofNode>>& children,
63
    const std::vector<Node>& args)
64
{
65
18438409
  d_rule = id;
66
18438409
  d_children = children;
67
18438409
  d_args = args;
68
18438409
}
69
70
31366
void ProofNode::printDebug(std::ostream& os) const
71
{
72
  // convert to sexpr and print
73
62732
  ProofNodeToSExpr pnts;
74
62732
  Node ps = pnts.convertToSExpr(this);
75
31366
  os << ps;
76
31366
}
77
78
std::ostream& operator<<(std::ostream& out, const ProofNode& pn)
79
{
80
  pn.printDebug(out);
81
  return out;
82
}
83
84
26685
}  // namespace CVC4