GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/sygus_extension.cpp Lines: 854 1004 85.1 %
Date: 2021-03-22 Branches: 1992 4958 40.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_extension.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Mathias Preiner, Morgan Deters
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 Implementation of the sygus extension of the theory of datatypes.
13
 **/
14
15
#include "theory/datatypes/sygus_extension.h"
16
17
#include "expr/dtype.h"
18
#include "expr/dtype_cons.h"
19
#include "expr/node_manager.h"
20
#include "expr/sygus_datatype.h"
21
#include "options/base_options.h"
22
#include "options/datatypes_options.h"
23
#include "options/quantifiers_options.h"
24
#include "printer/printer.h"
25
#include "smt/logic_exception.h"
26
#include "theory/datatypes/inference_manager.h"
27
#include "theory/datatypes/sygus_datatype_utils.h"
28
#include "theory/datatypes/theory_datatypes_utils.h"
29
#include "theory/quantifiers/sygus/sygus_explain.h"
30
#include "theory/quantifiers/sygus/synth_conjecture.h"
31
#include "theory/quantifiers/sygus/term_database_sygus.h"
32
#include "theory/quantifiers/term_util.h"
33
#include "theory/rewriter.h"
34
#include "theory/theory_model.h"
35
36
using namespace CVC4;
37
using namespace CVC4::kind;
38
using namespace CVC4::context;
39
using namespace CVC4::theory;
40
using namespace CVC4::theory::datatypes;
41
42
2190
SygusExtension::SygusExtension(TheoryState& s,
43
                               InferenceManager& im,
44
                               quantifiers::TermDbSygus* tds,
45
2190
                               DecisionManager* dm)
46
    : d_state(s),
47
      d_im(im),
48
      d_tds(tds),
49
      d_dm(dm),
50
      d_ssb(tds),
51
      d_testers(s.getSatContext()),
52
      d_testers_exp(s.getSatContext()),
53
      d_active_terms(s.getSatContext()),
54
2190
      d_currTermSize(s.getSatContext())
55
{
56
2190
  d_zero = NodeManager::currentNM()->mkConst(Rational(0));
57
2190
  d_true = NodeManager::currentNM()->mkConst(true);
58
2190
}
59
60
2188
SygusExtension::~SygusExtension() {
61
62
2188
}
63
64
/** add tester */
65
342598
void SygusExtension::assertTester(int tindex, TNode n, Node exp)
66
{
67
342598
  registerTerm(n);
68
  // check if this is a relevant (sygus) term
69
342598
  if( d_term_to_anchor.find( n )!=d_term_to_anchor.end() ){
70
303295
    Trace("sygus-sb-debug2") << "Sygus : process tester : " << exp << std::endl;
71
    // if not already active (may have duplicate calls for the same tester)
72
303295
    if( d_active_terms.find( n )==d_active_terms.end() ) {
73
251194
      d_testers[n] = tindex;
74
251194
      d_testers_exp[n] = exp;
75
76
      // check if parent is active
77
251194
      bool do_add = true;
78
727038
      if( options::sygusSymBreakLazy() ){
79
251186
        if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
80
220035
          NodeSet::const_iterator it = d_active_terms.find( n[0] );
81
220035
          if( it==d_active_terms.end() ){
82
87774
            do_add = false;
83
          }else{
84
            //this must be a proper selector
85
132261
            IntMap::const_iterator itt = d_testers.find( n[0] );
86
132261
            Assert(itt != d_testers.end());
87
132261
            int ptindex = (*itt).second;
88
264522
            TypeNode ptn = n[0].getType();
89
132261
            const DType& pdt = ptn.getDType();
90
            int sindex_in_parent =
91
132261
                pdt[ptindex].getSelectorIndexInternal(n.getOperator());
92
            // the tester is irrelevant in this branch
93
132261
            if( sindex_in_parent==-1 ){
94
62315
              do_add = false;
95
            }
96
          }
97
        }
98
      }
99
251194
      if( do_add ){
100
101105
        assertTesterInternal(tindex, n, exp);
101
      }else{
102
150089
        Trace("sygus-sb-debug2") << "...ignore inactive tester : " << exp << std::endl;
103
      }
104
    }else{
105
52101
      Trace("sygus-sb-debug2") << "...ignore repeated tester : " << exp << std::endl;
106
    }
107
  }else{
108
39303
    Trace("sygus-sb-debug2") << "...ignore non-sygus tester : " << exp << std::endl;
109
  }
110
342598
}
111
112
2632655
void SygusExtension::assertFact(Node n, bool polarity)
113
{
114
2632655
  if (n.getKind() == kind::DT_SYGUS_BOUND)
115
  {
116
28700
    Node m = n[0];
117
14350
    Trace("sygus-fair") << "Have sygus bound : " << n << ", polarity=" << polarity << " on measure " << m << std::endl;
118
14350
    registerMeasureTerm( m );
119
160492
    if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
120
    {
121
      std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
122
14344
          d_szinfo.find(m);
123
14344
      Assert(its != d_szinfo.end());
124
28688
      Node mt = its->second->getOrMkMeasureValue();
125
      //it relates the measure term to arithmetic
126
28688
      Node blem = n.eqNode( NodeManager::currentNM()->mkNode( kind::LEQ, mt, n[1] ) );
127
14344
      d_im.lemma(blem, InferenceId::DATATYPES_SYGUS_FAIR_SIZE);
128
    }
129
14350
    if( polarity ){
130
10546
      uint64_t s = n[1].getConst<Rational>().getNumerator().toUnsignedInt();
131
10546
      notifySearchSize(m, s, n);
132
    }
133
2618305
  }else if( n.getKind() == kind::DT_HEIGHT_BOUND || n.getKind()==DT_SIZE_BOUND ){
134
    //reduce to arithmetic TODO ?
135
136
  }
137
2632655
}
138
139
377
Node SygusExtension::getTermOrderPredicate( Node n1, Node n2 ) {
140
377
  NodeManager* nm = NodeManager::currentNM();
141
754
  std::vector< Node > comm_disj;
142
  // size of left is greater than or equal to the size of right
143
  Node szGeq =
144
377
      nm->mkNode(GEQ, nm->mkNode(DT_SIZE, n1), nm->mkNode(DT_SIZE, n2));
145
754
  return szGeq;
146
}
147
148
344445
void SygusExtension::registerTerm(Node n)
149
{
150
344445
  if( d_is_top_level.find( n )==d_is_top_level.end() ){
151
2660
    d_is_top_level[n] = false;
152
5320
    TypeNode tn = n.getType();
153
2660
    unsigned d = 0;
154
2660
    bool is_top_level = false;
155
2660
    bool success = false;
156
2660
    if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
157
1847
      registerTerm(n[0]);
158
      std::unordered_map<Node, Node, NodeHashFunction>::iterator it =
159
1847
          d_term_to_anchor.find(n[0]);
160
1847
      if( it!=d_term_to_anchor.end() ) {
161
1775
        d_term_to_anchor[n] = it->second;
162
        unsigned sel_weight =
163
1775
            d_tds->getSelectorWeight(n[0].getType(), n.getOperator());
164
1775
        d = d_term_to_depth[n[0]] + sel_weight;
165
1775
        is_top_level = computeTopLevel( tn, n[0] );
166
1775
        success = true;
167
      }
168
813
    }else if( n.isVar() ){
169
766
      registerSizeTerm(n);
170
766
      if( d_register_st[n] ){
171
629
        d_term_to_anchor[n] = n;
172
629
        d_anchor_to_conj[n] = d_tds->getConjectureForEnumerator(n);
173
        // this assertion fails if we have a sygus term in the search that is unmeasured
174
629
        d = 0;
175
629
        is_top_level = true;
176
629
        success = true;
177
      }
178
    }
179
2660
    if( success ){
180
4808
      Trace("sygus-sb-debug")
181
2404
          << "Register : " << n << ", depth : " << d
182
2404
          << ", top level = " << is_top_level
183
2404
          << ", type = " << tn.getDType().getName() << std::endl;
184
2404
      d_term_to_depth[n] = d;
185
2404
      d_is_top_level[n] = is_top_level;
186
2404
      registerSearchTerm(tn, d, n, is_top_level);
187
    }else{
188
256
      Trace("sygus-sb-debug2") << "Term " << n << " is not part of sygus search." << std::endl;
189
    }
190
  }
191
344445
}
192
193
2420
bool SygusExtension::computeTopLevel( TypeNode tn, Node n ){
194
2420
  if( n.getType()==tn ){
195
1091
    return false;
196
1329
  }else if( n.getKind()==kind::APPLY_SELECTOR_TOTAL ){
197
645
    return computeTopLevel( tn, n[0] );
198
  }else{
199
684
    return true;
200
  }
201
}
202
203
109313
void SygusExtension::assertTesterInternal(int tindex, TNode n, Node exp)
204
{
205
218626
  TypeNode ntn = n.getType();
206
109313
  if (!ntn.isDatatype())
207
  {
208
    // nothing to do for non-datatype types
209
    return;
210
  }
211
109313
  const DType& dt = ntn.getDType();
212
109313
  if (!dt.isSygus())
213
  {
214
    // nothing to do for non-sygus-datatype type
215
    return;
216
  }
217
109313
  d_active_terms.insert(n);
218
218626
  Trace("sygus-sb-debug2") << "Sygus : activate term : " << n << " : " << exp
219
109313
                           << std::endl;
220
221
  // get the search size for this
222
109313
  Assert(d_term_to_anchor.find(n) != d_term_to_anchor.end());
223
218626
  Node a = d_term_to_anchor[n];
224
109313
  Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end());
225
218626
  Node m = d_anchor_to_measure_term[a];
226
  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz =
227
109313
      d_szinfo.find(m);
228
109313
  Assert(itsz != d_szinfo.end());
229
109313
  unsigned ssz = itsz->second->d_curr_search_size;
230
231
109313
  if (options::sygusFair() == options::SygusFairMode::DIRECT)
