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

 * Top contributors (to current version):

 *   Andrew Reynolds

 *

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

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

 *

 * A let binding.

 */

#include "cvc5_private.h"

#ifndef CVC5__PRINTER__LET_BINDING_H

#define CVC5__PRINTER__LET_BINDING_H

#include <vector>

#include "context/cdhashmap.h"

#include "context/cdlist.h"

#include "expr/node.h"

namespace cvc5 {

/**

 * A flexible let binding class. This class provides functionalities for

 * printing letified terms. A simple use case is the following for Node n

 * and LetBinding lbind:

 * ```

 *   std::vector<Node> letList;

 *   lbind.letify(n, letList);

 * ```

 * Now, letList contains a list of subterms of n that should be letified based

 * on the threshold value passed to this class where a value n>0 indicates that

 * terms with n or more occurrences should be letified.

 *

 * The above is equivalent to:

 * ```

 *   std::vector<Node> letList;

 *   lbind.pushScope();

 *   lbind.process(n);

 *   lbind.letify(letList);

 * ```

 * In fact, multiple terms can be passed to calls to process, in which case the

 * counting is cumulative.

 *

 * All quantified formulas are treated as black boxes. This class can be used

 * to letify terms with quantifiers, where multiple calls to pushScope /

 * popScope can be used. In particular, consider:

 * ```

 *   std::vector<Node> letList1;

 *   lbind.letify(n1, letList1);

 *   std::vector<Node> letList2;

 *   lbind.letify(n2, letList2);

 *   ...

 *   lbind.popScope();

 *   lbind.popScope();

 * ```

 * In a typical use case, n2 is the body of a quantified formula that is a

 * subterm of n1. We have that letList2 is the list of subterms of n2 that

 * should be letified, assuming that we have already have let definitions

 * given by letList1.

 *

 * Internally, a let binding is a list and a map that can be printed as a let

 * expression. In particular, the list d_letList is ordered such that

 * d_letList[i] does not contain subterm d_letList[j] for j>i.

 * It is intended that d_letList contains only unique nodes. Each node

 * in d_letList is mapped to a unique identifier in d_letMap.

 *

 * Notice that this class will *not* use introduced let symbols when converting

 * the bodies of quantified formulas. Consider the formula:

 * (let ((Q (forall ((x Int)) (= x (+ a a))))) (and (= (+ a a) (+ a a)) Q Q))

 * where "let" above is from the user. When this is letified by this class,

 * note that (+ a a) occurs as a subterm of Q, however it is not seen until

 * after we have seen Q twice, since we traverse in reverse topological order.

 * Since we do not traverse underneath quantified formulas, this means that Q

 * may be marked as a term-to-letify before (+ a a), which leads to violation

 * of the above invariant concerning containment. Thus, when converting, if

 * a let symbol is introduced for (+ a a), we will not replace the occurence

 * of (+ a a) within Q. Instead, the user of this class is responsible for

 * letifying the bodies of quantified formulas independently.

 */

{

  using NodeList = context::CDList<Node>;

  using NodeIdMap = context::CDHashMap<Node, uint32_t>;

 public:

  LetBinding(uint32_t thresh = 2);

  /** Get threshold */

  uint32_t getThreshold() const;

  /**

   * This updates this let binding to consider the counts for node n.

   */

  void process(Node n);

  /**

   * This pushes a scope, computes the letification for n, adds the (new) terms

   * that must be letified in this context to letList.

   *

   * Notice that this method does not traverse inside of closures.

   *

   * @param n The node to letify

   * @param letList The list of terms that should be letified within n. This

   * list is ordered in such a way that letList[i] does not contain subterm

   * letList[j] for j>i.

   */

  void letify(Node n, std::vector<Node>& letList);

  /**

   * Same as above, without a node to letify.

   */

  void letify(std::vector<Node>& letList);

  /** Push scope */

  void pushScope();

  /** Pop scope for n, reverts the state change of the above method */

  void popScope();

  /**

   * @return the identifier for node n, or 0 if it does not have one.

   */

  uint32_t getId(Node n) const;

  /**

   * Convert n based on the state of the let binding. This replaces all

   * letified subterms of n with a fresh variable whose name prefix is the

   * given one.

   *

   * @param n The node to convert

   * @param prefix The prefix of variables to convert

   * @param letTop Whether we letify n itself

   * @return the converted node.

   */

  Node convert(Node n, const std::string& prefix, bool letTop = true) const;

 private:

  /**

   * Compute the count of sub nodes in n, store in d_count. Additionally,

   * store each node in the domain of d_count in an order in d_visitList

   * such that d_visitList[i] does not contain sub d_visitList[j] for j>i.

   */

  void updateCounts(Node n);

  /**

   * Convert a count to a let binding.

   */

  void convertCountToLet();

  /** The dag threshold */

  uint32_t d_thresh;

  /** An internal context */

  context::Context d_context;

  /** Visit list */

  NodeList d_visitList;

  /** Count */

  NodeIdMap d_count;

  /** The let list */

  NodeList d_letList;

  /** The let map */

  NodeIdMap d_letMap;

};

}  // namespace cvc5

#endif