Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/rewriter.cpp	Lines:	171	195	87.7 %
Date:	2021-05-24	Branches:	331	766	43.2 %


/******************************************************************************
 * 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 "expr/term_conversion_proof_generator.h"
#include "options/theory_options.h"
#include "smt/smt_engine.h"
#include "smt/smt_engine_scope.h"
#include "smt/smt_statistics_registry.h"
#include "theory/builtin/proof_checker.h"
#include "theory/rewriter_tables.h"
#include "theory/theory.h"
#include "util/resource_manager.h"

using namespace std;

namespace cvc5 {
namespace theory {

/** Attribute true for nodes that have been rewritten with proofs enabled */
struct RewriteWithProofsAttributeId
{
};
typedef expr::Attribute<RewriteWithProofsAttributeId, bool>
    RewriteWithProofsAttribute;

// 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;
};

RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n)
{
  return RewriteResponse(REWRITE_DONE, n);
}

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);
}

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 getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(
      node);
}

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

void Rewriter::registerPreRewrite(
    Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
{
  Assert(k != kind::EQUAL) << "Register pre-rewrites for EQUAL with registerPreRewriteEqual.";
  d_preRewriters[k] = fn;
}

void Rewriter::registerPostRewrite(
    Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
{
  Assert(k != kind::EQUAL) << "Register post-rewrites for EQUAL with registerPostRewriteEqual.";
  d_postRewriters[k] = fn;
}

void Rewriter::registerPreRewriteEqual(
    theory::TheoryId tid,
    std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
{
  d_preRewritersEqual[tid] = fn;
}

void Rewriter::registerPostRewriteEqual(
    theory::TheoryId tid,
    std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
{
  d_postRewritersEqual[tid] = fn;
}

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

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

Node Rewriter::rewriteTo(theory::TheoryId theoryId,
                         Node node,
                         TConvProofGenerator* tcpg)
{
  RewriteWithProofsAttribute rpfa;
#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 || node.getAttribute(rpfa)))
  {
    return cached;
  }

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

  ResourceManager* rm = NULL;
  bool hasSmtEngine = smt::smtEngineInScope();
  if (hasSmtEngine) {
    rm = smt::currentResourceManager();
  }
  // Rewrite until the stack is empty
  for (;;){
    if (hasSmtEngine)
    {
      rm->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 && !rewriteStackTop.d_node.getAttribute(rpfa)))
      {
        // 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 && !rewriteStackTop.d_node.getAttribute(rpfa)))
    {
      // 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
        rewriteStackTop.d_original.setAttribute(rpfa, true);
        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)
{
  Kind k = n.getKind();
  std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
      (k == kind::EQUAL) ? d_preRewritersEqual[theoryId] : d_preRewriters[k];
  if (fn == nullptr)
  {
    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);
  }
  return fn(&d_re, n);
}

RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
                                      TNode n,
                                      TConvProofGenerator* tcpg)
{
  Kind k = n.getKind();
  std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
      (k == kind::EQUAL) ? d_postRewritersEqual[theoryId] : d_postRewriters[k];
  if (fn == nullptr)
  {
    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);
  }
  return fn(&d_re, 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() {
  Rewriter* rewriter = getInstance();

#ifdef CVC5_ASSERTIONS
  rewriter->d_rewriteStack.reset(nullptr);
#endif

  rewriter->clearCachesInternal();
}

}  // 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 "expr/term_conversion_proof_generator.h"
19		#include "options/theory_options.h"
20		#include "smt/smt_engine.h"
21		#include "smt/smt_engine_scope.h"
22		#include "smt/smt_statistics_registry.h"
23		#include "theory/builtin/proof_checker.h"
24		#include "theory/rewriter_tables.h"
25		#include "theory/theory.h"
26		#include "util/resource_manager.h"
27
28		using namespace std;
29
30		namespace cvc5 {
31		namespace theory {
32
33		/** Attribute true for nodes that have been rewritten with proofs enabled */
34		struct RewriteWithProofsAttributeId
35		{
36		};
37		typedef expr::Attribute<RewriteWithProofsAttributeId, bool>
38		RewriteWithProofsAttribute;
39
40		// Note that this function is a simplified version of Theory::theoryOf for
41		// (type-based) theoryOfMode. We expand and simplify it here for the sake of
42		// efficiency.
43	147662921	static TheoryId theoryOf(TNode node) {
44	147662921	if (node.getKind() == kind::EQUAL)
45		{
46		// Equality is owned by the theory that owns the domain
47	20101737	return Theory::theoryOf(node[0].getType());
48		}
49		// Regular nodes are owned by the kind
50	127561184	return kindToTheoryId(node.getKind());
51		}
52
53		/**
54		* TheoryEngine::rewrite() keeps a stack of things that are being pre-
55		* and post-rewritten. Each element of the stack is a
56		* RewriteStackElement.
57		*/
58	127314509	struct RewriteStackElement {
59		/**
60		* Construct a fresh stack element.
61		*/
62	38056839	RewriteStackElement(TNode node, TheoryId theoryId)
63	38056839	: d_node(node),
64		d_original(node),
65		d_theoryId(theoryId),
66		d_originalTheoryId(theoryId),
67	38056839	d_nextChild(0)
68		{
69	38056839	}
70
71	226518859	TheoryId getTheoryId() { return static_cast<TheoryId>(d_theoryId); }
72
73	22563504	TheoryId getOriginalTheoryId()
74		{
75	22563504	return static_cast<TheoryId>(d_originalTheoryId);
76		}
77
78		/** The node we're currently rewriting */
79		Node d_node;
80		/** Original node (either the unrewritten node or the node after prerewriting)
81		*/
82		Node d_original;
83		/** Id of the theory that's currently rewriting this node */
84		unsigned d_theoryId : 8;
85		/** Id of the original theory that started the rewrite */
86		unsigned d_originalTheoryId : 8;
87		/** Index of the child this node is done rewriting */
88		unsigned d_nextChild : 32;
89		/** Builder for this node */
90		NodeBuilder d_builder;
91		};
92
93		RewriteResponse identityRewrite(RewriteEnvironment* re, TNode n)
94		{
95		return RewriteResponse(REWRITE_DONE, n);
96		}
97
98	35625367	Node Rewriter::rewrite(TNode node) {
99	35625367	if (node.getNumChildren() == 0)
100		{
101		// Nodes with zero children should never change via rewriting. We return
102		// eagerly for the sake of efficiency here.
103	8026483	return node;
104		}
105	27598884	return getInstance()->rewriteTo(theoryOf(node), node);
106		}
107
108	57096	TrustNode Rewriter::rewriteWithProof(TNode node,
109		bool isExtEq)
110		{
111		// must set the proof checker before calling this
112	57096	Assert(d_tpg != nullptr);
113	57096	if (isExtEq)
114		{
115		// theory rewriter is responsible for rewriting the equality
116	8	TheoryRewriter* tr = getInstance()->d_theoryRewriters[theoryOf(node)];
117	8	Assert(tr != nullptr);
118	8	return tr->rewriteEqualityExtWithProof(node);
119		}
120	114176	Node ret = getInstance()->rewriteTo(theoryOf(node), node, d_tpg.get());
121	57088	return TrustNode::mkTrustRewrite(node, ret, d_tpg.get());
122		}
123
124	3600	void Rewriter::setProofNodeManager(ProofNodeManager* pnm)
125		{
126		// if not already initialized with proof support
127	3600	if (d_tpg == nullptr)
128		{
129	3600	Trace("rewriter") << "Rewriter::setProofNodeManager" << std::endl;
130		// the rewriter is staticly determinstic, thus use static cache policy
131		// for the term conversion proof generator
132	7200	d_tpg.reset(new TConvProofGenerator(pnm,
133		nullptr,
134		TConvPolicy::FIXPOINT,
135		TConvCachePolicy::STATIC,
136	3600	"Rewriter::TConvProofGenerator"));
137		}
138	3600	}
139
140	104	Node Rewriter::rewriteEqualityExt(TNode node)
141		{
142	104	Assert(node.getKind() == kind::EQUAL);
143		// note we don't force caching of this method currently
144	208	return getInstance()->d_theoryRewriters[theoryOf(node)]->rewriteEqualityExt(
145	208	node);
146		}
147
148	123003	void Rewriter::registerTheoryRewriter(theory::TheoryId tid,
149		TheoryRewriter* trew)
150		{
151	123003	getInstance()->d_theoryRewriters[tid] = trew;
152	123003	}
153
154		void Rewriter::registerPreRewrite(
155		Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
156		{
157		Assert(k != kind::EQUAL) << "Register pre-rewrites for EQUAL with registerPreRewriteEqual.";
158		d_preRewriters[k] = fn;
159		}
160
161		void Rewriter::registerPostRewrite(
162		Kind k, std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
163		{
164		Assert(k != kind::EQUAL) << "Register post-rewrites for EQUAL with registerPostRewriteEqual.";
165		d_postRewriters[k] = fn;
166		}
167
168		void Rewriter::registerPreRewriteEqual(
169		theory::TheoryId tid,
170		std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
171		{
172		d_preRewritersEqual[tid] = fn;
173		}
174
175		void Rewriter::registerPostRewriteEqual(
176		theory::TheoryId tid,
177		std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn)
178		{
179		d_postRewritersEqual[tid] = fn;
180		}
181
182	12333	TheoryRewriter* Rewriter::getTheoryRewriter(theory::TheoryId theoryId)
183		{
184	12333	return d_theoryRewriters[theoryId];
185		}
186
187	27779087	Rewriter* Rewriter::getInstance()
188		{
189	27779087	return smt::currentSmtEngine()->getRewriter();
190		}
191
192	28773126	Node Rewriter::rewriteTo(theory::TheoryId theoryId,
193		Node node,
194		TConvProofGenerator* tcpg)
195		{
196		RewriteWithProofsAttribute rpfa;
197		#ifdef CVC5_ASSERTIONS
198	28773126	bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
199
200	28773126	if (d_rewriteStack == nullptr)
201		{
202	9130	d_rewriteStack.reset(new std::unordered_set<Node>());
203		}
204		#endif
205
206	28773126	Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
207
208		// Check if it's been cached already
209	57546252	Node cached = getPostRewriteCache(theoryId, node);
210	28773126	if (!cached.isNull() && (tcpg == nullptr \|\| node.getAttribute(rpfa)))
211		{
212	23024875	return cached;
213		}
214
215		// Put the node on the stack in order to start the "recursive" rewrite
216	11496502	vector<RewriteStackElement> rewriteStack;
217	5748251	rewriteStack.push_back(RewriteStackElement(node, theoryId));
218
219	5748251	ResourceManager* rm = NULL;
220	5748251	bool hasSmtEngine = smt::smtEngineInScope();
221	5748251	if (hasSmtEngine) {
222	5748251	rm = smt::currentResourceManager();
223		}
224		// Rewrite until the stack is empty
225		for (;;){
226	70365425	if (hasSmtEngine)
227		{
228	70365425	rm->spendResource(Resource::RewriteStep);
229		}
230
231		// Get the top of the recursion stack
232	70365425	RewriteStackElement& rewriteStackTop = rewriteStack.back();
233
234	140730850	Trace("rewriter") << "Rewriter::rewriting: "
235	140730850	<< rewriteStackTop.getTheoryId() << ","
236	70365425	<< rewriteStackTop.d_node << std::endl;
237
238		// Before rewriting children we need to do a pre-rewrite of the node
239	70365425	if (rewriteStackTop.d_nextChild == 0)
240		{
241		// Check if the pre-rewrite has already been done (it's in the cache)
242	38056839	cached = getPreRewriteCache(rewriteStackTop.getTheoryId(),
243		rewriteStackTop.d_node);
244	76113678	if (cached.isNull()
245	38056839	\|\| (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
246		{
247		// Rewrite until fix-point is reached
248		for(;;) {
249		// Perform the pre-rewrite
250		RewriteResponse response = preRewrite(
251	13463579	rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
252
253		// Put the rewritten node to the top of the stack
254	12521187	rewriteStackTop.d_node = response.d_node;
255	12521187	TheoryId newTheory = theoryOf(rewriteStackTop.d_node);
256		// In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
257	25042374	if (newTheory == rewriteStackTop.getTheoryId()
258	12521187	&& response.d_status == REWRITE_DONE)
259		{
260	11578795	break;
261		}
262	942392	rewriteStackTop.d_theoryId = newTheory;
263	942392	}
264
265		// Cache the rewrite
266	11578795	setPreRewriteCache(rewriteStackTop.getOriginalTheoryId(),
267		rewriteStackTop.d_original,
268		rewriteStackTop.d_node);
269		}
270		// Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
271		else {
272		// Continue with the cached version
273	26478044	rewriteStackTop.d_node = cached;
274	26478044	rewriteStackTop.d_theoryId = theoryOf(cached);
275		}
276		}
277
278	70365425	rewriteStackTop.d_original = rewriteStackTop.d_node;
279		// Now it's time to rewrite the children, check if this has already been done
280	70365425	cached = getPostRewriteCache(rewriteStackTop.getTheoryId(),
281		rewriteStackTop.d_node);
282		// If not, go through the children
283	140730850	if (cached.isNull()
284	70365425	\|\| (tcpg != nullptr && !rewriteStackTop.d_node.getAttribute(rpfa)))
285		{
286		// The child we need to rewrite
287	43293299	unsigned child = rewriteStackTop.d_nextChild++;
288
289		// To build the rewritten expression we set up the builder
290	43293299	if(child == 0) {
291	10984713	if (rewriteStackTop.d_node.getNumChildren() > 0)
292		{
293		// The children will add themselves to the builder once they're done
294	10402393	rewriteStackTop.d_builder << rewriteStackTop.d_node.getKind();
295	10402393	kind::MetaKind metaKind = rewriteStackTop.d_node.getMetaKind();
296	10402393	if (metaKind == kind::metakind::PARAMETERIZED) {
297	726976	rewriteStackTop.d_builder << rewriteStackTop.d_node.getOperator();
298		}
299		}
300		}
301
302		// Process the next child
303	43293299	if (child < rewriteStackTop.d_node.getNumChildren())
304		{
305		// The child node
306	64617176	Node childNode = rewriteStackTop.d_node[child];
307		// Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
308	32308588	rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
309		// Go on with the rewriting
310	32308588	continue;
311		}
312
313		// Incorporate the children if necessary
314	10984711	if (rewriteStackTop.d_node.getNumChildren() > 0)
315		{
316	20804782	Node rewritten = rewriteStackTop.d_builder;
317	10402391	rewriteStackTop.d_node = rewritten;
318	10402391	rewriteStackTop.d_theoryId = theoryOf(rewriteStackTop.d_node);
319		}
320
321		// Done with all pre-rewriting, so let's do the post rewrite
322		for(;;) {
323		// Do the post-rewrite
324		RewriteResponse response = postRewrite(
325	11464297	rewriteStackTop.getTheoryId(), rewriteStackTop.d_node, tcpg);
326
327		// We continue with the response we got
328	11224501	TheoryId newTheoryId = theoryOf(response.d_node);
329	22449002	if (newTheoryId != rewriteStackTop.getTheoryId()
330	11224501	\|\| response.d_status == REWRITE_AGAIN_FULL)
331		{
332		// In the post rewrite if we've changed theories, we must do a full rewrite
333	1117154	Assert(response.d_node != rewriteStackTop.d_node);
334		//TODO: this is not thread-safe - should make this assertion dependent on sequential build
335		#ifdef CVC5_ASSERTIONS
336	1117154	Assert(d_rewriteStack->find(response.d_node)
337		== d_rewriteStack->end());
338	1117154	d_rewriteStack->insert(response.d_node);
339		#endif
340	2234308	Node rewritten = rewriteTo(newTheoryId, response.d_node, tcpg);
341	1117154	rewriteStackTop.d_node = rewritten;
342		#ifdef CVC5_ASSERTIONS
343	1117154	d_rewriteStack->erase(response.d_node);
344		#endif
345	1117154	break;
346		}
347	10107347	else if (response.d_status == REWRITE_DONE)
348		{
349		#ifdef CVC5_ASSERTIONS
350		RewriteResponse r2 =
351	19735110	d_theoryRewriters[newTheoryId]->postRewrite(response.d_node);
352	19735110	Assert(r2.d_node == response.d_node)
353	9867555	<< r2.d_node << " != " << response.d_node;
354		#endif
355	9867555	rewriteStackTop.d_node = response.d_node;
356	9867555	break;
357		}
358		// Check for trivial rewrite loops of size 1 or 2
359	239792	Assert(response.d_node != rewriteStackTop.d_node);
360	239792	Assert(d_theoryRewriters[rewriteStackTop.getTheoryId()]
361		->postRewrite(response.d_node)
362		.d_node
363		!= rewriteStackTop.d_node);
364	239792	rewriteStackTop.d_node = response.d_node;
365	239792	}
366
367		// We're done with the post rewrite, so we add to the cache
368	10984709	if (tcpg != nullptr)
369		{
370		// if proofs are enabled, mark that we've rewritten with proofs
371	348910	rewriteStackTop.d_original.setAttribute(rpfa, true);
372	348910	if (!cached.isNull())
373		{
374		// We may have gotten a different node, due to non-determinism in
375		// theory rewriters (e.g. quantifiers rewriter which introduces
376		// fresh BOUND_VARIABLE). This can happen if we wrote once without
377		// proofs and then rewrote again with proofs.
378	334368	if (rewriteStackTop.d_node != cached)
379		{
380	78	Trace("rewriter-proof") << "WARNING: Rewritten forms with and "
381	39	"without proofs were not equivalent"
382	39	<< std::endl;
383	78	Trace("rewriter-proof")
384	39	<< " original: " << rewriteStackTop.d_original << std::endl;
385	78	Trace("rewriter-proof")
386	39	<< "with proofs: " << rewriteStackTop.d_node << std::endl;
387	39	Trace("rewriter-proof") << " w/o proofs: " << cached << std::endl;
388	78	Node eq = rewriteStackTop.d_node.eqNode(cached);
389		// we make this a post-rewrite, since we are processing a node that
390		// has finished post-rewriting above
391	78	tcpg->addRewriteStep(rewriteStackTop.d_node,
392		cached,
393		PfRule::TRUST_REWRITE,
394		{},
395		{eq},
396	39	false);
397		// don't overwrite the cache, should be the same
398	39	rewriteStackTop.d_node = cached;
399		}
400		}
401		}
402	10984709	setPostRewriteCache(rewriteStackTop.getOriginalTheoryId(),
403		rewriteStackTop.d_original,
404		rewriteStackTop.d_node);
405		}
406		else
407		{
408		// We were already in cache, so just remember it
409	27072126	rewriteStackTop.d_node = cached;
410	27072126	rewriteStackTop.d_theoryId = theoryOf(cached);
411		}
412
413		// If this is the last node, just return
414	38056835	if (rewriteStack.size() == 1) {
415	5748249	Assert(!isEquality \|\| rewriteStackTop.d_node.getKind() == kind::EQUAL
416		\|\| rewriteStackTop.d_node.isConst());
417	5748249	return rewriteStackTop.d_node;
418		}
419
420		// We're done with this node, append it to the parent
421	32308586	rewriteStack[rewriteStack.size() - 2].d_builder << rewriteStackTop.d_node;
422	32308586	rewriteStack.pop_back();
423	64617174	}
424
425		Unreachable();
426		} /* Rewriter::rewriteTo() */
427
428	12521187	RewriteResponse Rewriter::preRewrite(theory::TheoryId theoryId,
429		TNode n,
430		TConvProofGenerator* tcpg)
431		{
432	12521187	Kind k = n.getKind();
433		std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
434	25042374	(k == kind::EQUAL) ? d_preRewritersEqual[theoryId] : d_preRewriters[k];
435	12521187	if (fn == nullptr)
436		{
437	12521187	if (tcpg != nullptr)
438		{
439		// call the trust rewrite response interface
440		TrustRewriteResponse tresponse =
441	935458	d_theoryRewriters[theoryId]->preRewriteWithProof(n);
442		// process the trust rewrite response: store the proof step into
443		// tcpg if necessary and then convert to rewrite response.
444	467729	return processTrustRewriteResponse(theoryId, tresponse, true, tcpg);
445		}
446	12053458	return d_theoryRewriters[theoryId]->preRewrite(n);
447		}
448		return fn(&d_re, n);
449		}
450
451	11224503	RewriteResponse Rewriter::postRewrite(theory::TheoryId theoryId,
452		TNode n,
453		TConvProofGenerator* tcpg)
454		{
455	11224503	Kind k = n.getKind();
456		std::function<RewriteResponse(RewriteEnvironment*, TNode)> fn =
457	22449006	(k == kind::EQUAL) ? d_postRewritersEqual[theoryId] : d_postRewriters[k];
458	11224503	if (fn == nullptr)
459		{
460	11224503	if (tcpg != nullptr)
461		{
462		// same as above, for post-rewrite
463		TrustRewriteResponse tresponse =
464	702292	d_theoryRewriters[theoryId]->postRewriteWithProof(n);
465	351146	return processTrustRewriteResponse(theoryId, tresponse, false, tcpg);
466		}
467	10873359	return d_theoryRewriters[theoryId]->postRewrite(n);
468		}
469		return fn(&d_re, n);
470		}
471
472	818875	RewriteResponse Rewriter::processTrustRewriteResponse(
473		theory::TheoryId theoryId,
474		const TrustRewriteResponse& tresponse,
475		bool isPre,
476		TConvProofGenerator* tcpg)
477		{
478	818875	Assert(tcpg != nullptr);
479	1637750	TrustNode trn = tresponse.d_node;
480	818875	Assert(trn.getKind() == TrustNodeKind::REWRITE);
481	1637750	Node proven = trn.getProven();
482	818875	if (proven[0] != proven[1])
483		{
484	183310	ProofGenerator* pg = trn.getGenerator();
485	183310	if (pg == nullptr)
486		{
487	366620	Node tidn = builtin::BuiltinProofRuleChecker::mkTheoryIdNode(theoryId);
488		// add small step trusted rewrite
489		Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE
490	366620	: MethodId::RW_REWRITE_THEORY_POST);
491	733240	tcpg->addRewriteStep(proven[0],
492		proven[1],
493		PfRule::THEORY_REWRITE,
494		{},
495		{proven, tidn, rid},
496	549930	isPre);
497		}
498		else
499		{
500		// store proven rewrite step
501		tcpg->addRewriteStep(proven[0], proven[1], pg, isPre);
502		}
503		}
504	1637750	return RewriteResponse(tresponse.d_status, trn.getNode());
505		}
506
507		void Rewriter::clearCaches() {
508		Rewriter* rewriter = getInstance();
509
510		#ifdef CVC5_ASSERTIONS
511		rewriter->d_rewriteStack.reset(nullptr);
512		#endif
513
514		rewriter->clearCachesInternal();
515		}
516
517		} // namespace theory
518	28191	} // namespace cvc5