232
  {
233
6
    if( dt[tindex].getNumArgs()>0 ){
234
      quantifiers::SygusTypeInfo& nti = d_tds->getTypeInfo(ntn);
235
      // consider lower bounds for size of types
236
      unsigned lb_add = nti.getMinConsTermSize(tindex);
237
      unsigned lb_rem = n == a ? 0 : nti.getMinTermSize();
238
      Assert(lb_add >= lb_rem);
239
      d_currTermSize[a].set( d_currTermSize[a].get() + ( lb_add - lb_rem ) );
240
    }
241
6
    if( (unsigned)d_currTermSize[a].get()>ssz ){
242
      if( Trace.isOn("sygus-sb-fair") ){
243
        std::map< TypeNode, int > var_count;
244
        Node templ = getCurrentTemplate( a, var_count );
245
        Trace("sygus-sb-fair") << "FAIRNESS : we have " <<  d_currTermSize[a].get() << " at search size " << ssz << ", template is " << templ << std::endl;
246
      }
247
      // conflict
248
      std::vector< Node > conflict;
249
      for( NodeSet::const_iterator its = d_active_terms.begin(); its != d_active_terms.end(); ++its ){
250
        Node x = *its;
251
        Node xa = d_term_to_anchor[x];
252
        if( xa==a ){
253
          IntMap::const_iterator ittv = d_testers.find( x );
254
          Assert(ittv != d_testers.end());
255
          int tidx = (*ittv).second;
256
          const DType& dti = x.getType().getDType();
257
          if (dti[tidx].getNumArgs() > 0)
258
          {
259
            NodeMap::const_iterator itt = d_testers_exp.find( x );
260
            Assert(itt != d_testers_exp.end());
261
            conflict.push_back( (*itt).second );
262
          }
263
        }
264
      }
265
      Assert(conflict.size() == (unsigned)d_currTermSize[a].get());
266
      Assert(itsz->second->d_search_size_exp.find(ssz)
267
             != itsz->second->d_search_size_exp.end());
268
      conflict.push_back( itsz->second->d_search_size_exp[ssz] );
269
      Node conf = NodeManager::currentNM()->mkNode( kind::AND, conflict );
270
      Trace("sygus-sb-fair") << "Conflict is : " << conf << std::endl;
271
      Node confn = conf.negate();
272
      d_im.lemma(confn, InferenceId::DATATYPES_SYGUS_FAIR_SIZE_CONFLICT);
273
      return;
274
    }
275
  }
276
277
  // now, add all applicable symmetry breaking lemmas for this term
278
109313
  Assert(d_term_to_depth.find(n) != d_term_to_depth.end());
279
109313
  unsigned d = d_term_to_depth[n];
280
109313
  Trace("sygus-sb-fair-debug") << "Tester " << exp << " is for depth " << d << " term in search size " << ssz << std::endl;
281
  //Assert( d<=ssz );
282
109313
  if( options::sygusSymBreakLazy() ){
283
    // dynamic symmetry breaking
284
109305
    addSymBreakLemmasFor(ntn, n, d);
285
  }
286
287
109313
  Trace("sygus-sb-debug") << "Get simple symmetry breaking predicates...\n";
288
109313
  unsigned max_depth = ssz>=d ? ssz-d : 0;
289
109313
  unsigned min_depth = d_simple_proc[exp];
290
109313
  NodeManager* nm = NodeManager::currentNM();
291
109313
  if( min_depth<=max_depth ){
292
19036
    TNode x = getFreeVar( ntn );
293
19036
    std::vector<std::pair<Node, InferenceId>> sbLemmas;
294
    // symmetry breaking lemmas requiring predicate elimination
295
19036
    std::map<Node, bool> sb_elim_pred;
296
9518
    bool usingSymCons = d_tds->usingSymbolicConsForEnumerator(m);
297
9518
    bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(m);
298
24955
    for (unsigned ds = 0; ds <= max_depth; ds++)
299
    {
300
      // static conjecture-independent symmetry breaking
301
15437
      Trace("sygus-sb-debug") << "  simple symmetry breaking...\n";
302
      Node ipred = getSimpleSymBreakPred(
303
30874
          m, ntn, tindex, ds, usingSymCons, isVarAgnostic);
304
15437
      if (!ipred.isNull())
305
      {
306
11224
        sbLemmas.emplace_back(ipred,
307
22448
                              InferenceId::DATATYPES_SYGUS_SIMPLE_SYM_BREAK);
308
11224
        if (ds == 0 && isVarAgnostic)
309
        {
310
6
          sb_elim_pred[ipred] = true;
311
        }
312
      }
313
      // static conjecture-dependent symmetry breaking
314
30874
      Trace("sygus-sb-debug")
315
15437
          << "  conjecture-dependent symmetry breaking...\n";
316
      std::map<Node, quantifiers::SynthConjecture*>::iterator itc =
317
15437
          d_anchor_to_conj.find(a);
318
15437
      if (itc != d_anchor_to_conj.end())
319
      {
320
15437
        quantifiers::SynthConjecture* conj = itc->second;
321
15437
        if (conj)
322
        {
323
          Node dpred =
324
30280
              conj->getSymmetryBreakingPredicate(x, a, ntn, tindex, ds);
325
15140
          if (!dpred.isNull())
326
          {
327
            sbLemmas.emplace_back(dpred,
328
                                  InferenceId::DATATYPES_SYGUS_CDEP_SYM_BREAK);
329
          }
330
        }
331
      }
332
    }
333
334
    // add the above symmetry breaking predicates to lemmas
335
19036
    std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
336
19036
    Node rlv = getRelevancyCondition(n);
337
20742
    for (std::pair<Node, InferenceId>& sbl : sbLemmas)
338
    {
339
22448
      Node slem = sbl.first;
340
22448
      Node sslem = slem.substitute(x, n, cache);
341
      // if we require predicate elimination
342
11224
      if (sb_elim_pred.find(slem) != sb_elim_pred.end())
343
      {
344
12
        Trace("sygus-sb-tp") << "Eliminate traversal predicates: start "
345
6
                             << sslem << std::endl;
346
6
        sslem = eliminateTraversalPredicates(sslem);
347
12
        Trace("sygus-sb-tp") << "Eliminate traversal predicates: finish "
348
6
                             << sslem << std::endl;
349
      }
350
11224
      if (!rlv.isNull())
351
      {
352
6651
        sslem = nm->mkNode(OR, rlv, sslem);
353
      }
354
11224
      d_im.lemma(sslem, sbl.second);
355
    }
356
  }
357
109313
  d_simple_proc[exp] = max_depth + 1;
358
359
  // now activate the children those testers were previously asserted in this
360
  // context and are awaiting activation, if they exist.
361
109313
  if( options::sygusSymBreakLazy() ){
362
109305
    Trace("sygus-sb-debug") << "Do lazy symmetry breaking...\n";
363
190943
    for( unsigned j=0; j<dt[tindex].getNumArgs(); j++ ){
364
      Node sel = nm->mkNode(
365
163276
          APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(ntn, j), n);
366
81638
      Trace("sygus-sb-debug2") << "  activate child sel : " << sel << std::endl;
367
81638
      Assert(d_active_terms.find(sel) == d_active_terms.end());
368
81638
      IntMap::const_iterator itt = d_testers.find( sel );
369
81638
      if( itt != d_testers.end() ){
370
8208
        Assert(d_testers_exp.find(sel) != d_testers_exp.end());
371
8208
        assertTesterInternal((*itt).second, sel, d_testers_exp[sel]);
372
      }
373
    }
374
109305
    Trace("sygus-sb-debug") << "...finished" << std::endl;
375
  }
376
}
377
378
123130
Node SygusExtension::getRelevancyCondition( Node n ) {
379
246264
  if (!options::sygusSymBreakRlv())
380
  {
381
6
    return Node::null();
382
  }
383
123124
  std::map< Node, Node >::iterator itr = d_rlv_cond.find( n );
384
123124
  if( itr==d_rlv_cond.end() ){
385
4040
    Node cond;
386
2020
    if (n.getKind() == APPLY_SELECTOR_TOTAL)
387
    {
388
2786
      TypeNode ntn = n[0].getType();
389
1393
      const DType& dt = ntn.getDType();
390
2786
      Node sel = n.getOperator();
391
945249
      if( options::dtSharedSelectors() ){
392
2786
        std::vector< Node > disj;
393
1393
        bool excl = false;
394
8606
        for( unsigned i=0; i<dt.getNumConstructors(); i++ ){
395
7213
          int sindexi = dt[i].getSelectorIndexInternal(sel);
396
7213
          if (sindexi != -1)
397
          {
398
2885
            disj.push_back(utils::mkTester(n[0], i, dt).negate());
399
          }
400
          else
401
          {
402
4328
            excl = true;
403
          }
404
        }
405
1393
        Assert(!disj.empty());
406
1393
        if( excl ){
407
1125
          cond = disj.size() == 1 ? disj[0] : NodeManager::currentNM()->mkNode(
408
                                                  kind::AND, disj);
409
        }
410
      }else{
411
        int sindex = utils::cindexOf(sel);
412
        Assert(sindex != -1);
413
        cond = utils::mkTester(n[0], sindex, dt).negate();
414
      }
415
2786
      Node c1 = getRelevancyCondition( n[0] );
416
1393
      if( cond.isNull() ){
417
268
        cond = c1;
418
1125
      }else if( !c1.isNull() ){
419
622
        cond = NodeManager::currentNM()->mkNode(kind::OR, cond, c1);
420
      }
421
    }
422
2020
    Trace("sygus-sb-debug2") << "Relevancy condition for " << n << " is " << cond << std::endl;
423
2020
    d_rlv_cond[n] = cond;
424
2020
    return cond;
425
  }else{
426
121104
    return itr->second;
427
  }
428
}
429
430
46
Node SygusExtension::getTraversalPredicate(TypeNode tn, Node n, bool isPre)
431
{
432
46
  unsigned index = isPre ? 0 : 1;
433
46
  std::map<Node, Node>::iterator itt = d_traversal_pred[index][tn].find(n);
434
46
  if (itt != d_traversal_pred[index][tn].end())
435
  {
436
38
    return itt->second;
437
  }
438
8
  NodeManager* nm = NodeManager::currentNM();
439
16
  std::vector<TypeNode> types;
440
8
  types.push_back(tn);
441
16
  TypeNode ptn = nm->mkPredicateType(types);
442
16
  Node pred = nm->mkSkolem(isPre ? "pre" : "post", ptn);
443
8
  d_traversal_pred[index][tn][n] = pred;
444
8
  return pred;
445
}
446
447
8
Node SygusExtension::eliminateTraversalPredicates(Node n)
448
{
449
8
  NodeManager* nm = NodeManager::currentNM();
450
16
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
451
8
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
452
8
  std::map<Node, Node>::iterator ittb;
453
16
  std::vector<TNode> visit;
454
16
  TNode cur;
455
8
  visit.push_back(n);
456
220
  do
457
  {
458
228
    cur = visit.back();
459
228
    visit.pop_back();
460
228
    it = visited.find(cur);
461
462
228
    if (it == visited.end())
463
    {
464
128
      if (cur.getKind() == APPLY_UF)
465
      {
466
40
        Assert(cur.getType().isBoolean());
467
40
        Assert(cur.getNumChildren() == 1
468
               && (cur[0].isVar() || cur[0].getKind() == APPLY_SELECTOR_TOTAL));
469
40
        ittb = d_traversal_bool.find(cur);
470
80
        Node ret;
471
40
        if (ittb == d_traversal_bool.end())
472
        {
473
48
          std::stringstream ss;
474
24
          ss << "v_" << cur;
475
24
          ret = nm->mkSkolem(ss.str(), cur.getType());
476
24
          d_traversal_bool[cur] = ret;
477
        }
478
        else
479
        {
480
16
          ret = ittb->second;
481
        }
482
40
        visited[cur] = ret;
483
      }
484
      else
485
      {
486
88
        visited[cur] = Node::null();
487
88
        visit.push_back(cur);
488
220
        for (const Node& cn : cur)
489
        {
490
132
          visit.push_back(cn);
491
        }
492
      }
493
    }
494
100
    else if (it->second.isNull())
495
    {
496
176
      Node ret = cur;
497
88
      bool childChanged = false;
498
176
      std::vector<Node> children;
499
88
      if (cur.getMetaKind() == metakind::PARAMETERIZED)
500
      {
501
10
        children.push_back(cur.getOperator());
502
      }
503
220
      for (const Node& cn : cur)
504
      {
505
132
        it = visited.find(cn);
506
132
        Assert(it != visited.end());
507
132
        Assert(!it->second.isNull());
508
132
        childChanged = childChanged || cn != it->second;
509
132
        children.push_back(it->second);
510
      }
511
88
      if (childChanged)
512
      {
513
38
        ret = nm->mkNode(cur.getKind(), children);
514
      }
515
88
      visited[cur] = ret;
516
    }
517
228
  } while (!visit.empty());
518
8
  Assert(visited.find(n) != visited.end());
519
8
  Assert(!visited.find(n)->second.isNull());
520
16
  return visited[n];
521
}
522
523
15437
Node SygusExtension::getSimpleSymBreakPred(Node e,
524
                                             TypeNode tn,
525
                                             int tindex,
526
                                             unsigned depth,
527
                                             bool usingSymCons,
528
                                             bool isVarAgnostic)
