GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/theory_proof_step_buffer.h Lines: 1 1 100.0 %
Date: 2021-03-22 Branches: 0 0 0.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_proof_step_buffer.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa
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 Theory proof step buffer utility.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H
18
#define CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
#include "expr/proof_step_buffer.h"
24
#include "theory/builtin/proof_checker.h"
25
26
namespace CVC4 {
27
namespace theory {
28
/**
29
 * Class used to speculatively try and buffer a set of proof steps before
30
 * sending them to a proof object, extended with theory-specfic proof rule
31
 * utilities.
32
 */
33
class TheoryProofStepBuffer : public ProofStepBuffer
34
{
35
 public:
36
  TheoryProofStepBuffer(ProofChecker* pc = nullptr);
37
6419
  ~TheoryProofStepBuffer() {}
38
  //---------------------------- utilities builtin proof rules
39
  /**
40
   * Apply equality introduction. If this method returns true, it adds proof
41
   * step(s) to the buffer that conclude (= src tgt) from premises exp. In
42
   * particular, it may attempt to apply the rule MACRO_SR_EQ_INTRO. This
43
   * method should be applied when tgt is equivalent to src assuming exp.
44
   */
45
  bool applyEqIntro(Node src,
46
                    Node tgt,
47
                    const std::vector<Node>& exp,
48
                    MethodId ids = MethodId::SB_DEFAULT,
49
                    MethodId idr = MethodId::RW_REWRITE);
50
  /**
51
   * Apply predicate transform. If this method returns true, it adds (at most
52
   * one) proof step to the buffer that conclude tgt from premises src, exp. In
53
   * particular, it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method
54
   * should be applied when src and tgt are equivalent formulas assuming exp.
55
   */
56
  bool applyPredTransform(Node src,
57
                          Node tgt,
58
                          const std::vector<Node>& exp,
59
                          MethodId ids = MethodId::SB_DEFAULT,
60
                          MethodId idr = MethodId::RW_REWRITE);
61
  /**
62
   * Apply predicate introduction. If this method returns true, it adds proof
63
   * step(s) to the buffer that conclude tgt from premises exp. In particular,
64
   * it may attempt to apply the rule MACRO_SR_PRED_INTRO. This method should be
65
   * applied when tgt is equivalent to true assuming exp.
66
   */
67
  bool applyPredIntro(Node tgt,
68
                      const std::vector<Node>& exp,
69
                      MethodId ids = MethodId::SB_DEFAULT,
70
                      MethodId idr = MethodId::RW_REWRITE);
71
  /**
72
   * Apply predicate elimination. This method returns the result of applying
73
   * the rule MACRO_SR_PRED_ELIM on src, exp. The returned formula is equivalent
74
   * to src assuming exp. If the return value is equivalent to src, then no
75
   * proof step is added to this buffer, since this step is a no-op in this
76
   * case.
77
   *
78
   * Notice that in contrast to the other rules above, predicate elimination
79
   * never fails and proves a formula that is not explicitly given as an
80
   * argument tgt. Thus, the return value of this method is Node not bool.
81
   */
82
  Node applyPredElim(Node src,
83
                     const std::vector<Node>& exp,
84
                     MethodId ids = MethodId::SB_DEFAULT,
85
                     MethodId idr = MethodId::RW_REWRITE);
86
  //---------------------------- end utilities builtin proof rules
87
88
  //---------------------------- utility methods for normalizing clauses
89
  /**
90
   * Normalizes a non-unit clause (an OR node) according to factoring and
91
   * reordering, i.e. removes duplicates and reorders literals (according to
92
   * node ids). Moreover it eliminates double negations, which can be done also
93
   * for unit clauses (a arbitrary Boolean node). All normalization steps are
94
   * tracked via proof steps added to this proof step buffer.
95
   *
96
   * @param n the clause to be normalized
97
   * @return the normalized clause node
98
   */
99
  Node factorReorderElimDoubleNeg(Node n);
100
101
  /**
102
   * Eliminates double negation of a literal if it has the form
103
   *  (not (not t))
104
   * If the elimination happens, a step is added to this proof step buffer.
105
   *
106
   * @param n the node to have the top-level double negation eliminated
107
   * @return the normalized clause node
108
   */
109
  Node elimDoubleNegLit(Node n);
110
};
111
112
}  // namespace theory
113
}  // namespace CVC4
114
115
#endif /* CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H */