path: root/src/theory/quantifiers/extended_rewrite.h

/******************************************************************************
 * Top contributors (to current version):
 *   Andrew Reynolds, Mathias Preiner
 *
 * 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.
 * ****************************************************************************
 *
 * extended rewriting class
 */

#include "cvc5_private.h"

#ifndef CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H
#define CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H

#include <unordered_map>

#include "expr/node.h"

namespace cvc5 {
namespace theory {

class Rewriter;

namespace quantifiers {

/** Extended rewriter
 *
 * This class is used for all rewriting that is not necessarily
 * helpful for quantifier-free solving, but is helpful
 * in other use cases. An example of this is SyGuS, where rewriting
 * can be used for generalizing refinement lemmas, and hence
 * should be highly aggressive.
 *
 * This class extended the standard techniques for rewriting
 * with techniques, including but not limited to:
 * - Redundant child elimination,
 * - Sorting children of commutative operators,
 * - Boolean constraint propagation,
 * - Equality chain normalization,
 * - Negation normal form,
 * - Simple ITE pulling,
 * - ITE conditional variable elimination,
 * - ITE condition subsumption.
 */
class ExtendedRewriter
{
 public:
  ExtendedRewriter(Rewriter& rew, bool aggr = true);
  ~ExtendedRewriter() {}
  /** return the extended rewritten form of n */
  Node extendedRewrite(Node n) const;

 private:
  /** The underlying rewriter that we are extending  */
  Rewriter& d_rew;
  /** cache that the extended rewritten form of n is ret */
  void setCache(Node n, Node ret) const;
  /** get the cache for n */
  Node getCache(Node n) const;
  /** add to children
   *
   * Adds nc to the vector of children, if dropDup is true, we do not add
   * nc if it already occurs in children. This method returns false in this
   * case, otherwise it returns true.
   */
  bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup) const;