529
{
530
  // Compute the tuple of expressions we hash the predicate for.
531
532
  // The hash value in d_simple_sb_pred for the given options
533
15437
  unsigned optHashVal = usingSymCons ? 1 : 0;
534
15437
  if (isVarAgnostic && depth == 0)
535
  {
536
    // variable agnostic symmetry breaking only applies at depth 0
537
6
    optHashVal = optHashVal + 2;
538
  }
539
  else
540
  {
541
    // enumerator is only specific to variable agnostic symmetry breaking
542
15431
    e = Node::null();
543
  }
544
  std::map<unsigned, Node>& ssbCache =
545
15437
      d_simple_sb_pred[e][tn][tindex][optHashVal];
546
15437
  std::map<unsigned, Node>::iterator it = ssbCache.find(depth);
547
15437
  if (it != ssbCache.end())
548
  {
549
10643
    return it->second;
550
  }
551
  // this function is only called on sygus datatype types
552
4794
  Assert(tn.isDatatype());
553
4794
  NodeManager* nm = NodeManager::currentNM();
554
9588
  Node n = getFreeVar(tn);
555
4794
  const DType& dt = tn.getDType();
556
4794
  Assert(dt.isSygus());
557
4794
  Assert(tindex >= 0 && tindex < static_cast<int>(dt.getNumConstructors()));
558
559
9588
  Trace("sygus-sb-simple-debug")
560
9588
      << "Simple symmetry breaking for " << dt.getName() << ", constructor "
561
4794
      << dt[tindex].getName() << ", at depth " << depth << std::endl;
562
563
4794
  quantifiers::SygusTypeInfo& ti = d_tds->getTypeInfo(tn);
564
  // get the sygus operator
565
9588
  Node sop = dt[tindex].getSygusOp();
566
  // get the kind of the constructor operator
567
4794
  Kind nk = ti.getConsNumKind(tindex);
568
  // is this the any-constant constructor?
569
4794
  bool isAnyConstant = sop.getAttribute(SygusAnyConstAttribute());
570
571
  // conjunctive conclusion of lemma
572
9588
  std::vector<Node> sbp_conj;
573
574
  // the number of (sygus) arguments
575
  // Notice if this is an any-constant constructor, its child is not a
576
  // sygus child, hence we set to 0 here.
577
4794
  unsigned dt_index_nargs = isAnyConstant ? 0 : dt[tindex].getNumArgs();
578
579
  // builtin type
580
9588
  TypeNode tnb = dt.getSygusType();
581
  // get children
582
9588
  std::vector<Node> children;
583
9699
  for (unsigned j = 0; j < dt_index_nargs; j++)
584
  {
585
    Node sel = nm->mkNode(
586
9810
        APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, j), n);
587
4905
    Assert(sel.getType().isDatatype());
588
4905
    children.push_back(sel);
589
  }
590
591
4794
  if (depth == 0)
592
  {
593
2769
    Trace("sygus-sb-simple-debug") << "  Size..." << std::endl;
594
    // fairness
595
5538
    if (options::sygusFair() == options::SygusFairMode::DT_SIZE
596
2769
        && !isAnyConstant)
597
    {
598
5448
      Node szl = nm->mkNode(DT_SIZE, n);
599
5448
      Node szr = nm->mkNode(DT_SIZE, utils::getInstCons(n, dt, tindex));
600
2724
      szr = Rewriter::rewrite(szr);
601
2724
      sbp_conj.push_back(szl.eqNode(szr));
602
    }
603
2769
    if (isVarAgnostic)
604
    {
605
      // Enforce symmetry breaking lemma template for each x_i:
606
      // template z.
607
      //   is-x_i( z ) => pre_{x_{i-1}}( z )
608
      //   for args a = 1...n
609
      //      // pre-definition
610
      //      pre_{x_i}( z.a ) = a=0 ? pre_{x_i}( z ) : post_{x_i}( z.{a-1} )
611
      //   post_{x_i}( z ) = post_{x_i}( z.n ) OR is-x_i( z )
612
613
      // Notice that we are constructing a symmetry breaking template
614
      // under the condition that is-C( z ) holds in this method, where C
615
      // is the tindex^{th} constructor of dt. Thus, is-x_i( z ) is either
616
      // true or false below.
617
618
12
      Node svl = dt.getSygusVarList();
619
      // for each variable
620
6
      Assert(!e.isNull());
621
12
      TypeNode etn = e.getType();
622
      // for each variable in the sygus type
623
18
      for (const Node& var : svl)
624
      {
625
12
        quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn);
626
12
        unsigned sc = eti.getSubclassForVar(var);
627
12
        if (eti.getNumSubclassVars(sc) == 1)
628
        {
629
          // unique variable in singleton subclass, skip
630
          continue;
631
        }
632
        // Compute the "predecessor" variable in the subclass of var.
633
24
        Node predVar;
634
12
        unsigned scindex = 0;
635
12
        if (eti.getIndexInSubclassForVar(var, scindex))
636
        {
637
12
          if (scindex > 0)
638
          {
639
6
            predVar = eti.getVarSubclassIndex(sc, scindex - 1);
640
          }
641
        }
642
24
        Node preParentOp = getTraversalPredicate(tn, var, true);
643
24
        Node preParent = nm->mkNode(APPLY_UF, preParentOp, n);
644
24
        Node prev = preParent;
645
        // for each child
646
20
        for (const Node& child : children)
647
        {
648
16
          TypeNode ctn = child.getType();
649
          // my pre is equal to the previous
650
16
          Node preCurrOp = getTraversalPredicate(ctn, var, true);
651
16
          Node preCurr = nm->mkNode(APPLY_UF, preCurrOp, child);
652
          // definition of pre, for each argument
653
8
          sbp_conj.push_back(preCurr.eqNode(prev));
654
16
          Node postCurrOp = getTraversalPredicate(ctn, var, false);
655
8
          prev = nm->mkNode(APPLY_UF, postCurrOp, child);
656
        }
657
24
        Node postParent = getTraversalPredicate(tn, var, false);
658
24
        Node finish = nm->mkNode(APPLY_UF, postParent, n);
659
        // check if we are constructing the symmetry breaking predicate for the
660
        // variable in question. If so, is-{x_i}( z ) is true.
661
12
        int varCn = ti.getOpConsNum(var);
662
12
        if (varCn == static_cast<int>(tindex))
663
        {
664
          // the post value is true
665
4
          prev = d_true;
666
          // requirement : If I am the variable, I must have seen
667
          // the variable before this one in its type class.
668
4
          if (!predVar.isNull())
669
          {
670
4
            Node preParentPredVarOp = getTraversalPredicate(tn, predVar, true);
671
4
            Node preParentPredVar = nm->mkNode(APPLY_UF, preParentPredVarOp, n);
672
2
            sbp_conj.push_back(preParentPredVar);
673
          }
674
        }
675
        // definition of post
676
12
        sbp_conj.push_back(finish.eqNode(prev));
677
      }
678
    }
679
  }
680
681
  // if we are the "any constant" constructor, we do no symmetry breaking
682
  // only do simple symmetry breaking up to depth 2
683
9604
  bool doSymBreak = options::sygusSymBreak();
684
4794
  if (isAnyConstant || depth > 2)
685
  {
686
469
    doSymBreak = false;
687
  }
688
  // symmetry breaking
689
4794
  if (doSymBreak)
