GCC Code Coverage Report
 Directory: . Exec Total Coverage File: src/theory/quantifiers/sygus/sygus_unif_rl.h Lines: 7 7 100.0 % Date: 2021-03-22 Branches: 14 46 30.4 %

 Line Exec Source 1 /********************* */ 2 /*! \file sygus_unif_rl.h 3  ** \verbatim 4  ** Top contributors (to current version): 5  ** Haniel Barbosa, 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 sygus_unif_rl 13  **/ 14 15 #include "cvc4_private.h" 16 17 #ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H 18 #define CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H 19 20 #include  21 #include "options/main_options.h" 22 #include "theory/quantifiers/sygus/sygus_unif.h" 23 24 #include "theory/quantifiers/lazy_trie.h" 25 26 namespace CVC4 { 27 namespace theory { 28 namespace quantifiers { 29 30 using BoolNodePair = std::pair; 31 using BoolNodePairHashFunction = 32  PairHashFunction; 33 using BoolNodePairMap = 34  std::unordered_map; 35 using NodePairMap = std::unordered_map; 36 using NodePair = std::pair; 37 38 class SynthConjecture; 39 40 /** Sygus unification Refinement Lemmas utility 41  * 42  * This class implement synthesis-by-unification, where the specification is a 43  * set of refinement lemmas. With respect to SygusUnif, it's main interface 44  * function is addExample, which adds a refinement lemma to the specification. 45  */ 46 class SygusUnifRl : public SygusUnif 47 { 48  public: 49  SygusUnifRl(SynthConjecture* p); 50  ~SygusUnifRl(); 51 52  /** initialize */ 53  void initializeCandidate( 54  QuantifiersEngine* qe, 55  Node f, 56  std::vector& enums, 57  std::map>& strategy_lemmas) override; 58 59  /** Notify enumeration (unused) */ 60  void notifyEnumeration(Node e, Node v, std::vector& lemmas) override; 61  /** Construct solution */ 62  bool constructSolution(std::vector& sols, 63  std::vector& lemmas) override; 64  /** add refinement lemma 65  * 66  * This adds a lemma to the specification. It returns the purified form 67  * of the lemma based on the method purifyLemma below. The method adds the 68  * head of "evaluation points" to the map eval_hds, where an evaluation point 69  * is a term of the form: 70  * ev( e1, c1...cn ) 71  * where ev is an evaluation function for the sygus deep embedding, e1 is of 72  * sygus datatype type (the "head" of the evaluation point), and c1...cn are 73  * constants. If ev( e1, c1...cn ) is the purified form of ev( e, t1...tn ), 74  * then e1 is added to eval_hds[e]. We add evaluation points to eval_hds only 75  * for those terms that are newly generated by this call (and have not been 76  * returned by a previous call to this method). 77  */ 78  Node addRefLemma(Node lemma, std::map>& eval_hds); 79  /** 80  * whether f is being synthesized with unification strategies. This can be 81  * checked through wehether f has conditional or point enumerators (we use the 82  * former) 83  */ 84  bool usingUnif(Node f) const; 85  /** get condition for evaluation point 86  * 87  * Returns the strategy point corresponding to the condition of the strategy 88  * point e. 89  */ 90  Node getConditionForEvaluationPoint(Node e) const; 91  /** set conditional enumerators 92  * 93  * This informs this class that the current set of conditions for evaluation 94  * point e are enumerated by "enums" and have values "conds"; "guard" is 95  * Boolean variable whose semantics correspond to "there is a solution using 96  * at most enums.size() conditions." 97  */ 98  void setConditions(Node e, 99  Node guard, 100  const std::vector& enums, 101  const std::vector& conds); 102 103  /** retrieve the head of evaluation points for candidate c, if any */ 104  std::vector getEvalPointHeads(Node c); 105 106  /** 107  * Whether we are using condition pool enumeration (Section 4 of Barbosa et al 108  * FMCAD 2019). This is determined by option::sygusUnifPi(). 109  */ 110  bool usingConditionPool() const; 111  /** Whether we are additionally using information gain. */ 112  bool usingConditionPoolInfoGain() const; 113 114  protected: 115  /** reference to the parent conjecture */ 116  SynthConjecture* d_parent; 117  /** Whether we are using condition pool enumeration */ 118  bool d_useCondPool; 119  /** Whether we are additionally using information gain heuristics */ 120  bool d_useCondPoolIGain; 121  /* Functions-to-synthesize (a.k.a. candidates) with unification strategies */ 122  std::unordered_set d_unif_candidates; 123  /** construct sol */ 124  Node constructSol(Node f, 125  Node e, 126  NodeRole nrole, 127  int ind, 128  std::vector& lemmas) override; 129  /** collects data from refinement lemmas to drive solution construction 130  * 131  * In particular it rebuilds d_app_to_pt whenever d_prev_rlemmas is different 132  * from d_rlemmas, in which case we may have added or removed data points 133  */ 134  void initializeConstructSol() override; 135  /** initialize construction solution for function-to-synthesize f */ 136  void initializeConstructSolFor(Node f) override; 137  /** maps unif functions-to~synhesize to their last built solutions */ 138  std::map d_cand_to_sol; 139  /* 140  -------------------------------------------------------------- 141  Purification 142  -------------------------------------------------------------- 143  */ 144  /** 145  * maps heads of applications of a unif function-to-synthesize to their tuple 146  * of arguments (which constitute a "data point" aka an "evaluation point") 147  */ 148  std::map> d_hd_to_pt; 149  /** maps unif candidates to heads of their evaluation points */ 150  std::map> d_cand_to_eval_hds; 151  /** 152  * maps applications of unif functions-to-synthesize to the result of their 153  * purification */ 154  std::map d_app_to_purified; 155  /** maps unif functions-to-synthesize to counters of heads of evaluation 156  * points */ 157  std::map d_cand_to_hd_count; 158  /** 159  * This is called on the refinement lemma and will rewrite applications of 160  * functions-to-synthesize to their respective purified form, i.e. such that 161  * all unification functions are applied over concrete values. Moreover 162  * unification functions are also rewritten such that every different tuple of 163  * arguments has a fresh function symbol applied to it. 164  * 165  * Non-unification functions are also equated to their model values when they 166  * occur as arguments of unification functions. 167  * 168  * A vector of guards with the (negated) equalities between the original 169  * arguments and their model values is populated accordingly. 170  * 171  * When the traversal encounters an application of a unification 172  * function-to-synthesize it will proceed to ensure that the arguments of that 173  * function application are constants (ensureConst becomes "true"). If an 174  * applicatin of a non-unif function-to-synthesize is reached, the requirement 175  * is lifted (ensureConst becomes "false"). This avoides introducing spurious 176  * equalities in model_guards. 177  * 178  * For example if "f" is being synthesized with a unification strategy and "g" 179  * is not then the application 180  * f(g(f(g(0))))=1 181  * would be purified into 182  * g(0) = c1 ^ g(f1(c1)) = c3 => f2(c3) 183  * 184  * Similarly 185  * f(+(0,f(g(0)))) 186  * would be purified into 187  * g(0) = c1 ^ f1(c1) = c2 => f2(+(0,c2)) 188  * 189  * This function also populates the maps between candidates, heads and 190  * evaluation points 191  */ 192  Node purifyLemma(Node n, 193  bool ensureConst, 194  std::vector& model_guards, 195  BoolNodePairMap& cache); 196  /* 197  -------------------------------------------------------------- 198  Strategy information 199  -------------------------------------------------------------- 200  */ 201  /** 202  * This class stores the necessary information for building a decision tree 203  * for a particular node in the strategy tree of a candidate variable f. 204  */ 205  class DecisionTreeInfo 206  { 207  public: 208 17  DecisionTreeInfo() 209 17  : d_unif(nullptr), d_strategy(nullptr), d_strategy_index(0) 210  { 211 17  } 212 17  ~DecisionTreeInfo() {} 213  /** initializes this class */ 214  void initialize(Node cond_enum, 215  SygusUnifRl* unif, 216  SygusUnifStrategy* strategy, 217  unsigned strategy_index); 218  /** returns index of strategy information of strategy node for this DT */ 219  unsigned getStrategyIndex() const; 220  /** builds solution, if possible, using the given constructor 221  * 222  * A solution is possible when all different valued heads can be separated, 223  * i.e. the current set of conditions separates them in a decision tree 224  */ 225  Node buildSol(Node cons, std::vector& lemmas); 226  /** bulids a solution by considering all condition values ever enumerated */ 227  Node buildSolAllCond(Node cons, std::vector& lemmas); 228  /** builds a solution by incrementally adding points and conditions to DT 229  * 230  * Differently from the above method, here a condition is only added to the 231  * DT when it's necessary for resolving a separation conflict (i.e. heads 232  * with different values in the same leaf of the DT). Only one value per 233  * condition enumerated is considered. 234  * 235  * If a solution cannot be built, then there are more conflicts to be 236  * resolved than condition enumerators. A conflict lemma is added to lemmas 237  * that forces a new assigment in which the conflict is removed (heads are 238  * made equal) or a new condition is enumerated to try to separate them. 239  */ 240  Node buildSolMinCond(Node cons, std::vector& lemmas); 241  /** reference to parent unif util */ 242  SygusUnifRl* d_unif; 243  /** enumerator template (if no templates, nodes in pair are Node::null()) */ 244  NodePair d_template; 245  /** enumerated condition values, this is set by setConditions(...). */ 246  std::vector d_conds; 247  /** gathered evaluation point heads */ 248  std::vector d_hds; 249  /** all enumerated model values for conditions */ 250  std::unordered_set d_cond_mvs; 251  /** get condition enumerator */ 252 17  Node getConditionEnumerator() const { return d_cond_enum; } 253  /** set conditions */ 254  void setConditions(Node guard, 255  const std::vector& enums, 256  const std::vector& conds); 257 258  private: 259  /** true and false nodes */ 260  Node d_true; 261  Node d_false; 262  /** Accumulates solutions built when considering all enumerated condition 263  * values (which may generate repeated solutions) */ 264  std::unordered_set d_sols; 265  /** 266  * Conditional enumerator variables corresponding to the condition values in 267  * d_conds. These are used for generating separation lemmas during 268  * buildSol. This is set by setConditions(...). 269  */ 270  std::vector d_enums; 271  /** 272  * The guard literal whose semantics is "we need at most d_enums.size() 273  * conditions in our solution. This is set by setConditions(...). 274  */ 275  Node d_guard; 276  /** 277  * reference to inferred strategy for the function-to-synthesize this DT is 278  * associated with 279  */ 280  SygusUnifStrategy* d_strategy; 281  /** index of strategy information of strategy node this DT is based on 282  * 283  * this is the index of the strategy (d_strats[index]) in the strategy node 284  * to which this decision tree corresponds, which can be accessed through 285  * the above strategy reference 286  */ 287  unsigned d_strategy_index; 288  /** 289  * The enumerator in the strategy tree that stores conditions of the 290  * decision tree. 291  */ 292  Node d_cond_enum; 293  /** extracts solution from decision tree built 294  * 295  * Depending on the active options, the decision tree might be rebuilt 296  * before a solution is extracted, for example to optimize size (smaller 297  * DTs) or chance of having a general solution (information gain heuristics) 298  */ 299  Node extractSol(Node cons, std::map& hd_mv); 300 301  /** rebuild decision tree using information gain heuristic 302  * 303  * In a scenario in which the decision tree potentially contains more 304  * conditions than necessary, it is beneficial to rebuild it in a way that 305  * "better" conditions occurr closer to the top. 306  * 307  * The information gain heuristic selects conditions that lead to a 308  * greater reduction of the Shannon entropy in the set of points 309  */ 310  void recomputeSolHeuristically(std::map& hd_mv); 311  /** recursively select (best) conditions to split heads 312  * 313  * At each call picks the best condition based on the information gain 314  * heuristic and splits the set of heads accordingly, then recurses on 315  * them. 316  * 317  * The base case is a set being fully classified (i.e. all heads have the 318  * same value) 319  * 320  * hds is the set of evaluation point heads we must classify with the 321  * values in conds. The classification is guided by how a condition value 322  * splits the heads through its evaluation on the points associated with 323  * the heads. The metric is based on the model values of the heads (hd_mv) 324  * in the resulting splits. 325  * 326  * ind is the current level of indentation (for debugging) 327  */ 328  void buildDtInfoGain(std::vector& hds, 329  std::vector conds, 330  std::map& hd_mv, 331  int ind); 332  /** computes the Shannon entropy of a set of heads 333  * 334  * The entropy depends on how many positive and negative heads are in the 335  * set and in their distribution. The polarity of the evaluation heads is 336  * queried from their model values in hd_mv. 337  * 338  * ind is the current level of indentation (for debugging) 339  */ 340  double getEntropy(const std::vector& hds, 341  std::map& hd_mv, 342  int ind); 343  /** evaluates a condition on a set of points 344  * 345  * The result is two sets of points: those on which the condition holds 346  * and those on which it does not 347  */ 348  std::pair, std::vector> evaluateCond( 349  std::vector& pts, Node cond); 350  /** Classifies evaluation points according to enumerated condition values 351  * 352  * Maintains the invariant that points evaluated in the same way in the 353  * current condition values are kept in the same "separation class." 354  */ 355 2376652  class PointSeparator : public LazyTrieEvaluator 356  { 357  public: 358 17  PointSeparator() : d_dt(nullptr) {} 359  /** initializes this class */ 360  void initialize(DecisionTreeInfo* dt); 361  /** 362  * evaluates the respective evaluation point of the head n on the index-th 363  * condition 364  */ 365  Node evaluate(Node n, unsigned index) override; 366 367  /** the lazy trie for building the separation classes */ 368  LazyTrieMulti d_trie; 369  /** extracts solution from decision tree built */ 370  Node extractSol(Node cons, std::map& hd_mv); 371  /** computes the result of applying cond on the respective point of hd 372  * 373  * If for example cond is (\lambda xy. x < y) and hd is an evaluation head 374  * in point (hd 0 1) this function will result in true, since 375  * (\lambda xy. x < y) 0 1 evaluates to true 376  */ 377  Node computeCond(Node cond, Node hd); 378 379  private: 380  /** reference to parent unif util */ 381  DecisionTreeInfo* d_dt; 382  /** cache of conditions evaluations on heads 383  * 384  * If for example cond is (\lambda xy. x < y) and hd is an evaluation head 385  * in point (hd 0 1), then after invoking computeCond(cond, hd) this map 386  * will contain d_eval_cond_hd[] = true, since 387  * 388  * (\lambda xy. x < y) 0 1 evaluates to true 389  */ 390  std::map, Node> d_eval_cond_hd; 391  }; 392  /** 393  * Utility for determining how evaluation points are separated by currently 394  * enumerated condiotion values 395  */ 396  PointSeparator d_pt_sep; 397  }; 398  /** maps strategy points in the strategy tree to the above data */ 399  std::map d_stratpt_to_dt; 400  /** maps conditional enumerators to strategy points in which they occur */ 401  std::map> d_cenum_to_stratpt; 402  /** maps unif candidates to their conditional enumerators */ 403  std::map> d_cand_cenums; 404  /** all conditional enumerators */ 405  std::vector d_cond_enums; 406  /** register strategy 407  * 408  * Initialize the above data for the relevant enumerators in the strategy tree 409  * of candidate variable f. For each strategy point e which there is a 410  * decision tree strategy, we add e to enums. For each strategy with index 411  * i in an strategy point e, if we are not using the strategy, we add i to 412  * unused_strats[e]. This map is later passed to 413  * SygusUnifStrategy::staticLearnRedundantOps. 414  */ 415  void registerStrategy( 416  Node f, 417  std::vector& enums, 418  std::map>& unused_strats); 419  /** register strategy node 420  * 421  * Called while traversing the strategy tree of f. The arguments e and nrole 422  * indicate the current node in the tree we are traversing, and visited 423  * indicates the nodes we have already visited. The arguments enums and 424  * unused_strats are modified as described above. 425  */ 426  void registerStrategyNode( 427  Node f, 428  Node e, 429  NodeRole nrole, 430  std::map>& visited, 431  std::vector& enums, 432  std::map>& unused_strats); 433  /** register conditional enumerator 434  * 435  * Registers that cond is a conditional enumerator for building a (recursive) 436  * decision tree at strategy node e within the strategy tree of f. 437  */ 438  void registerConditionalEnumerator(Node f, 439  Node e, 440  Node cond, 441  unsigned strategy_index); 442 }; 443 444 } // namespace quantifiers 445 } // namespace theory 446 } // namespace CVC4 447 448 #endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_UNIF_RL_H */

 Generated by: GCOVR (Version 3.2)