Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/rewriter.h	Lines:	1	1	100.0 %
Date:	2021-08-16	Branches:	12	16	75.0 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andres Noetzli, Andrew Reynolds, Dejan Jovanovic
 *
 * 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 Rewriter class.
 */

#include "cvc5_private.h"

#pragma once

#include "expr/node.h"
#include "theory/theory_rewriter.h"

namespace cvc5 {

class TConvProofGenerator;
class ProofNodeManager;
class TrustNode;

namespace theory {

namespace builtin {
class BuiltinProofRuleChecker;
}

/**
 * The rewrite environment holds everything that the individual rewrites have
 * access to.
 */
class RewriteEnvironment
{
};

/**
 * The identity rewrite just returns the original node.
 *
 * @param re The rewrite environment
 * @param n The node to rewrite
 * @return The original node
 */
RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);

/**
 * The main rewriter class.
 */
class Rewriter {
  friend builtin::BuiltinProofRuleChecker;

 public:
  Rewriter();

  /**
   * Rewrites the node using theoryOf() to determine which rewriter to
   * use on the node.
   */
  static Node rewrite(TNode node);

  /**
   * Rewrites the equality node using theoryOf() to determine which rewriter to
   * use on the node corresponding to an equality s = t.
   *
   * Specifically, this method performs rewrites whose conclusion is not
   * necessarily one of { s = t, t = s, true, false }, which is an invariant
   * guaranted by the above method. This invariant is motivated by theory
   * combination, which needs to guarantee that equalities between terms
   * can be communicated for all pairs of terms.
   */
  static Node rewriteEqualityExt(TNode node);

  /**
   * Rewrite with proof production, which is managed by the term conversion
   * proof generator managed by this class (d_tpg). This method requires a call
   * to setProofNodeManager prior to this call.
   *
   * @param node The node to rewrite.
   * @param isExtEq Whether node is an equality which we are applying
   * rewriteEqualityExt on.
   * @return The trust node of kind TrustNodeKind::REWRITE that contains the
   * rewritten form of node.
   */
  TrustNode rewriteWithProof(TNode node,
                             bool isExtEq = false);

  /** Set proof node manager */
  void setProofNodeManager(ProofNodeManager* pnm);

  /**
   * Garbage collects the rewrite caches.
   */
  static void clearCaches();

  /**
   * Registers a theory rewriter with this rewriter. The rewriter does not own
   * the theory rewriters.
   *
   * @param tid The theory that the theory rewriter should be associated with.
   * @param trew The theory rewriter to register.
   */
  static void registerTheoryRewriter(theory::TheoryId tid,
                                     TheoryRewriter* trew);

  /**
   * Register a prerewrite for a given kind.
   *
   * @param k The kind to register a rewrite for.
   * @param fn The function that performs the rewrite.
   */
  void registerPreRewrite(
      Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);

  /**
   * Register a postrewrite for a given kind.
   *
   * @param k The kind to register a rewrite for.
   * @param fn The function that performs the rewrite.
   */
  void registerPostRewrite(
      Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);

  /**
   * Register a prerewrite for equalities belonging to a given theory.
   *
   * @param tid The theory to register a rewrite for.
   * @param fn The function that performs the rewrite.
   */
  void registerPreRewriteEqual(
      theory::TheoryId tid,
      std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);

  /**
   * Register a postrewrite for equalities belonging to a given theory.
   *
   * @param tid The theory to register a rewrite for.
   * @param fn The function that performs the rewrite.
   */
  void registerPostRewriteEqual(
      theory::TheoryId tid,
      std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);

  /** Get the theory rewriter for the given id */
  TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);

 private:
  /**
   * Get the rewriter associated with the SmtEngine in scope.
   *
   * TODO(#3468): Get rid of this function (it relies on there being an
   * singleton with the current SmtEngine in scope)
   */
  static Rewriter* getInstance();

