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

 * Top contributors (to current version):

 *   Andrew Reynolds, Dejan Jovanovic, Mudathir Mohamed

 *

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

 * ****************************************************************************

 *

 * Removal of term formulas.

 */

#include "smt/term_formula_removal.h"

#include <vector>

#include "expr/attribute.h"

#include "expr/node_algorithm.h"

#include "expr/skolem_manager.h"

#include "expr/term_context_stack.h"

#include "options/smt_options.h"

#include "proof/conv_proof_generator.h"

#include "proof/lazy_proof.h"

using namespace std;

namespace cvc5 {

    : d_tfCache(u),

      d_skolem_cache(u),

      d_pnm(pnm),

      d_tpg(nullptr),

{

  // enable proofs if necessary

  {

        new TConvProofGenerator(d_pnm,

                                nullptr,

                                TConvPolicy::FIXPOINT,

                                TConvCachePolicy::NEVER,

                                "RemoveTermFormulas::TConvProofGenerator",

  }

                                  std::vector<TrustNode>& newAsserts,

                                  std::vector<Node>& newSkolems,

                                  bool fixedPoint)

{

  {

  }

  // if running to fixed point, we run each new assertion through the

  // run lemma method

  {

    {

      // do not run to fixed point on subcall, since we are processing all

      // lemmas in this loop

    }

  }

  // The rewriting of assertion can be justified by the term conversion proof

  // generator d_tpg.

}

{

}

                                       std::vector<TrustNode>& newAsserts,

                                       std::vector<Node>& newSkolems,

                                       bool fixedPoint)

{

  {

    // no change

  }

  {

    // proofs not enabled, just take result

  }

  // this method is applying this method to TrustNode whose generator is

  // already d_lp (from the run method above), in which case this link is

  // not necessary.

  {

  }

  // ---------------- from input  ------------------------------- from trn

  // assertionPre                 assertionPre = newAssertion

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

  // newAssertion

}

                                     std::vector<TrustNode>& output,

                                     std::vector<Node>& newSkolems)

{

  uint32_t nodeVal;

  {

    {

      // already computed

    }

    // if we have yet to process children

    {

      // check if we should replace the current node

      // if we replaced by a skolem, we do not recurse

      {

        // if this is the first time we've seen this term, we have a new lemma

        // which we add to our vectors

        {

        }

      }

      {

        // currently, we never do any term formula removal in quantifier bodies

      }

      else

      {

        {

          // recurse if we have children

          {

          }

        }

        else

        {

        }

      }

    }

    // otherwise, we are now finished processing children, pop the current node

    // and compute the result

    // if we have not already computed the result

    {

    }

    // reconstruct from the children

    {

      // recompute the value of the child

    }

    // If changes, we reconstruct the node

    {

    }

    // cache

  }

}

                                    TrustNode& newLem)

