1 /********************* */ 2 /*! \file sygus_process_conj.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 Techniqures for static preprocessing and analysis of 13 ** sygus conjectures. 14 **/ 15 16 #include "cvc4_private.h" 17 18 #ifndef __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H 19 #define __CVC4__THEORY__QUANTIFIERS__SYGUS_PROCESS_CONJ_H 20 21 #include <map> 22 #include <unordered_map> 23 #include <unordered_set> 24 #include <vector> 25 26 #include "expr/node.h" 27 #include "expr/type_node.h" 28 #include "theory/quantifiers_engine.h" 29 30 namespace CVC4 { 31 namespace theory { 32 namespace quantifiers { 33 34 /** This file contains techniques that compute 35 * argument relevancy for synthesis functions 36 * 37 * Let F be a synthesis conjecture of the form: 38 * exists f. forall X. P( f, X ) 39 * 40 * The classes below compute whether certain arguments of 41 * the function-to-synthesize f are irrelevant. 42 * Assume that f is a binary function, where possible solutions 43 * to the above conjecture are of the form: 44 * f -> (lambda (xy) t[x,y]) 45 * We say e.g. that the 2nd argument of f is irrelevant if we 46 * can determine: 47 * F has a solution 48 * if and only if 49 * F has a solution of the form f -> (lambda (xy) t[x] ) 50 * We conclude that arguments are irrelevant using the following 51 * techniques. 52 * 53 * 54 * (1) Argument invariance: 55 * 56 * Let s[z] be a term whose free variables are contained in { z }. 57 * If all occurrences of f-applications in F are of the form: 58 * f(t, s[t]) 59 * then: 60 * f = (lambda (xy) r[x,y]) 61 * is a solution to F only if: 62 * f = (lambda (xy) r[x,s[x]]) 63 * is as well. 64 * Hence the second argument of f is not relevant. 65 * 66 * 67 * (2) Variable irrelevance: 68 * 69 * If F is equivalent to: 70 * exists f. forall w z u1...un. C1 ^...^Cm, 71 * where for i=1...m, Ci is of the form: 72 * ( w1 = f(tm1[z], u1) ^ 73 * ... ^ 74 * wn = f(tmn[z], un) ) => Pm(w1...wn, z) 75 * then the second argument of f is irrelevant. 76 * We call u1...un single occurrence variables 77 * (in Ci). 78 * 79 * 80 * TODO (#1210) others, generalize (2)? 81 * 82 */ 83 84 /** This structure stores information regarding 85 * an argument of a function to synthesize. 86 * 87 * It is used to store whether the argument 88 * position in the function to synthesize is 89 * relevant. 90 */ 91 class SynthConjectureProcessArg 92 { 93 public: SynthConjectureProcessArg()94 SynthConjectureProcessArg() : d_var_single_occ(false), d_relevant(false) {} 95 /** template definition 96 * This is the term s[z] described 97 * under "Argument Invariance" above. 98 */ 99 Node d_template; 100 /** single occurrence 101 * Whether we are trying to show this argument 102 * is irrelevant by "Variable irrelevance" 103 * described above. 104 */ 105 bool d_var_single_occ; 106 /** whether this argument is relevant 107 * An argument is marked as relevant if: 108 * (A) it is explicitly marked as relevant 109 * due to a function application containing 110 * a relevant term at this argument position, or 111 * (B) if it is given conflicting template definitions. 112 */ 113 bool d_relevant; 114 }; 115 116 /** This structure stores information regarding conjecture-specific 117 * analysis of a single function to synthesize within 118 * a conjecture to synthesize. 119 * 120 * It maintains information about each of the function to 121 * synthesize's arguments. 122 */ 123 struct SynthConjectureProcessFun 124 { 125 public: SynthConjectureProcessFunSynthConjectureProcessFun126 SynthConjectureProcessFun() {} ~SynthConjectureProcessFunSynthConjectureProcessFun127 ~SynthConjectureProcessFun() {} 128 /** initialize this class for function f */ 129 void init(Node f); 130 /** process terms 131 * 132 * This is called once per conjunction in 133 * the synthesis conjecture. 134 * 135 * ns are the f-applications to process, 136 * ks are the variables we introduced to flatten them, 137 * nf is the flattened form of our conjecture to process, 138 * free_vars maps all subterms of n and nf to the set 139 * of variables (in set synth_fv) they contain. 140 * 141 * This updates information regarding which arguments 142 * of the function-to-synthesize are relevant. 143 */ 144 void processTerms( 145 std::vector<Node>& ns, 146 std::vector<Node>& ks, 147 Node nf, 148 std::unordered_set<Node, NodeHashFunction>& synth_fv, 149 std::unordered_map<Node, 150 std::unordered_set<Node, NodeHashFunction>, 151 NodeHashFunction>& free_vars); 152 /** is the i^th argument of the function-to-synthesize of this class relevant? 153 */ 154 bool isArgRelevant(unsigned i); 155 /** get irrelevant arguments for the function-to-synthesize of this class */ 156 void getIrrelevantArgs(std::unordered_set<unsigned>& args); 157 158 private: 159 /** the synth fun associated with this */ 160 Node d_synth_fun; 161 /** properties of each argument */ 162 std::vector<SynthConjectureProcessArg> d_arg_props; 163 /** variables for each argument type of f 164 * 165 * These are used to express templates for argument 166 * invariance, in the data member 167 * SynthConjectureProcessArg::d_template. 168 */ 169 std::vector<Node> d_arg_vars; 170 /** map from d_arg_vars to the argument # 171 * they represent. 172 */ 173 std::unordered_map<Node, unsigned, NodeHashFunction> d_arg_var_num; 174 /** check match 175 * This function returns true iff we can infer: 176 * cn * { x -> n_arg_map[d_arg_var_num[x]] | x in d_arg_vars } = n 177 * In other words, cn and n are equivalent 178 * via the substitution mapping argument variables to terms 179 * specified by n_arg_map. The rewriter is used for inferring 180 * this equivalence. 181 * 182 * For example, if n_arg_map contains { 1 -> t, 2 -> s }, then 183 * checkMatch( x1+x2, t+s, n_arg_map ) returns true, 184 * checkMatch( x1+1, t+1, n_arg_map ) returns true, 185 * checkMatch( 0, 0, n_arg_map ) returns true, 186 * checkMatch( x1+1, s, n_arg_map ) returns false. 187 */ 188 bool checkMatch(Node cn, 189 Node n, 190 std::unordered_map<unsigned, Node>& n_arg_map); 191 /** infer definition 192 * 193 * In the following, we say a term is a "template 194 * definition" if its free variables are a subset of d_arg_vars. 195 * 196 * If this function returns a non-null node ret, then 197 * checkMatch( ret, n, term_to_arg_carry^-1 ) returns true. 198 * and ret is a template definition. 199 * 200 * The free variables for all subterms of n are stored in 201 * free_vars. The map term_to_arg_carry is injective. 202 * 203 * For example, if term_to_arg_carry contains { t -> 1, s -> 2 } and 204 * free_vars is { t -> {y}, r -> {y}, s -> {}, q -> {}, ... -> {} }, then 205 * inferDefinition( 0, term_to_arg_carry, free_vars ) 206 * returns 0 207 * inferDefinition( t, term_to_arg_carry, free_vars ) 208 * returns x1 209 * inferDefinition( t+s+q, term_to_arg_carry, free_vars ) 210 * returns x1+x2+q 211 * inferDefinition( t+r, term_to_arg_carry, free_vars ) 212 * returns null 213 * 214 * Notice that multiple definitions are possible, e.g. above: 215 * inferDefinition( s, term_to_arg_carry, free_vars ) 216 * may return either s or x2 217 * TODO (#1210) : try multiple definitions? 218 */ 219 Node inferDefinition( 220 Node n, 221 std::unordered_map<Node, unsigned, NodeHashFunction>& term_to_arg_carry, 222 std::unordered_map<Node, 223 std::unordered_set<Node, NodeHashFunction>, 224 NodeHashFunction>& free_vars); 225 /** Assign relevant definition 226 * 227 * If def is non-null, 228 * this function assigns def as a template definition 229 * for the argument positions in args. 230 * This is called when there exists a term of the form 231 * f( t1....tn ) 232 * in the synthesis conjecture that we are processing, 233 * where t_i = def * sigma for all i \in args, 234 * for some substitution sigma, where def is a template 235 * definition. 236 * 237 * If def is null, then there exists a term of the form 238 * f( t1....tn ) 239 * where t_i = s for for all i \in args, and s is not 240 * a template definition. In this case, at least one 241 * argument in args must be marked as a relevant 242 * argument position. 243 * 244 * Returns a value rid such that: 245 * (1) rid occurs in args, 246 * (2) if def is null, then argument rid was marked 247 * relevant by this call. 248 */ 249 unsigned assignRelevantDef(Node def, std::vector<unsigned>& args); 250 /** returns true if n is in d_arg_vars, updates arg_index 251 * to its position in d_arg_vars. 252 */ 253 bool isArgVar(Node n, unsigned& arg_index); 254 }; 255 256 /** Ceg Conjecture Process 257 * 258 * This class implements static techniques for preprocessing and analysis of 259 * sygus conjectures. 260 * 261 * It is used as a back-end to SynthConjecture, which calls it using the 262 * following interface: (1) When a sygus conjecture is asserted, we call 263 * SynthConjectureProcess::simplify( q ), 264 * where q is the sygus conjecture in original form. 265 * 266 * (2) After a sygus conjecture is simplified and converted to deep 267 * embedding form, we call SynthConjectureProcess::initialize( n, candidates ). 268 * 269 * (3) During enumerative SyGuS search, calls may be made by 270 * the extension of the quantifier-free datatypes decision procedure for 271 * sygus to SynthConjectureProcess::getSymmetryBreakingPredicate(...), which are 272 * used for pruning search space based on conjecture-specific analysis. 273 */ 274 class SynthConjectureProcess 275 { 276 public: 277 SynthConjectureProcess(QuantifiersEngine* qe); 278 ~SynthConjectureProcess(); 279 /** simplify the synthesis conjecture q 280 * Returns a formula that is equivalent to q. 281 * This simplification pass is called before all others 282 * in SynthConjecture::assign. 283 * 284 * This function is intended for simplifications that 285 * impact whether or not the synthesis conjecture is 286 * single-invocation. 287 */ 288 Node preSimplify(Node q); 289 /** simplify the synthesis conjecture q 290 * Returns a formula that is equivalent to q. 291 * This simplification pass is called after all others 292 * in SynthConjecture::assign. 293 */ 294 Node postSimplify(Node q); 295 /** initialize 296 * 297 * n is the "base instantiation" of the deep-embedding version of 298 * the synthesis conjecture under "candidates". 299 * (see SynthConjecture::d_base_inst) 300 */ 301 void initialize(Node n, std::vector<Node>& candidates); 302 /** is the i^th argument of the function-to-synthesize f relevant? */ 303 bool isArgRelevant(Node f, unsigned i); 304 /** get irrelevant arguments for function-to-synthesize f 305 * returns true if f is a function-to-synthesize. 306 */ 307 bool getIrrelevantArgs(Node f, std::unordered_set<unsigned>& args); 308 /** get symmetry breaking predicate 309 * 310 * Returns a formula that restricts the enumerative search space (for a given 311 * depth) for a term x of sygus type tn whose top symbol is the tindex^{th} 312 * constructor, where x is a subterm of enumerator e. 313 */ 314 Node getSymmetryBreakingPredicate( 315 Node x, Node e, TypeNode tn, unsigned tindex, unsigned depth); 316 /** print out debug information about this conjecture */ 317 void debugPrint(const char* c); 318 private: 319 /** process conjunct 320 * 321 * This sets up initial information about functions to synthesize 322 * where n is a conjunct of the synthesis conjecture, and synth_fv 323 * is the set of (inner) universal variables in the synthesis 324 * conjecture. 325 */ 326 void processConjunct(Node n, 327 Node f, 328 std::unordered_set<Node, NodeHashFunction>& synth_fv); 329 /** flatten 330 * 331 * Flattens all applications of f in term n. 332 * This may add new variables to synth_fv, which 333 * are introduced at all positions of functions 334 * to synthesize in a bottom-up fashion. For each 335 * variable k introduced for a function application 336 * f(t), we add ( k -> f(t) ) to defs and ( f -> k ) 337 * to fun_to_defs. 338 */ 339 Node flatten(Node n, 340 Node f, 341 std::unordered_set<Node, NodeHashFunction>& synth_fv, 342 std::unordered_map<Node, Node, NodeHashFunction>& defs); 343 /** get free variables 344 * Constructs a map of all free variables that occur in n 345 * from synth_fv and stores them in the map free_vars. 346 */ 347 void getFreeVariables( 348 Node n, 349 std::unordered_set<Node, NodeHashFunction>& synth_fv, 350 std::unordered_map<Node, 351 std::unordered_set<Node, NodeHashFunction>, 352 NodeHashFunction>& free_vars); 353 /** for each synth-fun, information that is specific to this conjecture */ 354 std::map<Node, SynthConjectureProcessFun> d_sf_info; 355 356 /** get component vector */ 357 void getComponentVector(Kind k, Node n, std::vector<Node>& args); 358 }; 359 360 } /* namespace CVC4::theory::quantifiers */ 361 } /* namespace CVC4::theory */ 362 } /* namespace CVC4 */ 363 364 #endif 365