GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_invariance.h Lines: 19 20 95.0 %
Date: 2021-03-23 Branches: 14 28 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_invariance.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, 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 sygus invariance tests
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
18
#define CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H
19
20
#include <unordered_map>
21
#include <vector>
22
23
#include "expr/node.h"
24
25
namespace CVC4 {
26
namespace theory {
27
namespace quantifiers {
28
29
class TermDbSygus;
30
class SynthConjecture;
31
32
/* SygusInvarianceTest
33
*
34
* This class is the standard interface for term generalization
35
* in SyGuS. Its interface is a single function is_variant,
36
* which is a virtual condition for SyGuS terms.
37
*
38
* The common use case of invariance tests is when constructing
39
* minimal explanations for refinement lemmas in the
40
* counterexample-guided inductive synthesis (CEGIS) loop.
41
* See sygus_explain.h for more details.
42
*/
43
43367
class SygusInvarianceTest
44
{
45
 public:
46
43367
  virtual ~SygusInvarianceTest() {}
47
48
  /** Is nvn invariant with respect to this test ?
49
   *
50
   * - nvn is the term to check whether it is invariant.
51
   * - x is a variable such that the previous call to
52
   *   is_invariant (if any) was with term nvn_prev, and
53
   *   nvn is equal to nvn_prev with some subterm
54
   *   position replaced by x. This is typically used
55
   *   for debugging only.
56
   */
57
81278
  bool is_invariant(TermDbSygus* tds, Node nvn, Node x)
58
  {
59
81278
    if (invariant(tds, nvn, x))
60
    {
61
7497
      d_update_nvn = nvn;
62
7497
      return true;
63
    }
64
73781
    return false;
65
  }
66
  /** get updated term */
67
24086
  Node getUpdatedTerm() { return d_update_nvn; }
68
  /** set updated term */
69
12043
  void setUpdatedTerm(Node n) { d_update_nvn = n; }
70
 protected:
71
  /** result of the node that satisfies this invariant */
72
  Node d_update_nvn;
73
  /** check whether nvn[ x ] is invariant */
74
  virtual bool invariant(TermDbSygus* tds, Node nvn, Node x) = 0;
75
};
76
77
/** EquivSygusInvarianceTest
78
*
79
* This class tests whether a term evaluates via evaluation
80
* operators in the deep embedding (Section 4 of Reynolds
81
* et al. CAV 2015) to fixed term d_result.
82
*
83
* For example, consider a SyGuS evaluation function eval
84
* for a synthesis conjecture with arguments x and y.
85
* Notice that the term t = (mult x y) is such that:
86
*   eval( t, 0, 1 ) ----> 0
87
* This test is invariant on the content of the second
88
* argument of t, noting that:
89
*   eval( (mult x _), 0, 1 ) ----> 0
90
* as well, via a call to EvalSygusInvarianceTest::invariant.
91
*
92
* Another example, t = ite( gt( x, y ), x, y ) is such that:
93
*   eval( t, 2, 3 ) ----> 3
94
* This test is invariant on the second child of t, noting:
95
*   eval( ite( gt( x, y ), _, y ), 2, 3 ) ----> 3
96
*/
97
40612
class EvalSygusInvarianceTest : public SygusInvarianceTest
98
{
99
 public:
100
40612
  EvalSygusInvarianceTest()
101
40612
      : d_kind(kind::UNDEFINED_KIND), d_is_conjunctive(false)
102
  {
103
40612
  }
104
105
  /** initialize this invariance test
106
   *
107
   * This sets d_terms/d_var/d_result, where we are checking whether:
108
   *   <d_kind>(d_terms) { d_var -> n } ----> d_result.
109
   * for terms n.
110
   */
111
  void init(Node conj, Node var, Node res);
112
113
  /** do evaluate with unfolding, using the cache of this class */
114
  Node doEvaluateWithUnfolding(TermDbSygus* tds, Node n);
115
116
 protected:
117
  /** does d_terms{ d_var -> nvn } still rewrite to d_result? */
118
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
119
120
 private:
121
  /** the formulas we are evaluating */
122
  std::vector<Node> d_terms;
123
  /** the variable */
124
  TNode d_var;
125
  /** the result of the evaluation */
126
  Node d_result;
127
  /** the parent kind we are checking, undefined if size(d_terms) is 1. */
128
  Kind d_kind;
129
  /** whether we are conjunctive
130
   *
131
   * If this flag is true, then the evaluation tests:
132
   *   d_terms[1] {d_var -> n} = d_result ... d_term[k] {d_var -> n} = d_result
133
   * should be processed conjunctively, that is,
134
   * <d_kind>(d_terms) { d_var -> n } = d_result only if each of the above
135
   * holds. If this flag is false, then these tests are interpreted
136
   * disjunctively, i.e. if one child test succeeds, the overall test succeeds.
137
   */
138
  bool d_is_conjunctive;
139
  /** cache of n -> the simplified form of eval( n ) */
140
  std::unordered_map<Node, Node, NodeHashFunction> d_visited;
141
};
142
143
/** EquivSygusInvarianceTest
144
*
145
* This class tests whether a builtin version of a
146
* sygus term is equivalent up to rewriting to a RHS value bvr.
147
*
148
* For example,
149
*
150
* ite( t>0, 0, 0 ) + s*0 ----> 0
151
*
152
* This test is invariant on the condition t>0 and s, since:
153
*
154
* ite( _, 0, 0 ) + _*0 ----> 0
155
*
156
* for any values of _.
157
*
158
* It also manages the case where the rewriting is invariant
159
* wrt a finite set of examples occurring in the conjecture.
160
* (EX1) : For example if our input examples are:
161
* (x,y,z) = (3,2,4), (5,2,6), (3,2,1)
162
* On these examples, we have:
163
*
164
* ite( x>y, z, 0) ---> 4,6,1
165
*
166
* which is invariant on the second argument:
167
*
168
* ite( x>y, z, _) ---> 4,6,1
169
*
170
* For details, see Reynolds et al SYNT 2017.
171
*/
172
85854
class EquivSygusInvarianceTest : public SygusInvarianceTest
173
{
174
 public:
175
2659
  EquivSygusInvarianceTest() : d_conj(nullptr) {}
176
177
  /** initialize this invariance test
178
   * tn is the sygus type for e
179
   * aconj/e are used for conjecture-specific symmetry breaking
180
   * bvr is the builtin version of the right hand side of the rewrite that we
181
   * are checking for invariance
182
   */
183
  void init(
184
      TermDbSygus* tds, TypeNode tn, SynthConjecture* aconj, Node e, Node bvr);
185
186
 protected:
187
  /** checks whether the analog of nvn still rewrites to d_bvr */
188
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
189
190
 private:
191
  /** the conjecture associated with the enumerator d_enum */
192
  SynthConjecture* d_conj;
193
  /** the enumerator associated with the term for which this test is for */
194
  Node d_enum;
195
  /** the RHS of the evaluation */
196
  Node d_bvr;
197
  /** the result of the examples
198
   * In (EX1), this is (4,6,1)
199
   */
200
  std::vector<Node> d_exo;
201
};
202
203
/** DivByZeroSygusInvarianceTest
204
 *
205
 * This class tests whether a sygus term involves
206
 * division by zero.
207
 *
208
 * For example the test for:
209
 *    ( x + ( y/0 )*2 )
210
 * is invariant on the contents of _ below:
211
 *    ( _ + ( _/0 )*_ )
212
 */
213
8071
class DivByZeroSygusInvarianceTest : public SygusInvarianceTest
214
{
215
 public:
216
  DivByZeroSygusInvarianceTest() {}
217
218
 protected:
219
  /** checks whether nvn involves division by zero. */
220
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
221
};
222
223
/** NegContainsSygusInvarianceTest
224
*
225
* This class is used to construct a minimal shape of a term that cannot
226
* be contained in at least one output of an I/O pair.
227
*
228
* Say our PBE conjecture is:
229
*
230
* exists f.
231
*   f( "abc" ) = "abc abc" ^
232
*   f( "de" ) = "de de"
233
*
234
* Then, this class is used when there is a candidate solution t[x1]
235
* such that either:
236
*   contains( "abc abc", t["abc"] ) ---> false or
237
*   contains( "de de", t["de"] ) ---> false
238
*
239
* It is used to determine whether certain generalizations of t[x1]
240
* are still sufficient to falsify one of the above containments.
241
*
242
* For example:
243
*
244
* The test for str.++( x1, "d" ) is invariant on its first argument
245
*   ...since contains( "abc abc", str.++( _, "d" ) ) ---> false
246
* The test for str.replace( "de", x1, "b" ) is invariant on its third argument
247
*   ...since contains( "abc abc", str.replace( "de", "abc", _ ) ) ---> false
248
*/
249
96
class NegContainsSygusInvarianceTest : public SygusInvarianceTest
250
{
251
 public:
252
96
  NegContainsSygusInvarianceTest() : d_isUniversal(false) {}
253
254
  /** initialize this invariance test
255
   *  e is the enumerator which we are reasoning about (associated with a synth
256
   *    fun).
257
   *  ex is the list of inputs,
258
   *  exo is the list of outputs,
259
   *  ncind is the set of possible example indices to check invariance of
260
   *  non-containment.
261
   *    For example, in the above example, when t[x1] = "ab", then this
262
   *    has the index 1 since contains("de de", "ab") ---> false but not
263
   *    the index 0 since contains("abc abc","ab") ---> true.
264
   */
265
  void init(Node e,
266
            std::vector<std::vector<Node> >& ex,
267
            std::vector<Node>& exo,
268
            std::vector<unsigned>& ncind);
269
  /** set universal
270
   *
271
   * This updates the semantics of this check such that *all* instead of some
272
   * examples must fail the containment test.
273
   */
274
6
  void setUniversal() { d_isUniversal = true; }
275
276
 protected:
277
  /**
278
   * Checks if contains( out_i, nvn[in_i] ) --> false for some I/O pair i; if
279
   * d_isUniversal is true, then we check if the rewrite holds for *all* I/O
280
   * pairs.
281
   */
282
  bool invariant(TermDbSygus* tds, Node nvn, Node x) override;
283
284
 private:
285
  /** The enumerator whose value we are considering in this invariance test */
286
  Node d_enum;
287
  /** The input examples */
288
  std::vector<std::vector<Node> > d_ex;
289
  /** The output examples for the enumerator */
290
  std::vector<Node> d_exo;
291
  /** The set of I/O pair indices i such that
292
   *    contains( out_i, nvn[in_i] ) ---> false
293
   */
294
  std::vector<unsigned> d_neg_con_indices;
295
  /** requires not being in all examples */
296
  bool d_isUniversal;
297
};
298
299
} /* CVC4::theory::quantifiers namespace */
300
} /* CVC4::theory namespace */
301
} /* CVC4 namespace */
302
303
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_INVARIANCE_H */