690
  {
691
    // direct solving for children
692
    //   for instance, we may want to insist that the LHS of MINUS is 0
693
4288
    Trace("sygus-sb-simple-debug") << "  Solve children..." << std::endl;
694
8576
    std::map<unsigned, unsigned> children_solved;
695
8639
    for (unsigned j = 0; j < dt_index_nargs; j++)
696
    {
697
4351
      int i = d_ssb.solveForArgument(tn, tindex, j);
698
4351
      if (i >= 0)
699
      {
700
        children_solved[j] = i;
701
        TypeNode ctn = children[j].getType();
702
        const DType& cdt = ctn.getDType();
703
        Assert(i < static_cast<int>(cdt.getNumConstructors()));
704
        sbp_conj.push_back(utils::mkTester(children[j], i, cdt));
705
      }
706
    }
707
708
    // depth 1 symmetry breaking : talks about direct children
709
4288
    if (depth == 1)
710
    {
711
1160
      if (nk != UNDEFINED_KIND)
712
      {
713
1248
        Trace("sygus-sb-simple-debug")
714
624
            << "  Equality reasoning about children..." << std::endl;
715
        // commutative operators
716
624
        if (quantifiers::TermUtil::isComm(nk))
717
        {
718
610
          if (children.size() == 2
719
610
              && children[0].getType() == children[1].getType())
720
          {
721
594
            Node order_pred = getTermOrderPredicate(children[0], children[1]);
722
297
            sbp_conj.push_back(order_pred);
723
          }
724
        }
725
        // operators whose arguments are non-additive (e.g. should be different)
726
1248
        std::vector<unsigned> deq_child[2];
727
624
        if (children.size() == 2 && children[0].getType() == tn)
728
        {
729
290
          bool argDeq = false;
730
290
          if (quantifiers::TermUtil::isNonAdditive(nk))
731
          {
732
84
            argDeq = true;
733
          }
734
          else
735
          {
736
            // other cases of rewriting x k x -> x'
737
412
            Node req_const;
738
206
            if (nk == GT || nk == LT || nk == XOR || nk == MINUS
739
148
                || nk == BITVECTOR_SUB || nk == BITVECTOR_XOR
740
142
                || nk == BITVECTOR_UREM)
741
            {
742
              // must have the zero element
743
66
              req_const = quantifiers::TermUtil::mkTypeValue(tnb, 0);
744
            }
745
140
            else if (nk == EQUAL || nk == LEQ || nk == GEQ
746
140
                     || nk == BITVECTOR_XNOR)
747
            {
748
              req_const = quantifiers::TermUtil::mkTypeMaxValue(tnb);
749
            }
750
            // cannot do division since we have to consider when both are zero
751
206
            if (!req_const.isNull())
752
            {
753
66
              if (ti.hasConst(req_const))
754
              {
755
54
                argDeq = true;
756
              }
757
            }
758
          }
759
290
          if (argDeq)
760
          {
761
138
            deq_child[0].push_back(0);
762
138
            deq_child[1].push_back(1);
763
          }
764
        }
765
624
        if (nk == ITE || nk == STRING_STRREPL || nk == STRING_STRREPLALL)
766
        {
767
70
          deq_child[0].push_back(1);
768
70
          deq_child[1].push_back(2);
769
        }
770
624
        if (nk == STRING_STRREPL || nk == STRING_STRREPLALL)
771
        {
772
          deq_child[0].push_back(0);
773
          deq_child[1].push_back(1);
774
        }
775
        // this code adds simple symmetry breaking predicates of the form
776
        // d.i != d.j, for example if we are considering an ITE constructor,
777
        // we enforce that d.1 != d.2 since otherwise the ITE can be
778
        // simplified.
779
832
        for (unsigned i = 0, size = deq_child[0].size(); i < size; i++)
780
        {
781
208
          unsigned c1 = deq_child[0][i];
782
208
          unsigned c2 = deq_child[1][i];
783
416
          TypeNode tnc = children[c1].getType();
784
          // we may only apply this symmetry breaking scheme (which introduces
785
          // disequalities) if the types are infinite.
786
208
          if (tnc == children[c2].getType() && !tnc.isInterpretedFinite())
787
          {
788
416
            Node sym_lem_deq = children[c1].eqNode(children[c2]).negate();
789
            // notice that this symmetry breaking still allows for
790
            //   ite( C, any_constant(x), any_constant(y) )
791
            // since any_constant takes a builtin argument.
792
208
            sbp_conj.push_back(sym_lem_deq);
793
          }
794
        }
795
796
1248
        Trace("sygus-sb-simple-debug") << "  Redundant operators..."
797
624
                                       << std::endl;
798
        // singular arguments (e.g. 0 for mult)
799
        // redundant arguments (e.g. 0 for plus, 1 for mult)
800
        // right-associativity
801
        // simple rewrites
802
        // explanation of why not all children of this are constant
803
1248
        std::vector<Node> exp_not_all_const;
804
        // is the above explanation valid? This is set to false if
805
        // one child does not have a constant, hence making the explanation
806
        // false.
807
624
        bool exp_not_all_const_valid = dt_index_nargs > 0;
808
        // does the parent have an any constant constructor?
809
        bool usingAnyConstCons =
810
624
            usingSymCons && (ti.getAnyConstantConsNum() != -1);
811
1883
        for (unsigned j = 0; j < dt_index_nargs; j++)
812
        {
813
2518
          Node nc = children[j];
814
          // if not already solved
815
1259
          if (children_solved.find(j) != children_solved.end())
816
          {
817
            continue;
818
          }
819
2518
          TypeNode tnc = nc.getType();
820
1259
          quantifiers::SygusTypeInfo& cti = d_tds->getTypeInfo(tnc);
821
1259
          int anyc_cons_num = cti.getAnyConstantConsNum();
822
1259
          const DType& cdt = tnc.getDType();
823
2518
          std::vector<Node> exp_const;
824
9863
          for (unsigned k = 0, ncons = cdt.getNumConstructors(); k < ncons; k++)
825
          {
826
8604
            Kind nck = cti.getConsNumKind(k);
827
8604
            bool red = false;
828
17208
            Node tester = utils::mkTester(nc, k, cdt);
829
            // check if the argument is redundant
830
8604
            if (static_cast<int>(k) == anyc_cons_num)
831
            {
832
84
              exp_const.push_back(tester);
833
            }
834
8520
            else if (nck != UNDEFINED_KIND)
835
            {
836
9952
              Trace("sygus-sb-simple-debug") << "  argument " << j << " " << k
837
4976
                                             << " is : " << nck << std::endl;
838
4976
              red = !d_ssb.considerArgKind(tnc, tn, nck, nk, j);
839
            }
840
            else
841
            {
842
7088
              Node cc = cti.getConsNumConst(k);
843
3544
              if (!cc.isNull())
844
              {
845
3832
                Trace("sygus-sb-simple-debug")
846
1916
                    << "  argument " << j << " " << k << " is constant : " << cc
847
1916
                    << std::endl;
848
1916
                red = !d_ssb.considerConst(tnc, tn, cc, nk, j);
849
1916
                if (usingAnyConstCons)
850
                {
851
                  // we only consider concrete constant constructors
852
                  // of children if we have the "any constant" constructor
853
                  // otherwise, we would disallow solutions for grammars
854
                  // like the following:
855
                  //   A -> B+B
856
                  //   B -> 4 | 8 | 100
857
                  // where A allows all constants but is not using the
858
                  // any constant constructor.
859
                  exp_const.push_back(tester);
860
                }
861
              }
862
              else
863
              {
864
                // defined function?
865
              }
866
            }
867
8604
            if (red)
868
            {
869
1947
              Trace("sygus-sb-simple-debug") << "  ...redundant." << std::endl;
870
1947
              sbp_conj.push_back(tester.negate());
871
            }
872
          }
873
1259
          if (exp_const.empty())
874
          {
875
1175
            exp_not_all_const_valid = false;
876
          }
877
          else
878
          {
879
168
            Node ecn = exp_const.size() == 1 ? exp_const[0]
880
252
                                             : nm->mkNode(OR, exp_const);
881
84
            exp_not_all_const.push_back(ecn.negate());
882
          }
883
        }
884
        // explicitly handle constants and "any constant" constructors
885
        // if this type admits any constant, then at least one of my
886
        // children must not be a constant or the "any constant" constructor
887
624
        if (dt.getSygusAllowConst() && exp_not_all_const_valid)
888
        {
889
30
          Assert(!exp_not_all_const.empty());
890
30
          Node expaan = exp_not_all_const.size() == 1
891
2
                            ? exp_not_all_const[0]
892
62
                            : nm->mkNode(OR, exp_not_all_const);
893
60
          Trace("sygus-sb-simple-debug")
894
30
              << "Ensure not all constant: " << expaan << std::endl;
895
30
          sbp_conj.push_back(expaan);
896
        }
897
      }
898
      else
899
      {
900
        // defined function?
901
      }
902
    }
903
3128
    else if (depth == 2)
904
    {
905
      // commutative operators
906
1010
      if (quantifiers::TermUtil::isComm(nk) && children.size() == 2
907
1010
          && children[0].getType() == tn && children[1].getType() == tn)
908
      {
909
        // chainable
910
        Node child11 = nm->mkNode(APPLY_SELECTOR_TOTAL,
911
160
                                  dt[tindex].getSelectorInternal(tn, 1),
912
320
                                  children[0]);
913
80
        Assert(child11.getType() == children[1].getType());
914
        Node order_pred_trans =
915
            nm->mkNode(OR,
916
160
                       utils::mkTester(children[0], tindex, dt).negate(),
917
320
                       getTermOrderPredicate(child11, children[1]));
918
80
        sbp_conj.push_back(order_pred_trans);
919
      }
920
    }
921
  }
922
923
9588
  Node sb_pred;
924
4794
  if (!sbp_conj.empty())
925
  {
926
3370
    sb_pred =
927
6740
        sbp_conj.size() == 1 ? sbp_conj[0] : nm->mkNode(kind::AND, sbp_conj);
928
6740
    Trace("sygus-sb-simple")
929
3370
        << "Simple predicate for " << tn << " index " << tindex << " (" << nk
930
3370
        << ") at depth " << depth << " : " << std::endl;
931
3370
    Trace("sygus-sb-simple") << "   " << sb_pred << std::endl;
932
3370
    sb_pred = nm->mkNode(OR, utils::mkTester(n, tindex, dt).negate(), sb_pred);
933
  }
934
4794
  d_simple_sb_pred[e][tn][tindex][optHashVal][depth] = sb_pred;
935
4794
  return sb_pred;
936
}
937
938
97117
TNode SygusExtension::getFreeVar( TypeNode tn ) {
939
97117
  return d_tds->getFreeVar(tn, 0);
940
}
941
942
2404
void SygusExtension::registerSearchTerm(TypeNode tn,
943
                                        unsigned d,
944
                                        Node n,
945
                                        bool topLevel)
