Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/builtin/theory_builtin_rewriter.h	Lines:	2	2	100.0 %
Date:	2021-11-07	Branches:	1	2	50.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * [[ Add one-line brief description here ]]
 *
 * [[ Add lengthier description here ]]
 * \todo document this file
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H

#include "theory/theory_rewriter.h"

namespace cvc5 {
namespace theory {
namespace builtin {

class TheoryBuiltinRewriter : public TheoryRewriter
{
  static Node blastDistinct(TNode node);

 public:

  RewriteResponse postRewrite(TNode node) override;

  RewriteResponse preRewrite(TNode node) override { return doRewrite(node); }

 public:
  /**
   * The default rewriter for rewrites that occur at both pre and post rewrite.
   */
  static RewriteResponse doRewrite(TNode node);
  /**
   * Main entry point for rewriting terms of the form (witness ((x T)) (P x)).
   * Returns the rewritten form of node.
   */
  static Node rewriteWitness(TNode node);
}; /* class TheoryBuiltinRewriter */

}  // namespace builtin
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, Mathias Preiner
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		* [[ Add one-line brief description here ]]
14		*
15		* [[ Add lengthier description here ]]
16		* \todo document this file
17		*/
18
19		#include "cvc5_private.h"
20
21		#ifndef CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
22		#define CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H
23
24		#include "theory/theory_rewriter.h"
25
26		namespace cvc5 {
27		namespace theory {
28		namespace builtin {
29
30	30541	class TheoryBuiltinRewriter : public TheoryRewriter
31		{
32		static Node blastDistinct(TNode node);
33
34		public:
35
36		RewriteResponse postRewrite(TNode node) override;
37
38	296145	RewriteResponse preRewrite(TNode node) override { return doRewrite(node); }
39
40		public:
41		/**
42		* The default rewriter for rewrites that occur at both pre and post rewrite.
43		*/
44		static RewriteResponse doRewrite(TNode node);
45		/**
46		* Main entry point for rewriting terms of the form (witness ((x T)) (P x)).
47		* Returns the rewritten form of node.
48		*/
49		static Node rewriteWitness(TNode node);
50		}; /* class TheoryBuiltinRewriter */
51
52		} // namespace builtin
53		} // namespace theory
54		} // namespace cvc5
55
56		#endif /* CVC5__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */