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

 * Top contributors (to current version):

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

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

 *

 * Utility class for Sygus Reconstruct module.

 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_H

#define CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_H

#include "expr/node.h"

namespace cvc5 {

namespace theory {

namespace quantifiers {

/**

 * A class for holding Sygus Reconstruct obligations. An obligation is a builtin

 * term t and a SyGuS type T, and indicates that we are trying to build a term

 * of type T whose builtin analog is equivalent to t. This class encodes each

 * obligation (T, t) as a skolem k of type T to embed obligations in candidate

 * solutions (see d_candSols below). Notice that the SyGuS type T of an

 * obligation is not stored in this class as it can be inferred from the type of

 * the skolem k.

 */

{

 public:

  /**

   * Constructor. Default value needed for maps.

   *

   * @param stn sygus datatype type to reconstruct `t` into

   * @param t builtin term to reconstruct

   */

  RConsObligation(TypeNode stn, Node t);

  /**

   * @return sygus datatype type to reconstruct equivalent builtin terms into

   */

  TypeNode getType() const;

  /**

   * @return skolem representing this obligation

   */

  Node getSkolem() const;

  /**

   * Add `t` to the set of equivalent builtins this obligation solves.

   *

   * \note `t` MUST be equivalent to the builtin terms in `d_ts`

   *

   * @param t builtin term to add

   */

  void addBuiltin(Node t);

  /**

   * @return equivalent builtin terms to reconstruct for this obligation

   */

  const std::unordered_set<Node>& getBuiltins() const;

  /**

   * Add candidate solution to the set of candidate solutions for the

   * corresponding obligation.

   *

   * @param candSol the candidate solution to add

   */

  void addCandidateSolution(Node candSol);

  /**

   * @return set of candidate solutions for this obligation

   */

  const std::unordered_set<Node>& getCandidateSolutions() const;

  /**

   * Add candidate solution to the set of candidate solutions waiting for the

   * corresponding obligation to be solved.

   *

   * @param candSol the candidate solution to add to watch set

   */

  void addCandidateSolutionToWatchSet(Node candSol);

  /**

   * @return set of candidate solutions waiting for this obligation to be solved

   */

  const std::unordered_set<Node>& getWatchSet() const;

  /**

   * Print all reachable obligations and their candidate solutions from

   * the `root` obligation and its candidate solutions.

   *

   * An obligation is reachable from the `root` obligation if it is the `root`

   * obligation or is needed by one of the candidate solutions of other

   * reachable obligations.

   *

   * For example, if we have:

   *

   * Obs = [(k1, {(+ 1 (- x))}, (k2, (- x)), (k3, x), (k4, 0)]

   * CandSols = {k1 -> {(c_+ c_1 k2)}, k2 -> {(c_- k3)},

   *             k3 -> {c_x}, k4 -> {c_0}}

   * root = k1

   *

   * Then, the set of reachable obligations from `root` is {k1, k2, k3}

   *

   * \note requires enabling "sygus-rcons" trace

   *

   * @param root the root obligation to start from

   * @param obs a list of obligations containing at least 1 obligation

   * @param

   */

  static void printCandSols(

      const RConsObligation* root,

      const std::vector<std::unique_ptr<RConsObligation>>& obs);

 private:

  /** Skolem representing this obligation used to embed obligations in candidate

   * solutions. */

  Node d_k;

  /** Equivalent builtin terms for this obligation.

   *

   * To solve the obligation, one of these builtin terms must be reconstructed

   * in the specified grammar (sygus datatype type) of the obligation.

   */

  std::unordered_set<Node> d_ts;

  /** A set of candidate solutions to this obligation.

   *

   * Each candidate solution is a sygus datatype term containing skolem subterms

   * (sub-obligations). By replacing all sub-obligations with their

   * corresponding solutions, we get a term whose builtin analog rewrites to

   * a term in `d_ts` and hence solves this obligation. For example, given:

   *   d_ts = {(+ x y)}

   * a possible set of candidate solutions would be:

   *   d_candSols = {(c_+ k1 k2), (c_+ c_x k2), (c_+ k1 c_y), (c_+ c_x c_y)}

   * where k1 and k2 are skolems. Notice that `d_candSols` may contain a

   * pure term that solves the obligation ((c_+ c_x c_y) in this example).

   */

  std::unordered_set<Node> d_candSols;

  /** A set of candidate solutions waiting for this obligation to be solved.

   *

   * In the example above, (c_+ k1 k2) and (c_+ c_x k2) are in the watch-set of

   * k2. Similarly, (c_+ k1 k2) and (c_+ k1 c_y) are in the watch-set of k1.

   */

  std::unordered_set<Node> d_watchSet;

};

/**

 * Print obligation `ob` into the given output stream `out`

 *

 * @param out the output stream to print `ob` into

 * @param ob the obligation to print

 * @return a reference to the given output stream `out`

 */

std::ostream& operator<<(std::ostream& out, const RConsObligation& ob);

}  // namespace quantifiers

}  // namespace theory

}  // namespace cvc5

#endif  // CVC5__THEORY__QUANTIFIERS__RCONS_OBLIGATION_H