946
{
947
  //register this term
948
  std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
949
2404
      d_term_to_anchor.find(n);
950
2404
  Assert(ita != d_term_to_anchor.end());
951
4808
  Node a = ita->second;
952
2404
  Assert(!a.isNull());
953
2404
  SearchCache& sca = d_cache[a];
954
7212
  if (std::find(
955
2404
          sca.d_search_terms[tn][d].begin(), sca.d_search_terms[tn][d].end(), n)
956
7212
      == sca.d_search_terms[tn][d].end())
957
  {
958
2404
    Trace("sygus-sb-debug") << "  register search term : " << n << " at depth " << d << ", type=" << tn << ", tl=" << topLevel << std::endl;
959
2404
    sca.d_search_terms[tn][d].push_back(n);
960
2404
    if( !options::sygusSymBreakLazy() ){
961
2
      addSymBreakLemmasFor(tn, n, d);
962
    }
963
  }
964
2404
}
965
966
52739
Node SygusExtension::registerSearchValue(Node a,
967
                                           Node n,
968
                                           Node nv,
969
                                           unsigned d,
970
                                           bool isVarAgnostic,
971
                                           bool doSym)
972
{
973
52739
  Assert(n.getType().isComparableTo(nv.getType()));
974
105478
  TypeNode tn = n.getType();
975
52739
  if (!tn.isDatatype())
976
  {
977
    // don't register non-datatype terms, instead we return the
978
    // selector chain n.
979
763
    return n;
980
  }
981
51976
  const DType& dt = tn.getDType();
982
51976
  if (!dt.isSygus())
983
  {
984
    // don't register non-sygus-datatype terms
985
    return n;
986
  }
987
51976
  Assert(nv.getKind() == APPLY_CONSTRUCTOR);
988
51976
  NodeManager* nm = NodeManager::currentNM();
989
  // we call the body of this function in a bottom-up fashion
990
  // this ensures that the "abstraction" of the model value is available
991
51976
  if( nv.getNumChildren()>0 ){
992
17735
    unsigned cindex = utils::indexOf(nv.getOperator());
993
34987
    std::vector<Node> rcons_children;
994
17735
    rcons_children.push_back(nv.getOperator());
995
17735
    bool childrenChanged = false;
996
51686
    for (unsigned i = 0, nchild = nv.getNumChildren(); i < nchild; i++)
997
    {
998
      Node sel = nm->mkNode(
999
68385
          APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
1000
      Node nvc = registerSearchValue(a,
1001
                                     sel,
1002
                                     nv[i],
1003
                                     d + 1,
1004
                                     isVarAgnostic,
1005
68385
                                     doSym && (!isVarAgnostic || i == 0));
1006
34434
      if (nvc.isNull())
1007
      {
1008
483
        return Node::null();
1009
      }
1010
33951
      rcons_children.push_back(nvc);
1011
33951
      childrenChanged = childrenChanged || nvc != nv[i];
1012
    }
1013
    // reconstruct the value, which may be a skeleton
1014
17252
    if (childrenChanged)
1015
    {
1016
1344
      nv = nm->mkNode(APPLY_CONSTRUCTOR, rcons_children);
1017
    }
1018
  }
1019
51493
  if (!doSym)
1020
  {
1021
    return nv;
1022
  }
1023
51493
  Trace("sygus-sb-debug2") << "Registering search value " << n << " -> " << nv << std::endl;
1024
102986
  std::map<TypeNode, int> var_count;
1025
102986
  Node cnv = d_tds->canonizeBuiltin(nv, var_count);
1026
51493
  Trace("sygus-sb-debug") << "  ...canonized value is " << cnv << std::endl;
1027
51493
  SearchCache& sca = d_cache[a];
1028
  // must do this for all nodes, regardless of top-level
1029
51493
  if (sca.d_search_val_proc.find(cnv) == sca.d_search_val_proc.end())
1030
  {
1031
8316
    sca.d_search_val_proc.insert(cnv);
1032
    // get the root (for PBE symmetry breaking)
1033
8316
    Assert(d_anchor_to_conj.find(a) != d_anchor_to_conj.end());
1034
8316
    quantifiers::SynthConjecture* aconj = d_anchor_to_conj[a];
1035
16632
    Trace("sygus-sb-debug") << "  ...register search value " << cnv
1036
8316
                            << ", type=" << tn << std::endl;
1037
13991
    Node bv = d_tds->sygusToBuiltin(cnv, tn);
1038
8316
    Trace("sygus-sb-debug") << "  ......builtin is " << bv << std::endl;
1039
13991
    Node bvr = d_tds->getExtRewriter()->extendedRewrite(bv);
1040
8316
    Trace("sygus-sb-debug") << "  ......search value rewrites to " << bvr << std::endl;
1041
8316
    Trace("dt-sygus") << "  * DT builtin : " << n << " -> " << bvr << std::endl;
1042
8316
    unsigned sz = d_tds->getSygusTermSize( nv );
1043
8316
    if( d_tds->involvesDivByZero( bvr ) ){
1044
      quantifiers::DivByZeroSygusInvarianceTest dbzet;
1045
      Trace("sygus-sb-mexp-debug") << "Minimize explanation for div-by-zero in "
1046
                                   << bv << std::endl;
1047
      registerSymBreakLemmaForValue(a, nv, dbzet, Node::null(), var_count);
1048
      return Node::null();
1049
    }else{
1050
      std::unordered_map<Node, Node, NodeHashFunction>& scasv =
1051
8316
          sca.d_search_val[tn];
1052
      std::unordered_map<Node, unsigned, NodeHashFunction>& scasvs =
1053
8316
          sca.d_search_val_sz[tn];
1054
      std::unordered_map<Node, Node, NodeHashFunction>::iterator itsv =
1055
8316
          scasv.find(bvr);
1056
13991
      Node bad_val_bvr;
1057
8316
      bool by_examples = false;
1058
8316
      if (itsv == scasv.end())
1059
      {
1060
        // Is it equivalent under examples?
1061
11386
        Node bvr_equiv;
1062
13720
        if (aconj != nullptr && options::sygusSymBreakPbe())
1063
        {
1064
          // If the enumerator has examples, see if it is equivalent up to its
1065
          // examples with a previous term.
1066
5443
          quantifiers::ExampleEvalCache* eec = aconj->getExampleEvalCache(a);
1067
5443
          if (eec != nullptr)
1068
          {
1069
745
            bvr_equiv = eec->addSearchVal(tn, bvr);
1070
          }
1071
        }
1072
5693
        if( !bvr_equiv.isNull() ){
1073
745
          if( bvr_equiv!=bvr ){
1074
36
            Trace("sygus-sb-debug") << "......adding search val for " << bvr << " returned " << bvr_equiv << std::endl;
1075
36
            Assert(scasv.find(bvr_equiv) != scasv.end());
1076
72
            Trace("sygus-sb-debug")
1077
36
                << "......search value was " << scasv[bvr_equiv] << std::endl;
1078
36
            if( Trace.isOn("sygus-sb-exc") ){
1079
              Node prev = d_tds->sygusToBuiltin(scasv[bvr_equiv], tn);
1080
              Trace("sygus-sb-exc") << "  ......programs " << prev << " and " << bv << " are equivalent up to examples." << std::endl;
1081
            }
1082
36
            bad_val_bvr = bvr_equiv;
1083
36
            by_examples = true;
1084
          }
1085
        }
1086
        //store rewritten values, regardless of whether it will be considered
1087
5693
        scasv[bvr] = nv;
1088
5693
        scasvs[bvr] = sz;
1089
      }
1090
      else
1091
      {
1092
2623
        bad_val_bvr = bvr;
1093
2623
        if( Trace.isOn("sygus-sb-exc") ){
1094
          Node prev_bv = d_tds->sygusToBuiltin( itsv->second, tn );
1095
          Trace("sygus-sb-exc") << "  ......programs " << prev_bv << " and " << bv << " rewrite to " << bvr << "." << std::endl;
1096
        }
1097
      }
1098
1099
8316
      if (options::sygusRewVerify())
1100
      {
1101
7
        if (bv != bvr)
1102
        {
1103
          // add to the sampler database object
1104
          std::map<TypeNode, quantifiers::SygusSampler>::iterator its =
1105
1
              d_sampler[a].find(tn);
1106
1
          if (its == d_sampler[a].end())
1107
          {
1108
2
            d_sampler[a][tn].initializeSygus(
1109
45
                d_tds, nv, options::sygusSamples(), false);
1110
1
            its = d_sampler[a].find(tn);
1111
          }
1112
          // check equivalent
1113
1
          its->second.checkEquivalent(bv, bvr);
1114
        }
1115
      }
1116
1117
8316
      if( !bad_val_bvr.isNull() ){
1118
2677
        Node bad_val = nv;
1119
2677
        Node bad_val_o = scasv[bad_val_bvr];
1120
2659
        Assert(scasvs.find(bad_val_bvr) != scasvs.end());
1121
2659
        unsigned prev_sz = scasvs[bad_val_bvr];
1122
2659
        bool doFlip = (prev_sz > sz);
1123
2659
        if (doFlip)
1124
        {
1125
          //swap : the excluded value is the previous
1126
18
          scasvs[bad_val_bvr] = sz;
1127
18
          bad_val = scasv[bad_val_bvr];
1128
18
          bad_val_o = nv;
1129
18
          if (Trace.isOn("sygus-sb-exc"))
1130
          {
1131
            Trace("sygus-sb-exc") << "Flip : exclude ";
1132
            quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val);
1133
            Trace("sygus-sb-exc") << " instead of ";
1134
            quantifiers::TermDbSygus::toStreamSygus("sygus-sb-exc", bad_val_o);
1135
            Trace("sygus-sb-exc") << ", since its size is " << sz << " < "
1136
                                  << prev_sz << std::endl;
1137
          }
1138
18
          sz = prev_sz;
1139
        }
1140
2659
        if( Trace.isOn("sygus-sb-exc") ){
1141
          Node bad_val_bv = d_tds->sygusToBuiltin( bad_val, tn );
1142
          Trace("sygus-sb-exc") << "  ........exclude : " << bad_val_bv;
1143
          if( by_examples ){
1144
            Trace("sygus-sb-exc") << " (by examples)";
1145
          }
1146
          Trace("sygus-sb-exc") << std::endl;
1147
        }
1148
2659
        Assert(d_tds->getSygusTermSize(bad_val) == sz);
1149
1150
        // generalize the explanation for why the analog of bad_val
1151
        // is equivalent to bvr
1152
2677
        quantifiers::EquivSygusInvarianceTest eset;
1153
2659
        eset.init(d_tds, tn, aconj, a, bvr);
1154
1155
2659
        Trace("sygus-sb-mexp-debug") << "Minimize explanation for eval[" << d_tds->sygusToBuiltin( bad_val ) << "] = " << bvr << std::endl;
1156
2659
        registerSymBreakLemmaForValue(a, bad_val, eset, bad_val_o, var_count);
1157
1158
        // other generalization criteria go here
1159
1160
        // If the exclusion was flipped, we are excluding a previous value
1161
        // instead of the current one. Hence, the current value is a legal
1162
        // value that we will consider.
1163
2659
        if (!doFlip)
1164
        {
1165
2641
          return Node::null();
1166
        }
1167
      }
1168
    }
1169
  }
1170
48852
  return nv;
1171
}
1172
1173
2659
void SygusExtension::registerSymBreakLemmaForValue(
1174
    Node a,
1175
    Node val,
1176
    quantifiers::SygusInvarianceTest& et,
1177
    Node valr,
1178
    std::map<TypeNode, int>& var_count)
