Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_proof_step_buffer.h	Lines:	1	1	100.0 %
Date:	2021-05-22	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__THEORY__THEORY_PROOF_STEP_BUFFER_H
#define CVC5__THEORY__THEORY_PROOF_STEP_BUFFER_H

#include <vector>

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

namespace cvc5 {
namespace theory {
/**
 * 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 theory
}  // namespace cvc5

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