GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/quantifiers/sygus/sygus_process_conj.h Lines: 4 4 100.0 % Date: 2021-03-22 Branches: 0 0 0.0 %

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

 Generated by: GCOVR (Version 3.2)