{

  bool inQuant, inTerm;

  // the exists form of the assertion

  // Handle non-Boolean ITEs here. Boolean ones (within terms) are handled

  // in the "non-variable Boolean term within term" case below.

  {

    // Here, we eliminate the ITE if we are not Boolean and if we are

    // not in a quantified formula. This policy should be in sync with

    // the policy for when to apply theory preprocessing to terms, see PR

    // #5497.

    {

      // Make the skolem to represent the ITE

          node,

          "termITE",

          "a variable introduced due to term-level ITE removal");

      // Notice that in very rare cases, two different terms may have the

      // same purification skolem (see SkolemManager::mkPurifySkolem) For such

      // cases, for simplicity, we repeat the work of constructing the

      // assertion and proofs below. This is so that the proof for the new form

      // of the lemma is used.

      // The new assertion

      // we justify it internally

      {

        // ---------------------- REMOVE_TERM_FORMULA_AXIOM

        // (ite node[0]

        //      (= node node[1])            ------------- MACRO_SR_PRED_INTRO

        //      (= node node[2]))           node = skolem

        // ------------------------------------------ MACRO_SR_PRED_TRANSFORM

        // (ite node[0] (= skolem node[1]) (= skolem node[2]))

        //

        // Note that the MACRO_SR_PRED_INTRO step holds due to conversion

        // of skolem into its witness form, which is node.

                      PfRule::MACRO_SR_PRED_TRANSFORM,

                      {axiom, eq},

      }

    }

  }

  {

    // if a lambda, do lambda-lifting

    {

      {

        // Make the skolem to represent the lambda

            node,

            "lambdaF",

            "a function introduced due to term-level lambda removal");

        // The new assertion

        // bound variable list

        // body

        // axiom defining skolem

        // Lambda lifting is trivial to justify, hence we don't set a proof

        // generator here. In particular, replacing the skolem introduced

        // here with its original lambda ensures the new assertion rewrites

        // to true.

        // For example, if (lambda y. t[y]) has skolem k, then this lemma is:

        //   forall x. k(x)=t[x]

        // whose witness form rewrites

        //   forall x. (lambda y. t[y])(x)=t[x] --> forall x. t[x]=t[x] --> true

      }

    }

  }

  {

    // If a witness choice

    //   For details on this operator, see

    //   http://planetmath.org/hilbertsvarepsilonoperator.

    {

      // NOTE: we can replace by t if body is of the form (and (= z t) ...)

      {

        // Make the skolem to witness the choice, which notice is handled

        // as a special case within SkolemManager::mkPurifySkolem.

            node,

            "witnessK",

            "a skolem introduced due to term-level witness removal");

        // The new assertion is the assumption that the body

        // of the witness operator holds for the Skolem

        // Get the proof generator, if one exists, which was responsible for

        // constructing this witness term. This may not exist, in which case

        // the witness term was trivial to justify. This is the case e.g. for

        // purification witness terms.

        {

          Node existsAssertion =

          // -------------------- from skolem manager

          // (exists x. node[1])

          // -------------------- SKOLEMIZE

          // node[1] * { x -> skolem }

                            expg,

                            PfRule::WITNESS_AXIOM,

                            true,

                            "RemoveTermFormulas::run:skolem_pf");

        }

      }

    }

  }

  {

    // if a non-variable Boolean term within another term, replace it

    {

      // Make the skolem to represent the Boolean term

      // Skolems introduced for Boolean formulas appearing in terms have a

      // special kind (BOOLEAN_TERM_VARIABLE) that ensures they are handled

      // properly in theory combination. We must use this kind here instead of a

      // generic skolem. Notice that the name/comment are currently ignored

      // within SkolemManager::mkPurifySkolem, since BOOLEAN_TERM_VARIABLE

      // variables cannot be given names.

          node,

          "btvK",

          "a Boolean term variable introduced during term formula removal",

          NodeManager::SKOLEM_BOOL_TERM_VAR);

      // The new assertion

      // Boolean term removal is trivial to justify, hence we don't set a proof

      // generator here. It is trivial to justify since it is an instance of

      // purification, which is justified by conversion to witness forms.

    }

  }

  // if the term should be replaced by a skolem

    // this must be done regardless of whether the assertion was new below,

    // since a formula-term may rewrite to the same skolem in multiple contexts.

    {

      // justify the introduction of the skolem

      // ------------------- MACRO_SR_PRED_INTRO

      // t = witness x. x=t

      // The above step is trivial, since the skolems introduced above are

      // all purification skolems. We record this equality in the term

      // conversion proof generator.

                            skolem,

                            PfRule::MACRO_SR_PRED_INTRO,

                            {},

                            {node.eqNode(skolem)},

                            true,

    }

    // if the skolem was introduced in this call

    {

      // if proofs are enabled

      {

        // justify the axiom that defines the skolem, if not already done so

        {

          // Should have trivial justification if not yet provided. This is the

          // case of lambda lifting and Boolean term removal.

          // ---------------- MACRO_SR_PRED_INTRO

          // newAssertion

        }

      }

                              "RemoveTermFormulas::run:new_assert");

    }

    // The representation is now the skolem

  }

  // return null, indicating we will traverse children within runInternal

}

{

  context::CDInsertHashMap<Node, Node>::const_iterator itk =

  {

  }

}

{

  {

  }

}

{

}