Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_rewriter.h	Lines:	5	6	83.3 %
Date:	2021-09-12	Branches:	0	0	0.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli, Andrew Reynolds, Morgan Deters
 *
 * 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.
 * ****************************************************************************
 *
 * The TheoryRewriter class.
 *
 * The interface that theory rewriters implement.
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__THEORY_REWRITER_H
#define CVC5__THEORY__THEORY_REWRITER_H

#include "expr/node.h"
#include "proof/trust_node.h"

namespace cvc5 {
namespace theory {

class Rewriter;

/**
 * Theory rewriters signal whether more rewriting is needed (or not)
 * by using a member of this enumeration.  See RewriteResponse, below.
 */
enum RewriteStatus
{
  /** The node is fully rewritten (no more rewrites apply) */
  REWRITE_DONE,
  /** The node may be rewritten further */
  REWRITE_AGAIN,
  /** Subnodes of the node may be rewritten further */
  REWRITE_AGAIN_FULL
}; /* enum RewriteStatus */

/**
 * Instances of this class serve as response codes from
 * TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
 * consists of the rewritten node as well as a status that indicates whether
 * more rewriting is needed or not.
 */
struct RewriteResponse
{
  const RewriteStatus d_status;
  const Node d_node;
  RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
}; /* struct RewriteResponse */

/** Same as above, with trust node instead of node. */
struct TrustRewriteResponse
{
  TrustRewriteResponse(RewriteStatus status,
                       Node n,
                       Node nr,
                       ProofGenerator* pg);
  /** The status of the rewrite */
  const RewriteStatus d_status;
  /**
   * The trust node corresponding to the rewrite.
   */
  TrustNode d_node;
};

/**
 * The interface that a theory rewriter has to implement.
 *
 * Note: A theory rewriter is expected to handle all kinds of a theory, even
 * the ones that are removed by `Theory::expandDefinition()` since it may be
 * called on terms before the definitions have been expanded.
 */
class TheoryRewriter
{
 public:
  virtual ~TheoryRewriter() = default;

  /**
   * Registers the rewrites of a given theory with the rewriter.
   *
   * @param rewriter The rewriter to register the rewrites with.
   */
  virtual void registerRewrites(Rewriter* rewriter) {}

  /**
   * Performs a pre-rewrite step.
   *
   * @param node The node to rewrite
   */
  virtual RewriteResponse postRewrite(TNode node) = 0;

  /**
   * Performs a pre-rewrite step, with proofs.
   *
   * @param node The node to rewrite
   */
  virtual TrustRewriteResponse postRewriteWithProof(TNode node);

  /**
   * Performs a post-rewrite step.
   *
   * @param node The node to rewrite
   */
  virtual RewriteResponse preRewrite(TNode node) = 0;

  /**
   * Performs a pre-rewrite step, with proofs.
   *
   * @param node The node to rewrite
   */
  virtual TrustRewriteResponse preRewriteWithProof(TNode node);

  /** rewrite equality extended
   *
   * This method returns a formula that is equivalent to the equality between
   * two terms s = t, given by node.
   *
   * Specifically, this method performs rewrites whose conclusion is not
   * necessarily one of { s = t, t = s, true, false }. This is in constrast
   * to postRewrite and preRewrite above, where the rewritten form of an
   * equality must be one of these.
   *
   * @param node The node to rewrite
   */
  virtual Node rewriteEqualityExt(Node node);

  /** rewrite equality extended, with proofs
   *
   * @param node The node to rewrite
   * @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
   * node if no rewrites are applied.
   */
  virtual TrustNode rewriteEqualityExtWithProof(Node node);

