Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_preprocessor.cpp	Lines:	208	216	96.3 %
Date:	2021-11-06	Branches:	410	902	45.5 %


/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Dejan Jovanovic, Morgan Deters
 *
 * This file is part of the cvc5 project.
 *
 * Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
 * in the top-level source directory and their institutional affiliations.
 * All rights reserved.  See the file COPYING in the top-level source
 * directory for licensing information.
 * ****************************************************************************
 *
 * The theory preprocessor.
 */

#include "theory/theory_preprocessor.h"

#include "expr/skolem_manager.h"
#include "expr/term_context_stack.h"
#include "proof/lazy_proof.h"
#include "smt/logic_exception.h"
#include "theory/logic_info.h"
#include "theory/rewriter.h"
#include "theory/theory_engine.h"

using namespace std;

namespace cvc5 {
namespace theory {

TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine)
    : EnvObj(env),
      d_engine(engine),
      d_cache(userContext()),
      d_tfr(env),
      d_tpg(nullptr),
      d_tpgRew(nullptr),
      d_tspg(nullptr),
      d_lp(nullptr)
{
  // proofs are enabled in the theory preprocessor regardless of the proof mode
  ProofNodeManager* pnm = env.getProofNodeManager();
  if (pnm != nullptr)
  {
    context::Context* u = userContext();
    d_tpg.reset(
        new TConvProofGenerator(pnm,
                                u,
                                TConvPolicy::FIXPOINT,
                                TConvCachePolicy::NEVER,
                                "TheoryPreprocessor::preprocess_rewrite",
                                &d_rtfc));
    d_tpgRew.reset(new TConvProofGenerator(pnm,
                                           u,
                                           TConvPolicy::ONCE,
                                           TConvCachePolicy::NEVER,
                                           "TheoryPreprocessor::pprew"));
    d_lp.reset(
        new LazyCDProof(pnm, nullptr, u, "TheoryPreprocessor::LazyCDProof"));
    // Make the main term conversion sequence generator, which tracks up to
    // three conversions made in succession:
    // (1) rewriting
    // (2) (theory preprocessing+rewriting until fixed point)+term formula
    // removal+rewriting.
    std::vector<ProofGenerator*> ts;
    ts.push_back(d_tpgRew.get());
    ts.push_back(d_tpg.get());
    d_tspg.reset(new TConvSeqProofGenerator(
        pnm, ts, userContext(), "TheoryPreprocessor::sequence"));
  }
}

TheoryPreprocessor::~TheoryPreprocessor() {}

TrustNode TheoryPreprocessor::preprocess(TNode node,
                                         std::vector<SkolemLemma>& newLemmas)
{
  return preprocessInternal(node, newLemmas, true);
}

TrustNode TheoryPreprocessor::preprocessInternal(
    TNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
{
  // In this method, all rewriting steps of node are stored in d_tpg.

  Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl;

  // We must rewrite before preprocessing, because some terms when rewritten
  // may introduce new terms that are not top-level and require preprocessing.
  // An example of this is (forall ((x Int)) (and (tail L) (P x))) which
  // rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L)
  // must be preprocessed as a child here.
  Node irNode = rewriteWithProof(node, d_tpgRew.get(), true, 0);

  // run theory preprocessing
  TrustNode tpp = theoryPreprocess(irNode, newLemmas);
  Node ppNode = tpp.getNode();

  if (Trace.isOn("tpp-debug"))
  {
    if (node != irNode)
    {
      Trace("tpp-debug") << "after initial rewriting : " << irNode << std::endl;
    }
    if (irNode != ppNode)
    {
      Trace("tpp-debug")
          << "after preprocessing + rewriting and term formula removal : "
          << ppNode << std::endl;
    }
    Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
  }

  if (procLemmas)
  {
    // Also must preprocess the new lemmas. This is especially important for
    // formulas containing witness terms whose bodies are not in preprocessed
    // form, as term formula removal introduces new lemmas for these that
    // require theory-preprocessing.
    size_t i = 0;
    while (i < newLemmas.size())
    {
      TrustNode cur = newLemmas[i].d_lemma;
      newLemmas[i].d_lemma = preprocessLemmaInternal(cur, newLemmas, false);
      Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
      i++;
    }
  }

  if (node == ppNode)
  {
    Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
                       << std::endl;
    // no change
    return TrustNode::null();
  }

  // Now, sequence the conversion steps if proofs are enabled.
  TrustNode tret;
  if (isProofEnabled())
  {
    std::vector<Node> cterms;
    cterms.push_back(node);
    cterms.push_back(irNode);
    cterms.push_back(ppNode);
    // We have that:
    // node -> irNode via rewriting
    // irNode -> ppNode via theory-preprocessing + rewriting + tf removal
    tret = d_tspg->mkTrustRewriteSequence(cterms);
    tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
  }
  else
  {
    tret = TrustNode::mkTrustRewrite(node, ppNode, nullptr);
  }

  Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
                     << tret.getNode() << std::endl;
  Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode()
               << ", procLemmas=" << procLemmas
               << ", # lemmas = " << newLemmas.size() << std::endl;
  return tret;
}

TrustNode TheoryPreprocessor::preprocessLemma(
    TrustNode node, std::vector<SkolemLemma>& newLemmas)
{
  return preprocessLemmaInternal(node, newLemmas, true);
}

TrustNode TheoryPreprocessor::preprocessLemmaInternal(
    TrustNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
{
  // what was originally proven
  Node lemma = node.getProven();
  TrustNode tplemma = preprocessInternal(lemma, newLemmas, procLemmas);
  if (tplemma.isNull())
  {
    // no change needed
    return node;
  }
  Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
  // what it was preprocessed to
  Node lemmap = tplemma.getNode();
  Assert(lemmap != node.getProven());
  // process the preprocessing
  if (isProofEnabled())
  {
    Assert(d_lp != nullptr);
    // add the original proof to the lazy proof
    d_lp->addLazyStep(
        node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA);
    // only need to do anything if lemmap changed in a non-trivial way
    if (!CDProof::isSame(lemmap, lemma))
    {
      d_lp->addLazyStep(tplemma.getProven(),
                        tplemma.getGenerator(),
                        PfRule::THEORY_PREPROCESS,
                        true,
                        "TheoryEngine::lemma_pp");
      // ---------- from node -------------- from theory preprocess
      // lemma                lemma = lemmap
      // ------------------------------------------ EQ_RESOLVE
      // lemmap
      std::vector<Node> pfChildren;
      pfChildren.push_back(lemma);
      pfChildren.push_back(tplemma.getProven());
      d_lp->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
    }
  }
  return TrustNode::mkTrustLemma(lemmap, d_lp.get());
}

RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
{
  return d_tfr;
}

TrustNode TheoryPreprocessor::theoryPreprocess(
    TNode assertion, std::vector<SkolemLemma>& newLemmas)
{
  // Map from (term, term context identifier) to the term that it was
  // theory-preprocessed to. This is used when the result of the current node
  // should be set to the final result of converting its theory-preprocessed
  // form.
  std::unordered_map<std::pair<Node, uint32_t>,
                     Node,
                     PairHashFunction<Node, uint32_t, std::hash<Node>>>
      wasPreprocessed;
  std::unordered_map<
      std::pair<Node, uint32_t>,
      Node,
      PairHashFunction<Node, uint32_t, std::hash<Node>>>::iterator itw;
  NodeManager* nm = NodeManager::currentNM();
  TCtxStack ctx(&d_rtfc);
  std::vector<bool> processedChildren;
  ctx.pushInitial(assertion);
  processedChildren.push_back(false);
  std::pair<Node, uint32_t> initial = ctx.getCurrent();
  std::pair<Node, uint32_t> curr;
  Node node;
  uint32_t nodeVal;
  TppCache::const_iterator itc;
  while (!ctx.empty())
  {
    curr = ctx.getCurrent();
    itc = d_cache.find(curr);
    node = curr.first;
    nodeVal = curr.second;
    Trace("tpp-debug") << "Visit " << node << ", " << nodeVal << std::endl;
    if (itc != d_cache.end())
    {
      Trace("tpp-debug") << "...already computed" << std::endl;
      ctx.pop();
      processedChildren.pop_back();
      // already computed
      continue;
    }
    // if we have yet to process children
    if (!processedChildren.back())
    {
      // check if we should replace the current node by a Skolem
      TrustNode newLem;
      bool inQuant, inTerm;
      RtfTermContext::getFlags(nodeVal, inQuant, inTerm);
      Assert(!inQuant);
      TrustNode currTrn = d_tfr.runCurrent(node, inTerm, newLem);
      // if we replaced by a skolem, we do not recurse
      if (!currTrn.isNull())
      {
        Node ret = currTrn.getNode();
        // if this is the first time we've seen this term, we have a new lemma
        // which we add to our vectors
        if (!newLem.isNull())
        {
          newLemmas.push_back(theory::SkolemLemma(newLem, ret));
        }
        // register the rewrite into the proof generator
        if (isProofEnabled())
        {
          registerTrustedRewrite(currTrn, d_tpg.get(), true, nodeVal);
        }
        Trace("tpp-debug") << "...replace by skolem" << std::endl;
        d_cache.insert(curr, ret);
        continue;
      }
      size_t nchild = node.getNumChildren();
      if (nchild > 0)
      {
        if (node.isClosure())
        {
          // currently, we never do any term formula removal in quantifier
          // bodies
        }
        else
        {
          Trace("tpp-debug") << "...recurse to children" << std::endl;
          // recurse if we have children
          processedChildren[processedChildren.size() - 1] = true;
          for (size_t i = 0; i < nchild; i++)
          {
            ctx.pushChild(node, nodeVal, i);
            processedChildren.push_back(false);
          }
          continue;
        }
      }
      else
      {
        Trace("tpp-debug") << "...base case" << std::endl;
      }
    }
    Trace("tpp-debug") << "...reconstruct" << std::endl;
    // otherwise, we are now finished processing children, pop the current node
    // and compute the result
    ctx.pop();
    processedChildren.pop_back();
    // if this was preprocessed previously, we set our result to the final
    // form of the preprocessed form of this.
    itw = wasPreprocessed.find(curr);
    if (itw != wasPreprocessed.end())
    {
      // we preprocessed it to something else, carry that
      std::pair<Node, uint32_t> key(itw->second, nodeVal);
      itc = d_cache.find(key);
      Assert(itc != d_cache.end());
      d_cache.insert(curr, itc->second);
      wasPreprocessed.erase(curr);
      continue;
    }
    Node ret = node;
    Node pret = node;
    if (!node.isClosure() && node.getNumChildren() > 0)
    {
      // if we have not already computed the result
      std::vector<Node> newChildren;
      bool childChanged = false;
      if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        newChildren.push_back(node.getOperator());
      }
      // reconstruct from the children
      std::pair<Node, uint32_t> currChild;
      for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
      {
        // recompute the value of the child
        uint32_t val = d_rtfc.computeValue(node, nodeVal, i);
        currChild = std::pair<Node, uint32_t>(node[i], val);
        itc = d_cache.find(currChild);
        Assert(itc != d_cache.end());
        Node newChild = (*itc).second;
        Assert(!newChild.isNull());
        childChanged |= (newChild != node[i]);
        newChildren.push_back(newChild);
      }
      // If changes, we reconstruct the node
      if (childChanged)
      {
        ret = nm->mkNode(node.getKind(), newChildren);
      }
      // Finish the conversion by rewriting. Notice that we must consider this a
      // pre-rewrite since we do not recursively register the rewriting steps
      // of subterms of rtfNode. For example, if this step rewrites
      // (not A) ---> B, then if registered a pre-rewrite, it will apply when
      // reconstructing proofs via d_tpg. However, if it is a post-rewrite
      // it will fail to apply if another call to this class registers A -> C,
      // in which case (not C) will be returned instead of B (see issue 6754).
      pret = rewriteWithProof(ret, d_tpg.get(), false, nodeVal);
    }
    // if we did not rewrite above, we are ready to theory preprocess
    if (pret == ret)
    {
      pret = preprocessWithProof(ret, newLemmas, nodeVal);
    }
    // if we changed due to rewriting or preprocessing, we traverse again
    if (pret != ret)
    {
      // must restart
      ctx.push(node, nodeVal);
      processedChildren.push_back(true);
      ctx.push(pret, nodeVal);
      processedChildren.push_back(false);
      wasPreprocessed[curr] = pret;
      continue;
    }
    // cache
    d_cache.insert(curr, ret);
  }
  itc = d_cache.find(initial);
  Assert(itc != d_cache.end());
  return TrustNode::mkTrustRewrite(assertion, (*itc).second, d_tpg.get());
}

Node TheoryPreprocessor::rewriteWithProof(Node term,
                                          TConvProofGenerator* pg,
                                          bool isPre,
                                          uint32_t tctx)
{
  Node termr = rewrite(term);
  // store rewrite step if tracking proofs and it rewrites
  if (isProofEnabled())
  {
    // may rewrite the same term more than once, thus check hasRewriteStep
    if (termr != term)
    {
      Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
                         << term << " -> " << termr << std::endl;
      pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre, tctx);
    }
  }
  return termr;
}

Node TheoryPreprocessor::preprocessWithProof(Node term,
                                             std::vector<SkolemLemma>& lems,
                                             uint32_t tctx)
{
  // Important that it is in rewritten form, to ensure that the rewrite steps
  // recorded in d_tpg are functional. In other words, there should not
  // be steps from the same term to multiple rewritten forms, which would be
  // the case if we registered a preprocessing step for a non-rewritten term.
  Assert(term == rewrite(term));
  Trace("tpp-debug2") << "preprocessWithProof " << term
                      << ", #lems = " << lems.size() << std::endl;
  // We never call ppRewrite on equalities here, since equalities have a
  // special status. In particular, notice that theory preprocessing can be
  // called on all formulas asserted to theory engine, including those generated
  // as new literals appearing in lemmas. Calling ppRewrite on equalities is
  // incompatible with theory combination where a split on equality requested
  // by a theory could be preprocessed to something else, thus making theory
  // combination either non-terminating or result in solution soundness.
  // Notice that an alternative solution is to ensure that certain lemmas
  // (e.g. splits from theory combination) can never have theory preprocessing
  // applied to them. However, it is more uniform to say that theory
  // preprocessing is applied to all formulas. This makes it so that e.g.
  // theory solvers do not need to specify whether they want their lemmas to
  // be theory-preprocessed or not.
  if (term.getKind() == kind::EQUAL)
  {
    return term;
  }
  // call ppRewrite for the given theory
  TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems);
  Trace("tpp-debug2") << "preprocessWithProof returned " << trn
                      << ", #lems = " << lems.size() << std::endl;
  if (trn.isNull())
  {
    // no change, return
    return term;
  }
  Node termr = trn.getNode();
  Assert(term != termr);
  if (isProofEnabled())
  {
    registerTrustedRewrite(trn, d_tpg.get(), false, tctx);
  }
  // Rewrite again here, which notice is a *pre* rewrite.
  return rewriteWithProof(termr, d_tpg.get(), true, tctx);
}

bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }

void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
                                                TConvProofGenerator* pg,
                                                bool isPre,
                                                uint32_t tctx)
{
  if (!isProofEnabled() || trn.isNull())
  {
    return;
  }
  Assert(trn.getKind() == TrustNodeKind::REWRITE);
  Node eq = trn.getProven();
  Node term = eq[0];
  Node termr = eq[1];
  if (trn.getGenerator() != nullptr)
  {
    Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
                       << term << " -> " << termr << std::endl;
    trn.debugCheckClosed("tpp-debug",
                         "TheoryPreprocessor::preprocessWithProof");
    // always use term context hash 0 (default)
    pg->addRewriteStep(
        term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true, tctx);
  }
  else
  {
    Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
                       << term << " -> " << termr << std::endl;
    // small step trust
    pg->addRewriteStep(term,
                       termr,
                       PfRule::THEORY_PREPROCESS,
                       {},
                       {term.eqNode(termr)},
                       isPre,
                       tctx);
  }
}

}  // namespace theory
}  // namespace cvc5


Generated by: GCOVR (Version 3.2)

Line	Exec	Source
1		/******************************************************************************
2		* Top contributors (to current version):
3		* Andrew Reynolds, Dejan Jovanovic, Morgan Deters
4		*
5		* This file is part of the cvc5 project.
6		*
7		* Copyright (c) 2009-2021 by the authors listed in the file AUTHORS
8		* in the top-level source directory and their institutional affiliations.
9		* All rights reserved. See the file COPYING in the top-level source
10		* directory for licensing information.
11		* ****************************************************************************
12		*
13		* The theory preprocessor.
14		*/
15
16		#include "theory/theory_preprocessor.h"
17
18		#include "expr/skolem_manager.h"
19		#include "expr/term_context_stack.h"
20		#include "proof/lazy_proof.h"
21		#include "smt/logic_exception.h"
22		#include "theory/logic_info.h"
23		#include "theory/rewriter.h"
24		#include "theory/theory_engine.h"
25
26		using namespace std;
27
28		namespace cvc5 {
29		namespace theory {
30
31	15339	TheoryPreprocessor::TheoryPreprocessor(Env& env, TheoryEngine& engine)
32		: EnvObj(env),
33		d_engine(engine),
34	15339	d_cache(userContext()),
35		d_tfr(env),
36		d_tpg(nullptr),
37		d_tpgRew(nullptr),
38		d_tspg(nullptr),
39	30678	d_lp(nullptr)
40		{
41		// proofs are enabled in the theory preprocessor regardless of the proof mode
42	15339	ProofNodeManager* pnm = env.getProofNodeManager();
43	15339	if (pnm != nullptr)
44		{
45	8003	context::Context* u = userContext();
46	16006	d_tpg.reset(
47		new TConvProofGenerator(pnm,
48		u,
49		TConvPolicy::FIXPOINT,
50		TConvCachePolicy::NEVER,
51		"TheoryPreprocessor::preprocess_rewrite",
52	8003	&d_rtfc));
53	16006	d_tpgRew.reset(new TConvProofGenerator(pnm,
54		u,
55		TConvPolicy::ONCE,
56		TConvCachePolicy::NEVER,
57	8003	"TheoryPreprocessor::pprew"));
58	16006	d_lp.reset(
59	8003	new LazyCDProof(pnm, nullptr, u, "TheoryPreprocessor::LazyCDProof"));
60		// Make the main term conversion sequence generator, which tracks up to
61		// three conversions made in succession:
62		// (1) rewriting
63		// (2) (theory preprocessing+rewriting until fixed point)+term formula
64		// removal+rewriting.
65	16006	std::vector<ProofGenerator*> ts;
66	8003	ts.push_back(d_tpgRew.get());
67	8003	ts.push_back(d_tpg.get());
68	24009	d_tspg.reset(new TConvSeqProofGenerator(
69	16006	pnm, ts, userContext(), "TheoryPreprocessor::sequence"));
70		}
71	15339	}
72
73	15334	TheoryPreprocessor::~TheoryPreprocessor() {}
74
75	370394	TrustNode TheoryPreprocessor::preprocess(TNode node,
76		std::vector<SkolemLemma>& newLemmas)
77		{
78	370394	return preprocessInternal(node, newLemmas, true);
79		}
80
81	915391	TrustNode TheoryPreprocessor::preprocessInternal(
82		TNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
83		{
84		// In this method, all rewriting steps of node are stored in d_tpg.
85
86	915391	Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl;
87
88		// We must rewrite before preprocessing, because some terms when rewritten
89		// may introduce new terms that are not top-level and require preprocessing.
90		// An example of this is (forall ((x Int)) (and (tail L) (P x))) which
91		// rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L)
92		// must be preprocessed as a child here.
93	1830782	Node irNode = rewriteWithProof(node, d_tpgRew.get(), true, 0);
94
95		// run theory preprocessing
96	1830782	TrustNode tpp = theoryPreprocess(irNode, newLemmas);
97	1830754	Node ppNode = tpp.getNode();
98
99	915377	if (Trace.isOn("tpp-debug"))
100		{
101		if (node != irNode)
102		{
103		Trace("tpp-debug") << "after initial rewriting : " << irNode << std::endl;
104		}
105		if (irNode != ppNode)
106		{
107		Trace("tpp-debug")
108		<< "after preprocessing + rewriting and term formula removal : "
109		<< ppNode << std::endl;
110		}
111		Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
112		}
113
114	915377	if (procLemmas)
115		{
116		// Also must preprocess the new lemmas. This is especially important for
117		// formulas containing witness terms whose bodies are not in preprocessed
118		// form, as term formula removal introduces new lemmas for these that
119		// require theory-preprocessing.
120	885939	size_t i = 0;
121	944815	while (i < newLemmas.size())
122		{
123	58876	TrustNode cur = newLemmas[i].d_lemma;
124	29438	newLemmas[i].d_lemma = preprocessLemmaInternal(cur, newLemmas, false);
125	29438	Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
126	29438	i++;
127		}
128		}
129
130	915377	if (node == ppNode)
131		{
132	1454520	Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
133	727260	<< std::endl;
134		// no change
135	727260	return TrustNode::null();
136		}
137
138		// Now, sequence the conversion steps if proofs are enabled.
139	376234	TrustNode tret;
140	188117	if (isProofEnabled())
141		{
142	150494	std::vector<Node> cterms;
143	75247	cterms.push_back(node);
144	75247	cterms.push_back(irNode);
145	75247	cterms.push_back(ppNode);
146		// We have that:
147		// node -> irNode via rewriting
148		// irNode -> ppNode via theory-preprocessing + rewriting + tf removal
149	75247	tret = d_tspg->mkTrustRewriteSequence(cterms);
150	75247	tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
151		}
152		else
153		{
154	112870	tret = TrustNode::mkTrustRewrite(node, ppNode, nullptr);
155		}
156
157	376234	Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
158	188117	<< tret.getNode() << std::endl;
159	376234	Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode()
160	188117	<< ", procLemmas=" << procLemmas
161	188117	<< ", # lemmas = " << newLemmas.size() << std::endl;
162	188117	return tret;
163		}
164
165	515559	TrustNode TheoryPreprocessor::preprocessLemma(
166		TrustNode node, std::vector<SkolemLemma>& newLemmas)
167		{
168	515559	return preprocessLemmaInternal(node, newLemmas, true);
169		}
170
171	544997	TrustNode TheoryPreprocessor::preprocessLemmaInternal(
172		TrustNode node, std::vector<SkolemLemma>& newLemmas, bool procLemmas)
173		{
174		// what was originally proven
175	1089994	Node lemma = node.getProven();
176	1089994	TrustNode tplemma = preprocessInternal(lemma, newLemmas, procLemmas);
177	544995	if (tplemma.isNull())
178		{
179		// no change needed
180	399077	return node;
181		}
182	145918	Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
183		// what it was preprocessed to
184	291836	Node lemmap = tplemma.getNode();
185	145918	Assert(lemmap != node.getProven());
186		// process the preprocessing
187	145918	if (isProofEnabled())
188		{
189	56146	Assert(d_lp != nullptr);
190		// add the original proof to the lazy proof
191	112292	d_lp->addLazyStep(
192	112292	node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA);
193		// only need to do anything if lemmap changed in a non-trivial way
194	56146	if (!CDProof::isSame(lemmap, lemma))
195		{
196	51852	d_lp->addLazyStep(tplemma.getProven(),
197		tplemma.getGenerator(),
198		PfRule::THEORY_PREPROCESS,
199		true,
200		"TheoryEngine::lemma_pp");
201		// ---------- from node -------------- from theory preprocess
202		// lemma lemma = lemmap
203		// ------------------------------------------ EQ_RESOLVE
204		// lemmap
205	103704	std::vector<Node> pfChildren;
206	51852	pfChildren.push_back(lemma);
207	51852	pfChildren.push_back(tplemma.getProven());
208	51852	d_lp->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
209		}
210		}
211	145918	return TrustNode::mkTrustLemma(lemmap, d_lp.get());
212		}
213
214	2	RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
215		{
216	2	return d_tfr;
217		}
218
219	915391	TrustNode TheoryPreprocessor::theoryPreprocess(
220		TNode assertion, std::vector<SkolemLemma>& newLemmas)
221		{
222		// Map from (term, term context identifier) to the term that it was
223		// theory-preprocessed to. This is used when the result of the current node
224		// should be set to the final result of converting its theory-preprocessed
225		// form.
226		std::unordered_map<std::pair<Node, uint32_t>,
227		Node,
228		PairHashFunction<Node, uint32_t, std::hash<Node>>>
229	1830782	wasPreprocessed;
230		std::unordered_map<
231		std::pair<Node, uint32_t>,
232		Node,
233	915391	PairHashFunction<Node, uint32_t, std::hash<Node>>>::iterator itw;
234	915391	NodeManager* nm = NodeManager::currentNM();
235	1830782	TCtxStack ctx(&d_rtfc);
236	1830782	std::vector<bool> processedChildren;
237	915391	ctx.pushInitial(assertion);
238	915391	processedChildren.push_back(false);
239	1830782	std::pair<Node, uint32_t> initial = ctx.getCurrent();
240	1830782	std::pair<Node, uint32_t> curr;
241	1830782	Node node;
242		uint32_t nodeVal;
243	915391	TppCache::const_iterator itc;
244	24066727	while (!ctx.empty())
245		{
246	11575682	curr = ctx.getCurrent();
247	11575682	itc = d_cache.find(curr);
248	11575682	node = curr.first;
249	11575682	nodeVal = curr.second;
250	11575682	Trace("tpp-debug") << "Visit " << node << ", " << nodeVal << std::endl;
251	17077001	if (itc != d_cache.end())
252		{
253	5501319	Trace("tpp-debug") << "...already computed" << std::endl;
254	5501319	ctx.pop();
255	5501319	processedChildren.pop_back();
256		// already computed
257	13916856	continue;
258		}
259		// if we have yet to process children
260	6074363	if (!processedChildren.back())
261		{
262		// check if we should replace the current node by a Skolem
263	3565912	TrustNode newLem;
264		bool inQuant, inTerm;
265	3216159	RtfTermContext::getFlags(nodeVal, inQuant, inTerm);
266	3216159	Assert(!inQuant);
267	3565912	TrustNode currTrn = d_tfr.runCurrent(node, inTerm, newLem);
268		// if we replaced by a skolem, we do not recurse
269	3216157	if (!currTrn.isNull())
270		{
271	64158	Node ret = currTrn.getNode();
272		// if this is the first time we've seen this term, we have a new lemma
273		// which we add to our vectors
274	32079	if (!newLem.isNull())
275		{
276	27505	newLemmas.push_back(theory::SkolemLemma(newLem, ret));
277		}
278		// register the rewrite into the proof generator
279	32079	if (isProofEnabled())
280		{
281	16211	registerTrustedRewrite(currTrn, d_tpg.get(), true, nodeVal);
282		}
283	32079	Trace("tpp-debug") << "...replace by skolem" << std::endl;
284	32079	d_cache.insert(curr, ret);
285	32079	continue;
286		}
287	3184078	size_t nchild = node.getNumChildren();
288	3184078	if (nchild > 0)
289		{
290	2862353	if (node.isClosure())
291		{
292		// currently, we never do any term formula removal in quantifier
293		// bodies
294		}
295		else
296		{
297	2834327	Trace("tpp-debug") << "...recurse to children" << std::endl;
298		// recurse if we have children
299	2834327	processedChildren[processedChildren.size() - 1] = true;
300	10580453	for (size_t i = 0; i < nchild; i++)
301		{
302	7746126	ctx.pushChild(node, nodeVal, i);
303	7746126	processedChildren.push_back(false);
304		}
305	2834327	continue;
306		}
307		}
308		else
309		{
310	321725	Trace("tpp-debug") << "...base case" << std::endl;
311		}
312		}
313	3207955	Trace("tpp-debug") << "...reconstruct" << std::endl;
314		// otherwise, we are now finished processing children, pop the current node
315		// and compute the result
316	3207955	ctx.pop();
317	3207955	processedChildren.pop_back();
318		// if this was preprocessed previously, we set our result to the final
319		// form of the preprocessed form of this.
320	3207955	itw = wasPreprocessed.find(curr);
321	3207955	if (itw != wasPreprocessed.end())
322		{
323		// we preprocessed it to something else, carry that
324	47812	std::pair<Node, uint32_t> key(itw->second, nodeVal);
325	23906	itc = d_cache.find(key);
326	23906	Assert(itc != d_cache.end());
327	23906	d_cache.insert(curr, itc->second);
328	23906	wasPreprocessed.erase(curr);
329	23906	continue;
330		}
331	6344192	Node ret = node;
332	6344192	Node pret = node;
333	3184049	if (!node.isClosure() && node.getNumChildren() > 0)
334		{
335		// if we have not already computed the result
336	5668596	std::vector<Node> newChildren;
337	2834298	bool childChanged = false;
338	2834298	if (node.getMetaKind() == kind::metakind::PARAMETERIZED)
339		{
340	231868	newChildren.push_back(node.getOperator());
341		}
342		// reconstruct from the children
343	5668596	std::pair<Node, uint32_t> currChild;
344	10580365	for (size_t i = 0, nchild = node.getNumChildren(); i < nchild; i++)
345		{
346		// recompute the value of the child
347	7746067	uint32_t val = d_rtfc.computeValue(node, nodeVal, i);
348	7746067	currChild = std::pair<Node, uint32_t>(node[i], val);
349	7746067	itc = d_cache.find(currChild);
350	7746067	Assert(itc != d_cache.end());
351	15492134	Node newChild = (*itc).second;
352	7746067	Assert(!newChild.isNull());
353	7746067	childChanged \|= (newChild != node[i]);
354	7746067	newChildren.push_back(newChild);
355		}
356		// If changes, we reconstruct the node
357	2834298	if (childChanged)
358		{
359	194526	ret = nm->mkNode(node.getKind(), newChildren);
360		}
361		// Finish the conversion by rewriting. Notice that we must consider this a
362		// pre-rewrite since we do not recursively register the rewriting steps
363		// of subterms of rtfNode. For example, if this step rewrites
364		// (not A) ---> B, then if registered a pre-rewrite, it will apply when
365		// reconstructing proofs via d_tpg. However, if it is a post-rewrite
366		// it will fail to apply if another call to this class registers A -> C,
367		// in which case (not C) will be returned instead of B (see issue 6754).
368	2834298	pret = rewriteWithProof(ret, d_tpg.get(), false, nodeVal);
369		}
370		// if we did not rewrite above, we are ready to theory preprocess
371	3184049	if (pret == ret)
372		{
373	3167728	pret = preprocessWithProof(ret, newLemmas, nodeVal);
374		}
375		// if we changed due to rewriting or preprocessing, we traverse again
376	3207943	if (pret != ret)
377		{
378		// must restart
379	23906	ctx.push(node, nodeVal);
380	23906	processedChildren.push_back(true);
381	23906	ctx.push(pret, nodeVal);
382	23906	processedChildren.push_back(false);
383	23906	wasPreprocessed[curr] = pret;
384	23906	continue;
385		}
386		// cache
387	3160131	d_cache.insert(curr, ret);
388		}
389	915377	itc = d_cache.find(initial);
390	915377	Assert(itc != d_cache.end());
391	1830754	return TrustNode::mkTrustRewrite(assertion, (*itc).second, d_tpg.get());
392		}
393
394	3757274	Node TheoryPreprocessor::rewriteWithProof(Node term,
395		TConvProofGenerator* pg,
396		bool isPre,
397		uint32_t tctx)
398		{
399	3757274	Node termr = rewrite(term);
400		// store rewrite step if tracking proofs and it rewrites
401	3757274	if (isProofEnabled())
402		{
403		// may rewrite the same term more than once, thus check hasRewriteStep
404	1853498	if (termr != term)
405		{
406	144134	Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
407	72067	<< term << " -> " << termr << std::endl;
408	72067	pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre, tctx);
409		}
410		}
411	3757274	return termr;
412		}
413
414	3167728	Node TheoryPreprocessor::preprocessWithProof(Node term,
415		std::vector<SkolemLemma>& lems,
416		uint32_t tctx)
417		{
418		// Important that it is in rewritten form, to ensure that the rewrite steps
419		// recorded in d_tpg are functional. In other words, there should not
420		// be steps from the same term to multiple rewritten forms, which would be
421		// the case if we registered a preprocessing step for a non-rewritten term.
422	3167728	Assert(term == rewrite(term));
423	6335456	Trace("tpp-debug2") << "preprocessWithProof " << term
424	3167728	<< ", #lems = " << lems.size() << std::endl;
425		// We never call ppRewrite on equalities here, since equalities have a
426		// special status. In particular, notice that theory preprocessing can be
427		// called on all formulas asserted to theory engine, including those generated
428		// as new literals appearing in lemmas. Calling ppRewrite on equalities is
429		// incompatible with theory combination where a split on equality requested
430		// by a theory could be preprocessed to something else, thus making theory
431		// combination either non-terminating or result in solution soundness.
432		// Notice that an alternative solution is to ensure that certain lemmas
433		// (e.g. splits from theory combination) can never have theory preprocessing
434		// applied to them. However, it is more uniform to say that theory
435		// preprocessing is applied to all formulas. This makes it so that e.g.
436		// theory solvers do not need to specify whether they want their lemmas to
437		// be theory-preprocessed or not.
438	3167728	if (term.getKind() == kind::EQUAL)
439		{
440	454798	return term;
441		}
442		// call ppRewrite for the given theory
443	5425860	TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems);
444	5425836	Trace("tpp-debug2") << "preprocessWithProof returned " << trn
445	2712918	<< ", #lems = " << lems.size() << std::endl;
446	2712918	if (trn.isNull())
447		{
448		// no change, return
449	2705333	return term;
450		}
451	15170	Node termr = trn.getNode();
452	7585	Assert(term != termr);
453	7585	if (isProofEnabled())
454		{
455	4074	registerTrustedRewrite(trn, d_tpg.get(), false, tctx);
456		}
457		// Rewrite again here, which notice is a pre rewrite.
458	7585	return rewriteWithProof(termr, d_tpg.get(), true, tctx);
459		}
460
461	4151258	bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
462
463	20285	void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
464		TConvProofGenerator* pg,
465		bool isPre,
466		uint32_t tctx)
467		{
468	20285	if (!isProofEnabled() \|\| trn.isNull())
469		{
470		return;
471		}
472	20285	Assert(trn.getKind() == TrustNodeKind::REWRITE);
473	40570	Node eq = trn.getProven();
474	40570	Node term = eq[0];
475	40570	Node termr = eq[1];
476	20285	if (trn.getGenerator() != nullptr)
477		{
478	32436	Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
479	16218	<< term << " -> " << termr << std::endl;
480	16218	trn.debugCheckClosed("tpp-debug",
481		"TheoryPreprocessor::preprocessWithProof");
482		// always use term context hash 0 (default)
483	16218	pg->addRewriteStep(
484		term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true, tctx);
485		}
486		else
487		{
488	8134	Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
489	4067	<< term << " -> " << termr << std::endl;
490		// small step trust
491	8134	pg->addRewriteStep(term,
492		termr,
493		PfRule::THEORY_PREPROCESS,
494		{},
495		{term.eqNode(termr)},
496		isPre,
497	4067	tctx);
498		}
499		}
500
501		} // namespace theory
502	31137	} // namespace cvc5