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

 * Top contributors (to current version):

 *   Andrew Reynolds, Haniel Barbosa, Aina Niemetz

 *

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

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

 *

 * Implementation of module for processing proof nodes.

 */

#include "smt/proof_post_processor.h"

#include "expr/skolem_manager.h"

#include "options/proof_options.h"

#include "preprocessing/assertion_pipeline.h"

#include "proof/proof_node_manager.h"

#include "smt/smt_engine.h"

#include "theory/arith/arith_utilities.h"

#include "theory/builtin/proof_checker.h"

#include "theory/bv/bitblast/bitblast_proof_generator.h"

#include "theory/bv/bitblast/proof_bitblaster.h"

#include "theory/rewriter.h"

#include "theory/strings/infer_proof_cons.h"

#include "theory/theory.h"

#include "util/rational.h"

using namespace cvc5::kind;

using namespace cvc5::theory;

namespace cvc5 {

namespace smt {

                                                   ProofGenerator* pppg,

                                                   rewriter::RewriteDb* rdb,

    : d_env(env),

      d_pppg(pppg),

      d_wfpm(env.getProofNodeManager()),

{

{

{

                                            const std::vector<Node>& fa,

                                            bool& continueUpdate)

{

  {

  }

  // other than elimination rules, we always update assumptions as long as

  // d_updateScopedAssumptions is true or they are *not* in scope, i.e., not in

  // fa

  {

  }

}

                                      PfRule id,

                                      const std::vector<Node>& children,

                                      const std::vector<Node>& args,

                                      CDProof* cdp,

                                      bool& continueUpdate)

{

  {

    // we cache based on the assumption node, not the proof node, since there

    // may be multiple occurrences of the same node.

    std::map<Node, std::shared_ptr<ProofNode>>::iterator it =

    {

    }

    else

    {

      // get proof from preprocess proof generator

      // print for debugging

      {

      }

      else

      {

        {

        }

      }

    }

    {

      // no update

    }

    // connect the proof

  }

}

                                              PfRule id,

                                              const std::vector<Node>& children,

                                              const std::vector<Node>& args,

                                              CDProof* cdp)

{

}

    const std::vector<Node>& clauseLits,

    const std::vector<Node>& targetClauseLits,

    const std::vector<Node>& children,

    const std::vector<Node>& args,

    CDProof* cdp)

{

  // get crowding lits and the position of the last clause that includes

  // them. The factoring step must be added after the last inclusion and before

  // its elimination.

  // positions of eliminators of crowding literals, which are the positions of

  // the clauses that eliminate crowding literals *after* their last inclusion

  {

    {

      // found crowding lit, now get its last inclusion position, which is the

      // position of the last resolution link that introduces the crowding

      // literal. Note that this position has to be *before* the last link, as a

      // link *after* the last inclusion must eliminate the crowding literal.

      size_t j;

      {

        // notice that only non-singleton clauses may be introducing the

        // crowding literal, so we only care about non-singleton OR nodes. We

        // check then against the kind and whether the whole OR node occurs as a

        // pivot of the respective resolution

        {

        }

        {

        }

        {

        }

      }

      // get elimination position, starting from the following link as the last

      // inclusion one. The result is the last (in the chain, but first from

      // this point on) resolution link that eliminates the crowding literal. A

      // literal l is eliminated by a link if it contains a literal l' with

      // opposite polarity to l.

      {

        // To eliminate the crowding literal (crowdLit), the clause must contain

        // it with opposite polarity. There are three successful cases,

        // according to the pivot and its sign

        //

        // - crowdLit is the same as the pivot and posFirst is true, which means

        //   that the clause contains its negation and eliminates it

        //

        // - crowdLit is the negation of the pivot and posFirst is false, so the

        //   clause contains the node whose negation is crowdLit. Note that this

        //   case may either be crowdLit.notNode() == pivot or crowdLit ==

        //   pivot.notNode().

        {

        }

      }

    }

  }

  // order map so that we process crowding literals in the order of the clauses

  // that last introduce them

  // order eliminators

  {

    {

    }

    {

    }

  }

  // TODO (cvc4-wishues/issues/77): implement also simpler version and compare

  //

  // We now start to break the chain, one step at a time. Naively this breaking

  // down would be one resolution/factoring to each crowding literal, but we can

  // merge some of the cases. Effectively we do the following:

  //

  //

  // lastClause   children[start] ... children[end]

  // ---------------------------------------------- CHAIN_RES

  //         C

  //    ----------- FACTORING

  //    lastClause'                children[start'] ... children[end']

  //    -------------------------------------------------------------- CHAIN_RES

  //                                    ...

  //

  // where

  //   lastClause_0 = children[0]

  //   start_0 = 1

  //   end_0 = eliminators[0] - 1

  //   start_i+1 = nextGuardedElimPos - 1

  //

  // The important point is how end_i+1 is computed. It is based on what we call

  // the "nextGuardedElimPos", i.e., the next elimination position that requires

  // removal of duplicates. The intuition is that a factoring step may eliminate

  // the duplicates of crowding literals l1 and l2. If the last inclusion of l2

  // is before the elimination of l1, then we can go ahead and also perform the

  // elimination of l2 without another factoring. However if another literal l3

  // has its last inclusion after the elimination of l2, then the elimination of

  // l3 is the next guarded elimination.

  //

  // To do the above computation then we determine, after a resolution/factoring

  // step, the first crowded literal to have its last inclusion after "end". The

  // first elimination position to be bigger than the position of that crowded

  // literal is the next guarded elimination position.

  do

  {

    // note that the interval of insert is exclusive in the end, so we add 1

                                                     childrenRes,

                                                     childrenResArgs,

                                                     "");

        resPlaceHolder, PfRule::CHAIN_RESOLUTION, childrenRes, childrenResArgs);