  /**
   * Expand definitions in the term node. This returns a term that is
   * equivalent to node. It wraps this term in a TrustNode of kind
   * TrustNodeKind::REWRITE. If node is unchanged by this method, the
   * null TrustNode may be returned. This is an optimization to avoid
   * constructing the trivial equality (= node node) internally within
   * TrustNode.
   *
   * The purpose of this method is typically to eliminate the operators in node
   * that are syntax sugar that cannot otherwise be eliminated during rewriting.
   * For example, division relies on the introduction of an uninterpreted
   * function for the divide-by-zero case, which we do not introduce with
   * the standard rewrite methods.
   *
   * Some theories have kinds that are effectively definitions and should be
   * expanded before they are handled.  Definitions allow a much wider range of
   * actions than the normal forms given by the rewriter. However no
   * assumptions can be made about subterms having been expanded or rewritten.
   * Where possible rewrite rules should be used, definitions should only be
   * used when rewrites are not possible, for example in handling
   * under-specified operations using partially defined functions.
   */
  virtual TrustNode expandDefinition(Node node);
};

}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__THEORY_REWRITER_H */


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andres Noetzli, Andrew Reynolds, Morgan Deters
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		* The TheoryRewriter class.
14		*
15		* The interface that theory rewriters implement.
16		*/
17
18		#include "cvc5_private.h"
19
20		#ifndef CVC5__THEORY__THEORY_REWRITER_H
21		#define CVC5__THEORY__THEORY_REWRITER_H
22
23		#include "expr/node.h"
24		#include "proof/trust_node.h"
25
26		namespace cvc5 {
27		namespace theory {
28
29		class Rewriter;
30
31		/**
32		* Theory rewriters signal whether more rewriting is needed (or not)
33		* by using a member of this enumeration. See RewriteResponse, below.
34		*/
35		enum RewriteStatus
36		{
37		/** The node is fully rewritten (no more rewrites apply) */
38		REWRITE_DONE,
39		/** The node may be rewritten further */
40		REWRITE_AGAIN,
41		/** Subnodes of the node may be rewritten further */
42		REWRITE_AGAIN_FULL
43		}; /* enum RewriteStatus */
44
45		/**
46		* Instances of this class serve as response codes from
47		* TheoryRewriter::preRewrite() and TheoryRewriter::postRewrite(). The response
48		* consists of the rewritten node as well as a status that indicates whether
49		* more rewriting is needed or not.
50		*/
51	47438455	struct RewriteResponse
52		{
53		const RewriteStatus d_status;
54		const Node d_node;
55	36074949	RewriteResponse(RewriteStatus status, Node n) : d_status(status), d_node(n) {}
56		}; /* struct RewriteResponse */
57
58		/** Same as above, with trust node instead of node. */
59	799779	struct TrustRewriteResponse
60		{
61		TrustRewriteResponse(RewriteStatus status,
62		Node n,
63		Node nr,
64		ProofGenerator* pg);
65		/** The status of the rewrite */
66		const RewriteStatus d_status;
67		/**
68		* The trust node corresponding to the rewrite.
69		*/
70		TrustNode d_node;
71		};
72
73		/**
74		* The interface that a theory rewriter has to implement.
75		*
76		* Note: A theory rewriter is expected to handle all kinds of a theory, even
77		* the ones that are removed by `Theory::expandDefinition()` since it may be
78		* called on terms before the definitions have been expanded.
79		*/
80	129323	class TheoryRewriter
81		{
82		public:
83	129284	virtual ~TheoryRewriter() = default;
84
85		/**
86		* Registers the rewrites of a given theory with the rewriter.
87		*
88		* @param rewriter The rewriter to register the rewrites with.
89		*/
90		virtual void registerRewrites(Rewriter* rewriter) {}
91
92		/**
93		* Performs a pre-rewrite step.
94		*
95		* @param node The node to rewrite
96		*/
97		virtual RewriteResponse postRewrite(TNode node) = 0;
98
99		/**
100		* Performs a pre-rewrite step, with proofs.
101		*
102		* @param node The node to rewrite
103		*/
104		virtual TrustRewriteResponse postRewriteWithProof(TNode node);
105
106		/**
107		* Performs a post-rewrite step.
108		*
109		* @param node The node to rewrite
110		*/
111		virtual RewriteResponse preRewrite(TNode node) = 0;
112
113		/**
114		* Performs a pre-rewrite step, with proofs.
115		*
116		* @param node The node to rewrite
117		*/
118		virtual TrustRewriteResponse preRewriteWithProof(TNode node);
119
120		/** rewrite equality extended
121		*
122		* This method returns a formula that is equivalent to the equality between
123		* two terms s = t, given by node.
124		*
125		* Specifically, this method performs rewrites whose conclusion is not
126		* necessarily one of { s = t, t = s, true, false }. This is in constrast
127		* to postRewrite and preRewrite above, where the rewritten form of an
128		* equality must be one of these.
129		*
130		* @param node The node to rewrite
131		*/
132		virtual Node rewriteEqualityExt(Node node);
133
134		/** rewrite equality extended, with proofs
135		*
136		* @param node The node to rewrite
137		* @return A trust node of kind TrustNodeKind::REWRITE, or the null trust
138		* node if no rewrites are applied.
139		*/
140		virtual TrustNode rewriteEqualityExtWithProof(Node node);
141
142		/**
143		* Expand definitions in the term node. This returns a term that is
144		* equivalent to node. It wraps this term in a TrustNode of kind
145		* TrustNodeKind::REWRITE. If node is unchanged by this method, the
146		* null TrustNode may be returned. This is an optimization to avoid
147		* constructing the trivial equality (= node node) internally within
148		* TrustNode.
149		*
150		* The purpose of this method is typically to eliminate the operators in node
151		* that are syntax sugar that cannot otherwise be eliminated during rewriting.
152		* For example, division relies on the introduction of an uninterpreted
153		* function for the divide-by-zero case, which we do not introduce with
154		* the standard rewrite methods.
155		*
156		* Some theories have kinds that are effectively definitions and should be
157		* expanded before they are handled. Definitions allow a much wider range of
158		* actions than the normal forms given by the rewriter. However no
159		* assumptions can be made about subterms having been expanded or rewritten.
160		* Where possible rewrite rules should be used, definitions should only be
161		* used when rewrites are not possible, for example in handling
162		* under-specified operations using partially defined functions.
163		*/
164		virtual TrustNode expandDefinition(Node node);
165		};
166
167		} // namespace theory
168		} // namespace cvc5
169
170		#endif /* CVC5__THEORY__THEORY_REWRITER_H */