1179
{
1180
5318
  TypeNode tn = val.getType();
1181
5318
  Node x = getFreeVar(tn);
1182
2659
  unsigned sz = d_tds->getSygusTermSize(val);
1183
5318
  std::vector<Node> exp;
1184
2659
  d_tds->getExplain()->getExplanationFor(x, val, exp, et, valr, var_count, sz);
1185
  Node lem =
1186
5318
      exp.size() == 1 ? exp[0] : NodeManager::currentNM()->mkNode(AND, exp);
1187
2659
  lem = lem.negate();
1188
5318
  Trace("sygus-sb-exc") << "  ........exc lemma is " << lem << ", size = " << sz
1189
2659
                        << std::endl;
1190
2659
  registerSymBreakLemma(tn, lem, sz, a);
1191
2659
}
1192
1193
2673
void SygusExtension::registerSymBreakLemma(TypeNode tn,
1194
                                           Node lem,
1195
                                           unsigned sz,
1196
                                           Node a)
1197
{
1198
  // lem holds for all terms of type tn, and is applicable to terms of size sz
1199
5346
  Trace("sygus-sb-debug") << "  register sym break lemma : " << lem
1200
2673
                          << std::endl;
1201
2673
  Trace("sygus-sb-debug") << "     anchor : " << a << std::endl;
1202
2673
  Trace("sygus-sb-debug") << "     type : " << tn << std::endl;
1203
2673
  Trace("sygus-sb-debug") << "     size : " << sz << std::endl;
1204
2673
  Assert(!a.isNull());
1205
2673
  SearchCache& sca = d_cache[a];
1206
2673
  sca.d_sbLemmas[tn][sz].push_back(lem);
1207
5346
  TNode x = getFreeVar( tn );
1208
2673
  unsigned csz = getSearchSizeForAnchor( a );
1209
2673
  int max_depth = ((int)csz)-((int)sz);
1210
2673
  NodeManager* nm = NodeManager::currentNM();
1211
6039
  for( int d=0; d<=max_depth; d++ ){
1212
    std::map<unsigned, std::vector<Node>>::iterator itt =
1213
3366
        sca.d_search_terms[tn].find(d);
1214
3366
    if (itt != sca.d_search_terms[tn].end())
1215
    {
1216
6011
      for (const Node& t : itt->second)
1217
      {
1218
6456
        if (!options::sygusSymBreakLazy()
1219
3228
            || d_active_terms.find(t) != d_active_terms.end())
1220
        {
1221
5824
          Node slem = lem.substitute(x, t);
1222
5824
          Node rlv = getRelevancyCondition(t);
1223
2912
          if (!rlv.isNull())
1224
          {
1225
416
            slem = nm->mkNode(OR, rlv, slem);
1226
          }
1227
2912
          d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_SYM_BREAK);
1228
        }
1229
      }
1230
    }
1231
  }
1232
2673
}
1233
1234
109307
void SygusExtension::addSymBreakLemmasFor(TypeNode tn, TNode t, unsigned d)
1235
{
1236
109307
  Assert(d_term_to_anchor.find(t) != d_term_to_anchor.end());
1237
218614
  Node a = d_term_to_anchor[t];
1238
109307
  addSymBreakLemmasFor(tn, t, d, a);
1239
109307
}
1240
1241
109307
void SygusExtension::addSymBreakLemmasFor(TypeNode tn,
1242
                                          TNode t,
1243
                                          unsigned d,
1244
                                          Node a)
1245
{
1246
109307
  Assert(t.getType() == tn);
1247
109307
  Assert(!a.isNull());
1248
218614
  Trace("sygus-sb-debug2") << "add sym break lemmas for " << t << " " << d
1249
109307
                           << " " << a << std::endl;
1250
109307
  SearchCache& sca = d_cache[a];
1251
  std::map<TypeNode, std::map<uint64_t, std::vector<Node>>>::iterator its =
1252
109307
      sca.d_sbLemmas.find(tn);
1253
218614
  Node rlv = getRelevancyCondition(t);
1254
109307
  NodeManager* nm = NodeManager::currentNM();
1255
109307
  if (its != sca.d_sbLemmas.end())
1256
  {
1257
154714
    TNode x = getFreeVar( tn );
1258
    //get symmetry breaking lemmas for this term
1259
77357
    unsigned csz = getSearchSizeForAnchor( a );
1260
77357
    uint64_t max_sz = d > csz ? 0 : (csz - d);
1261
154714
    Trace("sygus-sb-debug2")
1262
77357
        << "add lemmas up to size " << max_sz << ", which is (search_size) "
1263
77357
        << csz << " - (depth) " << d << std::endl;
1264
154714
    std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
1265
244900
    for (std::pair<const uint64_t, std::vector<Node>>& sbls : its->second)
1266
    {
1267
167543
      if (sbls.first <= max_sz)
1268
      {
1269
623875
        for (const Node& lem : sbls.second)
1270
        {
1271
1060284
          Node slem = lem.substitute(x, t, cache);
1272
          // add the relevancy condition for t
1273
530142
          if (!rlv.isNull())
1274
          {
1275
265058
            slem = nm->mkNode(OR, rlv, slem);
1276
          }
1277
530142
          d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_SYM_BREAK);
1278
        }
1279
      }
1280
    }
1281
  }
1282
109307
  Trace("sygus-sb-debug2") << "...finished." << std::endl;
1283
109307
}
1284
1285
35601
void SygusExtension::preRegisterTerm(TNode n)
1286
{
1287
35601
  if( n.isVar() ){
1288
2097
    Trace("sygus-sb-debug") << "Pre-register variable : " << n << std::endl;
1289
2097
    registerSizeTerm(n);
1290
  }
1291
35601
}
1292
1293
3319
void SygusExtension::registerSizeTerm(Node e)
1294
{
1295
3319
  if (d_register_st.find(e) != d_register_st.end())
1296
  {
1297
    // already registered
1298
4600
    return;
1299
  }
1300
2038
  TypeNode etn = e.getType();
1301
1406
  if (!etn.isDatatype())
1302
  {
1303
    // not a datatype term
1304
58
    d_register_st[e] = false;
1305
58
    return;
1306
  }
1307
1348
  const DType& dt = etn.getDType();
1308
1348
  if (!dt.isSygus())
1309
  {
1310
    // not a sygus datatype term
1311
285
    d_register_st[e] = false;
1312
285
    return;
1313
  }
1314
1063
  if (!d_tds->isEnumerator(e))
1315
  {
1316
    // not sure if it is a size term or not (may be registered later?)
1317
431
    return;
1318
  }
1319
632
  d_register_st[e] = true;
1320
1264
  Node ag = d_tds->getActiveGuardForEnumerator(e);
1321
632
  if (!ag.isNull())
1322
  {
1323
200
    d_anchor_to_active_guard[e] = ag;
1324
    std::map<Node, std::unique_ptr<DecisionStrategy>>::iterator itaas =
1325
200
        d_anchor_to_ag_strategy.find(e);
1326
200
    if (itaas == d_anchor_to_ag_strategy.end())
1327
    {
1328
600
      d_anchor_to_ag_strategy[e].reset(
1329
          new DecisionStrategySingleton("sygus_enum_active",
1330
                                        ag,
1331
200
                                        d_state.getSatContext(),
1332
400
                                        d_state.getValuation()));
1333
    }
1334
400
    d_dm->registerStrategy(DecisionManager::STRAT_DT_SYGUS_ENUM_ACTIVE,
1335
200
                           d_anchor_to_ag_strategy[e].get());
1336
  }
1337
1264
  Node m;
1338
632
  if (!ag.isNull())
1339
  {
1340
    // if it has an active guard (it is an enumerator), use itself as measure
1341
    // term. This will enforce fairness on it independently.
1342
200
    m = e;
1343
  }
1344
  else
1345
  {
1346
    // otherwise we enforce fairness in a unified way for all
1347
432
    if (d_generic_measure_term.isNull())
1348
    {
1349
      // choose e as master for all future terms
1350
213
      d_generic_measure_term = e;
1351
    }
1352
432
    m = d_generic_measure_term;
1353
  }
1354
1264
  Trace("sygus-sb") << "Sygus : register size term : " << e << " with measure "
1355
632
                    << m << std::endl;
1356
632
  registerMeasureTerm(m);
1357
632
  d_szinfo[m]->d_anchors.push_back(e);
1358
632
  d_anchor_to_measure_term[e] = m;
1359
632
  NodeManager* nm = NodeManager::currentNM();
1360
632
  if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
1361
  {
1362
    // update constraints on the measure term
1363
1252
    Node slem;
1364
1252
    if (options::sygusFairMax())
1365
    {
1366
1252
      Node ds = nm->mkNode(DT_SIZE, e);
1367
626
      slem = nm->mkNode(LEQ, ds, d_szinfo[m]->getOrMkMeasureValue());
1368
    }else{
1369
      Node mt = d_szinfo[m]->getOrMkActiveMeasureValue();
1370
      Node new_mt = d_szinfo[m]->getOrMkActiveMeasureValue(true);
1371
      Node ds = nm->mkNode(DT_SIZE, e);
1372
      slem = mt.eqNode(nm->mkNode(PLUS, new_mt, ds));
1373
    }
1374
626
    Trace("sygus-sb") << "...size lemma : " << slem << std::endl;
1375
626
    d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_MT_BOUND);
1376
  }
1377
632
  if (d_tds->isVariableAgnosticEnumerator(e))
