/*********************                                                        */
/*! \file arith_entail.h
 ** \verbatim
 ** Top contributors (to current version):
 **   Andrew Reynolds, Andres Noetzli
 ** This file is part of the CVC4 project.
 ** Copyright (c) 2009-2019 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.\endverbatim
 **
 ** \brief Arithmetic entailment computation for string terms.
 **/

#include "cvc4_private.h"

#ifndef CVC4__THEORY__STRINGS__ARITH_ENTAIL_H
#define CVC4__THEORY__STRINGS__ARITH_ENTAIL_H

#include <vector>

#include "expr/node.h"

namespace CVC4 {
namespace theory {
namespace strings {

/**
 * Techniques for computing arithmetic entailment for string terms. This
 * is an implementation of the techniques from Reynolds et al, "High Level
 * Abstractions for Simplifying Extended String Constraints in SMT", CAV 2019.
 */
class ArithEntail
{
 public:
  /** check arithmetic entailment equal
   * Returns true if it is always the case that a = b.
   */
  static bool checkEq(Node a, Node b);
  /** check arithmetic entailment
   * Returns true if it is always the case that a >= b,
   * and a>b if strict is true.
   */
  static bool check(Node a, Node b, bool strict = false);
  /** check arithmetic entailment
   * Returns true if it is always the case that a >= 0.
   */
  static bool check(Node a, bool strict = false);
  /** check arithmetic entailment with approximations
   *
   * Returns true if it is always the case that a >= 0. We expect that a is in
   * rewritten form.
   *
   * This function uses "approximation" techniques that under-approximate
   * the value of a for the purposes of showing the entailment holds. For
   * example, given:
   *   len( x ) - len( substr( y, 0, len( x ) ) )
   * Since we know that len( substr( y, 0, len( x ) ) ) <= len( x ), the above
   * term can be under-approximated as len( x ) - len( x ) = 0, which is >= 0,
   * and thus the entailment len( x ) - len( substr( y, 0, len( x ) ) ) >= 0
   * holds.
   */
  static bool checkApprox(Node a);

  /**
   * Checks whether assumption |= a >= 0 (if strict is false) or
   * assumption |= a > 0 (if strict is true), where assumption is an equality
   * assumption. The assumption must be in rewritten form.
   *
   * Example:
   *
   * checkWithEqAssumption(x + (str.len y) = 0, -x, false) = true
   *
   * Because: x = -(str.len y), so -x >= 0 --> (str.len y) >= 0 --> true
   */
  static bool checkWithEqAssumption(Node assumption,
                                    Node a,
                                    bool strict = false);

  /**
   * Checks whether assumption |= a >= b (if strict is false) or
   * assumption |= a > b (if strict is true). The function returns true if it
   * can be shown that the entailment holds and false otherwise. Assumption
   * must be in rewritten form. Assumption may be an equality or an inequality.
   *
   * Example:
   *
   * checkWithAssumption(x + (str.len y) = 0, 0, x, false) = true
   *
   * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
   */
  static bool checkWithAssumption(Node assumption,
                                  Node a,
                                  Node b,
                                  bool strict = false);

  /**
   * Checks whether assumptions |= a >= b (if strict is false) or
   * assumptions |= a > b (if strict is true). The function returns true if it
   * can be shown that the entailment holds and false otherwise. Assumptions
   * must be in rewritten form. Assumptions may be an equalities or an
   * inequalities.
   *
   * Example:
   *
   * checkWithAssumptions([x + (str.len y) = 0], 0, x, false) = true
   *
   * Because: x = -(str.len y), so 0 >= x --> 0 >= -(str.len y) --> true
   */
  static bool checkWithAssumptions(std::vector<Node> assumptions,
                                   Node a,
                                   Node b,
                                   bool strict = false);

  /** get arithmetic lower bound
   * If this function returns a non-null Node ret,
   * then ret is a rational constant and
   * we know that n >= ret always if isLower is true,
   * or n <= ret if isLower is false.
   *
   * Notice the following invariant.
   * If getConstantArithBound(a, true) = ret where ret is non-null, then for
   * strict = { true, false } :
   *   ret >= strict ? 1 : 0
   *     if and only if
   *   check( a, strict ) = true.
   */
  static Node getConstantBound(Node a, bool isLower = true);

  /**
   * Given an inequality y1 + ... + yn >= x, removes operands yi s.t. the
   * original inequality still holds. Returns true if the original inequality
   * holds and false otherwise. The list of ys is modified to contain a subset
   * of the original ys.
   *
   * Example:
   *
   * inferZerosInSumGeq( (str.len x), [ (str.len x), (str.len y), 1 ], [] )
   * --> returns true with ys = [ (str.len x) ] and zeroYs = [ (str.len y), 1 ]
   *     (can be used to rewrite the inequality to false)
   *
   * inferZerosInSumGeq( (str.len x), [ (str.len y) ], [] )
   * --> returns false because it is not possible to show
   *     str.len(y) >= str.len(x)
   */
  static bool inferZerosInSumGeq(Node x,
                                 std::vector<Node>& ys,
                                 std::vector<Node>& zeroYs);

 private:
  /** check entail arithmetic internal
   * Returns true if we can show a >= 0 always.
   * a is in rewritten form.
   */
  static bool checkInternal(Node a);
  /** Get arithmetic approximations
   *
   * This gets the (set of) arithmetic approximations for term a and stores
   * them in approx. If isOverApprox is true, these are over-approximations
   * for the value of a, otherwise, they are underapproximations. For example,
   * an over-approximation for len( substr( y, n, m ) ) is m; an
   * under-approximation for indexof( x, y, n ) is -1.
   *
   * Notice that this function is not generally recursive (although it may make
   * a small bounded of recursive calls). Instead, it returns the shape
   * of the approximations for a. For example, an under-approximation
   * for the term len( replace( substr( x, 0, n ), y, z ) ) returned by this
   * function might be len( substr( x, 0, n ) ) - len( y ), where we don't
   * consider (recursively) the approximations for len( substr( x, 0, n ) ).
   */
  static void getArithApproximations(Node a,
                                     std::vector<Node>& approx,
                                     bool isOverApprox = false);
};

}  // namespace strings
}  // namespace theory
}  // namespace CVC4

#endif