Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/rewriter.cpp	Lines:	156	173	90.2 %
Date:	2021-11-06	Branches:	302	722	41.8 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Andres Noetzli, 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 "theory/rewriter.h"

#include "options/theory_options.h"
#include "proof/conv_proof_generator.h"
#include "smt/smt_statistics_registry.h"
#include "smt/solver_engine.h"
#include "smt/solver_engine_scope.h"
#include "theory/builtin/proof_checker.h"
#include "theory/evaluator.h"
#include "theory/quantifiers/extended_rewrite.h"
#include "theory/rewriter_tables.h"
#include "theory/theory.h"
#include "util/resource_manager.h"

using namespace std;

namespace cvc5 {
namespace theory {

// Note that this function is a simplified version of Theory::theoryOf for
// (type-based) theoryOfMode. We expand and simplify it here for the sake of
// efficiency.
static TheoryId theoryOf(TNode node) {
  if (node.getKind() == kind::EQUAL)
  {
    // Equality is owned by the theory that owns the domain
    return Theory::theoryOf(node[0].getType());
  }
  // Regular nodes are owned by the kind
  return kindToTheoryId(node.getKind());
}

/**
 * TheoryEngine::rewrite() keeps a stack of things that are being pre-
 * and post-rewritten.  Each element of the stack is a
 * RewriteStackElement.
 */
struct RewriteStackElement {
  /**
   * Construct a fresh stack element.
   */
  RewriteStackElement(TNode node, TheoryId theoryId)
      : d_node(node),
        d_original(node),
        d_theoryId(theoryId),
        d_originalTheoryId(theoryId),
        d_nextChild(0)
  {
  }

  TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); }

  TheoryId getOriginalTheoryId()
  {
    return static_cast<TheoryId>(d_originalTheoryId);
  }

  /** The node we're currently rewriting */
  Node d_node;
  /** Original node (either the unrewritten node or the node after prerewriting)
   */
  Node d_original;
  /** Id of the theory that's currently rewriting this node */
  unsigned d_theoryId : 8;
  /** Id of the original theory that started the rewrite */
  unsigned d_originalTheoryId : 8;
  /** Index of the child this node is done rewriting */
  unsigned d_nextChild : 32;
  /** Builder for this node */
  NodeBuilder d_builder;
};


Node Rewriter::rewrite(TNode node) {
  if (node.getNumChildren() == 0)
  {
    // Nodes with zero children should never change via rewriting. We return
    // eagerly for the sake of efficiency here.
    return node;
  }
  return getInstance()->rewriteTo(theoryOf(node), node);
}

Node Rewriter::callExtendedRewrite(TNode node, bool aggr)
{
  return getInstance()->extendedRewrite(node, aggr);
}

Node Rewriter::extendedRewrite(TNode node, bool aggr)
{
  quantifiers::ExtendedRewriter er(*this, aggr);
  return er.extendedRewrite(node);
}

TrustNode Rewriter::rewriteWithProof(TNode node,
                                     bool isExtEq)
{
  // must set the proof checker before calling this
  Assert(d_tpg != nullptr);
  if (isExtEq)
  {
    // theory rewriter is responsible for rewriting the equality
    TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)];
    Assert(tr != nullptr);
    return tr->rewriteEqualityExtWithProof(node);
  }
  Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get());
  return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
}

void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
{
  // if not already initialized with proof support
  if (d_tpg == nullptr)
  {
    Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl;
    // the rewriter is staticly determinstic, thus use static cache policy
    // for the term conversion proof generator
    d_tpg.reset(new TConvProofGenerator(pnm,
                                        nullptr,
                                        TConvPolicy::FIXPOINT,
                                        TConvCachePolicy::STATIC,
                                        "Rewriter::TConvProofGenerator"));
  }
}

Node Rewriter::rewriteEqualityExt(TNode node)
{
  Assert(node.getKind() == kind::EQUAL);
  // note we don't force caching of this method currently
  return d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(node);
}

void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
                                      TheoryRewriter* trew)
{
  d_theoryRewriters[tid] = trew;
}

TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
{
  return d_theoryRewriters[theoryId];
}

Rewriter* Rewriter::getInstance()
{
  return smt::currentSolverEngine()->getRewriter();
}

Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                         Node node,
                         TConvProofGenerator* tcpg)
{
#ifdef CVC5_ASSERTIONS
  bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());

  if (d_rewriteStack == nullptr)
  {
    d_rewriteStack.reset(new std::unordered_set<Node>());
  }