1378
  {
1379
    // if it is variable agnostic, enforce top-level constraint that says no
1380
    // variables occur pre-traversal at top-level
1381
4
    Node varList = dt.getSygusVarList();
1382
4
    std::vector<Node> constraints;
1383
2
    quantifiers::SygusTypeInfo& eti = d_tds->getTypeInfo(etn);
1384
6
    for (const Node& v : varList)
1385
    {
1386
4
      unsigned sc = eti.getSubclassForVar(v);
1387
      // no symmetry breaking occurs for variables in singleton subclasses
1388
4
      if (eti.getNumSubclassVars(sc) > 1)
1389
      {
1390
8
        Node preRootOp = getTraversalPredicate(etn, v, true);
1391
8
        Node preRoot = nm->mkNode(APPLY_UF, preRootOp, e);
1392
4
        constraints.push_back(preRoot.negate());
1393
      }
1394
    }
1395
2
    if (!constraints.empty())
1396
    {
1397
2
      Node preNoVar = constraints.size() == 1 ? constraints[0]
1398
4
                                              : nm->mkNode(AND, constraints);
1399
4
      Node preNoVarProc = eliminateTraversalPredicates(preNoVar);
1400
2
      Trace("sygus-sb") << "...variable order : " << preNoVarProc << std::endl;
1401
4
      Trace("sygus-sb-tp") << "...variable order : " << preNoVarProc
1402
2
                           << std::endl;
1403
2
      d_im.lemma(preNoVarProc, InferenceId::DATATYPES_SYGUS_VAR_AGNOSTIC);
1404
    }
1405
  }
1406
}
1407
1408
14982
void SygusExtension::registerMeasureTerm( Node m ) {
1409
  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator it =
1410
14982
      d_szinfo.find(m);
1411
14982
  if( it==d_szinfo.end() ){
1412
413
    Trace("sygus-sb") << "Sygus : register measure term : " << m << std::endl;
1413
413
    d_szinfo[m].reset(new SygusSizeDecisionStrategy(d_im, m, d_state));
1414
    // register this as a decision strategy
1415
826
    d_dm->registerStrategy(DecisionManager::STRAT_DT_SYGUS_ENUM_SIZE,
1416
413
                           d_szinfo[m].get());
1417
  }
1418
14982
}
1419
1420
10546
void SygusExtension::notifySearchSize(TNode m, uint64_t s, Node exp)
1421
{
1422
  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
1423
10546
      d_szinfo.find(m);
1424
10546
  Assert(its != d_szinfo.end());
1425
10546
  if( its->second->d_search_size.find( s )==its->second->d_search_size.end() ){
1426
761
    its->second->d_search_size[s] = true;
1427
761
    its->second->d_search_size_exp[s] = exp;
1428
761
    Assert(s == 0
1429
           || its->second->d_search_size.find(s - 1)
1430
                  != its->second->d_search_size.end());
1431
761
    Trace("sygus-fair") << "SygusExtension:: now considering term measure : " << s << " for " << m << std::endl;
1432
761
    Assert(s >= its->second->d_curr_search_size);
1433
1457
    while( s>its->second->d_curr_search_size ){
1434
348
      incrementCurrentSearchSize(m);
1435
    }
1436
761
    Trace("sygus-fair") << "...finish increment for term measure : " << s << std::endl;
1437
  }
1438
10546
}
1439
1440
unsigned SygusExtension::getSearchSizeFor( Node n ) {
1441
  Trace("sygus-sb-debug2") << "get search size for term : " << n << std::endl;
1442
  std::unordered_map<Node, Node, NodeHashFunction>::iterator ita =
1443
      d_term_to_anchor.find(n);
1444
  Assert(ita != d_term_to_anchor.end());
1445
  return getSearchSizeForAnchor( ita->second );
1446
}
1447
1448
98329
unsigned SygusExtension::getSearchSizeForAnchor( Node a ) {
1449
98329
  Trace("sygus-sb-debug2") << "get search size for anchor : " << a << std::endl;
1450
98329
  std::map< Node, Node >::iterator it = d_anchor_to_measure_term.find( a );
1451
98329
  Assert(it != d_anchor_to_measure_term.end());
1452
98329
  return getSearchSizeForMeasureTerm(it->second);
1453
}
1454
1455
98329
unsigned SygusExtension::getSearchSizeForMeasureTerm(Node m)
1456
{
1457
98329
  Trace("sygus-sb-debug2") << "get search size for measure : " << m << std::endl;
1458
  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator its =
1459
98329
      d_szinfo.find(m);
1460
98329
  Assert(its != d_szinfo.end());
1461
98329
  return its->second->d_curr_search_size;
1462
}
1463
1464
348
void SygusExtension::incrementCurrentSearchSize(TNode m)
1465
{
1466
  std::map<Node, std::unique_ptr<SygusSizeDecisionStrategy>>::iterator itsz =
1467
348
      d_szinfo.find(m);
1468
348
  Assert(itsz != d_szinfo.end());
1469
348
  itsz->second->d_curr_search_size++;
1470
348
  Trace("sygus-fair") << "  register search size " << itsz->second->d_curr_search_size << " for " << m << std::endl;
1471
348
  NodeManager* nm = NodeManager::currentNM();
1472
829
  for( std::map< Node, SearchCache >::iterator itc = d_cache.begin(); itc != d_cache.end(); ++itc ){
1473
962
    Node a = itc->first;
1474
481
    Trace("sygus-fair-debug") << "  look at anchor " << a << "..." << std::endl;
1475
    // check whether a is bounded by m
1476
481
    Assert(d_anchor_to_measure_term.find(a) != d_anchor_to_measure_term.end());
1477
481
    if( d_anchor_to_measure_term[a]==m ){
1478
116
      for (std::pair<const TypeNode, std::map<uint64_t, std::vector<Node>>>&
1479
475
               sbl : itc->second.d_sbLemmas)
1480
      {
1481
232
        TypeNode tn = sbl.first;
1482
232
        TNode x = getFreeVar( tn );
1483
274
        for (std::pair<const uint64_t, std::vector<Node>>& s : sbl.second)
1484
        {
1485
158
          unsigned sz = s.first;
1486
158
          int new_depth = ((int)itsz->second->d_curr_search_size) - ((int)sz);
1487
158
          std::map< unsigned, std::vector< Node > >::iterator itt = itc->second.d_search_terms[tn].find( new_depth );
1488
158
          if( itt!=itc->second.d_search_terms[tn].end() ){
1489
520
            for (const Node& t : itt->second)
1490
            {
1491
776
              if (!options::sygusSymBreakLazy()
1492
388
                  || (d_active_terms.find(t) != d_active_terms.end()
1493
                      && !s.second.empty()))
1494
              {
1495
                Node rlv = getRelevancyCondition(t);
1496
                std::unordered_map<TNode, TNode, TNodeHashFunction> cache;
1497
                for (const Node& lem : s.second)
1498
                {
1499
                  Node slem = lem.substitute(x, t, cache);
1500
                  if (!rlv.isNull())
1501
                  {
1502
                    slem = nm->mkNode(OR, rlv, slem);
1503
                  }
1504
                  d_im.lemma(slem, InferenceId::DATATYPES_SYGUS_SYM_BREAK);
1505
                }
1506
              }
1507
            }
1508
          }
1509
        }
1510
      }
1511
    }
1512
  }
1513
348
}
1514
1515
9991
void SygusExtension::check()
1516
{
1517
9991
  Trace("sygus-sb") << "SygusExtension::check" << std::endl;
1518
1519
  // reset the count of lemmas sent
1520
9991
  d_im.reset();
1521
1522
  // check for externally registered symmetry breaking lemmas
1523
19643
  std::vector<Node> anchors;
1524
9991
  if (d_tds->hasSymBreakLemmas(anchors))
1525
  {
1526
611
    for (const Node& a : anchors)
1527
    {
1528
      // is this a registered enumerator?
1529
316
      if (d_register_st.find(a) != d_register_st.end())
1530
      {
1531
        // symmetry breaking lemmas should only be for enumerators
1532
230
        Assert(d_register_st[a]);
1533
        // If this is a non-basic enumerator, process its symmetry breaking
1534
        // clauses. Since this class is not responsible for basic enumerators,
1535
        // their symmetry breaking clauses are ignored.
1536
230
        if (!d_tds->isBasicEnumerator(a))
1537
        {
1538
12
          std::vector<Node> sbl;
1539
6
          d_tds->getSymBreakLemmas(a, sbl);
1540
20
          for (const Node& lem : sbl)
1541
          {
1542
14
            if (d_tds->isSymBreakLemmaTemplate(lem))
1543
            {
1544
              // register the lemma template
1545
28
              TypeNode tn = d_tds->getTypeForSymBreakLemma(lem);
1546
14
              unsigned sz = d_tds->getSizeForSymBreakLemma(lem);
1547
14
              registerSymBreakLemma(tn, lem, sz, a);
1548
            }
1549
            else
1550
            {
1551
              Trace("dt-sygus-debug")
1552
                  << "DT sym break lemma : " << lem << std::endl;
1553
              // it is a normal lemma
1554
              d_im.lemma(lem, InferenceId::DATATYPES_SYGUS_ENUM_SYM_BREAK);
1555
            }
1556
          }
1557
6
          d_tds->clearSymBreakLemmas(a);
1558
        }
1559
      }
1560
    }
1561
295
    if (d_im.hasSentLemma())
1562
    {
1563
      return;
1564
    }
1565
  }
1566
1567
  // register search values, add symmetry breaking lemmas if applicable
1568
19643
  std::vector<Node> es;
1569
9991
  d_tds->getEnumerators(es);
1570
9991
  bool needsRecheck = false;
1571
  // for each enumerator registered to d_tds
1572
29242
  for (Node& prog : es)
1573
  {
1574
19251
    if (d_register_st.find(prog) == d_register_st.end())
1575
    {
1576
      // not yet registered, do so now
1577
456
      registerSizeTerm(prog);
1578
456
      needsRecheck = true;
1579
    }
1580
    else
1581
    {
1582
37590
      Trace("dt-sygus-debug") << "Checking model value of " << prog << "..."
1583
18795
                              << std::endl;
1584
18795
      Assert(prog.getType().isDatatype());
1585
37590
      Node progv = d_state.getValuation().getModel()->getValue(prog);
1586
18795
      if (Trace.isOn("dt-sygus"))
1587
      {
1588
        Trace("dt-sygus") << "* DT model : " << prog << " -> ";
1589
        std::stringstream ss;
1590
        quantifiers::TermDbSygus::toStreamSygus(ss, progv);
1591
        Trace("dt-sygus") << ss.str() << std::endl;
1592
      }
1593
      // first check that the value progv for prog is what we expected
1594
18795
      bool isExc = true;
1595
18795
      if (checkValue(prog, progv, 0))
1596
      {
1597
18305
        isExc = false;
1598
        //debugging : ensure fairness was properly handled
1599
18305
        if (options::sygusFair() == options::SygusFairMode::DT_SIZE)
1600
        {
1601
36598
          Node prog_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, prog );
1602
36598
          Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz);
1603
36598
          Node progv_sz = NodeManager::currentNM()->mkNode( kind::DT_SIZE, progv );
1604
1605
18299
          Trace("sygus-sb") << "  Mv[" << prog << "] = " << progv << ", size = " << prog_szv << std::endl;
1606
18299
          if( prog_szv.getConst<Rational>().getNumerator().toUnsignedInt() > getSearchSizeForAnchor( prog ) ){
1607
            AlwaysAssert(false);
1608
            Node szlem = NodeManager::currentNM()->mkNode( kind::OR, prog.eqNode( progv ).negate(),
1609
                                                                     prog_sz.eqNode( progv_sz ) );
1610
            Trace("sygus-sb-warn") << "SygusSymBreak : WARNING : adding size correction : " << szlem << std::endl;
1611
            d_im.lemma(szlem, InferenceId::DATATYPES_SYGUS_SIZE_CORRECTION);
1612
            isExc = true;
1613
          }
1614
        }
1615
1616
        // register the search value ( prog -> progv ), this may invoke symmetry
1617
        // breaking
1618
99841
        if (!isExc && options::sygusSymBreakDynamic())
1619
        {
1620
18305
          bool isVarAgnostic = d_tds->isVariableAgnosticEnumerator(prog);
1621
          // check that it is unique up to theory-specific rewriting and
1622
          // conjecture-specific symmetry breaking.
1623
          Node rsv =
1624
36610
              registerSearchValue(prog, prog, progv, 0, isVarAgnostic, true);
1625
18305
          if (rsv.isNull())
1626
          {
1627
2641
            isExc = true;
1628
2641
            Trace("sygus-sb") << "  SygusExtension::check: ...added new symmetry breaking lemma for " << prog << "." << std::endl;
1629
          }
1630
          else
1631
          {
1632
15664
            Trace("dt-sygus") << "  ...success." << std::endl;
1633
          }
1634
        }
1635
      }
1636
      SygusSymBreakOkAttribute ssbo;
1637
18795
      prog.setAttribute(ssbo, !isExc);
1638
    }