  /** Returns the appropriate cache for a node */
  Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);

  /** Returns the appropriate cache for a node */
  Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);

  /** Sets the appropriate cache for a node */
  void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);

  /** Sets the appropriate cache for a node */
  void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);

  /**
   * Rewrites the node using the given theory rewriter.
   */
  Node rewriteTo(theory::TheoryId theoryId,
                 Node node,
                 TConvProofGenerator* tcpg = nullptr);

  /** Calls the pre-rewriter for the given theory */
  RewriteResponse preRewrite(theory::TheoryId theoryId,
                             TNode n,
                             TConvProofGenerator* tcpg = nullptr);

  /** Calls the post-rewriter for the given theory */
  RewriteResponse postRewrite(theory::TheoryId theoryId,
                              TNode n,
                              TConvProofGenerator* tcpg = nullptr);
  /** processes a trust rewrite response */
  RewriteResponse processTrustRewriteResponse(
      theory::TheoryId theoryId,
      const TrustRewriteResponse& tresponse,
      bool isPre,
      TConvProofGenerator* tcpg);

  /**
   * Calls the equality-rewriter for the given theory.
   */
  Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);

  void clearCachesInternal();

  /** Theory rewriters used by this rewriter instance */
  TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];

  /** Rewriter table for prewrites. Maps kinds to rewriter function. */
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
      d_preRewriters[kind::LAST_KIND];
  /** Rewriter table for postrewrites. Maps kinds to rewriter function. */
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
      d_postRewriters[kind::LAST_KIND];
  /**
   * Rewriter table for prerewrites of equalities. Maps theory to rewriter
   * function.
   */
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
      d_preRewritersEqual[theory::THEORY_LAST];
  /**
   * Rewriter table for postrewrites of equalities. Maps theory to rewriter
   * function.
   */
  std::function<RewriteResponse(RewriteEnvironment*, TNode)>
      d_postRewritersEqual[theory::THEORY_LAST];

  RewriteEnvironment d_re;

  /** The proof generator */
  std::unique_ptr<TConvProofGenerator> d_tpg;
#ifdef CVC5_ASSERTIONS
  std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