#endif

  Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;

  // Check if it's been cached already
  Node cached = getPostRewriteCache(theoryId, node);
  if (!cached.isNull() && (tcpg == nullptr || hasRewrittenWithProofs(node)))
  {
    return cached;
  }

  // Put the node on the stack in order to start the "recursive" rewrite
  vector<RewriteStackElement> rewriteStack;
  rewriteStack.push_back(RewriteStackElement(node, theoryId));

  // Rewrite until the stack is empty
  for (;;){
    if (d_resourceManager != nullptr)
    {
      d_resourceManager->spendResource(Resource::RewriteStep);
    }

    // Get the top of the recursion stack
    RewriteStackElement& rewriteStackTop = rewriteStack.back();

    Trace("rewriter") << "Rewriter::rewriting: "
                      << rewriteStackTop.getTheoryId() << ","
                      << rewriteStackTop.d_node << std::endl;

    // Before rewriting children we need to do a pre-rewrite of the node
    if (rewriteStackTop.d_nextChild == 0)
    {
      // Check if the pre-rewrite has already been done (it's in the cache)
      cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
                                  rewriteStackTop.d_node);
      if (cached.isNull()
          || (tcpg != nullptr
              && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
      {
        // Rewrite until fix-point is reached
        for(;;) {
          // Perform the pre-rewrite
          RewriteResponse response = preRewrite(
              rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);

          // Put the rewritten node to the top of the stack
          rewriteStackTop.d_node = response.d_node;
          TheoryId newTheory = theoryOf(rewriteStackTop.d_node);
          // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
          if (newTheory == rewriteStackTop.getTheoryId()
              && response.d_status == REWRITE_DONE)
          {
            break;
          }
          rewriteStackTop.d_theoryId = newTheory;
        }

        // Cache the rewrite
        setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
                           rewriteStackTop.d_original,
                           rewriteStackTop.d_node);
      }
      // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
      else {
        // Continue with the cached version
        rewriteStackTop.d_node = cached;
        rewriteStackTop.d_theoryId = theoryOf(cached);
      }
    }

    rewriteStackTop.d_original = rewriteStackTop.d_node;
    // Now it's time to rewrite the children, check if this has already been done
    cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
                                 rewriteStackTop.d_node);
    // If not, go through the children
    if (cached.isNull()
        || (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
    {
      // The child we need to rewrite
      unsigned child = rewriteStackTop.d_nextChild++;

      // To build the rewritten expression we set up the builder
      if(child == 0) {
        if (rewriteStackTop.d_node.getNumChildren() > 0)
        {
          // The children will add themselves to the builder once they're done
          rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind();
          kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind();
          if (metaKind == kind::metakind::PARAMETERIZED) {
            rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator();
          }
        }
      }

      // Process the next child
      if (child < rewriteStackTop.d_node.getNumChildren())
      {
        // The child node
        Node childNode = rewriteStackTop.d_node[child];
        // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
        rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
        // Go on with the rewriting
        continue;
      }

      // Incorporate the children if necessary
      if (rewriteStackTop.d_node.getNumChildren() > 0)
      {
        Node rewritten = rewriteStackTop.d_builder;
        rewriteStackTop.d_node = rewritten;
        rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
      }

      // Done with all pre-rewriting, so let's do the post rewrite
      for(;;) {
        // Do the post-rewrite
        RewriteResponse response = postRewrite(
            rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);

        // We continue with the response we got
        TheoryId newTheoryId = theoryOf(response.d_node);
        if (newTheoryId != rewriteStackTop.getTheoryId()
            || response.d_status == REWRITE_AGAIN_FULL)
        {
          // In the post rewrite if we've changed theories, we must do a full rewrite
          Assert(response.d_node != rewriteStackTop.d_node);
          //TODO: this is not thread-safe - should make this assertion dependent on sequential build
#ifdef CVC5_ASSERTIONS
          Assert(d_rewriteStack->find(response.d_node)
                 == d_rewriteStack->end());
          d_rewriteStack->insert(response.d_node);
#endif
          Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
          rewriteStackTop.d_node = rewritten;
#ifdef CVC5_ASSERTIONS
          d_rewriteStack->erase(response.d_node);
#endif
          break;
        }
        else if (response.d_status == REWRITE_DONE)
        {
#ifdef CVC5_ASSERTIONS
          RewriteResponse r2 =
              d_theoryRewriters[newTheoryId]->postRewrite(response.d_node);
          Assert(r2.d_node == response.d_node)
              << r2.d_node << " != " << response.d_node;
#endif
          rewriteStackTop.d_node = response.d_node;
          break;
        }
        // Check for trivial rewrite loops of size 1 or 2
        Assert(response.d_node != rewriteStackTop.d_node);
        Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
                   ->postRewrite(response.d_node)
                   .d_node
               != rewriteStackTop.d_node);
        rewriteStackTop.d_node = response.d_node;
      }

      // We're done with the post rewrite, so we add to the cache
      if (tcpg != nullptr)
      {
        // if proofs are enabled, mark that we've rewritten with proofs
        d_tpgNodes.insert(rewriteStackTop.d_original);
        if (!cached.isNull())
        {
          // We may have gotten a different node, due to non-determinism in
          // theory rewriters (e.g. quantifiers rewriter which introduces
          // fresh BOUND_VARIABLE). This can happen if we wrote once without
          // proofs and then rewrote again with proofs.
          if (rewriteStackTop.d_node != cached)
          {
            Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
                                       "without proofs were not equivalent"
                                    << std::endl;
            Trace("rewriter-proof")
                << "   original: " << rewriteStackTop.d_original << std::endl;
            Trace("rewriter-proof")
                << "with proofs: " << rewriteStackTop.d_node << std::endl;
            Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
            Node eq = rewriteStackTop.d_node.eqNode(cached);
            // we make this a post-rewrite, since we are processing a node that
            // has finished post-rewriting above
            tcpg->addRewriteStep(rewriteStackTop.d_node,
                                 cached,
                                 PfRule::TRUST_REWRITE,
                                 {},
                                 {eq},
                                 false);
            // don't overwrite the cache, should be the same
            rewriteStackTop.d_node = cached;
          }
        }
      }
      setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
                          rewriteStackTop.d_original,
                          rewriteStackTop.d_node);
    }
    else
    {
      // We were already in cache, so just remember it
      rewriteStackTop.d_node = cached;
      rewriteStackTop.d_theoryId = theoryOf(cached);
    }

    // If this is the last node, just return
    if (rewriteStack.size() == 1) {
      Assert(!isEquality || rewriteStackTop.d_node.getKind() == kind::EQUAL
             || rewriteStackTop.d_node.isConst());
      return rewriteStackTop.d_node;
    }

    // We're done with this node, append it to the parent
    rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node;
    rewriteStack.pop_back();
  }

  Unreachable();
} /* Rewriter::rewriteTo() */

RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
                                     TNode n,
                                     TConvProofGenerator* tcpg)
{
  if (tcpg != nullptr)
  {
    // call the trust rewrite response interface
    TrustRewriteResponse tresponse =
        d_theoryRewriters[theoryId]->preRewriteWithProof(n);
    // process the trust rewrite response: store the proof step into
    // tcpg if necessary and then convert to rewrite response.
    return processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
  }
  return d_theoryRewriters[theoryId]->preRewrite(n);
}

RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
                                      TNode n,
                                      TConvProofGenerator* tcpg)
{
  if (tcpg != nullptr)
  {
    // same as above, for post-rewrite
    TrustRewriteResponse tresponse =
        d_theoryRewriters[theoryId]->postRewriteWithProof(n);
    return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
  }
  return d_theoryRewriters[theoryId]->postRewrite(n);
}

RewriteResponse Rewriter::processTrustRewriteResponse(
    theory::TheoryId theoryId,
    const TrustRewriteResponse& tresponse,
    bool isPre,
    TConvProofGenerator* tcpg)
{
  Assert(tcpg != nullptr);
  TrustNode trn = tresponse.d_node;
  Assert(trn.getKind() == TrustNodeKind::REWRITE);
  Node proven = trn.getProven();
  if (proven[0] != proven[1])
  {
    ProofGenerator* pg = trn.getGenerator();
    if (pg == nullptr)
    {
      Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
      // add small step trusted rewrite
      Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE
                                  : MethodId::RW_REWRITE_THEORY_POST);
      tcpg->addRewriteStep(proven[0],
                           proven[1],
                           PfRule::THEORY_REWRITE,
                           {},
                           {proven, tidn, rid},
                           isPre);
    }
    else
    {
      // store proven rewrite step
      tcpg->addRewriteStep(proven[0], proven[1], pg, isPre);
    }
  }
  return RewriteResponse(tresponse.d_status, trn.getNode());
}

