1 /********************* */
2 /*! \file theory_proof_step_buffer.h
4 ** Top contributors (to current version):
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2020 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
12 ** \brief Theory proof step buffer utility.
15 #include "cvc4_private.h"
17 #ifndef CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H
18 #define CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H
22 #include "expr/node.h"
23 #include "expr/proof_step_buffer.h"
24 #include "theory/builtin/proof_checker.h"
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
33 class TheoryProofStepBuffer
: public ProofStepBuffer
36 TheoryProofStepBuffer(ProofChecker
* pc
= nullptr);
37 ~TheoryProofStepBuffer() {}
38 //---------------------------- utilities builtin proof rules
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.
45 bool applyEqIntro(Node src
,
47 const std::vector
<Node
>& exp
,
48 MethodId ids
= MethodId::SB_DEFAULT
,
49 MethodId idr
= MethodId::RW_REWRITE
);
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.
56 bool applyPredTransform(Node src
,
58 const std::vector
<Node
>& exp
,
59 MethodId ids
= MethodId::SB_DEFAULT
,
60 MethodId idr
= MethodId::RW_REWRITE
);
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.
67 bool applyPredIntro(Node tgt
,
68 const std::vector
<Node
>& exp
,
69 MethodId ids
= MethodId::SB_DEFAULT
,
70 MethodId idr
= MethodId::RW_REWRITE
);
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
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.
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
88 //---------------------------- utility methods for normalizing clauses
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.
96 * @param n the clause to be normalized
97 * @return the normalized clause node
99 Node
factorReorderElimDoubleNeg(Node n
);
102 * Eliminates double negation of a literal if it has the form
104 * If the elimination happens, a step is added to this proof step buffer.
106 * @param n the node to have the top-level double negation eliminated
107 * @return the normalized clause node
109 Node
elimDoubleNegLit(Node n
);
112 } // namespace theory
115 #endif /* CVC4__THEORY__THEORY_PROOF_STEP_BUFFER_H */