    // I need to add factoring if end < children.size(). Otherwise, this is

    // to be handled by the caller

    {

      {

      }

      else

      {

      }

    }

    else

    {

    }

    // update for next round

    // find the position of the last inclusion of the next crowded literal

    {

      {

      }

    }

    // if there is none, then the remaining literals will be used in the next

    // round

    {

    }

    else

    {

      {

        //  nextGuardedElimPos is the largest element of

        // eliminators bigger the next crowded literal's last inclusion

        {

        }

      }

    }

  } while (true);

}

                                            const std::vector<Node>& children,

                                            const std::vector<Node>& args,

                                            CDProof* cdp)

{

  {

    // not eliminated

  }

  // macro elimination

  {

    // (TRANS

    //   (SUBS <children> :args args[0:1])

    //   (REWRITE :args <t.substitute(x1,t1). ... .substitute(xn,tn)> args[2]))

    {

      {

        {

        }

      }

      {

        {

        }

      }

          t, children, ids, ida);

      {

        // apply SUBS proof rule if necessary

        {

          // if we specified that we did not want to eliminate, add as step

        }

      }

    }

    else

    {

      // no substitute

    }

    {

      {

      }

    }

    {

      // apply REWRITE proof rule

      {

        // if not elimianted, add as step

      }

    }

    {

      // typically not necessary, but done to be robust

    }

    // must add TRANS if two step

  }

  {

    // take into account witness form, if necessary

    // (TRUE_ELIM

    // (TRANS

    //    (MACRO_SR_EQ_INTRO <children> :args (t args[1:]))

    //    ... proof of apply_SR(t) = toWitness(apply_SR(t)) ...

    //    (MACRO_SR_EQ_INTRO {} {toWitness(apply_SR(t))})

    // ))

    // Notice this is an optimized, one sided version of the expansion of

    // MACRO_SR_PRED_TRANSFORM below.

    // We call the expandMacros method on MACRO_SR_EQ_INTRO, where notice

    // that this rule application is immediately expanded in the recursive

    // call and not added to the proof.

    {

      {

        // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))

        // rewrite again, don't need substitution. Also we always use the

        // default rewriter, due to the definition of MACRO_SR_PRED_INTRO.

      }

    }

    // apply transitivity if necessary

  }

  {

    // (EQ_RESOLVE

    //   children[0]

    //   (MACRO_SR_EQ_INTRO children[1:] :args children[0] ++ args))

    // apply equality resolve

  }

  {

    // (EQ_RESOLVE

    //   children[0]

    //   (TRANS

    //      (MACRO_SR_EQ_INTRO children[1:] :args (children[0] args[1:]))

    //      ... proof of c = wc

    //      (MACRO_SR_EQ_INTRO {} wc)

    //      (SYMM

    //        (MACRO_SR_EQ_INTRO children[1:] :args <args>)

    //        ... proof of a = wa

    //        (MACRO_SR_EQ_INTRO {} wa))))

    // where

    // wa = toWitness(apply_SR(args[0])) and

    // wc = toWitness(apply_SR(children[0])).

    {

      // nothing to do

    }

    // first, compute if we need

    // convert both sides, in three steps, take symmetry of second chain

    {

      // first rewrite children[0], then args[0]

      // t = apply_SR(t)

      // apply_SR(t) = toWitness(apply_SR(t))

      {

        {

          // toWitness(apply_SR(t)) = apply_SR(toWitness(apply_SR(t)))

          // rewrite again, don't need substitution. Also, we always use the

          // default rewriter, due to the definition of MACRO_SR_PRED_TRANSFORM.

          Node weqr =

        }

      }

      // add to overall chain

      {

        // add the current chain to the overall chain

      }

      else

      {

        // add the current chain to cdp

        {

          // take symmetry of above and add it to the overall chain

        }

      }

    }

    // apply transitivity if necessary

  }

  {

    // first generate the naive chain_resolution

    // There are n cases:

    // - if the conclusion is the same, just replace

    // - if they have the same literals but in different quantity, add a

    //   FACTORING step

    // - if the order is not the same, add a REORDERING step

    // - if there are literals in chainConclusion that are not in the original

    //   conclusion, we need to transform the MACRO_RESOLUTION into a series of

    //   CHAIN_RESOLUTION + FACTORING steps, so that we explicitly eliminate all

    //   these "crowding" literals. We do this via FACTORING so we avoid adding

    //   an exponential number of premises, which would happen if we just

    //   repeated in the premises the clauses needed for eliminating crowding

    //   literals, which could themselves add crowding literals.

    {

          chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);

    }

    // If we got here, then chainConclusion is NECESSARILY an OR node

    // get the literals in the chain conclusion

    std::vector<Node> chainConclusionLits{chainConclusion.begin(),

    std::set<Node> chainConclusionLitsSet{chainConclusion.begin(),

    // is args[0] a singleton clause? If it's not an OR node, then yes.

    // Otherwise, it's only a singleton if it occurs in chainConclusionLitsSet

    // whether conclusion is singleton

    {

    }

    else

    {

    }

    std::set<Node> conclusionLitsSet{conclusionLits.begin(),

    // If the sets are different, there are "crowding" literals, i.e. literals

    // that were removed by implicit multi-usage of premises in the resolution

    // chain.

    {

          chainConclusionLits, conclusionLits, children, args, cdp);

      // update vector of lits. Note that the set is no longer used, so we don't

      // need to update it

      //

      // We need again to check whether chainConclusion is a singleton

      // clause. As above, it's a singleton if it's in the original

      // chainConclusionLitsSet.

      {

      }

      else

      {

                                   chainConclusion.begin(),

      }

    }

    else

    {

          chainConclusion, PfRule::CHAIN_RESOLUTION, children, chainResArgs);

    }

    // Placeholder for running conclusion

    // factoring

    {

      // We build it rather than taking conclusionLits because the order may be

      // different

      {

        {

        }

      }

                          ? nm->mkConst(false)

    }

    // either same node or n as a clause

    // reordering

    {

    }

  }

  {

    // Notice that a naive way to reconstruct SUBS is to do a term conversion

    // proof for each substitution.

    // The proof of f(a) * { a -> g(b) } * { b -> c } = f(g(c)) is:

    //   TRANS( CONG{f}( a=g(b) ), CONG{f}( CONG{g}( b=c ) ) )

    // Notice that more optimal proofs are possible that do a single traversal

    // over t. This is done by applying later substitutions to the range of

    // previous substitutions, until a final simultaneous substitution is

    // applied to t.  For instance, in the above example, we first prove:

    //   CONG{g}( b = c )

    // by applying the second substitution { b -> c } to the range of the first,

    // giving us a proof of g(b)=g(c). We then construct the updated proof

    // by tranitivity:

    //   TRANS( a=g(b), CONG{g}( b=c ) )

    // We then apply the substitution { a -> g(c), b -> c } to f(a), to obtain:

    //   CONG{f}( TRANS( a=g(b), CONG{g}( b=c ) ) )

    // which notice is more compact than the proof above.

    // get the kind of substitution

    {

    }

    {

    }

    // first, compute the entire substitution

    {

      // get the substitution

      // ensure proofs for each formula in fromList

      {

             j++)

        {

        }

      }

    }

    {

      // Note we process in forward order, since later substitution should be

      // applied to earlier ones, and the last child of a SUBS is processed

      // first.

      // apply the current substitution to the range

      {

        Node ss =

        {

          // make the proof for the tranitivity step

          // prove the updated substitution

          TConvProofGenerator tcg(d_pnm,

                                  nullptr,

                                  TConvPolicy::ONCE,

                                  TConvCachePolicy::NEVER,

                                  "nested_SUBS_TConvProofGenerator",

                                  nullptr,

          // add previous rewrite steps

          {

            // substitutions are pre-rewrites

          }

          // get the proof for the update to the current substitution

          // add the proof

          // get proof for childFrom from cdp

          // ensure we have a proof of var = subs

          // transitivity

          // add to the substitution

        }

      }

      // Just use equality from CDProof, but ensure we have a proof in cdp.

      // This may involve a TRUE_INTRO/FALSE_INTRO if the substitution step

      // uses the assumption childFrom as a Boolean assignment (e.g.

      // childFrom = true if we are using MethodId::SB_LITERAL).

    }

    // should be implied by the substitution now

                                                         : TConvPolicy::ONCE;

    TConvProofGenerator tcpg(d_pnm,

                             nullptr,

                             tcpolicy,

                             TConvCachePolicy::NEVER,

                             "SUBS_TConvProofGenerator",

                             nullptr,

    {

      // substitutions are pre-rewrites

    }

    // add the proof constructed by the term conversion utility

    Node ts = builtin::BuiltinProofRuleChecker::applySubstitution(

    {

    }

    // should give a proof, if not, then tcpg does not agree with the

    // substitution.

    {

    }

    else

    {

    }

  }

  {

    // get the kind of rewrite

    {

    }

    {

      // rewrites from theory::Rewriter

      // use rewrite with proof interface

      {

        // did not have a proof of rewriting, probably isExtEq is true

        {

          // update to THEORY_REWRITE with idr

        }

        else

        {

          // this should never be applied

        }

      }

      else

      {

      }

    }

    {

      // change to evaluate, which is never eliminated

    }

    else

    {

      // try to reconstruct as a standalone rewrite

      // in this case, must be a non-standard rewrite kind

      {

        // don't know how to eliminate

      }

    }

    {

      // should not be necessary typically

    }

  }

  {

    // try to replay theory rewrite

    // first, check that maybe its just an evaluation step

    Node ceval =

    {

    }

    // otherwise no update

  }

  {

    {

      {

      }

    }

    // Scale all children, accumulating

    {

      Node scalarCmp =

      // (= scalarCmp true)

      // scalarCmp

      // (and scalarCmp relation)

      Node scalarCmpAndRel =

      // (=> (and scalarCmp relation) scaled)

      Node impl =

          steps.tryStep(isPos ? PfRule::ARITH_MULT_POS : PfRule::ARITH_MULT_NEG,

                        {},

      // scaled

      Node scaled =

    }

  }

  {

    // get the arguments

    InferenceId iid;

    bool isRev;

    {

      {

      }

    }

  }

  {

  }

  // TRUST, PREPROCESS, THEORY_LEMMA, THEORY_PREPROCESS?

}

{

  {

    // not necessary, add REFL step

  }

  {

    // add the proof