1 /********************* */ 2 /*! \file extended_rewrite.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2019 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 extended rewriting class 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H 18 #define __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H 19 20 #include <unordered_map> 21 22 #include "expr/node.h" 23 24 namespace CVC4 { 25 namespace theory { 26 namespace quantifiers { 27 28 /** Extended rewriter 29 * 30 * This class is used for all rewriting that is not necessarily 31 * helpful for quantifier-free solving, but is helpful 32 * in other use cases. An example of this is SyGuS, where rewriting 33 * can be used for generalizing refinement lemmas, and hence 34 * should be highly aggressive. 35 * 36 * This class extended the standard techniques for rewriting 37 * with techniques, including but not limited to: 38 * - Redundant child elimination, 39 * - Sorting children of commutative operators, 40 * - Boolean constraint propagation, 41 * - Equality chain normalization, 42 * - Negation normal form, 43 * - Simple ITE pulling, 44 * - ITE conditional variable elimination, 45 * - ITE condition subsumption. 46 */ 47 class ExtendedRewriter 48 { 49 public: 50 ExtendedRewriter(bool aggr = true); ~ExtendedRewriter()51 ~ExtendedRewriter() {} 52 /** return the extended rewritten form of n */ 53 Node extendedRewrite(Node n); 54 55 private: 56 /** 57 * Whether this extended rewriter applies aggressive rewriting techniques, 58 * which are more expensive. Examples of aggressive rewriting include: 59 * - conditional rewriting, 60 * - condition merging, 61 * - sorting childing of commutative operators with more than 5 children. 62 * 63 * Aggressive rewriting is applied for SyGuS, whereas non-aggressive rewriting 64 * may be applied as a preprocessing step. 65 */ 66 bool d_aggr; 67 /** true/false nodes */ 68 Node d_true; 69 Node d_false; 70 /** cache that the extended rewritten form of n is ret */ 71 void setCache(Node n, Node ret); 72 /** add to children 73 * 74 * Adds nc to the vector of children, if dropDup is true, we do not add 75 * nc if it already occurs in children. This method returns false in this 76 * case, otherwise it returns true. 77 */ 78 bool addToChildren(Node nc, std::vector<Node>& children, bool dropDup); 79 80 //--------------------------------------generic utilities 81 /** Rewrite ITE, for example: 82 * 83 * ite( ~C, s, t ) ---> ite( C, t, s ) 84 * ite( A or B, s, t ) ---> ite( ~A and ~B, t, s ) 85 * ite( x = c, x, t ) --> ite( x = c, c, t ) 86 * t * { x -> c } = s => ite( x = c, s, t ) ---> t 87 * 88 * The parameter "full" indicates an effort level that this rewrite will 89 * take. If full is false, then we do only perform rewrites that 90 * strictly decrease the term size of n. 91 */ 92 Node extendedRewriteIte(Kind itek, Node n, bool full = true); 93 /** Rewrite AND/OR 94 * 95 * This implements BCP, factoring, and equality resolution for the Boolean 96 * term n whose top symbolic is AND/OR. 97 */ 98 Node extendedRewriteAndOr(Node n); 99 /** Pull ITE, for example: 100 * 101 * D=C2 ---> false 102 * implies 103 * D=ite( C, C1, C2 ) ---> C ^ D=C1 104 * 105 * f(t,t1) --> s and f(t,t2)---> s 106 * implies 107 * f(t,ite(C,t1,t2)) ---> s 108 * 109 * If this function returns a non-null node ret, then n ---> ret. 110 */ 111 Node extendedRewritePullIte(Kind itek, Node n); 112 /** Negation Normal Form (NNF), for example: 113 * 114 * ~( A & B ) ---> ( ~ A | ~B ) 115 * ~( ite( A, B, C ) ---> ite( A, ~B, ~C ) 116 * 117 * If this function returns a non-null node ret, then n ---> ret. 118 */ 119 Node extendedRewriteNnf(Node n); 120 /** (type-independent) Boolean constraint propagation, for example: 121 * 122 * ~A & ( B V A ) ---> ~A & B 123 * A & ( B = ( A V C ) ) ---> A & B 124 * 125 * This function takes as arguments the kinds that specify AND, OR, and NOT. 126 * It additionally takes as argument a map bcp_kinds. If this map is 127 * non-empty, then all terms that have a Kind that is *not* in this map should 128 * be treated as immutable. This is for instance to prevent propagation 129 * beneath illegal terms. As an example: 130 * (bvand A (bvor A B)) is equivalent to (bvand A (bvor 1...1 B)), but 131 * (bvand A (bvplus A B)) is not equivalent to (bvand A (bvplus 1..1 B)), 132 * hence, when using this function to do BCP for bit-vectors, we have that 133 * BITVECTOR_AND is a bcp_kind, but BITVECTOR_PLUS is not. 134 * 135 * If this function returns a non-null node ret, then n ---> ret. 136 */ 137 Node extendedRewriteBcp( 138 Kind andk, Kind ork, Kind notk, std::map<Kind, bool>& bcp_kinds, Node n); 139 /** (type-independent) factoring, for example: 140 * 141 * ( A V B ) ^ ( A V C ) ----> A V ( B ^ C ) 142 * ( A ^ B ) V ( A ^ C ) ----> A ^ ( B V C ) 143 * 144 * This function takes as arguments the kinds that specify AND, OR, NOT. 145 * We assume that the children of n do not contain duplicates. 146 */ 147 Node extendedRewriteFactoring(Kind andk, Kind ork, Kind notk, Node n); 148 /** (type-independent) equality resolution, for example: 149 * 150 * ( A V C ) & ( A = B ) ---> ( B V C ) & ( A = B ) 151 * ( A V ~B ) & ( A = B ) ----> ( A = B ) 152 * ( A V B ) & ( A xor B ) ----> ( A xor B ) 153 * ( A & B ) V ( A xor B ) ----> B V ( A xor B ) 154 * 155 * This function takes as arguments the kinds that specify AND, OR, EQUAL, 156 * and NOT. The equal kind eqk is interpreted as XOR if isXor is true. 157 * It additionally takes as argument a map bcp_kinds, which 158 * serves the same purpose as the above function. 159 * If this function returns a non-null node ret, then n ---> ret. 160 */ 161 Node extendedRewriteEqRes(Kind andk, 162 Kind ork, 163 Kind eqk, 164 Kind notk, 165 std::map<Kind, bool>& bcp_kinds, 166 Node n, 167 bool isXor = false); 168 /** (type-independent) Equality chain rewriting, for example: 169 * 170 * A = ( A = B ) ---> B 171 * ( A = D ) = ( C = B ) ---> A = ( B = ( C = D ) ) 172 * A = ( A & B ) ---> ~A | B 173 * 174 * If this function returns a non-null node ret, then n ---> ret. 175 * This function takes as arguments the kinds that specify EQUAL, AND, OR, 176 * and NOT. If the flag isXor is true, the eqk is treated as XOR. 177 */ 178 Node extendedRewriteEqChain( 179 Kind eqk, Kind andk, Kind ork, Kind notk, Node n, bool isXor = false); 180 /** extended rewrite aggressive 181 * 182 * All aggressive rewriting techniques (those that should be prioritized 183 * at a lower level) go in this function. 184 */ 185 Node extendedRewriteAggr(Node n); 186 /** Decompose right associative chain 187 * 188 * For term f( ... f( f( base, tn ), t{n-1} ) ... t1 ), returns term base, and 189 * appends t1...tn to children. 190 */ 191 Node decomposeRightAssocChain(Kind k, Node n, std::vector<Node>& children); 192 /** Make right associative chain 193 * 194 * Sorts children to obtain list { tn...t1 }, and returns the term 195 * f( ... f( f( base, tn ), t{n-1} ) ... t1 ). 196 */ 197 Node mkRightAssocChain(Kind k, Node base, std::vector<Node>& children); 198 /** Partial substitute 199 * 200 * Applies the substitution specified by assign to n, recursing only beneath 201 * terms whose Kind appears in rec_kinds. 202 */ 203 Node partialSubstitute(Node n, 204 std::map<Node, Node>& assign, 205 std::map<Kind, bool>& rkinds); 206 /** solve equality 207 * 208 * If this function returns a non-null node n', then n' is equivalent to n 209 * and is of the form that can be used by inferSubstitution below. 210 */ 211 Node solveEquality(Node n); 212 /** infer substitution 213 * 214 * If n is an equality of the form x = t, where t is either: 215 * (1) a constant, or 216 * (2) a variable y such that x < y based on an ordering, 217 * then this method adds x to vars and y to subs and return true, otherwise 218 * it returns false. 219 * If usePred is true, we may additionally add n -> true, or n[0] -> false 220 * is n is a negation. 221 */ 222 bool inferSubstitution(Node n, 223 std::vector<Node>& vars, 224 std::vector<Node>& subs, 225 bool usePred = false); 226 /** extended rewrite 227 * 228 * Prints debug information, indicating the rewrite n ---> ret was found. 229 */ 230 inline void debugExtendedRewrite(Node n, Node ret, const char* c) const; 231 //--------------------------------------end generic utilities 232 233 //--------------------------------------theory-specific top-level calls 234 /** extended rewrite arith 235 * 236 * If this method returns a non-null node ret', then ret is equivalent to 237 * ret'. 238 */ 239 Node extendedRewriteArith(Node ret); 240 /** extended rewrite strings 241 * 242 * If this method returns a non-null node ret', then ret is equivalent to 243 * ret'. 244 */ 245 Node extendedRewriteStrings(Node ret); 246 //--------------------------------------end theory-specific top-level calls 247 }; 248 249 } /* CVC4::theory::quantifiers namespace */ 250 } /* CVC4::theory namespace */ 251 } /* CVC4 namespace */ 252 253 #endif /* __CVC4__THEORY__QUANTIFIERS__EXTENDED_REWRITE_H */ 254