Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/proof/theory_proof_step_buffer.h	Lines:	1	1	100.0 %
Date:	2021-09-18	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Haniel Barbosa
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * Theory proof step buffer utility.
 */

#include "cvc5_private.h"

#ifndef CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H
#define CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H

#include <vector>

#include "expr/node.h"
#include "proof/proof_step_buffer.h"
#include "theory/builtin/proof_checker.h"

namespace cvc5 {
/**
 * Class used to speculatively try and buffer a set of proof steps before
 * sending them to a proof object, extended with theory-specfic proof rule
 * utilities.
 */
class TheoryProofStepBuffer : public ProofStepBuffer
{
 public:
  TheoryProofStepBuffer(ProofChecker* pc = nullptr);
  ~TheoryProofStepBuffer() {}
  //---------------------------- utilities builtin proof rules
  /**
   * Apply equality introduction. If this method returns true, it adds proof
   * step(s) to the buffer that conclude (= src tgt) from premises exp. In
   * particular, it may attempt to apply the rule MACRO_SR_EQ_INTRO. This
   * method should be applied when tgt is equivalent to src assuming exp.
   */
  bool applyEqIntro(Node src,
                    Node tgt,
                    const std::vector<Node>& exp,
                    MethodId ids = MethodId::SB_DEFAULT,
                    MethodId ida = MethodId::SBA_SEQUENTIAL,
                    MethodId idr = MethodId::RW_REWRITE);
  /**
   * Apply predicate transform. If this method returns true, it adds (at most
   * one) proof step to the buffer that conclude tgt from premises src, exp. In
   * particular, it may attempt to apply MACRO_SR_PRED_TRANSFORM. This method
   * should be applied when src and tgt are equivalent formulas assuming exp.
   */
  bool applyPredTransform(Node src,
                          Node tgt,
                          const std::vector<Node>& exp,
                          MethodId ids = MethodId::SB_DEFAULT,
                          MethodId ida = MethodId::SBA_SEQUENTIAL,
                          MethodId idr = MethodId::RW_REWRITE);
  /**
   * Apply predicate introduction. If this method returns true, it adds proof
   * step(s) to the buffer that conclude tgt from premises exp. In particular,
   * it may attempt to apply the rule MACRO_SR_PRED_INTRO. This method should be
   * applied when tgt is equivalent to true assuming exp.
   */
  bool applyPredIntro(Node tgt,
                      const std::vector<Node>& exp,
                      MethodId ids = MethodId::SB_DEFAULT,
                      MethodId ida = MethodId::SBA_SEQUENTIAL,
                      MethodId idr = MethodId::RW_REWRITE);
  /**
   * Apply predicate elimination. This method returns the result of applying
   * the rule MACRO_SR_PRED_ELIM on src, exp. The returned formula is equivalent
   * to src assuming exp. If the return value is equivalent to src, then no
   * proof step is added to this buffer, since this step is a no-op in this
   * case.
   *
   * Notice that in contrast to the other rules above, predicate elimination
   * never fails and proves a formula that is not explicitly given as an
   * argument tgt. Thus, the return value of this method is Node not bool.
   */
  Node applyPredElim(Node src,
                     const std::vector<Node>& exp,
                     MethodId ids = MethodId::SB_DEFAULT,
                     MethodId ida = MethodId::SBA_SEQUENTIAL,
                     MethodId idr = MethodId::RW_REWRITE);
  //---------------------------- end utilities builtin proof rules

  //---------------------------- utility methods for normalizing clauses
  /**
   * Normalizes a non-unit clause (an OR node) according to factoring and
   * reordering, i.e. removes duplicates and reorders literals (according to
   * node ids). Moreover it eliminates double negations, which can be done also
   * for unit clauses (a arbitrary Boolean node). All normalization steps are
   * tracked via proof steps added to this proof step buffer.
   *
   * @param n the clause to be normalized
   * @return the normalized clause node
   */
  Node factorReorderElimDoubleNeg(Node n);

  /**
   * Eliminates double negation of a literal if it has the form
   *  (not (not t))
   * If the elimination happens, a step is added to this proof step buffer.
   *
   * @param n the node to have the top-level double negation eliminated
   * @return the normalized clause node
   */
  Node elimDoubleNegLit(Node n);
};

}  // namespace cvc5

#endif /* CVC5__PROOF__THEORY_PROOF_STEP_BUFFER_H */


Generated by: GCOVR (Version 3.2)

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