src/theory/quantifiers/quantifiers_rewriter.h

   1 /*********************                                                        */
   2 /*! \file quantifiers_rewriter.h
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Andrew Reynolds, Morgan Deters, Andres Noetzli
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS
   8  ** in the top-level source directory) and their institutional affiliations.
   9  ** All rights reserved.  See the file COPYING in the top-level source
  10  ** directory for licensing information.\endverbatim
  11  **
  12  ** \brief Rewriter for the theory of inductive quantifiers
  13  **
  14  ** Rewriter for the theory of inductive quantifiers.
  15  **/
  16
  17 #include "cvc4_private.h"
  18
  19 #ifndef CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
  20 #define CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H
  21
  22 #include "theory/theory_rewriter.h"
  23
  24 namespace CVC4 {
  25 namespace theory {
  26 namespace quantifiers {
  27
  28 struct QAttributes;
  29
  30 /**
  31  * List of steps used by the quantifiers rewriter, details on these steps
  32  * can be found in the class below.
  33  */
  34 enum RewriteStep
  35 {
  36   /** Eliminate symbols (e.g. implies, xor) */
  37   COMPUTE_ELIM_SYMBOLS = 0,
  38   /** Miniscoping */
  39   COMPUTE_MINISCOPING,
  40   /** Aggressive miniscoping */
  41   COMPUTE_AGGRESSIVE_MINISCOPING,
  42   /** Apply the extended rewriter to quantified formula bodies */
  43   COMPUTE_EXT_REWRITE,
  44   /**
  45    * Term processing (e.g. simplifying terms based on ITE lifting,
  46    * eliminating extended arithmetic symbols).
  47    */
  48   COMPUTE_PROCESS_TERMS,
  49   /** Prenexing */
  50   COMPUTE_PRENEX,
  51   /** Variable elimination */
  52   COMPUTE_VAR_ELIMINATION,
  53   /** Conditional splitting */
  54   COMPUTE_COND_SPLIT,
  55   /** Placeholder for end of steps */
  56   COMPUTE_LAST
  57 };
  58 std::ostream& operator<<(std::ostream& out, RewriteStep s);
  59
  60 class QuantifiersRewriter : public TheoryRewriter
  61 {
  62  public:
  63   static bool isLiteral( Node n );
  64   //-------------------------------------variable elimination utilities
  65   /** is variable elimination
  66    *
  67    * Returns true if v is not a subterm of s, and the type of s is a subtype of
  68    * the type of v.
  69    */
  70   static bool isVarElim(Node v, Node s);
  71   /** get variable elimination literal
  72    *
  73    * If n asserted with polarity pol is equivalent to an equality of the form
  74    * v = s for some v in args, where isVariableElim( v, s ) holds, then this
  75    * method removes v from args, adds v to vars, adds s to subs, and returns
  76    * true. Otherwise, it returns false.
  77    */
  78   static bool getVarElimLit(Node n,
  79                             bool pol,
  80                             std::vector<Node>& args,
  81                             std::vector<Node>& vars,
  82                             std::vector<Node>& subs);
  83   /** variable eliminate for bit-vector equalities
  84    *
  85    * If this returns a non-null value ret, then var is updated to a member of
  86    * args, lit is equivalent to ( var = ret ).
  87    */
  88   static Node getVarElimLitBv(Node lit,
  89                               const std::vector<Node>& args,
  90                               Node& var);
  91   /** variable eliminate for string equalities
  92    *
  93    * If this returns a non-null value ret, then var is updated to a member of
  94    * args, lit is equivalent to ( var = ret ).
  95    */
  96   static Node getVarElimLitString(Node lit,
  97                                   const std::vector<Node>& args,
  98                                   Node& var);
  99   /** get variable elimination
 100    *
 101    * If n asserted with polarity pol entails a literal lit that corresponds
 102    * to a variable elimination for some v via the above method, we return true.
 103    * In this case, we update args/vars/subs based on eliminating v.
 104    */
 105   static bool getVarElim(Node n,
 106                          bool pol,
 107                          std::vector<Node>& args,
 108                          std::vector<Node>& vars,
 109                          std::vector<Node>& subs);
 110   /** has variable elimination
 111    *
 112    * Returns true if n asserted with polarity pol entails a literal for
 113    * which variable elimination is possible.
 114    */
 115   static bool hasVarElim(Node n, bool pol, std::vector<Node>& args);
 116   /** compute variable elimination inequality
 117    *
 118    * This method eliminates variables from the body of quantified formula
 119    * "body" using (global) reasoning about inequalities. In particular, if there
 120    * exists a variable x that only occurs in body or annotation qa in literals
 121    * of the form x>=t with a fixed polarity P, then we may replace all such
 122    * literals with P. For example, note that:
 123    *   forall xy. x>y OR P(y) is equivalent to forall y. P(y).
 124    *
 125    * In the case that a variable x from args can be eliminated in this way,
 126    * we remove x from args, add x >= t1, ..., x >= tn to bounds, add false, ...,
 127    * false to subs, and return true.
 128    */
 129   static bool getVarElimIneq(Node body,
 130                              std::vector<Node>& args,
 131                              std::vector<Node>& bounds,
 132                              std::vector<Node>& subs,
 133                              QAttributes& qa);
 134   //-------------------------------------end variable elimination utilities
 135  private:
 136   static int getPurifyIdLit2(Node n, std::map<Node, int>& visited);
 137   static bool addCheckElimChild(std::vector<Node>& children,
 138                                 Node c,
 139                                 Kind k,
 140                                 std::map<Node, bool>& lit_pol,
 141                                 bool& childrenChanged);
 142   static void addNodeToOrBuilder(Node n, NodeBuilder<>& t);
 143   static void computeArgs(const std::vector<Node>& args,
 144                           std::map<Node, bool>& activeMap,
 145                           Node n,
 146                           std::map<Node, bool>& visited);
 147   static void computeArgVec(const std::vector<Node>& args,
 148                             std::vector<Node>& activeArgs,
 149                             Node n);
 150   static void computeArgVec2(const std::vector<Node>& args,
 151                              std::vector<Node>& activeArgs,
 152                              Node n,
 153                              Node ipl);
 154   static Node computeProcessTerms2(Node body,
 155                                    std::map<Node, Node>& cache,
 156                                    std::vector<Node>& new_vars,
 157                                    std::vector<Node>& new_conds,
 158                                    bool elimExtArith);
 159   static void computeDtTesterIteSplit(
 160       Node n,
 161       std::map<Node, Node>& pcons,
 162       std::map<Node, std::map<int, Node> >& ncons,
 163       std::vector<Node>& conj);
 164   /** datatype expand
 165    *
 166    * If v occurs in args and has a datatype type whose index^th constructor is
 167    * C, this method returns a node of the form C( x1, ..., xn ), removes v from
 168    * args and adds x1...xn to args.
 169    */
 170   static Node datatypeExpand(unsigned index, Node v, std::vector<Node>& args);
 171
 172   //-------------------------------------variable elimination
 173   /** compute variable elimination
 174    *
 175    * This computes variable elimination rewrites for a body of a quantified
 176    * formula with bound variables args. This method updates args to args' and
 177    * returns a node body' such that (forall args. body) is equivalent to
 178    * (forall args'. body'). An example of a variable elimination rewrite is:
 179    *   forall xy. x != a V P( x,y ) ---> forall y. P( a, y )
 180    */
 181   static Node computeVarElimination(Node body,
 182                                     std::vector<Node>& args,
 183                                     QAttributes& qa);
 184   //-------------------------------------end variable elimination
 185   //-------------------------------------conditional splitting
 186   /** compute conditional splitting
 187    *
 188    * This computes conditional splitting rewrites for a body of a quantified
 189    * formula with bound variables args. It returns a body' that is equivalent
 190    * to body. We split body into a conjunction if variable elimination can
 191    * occur in one of the conjuncts. Examples of this are:
 192    *   ite( x=a, P(x), Q(x) ) ----> ( x!=a V P(x) ) ^ ( x=a V Q(x) )
 193    *   (x=a) = P(x) ----> ( x!=a V P(x) ) ^ ( x=a V ~P(x) )
 194    *   ( x!=a ^ P(x) ) V Q(x) ---> ( x!=a V Q(x) ) ^ ( P(x) V Q(x) )
 195    * where in each case, x can be eliminated in the first conjunct.
 196    */
 197   static Node computeCondSplit(Node body,
 198                                const std::vector<Node>& args,
 199                                QAttributes& qa);
 200   //-------------------------------------end conditional splitting
 201   //------------------------------------- process terms
 202   /** compute process terms
 203    *
 204    * This takes as input a quantified formula q with attributes qa whose
 205    * body is body.
 206    *
 207    * This rewrite eliminates problematic terms from the bodies of
 208    * quantified formulas, which includes performing:
 209    * - Certain cases of ITE lifting,
 210    * - Elimination of extended arithmetic functions like to_int/is_int/div/mod,
 211    * - Elimination of select over store.
 212    *
 213    * It may introduce new variables V into new_vars and new conditions C into
 214    * new_conds. It returns a node retBody such that q of the form
 215    *   forall X. body
 216    * is equivalent to:
 217    *   forall X, V. ( C => retBody )
 218    */
 219   static Node computeProcessTerms(Node body,
 220                                   std::vector<Node>& new_vars,
 221                                   std::vector<Node>& new_conds,
 222                                   Node q,
 223                                   QAttributes& qa);
 224   //------------------------------------- end process terms
 225   //------------------------------------- extended rewrite
 226   /** compute extended rewrite
 227    *
 228    * This returns the result of applying the extended rewriter on the body
 229    * of quantified formula q.
 230    */
 231   static Node computeExtendedRewrite(Node q);
 232   //------------------------------------- end extended rewrite
 233  public:
 234   static Node computeElimSymbols( Node body );
 235   static Node computeMiniscoping( std::vector< Node >& args, Node body, QAttributes& qa );
 236   static Node computeAggressiveMiniscoping( std::vector< Node >& args, Node body );
 237   /**
 238    * This function removes top-level quantifiers from subformulas of body
 239    * appearing with overall polarity pol. It adds quantified variables that
 240    * appear in positive polarity positions into args, and those at negative
 241    * polarity positions in nargs.
 242    *
 243    * If prenexAgg is true, we ensure that all top-level quantifiers are
 244    * eliminated from subformulas. This means that we must expand ITE and
 245    * Boolean equalities to ensure that quantifiers are at fixed polarities.
 246    *
 247    * For example, calling this function on:
 248    *   (or (forall ((x Int)) (P x z)) (not (forall ((y Int)) (Q y z))))
 249    * would return:
 250    *   (or (P x z) (not (Q y z)))
 251    * and add {x} to args, and {y} to nargs.
 252    */
 253   static Node computePrenex( Node body, std::vector< Node >& args, std::vector< Node >& nargs, bool pol, bool prenexAgg );
 254   /**
 255    * Apply prenexing aggressively. Returns the prenex normal form of n.
 256    */
 257   static Node computePrenexAgg(Node n, std::map<Node, Node>& visited);
 258   static Node computeSplit( std::vector< Node >& args, Node body, QAttributes& qa );
 259 private:
 260  static Node computeOperation(Node f,
 261                               RewriteStep computeOption,
 262                               QAttributes& qa);
 263
 264 public:
 265  RewriteResponse preRewrite(TNode in) override;
 266  RewriteResponse postRewrite(TNode in) override;
 267
 268 private:
 269   /** options */
 270  static bool doOperation(Node f, RewriteStep computeOption, QAttributes& qa);
 271
 272 private:
 273   static Node preSkolemizeQuantifiers(Node n, bool polarity, std::vector< TypeNode >& fvTypes, std::vector<TNode>& fvs);
 274 public:
 275   static bool isPrenexNormalForm( Node n );
 276   /** preprocess
 277    *
 278    * This returns the result of applying simple quantifiers-specific
 279    * preprocessing to n, including but not limited to:
 280    * - rewrite rule elimination,
 281    * - pre-skolemization,
 282    * - aggressive prenexing.
 283    * The argument isInst is set to true if n is an instance of a previously
 284    * registered quantified formula. If this flag is true, we do not apply
 285    * certain steps like pre-skolemization since we know they will have no
 286    * effect.
 287    */
 288   static Node preprocess( Node n, bool isInst = false );
 289   static Node mkForAll( std::vector< Node >& args, Node body, QAttributes& qa );
 290   static Node mkForall( std::vector< Node >& args, Node body, bool marked = false );
 291   static Node mkForall( std::vector< Node >& args, Node body, std::vector< Node >& iplc, bool marked = false );
 292 }; /* class QuantifiersRewriter */
 293
 294 }/* CVC4::theory::quantifiers namespace */
 295 }/* CVC4::theory namespace */
 296 }/* CVC4 namespace */
 297
 298 #endif /* CVC4__THEORY__QUANTIFIERS__QUANTIFIERS_REWRITER_H */
 299
 300