GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/sygus_extension.h Lines: 5 5 100.0 %
Date: 2021-03-22 Branches: 1 2 50.0 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_extension.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Dejan Jovanovic
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 The sygus extension of the theory of datatypes.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H
18
#define CVC4__THEORY__DATATYPES__SYGUS_EXTENSION_H
19
20
#include <iostream>
21
#include <map>
22
23
#include "context/cdhashmap.h"
24
#include "context/cdhashset.h"
25
#include "context/context.h"
26
#include "expr/node.h"
27
#include "theory/datatypes/sygus_simple_sym.h"
28
#include "theory/decision_manager.h"
29
#include "theory/quantifiers/sygus_sampler.h"
30
#include "theory/quantifiers/term_database.h"
31
32
namespace CVC4 {
33
namespace theory {
34
namespace quantifiers {
35
class SynthConjecture;
36
}
37
namespace datatypes {
38
39
class InferenceManager;
40
41
/**
42
 * This is the sygus extension of the decision procedure for quantifier-free
43
 * inductive datatypes. At a high level, this class takes as input a
44
 * set of asserted testers is-C1( x ), is-C2( x.1 ), is-C3( x.2 ), and
45
 * generates lemmas that restrict the models of x, if x is a "sygus enumerator"
46
 * (see TermDbSygus::registerEnumerator).
47
 *
48
 * Some of these techniques are described in these papers:
49
 * "Refutation-Based Synthesis in SMT", Reynolds et al 2017.
50
 * "Sygus Techniques in the Core of an SMT Solver", Reynolds et al 2017.
51
 *
52
 * This class enforces two decisions stragies via calls to registerStrategy
53
 * of the owning theory's DecisionManager:
54
 * (1) Positive decisions on the active guards G of enumerators e registered
55
 * to this class. These assert "there are more values to enumerate for e".
56
 * (2) Positive bounds (DT_SYGUS_BOUND m n) for "measure terms" m (see below),
57
 * where n is a non-negative integer. This asserts "the measure of terms
58
 * we are enumerating for enumerators whose measure term m is at most n",
59
 * where measure is commonly term size, but can also be height.
60
 *
61
 * We prioritize decisions of form (1) before (2). Both kinds of decision are
62
 * critical for solution completeness, which is enforced by DecisionManager.
63
 */
64
class SygusExtension
65
{
66
  typedef context::CDHashMap< Node, int, NodeHashFunction > IntMap;
67
  typedef context::CDHashMap< Node, Node, NodeHashFunction > NodeMap;
68
  typedef context::CDHashMap< Node, bool, NodeHashFunction > BoolMap;
69
  typedef context::CDHashSet<Node, NodeHashFunction> NodeSet;
70
71
 public:
72
  SygusExtension(TheoryState& s,
73
                 InferenceManager& im,
74
                 quantifiers::TermDbSygus* tds,
75
                 DecisionManager* dm);
76
  ~SygusExtension();
77
  /**
78
   * Notify this class that tester for constructor tindex has been asserted for
79
   * n. Exp is the literal corresponding to this tester. This method may send
80
   * lemmas via inference manager, for details see assertTesterInternal below.
81
   * These lemmas are sent out on the output channel of datatypes by the caller.
82
   */
83
  void assertTester(int tindex, TNode n, Node exp);
84
  /**
85
   * Notify this class that literal n has been asserted with the given
86
   * polarity. This method may send lemmas via inference manager, for instance
87
   * based on inferring consequences of (not) n. One example is if n is
88
   * (DT_SIZE_BOUND x n), we add the lemma:
89
   *   (DT_SIZE_BOUND x n) <=> ((DT_SIZE x) <= n )
90
   */
91
  void assertFact(Node n, bool polarity);
92
  /** pre-register term n
93
   *
94
   * This is called when n is pre-registered with the theory of datatypes.
95
   * If n is a sygus enumerator, then we may send lemmas via inference manager
96
   * that are used to enforce fairness regarding the size of n.
97
   */
98
  void preRegisterTerm(TNode n);
99
  /** check
100
   *
101
   * This is called at last call effort, when the current model assignment is
102
   * satisfiable according to the quantifier-free decision procedures and a
103
   * model is built. This method may send lemmas via inference manager based
104
   * on dynamic symmetry breaking techniques, based on the model values of
105
   * all preregistered enumerators.
106
   */
107
  void check();
108
109
 private:
110
  /** The theory state of the datatype theory */
111
  TheoryState& d_state;
112
  /** The inference manager of the datatype theory */
113
  InferenceManager& d_im;
114
  /** Pointer to the sygus term database */
115
  quantifiers::TermDbSygus* d_tds;
116
  /** Pointer to the decision manager */
117
  DecisionManager* d_dm;
118
  /** the simple symmetry breaking utility */
119
  SygusSimpleSymBreak d_ssb;
120
  /**
121
   * Map from terms to the index of the tester that is asserted for them in
122
   * the current SAT context. In other words, if d_testers[n] = 2, then the
123
   * tester is-C_2(n) is asserted in this SAT context.
124
   */
125
  IntMap d_testers;
126
  /**
127
   * Map from terms to the tester asserted for them. In the example above,
128
   * d_testers[n] = is-C_2(n).
129
   */
130
  NodeMap d_testers_exp;
131
  /**
132
   * The set of (selector chain) terms that are active in the current SAT
133
   * context. A selector chain term S_n( ... S_1( x )... ) is active if either:
134
   * (1) n=0 and x is a sygus enumerator,
135
   *   or:
136
   * (2.1) S_{n-1}( ... S_1( x )) is active,
137
   * (2.2) is-C( S_{n-1}( ... S_1( x )) ) is asserted in this SAT context, and
138
   * (2.3) S_n is a selector for constructor C.
139
   */
140
  NodeSet d_active_terms;
141
  /**
142
   * Map from enumerators to a lower bound on their size in the current SAT
143
   * context.
144
   */
145
  IntMap d_currTermSize;
146
  /** zero */
147
  Node d_zero;
148
  /** true */
149
  Node d_true;
150
  /**
151
   * Map from terms (selector chains) to their anchors. The anchor of a
152
   * selector chain S1( ... Sn( x ) ... ) is x.
153
   */
154
  std::unordered_map<Node, Node, NodeHashFunction> d_term_to_anchor;
155
  /**
156
   * Map from anchors to the conjecture they are associated with.
157
   */
158
  std::map<Node, quantifiers::SynthConjecture*> d_anchor_to_conj;
159
  /**
160
   * Map from terms (selector chains) to their depth. The depth of a selector
161
   * chain S1( ... Sn( x ) ... ) is:
162
   *   weight( S1 ) + ... + weight( Sn ),
163
   * where weight is the selector weight of Si
164
   * (see SygusTermDatabase::getSelectorWeight).
165
   */
166
  std::unordered_map<Node, unsigned, NodeHashFunction> d_term_to_depth;
167
  /**
168
   * Map from terms (selector chains) to whether they are the topmost term
169
   * of their type. For example, if:
170
   *   S1 : T1 -> T2
171
   *   S2 : T2 -> T2
172
   *   S3 : T2 -> T1
173
   *   S4 : T1 -> T3
174
   * Then, x, S1( x ), and S4( S3( S2( S1( x ) ) ) ) are top-level terms,
175
   * whereas S2( S1( x ) ) and S3( S2( S1( x ) ) ) are not.
176
   */
177
  std::unordered_map<Node, bool, NodeHashFunction> d_is_top_level;
178
  /**
179
   * Returns true if the selector chain n is top-level based on the above
180
   * definition, when tn is the type of n.
181
   */
182
  bool computeTopLevel( TypeNode tn, Node n );
183
private:
184
 /** This caches all information regarding symmetry breaking for an anchor. */
185
629
 class SearchCache
186
 {
187
  public:
188
629
    SearchCache(){}
189
    /**
190
     * A cache of all search terms for (types, sizes). See registerSearchTerm
191
     * for definition of search terms.
192
     */
193
    std::map< TypeNode, std::map< unsigned, std::vector< Node > > > d_search_terms;
194
    /** A cache of all symmetry breaking lemma templates for (types, sizes). */
195
    std::map<TypeNode, std::map<uint64_t, std::vector<Node>>> d_sbLemmas;
196
    /** search value
197
     *
198
     * For each sygus type, a map from a builtin term to a sygus term for that
199
     * type that we encountered during the search whose analog rewrites to that
200
     * term. The range of this map can be updated if we later encounter a sygus
201
     * term that also rewrites to the builtin value but has a smaller term size.
202
     */
203
    std::map<TypeNode, std::unordered_map<Node, Node, NodeHashFunction>>
204
        d_search_val;
205
    /** the size of terms in the range of d_search val. */
206
    std::map<TypeNode, std::unordered_map<Node, unsigned, NodeHashFunction>>
207
        d_search_val_sz;
208
    /** For each term, whether this cache has processed that term */
209
    std::unordered_set<Node, NodeHashFunction> d_search_val_proc;
210
  };
211
  /** An instance of the above cache, for each anchor */
212
  std::map< Node, SearchCache > d_cache;
213
  //-----------------------------------traversal predicates
214
  /** pre/post traversal predicates for each type, variable
215
   *
216
   * This stores predicates (pre, post) whose semantics correspond to whether
217
   * a variable has occurred by a (pre, post) traversal of a symbolic term,
218
   * where index = 0 corresponds to pre, index = 1 corresponds to post. For
219
   * details, see getTraversalPredicate below.
220
   */
221
  std::map<TypeNode, std::map<Node, Node>> d_traversal_pred[2];
222
  /** traversal applications to Boolean variables
223
   *
224
   * This maps each application of a traversal predicate pre_x( t ) or
225
   * post_x( t ) to a fresh Boolean variable.
226
   */
227
  std::map<Node, Node> d_traversal_bool;
228
  /** get traversal predicate
229
   *
230
   * Get the predicates (pre, post) whose semantics correspond to whether
231
   * a variable has occurred by this point in a (pre, post) traversal of a term.
232
   * The type of getTraversalPredicate(tn, n, _) is tn -> Bool.
233
   *
234
   * For example, consider the term:
235
   *   f( x_1, g( x_2, x_3 ) )
236
   * and a left-to-right, depth-first traversal of this term. Let e be
237
   * a variable of the same type as this term. We say that for the above term:
238
   *   pre_{x_1} is false for e, e.1 and true for e.2, e.2.1, e.2.2
239
   *   pre_{x_2} is false for e, e.1, e.2, e.2.1, and true for e.2.2
240
   *   pre_{x_3} is false for e, e.1, e.2, e.2.1, e.2.2
241
   *   post_{x_1} is true for e.1, e.2.1, e.2.2, e.2, e
242
   *   post_{x_2} is false for e.1 and true for e.2.1, e.2.2, e.2, e
243
   *   post_{x_3} is false for e.1, e.2.1 and true for e.2.2, e.2, e
244
   *
245
   * We enforce a symmetry breaking scheme for each enumerator e that is
246
   * "variable-agnostic" (see argument isVarAgnostic in registerEnumerator)
247
   * that ensures the variables are ordered. This scheme makes use of these
248
   * predicates, described in the following:
249
   *
250
   * Let x_1, ..., x_m be variables that occur in the same subclass in the type
251
   * of e (see TermDbSygus::getSubclassForVar).
252
   * For i = 1, ..., m:
253
   *   // each variable does not occur initially in a traversal of e
254
   *   ~pre_{x_i}( e ) AND
255
   *   // for each subterm of e
256
   *   template z.
257
   *     // if this is variable x_i, then x_{i-1} must have already occurred
258
   *     is-x_i( z ) => pre_{x_{i-1}}( z ) AND
259
   *     for args a = 1...n
260
   *       // pre-definition for each argument of this term
261
   *       pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} ) AND
262
   *     // post-definition for this term
263
   *     post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z )
264
   *
265
   * For clarity, above we have written pre and post as first-order predicates.
266
   * However, applications of pre/post should be seen as indexed Boolean
267
   * variables. The reason for this is pre and post cannot be given a consistent
268
   * semantics. For example, consider term f( x_1, x_1 ) and enumerator variable
269
   * e of the same type over which we are encoding a traversal. We have that
270
   * pre_{x_1}( e.1 ) is false and pre_{x_1}( e.2 ) is true, although the model
271
   * values for e.1 and e.2 are equal. Instead, pre_{x_1}( e.1 ) should be seen
272
   * as a Boolean variable V_pre_{x_1,e.1} indexed by x_1 and e.1. and likewise
273
   * for e.2. We convert all applications of pre/post to Boolean variables in
274
   * the method eliminateTraversalPredicates below. Nevertheless, it is
275
   * important that applications pre and post are encoded as APPLY_UF
276
   * applications so that they behave as expected under substitutions. For
277
   * example, pre_{x_1}( z.1 ) { z -> e.2 } results in pre_{x_1}( e.2.1 ), which
278
   * after eliminateTraversalPredicates is V_pre_{x_1, e.2.1}.
279
   */
280
  Node getTraversalPredicate(TypeNode tn, Node n, bool isPre);
281
  /** eliminate traversal predicates
282
   *
283
   * This replaces all applications of traversal predicates P( x ) in n with
284
   * unique Boolean variables, given by d_traversal_bool[ P( x ) ], and
285
   * returns the result.
286
   */
287
  Node eliminateTraversalPredicates(Node n);
288
  //-----------------------------------end traversal predicates
289
  /** a sygus sampler object for each (anchor, sygus type) pair
290
   *
291
   * This is used for the sygusRewVerify() option to verify the correctness of
292
   * the rewriter.
293
   */
294
  std::map<Node, std::map<TypeNode, quantifiers::SygusSampler>> d_sampler;
295
  /** Assert tester internal
296
   *
297
   * This function is called when the tester with index tindex is asserted for
298
   * n, exp is the tester predicate. For example, for grammar:
299
   *   A -> A+A | x | 1 | 0
300
   * when is_+( d ) is asserted,
301
   * assertTesterInternal(0, s( d ), is_+( s( d ) ),...) is called. This
302
   * function may send lemmas via inference manager.
303
   *
304
   * These lemmas are of various forms, including:
305
   * (1) dynamic symmetry breaking clauses for subterms of n (those added to
306
   * lemmas on calls to addSymBreakLemmasFor, see function below),
307
   * (2) static symmetry breaking clauses for subterms of n (those added to
308
   * lemmas on getSimpleSymBreakPred, see function below),
309
   * (3) conjecture-specific symmetry breaking lemmas, see
310
   * SynthConjecture::getSymmetryBreakingPredicate,
311
   * (4) fairness conflicts if sygusFair() is SygusFairMode::DIRECT, e.g.:
312
   *    size( d ) <= 1 V ~is-C1( d ) V ~is-C2( d.1 )
313
   * where C1 and C2 are non-nullary constructors.
314
   */
315
  void assertTesterInternal(int tindex, TNode n, Node exp);
316
  /**
317
   * This function is called when term n is registered to the theory of
318
   * datatypes. It makes the appropriate call to registerSearchTerm below,
319
   * if applicable.
320
   */
321
  void registerTerm(Node n);
322
323
  //------------------------dynamic symmetry breaking
324
  /** Register search term
325
   *
326
   * This function is called when selector chain n of the form
327
   * S_1( ... S_m( x ) ... ) is registered to the theory of datatypes, where
328
   * tn is the type of n, d indicates the depth of n (the sum of weights of the
329
   * selectors S_1...S_m), and topLevel is whether n is a top-level term
330
   * (see d_is_top_level). We refer to n as a "search term".
331
   *
332
   * The purpose of this function is to notify this class that symmetry breaking
333
   * lemmas should be instantiated for n. Any symmetry breaking lemmas that
334
   * are active for n (see description of addSymBreakLemmasFor) are added to
335
   * lemmas in this call.
336
   */
337
  void registerSearchTerm(TypeNode tn, unsigned d, Node n, bool topLevel);
338
  /** Register search value
339
   *
340
   * This function is called when a selector chain n has been assigned a model
341
   * value nv. This function calls itself recursively so that extensions of the
342
   * selector chain n are registered with all the subterms of nv. For example,
343
   * if we call this function with:
344
   *   n = x, nv = +( 1(), x() )
345
   * we make recursive calls with:
346
   *   n = x.1, nv = 1() and n = x.2, nv = x()
347
   *
348
   * a : the anchor of n,
349
   * d : the depth of n.
350
   *
351
   * This function determines if the value nv is equivalent via rewriting to
352
   * any previously registered search values for anchor a. If so, we construct
353
   * a symmetry breaking lemma template and register it in d_cache[a]. For
354
   * example, for grammar:
355
   *   A -> A+A | x | 1 | 0
356
   * Registering search value d -> x followed by d -> +( x, 0 ) results in the
357
   * construction of the symmetry breaking lemma template:
358
   *   ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 )
359
   * which is stored in d_cache[a].d_sbLemmas. This lemma is instantiated with
360
   * z -> t for all terms t of appropriate depth, including d.
361
   * This function strengthens blocking clauses using generalization techniques
362
   * described in Reynolds et al SYNT 2017.
363
   *
364
   * The return value of this function is an abstraction of model assignment
365
   * of nv to n, or null if we wish to exclude the model assignment nv to n.
366
   * The return value of this method is different from nv itself, e.g. if it
367
   * contains occurrences of the "any constant" constructor. For example, if
368
   * nv is C_+( C_x(), C_{any_constant}( 5 ) ), then the return value of this
369
   * function will either be null, or C_+( C_x(), C_{any_constant}( n.1.0 ) ),
370
   * where n.1.0 is the appropriate selector chain applied to n. We build this
371
   * abstraction since the semantics of C_{any_constant} is "any constant" and
372
   * not "some constant". Thus, we should consider the subterm
373
   * C_{any_constant}( 5 ) above to be an unconstrained variable (as represented
374
   * by a selector chain), instead of the concrete value 5.
375
   *
376
   * The flag isVarAgnostic is whether "a" is a variable agnostic enumerator. If
377
   * this is the case, we restrict symmetry breaking to subterms of n on its
378
   * leftmost subchain. For example, consider the grammar:
379
   *   A -> B=B
380
   *   B -> B+B | x | y | 0
381
   * Say we are registering the search value x = y+x. Notice that this value is
382
   * ordered. If a were a variable-agnostic enumerator of type A in this
383
   * case, we would only register x = y+x and x, and not y+x or y, since the
384
   * latter two terms are not leftmost subterms in this value. If we did on the
385
   * other hand register y+x, we would be prevented from solutions like x+y = 0
386
   * later, since x+y is equivalent to (the already registered value) y+x.
387
   *
388
   * If doSym is false, we are not performing symmetry breaking on n. This flag
389
   * is set to false on branches of n that are not leftmost.
390
   */
391
  Node registerSearchValue(Node a,
392
                           Node n,
393
                           Node nv,
394
                           unsigned d,
395
                           bool isVarAgnostic,
396
                           bool doSym);
397
  /** Register symmetry breaking lemma
398
   *
399
   * This function adds the symmetry breaking lemma template lem for terms of
400
   * type tn with anchor a. This is added to d_cache[a].d_sbLemmas. Notice that
401
   * we use lem as a template with free variable x, e.g. our template is:
402
   *   (lambda ((x tn)) lem)
403
   * where x = getFreeVar( tn ). For all search terms t of the appropriate
404
   * depth, we send the lemma lem{ x -> t } via the inference manager.
405
   *
406
   * The argument sz indicates the size of terms that the lemma applies to, e.g.
407
   *   ~is_+( z ) has size 1
408
   *   ~is_+( z ) V ~is_x( z.1 ) V ~is_0( z.2 ) has size 1
409
   *   ~is_+( z ) V ~is_+( z.1 ) has size 2
410
   * This is equivalent to sum of weights of constructors corresponding to each
411
   * tester, e.g. above + has weight 1, and x and 0 have weight 0.
412
   */
413
  void registerSymBreakLemma(TypeNode tn, Node lem, unsigned sz, Node a);
414
  /** Register symmetry breaking lemma for value
415
   *
416
   * This function adds a symmetry breaking lemma template for selector chains
417
   * with anchor a, that effectively states that val should never be a subterm
418
   * of any value for a.
419
   *
420
   * et : an "invariance test" (see sygus/sygus_invariance.h) which states a
421
   * criterion that val meets, which is the reason for its exclusion. This is
422
   * used for generalizing the symmetry breaking lemma template.
423
   * valr : if non-null, this states a value that should *not* be excluded by
424
   * the symmetry breaking lemma template, which is a restriction to the above
425
   * generalization.
426
   *
427
   * This function may add instances of the symmetry breaking template for
428
   * existing search terms, which are sent via the inference manager.
429
   */
430
  void registerSymBreakLemmaForValue(Node a,
431
                                     Node val,
432
                                     quantifiers::SygusInvarianceTest& et,
433
                                     Node valr,
434
                                     std::map<TypeNode, int>& var_count);
435
  /** Add symmetry breaking lemmas for term
436
   *
437
   * Sends all active symmetry breaking lemmas for selector chain t via the
438
   * inference manager. A symmetry breaking lemma L is active for t based on
439
   * three factors:
440
   * (1) the current search size sz(a) for its anchor a,
441
   * (2) the depth d of term t (see d_term_to_depth),
442
   * (3) the size sz(L) of the symmetry breaking lemma L.
443
   * In particular, L is active if sz(L) <= sz(a) - d. In other words, a
444
   * symmetry breaking lemma is active if it is intended to block terms of
445
   * size sz(L), and the maximum size that t can take in the current search,
446
   * sz(a)-d, is greater than or equal to this value.
447
   *
448
   * tn : the type of term t,
449
   * a : the anchor of term t,
450
   * d : the depth of term t.
451
   */
452
  void addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d, Node a);
453
  /** calls the above function where a is the anchor t */
454
  void addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d);
455
  //------------------------end dynamic symmetry breaking
456
457
  /** Get relevancy condition
458
   *
459
   * This returns (the negation of) a predicate that holds in the contexts in
460
   * which the selector chain n is specified. For example, the negation of the
461
   * relevancy condition for sel_{C2,1}( sel_{C1,1}( d ) ) is
462
   *    ~( is-C1( d ) ^ is-C2( sel_{C1,1}( d ) ) )
463
   * If shared selectors are enabled, this is a conjunction of disjunctions,
464
   * since shared selectors may apply to multiple constructors.
465
   */
466
  Node getRelevancyCondition( Node n );
467
  /** Cache of the above function */
468
  std::map<Node, Node> d_rlv_cond;
469
470
  //------------------------static symmetry breaking
471
  /** Get simple symmetry breakind predicate
472
   *
473
   * This function returns the "static" symmetry breaking lemma template for
474
   * terms with type tn and constructor index tindex, for the given depth. This
475
   * includes inferences about size with depth=0. Given grammar:
476
   *   A -> ite( B, A, A ) | A+A | x | 1 | 0
477
   *   B -> A = A
478
   * Examples of static symmetry breaking lemma templates are:
479
   *   for +, depth 0: size(z)=size(z.1)+size(z.2)+1
480
   *   for +, depth 1: ~is-0( z.1 ) ^ ~is-0( z.2 ) ^ F
481
   *     where F ensures the constructor of z.1 is less than that of z.2 based
482
   *     on some ordering.
483
   *   for ite, depth 1: z.2 != z.3
484
   * These templates can be thought of as "hard-coded" cases of dynamic symmetry
485
   * breaking lemma templates. Notice that the above lemma templates are in
486
   * terms of getFreeVar( tn ), hence only one is created per
487
   * (constructor, depth). A static symmetry break lemma template F[z] for
488
   * constructor C are included in lemmas of the form:
489
   *   is-C( t ) => F[t]
490
   * where t is a search term, see registerSearchTerm for definition of search
491
   * term.
492
   *
493
   * usingSymCons: whether we are using symbolic constructors for subterms in
494
   * the type tn,
495
   * isVarAgnostic: whether the terms we are enumerating are agnostic to
496
   * variables.
497
   *
498
   * The latter two options may affect the form of the predicate we construct.
499
   */
500
  Node getSimpleSymBreakPred(Node e,
501
                             TypeNode tn,
502
                             int tindex,
503
                             unsigned depth,
504
                             bool usingSymCons,
505
                             bool isVarAgnostic);
506
  /** Cache of the above function */
507
  std::map<Node,
508
           std::map<TypeNode,
509
                    std::map<int, std::map<bool, std::map<unsigned, Node>>>>>
510
      d_simple_sb_pred;
511
  /**
512
   * For each search term, this stores the maximum depth for which we have added
513
   * a static symmetry breaking lemma.
514
   *
515
   * This should be user context-dependent if sygus is updated to work in
516
   * incremental mode.
517
   */
518
  std::unordered_map<Node, unsigned, NodeHashFunction> d_simple_proc;
519
  //------------------------end static symmetry breaking
520
521
  /** Get the canonical free variable for type tn */
522
  TNode getFreeVar( TypeNode tn );
523
  /** get term order predicate
524
   *
525
   * Assuming that n1 and n2 are children of a commutative operator, this
526
   * returns a symmetry breaking predicate that can be instantiated for n1 and
527
   * n2 while preserving satisfiability. By default, this is the predicate
528
   *   ( DT_SIZE n1 ) >= ( DT_SIZE n2 )
529
   */
530
  Node getTermOrderPredicate( Node n1, Node n2 );
531
532
 private:
533
  /**
534
   * Map from registered variables to whether they are a sygus enumerator.
535
   *
536
   * This should be user context-dependent if sygus is updated to work in
537
   * incremental mode.
538
   */
539
  std::map<Node, bool> d_register_st;
540
  //----------------------search size information
541
  /**
542
   * Checks whether e is a sygus enumerator, that is, a term for which this
543
   * class will track size for.
544
   *
545
   * We associate each sygus enumerator e with a "measure term", which is used
546
   * for bounding the size of terms for the models of e. The measure term for a
547
   * sygus enumerator may be e itself (if e has an active guard), or an
548
   * arbitrary sygus variable otherwise. A measure term m is one for which our
549
   * decision strategy decides on literals of the form (DT_SYGUS_BOUND m n).
550
   *
551
   * After determining the measure term m for e, if applicable, we initialize
552
   * SygusSizeDecisionStrategy for m below. This may result in lemmas sent via
553
   * the inference manager.
554
   */
555
  void registerSizeTerm(Node e);
556
  /** A decision strategy for each measure term allocated by this class */
557
826
  class SygusSizeDecisionStrategy : public DecisionStrategyFmf
558
  {
559
   public:
560
    SygusSizeDecisionStrategy(InferenceManager& im, Node t, TheoryState& s);
561
    /** the measure term */
562
    Node d_this;
563
    /**
564
     * For each size n, an explanation for why this measure term has size at
565
     * most n. This is typically the literal (DT_SYGUS_BOUND m n), which
566
     * we call the (n^th) "fairness literal" for m.
567
     */
568
    std::map< unsigned, Node > d_search_size_exp;
569
    /**
570
     * For each size, whether we have called SygusExtension::notifySearchSize.
571
     */
572
    std::map< unsigned, bool > d_search_size;
573
    /**
574
     * The current search size. This corresponds to the number of times
575
     * incrementCurrentSearchSize has been called for this measure term.
576
     */
577
    unsigned d_curr_search_size;
578
    /** the list of all enumerators whose measure term is this */
579
    std::vector< Node > d_anchors;
580
    /** get or make the measure value
581
     *
582
     * The measure value is an integer variable v that is a (symbolic) integer
583
     * value that is constrained to be less than or equal to the current search
584
     * size. For example, if we are using the fairness strategy
585
     * SygusFairMode::DT_SIZE (see options/datatype_options.h), then we
586
     * constrain: (DT_SYGUS_BOUND m n) <=> (v <= n) for all asserted fairness
587
     * literals. Then, if we are enforcing fairness based on the maximum size,
588
     * we assert: (DT_SIZE e) <= v for all enumerators e.
589
     */
590
    Node getOrMkMeasureValue();
591
    /** get or make the active measure value
592
     *
593
     * The active measure value av is an integer variable that corresponds to
594
     * the (symbolic) value of the sum of enumerators that are yet to be
595
     * registered. This is to enforce the "sum of measures" strategy. For
596
     * example, if we are using the fairness strategy SygusFairMode::DT_SIZE,
597
     * then initially av is equal to the measure value v, and the constraints
598
     *   (DT_SYGUS_BOUND m n) <=> (v <= n)
599
     * are added as before. When an enumerator e is registered, we add the
600
     * lemma:
601
     *   av = (DT_SIZE e) + av'
602
     * and update the active measure value to av'. This ensures that the sum
603
     * of sizes of active enumerators is at most n.
604
     *
605
     * If the flag mkNew is set to true, then we return a fresh variable and
606
     * update the active measure value.
607
     */
608
    Node getOrMkActiveMeasureValue(bool mkNew = false);
609
    /** Returns the s^th fairness literal for this measure term. */
610
    Node mkLiteral(unsigned s) override;
611
    /** identify */
612
1300595
    std::string identify() const override
613
    {
614
1300595
      return std::string("sygus_enum_size");
615
    }
616
617
   private:
618
    /** The inference manager we are using */
619
    InferenceManager& d_im;
620
    /** the measure value */
621
    Node d_measure_value;
622
    /** the sygus measure value */
623
    Node d_measure_value_active;
624
  };
625
  /** the above information for each registered measure term */
626
  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>> d_szinfo;
627
  /** map from enumerators (anchors) to their associated measure term */
628
  std::map< Node, Node > d_anchor_to_measure_term;
629
  /** map from enumerators (anchors) to their active guard*/
630
  std::map< Node, Node > d_anchor_to_active_guard;
631
  /** map from enumerators (anchors) to a decision stratregy for that guard */
632
  std::map<Node, std::unique_ptr<DecisionStrategy>> d_anchor_to_ag_strategy;
633
  /** generic measure term
634
   *
635
   * This is a global term that is used as the measure term for all sygus
636
   * enumerators that do not have active guards. This class enforces that
637
   * all enumerators have size at most n, where n is the minimal integer
638
   * such that (DT_SYGUS_BOUND d_generic_measure_term n) is asserted.
639
   */
640
  Node d_generic_measure_term;
641
  /**
642
   * This increments the current search size for measure term m. This may
643
   * cause lemmas to be added to lemmas based on the fact that symmetry
644
   * breaking lemmas are now relevant for new search terms, see discussion
645
   * of how search size affects which lemmas are relevant above
646
   * addSymBreakLemmasFor.
647
   */
648
  void incrementCurrentSearchSize(TNode m);
649
  /**
650
   * Notify this class that we are currently searching for terms of size at
651
   * most s as model values for measure term m. Literal exp corresponds to the
652
   * explanation of why the measure term has size at most n. This calls
653
   * incrementSearchSize above, until the total number of times we have called
654
   * incrementSearchSize so far is at least s.
655
   */
656
  void notifySearchSize(TNode m, uint64_t s, Node exp);
657
  /** Allocates a SygusSizeDecisionStrategy object in d_szinfo. */
658
  void registerMeasureTerm( Node m );
659
  /**
660
   * Return the current search size for arbitrary term n. This is the current
661
   * search size of the anchor of n.
662
   */
663
  unsigned getSearchSizeFor( Node n );
664
  /** return the current search size for enumerator (anchor) e */
665
  unsigned getSearchSizeForAnchor(Node e);
666
  /** Get the current search size for measure term m in this SAT context. */
667
  unsigned getSearchSizeForMeasureTerm(Node m);
668
  /** get current template
669
   *
670
   * For debugging. This returns a term that corresponds to the current
671
   * inferred shape of n. For example, if the testers
672
   *   is-C1( n ) and is-C2( n.1 )
673
   * have been asserted where C1 and C2 are binary constructors, then this
674
   * method may return a term of the form:
675
   *   C1( C2( x1, x2 ), x3 )
676
   * for fresh variables x1, x2, x3. The map var_count maintains the variable
677
   * count for generating these fresh variables.
678
   */
679
  Node getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count );
680
  //----------------------end search size information
681
  /** check value
682
   *
683
   * This is called when we have a model assignment vn for n, where n is
684
   * a selector chain applied to an enumerator (a search term). This function
685
   * ensures that testers have been asserted for each subterm of vn. This is
686
   * critical for ensuring that the proper steps have been taken by this class
687
   * regarding whether or not vn is a legal value for n (not greater than the
688
   * current search size and not a value that can be blocked by symmetry
689
   * breaking).
690
   *
691
   * For example, if vn = +( x(), x() ), then we ensure that the testers
692
   *   is-+( n ), is-x( n.1 ), is-x( n.2 )
693
   * have been asserted to this class. If a tester is not asserted for some
694
   * relevant selector chain S( n ) of n, then we add a lemma L for that
695
   * selector chain to lemmas, where L is the "splitting lemma" for S( n ), that
696
   * states that the top symbol of S( n ) must be one of the constructors of
697
   * its type.
698
   *
699
   * Notice that this function is a sanity check. Typically, it should be the
700
   * case that testers are asserted for all subterms of vn, and hence this
701
   * method should not ever add anything to lemmas. However, due to its
702
   * importance, we check this regardless.
703
   */
704
  bool checkValue(Node n, TNode vn, int ind);
705
  /**
706
   * Get the current SAT status of the guard g.
707
   * In particular, this returns 1 if g is asserted true, -1 if it is asserted
708
   * false, and 0 if it is not asserted.
709
   */
710
  int getGuardStatus( Node g );
711
};
712
713
}
714
}
715
}
716
717
#endif
718