GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/quantifiers/single_inv_partition.h Lines: 7 7 100.0 % Date: 2021-03-22 Branches: 5 6 83.3 %

 Line Exec Source 1 /********************* */ 2 /*! \file single_inv_partition.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Andrew Reynolds, Mathias Preiner 6 ** This file is part of the CVC4 project. 7 ** Copyright (c) 2009-2021 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 utility for single invocation partitioning 13 **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H 18 #define CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H 19 20 #include 21 #include 22 23 #include "expr/node.h" 24 #include "expr/type_node.h" 25 26 namespace CVC4 { 27 namespace theory { 28 namespace quantifiers { 29 30 /** single invocation partition 31 * 32 * This is a utility to group formulas into single invocation/non-single 33 * invocation parts, relative to a set of "input functions". 34 * It can be used when either the set of input functions is fixed, 35 * or is unknown. 36 * 37 * (EX1) For example, if input functions are { f }, 38 * then the formula is ( f( x, y ) = g( y ) V f( x, y ) = b ) 39 * is single invocation since there is only one 40 * unique application of f, that is, f( x, y ). 41 * Notice that 42 * exists f. forall xy. f( x, y ) = g( y ) V f( x, y ) = b 43 * is equivalent to: 44 * forall xy. exists z. z = g( y ) V z = b 45 * 46 * When handling multiple input functions, we only infer a formula 47 * is single invocation if all (relevant) input functions have the 48 * same argument types. An input function is relevant if it is 49 * specified by the input in a call to init() or occurs in the 50 * formula we are processing. 51 * 52 * Notice that this class may introduce auxiliary variables to 53 * coerce a formula into being single invocation. For example, 54 * see Example 5 of Reynolds et al. SYNT 2017. 55 * 56 */ 57 class SingleInvocationPartition 58 { 59 public: 60 2200 SingleInvocationPartition() : d_has_input_funcs(false) {} 61 2198 ~SingleInvocationPartition() {} 62 /** initialize this partition for formula n, with input functions funcs 63 * 64 * This initializes this class to check whether formula n is single 65 * invocation with respect to the input functions in funcs only. 66 * Below, the "processed formula" is a formula generated by this 67 * call that is equivalent to n (if this call is successful). 68 * 69 * This method returns true if all input functions have identical 70 * argument types, and false otherwise. Notice that all 71 * access functions below are only valid if this class is 72 * successfully initialized. 73 */ 74 bool init(std::vector& funcs, Node n); 75 76 /** initialize this partition for formula n 77 * 78 * In contrast to the above method, this version assumes that 79 * all uninterpreted functions are input functions. That is, this 80 * method is equivalent to the above function with funcs containing 81 * all uninterpreted functions occurring in n. 82 */ 83 bool init(Node n); 84 85 /** is the processed formula purely single invocation? 86 * 87 * A formula is purely single invocation if it is equivalent to: 88 * t[ f1( x ), ..., fn( x ), x ], 89 * for some F, where f1...fn are the input functions. 90 * Notice that the free variables of t are exactly x. 91 */ 92 488 bool isPurelySingleInvocation() { return d_conjuncts[1].empty(); } 93 /** is the processed formula non-ground single invocation? 94 * 95 * A formula is non-ground single invocation if it is equivalent to: 96 * F[ f1( x ), ..., fn( x ), x, y ], 97 * for some F, where f1...fn are the input functions. 98 */ 99 4 bool isNonGroundSingleInvocation() 100 { 101 4 return d_conjuncts[3].size() == d_conjuncts[1].size(); 102 } 103 104 /** Get the (portion of) the processed formula that is single invocation 105 * 106 * Notice this method returns the anti-skolemized version of the input 107 * formula. In (EX1), this method returns: 108 * z = g( y ) V z = b 109 * where z is the first-order variable for f (see 110 * getFirstOrderVariableForFunction). 111 */ 112 130 Node getSingleInvocation() { return getConjunct(0); } 113 /** Get the (portion of) the processed formula that is not single invocation 114 * 115 * This formula and the above form a partition of the conjuncts of the 116 * processed formula, that is: 117 * getSingleInvocation() * sigma ^ getNonSingleInvocation() 118 * is equivalent to the processed formula, where sigma is a substitution of 119 * the form: 120 * z_1 -> f_1( x ) .... z_n -> f_n( x ) 121 * where z_i are the first-order variables for input functions f_i 122 * for all i=1,...,n, and x are the single invocation arguments of the input 123 * formulas (see d_si_vars). 124 */ 125 Node getNonSingleInvocation() { return getConjunct(1); } 126 /** get full specification 127 * 128 * This returns getSingleInvocation() * sigma ^ getNonSingleInvocation(), 129 * which is equivalent to the processed formula, where sigma is the 130 * substitution described above. 131 */ 132 4 Node getFullSpecification() { return getConjunct(2); } 133 /** get first order variable for input function f 134 * 135 * This corresponds to the variable that we used when anti-skolemizing 136 * function f. For example, in (EX1), if getSingleInvocation() returns: 137 * z = g( y ) V z = b 138 * Then, getFirstOrderVariableForFunction(f) = z. 139 */ 140 Node getFirstOrderVariableForFunction(Node f) const; 141 142 /** get function for first order variable 143 * 144 * Opposite direction of above, where: 145 * getFunctionForFirstOrderVariable(z) = f. 146 */ 147 Node getFunctionForFirstOrderVariable(Node v) const; 148 149 /** get function invocation for 150 * 151 * Returns f( x ) where x are the single invocation arguments of the input 152 * formulas (see d_si_vars). If f is not an input function, it returns null. 153 */ 154 Node getFunctionInvocationFor(Node f) const; 155 156 /** get single invocation variables, appends them to sivars */ 157 void getSingleInvocationVariables(std::vector& sivars) const; 158 159 /** get all variables 160 * 161 * Appends all free variables of the processed formula to vars. 162 */ 163 void getAllVariables(std::vector& vars) const; 164 165 /** get function variables 166 * 167 * Appends all first-order variables corresponding to input functions to 168 * fvars. 169 */ 170 void getFunctionVariables(std::vector& fvars) const; 171 172 /** get functions 173 * 174 * Gets all input functions. This has the same order as the list of 175 * function variables above. 176 */ 177 void getFunctions(std::vector& fs) const; 178 179 /** print debugging information on Trace c */ 180 void debugPrint(const char* c); 181 182 private: 183 /** map from input functions to whether they have an anti-skolemizable type 184 * An anti-skolemizable type is one of the form: 185 * ( T1, ..., Tn ) -> T 186 * where Ti = d_arg_types[i] for i = 1,...,n. 187 */ 188 std::map d_funcs; 189 190 /** map from functions to the invocation we inferred for them */ 191 std::map d_func_inv; 192 193 /** the list of first-order variables for functions 194 * In (EX1), this is the list { z }. 195 */ 196 std::vector d_func_vars; 197 198 /** the arguments that we based the anti-skolemization on. 199 * In (EX1), this is the list { x, y }. 200 */ 201 std::vector d_si_vars; 202 203 /** every free variable of conjuncts[2] */ 204 std::unordered_set d_all_vars; 205 /** map from functions to first-order variables that anti-skolemized them */ 206 std::map d_func_fo_var; 207 /** map from first-order variables to the function it anti-skolemized */ 208 std::map d_fo_var_to_func; 209 210 /** The argument types for this single invocation partition. 211 * These are the argument types of the input functions we are 212 * processing, where notice that: 213 * d_si_vars[i].getType()==d_arg_types[i] 214 */ 215 std::vector d_arg_types; 216 217 /** the list of conjuncts with various properties : 218 * 0 : the single invocation conjuncts (stored in anti-skolemized form), 219 * 1 : the non-single invocation conjuncts, 220 * 2 : all conjuncts, 221 * 3 : non-ground single invocation conjuncts. 222 */ 223 std::vector d_conjuncts[4]; 224 225 /** did we initialize this class with input functions? */ 226 bool d_has_input_funcs; 227 /** the input functions we initialized this class with */ 228 std::vector d_input_funcs; 229 /** all input functions */ 230 std::vector d_all_funcs; 231 /** skolem of the same type as input functions */ 232 std::vector d_input_func_sks; 233 234 /** infer the argument types of uninterpreted function applications 235 * 236 * If this method returns true, then typs contains the list of types of 237 * the arguments (in order) of all uninterpreted functions in n. 238 * If this method returns false, then there exists (at least) two 239 * uninterpreted functions in n whose argument types are not identical. 240 */ 241 bool inferArgTypes(Node n, 242 std::vector& typs, 243 std::map& visited); 244 245 /** is anti-skolemizable type 246 * 247 * This method returns true if f's argument types are equal to the 248 * argument types we have fixed in this class (see d_arg_types). 249 */ 250 bool isAntiSkolemizableType(Node f); 251 252 /** 253 * This is the entry point for initializing this class, 254 * which is called by the public init(...) methods. 255 * funcs are the input functions (if any were explicitly provide), 256 * typs is the types of the arguments of funcs, 257 * n is the formula to process, 258 * has_funcs is whether input functions were explicitly provided. 259 */ 260 bool init(std::vector& funcs, 261 std::vector& typs, 262 Node n, 263 bool has_funcs); 264 265 /** 266 * Collect the top-level conjuncts of the formula (equivalent to) 267 * n or the negation of n if pol=false, and store them in conj. 268 */ 269 bool collectConjuncts(Node n, bool pol, std::vector& conj); 270 271 /** process conjunct n 272 * 273 * This function is called when n is a top-level conjunction in a 274 * formula that is equivalent to the input formula given to this 275 * class via init. 276 * 277 * args : stores the arguments (if any) that we have seen in an application 278 * of an application of an input function in this conjunct. 279 * terms/subs : this stores a term substitution with entries of the form: 280 * f(args) -> z 281 * where z is the first-order variable for input function f. 282 */ 283 bool processConjunct(Node n, 284 std::map& visited, 285 std::vector& args, 286 std::vector& terms, 287 std::vector& subs); 288 289 /** get the and node corresponding to d_conjuncts[index] */ 290 Node getConjunct(int index); 291 }; 292 293 } /* namespace CVC4::theory::quantifiers */ 294 } /* namespace CVC4::theory */ 295 } /* namespace CVC4 */ 296 297 #endif /* CVC4__THEORY__QUANTIFIERS__SINGLE_INV_PARTITION_H */

 Generated by: GCOVR (Version 3.2)