GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/quantifiers/sygus/sygus_grammar_norm.h Lines: 8 20 40.0 % Date: 2021-03-23 Branches: 1 38 2.6 %

 Line Exec Source 1 /********************* */ 2 /*! \file sygus_grammar_norm.h 3  ** \verbatim 4  ** Top contributors (to current version): 5  ** Haniel Barbosa, Andrew Reynolds, Tim King 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 class for simplifying SyGuS grammars after they are encoded into 13  ** datatypes. 14  **/ 15 #include "cvc4_private.h" 16 17 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H 18 #define CVC4__THEORY__QUANTIFIERS__SYGUS_GRAMMAR_NORM_H 19 20 #include  21 #include  22 #include  23 24 #include "expr/node.h" 25 #include "expr/sygus_datatype.h" 26 #include "expr/type_node.h" 27 28 namespace CVC4 { 29 namespace theory { 30 namespace quantifiers { 31 32 class SygusGrammarNorm; 33 class TermDbSygus; 34 35 /** Operator position trie class 36  * 37  * This data structure stores an unresolved type corresponding to the 38  * normalization of a type. This unresolved type is indexed by the positions of 39  * the construtors of the datatype associated with the original type. The list 40  * of positions represent the operators, associated with the respective 41  * considered constructors, that were used for building the unresolved type. 42  * 43  * Example: 44  * 45  * Let A be a type defined by the grammar "A -> x | 0 | 1 | A + A". In its 46  * datatype representation the operator for "x" is in position 0, for "0" in 47  * position "1" and so on. Consider entries (T, [op_1, ..., op_n]) -> T' to 48  * represent that a type T is normalized with operators [op_1, ..., op_n] into 49  * the type T'. For entries 50  * 51  * (A, [x, 0, 1, +]) -> A1 52  * (A, [x, 1, +]) -> A2 53  * (A, [1, +]) -> A3 54  * (A, [0]) -> AZ 55  * (A, [x]) -> AX 56  * (A, [1]) -> AO 57  * 58  * the OpPosTrie T we build for this type is : 59  * 60  * T[A] : 61  * T[A].d_children[0] : AX 62  * T[A].d_children[0].d_children[1] : 63  * T[A].d_children[0].d_children[1].d_children[2] : 64  * T[A].d_children[0].d_children[1].d_children[2].d_children[3] : A1 65  * T[A].d_children[0].d_children[2] : 66  * T[A].d_children[0].d_children[2].d_children[3] : A2 67  * T[A].d_children[1] : AZ 68  * T[A].d_children[2] : AO 69  * T[A].d_children[2].d_children[4] : A3 70  * 71  * Nodes store the types built for the path of positions up to that point, if 72  * any. 73  */ 74 8316 class OpPosTrie 75 { 76  public: 77  /** type retrieval/addition 78  * 79  * if type indexed by the given operator positions is already in the trie then 80  * unres_t becomes the indexed type and true is returned. Otherwise a new type 81  * is created, indexed by the given positions, and assigned to unres_t, with 82  * false being returned. 83  */ 84  bool getOrMakeType(TypeNode tn, 85  TypeNode& unres_tn, 86  const std::vector& op_pos, 87  unsigned ind = 0); 88  /** clear all data from this trie */ 89  void clear() { d_children.clear(); } 90 91  private: 92  /** the data (only set for the final node of an inserted path) */ 93  TypeNode d_unres_tn; 94  /* the children of the trie node */ 95  std::map d_children; 96 }; /* class OpPosTrie */ 97 98 /** Utility for normalizing SyGuS grammars to avoid spurious enumerations 99  * 100  * Uses the datatype representation of a SyGuS grammar to identify entries that 101  * can normalized in order to have less possible enumerations. An example is 102  * with integer types, e.g.: 103  * 104  * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int) 105  * 106  * becomes 107  * 108  * Int0 -> IntZ | Int1 109  * IntZ -> 0 110  * Int1 -> IntX | IntX + Int1 | Int2 111  * IntX -> x 112  * Int2 -> IntY | IntY + Int2 | Int3 113  * IntY -> y 114  * Int3 -> IntO | IntO + Int3 | Int4 115  * IntO -> 1 116  * Int4 -> IntITE | IntITE + Int4 117  * IntITE -> ite(Bool, Int0, Int0) 118  * 119  * TODO: #1304 normalize more complex grammars 120  * 121  * This class also performs more straightforward normalizations, such as 122  * expanding definitions of functions declared with a "define-fun" command. 123  * These lighweight transformations are always applied, independently of the 124  * normalization option being enabled. 125  */ 126 class SygusGrammarNorm 127 { 128  public: 129  SygusGrammarNorm(TermDbSygus* tds); 130 329  ~SygusGrammarNorm() {} 131  /** creates a normalized typenode from a given one. 132  * 133  * In a normalized typenode all typenodes it contains are normalized. 134  * Normalized typenodes can be structurally identicial to their original 135  * counterparts. 136  * 137  * sygus_vars are the input variables for the function to be synthesized, 138  * which are used as input for the built datatypes. 139  * 140  * This is the function that will resolve all types and datatypes built during 141  * normalization. This operation can only be performed after all types 142  * contained in "tn" have been normalized, since the resolution of datatypes 143  * depends on all types involved being defined. 144  */ 145  TypeNode normalizeSygusType(TypeNode tn, Node sygus_vars); 146 147  /* Retrives, or, if none, creates, stores and returns, the node for the 148  * identity operator (\lambda x. x) for the given type node */ 149  static inline Node getIdOp(TypeNode tn) 150  { 151  auto it = d_tn_to_id.find(tn); 152  if (it == d_tn_to_id.end()) 153  { 154  std::vector vars = {NodeManager::currentNM()->mkBoundVar(tn)}; 155  Node n = NodeManager::currentNM()->mkNode( 156  kind::LAMBDA, 157  NodeManager::currentNM()->mkNode(kind::BOUND_VAR_LIST, vars), 158  vars.back()); 159  d_tn_to_id[tn] = n; 160  return n; 161  } 162  return it->second; 163  } 164 165  private: 166  /** Keeps the necessary information for bulding a normalized type: 167  * 168  * the original typenode, from which the datatype representation can be 169  * extracted 170  * 171  * the operators, names, print callbacks and list of argument types for each 172  * constructor 173  * 174  * the unresolved type node used as placeholder for references of the yet to 175  * be built normalized type 176  * 177  * A (SyGuS) datatype to represent the structure of the type node for the 178  * normalized type. 179  */ 180  class TypeObject 181  { 182  public: 183  /* Stores the original type node and the unresolved placeholder. The 184  * datatype for the latter is created with the respective name. */ 185  TypeObject(TypeNode src_tn, TypeNode unres_tn); 186 729  ~TypeObject() {} 187 188  /** adds information in "cons" (operator, name, print callback, argument 189  * types) as it is into "to" 190  * 191  * A side effect of this procedure is to expand the definitions in the sygus 192  * operator of "cons" 193  * 194  * The types of the arguments of "cons" are recursively normalized 195  */ 196  void addConsInfo(SygusGrammarNorm* sygus_norm, 197  const DTypeConstructor& cons); 198 199  /** initializes a datatype with the information in the type object 200  * 201  * "dt" is the datatype of the original typenode. It is necessary for 202  * retrieving ancillary information during the datatype building, such as 203  * its sygus type (e.g. Int) 204  * 205  * The initialized datatype and its unresolved type are saved in the global 206  * accumulators of "sygus_norm" 207  */ 208  void initializeDatatype(SygusGrammarNorm* sygus_norm, const DType& dt); 209 210  //---------- information stored from original type node 211 212  /* The original typenode this TypeObject is built from */ 213  TypeNode d_tn; 214 215  //---------- information to build normalized type node 216 217  /* Unresolved type node placeholder */ 218  TypeNode d_unres_tn; 219  /** A sygus datatype */ 220  SygusDatatype d_sdt; 221  }; /* class TypeObject */ 222 223  /** Transformation abstract class 224  * 225  * Classes extending this one will define specif transformationst for building 226  * normalized types based on applications of specific operators 227  */ 228 27  class Transf 229  { 230  public: 231 27  virtual ~Transf() {} 232 233  /** abstract function for building normalized types 234  * 235  * Builds normalized types for the operators specifed by the positions in 236  * op_pos of constructors from dt. The built types are associated with the 237  * given type object and accumulated in the sygus_norm object, whose 238  * utilities for any extra necessary normalization. 239  */ 240  virtual void buildType(SygusGrammarNorm* sygus_norm, 241  TypeObject& to, 242  const DType& dt, 243  std::vector& op_pos) = 0; 244  }; /* class Transf */ 245 246  /** Drop transformation class 247  * 248  * This class builds a type by dropping a set of redundant constructors, 249  * whose indices are given as input to the constructor of this class. 250  */ 251 54  class TransfDrop : public Transf 252  { 253  public: 254 27  TransfDrop(const std::vector& indices) : d_drop_indices(indices) 255  { 256 27  } 257  /** build type */ 258  void buildType(SygusGrammarNorm* sygus_norm, 259  TypeObject& to, 260  const DType& dt, 261  std::vector& op_pos) override; 262 263  private: 264  std::vector d_drop_indices; 265  }; 266 267  /** Chain transformation class 268  * 269  * Determines how to build normalized types by chaining the application of one 270  * of its operators. The resulting type should admit the same terms as the 271  * previous one modulo commutativity, associativity and identity of the 272  * neutral element. 273  * 274  * TODO: #1304: 275  * - define this transformation for more than just PLUS for Int. 276  * - improve the building such that elements that should not be entitled a 277  * "link in the chain" (such as 5 in opposition to variables and 1) do not get 278  * one 279  * - consider the case when operator is applied to different types, e.g.: 280  * A -> B + B | x; B -> 0 | 1 281  * - consider the case in which in which the operator occurs nested in an 282  * argument type of itself, e.g.: 283  * A -> (B + B) + B | x; B -> 0 | 1 284  */ 285  class TransfChain : public Transf 286  { 287  public: 288  TransfChain(unsigned chain_op_pos, const std::vector& elem_pos) 289  : d_chain_op_pos(chain_op_pos), d_elem_pos(elem_pos){}; 290 291  /** builds types encoding a chain in which each link contains a repetition 292  * of the application of the chain operator over a non-identity element 293  * 294  * Example: when considering, over the integers, the operator "+" and the 295  * elemenst "1", "x" and "y", the built chain is e.g. 296  * 297  * x + ... + x + y + ... + y + 1 + ...+ 1 298  * 299  * whose encoding in types would be e.g. 300  * 301  * A -> AX | AX + A | B 302  * AX -> x 303  * B -> BY | BY + B | C 304  * BY -> y 305  * C -> C1 | C1 + C 306  * C1 -> 1 307  * 308  * ++++++++ 309  * 310  * The types composing links in the chain are built recursively by invoking 311  * sygus_norm, which caches results and handles the global normalization, on 312  * the operators not used in a given link, which will lead to recalling this 313  * transformation and so on until all operators originally given are 314  * considered. 315  */ 316  void buildType(SygusGrammarNorm* sygus_norm, 317  TypeObject& to, 318  const DType& dt, 319  std::vector& op_pos) override; 320 321  /** Whether operator is chainable for the type (e.g. PLUS for Int) 322  * 323  * Since the map this function depends on cannot be built statically, this 324  * function first build maps the first time a type is checked. As a 325  * consequence the list of chainabel operators is hardcoded in the map 326  * building. 327  * 328  * TODO: #1304: Cover more types and operators, make this robust to more 329  * complex grammars 330  */ 331  static bool isChainable(TypeNode tn, Node op); 332  /* Whether n is the identity for the chain operator of the type (e.g. 1 is 333  * not the identity 0 for PLUS for Int) 334  * 335  * TODO: #1304: Cover more types, make this robust to more complex grammars 336  */ 337  static bool isId(TypeNode tn, Node op, Node n); 338 339  private: 340  /* TODO #1304: this should admit more than one, as well as which elements 341  * are associated with which operator */ 342  /* Position of chain operator */ 343  unsigned d_chain_op_pos; 344  /* Positions (of constructors in the datatype whose type is being 345  * normalized) of elements the chain operator is applied to */ 346  std::vector d_elem_pos; 347  /** Specifies for each type node which are its chainable operators 348  * 349  * For example, for Int the map is {OP -> [+]} 350  * 351  * TODO #1304: consider more operators 352  */ 353  static std::map> d_chain_ops; 354  /** Specifies for each type node and chainable operator its identity 355  * 356  * For example, for Int and PLUS the map is {Int -> {+ -> 0}} 357  * 358  * TODO #1304: consider more operators 359  */ 360  static std::map> d_chain_op_id; 361 362  }; /* class TransfChain */ 363 364  /** sygus term database associated with this utility */ 365  TermDbSygus* d_tds; 366  /** List of variable inputs of function-to-synthesize. 367  * 368  * This information is needed in the construction of each datatype 369  * representation of type nodes contained in the type node being normalized 370  */ 371  TNode d_sygus_vars; 372  /* Datatypes to be resolved */ 373  std::vector d_dt_all; 374  /* Types to be resolved */ 375  std::set d_unres_t_all; 376  /* Associates type nodes with OpPosTries */ 377  std::map d_tries; 378  /* Map of type nodes into their identity operators (\lambda x. x) */ 379  static std::map d_tn_to_id; 380 381  /** recursively traverses a typenode normalizing all of its elements 382  * 383  * "tn" is the typenode to be normalized 384  * "dt" is its datatype representation 385  * "op_pos" is the list of positions of construtors of dt that are being 386  * considered for the normalization 387  * 388  * The result of normalizing tn with the respective constructors is cached 389  * with an OpPosTrie. New types and datatypes created during normalization are 390  * accumulated grobally to be later resolved. 391  * 392  * The normalization occurs following some inferred transformation based on 393  * the sygus type (e.g. Int) of tn, and the operators being considered. 394  * 395  * Example: Let A be the type node encoding the grammar 396  * 397  * Int -> x | y | Int + Int | 0 | 1 | ite(Bool, Int, Int) 398  * 399  * and assume all its datatype constructors are being used for 400  * normalization. The inferred normalization transformation will consider the 401  * non-zero elements {x, y, 1, ite(...)} and the operator {+} to build a chain 402  * of monomials, as seen above. The operator for "0" is rebuilt as is (the 403  * default behaviour of operators not selected for transformations). 404  * 405  * recursion depth is limited by the height of the types, which is small 406  */ 407  TypeNode normalizeSygusRec(TypeNode tn, 408  const DType& dt, 409  std::vector& op_pos); 410 411  /** wrapper for the above function 412  * 413  * invoked when all operators of "tn" are to be considered for normalization 414  */ 415  TypeNode normalizeSygusRec(TypeNode tn); 416 417  /** infers a transformation for normalizing dt when allowed to use the 418  * operators in the positions op_pos. 419  * 420  * TODO: #1304: Infer more complex transformations 421  */ 422  std::unique_ptr inferTransf(TypeNode tn, 423  const DType& dt, 424  const std::vector& op_pos); 425 }; /* class SygusGrammarNorm */ 426 427 } // namespace quantifiers 428 } // namespace theory 429 } // namespace CVC4 430 431 #endif

 Generated by: GCOVR (Version 3.2)