GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/proof_step_buffer.h Lines: 2 2 100.0 %
Date: 2021-03-23 Branches: 1 4 25.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file proof_step_buffer.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Gereon Kremer
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 Proof step and proof step buffer utilities.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__EXPR__PROOF_STEP_BUFFER_H
18
#define CVC4__EXPR__PROOF_STEP_BUFFER_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "expr/proof_rule.h"
24
25
namespace CVC4 {
26
27
class ProofChecker;
28
29
/**
30
 * Information for constructing a step in a CDProof. Notice that the conclusion
31
 * of the proof step is intentionally not included in this data structure.
32
 * Instead, it is intended that conclusions may be associated with proof steps
33
 * based on e.g. the result of proof checking.
34
 */
35
8143722
class ProofStep
36
{
37
 public:
38
  ProofStep();
39
  ProofStep(PfRule r,
40
            const std::vector<Node>& children,
41
            const std::vector<Node>& args);
42
  /** The proof rule */
43
  PfRule d_rule;
44
  /** The proof children */
45
  std::vector<Node> d_children;
46
  /** The proof arguments */
47
  std::vector<Node> d_args;
48
};
49
std::ostream& operator<<(std::ostream& out, ProofStep step);
50
51
/**
52
 * Class used to speculatively try and buffer a set of proof steps before
53
 * sending them to a proof object.
54
 */
55
class ProofStepBuffer
56
{
57
 public:
58
  ProofStepBuffer(ProofChecker* pc = nullptr);
59
6419
  ~ProofStepBuffer() {}
60
  /**
61
   * Returns the conclusion of the proof step, as determined by the proof
62
   * checker of the given proof. If this is non-null, then the given step
63
   * is added to the buffer maintained by this class.
64
   *
65
   * If expected is non-null, then this method returns null if the result of
66
   * checking is not equal to expected.
67
   */
68
  Node tryStep(PfRule id,
69
               const std::vector<Node>& children,
70
               const std::vector<Node>& args,
71
               Node expected = Node::null());
72
  /** Same as above, without checking */
73
  void addStep(PfRule id,
74
               const std::vector<Node>& children,
75
               const std::vector<Node>& args,
76
               Node expected);
77
  /** Multi-step version */
78
  void addSteps(ProofStepBuffer& psb);
79
  /** pop step */
80
  void popStep();
81
  /** Get num steps */
82
  size_t getNumSteps() const;
83
  /** Get steps */
84
  const std::vector<std::pair<Node, ProofStep>>& getSteps() const;
85
  /** Clear */
86
  void clear();
87
88
 private:
89
  /** The proof checker*/
90
  ProofChecker* d_checker;
91
  /** the queued proof steps */
92
  std::vector<std::pair<Node, ProofStep>> d_steps;
93
};
94
95
}  // namespace CVC4
96
97
#endif /* CVC4__EXPR__PROOF_STEP_BUFFER_H */