GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_step_buffer.cpp Lines: 26 44 59.1 %
Date: 2021-03-22 Branches: 18 90 20.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_step_buffer.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 step and proof step buffer utilities.
13
 **/
14
15
#include "expr/proof_step_buffer.h"
16
17
#include "expr/proof_checker.h"
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
23
2571
ProofStep::ProofStep() : d_rule(PfRule::UNKNOWN) {}
24
1782473
ProofStep::ProofStep(PfRule r,
25
                     const std::vector<Node>& children,
26
1782473
                     const std::vector<Node>& args)
27
1782473
    : d_rule(r), d_children(children), d_args(args)
28
{
29
1782473
}
30
std::ostream& operator<<(std::ostream& out, ProofStep step)
31
{
32
  out << "(step " << step.d_rule;
33
  for (const Node& c : step.d_children)
34
  {
35
    out << " " << c;
36
  }
37
  if (!step.d_args.empty())
38
  {
39
    out << " :args";
40
    for (const Node& a : step.d_args)
41
    {
42
      out << " " << a;
43
    }
44
  }
45
  out << ")";
46
  return out;
47
}
48
49
6419
ProofStepBuffer::ProofStepBuffer(ProofChecker* pc) : d_checker(pc) {}
50
51
27715
Node ProofStepBuffer::tryStep(PfRule id,
52
                              const std::vector<Node>& children,
53
                              const std::vector<Node>& args,
54
                              Node expected)
55
{
56
27715
  if (d_checker == nullptr)
57
  {
58
    Assert(false) << "ProofStepBuffer::ProofStepBuffer: no proof checker.";
59
    return Node::null();
60
  }
61
  Node res =
62
55430
      d_checker->checkDebug(id, children, args, expected, "pf-step-buffer");
63
27715
  if (!res.isNull())
64
  {
65
    // add proof step
66
55184
    d_steps.push_back(
67
55184
        std::pair<Node, ProofStep>(res, ProofStep(id, children, args)));
68
  }
69
27715
  return res;
70
}
71
72
1063266
void ProofStepBuffer::addStep(PfRule id,
73
                              const std::vector<Node>& children,
74
                              const std::vector<Node>& args,
75
                              Node expected)
76
{
77
2126532
  d_steps.push_back(
78
2126532
      std::pair<Node, ProofStep>(expected, ProofStep(id, children, args)));
79
1063266
}
80
81
void ProofStepBuffer::addSteps(ProofStepBuffer& psb)
82
{
83
  const std::vector<std::pair<Node, ProofStep>>& steps = psb.getSteps();
84
  for (const std::pair<Node, ProofStep>& step : steps)
85
  {
86
    addStep(step.second.d_rule,
87
            step.second.d_children,
88
            step.second.d_args,
89
            step.first);
90
  }
91
}
92
93
185
void ProofStepBuffer::popStep()
94
{
95
185
  Assert(!d_steps.empty());
96
185
  if (!d_steps.empty())
97
  {
98
185
    d_steps.pop_back();
99
  }
100
185
}
101
102
size_t ProofStepBuffer::getNumSteps() const { return d_steps.size(); }
103
104
128738
const std::vector<std::pair<Node, ProofStep>>& ProofStepBuffer::getSteps() const
105
{
106
128738
  return d_steps;
107
}
108
109
129315
void ProofStepBuffer::clear() { d_steps.clear(); }
110
111
26676
}  // namespace CVC4