  //--------------------------------------generic utilities
  /** Rewrite ITE, for example:
   *
   * ite( ~C, s, t ) ---> ite( C, t, s )
   * ite( A or B, s, t ) ---> ite( ~A and ~B, t, s )
   * ite( x = c, x, t ) --> ite( x = c, c, t )
   * t * { x -> c } = s => ite( x = c, s, t ) ---> t
   *
   * The parameter "full" indicates an effort level that this rewrite will
   * take. If full is false, then we do only perform rewrites that
   * strictly decrease the term size of n.
   */
  Node extendedRewriteIte(Kind itek, Node n, bool full = true) const;
  /** Rewrite AND/OR
   *
   * This implements BCP, factoring, and equality resolution for the Boolean
   * term n whose top symbolic is AND/OR.
   */
  Node extendedRewriteAndOr(Node n) const;
  /** Pull ITE, for example:
   *
   *   D=C2 ---> false
   *     implies
   *   D=ite( C, C1, C2 ) --->  C ^ D=C1
   *
   *   f(t,t1) --> s  and  f(t,t2)---> s
   *     implies
   *   f(t,ite(C,t1,t2)) ---> s
   *
   * If this function returns a non-null node ret, then n ---> ret.
   */
  Node extendedRewritePullIte(Kind itek, Node n) const;
  /** Negation Normal Form (NNF), for example:
   *
   *   ~( A & B ) ---> ( ~ A | ~B )
   *   ~( ite( A, B, C ) ---> ite( A, ~B, ~C )
   *
   * If this function returns a non-null node ret, then n ---> ret.
   */
  Node extendedRewriteNnf(Node n) const;
  /** (type-independent) Boolean constraint propagation, for example:
   *
   *   ~A & ( B V A ) ---> ~A & B
   *   A & ( B = ( A V C ) ) ---> A & B
   *
   * This function takes as arguments the kinds that specify AND, OR, and NOT.
   * It additionally takes as argument a map bcp_kinds. If this map is
   * non-empty, then all terms that have a Kind that is *not* in this map should
   * be treated as immutable. This is for instance to prevent propagation
   * beneath illegal terms. As an example:
   *   (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but
   *   (bvand A (bvadd A B)) is not equivalent to (bvand A (bvadd 1..1 B)),
   * hence, when using this function to do BCP for bit-vectors, we have that
   * BITVECTOR_AND is a bcp_kind, but BITVECTOR_ADD is not.
   *
   * If this function returns a non-null node ret, then n ---> ret.
   */
  Node extendedRewriteBcp(Kind andk,
                          Kind ork,
                          Kind notk,
                          std::map<Kind, bool>& bcp_kinds,
                          Node n) const;
  /** (type-independent) factoring, for example:
   *
   *   ( A V B ) ^ ( A V C ) ----> A V ( B ^ C )
   *   ( A ^ B ) V ( A ^ C ) ----> A ^ ( B V C )
   *
   * This function takes as arguments the kinds that specify AND, OR, NOT.
   * We assume that the children of n do not contain duplicates.
   */
  Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n) const;
  /** (type-independent) equality resolution, for example:
   *
   *   ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B )
   *   ( A V ~B ) & ( A = B ) ----> ( A = B )
   *   ( A V B ) & ( A xor B ) ----> ( A xor B )
   *   ( A & B ) V ( A xor B ) ----> B V ( A xor B )
   *
   * This function takes as arguments the kinds that specify AND, OR, EQUAL,
   * and NOT. The equal kind eqk is interpreted as XOR if isXor is true.
   * It additionally takes as argument a map bcp_kinds, which
   * serves the same purpose as the above function.
   * If this function returns a non-null node ret, then n ---> ret.
   */
  Node extendedRewriteEqRes(Kind andk,
                            Kind ork,
                            Kind eqk,
                            Kind notk,
                            std::map<Kind, bool>& bcp_kinds,
                            Node n,
                            bool isXor = false) const;
  /** (type-independent) Equality chain rewriting, for example:
   *
   *   A = ( A = B ) ---> B
   *   ( A = D ) = ( C = B ) ---> A = ( B = ( C = D ) )
   *   A = ( A & B ) ---> ~A | B
   *
   * If this function returns a non-null node ret, then n ---> ret.
   * This function takes as arguments the kinds that specify EQUAL, AND, OR,
   * and NOT. If the flag isXor is true, the eqk is treated as XOR.
   */
  Node extendedRewriteEqChain(Kind eqk,
                              Kind andk,
                              Kind ork,
                              Kind notk,
                              Node n,
                              bool isXor = false) const;
  /** extended rewrite aggressive
   *
   * All aggressive rewriting techniques (those that should be prioritized
   * at a lower level) go in this function.
   */
  Node extendedRewriteAggr(Node n) const;
  /** Decompose right associative chain
   *
   * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and
   * appends t1...tn to children.
   */
  Node decomposeRightAssocChain(Kind k,
                                Node n,
                                std::vector<Node>& children) const;
  /** Make right associative chain
   *
   * Sorts children to obtain list { tn...t1 }, and returns the term
   * f( ... f( f( base, tn ), t{n-1} ) ... t1 ).
   */
  Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children) const;
  /** Partial substitute
   *
   * Applies the substitution specified by assign to n, recursing only beneath
   * terms whose Kind appears in rkinds (when rkinds is empty), and additionally
   * never recursing beneath WITNESS.
   */
  Node partialSubstitute(Node n,
                         const std::map<Node, Node>& assign,
                         const std::map<Kind, bool>& rkinds) const;
  /** same as above, with vectors */
  Node partialSubstitute(Node n,
                         const std::vector<Node>& vars,
                         const std::vector<Node>& subs,
                         const std::map<Kind, bool>& rkinds) const;
  /** solve equality
   *
   * If this function returns a non-null node n', then n' is equivalent to n
   * and is of the form that can be used by inferSubstitution below.
   */
  Node solveEquality(Node n) const;
  /** infer substitution
   *
   * If n is an equality of the form x = t, where t is either:
   * (1) a constant, or
   * (2) a variable y such that x < y based on an ordering,
   * then this method adds x to vars and y to subs and return true, otherwise
   * it returns false.
   * If usePred is true, we may additionally add n -> true, or n[0] -> false
   * is n is a negation.
   */
  bool inferSubstitution(Node n,
                         std::vector<Node>& vars,
                         std::vector<Node>& subs,
                         bool usePred = false) const;
  /** extended rewrite
   *
   * Prints debug information, indicating the rewrite n ---> ret was found.
   */
  void debugExtendedRewrite(Node n, Node ret, const char* c) const;
  //--------------------------------------end generic utilities

  //--------------------------------------theory-specific top-level calls
  /** extended rewrite strings
   *
   * If this method returns a non-null node ret', then ret is equivalent to
   * ret'.
   */
  Node extendedRewriteStrings(Node ret) const;
  //--------------------------------------end theory-specific top-level calls

  /**
   * Whether this extended rewriter applies aggressive rewriting techniques,
   * which are more expensive. Examples of aggressive rewriting include:
   * - conditional rewriting,
   * - condition merging,
   * - sorting childing of commutative operators with more than 5 children.
   *
   * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting
   * may be applied as a preprocessing step.
   */
  bool d_aggr;
  /** Common constant nodes */
  Node d_true;
  Node d_false;
  Node d_zero;
};

}  // namespace quantifiers
}  // namespace theory
}  // namespace cvc5

#endif /* CVC5__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */