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

 * Top contributors (to current version):

 *   Mudathir Mohamed, Andrew Reynolds, Gereon Kremer

 *

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

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

 *

 * Inference generator utility.

 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H

#define CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H

#include "expr/node.h"

#include "infer_info.h"

namespace cvc5 {

namespace theory {

namespace bags {

class InferenceManager;

class SolverState;

/**

 * An inference generator class. This class is used by the core solver to

 * generate lemmas

 */

{

 public:

  InferenceGenerator(SolverState* state, InferenceManager* im);

  /**

   * @param A is a bag of type (Bag E)

   * @param e is a node of type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (>= (bag.count e A) 0)

   */

  InferInfo nonNegativeCount(Node n, Node e);

  /**

   * @param n is (bag x c) of type (Bag E)

   * @param e is a node of type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (= (bag.count e skolem) c))

   *   if e is exactly node x. Node skolem is a fresh variable equals (bag x c).

   *   Otherwise the following inference is returned

   * (=>

   *   true

   *   (= (bag.count e skolem) (ite (= e x) c 0)))

   */

  InferInfo mkBag(Node n, Node e);

  /**

   * @param n is (= A B) where A, B are bags of type (Bag E), and

   * (not (= A B)) is an assertion in the equality engine

   * @return an inference that represents the following implication

   * (=>

   *   (not (= A B))

   *   (not (= (count e A) (count e B))))

   *   where e is a fresh skolem of type E.

   */

  InferInfo bagDisequality(Node n);

  /**

   * @param n is (as emptybag (Bag E))

   * @param e is a node of Type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (= 0 (count e skolem)))

   *   where skolem = (as emptybag (Bag String))

   */

  InferInfo empty(Node n, Node e);

  /**

   * @param n is (union_disjoint A B) where A, B are bags of type (Bag E)

   * @param e is a node of Type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (= (count e skolem)

   *      (+ (count e A) (count e B))))

   *  where skolem is a fresh variable equals (union_disjoint A B)

   */

  InferInfo unionDisjoint(Node n, Node e);

  /**

   * @param n is (union_disjoint A B) where A, B are bags of type (Bag E)

   * @param e is a node of Type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (=

   *     (count e skolem)

   *     (ite

   *       (> (count e A) (count e B))

   *       (count e A)

   *       (count e B)))))

   * where skolem is a fresh variable equals (union_max A B)

   */

  InferInfo unionMax(Node n, Node e);

  /**

   * @param n is (intersection_min A B) where A, B are bags of type (Bag E)

   * @param e is a node of Type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (=

   *     (count e skolem)

   *     (ite(

   *       (< (count e A) (count e B))

   *       (count e A)

   *       (count e B)))))

   * where skolem is a fresh variable equals (intersection_min A B)

   */

  InferInfo intersection(Node n, Node e);

  /**

   * @param n is (difference_subtract A B) where A, B are bags of type (Bag E)

   * @param e is a node of Type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (=

   *     (count e skolem)

   *     (ite

   *       (>= (count e A) (count e B))

   *       (- (count e A) (count e B))

   *       0))))

   * where skolem is a fresh variable equals (difference_subtract A B)

   */

  InferInfo differenceSubtract(Node n, Node e);

  /**

   * @param n is (difference_remove A B) where A, B are bags of type (Bag E)

   * @param e is a node of Type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (=

   *     (count e skolem)

   *     (ite

   *       (= (count e B) 0)

   *       (count e A)

   *       0))))

   * where skolem is a fresh variable equals (difference_remove A B)

   */

  InferInfo differenceRemove(Node n, Node e);

  /**

   * @param n is (duplicate_removal A) where A is a bag of type (Bag E)

   * @param e is a node of Type E

   * @return an inference that represents the following implication

   * (=>

   *   true

   *   (=

   *    (count e skolem)

   *    (ite (>= (count e A) 1) 1 0))))

   * where skolem is a fresh variable equals (duplicate_removal A)

   */

  InferInfo duplicateRemoval(Node n, Node e);

  /**

   * @param element of type T

   * @param bag of type (bag T)

   * @return  a count term (bag.count element bag)

   */

  Node getMultiplicityTerm(Node element, Node bag);

 private:

  /** generate skolem variable for node n and add it to inferInfo */

  Node getSkolem(Node& n, InferInfo& inferInfo);

  NodeManager* d_nm;

  SkolemManager* d_sm;

  SolverState* d_state;

  /** Pointer to the inference manager */

  InferenceManager* d_im;

  /** Commonly used constants */

  Node d_true;

  Node d_zero;

  Node d_one;

};

}  // namespace bags

}  // namespace theory

}  // namespace cvc5

#endif /* CVC5__THEORY__BAGS__INFERENCE_GENERATOR_H */