void Rewriter::clearCaches()
{
#ifdef CVC5_ASSERTIONS
  d_rewriteStack.reset(nullptr);
#endif

  clearCachesInternal();
}

bool Rewriter::hasRewrittenWithProofs(TNode n) const
{
  return d_tpgNodes.find(n) != d_tpgNodes.end();
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Andres Noetzli, 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 "theory/rewriter.h"
17
18		#include "options/theory_options.h"
19		#include "proof/conv_proof_generator.h"
20		#include "smt/smt_statistics_registry.h"
21		#include "smt/solver_engine.h"
22		#include "smt/solver_engine_scope.h"
23		#include "theory/builtin/proof_checker.h"
24		#include "theory/evaluator.h"
25		#include "theory/quantifiers/extended_rewrite.h"
26		#include "theory/rewriter_tables.h"
27		#include "theory/theory.h"
28		#include "util/resource_manager.h"
29
30		using namespace std;
31
32		namespace cvc5 {
33		namespace theory {
34
35		// Note that this function is a simplified version of Theory::theoryOf for
36		// (type-based) theoryOfMode. We expand and simplify it here for the sake of
37		// efficiency.
38	174142126	static TheoryId theoryOf(TNode node) {
39	174142126	if (node.getKind() == kind::EQUAL)
40		{
41		// Equality is owned by the theory that owns the domain
42	25678392	return Theory::theoryOf(node[0].getType());
43		}
44		// Regular nodes are owned by the kind
45	148463734	return kindToTheoryId(node.getKind());
46		}
47
48		/**
49		* TheoryEngine::rewrite() keeps a stack of things that are being pre-
50		* and post-rewritten. Each element of the stack is a
51		* RewriteStackElement.
52		*/
53	136660687	struct RewriteStackElement {
54		/**
55		* Construct a fresh stack element.
56		*/
57	40557217	RewriteStackElement(TNode node, TheoryId theoryId)
58	40557217	: d_node(node),
59		d_original(node),
60		d_theoryId(theoryId),
61		d_originalTheoryId(theoryId),
62	40557217	d_nextChild(0)
63		{
64	40557217	}
65
66	239300169	TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); }
67
68	23752129	TheoryId getOriginalTheoryId()
69		{
70	23752129	return static_cast<TheoryId>(d_originalTheoryId);
71		}
72
73		/** The node we're currently rewriting */
74		Node d_node;
75		/** Original node (either the unrewritten node or the node after prerewriting)
76		*/
77		Node d_original;
78		/** Id of the theory that's currently rewriting this node */
79		unsigned d_theoryId : 8;
80		/** Id of the original theory that started the rewrite */
81		unsigned d_originalTheoryId : 8;
82		/** Index of the child this node is done rewriting */
83		unsigned d_nextChild : 32;
84		/** Builder for this node */
85		NodeBuilder d_builder;
86		};
87
88
89	51786651	Node Rewriter::rewrite(TNode node) {
90	51786651	if (node.getNumChildren() == 0)
91		{
92		// Nodes with zero children should never change via rewriting. We return
93		// eagerly for the sake of efficiency here.
94	4714439	return node;
95		}
96	47072212	return getInstance()->rewriteTo(theoryOf(node), node);
97		}
98
99	95771	Node Rewriter::callExtendedRewrite(TNode node, bool aggr)
100		{
101	95771	return getInstance()->extendedRewrite(node, aggr);
102		}
103
104	483454	Node Rewriter::extendedRewrite(TNode node, bool aggr)
105		{
106	966908	quantifiers::ExtendedRewriter er(*this, aggr);
107	966908	return er.extendedRewrite(node);
108		}
109
110	65923	TrustNode Rewriter::rewriteWithProof(TNode node,
111		bool isExtEq)
112		{
113		// must set the proof checker before calling this
114	65923	Assert(d_tpg != nullptr);
115	65923	if (isExtEq)
116		{
117		// theory rewriter is responsible for rewriting the equality
118	69	TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)];
119	69	Assert(tr != nullptr);
120	69	return tr->rewriteEqualityExtWithProof(node);
121		}
122	131708	Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get());
123	65854	return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
124		}
125
126	7987	void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
127		{
128		// if not already initialized with proof support
129	7987	if (d_tpg == nullptr)
130		{
131	7987	Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl;
132		// the rewriter is staticly determinstic, thus use static cache policy
133		// for the term conversion proof generator
134	15974	d_tpg.reset(new TConvProofGenerator(pnm,
135		nullptr,
136		TConvPolicy::FIXPOINT,
137		TConvCachePolicy::STATIC,
138	7987	"Rewriter::TConvProofGenerator"));
139		}
140	7987	}
141
142	237	Node Rewriter::rewriteEqualityExt(TNode node)
143		{
144	237	Assert(node.getKind() == kind::EQUAL);
145		// note we don't force caching of this method currently
146	237	return d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(node);
147		}
148
149	198572	void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
150		TheoryRewriter* trew)
151		{
152	198572	d_theoryRewriters[tid] = trew;
153	198572	}
154
155	20259	TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
156		{
157	20259	return d_theoryRewriters[theoryId];
158		}
159
160	47233906	Rewriter* Rewriter::getInstance()
161		{
162	47233906	return smt::currentSolverEngine()->getRewriter();
163		}
164
165	48551397	Node Rewriter::rewriteTo(theory::TheoryId theoryId,
166		Node node,
167		TConvProofGenerator* tcpg)
168		{
169		#ifdef CVC5_ASSERTIONS
170	48551397	bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
171
172	48551397	if (d_rewriteStack == nullptr)
173		{
174	14843	d_rewriteStack.reset(new std::unordered_set<Node>());
175		}
176		#endif
177
178	48551397	Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
179
180		// Check if it's been cached already
181	97102794	Node cached = getPostRewriteCache(theoryId, node);
182	48551397	if (!cached.isNull() && (tcpg == nullptr \|\| hasRewrittenWithProofs(node)))
183		{
184	41349307	return cached;
185		}
186
187		// Put the node on the stack in order to start the "recursive" rewrite
188	14404180	vector<RewriteStackElement> rewriteStack;
189	7202090	rewriteStack.push_back(RewriteStackElement(node, theoryId));
190
191		// Rewrite until the stack is empty
192		for (;;){
193	73912342	if (d_resourceManager != nullptr)
194		{
195	73912342	d_resourceManager->spendResource(Resource::RewriteStep);
196		}
197
198		// Get the top of the recursion stack
199	73912342	RewriteStackElement& rewriteStackTop = rewriteStack.back();
200
201	147824684	Trace("rewriter") << "Rewriter::rewriting: "
202	147824684	<< rewriteStackTop.getTheoryId() << ","
203	73912342	<< rewriteStackTop.d_node << std::endl;
204
205		// Before rewriting children we need to do a pre-rewrite of the node
206	73912342	if (rewriteStackTop.d_nextChild == 0)
207		{
208		// Check if the pre-rewrite has already been done (it's in the cache)
209	40557217	cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
210		rewriteStackTop.d_node);
211	81114434	if (cached.isNull()
212	93394981	\|\| (tcpg != nullptr
213	41536549	&& !hasRewrittenWithProofs(rewriteStackTop.d_node)))
214		{
215		// Rewrite until fix-point is reached
216		for(;;) {
217		// Perform the pre-rewrite
218		RewriteResponse response = preRewrite(
219	14854903	rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
220
221		// Put the rewritten node to the top of the stack
222	13567725	rewriteStackTop.d_node = response.d_node;
223	13567725	TheoryId newTheory = theoryOf(rewriteStackTop.d_node);
224		// In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
225	27135450	if (newTheory == rewriteStackTop.getTheoryId()
226	13567725	&& response.d_status == REWRITE_DONE)
227		{
228	12280547	break;
229		}
230	1287178	rewriteStackTop.d_theoryId = newTheory;
231	1287178	}
232
233		// Cache the rewrite
234	12280547	setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
235		rewriteStackTop.d_original,
236		rewriteStackTop.d_node);
237		}
238		// Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
239		else {
240		// Continue with the cached version
241	28276670	rewriteStackTop.d_node = cached;
242	28276670	rewriteStackTop.d_theoryId = theoryOf(cached);
243		}
244		}
245
246	73912342	rewriteStackTop.d_original = rewriteStackTop.d_node;
247		// Now it's time to rewrite the children, check if this has already been done
248	73912342	cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
249		rewriteStackTop.d_node);
250		// If not, go through the children
251	147824684	if (cached.isNull()
252	147824684	\|\| (tcpg != nullptr && !hasRewrittenWithProofs(rewriteStackTop.d_node)))
253		{
254		// The child we need to rewrite
255	44826711	unsigned child = rewriteStackTop.d_nextChild++;
256
257		// To build the rewritten expression we set up the builder
258	44826711	if(child == 0) {
259	11471586	if (rewriteStackTop.d_node.getNumChildren() > 0)
260		{
261		// The children will add themselves to the builder once they're done
262	10967137	rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind();
263	10967137	kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind();
264	10967137	if (metaKind == kind::metakind::PARAMETERIZED) {
265	742398	rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator();
266		}
267		}
268		}
269
270		// Process the next child
271	44826711	if (child < rewriteStackTop.d_node.getNumChildren())
272		{
273		// The child node
274	66710254	Node childNode = rewriteStackTop.d_node[child];
275		// Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
276	33355127	rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
277		// Go on with the rewriting
278	33355127	continue;
279		}
280
281		// Incorporate the children if necessary
282	11471584	if (rewriteStackTop.d_node.getNumChildren() > 0)
283		{
284	21934270	Node rewritten = rewriteStackTop.d_builder;
285	10967135	rewriteStackTop.d_node = rewritten;
286	10967135	rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
287		}
288
289		// Done with all pre-rewriting, so let's do the post rewrite
290		for(;;) {
291		// Do the post-rewrite
292		RewriteResponse response = postRewrite(
293	12031354	rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
294
295		// We continue with the response we got
296	11751466	TheoryId newTheoryId = theoryOf(response.d_node);
297	23502932	if (newTheoryId != rewriteStackTop.getTheoryId()
298	11751466	\|\| response.d_status == REWRITE_AGAIN_FULL)
299		{
300		// In the post rewrite if we've changed theories, we must do a full rewrite
301	1413331	Assert(response.d_node != rewriteStackTop.d_node);
302		//TODO: this is not thread-safe - should make this assertion dependent on sequential build
303		#ifdef CVC5_ASSERTIONS
304	1413331	Assert(d_rewriteStack->find(response.d_node)
305		== d_rewriteStack->end());
306	1413331	d_rewriteStack->insert(response.d_node);
307		#endif
308	2826662	Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
309	1413331	rewriteStackTop.d_node = rewritten;
310		#ifdef CVC5_ASSERTIONS
311	1413331	d_rewriteStack->erase(response.d_node);
312		#endif
313	1413331	break;
314		}
315	10338135	else if (response.d_status == REWRITE_DONE)
316		{
317		#ifdef CVC5_ASSERTIONS
318		RewriteResponse r2 =
319	20116502	d_theoryRewriters[newTheoryId]->postRewrite(response.d_node);
320	20116502	Assert(r2.d_node == response.d_node)
321	10058251	<< r2.d_node << " != " << response.d_node;
322		#endif
323	10058251	rewriteStackTop.d_node = response.d_node;
324	10058251	break;
325		}
326		// Check for trivial rewrite loops of size 1 or 2
327	279884	Assert(response.d_node != rewriteStackTop.d_node);
328	279884	Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
329		->postRewrite(response.d_node)
330		.d_node
331		!= rewriteStackTop.d_node);
332	279884	rewriteStackTop.d_node = response.d_node;
333	279884	}
334
335		// We're done with the post rewrite, so we add to the cache
336	11471582	if (tcpg != nullptr)
337		{
338		// if proofs are enabled, mark that we've rewritten with proofs
339	424548	d_tpgNodes.insert(rewriteStackTop.d_original);
340	424548	if (!cached.isNull())
341		{
342		// We may have gotten a different node, due to non-determinism in
343		// theory rewriters (e.g. quantifiers rewriter which introduces
344		// fresh BOUND_VARIABLE). This can happen if we wrote once without
345		// proofs and then rewrote again with proofs.
346	410414	if (rewriteStackTop.d_node != cached)
347		{
348		Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
349		"without proofs were not equivalent"
350		<< std::endl;
351		Trace("rewriter-proof")
352		<< " original: " << rewriteStackTop.d_original << std::endl;
353		Trace("rewriter-proof")
354		<< "with proofs: " << rewriteStackTop.d_node << std::endl;
355		Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
356		Node eq = rewriteStackTop.d_node.eqNode(cached);
357		// we make this a post-rewrite, since we are processing a node that
358		// has finished post-rewriting above
359		tcpg->addRewriteStep(rewriteStackTop.d_node,
360		cached,
361		PfRule::TRUST_REWRITE,
362		{},
363		{eq},
364		false);
365		// don't overwrite the cache, should be the same
366		rewriteStackTop.d_node = cached;
367		}
368		}
369		}
370	11471582	setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
371		rewriteStackTop.d_original,
372		rewriteStackTop.d_node);
373		}
374		else
375		{
376		// We were already in cache, so just remember it
377	29085631	rewriteStackTop.d_node = cached;
378	29085631	rewriteStackTop.d_theoryId = theoryOf(cached);
379		}
380
381		// If this is the last node, just return
382	40557213	if (rewriteStack.size() == 1) {
383	7202088	Assert(!isEquality \|\| rewriteStackTop.d_node.getKind() == kind::EQUAL
384		\|\| rewriteStackTop.d_node.isConst());
385	7202088	return rewriteStackTop.d_node;
386		}
387
388		// We're done with this node, append it to the parent
389	33355125	rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node;
390	33355125	rewriteStack.pop_back();
391	66710252	}
392
393		Unreachable();
394		} /* Rewriter::rewriteTo() */
395
396	13567725	RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
397		TNode n,
398		TConvProofGenerator* tcpg)
399		{
400	13567725	if (tcpg != nullptr)
401		{
402		// call the trust rewrite response interface
403		TrustRewriteResponse tresponse =
404	1212546	d_theoryRewriters[theoryId]->preRewriteWithProof(n);
405		// process the trust rewrite response: store the proof step into
406		// tcpg if necessary and then convert to rewrite response.
407	606273	return processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
408		}
409	12961452	return d_theoryRewriters[theoryId]->preRewrite(n);
410		}
411
412	11751468	RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
413		TNode n,
414		TConvProofGenerator* tcpg)
415		{
416	11751468	if (tcpg != nullptr)
417		{
418		// same as above, for post-rewrite
419		TrustRewriteResponse tresponse =
420	864598	d_theoryRewriters[theoryId]->postRewriteWithProof(n);
421	432299	return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
422		}
423	11319171	return d_theoryRewriters[theoryId]->postRewrite(n);
424		}
425
426	1038572	RewriteResponse Rewriter::processTrustRewriteResponse(
427		theory::TheoryId theoryId,
428		const TrustRewriteResponse& tresponse,
429		bool isPre,
430		TConvProofGenerator* tcpg)
431		{
432	1038572	Assert(tcpg != nullptr);
433	2077144	TrustNode trn = tresponse.d_node;
434	1038572	Assert(trn.getKind() == TrustNodeKind::REWRITE);
435	2077144	Node proven = trn.getProven();
436	1038572	if (proven[0] != proven[1])
437		{
438	260765	ProofGenerator* pg = trn.getGenerator();
439	260765	if (pg == nullptr)
440		{
441	521530	Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
442		// add small step trusted rewrite
443		Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE
444	521530	: MethodId::RW_REWRITE_THEORY_POST);
445	1043060	tcpg->addRewriteStep(proven[0],
446		proven[1],
447		PfRule::THEORY_REWRITE,
448		{},
449		{proven, tidn, rid},
450	782295	isPre);
451		}
452		else
453		{
454		// store proven rewrite step
455		tcpg->addRewriteStep(proven[0], proven[1], pg, isPre);
456		}
457		}
458	2077144	return RewriteResponse(tresponse.d_status, trn.getNode());
459		}
460
461		void Rewriter::clearCaches()
462		{
463		#ifdef CVC5_ASSERTIONS
464		d_rewriteStack.reset(nullptr);
465		#endif
466
467		clearCachesInternal();
468		}
469
470	2908570	bool Rewriter::hasRewrittenWithProofs(TNode n) const
471		{
472	2908570	return d_tpgNodes.find(n) != d_tpgNodes.end();
473		}
474
475		} // namespace theory
476	31137	} // namespace cvc5