#endif /* CVC5_ASSERTIONS */
};/* class Rewriter */

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andres Noetzli, Andrew Reynolds, Dejan Jovanovic
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 Rewriter class.
14		*/
15
16		#include "cvc5_private.h"
17
18		#pragma once
19
20		#include "expr/node.h"
21		#include "theory/theory_rewriter.h"
22
23		namespace cvc5 {
24
25		class TConvProofGenerator;
26		class ProofNodeManager;
27		class TrustNode;
28
29		namespace theory {
30
31		namespace builtin {
32		class BuiltinProofRuleChecker;
33		}
34
35		/**
36		* The rewrite environment holds everything that the individual rewrites have
37		* access to.
38		*/
39		class RewriteEnvironment
40		{
41		};
42
43		/**
44		* The identity rewrite just returns the original node.
45		*
46		* @param re The rewrite environment
47		* @param n The node to rewrite
48		* @return The original node
49		*/
50		RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n);
51
52		/**
53		* The main rewriter class.
54		*/
55	10497	class Rewriter {
56		friend builtin::BuiltinProofRuleChecker;
57
58		public:
59		Rewriter();
60
61		/**
62		* Rewrites the node using theoryOf() to determine which rewriter to
63		* use on the node.
64		*/
65		static Node rewrite(TNode node);
66
67		/**
68		* Rewrites the equality node using theoryOf() to determine which rewriter to
69		* use on the node corresponding to an equality s = t.
70		*
71		* Specifically, this method performs rewrites whose conclusion is not
72		* necessarily one of { s = t, t = s, true, false }, which is an invariant
73		* guaranted by the above method. This invariant is motivated by theory
74		* combination, which needs to guarantee that equalities between terms
75		* can be communicated for all pairs of terms.
76		*/
77		static Node rewriteEqualityExt(TNode node);
78
79		/**
80		* Rewrite with proof production, which is managed by the term conversion
81		* proof generator managed by this class (d_tpg). This method requires a call
82		* to setProofNodeManager prior to this call.
83		*
84		* @param node The node to rewrite.
85		* @param isExtEq Whether node is an equality which we are applying
86		* rewriteEqualityExt on.
87		* @return The trust node of kind TrustNodeKind::REWRITE that contains the
88		* rewritten form of node.
89		*/
90		TrustNode rewriteWithProof(TNode node,
91		bool isExtEq = false);
92
93		/** Set proof node manager */
94		void setProofNodeManager(ProofNodeManager* pnm);
95
96		/**
97		* Garbage collects the rewrite caches.
98		*/
99		static void clearCaches();
100
101		/**
102		* Registers a theory rewriter with this rewriter. The rewriter does not own
103		* the theory rewriters.
104		*
105		* @param tid The theory that the theory rewriter should be associated with.
106		* @param trew The theory rewriter to register.
107		*/
108		static void registerTheoryRewriter(theory::TheoryId tid,
109		TheoryRewriter* trew);
110
111		/**
112		* Register a prerewrite for a given kind.
113		*
114		* @param k The kind to register a rewrite for.
115		* @param fn The function that performs the rewrite.
116		*/
117		void registerPreRewrite(
118		Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
119
120		/**
121		* Register a postrewrite for a given kind.
122		*
123		* @param k The kind to register a rewrite for.
124		* @param fn The function that performs the rewrite.
125		*/
126		void registerPostRewrite(
127		Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
128
129		/**
130		* Register a prerewrite for equalities belonging to a given theory.
131		*
132		* @param tid The theory to register a rewrite for.
133		* @param fn The function that performs the rewrite.
134		*/
135		void registerPreRewriteEqual(
136		theory::TheoryId tid,
137		std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
138
139		/**
140		* Register a postrewrite for equalities belonging to a given theory.
141		*
142		* @param tid The theory to register a rewrite for.
143		* @param fn The function that performs the rewrite.
144		*/
145		void registerPostRewriteEqual(
146		theory::TheoryId tid,
147		std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn);
148
149		/** Get the theory rewriter for the given id */
150		TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);
151
152		private:
153		/**
154		* Get the rewriter associated with the SmtEngine in scope.
155		*
156		* TODO(#3468): Get rid of this function (it relies on there being an
157		* singleton with the current SmtEngine in scope)
158		*/
159		static Rewriter* getInstance();
160
161		/** Returns the appropriate cache for a node */
162		Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
163
164		/** Returns the appropriate cache for a node */
165		Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
166
167		/** Sets the appropriate cache for a node */
168		void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
169
170		/** Sets the appropriate cache for a node */
171		void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
172
173		/**
174		* Rewrites the node using the given theory rewriter.
175		*/
176		Node rewriteTo(theory::TheoryId theoryId,
177		Node node,
178		TConvProofGenerator* tcpg = nullptr);
179
180		/** Calls the pre-rewriter for the given theory */
181		RewriteResponse preRewrite(theory::TheoryId theoryId,
182		TNode n,
183		TConvProofGenerator* tcpg = nullptr);
184
185		/** Calls the post-rewriter for the given theory */
186		RewriteResponse postRewrite(theory::TheoryId theoryId,
187		TNode n,
188		TConvProofGenerator* tcpg = nullptr);
189		/** processes a trust rewrite response */
190		RewriteResponse processTrustRewriteResponse(
191		theory::TheoryId theoryId,
192		const TrustRewriteResponse& tresponse,
193		bool isPre,
194		TConvProofGenerator* tcpg);
195
196		/**
197		* Calls the equality-rewriter for the given theory.
198		*/
199		Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
200
201		void clearCachesInternal();
202
203		/** Theory rewriters used by this rewriter instance */
204		TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
205
206		/** Rewriter table for prewrites. Maps kinds to rewriter function. */
207		std::function<RewriteResponse(RewriteEnvironment*, TNode)>
208		d_preRewriters[kind::LAST_KIND];
209		/** Rewriter table for postrewrites. Maps kinds to rewriter function. */
210		std::function<RewriteResponse(RewriteEnvironment*, TNode)>
211		d_postRewriters[kind::LAST_KIND];
212		/**
213		* Rewriter table for prerewrites of equalities. Maps theory to rewriter
214		* function.
215		*/
216		std::function<RewriteResponse(RewriteEnvironment*, TNode)>
217		d_preRewritersEqual[theory::THEORY_LAST];
218		/**
219		* Rewriter table for postrewrites of equalities. Maps theory to rewriter
220		* function.
221		*/
222		std::function<RewriteResponse(RewriteEnvironment*, TNode)>
223		d_postRewritersEqual[theory::THEORY_LAST];
224
225		RewriteEnvironment d_re;
226
227		/** The proof generator */
228		std::unique_ptr<TConvProofGenerator> d_tpg;
229		#ifdef CVC5_ASSERTIONS
230		std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
231		#endif /* CVC5_ASSERTIONS */
232		};/* class Rewriter */
233
234		} // namespace theory
235		} // namespace cvc5