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

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_explain.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Fabian Wolff
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 explanations
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H
19
20
#include <vector>
21
22
#include "expr/node.h"
23
24
namespace CVC4 {
25
namespace theory {
26
namespace quantifiers {
27
28
class SygusInvarianceTest;
29
class TermDbSygus;
30
31
/** Recursive term builder
32
 *
33
 * This is a utility used to generate variants
34
 * of a term n, where subterms of n can be replaced
35
 * by others via calls to replaceChild(...).
36
 *
37
 * This class maintains a "context", which indicates
38
 * a position in term n. Below, we call the subterm of
39
 * the initial term n at this position the "active term".
40
 *
41
 */
42
21406
class TermRecBuild
43
{
44
 public:
45
21406
  TermRecBuild() {}
46
  /** set the initial term to n
47
   *
48
   * The context initially empty, that is,
49
   * the active term is initially n.
50
   */
51
  void init(Node n);
52
53
  /** push the context
54
   *
55
   * This updates the context so that the
56
   * active term is updated to curr[p], where
57
   * curr is the previously active term.
58
   */
59
  void push(unsigned p);
60
61
  /** pop the context */
62
  void pop();
63
  /** indicates that the i^th child of the active
64
   * term should be replaced by r in calls to build().
65
   */
66
  void replaceChild(unsigned i, Node r);
67
  /** get the i^th child of the active term */
68
  Node getChild(unsigned i);
69
  /** build the (modified) version of the term
70
   * we initialized via the call to init().
71
   */
72
  Node build(unsigned p = 0);
73
74
 private:
75
  /** stack of active terms */
76
  std::vector<Node> d_term;
77
  /** stack of children of active terms
78
   * Notice that these may be modified with calls to replaceChild(...).
79
   */
80
  std::vector<std::vector<Node> > d_children;
81
  /** stack the kind of active terms */
82
  std::vector<Kind> d_kind;
83
  /** stack of whether the active terms had an operator */
84
  std::vector<bool> d_has_op;
85
  /** stack of positions that were pushed via calls to push(...) */
86
  std::vector<unsigned> d_pos;
87
  /** add term to the context stack */
88
  void addTerm(Node n);
89
};
90
91
/*The SygusExplain utility
92
 *
93
 * This class is used to produce explanations for refinement lemmas
94
 * in the counterexample-guided inductive synthesis (CEGIS) loop.
95
 *
96
 * When given an invariance test T traverses the AST of a given term,
97
 * uses TermRecBuild to replace various subterms by fresh variables and
98
 * recheck whether the invariant, as specified by T still holds.
99
 * If it does, then we may exclude the explanation for that subterm.
100
 *
101
 * For example, say we have that the current value of
102
 * (datatype) sygus term n is:
103
 *  (if (gt x 0) 0 0)
104
 * where if, gt, x, 0 are datatype constructors.
105
 * The explanation returned by getExplanationForEquality
106
 * below for n and the above term is:
107
 *   { ((_ is if) n), ((_ is geq) n.0),
108
 *     ((_ is x) n.0.0), ((_ is 0) n.0.1),
109
 *     ((_ is 0) n.1), ((_ is 0) n.2) }
110
 *
111
 * This class can also return more precise
112
 * explanations based on a property that holds for
113
 * variants of n. For instance,
114
 * say we find that n's builtin analog rewrites to 0:
115
 *  ite( x>0, 0, 0 ) ----> 0
116
 * and we would like to find the minimal explanation for
117
 * why the builtin analog of n rewrites to 0.
118
 * We use the invariance test EquivSygusInvarianceTest
119
 * (see sygus_invariance.h) for doing this.
120
 * Using the SygusExplain::getExplanationFor method below,
121
 * this will invoke the invariant test to check, e.g.
122
 *   ite( x>0, 0, y1 ) ----> 0 ? fail
123
 *   ite( x>0, y2, 0 ) ----> 0 ? fail
124
 *   ite( y3, 0, 0 ) ----> 0 ? success
125
 * where y1, y2, y3 are fresh variables.
126
 * Hence the explanation for the condition x>0 is irrelevant.
127
 * This gives us the explanation:
128
 *   { ((_ is if) n), ((_ is 0) n.1), ((_ is 0) n.2) }
129
 * indicating that all terms of the form:
130
 *   (if _ 0 0) have a builtin equivalent that rewrites to 0.
131
 *
132
 * For details, see Reynolds et al SYNT 2017.
133
 *
134
 * Below, we let [[exp]]_n denote the term induced by
135
 * the explanation exp for n.
136
 * For example:
137
 *   exp = { ((_ is plus) n), ((_ is y) n.1) }
138
 * is such that:
139
 *   [[exp]]_n = (plus w y)
140
 * where w is a fresh variable.
141
 */
142
class SygusExplain
143
{
144
 public:
145
2275
  SygusExplain(TermDbSygus* tdb) : d_tdb(tdb) {}
146
2273
  ~SygusExplain() {}
147
  /** get explanation for equality
148
   *
149
   * This function constructs an explanation, stored in exp, such that:
150
   * - All formulas in exp are of the form ((_ is C) ns), where ns
151
   *   is a chain of selectors applied to n, and
152
   * - exp => ( n = vn )
153
   */
154
  void getExplanationForEquality(Node n, Node vn, std::vector<Node>& exp);
155
  /** returns the conjunction of exp computed in the above function */
156
  Node getExplanationForEquality(Node n, Node vn);
157
158
  /** get explanation for equality
159
   *
160
   * This is identical to the above function except that we
161
   * take an additional argument cexc, which says which
162
   * children of vn should be excluded from the explanation.
163
   *
164
   * For example, if vn = plus( plus( x, x ), y ) and cexc is { 0 -> true },
165
   * then the following is appended to exp :
166
   *   { ((_ is plus) n), ((_ is y) n.1) }
167
   * where notice that the 0^th argument of vn is excluded.
168
   */
169
  void getExplanationForEquality(Node n,
170
                                 Node vn,
171
                                 std::vector<Node>& exp,
172
                                 std::map<unsigned, bool>& cexc);
173
  /** returns the conjunction of exp computed in the above function */
174
  Node getExplanationForEquality(Node n,
175
                                 Node vn,
176
                                 std::map<unsigned, bool>& cexc);
177
178
  /** get explanation for
179
   *
180
   * This function constructs an explanation, stored in exp, such that:
181
   * - All formulas in exp are of the form ((_ is C) ns), where ns
182
   *   is a chain of selectors applied to n, and
183
   * - The test et holds for [[exp]]_n, and
184
   * - (if applicable) exp => ( n != vnr ).
185
   *
186
   * This function updates sz to be the term size of [[exp]]_n.
187
   *
188
   * If strict is false, then we also test whether the invariance test holds
189
   * independently of the entire value of vn.
190
   *
191
   * The argument var_count is used for tracking the variables that we introduce
192
   * to generalize the shape of vn. This map is passed to
193
   * TermDbSygus::getFreeVarInc. This argument should be used if we are
194
   * calling this function multiple times and the generalization should not
195
   * introduce variables that shadow the variables introduced on previous calls.
196
   */
197
  void getExplanationFor(Node n,
198
                         Node vn,
199
                         std::vector<Node>& exp,
200
                         SygusInvarianceTest& et,
201
                         Node vnr,
202
                         unsigned& sz);
203
  void getExplanationFor(Node n,
204
                         Node vn,
205
                         std::vector<Node>& exp,
206
                         SygusInvarianceTest& et,
207
                         Node vnr,
208
                         std::map<TypeNode, int>& var_count,
209
                         unsigned& sz);
210
  void getExplanationFor(Node n,
211
                         Node vn,
212
                         std::vector<Node>& exp,
213
                         SygusInvarianceTest& et,
214
                         bool strict = true);
215
  void getExplanationFor(Node n,
216
                         Node vn,
217
                         std::vector<Node>& exp,
218
                         SygusInvarianceTest& et,
219
                         std::map<TypeNode, int>& var_count,
220
                         bool strict = true);
221
222
 private:
223
  /** sygus term database associated with this utility */
224
  TermDbSygus* d_tdb;
225
  /** Helper function for getExplanationFor
226
   * var_count is the number of free variables we have introduced,
227
   *   per type, for the purposes of generalizing subterms of n.
228
   * vnr_exp stores the explanation, if one exists, for
229
   *   n != vnr.  It is only non-null if vnr is non-null.
230
   */
231
  void getExplanationFor(TermRecBuild& trb,
232
                         Node n,
233
                         Node vn,
234
                         std::vector<Node>& exp,
235
                         std::map<TypeNode, int>& var_count,
236
                         SygusInvarianceTest& et,
237
                         Node vnr,
238
                         Node& vnr_exp,
239
                         int& sz);
240
};
241
242
} /* CVC4::theory::quantifiers namespace */
243
} /* CVC4::theory namespace */
244
} /* CVC4 namespace */
245
246
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_EXPLAIN_H */