/******************************************************************************

 * 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 "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 {

                                       context::UserContext* userContext,

    : d_engine(engine),

      d_ppCache(userContext),

      d_rtfCache(userContext),

      d_tfr(userContext, pnm),

      d_tpg(pnm ? new TConvProofGenerator(

                      pnm,

                      userContext,

                      TConvPolicy::FIXPOINT,

                      TConvCachePolicy::NEVER,

                      "TheoryPreprocessor::preprocess_rewrite",

                : nullptr),

      d_tpgRtf(pnm ? new TConvProofGenerator(pnm,

                                             userContext,

                                             TConvPolicy::FIXPOINT,

                                             TConvCachePolicy::NEVER,

                                             "TheoryPreprocessor::rtf",

                   : nullptr),

      d_tpgRew(pnm ? new TConvProofGenerator(pnm,

                                             userContext,

                                             TConvPolicy::ONCE,

                                             TConvCachePolicy::NEVER,

                   : nullptr),

      d_tspg(nullptr),

      d_lp(pnm ? new LazyCDProof(pnm,

                                 nullptr,

                                 userContext,

{

  {

    // 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<TrustNode>& newLemmas,

                                         std::vector<Node>& newSkolems)

{

}

    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.

  // 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.

  // run theory preprocessing

  {

    {

    }

    {

    }

  }

  {

    // 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.

    {

    }

  }

  {

    // no change

  }

  // Now, sequence the conversion steps if proofs are enabled.

  {

    // We have that:

    // node -> irNode via rewriting

    // irNode -> ppNode via theory-preprocessing + rewriting + tf removal

  }

  else

  {

  }

}

                                              std::vector<TrustNode>& newLemmas,

                                              std::vector<Node>& newSkolems)

{

}

    TrustNode node,

    std::vector<TrustNode>& newLemmas,

    std::vector<Node>& newSkolems,

    bool procLemmas)

{

  // what was originally proven

  TrustNode tplemma =

  {

    // no change needed

  }

  // what it was preprocessed to

  // process the preprocessing

  {

    // add the original proof to the lazy proof

    // only need to do anything if lemmap changed in a non-trivial way

    {

                        tplemma.getGenerator(),

                        PfRule::THEORY_PREPROCESS,

                        true,

                        "TheoryEngine::lemma_pp");

      // ---------- from node -------------- from theory preprocess

      // lemma                lemma = lemmap

      // ------------------------------------------ EQ_RESOLVE

      // lemmap

    }

  }

}

{

}

{

  TNode node;

  bool children_added;

};

    TNode assertion,

    std::vector<TrustNode>& newLemmas,

    std::vector<Node>& newSkolems)

{

  // spendResource();

  // Do a topological sort of the subexpressions and substitute them

  {

    // The current node we are processing

    // If node already in the cache we're done, pop from the stack

    {

    }

    {

    }

    // If this is an atom, we preprocess its terms with the theory ppRewriter

    {

      {

      }

      {

        TrustNode trn =

      }

      // 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).

      {

      }

      // 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_tpgRtf. 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).

    }

    // Not yet substituted, so process

    {

      // Children have been processed, so substitute

      {

      }

      {

      }

      // Mark the substitution and continue

      // always rewrite here, since current may not be in rewritten form after

      // reconstruction

    }

    else

    {

      // Mark that we have added the children if any

      {

        // We need to add the children

             ++child_it)

        {

          {

          }

        }

      }

      else

      {

        // No children, so we're done

      }

    }

  }

  // Return the substituted version

}

// Recursively traverse a term and call the theory rewriter on its sub-terms

                                         std::vector<SkolemLemma>& lems)

{

  {

  }

  {

  }

  // should be in rewritten form here

  // do not rewrite inside quantifiers

  {

    {

    }

    {

    }

  }

}

                                          TConvProofGenerator* pg,

                                          bool isPre)

{

  // store rewrite step if tracking proofs and it rewrites

  {

    // may rewrite the same term more than once, thus check hasRewriteStep

    {

      // always use term context hash 0 (default)

    }

  }

}

                                             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.

  // 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.

  {

  }

  // call ppRewrite for the given theory

  {

    // no change, return

  }

  {

  }

  // Rewrite again here, which notice is a *pre* rewrite.

}

                                                TConvProofGenerator* pg,

                                                bool isPre)

{

  {

  }

  {

                         "TheoryPreprocessor::preprocessWithProof");

    // always use term context hash 0 (default)

        term, termr, trn.getGenerator(), isPre, PfRule::ASSUME, true);

  }

  else

  {

    // small step trust

                       termr,

                       PfRule::THEORY_PREPROCESS,

                       {},

                       {term.eqNode(termr)},

  }

}

}  // namespace theory