Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/rewriter.h	Lines:	1	1	100.0 %
Date:	2021-11-05	Branches:	0	0	0.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 Env;
class TConvProofGenerator;
class ProofNodeManager;
class TrustNode;

namespace theory {

class Evaluator;

/**
 * The main rewriter class.
 */
class Rewriter {
  friend class cvc5::Env;  // to set the resource manager
 public:
  Rewriter();

  /**
   * !!! Temporary until static access to rewriter is eliminated.
   *
   * Rewrites the node using theoryOf() to determine which rewriter to
   * use on the node.
   */
  static Node rewrite(TNode node);
  /**
   * !!! Temporary until static access to rewriter is eliminated.
   */
  static Node callExtendedRewrite(TNode node, bool aggr = true);

  /**
   * 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.
   */
  Node rewriteEqualityExt(TNode node);

  /**
   * !!! Temporary until static access to rewriter is eliminated. This method
   * should be moved to same place as evaluate (currently in Env).
   *
   * Extended rewrite of the given node. This method is implemented by a
   * custom ExtendRewriter class that wraps this class to perform custom
   * rewrites (usually those that are not useful for solving, but e.g. useful
   * for SyGuS symmetry breaking).
   * @param node The node to rewrite
   * @param aggr Whether to perform aggressive rewrites.
   */
  Node extendedRewrite(TNode node, bool aggr = true);

  /**
   * 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. */
  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.
   */
  void registerTheoryRewriter(theory::TheoryId tid, TheoryRewriter* trew);

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

 private:
  /**
   * Get the rewriter associated with the SolverEngine in scope.
   *
   * TODO(#3468): Get rid of this function (it relies on there being an
   * singleton with the current SolverEngine 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();

  /**
   * Has n been rewritten with proofs? This checks if n is in d_tpgNodes.
   */
  bool hasRewrittenWithProofs(TNode n) const;

  /** The resource manager, for tracking resource usage */
  ResourceManager* d_resourceManager;

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

  /** The proof generator */
  std::unique_ptr<TConvProofGenerator> d_tpg;
  /**
   * Nodes rewritten with proofs. Since d_tpg contains a reference to all
   * nodes that have been rewritten with proofs, we can keep only a TNode
   * here.
   */
  std::unordered_set<TNode> d_tpgNodes;
#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 Env;
26		class TConvProofGenerator;
27		class ProofNodeManager;
28		class TrustNode;
29
30		namespace theory {
31
32		class Evaluator;
33
34		/**
35		* The main rewriter class.
36		*/
37	15904	class Rewriter {
38		friend class cvc5::Env; // to set the resource manager
39		public:
40		Rewriter();
41
42		/**
43		* !!! Temporary until static access to rewriter is eliminated.
44		*
45		* Rewrites the node using theoryOf() to determine which rewriter to
46		* use on the node.
47		*/
48		static Node rewrite(TNode node);
49		/**
50		* !!! Temporary until static access to rewriter is eliminated.
51		*/
52		static Node callExtendedRewrite(TNode node, bool aggr = true);
53
54		/**
55		* Rewrites the equality node using theoryOf() to determine which rewriter to
56		* use on the node corresponding to an equality s = t.
57		*
58		* Specifically, this method performs rewrites whose conclusion is not
59		* necessarily one of { s = t, t = s, true, false }, which is an invariant
60		* guaranted by the above method. This invariant is motivated by theory
61		* combination, which needs to guarantee that equalities between terms
62		* can be communicated for all pairs of terms.
63		*/
64		Node rewriteEqualityExt(TNode node);
65
66		/**
67		* !!! Temporary until static access to rewriter is eliminated. This method
68		* should be moved to same place as evaluate (currently in Env).
69		*
70		* Extended rewrite of the given node. This method is implemented by a
71		* custom ExtendRewriter class that wraps this class to perform custom
72		* rewrites (usually those that are not useful for solving, but e.g. useful
73		* for SyGuS symmetry breaking).
74		* @param node The node to rewrite
75		* @param aggr Whether to perform aggressive rewrites.
76		*/
77		Node extendedRewrite(TNode node, bool aggr = true);
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		/** Garbage collects the rewrite caches. */
97		void clearCaches();
98
99		/**
100		* Registers a theory rewriter with this rewriter. The rewriter does not own
101		* the theory rewriters.
102		*
103		* @param tid The theory that the theory rewriter should be associated with.
104		* @param trew The theory rewriter to register.
105		*/
106		void registerTheoryRewriter(theory::TheoryId tid, TheoryRewriter* trew);
107
108		/** Get the theory rewriter for the given id */
109		TheoryRewriter* getTheoryRewriter(theory::TheoryId theoryId);
110
111		private:
112		/**
113		* Get the rewriter associated with the SolverEngine in scope.
114		*
115		* TODO(#3468): Get rid of this function (it relies on there being an
116		* singleton with the current SolverEngine in scope)
117		*/
118		static Rewriter* getInstance();
119
120		/** Returns the appropriate cache for a node */
121		Node getPreRewriteCache(theory::TheoryId theoryId, TNode node);
122
123		/** Returns the appropriate cache for a node */
124		Node getPostRewriteCache(theory::TheoryId theoryId, TNode node);
125
126		/** Sets the appropriate cache for a node */
127		void setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
128
129		/** Sets the appropriate cache for a node */
130		void setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache);
131
132		/**
133		* Rewrites the node using the given theory rewriter.
134		*/
135		Node rewriteTo(theory::TheoryId theoryId,
136		Node node,
137		TConvProofGenerator* tcpg = nullptr);
138
139		/** Calls the pre-rewriter for the given theory */
140		RewriteResponse preRewrite(theory::TheoryId theoryId,
141		TNode n,
142		TConvProofGenerator* tcpg = nullptr);
143
144		/** Calls the post-rewriter for the given theory */
145		RewriteResponse postRewrite(theory::TheoryId theoryId,
146		TNode n,
147		TConvProofGenerator* tcpg = nullptr);
148		/** processes a trust rewrite response */
149		RewriteResponse processTrustRewriteResponse(
150		theory::TheoryId theoryId,
151		const TrustRewriteResponse& tresponse,
152		bool isPre,
153		TConvProofGenerator* tcpg);
154
155		/**
156		* Calls the equality-rewriter for the given theory.
157		*/
158		Node callRewriteEquality(theory::TheoryId theoryId, TNode equality);
159
160		void clearCachesInternal();
161
162		/**
163		* Has n been rewritten with proofs? This checks if n is in d_tpgNodes.
164		*/
165		bool hasRewrittenWithProofs(TNode n) const;
166
167		/** The resource manager, for tracking resource usage */
168		ResourceManager* d_resourceManager;
169
170		/** Theory rewriters used by this rewriter instance */
171		TheoryRewriter* d_theoryRewriters[theory::THEORY_LAST];
172
173		/** The proof generator */
174		std::unique_ptr<TConvProofGenerator> d_tpg;
175		/**
176		* Nodes rewritten with proofs. Since d_tpg contains a reference to all
177		* nodes that have been rewritten with proofs, we can keep only a TNode
178		* here.
179		*/
180		std::unordered_set<TNode> d_tpgNodes;
181		#ifdef CVC5_ASSERTIONS
182		std::unique_ptr<std::unordered_set<Node>> d_rewriteStack = nullptr;
183		#endif /* CVC5_ASSERTIONS */
184		};/* class Rewriter */
185
186		} // namespace theory
187		} // namespace cvc5