Head

GCC Code Coverage Report

Directory:	.		Exec	Total	Coverage
File:	src/theory/theory_preprocessor.cpp	Lines:	201	216	93.1 %
Date:	2021-05-21	Branches:	476	1054	45.2 %


/******************************************************************************
 * 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/lazy_proof.h"
#include "expr/skolem_manager.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(TheoryEngine& engine,
                                       context::UserContext* userContext,
                                       ProofNodeManager* pnm)
    : d_engine(engine),
      d_logicInfo(engine.getLogicInfo()),
      d_ppCache(userContext),
      d_rtfCache(userContext),
      d_tfr(userContext, pnm),
      d_tpg(pnm ? new TConvProofGenerator(
                      pnm,
                      userContext,
                      TConvPolicy::FIXPOINT,
                      TConvCachePolicy::NEVER,
                      "TheoryPreprocessor::preprocess_rewrite",
                      &d_iqtc)
                : nullptr),
      d_tpgRtf(pnm ? new TConvProofGenerator(pnm,
                                             userContext,
                                             TConvPolicy::FIXPOINT,
                                             TConvCachePolicy::NEVER,
                                             "TheoryPreprocessor::rtf",
                                             &d_iqtc)
                   : nullptr),
      d_tpgRew(pnm ? new TConvProofGenerator(pnm,
                                             userContext,
                                             TConvPolicy::ONCE,
                                             TConvCachePolicy::NEVER,
                                             "TheoryPreprocessor::pprew")
                   : nullptr),
      d_tspg(nullptr),
      d_lp(pnm ? new LazyCDProof(pnm,
                                 nullptr,
                                 userContext,
                                 "TheoryPreprocessor::LazyCDProof")
               : nullptr)
{
  if (isProofEnabled())
  {
    // 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_tpgRtf.get());
    d_tspg.reset(new TConvSeqProofGenerator(
        pnm, ts, userContext, "TheoryPreprocessor::sequence"));
  }
}

TheoryPreprocessor::~TheoryPreprocessor() {}

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

TrustNode TheoryPreprocessor::preprocessInternal(
    TNode node,
    std::vector<TrustNode>& newLemmas,
    std::vector<Node>& newSkolems,
    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);

  // run theory preprocessing
  TrustNode tpp = theoryPreprocess(irNode, newLemmas, newSkolems);
  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];
      newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, 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<TrustNode>& newLemmas,
                                              std::vector<Node>& newSkolems)
{
  return preprocessLemmaInternal(node, newLemmas, newSkolems, true);
}

TrustNode TheoryPreprocessor::preprocessLemmaInternal(
    TrustNode node,
    std::vector<TrustNode>& newLemmas,
    std::vector<Node>& newSkolems,
    bool procLemmas)
{
  // what was originally proven
  Node lemma = node.getProven();
  TrustNode tplemma =
      preprocessInternal(lemma, newLemmas, newSkolems, 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;
}

struct preprocess_stack_element
{
  TNode node;
  bool children_added;
  preprocess_stack_element(TNode n) : node(n), children_added(false) {}
};

TrustNode TheoryPreprocessor::theoryPreprocess(
    TNode assertion,
    std::vector<TrustNode>& newLemmas,
    std::vector<Node>& newSkolems)
{
  Trace("theory::preprocess")
      << "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
  // spendResource();

  // Do a topological sort of the subexpressions and substitute them
  vector<preprocess_stack_element> toVisit;
  toVisit.push_back(assertion);

  while (!toVisit.empty())
  {
    // The current node we are processing
    preprocess_stack_element& stackHead = toVisit.back();
    TNode current = stackHead.node;

    Trace("theory::preprocess-debug")
        << "TheoryPreprocessor::theoryPreprocess processing " << current
        << endl;

    // If node already in the cache we're done, pop from the stack
    if (d_rtfCache.find(current) != d_rtfCache.end())
    {
      toVisit.pop_back();
      continue;
    }

    TheoryId tid = Theory::theoryOf(current);

    if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
    {
      stringstream ss;
      ss << "The logic was specified as " << d_logicInfo.getLogicString()
         << ", which doesn't include " << tid
         << ", but got a preprocessing-time fact for that theory." << endl
         << "The fact:" << endl
         << current;
      throw LogicException(ss.str());
    }
    // If this is an atom, we preprocess its terms with the theory ppRewriter
    if (tid != THEORY_BOOL)
    {
      std::vector<SkolemLemma> lems;
      Node ppRewritten = ppTheoryRewrite(current, lems);
      for (const SkolemLemma& lem : lems)
      {
        newLemmas.push_back(lem.d_lemma);
        newSkolems.push_back(lem.d_skolem);
      }
      Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
      if (isProofEnabled() && ppRewritten != current)
      {
        TrustNode trn =
            TrustNode::mkTrustRewrite(current, ppRewritten, d_tpg.get());
        registerTrustedRewrite(trn, d_tpgRtf.get(), true);
      }

      // Term formula removal without fixed point. We do not need to do fixed
      // point since newLemmas are theory-preprocessed until fixed point in
      // preprocessInternal (at top-level, when procLemmas=true).
      TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, newSkolems, false);
      Node rtfNode = ppRewritten;
      if (!ttfr.isNull())
      {
        rtfNode = ttfr.getNode();
        registerTrustedRewrite(ttfr, d_tpgRtf.get(), true);
      }
      // Finish the conversion by rewriting. This is registered as a
      // post-rewrite, since it is the last step applied for theory atoms.
      Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), false);
      d_rtfCache[current] = retNode;
      continue;
    }

    // Not yet substituted, so process
    if (stackHead.children_added)
    {
      // Children have been processed, so substitute
      NodeBuilder builder(current.getKind());
      if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
      {
        builder << current.getOperator();
      }
      for (unsigned i = 0; i < current.getNumChildren(); ++i)
      {
        Assert(d_rtfCache.find(current[i]) != d_rtfCache.end());
        builder << d_rtfCache[current[i]].get();
      }
      // Mark the substitution and continue
      Node result = builder;
      // always rewrite here, since current may not be in rewritten form after
      // reconstruction
      result = rewriteWithProof(result, d_tpgRtf.get(), false);
      Trace("theory::preprocess-debug")
          << "TheoryPreprocessor::theoryPreprocess setting " << current
          << " -> " << result << endl;
      d_rtfCache[current] = result;
      toVisit.pop_back();
    }
    else
    {
      // Mark that we have added the children if any
      if (current.getNumChildren() > 0)
      {
        stackHead.children_added = true;
        // We need to add the children
        for (TNode::iterator child_it = current.begin();
             child_it != current.end();
             ++child_it)
        {
          TNode childNode = *child_it;
          if (d_rtfCache.find(childNode) == d_rtfCache.end())
          {
            toVisit.push_back(childNode);
          }
        }
      }
      else
      {
        // No children, so we're done
        Trace("theory::preprocess-debug")
            << "SubstitutionMap::internalSubstitute setting " << current
            << " -> " << current << endl;
        d_rtfCache[current] = current;
        toVisit.pop_back();
      }
    }
  }
  Assert(d_rtfCache.find(assertion) != d_rtfCache.end());
  // Return the substituted version
  Node res = d_rtfCache[assertion];
  return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get());
}

// Recursively traverse a term and call the theory rewriter on its sub-terms
Node TheoryPreprocessor::ppTheoryRewrite(TNode term,
                                         std::vector<SkolemLemma>& lems)
{
  NodeMap::iterator find = d_ppCache.find(term);
  if (find != d_ppCache.end())
  {
    return (*find).second;
  }
  if (term.getNumChildren() == 0)
  {
    return preprocessWithProof(term, lems);
  }
  // should be in rewritten form here
  Assert(term == Rewriter::rewrite(term));
  Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
  // do not rewrite inside quantifiers
  Node newTerm = term;
  if (!term.isClosure())
  {
    NodeBuilder newNode(term.getKind());
    if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
    {
      newNode << term.getOperator();
    }
    for (const Node& nt : term)
    {
      newNode << ppTheoryRewrite(nt, lems);
    }
    newTerm = Node(newNode);
    newTerm = rewriteWithProof(newTerm, d_tpg.get(), false);
  }
  newTerm = preprocessWithProof(newTerm, lems);
  d_ppCache[term] = newTerm;
  Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
  return newTerm;
}

Node TheoryPreprocessor::rewriteWithProof(Node term,
                                          TConvProofGenerator* pg,
                                          bool isPre)
{
  Node termr = Rewriter::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;
      // always use term context hash 0 (default)
      pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre);
    }
  }
  return termr;
}

Node TheoryPreprocessor::preprocessWithProof(Node term,
                                             std::vector<SkolemLemma>& lems)
{
  // 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 == Rewriter::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);
  }
  // Rewrite again here, which notice is a *pre* rewrite.
  termr = rewriteWithProof(termr, d_tpg.get(), true);
  return ppTheoryRewrite(termr, lems);
}

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

void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
                                                TConvProofGenerator* pg,
                                                bool isPre)
{
  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);
  }
  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);
  }
}

}  // 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/lazy_proof.h"
19		#include "expr/skolem_manager.h"
20		#include "smt/logic_exception.h"
21		#include "theory/logic_info.h"
22		#include "theory/rewriter.h"
23		#include "theory/theory_engine.h"
24
25		using namespace std;
26
27		namespace cvc5 {
28		namespace theory {
29
30	8988	TheoryPreprocessor::TheoryPreprocessor(TheoryEngine& engine,
31		context::UserContext* userContext,
32	8988	ProofNodeManager* pnm)
33		: d_engine(engine),
34	8988	d_logicInfo(engine.getLogicInfo()),
35		d_ppCache(userContext),
36		d_rtfCache(userContext),
37		d_tfr(userContext, pnm),
38		d_tpg(pnm ? new TConvProofGenerator(
39		pnm,
40		userContext,
41		TConvPolicy::FIXPOINT,
42		TConvCachePolicy::NEVER,
43		"TheoryPreprocessor::preprocess_rewrite",
44	3130	&d_iqtc)
45		: nullptr),
46		d_tpgRtf(pnm ? new TConvProofGenerator(pnm,
47		userContext,
48		TConvPolicy::FIXPOINT,
49		TConvCachePolicy::NEVER,
50		"TheoryPreprocessor::rtf",
51	3130	&d_iqtc)
52		: nullptr),
53		d_tpgRew(pnm ? new TConvProofGenerator(pnm,
54		userContext,
55		TConvPolicy::ONCE,
56		TConvCachePolicy::NEVER,
57	3130	"TheoryPreprocessor::pprew")
58		: nullptr),
59		d_tspg(nullptr),
60		d_lp(pnm ? new LazyCDProof(pnm,
61		nullptr,
62		userContext,
63	3130	"TheoryPreprocessor::LazyCDProof")
64	30496	: nullptr)
65		{
66	8988	if (isProofEnabled())
67		{
68		// Make the main term conversion sequence generator, which tracks up to
69		// three conversions made in succession:
70		// (1) rewriting
71		// (2) (theory preprocessing+rewriting until fixed point)+term formula
72		// removal+rewriting.
73	6260	std::vector<ProofGenerator*> ts;
74	3130	ts.push_back(d_tpgRew.get());
75	3130	ts.push_back(d_tpgRtf.get());
76	6260	d_tspg.reset(new TConvSeqProofGenerator(
77	3130	pnm, ts, userContext, "TheoryPreprocessor::sequence"));
78		}
79	8988	}
80
81	8988	TheoryPreprocessor::~TheoryPreprocessor() {}
82
83	256634	TrustNode TheoryPreprocessor::preprocess(TNode node,
84		std::vector<TrustNode>& newLemmas,
85		std::vector<Node>& newSkolems)
86		{
87	256634	return preprocessInternal(node, newLemmas, newSkolems, true);
88		}
89
90	685289	TrustNode TheoryPreprocessor::preprocessInternal(
91		TNode node,
92		std::vector<TrustNode>& newLemmas,
93		std::vector<Node>& newSkolems,
94		bool procLemmas)
95		{
96		// In this method, all rewriting steps of node are stored in d_tpg.
97
98	685289	Trace("tpp") << "TheoryPreprocessor::preprocess: start " << node << std::endl;
99
100		// We must rewrite before preprocessing, because some terms when rewritten
101		// may introduce new terms that are not top-level and require preprocessing.
102		// An example of this is (forall ((x Int)) (and (tail L) (P x))) which
103		// rewrites to (and (tail L) (forall ((x Int)) (P x))). The subterm (tail L)
104		// must be preprocessed as a child here.
105	1370578	Node irNode = rewriteWithProof(node, d_tpgRew.get(), true);
106
107		// run theory preprocessing
108	1370578	TrustNode tpp = theoryPreprocess(irNode, newLemmas, newSkolems);
109	1370560	Node ppNode = tpp.getNode();
110
111	685280	if (Trace.isOn("tpp-debug"))
112		{
113		if (node != irNode)
114		{
115		Trace("tpp-debug") << "after initial rewriting : " << irNode << std::endl;
116		}
117		if (irNode != ppNode)
118		{
119		Trace("tpp-debug")
120		<< "after preprocessing + rewriting and term formula removal : "
121		<< ppNode << std::endl;
122		}
123		Trace("tpp-debug") << "TheoryPreprocessor::preprocess: finish" << std::endl;
124		}
125
126	685280	if (procLemmas)
127		{
128		// Also must preprocess the new lemmas. This is especially important for
129		// formulas containing witness terms whose bodies are not in preprocessed
130		// form, as term formula removal introduces new lemmas for these that
131		// require theory-preprocessing.
132	657415	size_t i = 0;
133	713145	while (i < newLemmas.size())
134		{
135	55730	TrustNode cur = newLemmas[i];
136	27865	newLemmas[i] = preprocessLemmaInternal(cur, newLemmas, newSkolems, false);
137	27865	Trace("tpp") << "Final lemma : " << newLemmas[i].getProven() << std::endl;
138	27865	i++;
139		}
140		}
141
142	685280	if (node == ppNode)
143		{
144	1040326	Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned no change"
145	520163	<< std::endl;
146		// no change
147	520163	return TrustNode::null();
148		}
149
150		// Now, sequence the conversion steps if proofs are enabled.
151	330234	TrustNode tret;
152	165117	if (isProofEnabled())
153		{
154	143354	std::vector<Node> cterms;
155	71677	cterms.push_back(node);
156	71677	cterms.push_back(irNode);
157	71677	cterms.push_back(ppNode);
158		// We have that:
159		// node -> irNode via rewriting
160		// irNode -> ppNode via theory-preprocessing + rewriting + tf removal
161	71677	tret = d_tspg->mkTrustRewriteSequence(cterms);
162	71677	tret.debugCheckClosed("tpp-debug", "TheoryPreprocessor::lemma_ret");
163		}
164		else
165		{
166	93440	tret = TrustNode::mkTrustRewrite(node, ppNode, nullptr);
167		}
168
169	330234	Trace("tpp-debug") << "...TheoryPreprocessor::preprocess returned "
170	165117	<< tret.getNode() << std::endl;
171	330234	Trace("tpp") << "TheoryPreprocessor::preprocess: return " << tret.getNode()
172	165117	<< ", procLemmas=" << procLemmas
173	165117	<< ", # lemmas = " << newLemmas.size() << std::endl;
174	165117	return tret;
175		}
176
177	400790	TrustNode TheoryPreprocessor::preprocessLemma(TrustNode node,
178		std::vector<TrustNode>& newLemmas,
179		std::vector<Node>& newSkolems)
180		{
181	400790	return preprocessLemmaInternal(node, newLemmas, newSkolems, true);
182		}
183
184	428655	TrustNode TheoryPreprocessor::preprocessLemmaInternal(
185		TrustNode node,
186		std::vector<TrustNode>& newLemmas,
187		std::vector<Node>& newSkolems,
188		bool procLemmas)
189		{
190		// what was originally proven
191	857310	Node lemma = node.getProven();
192		TrustNode tplemma =
193	857310	preprocessInternal(lemma, newLemmas, newSkolems, procLemmas);
194	428653	if (tplemma.isNull())
195		{
196		// no change needed
197	296220	return node;
198		}
199	132433	Assert(tplemma.getKind() == TrustNodeKind::REWRITE);
200		// what it was preprocessed to
201	264866	Node lemmap = tplemma.getNode();
202	132433	Assert(lemmap != node.getProven());
203		// process the preprocessing
204	132433	if (isProofEnabled())
205		{
206	54935	Assert(d_lp != nullptr);
207		// add the original proof to the lazy proof
208	109870	d_lp->addLazyStep(
209	109870	node.getProven(), node.getGenerator(), PfRule::THEORY_PREPROCESS_LEMMA);
210		// only need to do anything if lemmap changed in a non-trivial way
211	54935	if (!CDProof::isSame(lemmap, lemma))
212		{
213	51663	d_lp->addLazyStep(tplemma.getProven(),
214		tplemma.getGenerator(),
215		PfRule::THEORY_PREPROCESS,
216		true,
217		"TheoryEngine::lemma_pp");
218		// ---------- from node -------------- from theory preprocess
219		// lemma lemma = lemmap
220		// ------------------------------------------ EQ_RESOLVE
221		// lemmap
222	103326	std::vector<Node> pfChildren;
223	51663	pfChildren.push_back(lemma);
224	51663	pfChildren.push_back(tplemma.getProven());
225	51663	d_lp->addStep(lemmap, PfRule::EQ_RESOLVE, pfChildren, {});
226		}
227		}
228	132433	return TrustNode::mkTrustLemma(lemmap, d_lp.get());
229		}
230
231	4	RemoveTermFormulas& TheoryPreprocessor::getRemoveTermFormulas()
232		{
233	4	return d_tfr;
234		}
235
236	9479346	struct preprocess_stack_element
237		{
238		TNode node;
239		bool children_added;
240	2199474	preprocess_stack_element(TNode n) : node(n), children_added(false) {}
241		};
242
243	685289	TrustNode TheoryPreprocessor::theoryPreprocess(
244		TNode assertion,
245		std::vector<TrustNode>& newLemmas,
246		std::vector<Node>& newSkolems)
247		{
248	1370578	Trace("theory::preprocess")
249	685289	<< "TheoryPreprocessor::theoryPreprocess(" << assertion << ")" << endl;
250		// spendResource();
251
252		// Do a topological sort of the subexpressions and substitute them
253	1370578	vector<preprocess_stack_element> toVisit;
254	685289	toVisit.push_back(assertion);
255
256	8819667	while (!toVisit.empty())
257		{
258		// The current node we are processing
259	4067198	preprocess_stack_element& stackHead = toVisit.back();
260	6830487	TNode current = stackHead.node;
261
262	8134396	Trace("theory::preprocess-debug")
263	4067198	<< "TheoryPreprocessor::theoryPreprocess processing " << current
264	4067198	<< endl;
265
266		// If node already in the cache we're done, pop from the stack
267	4840462	if (d_rtfCache.find(current) != d_rtfCache.end())
268		{
269	773264	toVisit.pop_back();
270	773264	continue;
271		}
272
273	3293934	TheoryId tid = Theory::theoryOf(current);
274
275	3293934	if (!d_logicInfo.isTheoryEnabled(tid) && tid != THEORY_SAT_SOLVER)
276		{
277		stringstream ss;
278		ss << "The logic was specified as " << d_logicInfo.getLogicString()
279		<< ", which doesn't include " << tid
280		<< ", but got a preprocessing-time fact for that theory." << endl
281		<< "The fact:" << endl
282		<< current;
283		throw LogicException(ss.str());
284		}
285		// If this is an atom, we preprocess its terms with the theory ppRewriter
286	3293934	if (tid != THEORY_BOOL)
287		{
288	1061308	std::vector<SkolemLemma> lems;
289	1061308	Node ppRewritten = ppTheoryRewrite(current, lems);
290	532199	for (const SkolemLemma& lem : lems)
291		{
292	1554	newLemmas.push_back(lem.d_lemma);
293	1554	newSkolems.push_back(lem.d_skolem);
294		}
295	530645	Assert(Rewriter::rewrite(ppRewritten) == ppRewritten);
296	530645	if (isProofEnabled() && ppRewritten != current)
297		{
298		TrustNode trn =
299	4888	TrustNode::mkTrustRewrite(current, ppRewritten, d_tpg.get());
300	2444	registerTrustedRewrite(trn, d_tpgRtf.get(), true);
301		}
302
303		// Term formula removal without fixed point. We do not need to do fixed
304		// point since newLemmas are theory-preprocessed until fixed point in
305		// preprocessInternal (at top-level, when procLemmas=true).
306	1061290	TrustNode ttfr = d_tfr.run(ppRewritten, newLemmas, newSkolems, false);
307	1061290	Node rtfNode = ppRewritten;
308	530645	if (!ttfr.isNull())
309		{
310	64746	rtfNode = ttfr.getNode();
311	64746	registerTrustedRewrite(ttfr, d_tpgRtf.get(), true);
312		}
313		// Finish the conversion by rewriting. This is registered as a
314		// post-rewrite, since it is the last step applied for theory atoms.
315	1061290	Node retNode = rewriteWithProof(rtfNode, d_tpgRtf.get(), false);
316	530645	d_rtfCache[current] = retNode;
317	530645	continue;
318		}
319
320		// Not yet substituted, so process
321	2763280	if (stackHead.children_added)
322		{
323		// Children have been processed, so substitute
324	2674168	NodeBuilder builder(current.getKind());
325	1337084	if (current.getMetaKind() == kind::metakind::PARAMETERIZED)
326		{
327		builder << current.getOperator();
328		}
329	6085851	for (unsigned i = 0; i < current.getNumChildren(); ++i)
330		{
331	4748767	Assert(d_rtfCache.find(current[i]) != d_rtfCache.end());
332	4748767	builder << d_rtfCache[current[i]].get();
333		}
334		// Mark the substitution and continue
335	2674168	Node result = builder;
336		// always rewrite here, since current may not be in rewritten form after
337		// reconstruction
338	1337084	result = rewriteWithProof(result, d_tpgRtf.get(), false);
339	2674168	Trace("theory::preprocess-debug")
340	1337084	<< "TheoryPreprocessor::theoryPreprocess setting " << current
341	1337084	<< " -> " << result << endl;
342	1337084	d_rtfCache[current] = result;
343	1337084	toVisit.pop_back();
344		}
345		else
346		{
347		// Mark that we have added the children if any
348	1426196	if (current.getNumChildren() > 0)
349		{
350	1337093	stackHead.children_added = true;
351		// We need to add the children
352	6085877	for (TNode::iterator child_it = current.begin();
353	6085877	child_it != current.end();
354		++child_it)
355		{
356	9497568	TNode childNode = *child_it;
357	4748784	if (d_rtfCache.find(childNode) == d_rtfCache.end())
358		{
359	1514185	toVisit.push_back(childNode);
360		}
361		}
362		}
363		else
364		{
365		// No children, so we're done
366	178206	Trace("theory::preprocess-debug")
367	89103	<< "SubstitutionMap::internalSubstitute setting " << current
368	89103	<< " -> " << current << endl;
369	89103	d_rtfCache[current] = current;
370	89103	toVisit.pop_back();
371		}
372		}
373		}
374	685280	Assert(d_rtfCache.find(assertion) != d_rtfCache.end());
375		// Return the substituted version
376	1370560	Node res = d_rtfCache[assertion];
377	1370560	return TrustNode::mkTrustRewrite(assertion, res, d_tpg.get());
378		}
379
380		// Recursively traverse a term and call the theory rewriter on its sub-terms
381	2451653	Node TheoryPreprocessor::ppTheoryRewrite(TNode term,
382		std::vector<SkolemLemma>& lems)
383		{
384	2451653	NodeMap::iterator find = d_ppCache.find(term);
385	2451653	if (find != d_ppCache.end())
386		{
387	545677	return (*find).second;
388		}
389	1905976	if (term.getNumChildren() == 0)
390		{
391	987167	return preprocessWithProof(term, lems);
392		}
393		// should be in rewritten form here
394	918811	Assert(term == Rewriter::rewrite(term));
395	918811	Trace("theory-pp") << "ppTheoryRewrite { " << term << endl;
396		// do not rewrite inside quantifiers
397	1837622	Node newTerm = term;
398	918811	if (!term.isClosure())
399		{
400	1782728	NodeBuilder newNode(term.getKind());
401	891364	if (term.getMetaKind() == kind::metakind::PARAMETERIZED)
402		{
403	136340	newNode << term.getOperator();
404		}
405	2807164	for (const Node& nt : term)
406		{
407	1915800	newNode << ppTheoryRewrite(nt, lems);
408		}
409	891352	newTerm = Node(newNode);
410	891352	newTerm = rewriteWithProof(newTerm, d_tpg.get(), false);
411		}
412	918799	newTerm = preprocessWithProof(newTerm, lems);
413	918792	d_ppCache[term] = newTerm;
414	918792	Trace("theory-pp") << "ppTheoryRewrite returning " << newTerm << "}" << endl;
415	918792	return newTerm;
416		}
417
418	3449569	Node TheoryPreprocessor::rewriteWithProof(Node term,
419		TConvProofGenerator* pg,
420		bool isPre)
421		{
422	3449569	Node termr = Rewriter::rewrite(term);
423		// store rewrite step if tracking proofs and it rewrites
424	3449569	if (isProofEnabled())
425		{
426		// may rewrite the same term more than once, thus check hasRewriteStep
427	1472173	if (termr != term)
428		{
429	147388	Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (rewriting) "
430	73694	<< term << " -> " << termr << std::endl;
431		// always use term context hash 0 (default)
432	73694	pg->addRewriteStep(term, termr, PfRule::REWRITE, {}, {term}, isPre);
433		}
434		}
435	3449569	return termr;
436		}
437
438	1905964	Node TheoryPreprocessor::preprocessWithProof(Node term,
439		std::vector<SkolemLemma>& lems)
440		{
441		// Important that it is in rewritten form, to ensure that the rewrite steps
442		// recorded in d_tpg are functional. In other words, there should not
443		// be steps from the same term to multiple rewritten forms, which would be
444		// the case if we registered a preprocessing step for a non-rewritten term.
445	1905964	Assert(term == Rewriter::rewrite(term));
446	3811928	Trace("tpp-debug2") << "preprocessWithProof " << term
447	1905964	<< ", #lems = " << lems.size() << std::endl;
448		// We never call ppRewrite on equalities here, since equalities have a
449		// special status. In particular, notice that theory preprocessing can be
450		// called on all formulas asserted to theory engine, including those generated
451		// as new literals appearing in lemmas. Calling ppRewrite on equalities is
452		// incompatible with theory combination where a split on equality requested
453		// by a theory could be preprocessed to something else, thus making theory
454		// combination either non-terminating or result in solution soundness.
455		// Notice that an alternative solution is to ensure that certain lemmas
456		// (e.g. splits from theory combination) can never have theory preprocessing
457		// applied to them. However, it is more uniform to say that theory
458		// preprocessing is applied to all formulas. This makes it so that e.g.
459		// theory solvers do not need to specify whether they want their lemmas to
460		// be theory-preprocessed or not.
461	1905964	if (term.getKind() == kind::EQUAL)
462		{
463	282322	return term;
464		}
465		// call ppRewrite for the given theory
466	3247284	TrustNode trn = d_engine.theoryOf(term)->ppRewrite(term, lems);
467	3247266	Trace("tpp-debug2") << "preprocessWithProof returned " << trn
468	1623633	<< ", #lems = " << lems.size() << std::endl;
469	1623633	if (trn.isNull())
470		{
471		// no change, return
472	1618434	return term;
473		}
474	10398	Node termr = trn.getNode();
475	5199	Assert(term != termr);
476	5199	if (isProofEnabled())
477		{
478	2321	registerTrustedRewrite(trn, d_tpg.get(), false);
479		}
480		// Rewrite again here, which notice is a pre rewrite.
481	5199	termr = rewriteWithProof(termr, d_tpg.get(), true);
482	5199	return ppTheoryRewrite(termr, lems);
483		}
484
485	4361462	bool TheoryPreprocessor::isProofEnabled() const { return d_tpg != nullptr; }
486
487	69511	void TheoryPreprocessor::registerTrustedRewrite(TrustNode trn,
488		TConvProofGenerator* pg,
489		bool isPre)
490		{
491	69511	if (!isProofEnabled() \|\| trn.isNull())
492		{
493	31449	return;
494		}
495	38062	Assert(trn.getKind() == TrustNodeKind::REWRITE);
496	76124	Node eq = trn.getProven();
497	76124	Node term = eq[0];
498	76124	Node termr = eq[1];
499	38062	if (trn.getGenerator() != nullptr)
500		{
501	71486	Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (generator) "
502	35743	<< term << " -> " << termr << std::endl;
503	35743	trn.debugCheckClosed("tpp-debug",
504		"TheoryPreprocessor::preprocessWithProof");
505		// always use term context hash 0 (default)
506	35743	pg->addRewriteStep(
507		term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true);
508		}
509		else
510		{
511	4638	Trace("tpp-debug") << "TheoryPreprocessor: addRewriteStep (trusted) "
512	2319	<< term << " -> " << termr << std::endl;
513		// small step trust
514	4638	pg->addRewriteStep(term,
515		termr,
516		PfRule::THEORY_PREPROCESS,
517		{},
518		{term.eqNode(termr)},
519	2319	isPre);
520		}
521		}
522
523		} // namespace theory
524	27735	} // namespace cvc5