GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/cegis_core_connective.h Lines: 6 6 100.0 %
Date: 2021-03-23 Branches: 3 6 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file cegis_core_connective.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 Cegis core connective module.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
18
#define CVC4__THEORY__QUANTIFIERS__CEGIS_CORE_CONNECTIVE_H
19
20
#include <unordered_set>
21
22
#include "expr/node.h"
23
#include "expr/node_trie.h"
24
#include "theory/evaluator.h"
25
#include "theory/quantifiers/sygus/cegis.h"
26
#include "util/result.h"
27
28
namespace CVC4 {
29
30
class SmtEngine;
31
32
namespace theory {
33
namespace quantifiers {
34
35
/**
36
 * A trie that stores data at undetermined depth. Storing data at
37
 * undetermined depth is in contrast to the NodeTrie (expr/node_trie.h), which
38
 * assumes all data is stored at a fixed depth.
39
 *
40
 * Since data can be stored at any depth, we require both a d_children field
41
 * and a d_data field.
42
 */
43
8828
class VariadicTrie
44
{
45
 public:
46
  /** the children of this node */
47
  std::map<Node, VariadicTrie> d_children;
48
  /** the data at this node */
49
  Node d_data;
50
  /**
51
   * Add data with identifier n indexed by i, return true if data is not already
52
   * stored at the node indexed by i.
53
   */
54
  bool add(Node n, const std::vector<Node>& i);
55
  /** Is there any data in this trie that is indexed by any subset of is? */
56
  bool hasSubset(const std::vector<Node>& is) const;
57
};
58
59
/** CegisCoreConnective
60
 *
61
 * A sygus module that is specialized in handling conjectures of the form:
62
 * exists P. forall x. (A[x] => C(x)) ^ (C(x) => B(x))
63
 * That is, conjectures with a pre/post condition but no inductive relation
64
 * or other constraints. Additionally, we may have that the above conjecture
65
 * has a side condition SC, which requires that exists x. SC[x]^C(x) is
66
 * satisfiable.
67
 *
68
 * Two examples of this kind of sygus conjecture are abduction and
69
 * interpolation.
70
 *
71
 * This module implements a specific algorithm for constructing solutions
72
 * to this conjecture based on Boolean connectives and unsat cores, described
73
 * in following. We give two variants of the algorithm, both implemented as
74
 * special cases of this class. Below, let:
75
 *
76
 * pool(A) be a set of literals { c_1, ..., c_n } s.t. c_i => B for i=1,...,n,
77
 * pts(A) : a set of points { v | A[v] is true },
78
 * pool(B) : a set of literals { d_1, ..., d_m } s.t. A => d_i for i=1,...,m,
79
 * pts(B) : a set of points { v | ~B[v] is true },
80
 * cores(B) : a set of sets of literals { U_1, ..., U_p } s.t. for i=1,...,p:
81
 * - U_i is a subset of pool(B),
82
 * - A ^ U_i is unsat.
83
 * We construct pool(A)/pool(B) using enumerative SyGuS, discarding the literals
84
 * that do not match the criteria.
85
 *
86
 * Variant #1 (Interpolation)
87
 *
88
 * Let the synthesis conjecture be of the form
89
 *   exists C. forall x. A[x] => C[x] ^ C[x] => B[x]
90
 *
91
 * The high level idea is we construct solutions for C of the form
92
 *   c_1 OR ... OR c_n where c_i => B for each i=1,...,n, or
93
 *   d_1 AND ... AND d_m where A => d_i for each i=1,...,m.
94
 *
95
 * while(true){
96
 *   Let e_i = next_sygus_enum();
97
 *   // check if e_i should be added to pool(B)
98
 *   if e_i[v] is true for all v in pts(A)
99
 *     if A => e_i
100
 *       pool(B) += e_i;
101
 *     else
102
 *       pts(A) += { v } where { x -> v } is a model for A ^ ~e_i;
103
 *   // try to construct a solution based on the pool
104
 *   Let D = {}.
105
 *   while
106
 *     D[v] is true for some v in pts(B), and
107
 *     d'[v] is false for some d' in pool(B)
108
 *   {
109
 *     D += { d' }
110
 *     if D is false for all v in pts(B)
111
 *       if D => B
112
 *         return AND_{d in D}( d )
113
 *       else
114
 *         pts(B) += { v } where { x -> v } is a model for D ^ ~B
115
 *   }
116
 *
117
 *   // analogous for the other direction
118
 * }
119
 *
120
 *
121
 * Variant #2 (Abduction)
122
 *
123
 * Let the synthesis conjecture be of the form exists C. forall x. C[x] => B[x]
124
 * such that S[x] ^ C[x] is satisfiable. We refer to S as the side condition
125
 * for this conjecture. Notice that A in this variant is false, hence the
126
 * algorithm below is modified accordingly.
127
 *
128
 * The high level idea is we construct solutions for C of the form
129
 *   d_1 AND ... AND d_n
130
 * where the above conjunction is weakened based on only including conjuncts
131
 * that are in the unsat core of d_1 AND ... AND d_n => B.
132
 *
133
 * while(true){
134
 *   Let e_i = next_sygus_enum();
135
 *   // add e_i to the pool
136
 *   pool(B) += e_i;
137
 *   // try to construct a solution based on the pool
138
 *   Let D = {}.
139
 *   while
140
 *     D[v] is true for some v in pts(B), and
141
 *     d'[v] is false for some d' in pool(B) and
142
 *     no element of cores(B) is a subset of D ++ { d' }
143
 *   {
144
 *     D += { d' }
145
 *     if D is false for all v in pts(B)
146
 *       if (S ^ D) => B
147
 *         Let U be a subset of D such that S ^ U ^ ~B is unsat.
148
 *         if S ^ U is unsat
149
 *           Let W be a subset of D such that S ^ W is unsat.
150
 *             cores(B) += W
151
 *             remove some d'' in W from D
152
 *         else
153
 *           return u_1 AND ... AND u_m where U = { u_1, ..., u_m }
154
 *       else
155
 *         pts(B) += { v } where { x -> v } is a model for D ^ ~B
156
 *   }
157
 * }
158
 */
159
class CegisCoreConnective : public Cegis
160
{
161
 public:
162
  CegisCoreConnective(QuantifiersEngine* qe,
163
                      QuantifiersInferenceManager& qim,
164
                      SynthConjecture* p);
165
4376
  ~CegisCoreConnective() {}
166
  /**
167
   * Return whether this module has the possibility to construct solutions. This
168
   * is true if this module has been initialized, and the shape of the
169
   * conjecture allows us to use the core connective algorithm.
170
   */
171
  bool isActive() const;
172
173
 protected:
174
  /** do cegis-implementation-specific initialization for this class */
175
  bool processInitialize(Node conj,
176
                         Node n,
177
                         const std::vector<Node>& candidates,
178
                         std::vector<Node>& lemmas) override;
179
  /** do cegis-implementation-specific post-processing for construct candidate
180
   *
181
   * satisfiedRl is whether all refinement lemmas are satisfied under the
182
   * substitution { enums -> enum_values }.
183
   */
184
  bool processConstructCandidates(const std::vector<Node>& enums,
185
                                  const std::vector<Node>& enum_values,
186
                                  const std::vector<Node>& candidates,
187
                                  std::vector<Node>& candidate_values,
188
                                  bool satisfiedRl,
189
                                  std::vector<Node>& lems) override;
190
191
  /** construct solution
192
   *
193
   * This function is called when candidates -> candidate_values is the current
194
   * candidate solution for the synthesis conjecture.
195
   *
196
   * If this function returns true, then this class adds to solv the
197
   * a candidate solution for candidates.
198
   */
199
  bool constructSolution(const std::vector<Node>& candidates,
200
                         const std::vector<Node>& candidate_values,
201
                         std::vector<Node>& solv);
202
203
 private:
204
  /** common constants */
205
  Node d_true;
206
  Node d_false;
207
  /** The first-order datatype variable for the function-to-synthesize */
208
  TNode d_candidate;
209
  /**
210
   * Information about the pre and post conditions of the synthesis conjecture.
211
   * This maintains all information needed for producing solutions relative to
212
   * one direction of the synthesis conjecture. In other words, this component
213
   * may be focused on finding a C1 ... Cn such that A => C1 V ... V Cn
214
   * or alteratively C1 ^ ... ^ Cn such that C1 ^ ... ^ Cn => B.
215
   */
216
4376
  class Component
217
  {
218
   public:
219
4380
    Component() : d_numFalseCores(0), d_numRefPoints(0) {}
220
    /** initialize
221
     *
222
     * This initializes this component with pre/post condition given by n
223
     * and sygus constructor c.
224
     */
225
    void initialize(Node n, Node c);
226
    /** get the formula n that we initialized this with */
227
178
    Node getFormula() const { return d_this; }
228
    /** Is this component active? */
229
556
    bool isActive() const { return !d_scons.isNull(); }
230
    /** Add term n to pool whose sygus analog is s */
231
    void addToPool(Node n, Node s);
232
    /** Add a refinement point to this component */
233
    void addRefinementPt(Node id, const std::vector<Node>& pt);
234
    /** Add a false case to this component */
235
    void addFalseCore(Node id, const std::vector<Node>& u);
236
    /**
237
     * Selects a node from passerts that evaluates to false on point mv if one
238
     * exists, or otherwise returns false.
239
     * The argument mvId is an identifier used for indexing the point mv.
240
     * The argument asserts stores the current candidate solution (set D in
241
     * Variant #2 described above). If the method returns true, it updates
242
     * an (the node version of asserts) to be the conjunction of the nodes
243
     * in asserts.
244
     *
245
     * If true is returned, it is removed from passerts.
246
     */
247
    bool addToAsserts(CegisCoreConnective* p,
248
                      std::vector<Node>& passerts,
249
                      const std::vector<Node>& mvs,
250
                      Node mvId,
251
                      std::vector<Node>& asserts,
252
                      Node& an);
253
254
    /**
255
     * Get a refinement point that n evalutes to true on, taken from the
256
     * d_refinementPt trie, and store it in ss. The set visited is the set
257
     * of leaf nodes (reference by their data) that we have already processed
258
     * and should be ignored.
259
     */
260
    Node getRefinementPt(CegisCoreConnective* p,
261
                         Node n,
262
                         std::unordered_set<Node, NodeHashFunction>& visited,
263
                         std::vector<Node>& ss);
264
    /** Get term pool, i.e. pool(A)/pool(B) in the algorithms above */
265
    void getTermPool(std::vector<Node>& passerts) const;
266
    /**
267
     * Get the sygus solution corresponding to the Boolean connective for
268
     * this component applied to conj. In particular, this returns a
269
     * right-associative chain of applications of sygus constructor d_scons
270
     * to the sygus analog of formulas in conj.
271
     */
272
    Node getSygusSolution(std::vector<Node>& conjs) const;
273
    /** debug print summary (for debugging) */
274
    void debugPrintSummary(std::ostream& os) const;
275
276
   private:
277
    /** The original formula for the pre/post condition A/B. */
278
    Node d_this;
279
    /**
280
     * The sygus constructor for constructing solutions based on the core
281
     * connective algorithm. This is a sygus datatype constructor that
282
     * encodes applications of AND or OR.
283
     */
284
    Node d_scons;
285
    /** This is pool(A)/pool(B) in the algorithms above */
286
    std::vector<Node> d_cpool;
287
    /**
288
     * A map from the formulas in the above vector to their sygus analog.
289
     */
290
    std::map<Node, Node> d_cpoolToSol;
291
    /**
292
     * An index of list of predicates such that each list ( P1, ..., Pn )
293
     * indexed by this trie is such that P1 ^ ... ^ Pn ^ S is unsatisfiable,
294
     * where S is the side condition of our synthesis conjecture. We call this
295
     * a "false core". This set is "cores(B)" in Variant #2 above.
296
     */
297
    VariadicTrie d_falseCores;
298
    /**
299
     * The number of points that have been added to the above trie, for
300
     * debugging.
301
     */
302
    unsigned d_numFalseCores;
303
    /**
304
     * An index of the points that satisfy d_this.
305
     */
306
    NodeTrie d_refinementPt;
307
    /**
308
     * The number of points that have been added to the above trie, for
309
     * debugging.
310
     */
311
    unsigned d_numRefPoints;
312
  };
313
  /** Above information for the precondition of the synthesis conjecture */
314
  Component d_pre;
315
  /** Above information for the postcondition of the synthesis conjecture */
316
  Component d_post;
317
  /**
318
   * The free variables that may appear in the pre/post condition, and our
319
   * pools of predicates.
320
   */
321
  std::vector<Node> d_vars;
322
  /**
323
   * The evaluation term of the form:
324
   *   (DT_SYGUS_EVAL d_candidate d_vars[0]...d_vars[n])
325
   * This is used to convert enumerated sygus terms t to their builtin
326
   * equivalent via rewriting d_eterm * { d_candidate -> t }.
327
   */
328
  Node d_eterm;
329
  /**
330
   * The side condition of the conjecture. If this is non-null, then
331
   * this node is a formula such that (builtin) solutions t' are such that
332
   * t' ^ d_sc is satisfiable. Notice that the free variables of d_sc are
333
   * a subset of d_vars.
334
   */
335
  Node d_sc;
336
  //-----------------------------------for SMT engine calls
337
  /**
338
   * Assuming smt has just been called to check-sat and returned "SAT", this
339
   * method adds the model for d_vars to mvs.
340
   */
341
  void getModel(SmtEngine& smt, std::vector<Node>& mvs) const;
342
  /**
343
   * Assuming smt has just been called to check-sat and returned "UNSAT", this
344
   * method get the unsat core and adds it to uasserts.
345
   *
346
   * The assertions in the argument queryAsserts (which we are not interested
347
   * in tracking in the unsat core) are excluded from uasserts.
348
   * If one of the formulas in queryAsserts was in the unsat core, then this
349
   * method returns true. Otherwise, this method returns false.
350
   */
351
  bool getUnsatCore(
352
      SmtEngine& smt,
353
      const std::unordered_set<Node, NodeHashFunction>& queryAsserts,
354
      std::vector<Node>& uasserts) const;
355
  /**
356
   * Return the result of checking satisfiability of formula n.
357
   * If n was satisfiable, then we store the model for d_vars in mvs.
358
   */
359
  Result checkSat(Node n, std::vector<Node>& mvs) const;
360
  //-----------------------------------end for SMT engine calls
361
  //-----------------------------------for evaluation
362
  /**
363
   * Return the evaluation of n under the substitution { d_vars -> mvs }.
364
   * If id is non-null, then id is a unique identifier for mvs, and we cache
365
   * the result of n for this point.
366
   */
367
  Node evaluate(Node n, Node id, const std::vector<Node>& mvs);
368
  /** A cache of the above function */
369
  std::unordered_map<Node,
370
                     std::unordered_map<Node, Node, NodeHashFunction>,
371
                     NodeHashFunction>
372
      d_eval_cache;
373
  /** The evaluator utility used for the above function */
374
  Evaluator d_eval;
375
  //-----------------------------------end for evaluation
376
377
  /** Construct solution from pool
378
   *
379
   * This is the main body of the core connective algorithm, which attempts
380
   * to build a solution based on one direction (pre/post) of the synthesis
381
   * conjecture.
382
   *
383
   * It takes as input:
384
   * - a component ccheck that maintains information regarding the direction
385
   * we are trying to build a solution for,
386
   * - the current set of assertions asserts that comprise the current solution
387
   * we are building,
388
   * - the current pool passerts of available assertions that we may add to
389
   * asserts.
390
   *
391
   * This implements the while loop in the algorithms above. If this method
392
   * returns a non-null node, then this is a solution for the given synthesis
393
   * conjecture.
394
   */
395
  Node constructSolutionFromPool(Component& ccheck,
396
                                 std::vector<Node>& asserts,
397
                                 std::vector<Node>& passerts);
398
};
399
400
}  // namespace quantifiers
401
}  // namespace theory
402
}  // namespace CVC4
403
404
#endif /* CVC4__THEORY__QUANTIFIERS__SYGUS_REPAIR_CONST_H */