1639
  }
1640
9991
  Trace("sygus-sb") << "SygusExtension::check: finished." << std::endl;
1641
9991
  if (needsRecheck)
1642
  {
1643
339
    Trace("sygus-sb") << " SygusExtension::rechecking..." << std::endl;
1644
339
    return check();
1645
  }
1646
1647
9652
  if (Trace.isOn("sygus-engine") && !d_szinfo.empty())
1648
  {
1649
    if (d_im.hasSentLemma())
1650
    {
1651
      Trace("sygus-engine") << "*** Sygus : passed datatypes check. term size(s) : ";
1652
      for (std::pair<const Node, std::unique_ptr<SygusSizeDecisionStrategy>>&
1653
               p : d_szinfo)
1654
      {
1655
        SygusSizeDecisionStrategy* s = p.second.get();
1656
        Trace("sygus-engine") << s->d_curr_search_size << " ";
1657
      }
1658
      Trace("sygus-engine") << std::endl;
1659
    }
1660
    else
1661
    {
1662
      Trace("sygus-engine")
1663
          << "*** Sygus : produced symmetry breaking lemmas" << std::endl;
1664
    }
1665
  }
1666
}
1667
1668
54013
bool SygusExtension::checkValue(Node n, TNode vn, int ind)
1669
{
1670
54013
  if (vn.getKind() != kind::APPLY_CONSTRUCTOR)
1671
  {
1672
    // all datatype terms should be constant here
1673
773
    Assert(!vn.getType().isDatatype());
1674
773
    return true;
1675
  }
1676
53240
  NodeManager* nm = NodeManager::currentNM();
1677
53240
  if (Trace.isOn("sygus-sb-check-value"))
1678
  {
1679
    Node prog_sz = nm->mkNode(DT_SIZE, n);
1680
    Node prog_szv = d_state.getValuation().getModel()->getValue(prog_sz);
1681
    for( int i=0; i<ind; i++ ){
1682
      Trace("sygus-sb-check-value") << "  ";
1683
    }
1684
    Trace("sygus-sb-check-value") << n << " : " << vn << " : " << prog_szv
1685
                                  << std::endl;
1686
  }
1687
106480
  TypeNode tn = n.getType();
1688
53240
  const DType& dt = tn.getDType();
1689
1690
  // ensure that the expected size bound is met
1691
53240
  int cindex = utils::indexOf(vn.getOperator());
1692
106480
  Node tst = utils::mkTester(n, cindex, dt);
1693
53240
  bool hastst = d_state.getEqualityEngine()->hasTerm(tst);
1694
106480
  Node tstrep;
1695
53240
  if (hastst)
1696
  {
1697
52750
    tstrep = d_state.getEqualityEngine()->getRepresentative(tst);
1698
  }
1699
53240
  if (!hastst || tstrep != d_true)
1700
  {
1701
980
    Trace("sygus-check-value") << "- has tester : " << tst << " : "
1702
490
                               << (hastst ? "true" : "false");
1703
490
    Trace("sygus-check-value") << ", value=" << tstrep << std::endl;
1704
490
    if( !hastst ){
1705
      // This should not happen generally, it is caused by a sygus term not
1706
      // being assigned a tester.
1707
980
      Node split = utils::mkSplit(n, dt);
1708
980
      Trace("sygus-sb") << "  SygusExtension::check: ...WARNING: considered "
1709
490
                           "missing split for "
1710
490
                        << n << "." << std::endl;
1711
490
      Assert(!split.isNull());
1712
490
      d_im.lemma(split, InferenceId::DATATYPES_SYGUS_VALUE_CORRECTION);
1713
490
      return false;
1714
    }
1715
  }
1716
87910
  for( unsigned i=0; i<vn.getNumChildren(); i++ ){
1717
    Node sel = nm->mkNode(
1718
70378
        APPLY_SELECTOR_TOTAL, dt[cindex].getSelectorInternal(tn, i), n);
1719
35218
    if (!checkValue(sel, vn[i], ind + 1))
1720
    {
1721
58
      return false;
1722
    }
1723
  }
1724
52692
  return true;
1725
}
1726
1727
Node SygusExtension::getCurrentTemplate( Node n, std::map< TypeNode, int >& var_count ) {
1728
  if( d_active_terms.find( n )!=d_active_terms.end() ){
1729
    TypeNode tn = n.getType();
1730
    IntMap::const_iterator it = d_testers.find( n );
1731
    Assert(it != d_testers.end());
1732
    const DType& dt = tn.getDType();
1733
    int tindex = (*it).second;
1734
    Assert(tindex >= 0);
1735
    Assert(tindex < (int)dt.getNumConstructors());
1736
    std::vector< Node > children;
1737
    children.push_back(dt[tindex].getConstructor());
1738
    for( unsigned i=0; i<dt[tindex].getNumArgs(); i++ ){
1739
      Node sel = NodeManager::currentNM()->mkNode(
1740
          APPLY_SELECTOR_TOTAL, dt[tindex].getSelectorInternal(tn, i), n);
1741
      Node cc = getCurrentTemplate( sel, var_count );
1742
      children.push_back( cc );
1743
    }
1744
    return NodeManager::currentNM()->mkNode( kind::APPLY_CONSTRUCTOR, children );
1745
  }else{
1746
    return d_tds->getFreeVarInc( n.getType(), var_count );
1747
  }
1748
}
1749
1750
413
SygusExtension::SygusSizeDecisionStrategy::SygusSizeDecisionStrategy(
1751
413
    InferenceManager& im, Node t, TheoryState& s)
1752
413
    : DecisionStrategyFmf(s.getSatContext(), s.getValuation()),
1753
      d_this(t),
1754
      d_curr_search_size(0),
1755
826
      d_im(im)
1756
{
1757
413
}
1758
1759
14970
Node SygusExtension::SygusSizeDecisionStrategy::getOrMkMeasureValue()
1760
{
1761
14970
  if (d_measure_value.isNull())
1762
  {
1763
407
    NodeManager* nm = NodeManager::currentNM();
1764
407
    d_measure_value = nm->mkSkolem("mt", nm->integerType());
1765
    Node mtlem =
1766
814
        nm->mkNode(kind::GEQ, d_measure_value, nm->mkConst(Rational(0)));
1767
407
    d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
1768
  }
1769
14970
  return d_measure_value;
1770
}
1771
1772
Node SygusExtension::SygusSizeDecisionStrategy::getOrMkActiveMeasureValue(
1773
    bool mkNew)
1774
{
1775
  if (mkNew)
1776
  {
1777
    NodeManager* nm = NodeManager::currentNM();
1778
    Node new_mt = nm->mkSkolem("mt", nm->integerType());
1779
    Node mtlem = nm->mkNode(kind::GEQ, new_mt, nm->mkConst(Rational(0)));
1780
    d_measure_value_active = new_mt;
1781
    d_im.lemma(mtlem, InferenceId::DATATYPES_SYGUS_MT_POS);
1782
  }
1783
  else if (d_measure_value_active.isNull())
1784
  {
1785
    d_measure_value_active = getOrMkMeasureValue();
1786
  }
1787
  return d_measure_value_active;
1788
}
1789
1790
765
Node SygusExtension::SygusSizeDecisionStrategy::mkLiteral(unsigned s)
1791
{
1792
765
  if (options::sygusFair() == options::SygusFairMode::NONE)
1793
  {
1794
    return Node::null();
1795
  }
1796
2563
  if (options::sygusAbortSize() != -1
1797
765
      && static_cast<int>(s) > options::sygusAbortSize())
1798
  {
1799
8
    std::stringstream ss;
1800
4
    ss << "Maximum term size (" << options::sygusAbortSize()
1801
4
       << ") for enumerative SyGuS exceeded.";
1802
4
    throw LogicException(ss.str());
1803
  }
1804
761
  Assert(!d_this.isNull());
1805
761
  NodeManager* nm = NodeManager::currentNM();
1806
1522
  Trace("sygus-engine") << "******* Sygus : allocate size literal " << s
1807
761
                        << " for " << d_this << std::endl;
1808
761
  return nm->mkNode(DT_SYGUS_BOUND, d_this, nm->mkConst(Rational(s)));
1809
}
1810
1811
int SygusExtension::getGuardStatus( Node g ) {
1812
  bool value;
1813
  if (d_state.getValuation().hasSatValue(g, value))
1814
  {
1815
    if( value ){
1816
      return 1;
1817
    }else{
1818
      return -1;
1819
    }
1820
  }else{
1821
    return 0;
1822
  }
1823
26676
}
1824