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

 * Top contributors (to current version):

 *   Andrew Reynolds, Andres Noetzli, Dejan Jovanovic

 *

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

 */

#include "theory/rewriter.h"

#include "options/theory_options.h"

#include "proof/conv_proof_generator.h"

#include "smt/smt_engine.h"

#include "smt/smt_engine_scope.h"

#include "smt/smt_statistics_registry.h"

#include "theory/builtin/proof_checker.h"

#include "theory/evaluator.h"

#include "theory/quantifiers/extended_rewrite.h"

#include "theory/rewriter_tables.h"

#include "theory/theory.h"

#include "util/resource_manager.h"

using namespace std;

namespace cvc5 {

namespace theory {

/** Attribute true for nodes that have been rewritten with proofs enabled */

struct RewriteWithProofsAttributeId

{

};

typedef expr::Attribute<RewriteWithProofsAttributeId, bool>

    RewriteWithProofsAttribute;

// Note that this function is a simplified version of Theory::theoryOf for

// (type-based) theoryOfMode. We expand and simplify it here for the sake of

// efficiency.

  {

    // Equality is owned by the theory that owns the domain

  }

  // Regular nodes are owned by the kind

}

/**

 * TheoryEngine::rewrite() keeps a stack of things that are being pre-

 * and post-rewritten.  Each element of the stack is a

 * RewriteStackElement.

 */

  /**

   * Construct a fresh stack element.

   */

        d_original(node),

        d_theoryId(theoryId),

        d_originalTheoryId(theoryId),

  {

  {

  }

  /** The node we're currently rewriting */

  Node d_node;

  /** Original node (either the unrewritten node or the node after prerewriting)

   */

  Node d_original;

  /** Id of the theory that's currently rewriting this node */

  unsigned d_theoryId : 8;

  /** Id of the original theory that started the rewrite */

  unsigned d_originalTheoryId : 8;

  /** Index of the child this node is done rewriting */

  unsigned d_nextChild : 32;

  /** Builder for this node */

  NodeBuilder d_builder;

};

  {

    // Nodes with zero children should never change via rewriting. We return

    // eagerly for the sake of efficiency here.

  }

}

{

}

{

}

                                     bool isExtEq)

{

  // must set the proof checker before calling this

  {

    // theory rewriter is responsible for rewriting the equality

  }

}

{

  // if not already initialized with proof support

  {

    // the rewriter is staticly determinstic, thus use static cache policy

    // for the term conversion proof generator

                                        nullptr,

                                        TConvPolicy::FIXPOINT,

                                        TConvCachePolicy::STATIC,

  }

{

  // note we don't force caching of this method currently

}

                                      TheoryRewriter* trew)

{

{

}

{

}

                         Node node,

                         TConvProofGenerator* tcpg)

{

  RewriteWithProofsAttribute rpfa;

#ifdef CVC5_ASSERTIONS

  {

  }

#endif

  // Check if it's been cached already

  {

  }

  // Put the node on the stack in order to start the "recursive" rewrite

  }

  // Rewrite until the stack is empty

  for (;;){

    {

    }

    // Get the top of the recursion stack

    // Before rewriting children we need to do a pre-rewrite of the node

    {

      // Check if the pre-rewrite has already been done (it's in the cache)

                                  rewriteStackTop.d_node);

      {

        // Rewrite until fix-point is reached

        for(;;) {

          // Perform the pre-rewrite

          RewriteResponse response = preRewrite(

          // Put the rewritten node to the top of the stack

          // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite

          {

          }

        // Cache the rewrite

                           rewriteStackTop.d_original,

                           rewriteStackTop.d_node);

      }

      // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)

      else {

        // Continue with the cached version

      }

    }

    // Now it's time to rewrite the children, check if this has already been done

                                 rewriteStackTop.d_node);

    // If not, go through the children

    {

      // The child we need to rewrite

      // To build the rewritten expression we set up the builder

        {

          // The children will add themselves to the builder once they're done

          }

        }

      }

      // Process the next child

      {

        // The child node

        // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)

        // Go on with the rewriting

      }

      // Incorporate the children if necessary

      {

      }

      // Done with all pre-rewriting, so let's do the post rewrite

      for(;;) {

        // Do the post-rewrite

        RewriteResponse response = postRewrite(

        // We continue with the response we got

        {

          // In the post rewrite if we've changed theories, we must do a full rewrite

          //TODO: this is not thread-safe - should make this assertion dependent on sequential build

#ifdef CVC5_ASSERTIONS

                 == d_rewriteStack->end());

#endif

#ifdef CVC5_ASSERTIONS

#endif

        }

        {

#ifdef CVC5_ASSERTIONS

          RewriteResponse r2 =

#endif

        }

        // Check for trivial rewrite loops of size 1 or 2

                   ->postRewrite(response.d_node)

                   .d_node

               != rewriteStackTop.d_node);

      // We're done with the post rewrite, so we add to the cache

      {

        // if proofs are enabled, mark that we've rewritten with proofs

        {

          // We may have gotten a different node, due to non-determinism in

          // theory rewriters (e.g. quantifiers rewriter which introduces

          // fresh BOUND_VARIABLE). This can happen if we wrote once without

          // proofs and then rewrote again with proofs.

          {

            // we make this a post-rewrite, since we are processing a node that

            // has finished post-rewriting above

                                 cached,

                                 PfRule::TRUST_REWRITE,

                                 {},

                                 {eq},

            // don't overwrite the cache, should be the same

          }

        }

      }

                          rewriteStackTop.d_original,

                          rewriteStackTop.d_node);

    }

    else

    {

      // We were already in cache, so just remember it

    }

    // If this is the last node, just return

             || rewriteStackTop.d_node.isConst());

    }

    // We're done with this node, append it to the parent

  Unreachable();

} /* Rewriter::rewriteTo() */

                                     TNode n,

                                     TConvProofGenerator* tcpg)

{

  {

    // call the trust rewrite response interface

    TrustRewriteResponse tresponse =

    // process the trust rewrite response: store the proof step into

    // tcpg if necessary and then convert to rewrite response.

  }

}

                                      TNode n,

                                      TConvProofGenerator* tcpg)

{

  {

    // same as above, for post-rewrite

    TrustRewriteResponse tresponse =

  }

}

    theory::TheoryId theoryId,

    const TrustRewriteResponse& tresponse,

    bool isPre,

    TConvProofGenerator* tcpg)

{

  {

    {

      // add small step trusted rewrite

      Node rid = mkMethodId(isPre ? MethodId::RW_REWRITE_THEORY_PRE

                           proven[1],

                           PfRule::THEORY_REWRITE,

                           {},

                           {proven, tidn, rid},

    }

    else

    {

      // store proven rewrite step

    }

  }

}

{

#ifdef CVC5_ASSERTIONS

#endif

{

  {

  }

  {

  }

  {

  }

  {

    Evaluator eval;

  }

  {

    // does nothing

  }

  // unknown rewriter

  return n;

}

}  // namespace theory