GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/quantifiers/sygus/sygus_grammar_cons.cpp Lines: 787 898 87.6 %
Date: 2021-03-22 Branches: 1458 3478 41.9 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_grammar_cons.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Haniel Barbosa, Aina Niemetz
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 class for constructing inductive datatypes that
13
 ** correspond to grammars that encode syntactic restrictions for SyGuS.
14
 **/
15
#include "theory/quantifiers/sygus/sygus_grammar_cons.h"
16
17
#include <stack>
18
19
#include "expr/dtype_cons.h"
20
#include "options/quantifiers_options.h"
21
#include "theory/bv/theory_bv_utils.h"
22
#include "theory/datatypes/sygus_datatype_utils.h"
23
#include "theory/quantifiers/sygus/sygus_grammar_norm.h"
24
#include "theory/quantifiers/sygus/sygus_process_conj.h"
25
#include "theory/quantifiers/sygus/sygus_utils.h"
26
#include "theory/quantifiers/sygus/synth_conjecture.h"
27
#include "theory/quantifiers/sygus/term_database_sygus.h"
28
#include "theory/quantifiers/term_util.h"
29
#include "theory/rewriter.h"
30
#include "theory/strings/word.h"
31
32
using namespace CVC4::kind;
33
34
namespace CVC4 {
35
namespace theory {
36
namespace quantifiers {
37
38
2190
CegGrammarConstructor::CegGrammarConstructor(TermDbSygus* tds,
39
2190
                                             SynthConjecture* p)
40
2190
    : d_tds(tds), d_parent(p), d_is_syntax_restricted(false)
41
{
42
2190
}
43
44
115
bool CegGrammarConstructor::hasSyntaxRestrictions(Node q)
45
{
46
115
  Assert(q.getKind() == FORALL);
47
172
  for (const Node& f : q[0])
48
  {
49
172
    TypeNode tn = SygusUtils::getSygusTypeForSynthFun(f);
50
115
    if (tn.isDatatype() && tn.getDType().isSygus())
51
    {
52
58
      return true;
53
    }
54
  }
55
57
  return false;
56
}
57
58
2
void CegGrammarConstructor::collectTerms(
59
    Node n,
60
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& consts)
61
{
62
4
  std::unordered_map<TNode, bool, TNodeHashFunction> visited;
63
2
  std::unordered_map<TNode, bool, TNodeHashFunction>::iterator it;
64
4
  std::stack<TNode> visit;
65
4
  TNode cur;
66
2
  visit.push(n);
67
24
  do {
68
26
    cur = visit.top();
69
26
    visit.pop();
70
26
    it = visited.find(cur);
71
26
    if (it == visited.end()) {
72
22
      visited[cur] = true;
73
      // is this a constant?
74
22
      if( cur.isConst() ){
75
8
        TypeNode tn = cur.getType();
76
8
        Node c = cur;
77
4
        if( tn.isReal() ){
78
4
          c = NodeManager::currentNM()->mkConst( c.getConst<Rational>().abs() );
79
        }
80
4
        if( std::find( consts[tn].begin(), consts[tn].end(), c )==consts[tn].end() ){
81
4
          Trace("cegqi-debug") << "...consider const : " << c << std::endl;
82
4
          consts[tn].insert(c);
83
        }
84
      }
85
      // recurse
86
46
      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
87
24
        visit.push(cur[i]);
88
      }
89
    }
90
26
  } while (!visit.empty());
91
2
}
92
93
506
Node CegGrammarConstructor::process(Node q,
94
                                    const std::map<Node, Node>& templates,
95
                                    const std::map<Node, Node>& templates_arg)
96
{
97
  // convert to deep embedding and finalize single invocation here
98
  // now, construct the grammar
99
1012
  Trace("cegqi") << "SynthConjecture : convert to deep embedding..."
100
506
                 << std::endl;
101
1012
  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> extra_cons;
102
1020
  if( options::sygusAddConstGrammar() ){
103
2
    Trace("cegqi") << "SynthConjecture : collect constants..." << std::endl;
104
2
    collectTerms( q[1], extra_cons );
105
  }
106
1012
  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> exc_cons;
107
1012
  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>> inc_cons;
108
109
506
  NodeManager* nm = NodeManager::currentNM();
110
111
1012
  std::vector< Node > ebvl;
112
1289
  for( unsigned i=0; i<q[0].getNumChildren(); i++ ){
113
1566
    Node sf = q[0][i];
114
    // if non-null, v encodes the syntactic restrictions (via an inductive
115
    // datatype) on sf from the input.
116
1566
    Node v = sf.getAttribute(SygusSynthGrammarAttribute());
117
1566
    TypeNode preGrammarType;
118
783
    if (!v.isNull())
119
    {
120
329
      preGrammarType = v.getType();
121
    }
122
    else
123
    {
124
      // otherwise, the grammar is the default for the range of the function
125
454
      preGrammarType = sf.getType();
126
454
      if (preGrammarType.isFunction())
127
      {
128
311
        preGrammarType = preGrammarType.getRangeType();
129
      }
130
    }
131
132
    // the actual sygus datatype we will use (normalized below)
133
1566
    TypeNode tn;
134
1566
    std::stringstream ss;
135
783
    ss << sf;
136
1566
    Node sfvl;
137
783
    if (preGrammarType.isDatatype() && preGrammarType.getDType().isSygus())
138
    {
139
329
      sfvl = preGrammarType.getDType().getSygusVarList();
140
329
      tn = preGrammarType;
141
      // normalize type, if user-provided
142
658
      SygusGrammarNorm sygus_norm(d_tds);
143
329
      tn = sygus_norm.normalizeSygusType(tn, sfvl);
144
    }else{
145
454
      sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
146
      // check which arguments are irrelevant
147
908
      std::unordered_set<unsigned> arg_irrelevant;
148
454
      d_parent->getProcess()->getIrrelevantArgs(sf, arg_irrelevant);
149
908
      std::unordered_set<Node, NodeHashFunction> term_irlv;
150
      // convert to term
151
522
      for (const unsigned& arg : arg_irrelevant)
152
      {
153
68
        Assert(arg < sfvl.getNumChildren());
154
68
        term_irlv.insert(sfvl[arg]);
155
      }
156
157
      // make the default grammar
158
454
      tn = mkSygusDefaultType(preGrammarType,
159
                              sfvl,
160
908
                              ss.str(),
161
                              extra_cons,
162
                              exc_cons,
163
                              inc_cons,
164
                              term_irlv);
165
    }
166
    // sfvl may be null for constant synthesis functions
167
1566
    Trace("cegqi-debug") << "...sygus var list associated with " << sf << " is "
168
783
                         << sfvl << std::endl;
169
170
783
    std::map<Node, Node>::const_iterator itt = templates.find(sf);
171
783
    if( itt!=templates.end() ){
172
94
      Node templ = itt->second;
173
47
      std::map<Node, Node>::const_iterator itta = templates_arg.find(sf);
174
47
      Assert(itta != templates_arg.end());
175
94
      TNode templ_arg = itta->second;
176
47
      Assert(!templ_arg.isNull());
177
      // if there is a template for this argument, make a sygus type on top of it
178
158
      if( options::sygusTemplEmbedGrammar() ){
179
        Trace("cegqi-debug") << "Template for " << sf << " is : " << templ
180
                             << " with arg " << templ_arg << std::endl;
181
        Trace("cegqi-debug") << "  embed this template as a grammar..." << std::endl;
182
        tn = mkSygusTemplateType( templ, templ_arg, tn, sfvl, ss.str() );
183
      }
184
    }
185
186
    // ev is the first-order variable corresponding to this synth fun
187
1566
    std::stringstream ssf;
188
783
    ssf << "f" << sf;
189
1566
    Node ev = nm->mkBoundVar(ssf.str(), tn);
190
783
    ebvl.push_back(ev);
191
1566
    Trace("cegqi") << "...embedding synth fun : " << sf << " -> " << ev
192
783
                   << std::endl;
193
  }
194
1012
  return process(q, templates, templates_arg, ebvl);
195
}
196
197
506
Node CegGrammarConstructor::process(Node q,
198
                                    const std::map<Node, Node>& templates,
199
                                    const std::map<Node, Node>& templates_arg,
200
                                    const std::vector<Node>& ebvl)
201
{
202
506
  Assert(q[0].getNumChildren() == ebvl.size());
203
506
  Assert(d_synth_fun_vars.empty());
204
205
506
  NodeManager* nm = NodeManager::currentNM();
206
207
1012
  std::vector<Node> qchildren;
208
1012
  Node qbody_subs = q[1];
209
1289
  for (unsigned i = 0, size = q[0].getNumChildren(); i < size; i++)
210
  {
211
1566
    Node sf = q[0][i];
212
783
    d_synth_fun_vars[sf] = ebvl[i];
213
1566
    Node sfvl = SygusUtils::getSygusArgumentListForSynthFun(sf);
214
1566
    TypeNode tn = ebvl[i].getType();
215
    // check if there is a template
216
783
    std::map<Node, Node>::const_iterator itt = templates.find(sf);
217
783
    if (itt != templates.end())
218
    {
219
94
      Node templ = itt->second;
220
47
      std::map<Node, Node>::const_iterator itta = templates_arg.find(sf);
221
47
      Assert(itta != templates_arg.end());
222
94
      TNode templ_arg = itta->second;
223
47
      Assert(!templ_arg.isNull());
224
      // if there is a template for this argument, make a sygus type on top of
225
      // it
226
47
      if (!options::sygusTemplEmbedGrammar())
227
      {
228
        // otherwise, apply it as a preprocessing pass
229
94
        Trace("cegqi-debug") << "Template for " << sf << " is : " << templ
230
47
                             << " with arg " << templ_arg << std::endl;
231
47
        Trace("cegqi-debug") << "  apply this template as a substituion during preprocess..." << std::endl;
232
94
        std::vector< Node > schildren;
233
94
        std::vector< Node > largs;
234
324
        for( unsigned j=0; j<sfvl.getNumChildren(); j++ ){
235
277
          schildren.push_back( sfvl[j] );
236
277
          largs.push_back(nm->mkBoundVar(sfvl[j].getType()));
237
        }
238
94
        std::vector< Node > subsfn_children;
239
47
        subsfn_children.push_back( sf );
240
47
        subsfn_children.insert( subsfn_children.end(), schildren.begin(), schildren.end() );
241
94
        Node subsfn = nm->mkNode(kind::APPLY_UF, subsfn_children);
242
94
        TNode subsf = subsfn;
243
47
        Trace("cegqi-debug") << "  substitute arg : " << templ_arg << " -> " << subsf << std::endl;
244
47
        templ = templ.substitute( templ_arg, subsf );
245
        // substitute lambda arguments
246
47
        templ = templ.substitute( schildren.begin(), schildren.end(), largs.begin(), largs.end() );
247
        Node subsn =
248
94
            nm->mkNode(kind::LAMBDA, nm->mkNode(BOUND_VAR_LIST, largs), templ);
249
94
        TNode var = sf;
250
94
        TNode subs = subsn;
251
47
        Trace("cegqi-debug") << "  substitute : " << var << " -> " << subs << std::endl;
252
47
        qbody_subs = qbody_subs.substitute( var, subs );
253
47
        Trace("cegqi-debug") << "  body is now : " << qbody_subs << std::endl;
254
      }
255
    }
256
783
    d_tds->registerSygusType(tn);
257
783
    Assert(tn.isDatatype());
258
783
    const DType& dt = tn.getDType();
259
783
    Assert(dt.isSygus());
260
783
    if( !dt.getSygusAllowAll() ){
261
320
      d_is_syntax_restricted = true;
262
    }
263
  }
264
506
  qchildren.push_back(nm->mkNode(kind::BOUND_VAR_LIST, ebvl));
265
506
  if( qbody_subs!=q[1] ){
266
47
    Trace("cegqi") << "...rewriting : " << qbody_subs << std::endl;
267
47
    qbody_subs = Rewriter::rewrite( qbody_subs );
268
47
    Trace("cegqi") << "...got : " << qbody_subs << std::endl;
269
  }
270
506
  qchildren.push_back(convertToEmbedding(qbody_subs));
271
506
  if( q.getNumChildren()==3 ){
272
506
    qchildren.push_back( q[2] );
273
  }
274
1012
  return nm->mkNode(kind::FORALL, qchildren);
275
}
276
277
528
Node CegGrammarConstructor::convertToEmbedding(Node n)
278
{
279
528
  NodeManager* nm = NodeManager::currentNM();
280
1056
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
281
528
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
282
1056
  std::stack<TNode> visit;
283
1056
  TNode cur;
284
528
  visit.push(n);
285
49809
  do {
286
50337
    cur = visit.top();
287
50337
    visit.pop();
288
50337
    it = visited.find(cur);
289
50337
    if (it == visited.end()) {
290
18231
      visited[cur] = Node::null();
291
18231
      visit.push(cur);
292
49809
      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
293
31578
        visit.push(cur[i]);
294
      }
295
32106
    } else if (it->second.isNull()) {
296
36462
      Node ret = cur;
297
18231
      Kind ret_k = cur.getKind();
298
36462
      Node op;
299
18231
      bool childChanged = false;
300
36462
      std::vector<Node> children;
301
      // get the potential operator
302
18231
      if( cur.getNumChildren()>0 ){
303
13899
        if( cur.getKind()==kind::APPLY_UF ){
304
1518
          op = cur.getOperator();
305
        }
306
      }else{
307
4332
        op = cur;
308
      }
309
      // is the operator a synth function?
310
18231
      bool makeEvalFun = false;
311
18231
      if( !op.isNull() ){
312
5850
        std::map<Node, Node>::iterator its = d_synth_fun_vars.find(op);
313
5850
        if (its != d_synth_fun_vars.end())
314
        {
315
1602
          children.push_back( its->second );
316
1602
          makeEvalFun = true;
317
        }
318
      }
319
18231
      if (!makeEvalFun)
320
      {
321
        // otherwise, we apply the previous operator
322
16629
        if( cur.getMetaKind() == kind::metakind::PARAMETERIZED ){
323
428
          children.push_back( cur.getOperator() );
324
        }
325
      }
326
49809
      for (unsigned i = 0; i < cur.getNumChildren(); i++) {
327
31578
        it = visited.find(cur[i]);
328
31578
        Assert(it != visited.end());
329
31578
        Assert(!it->second.isNull());
330
31578
        childChanged = childChanged || cur[i] != it->second;
331
31578
        children.push_back(it->second);
332
      }
333
18231
      if (makeEvalFun)
334
      {
335
1602
        if (!cur.getType().isFunction())
336
        {
337
          // will make into an application of an evaluation function
338
1589
          ret = nm->mkNode(DT_SYGUS_EVAL, children);
339
        }
340
        else
341
        {
342
13
          Assert(children.size() == 1);
343
26
          Node ef = children[0];
344
          // Otherwise, we are using the function-to-synthesize itself in a
345
          // higher-order setting. We must return the lambda term:
346
          //   lambda x1...xn. (DT_SYGUS_EVAL ef x1 ... xn)
347
          // where ef is the first order variable for the
348
          // function-to-synthesize.
349
13
          SygusTypeInfo& ti = d_tds->getTypeInfo(ef.getType());
350
13
          const std::vector<Node>& vars = ti.getVarList();
351
13
          Assert(!vars.empty());
352
26
          std::vector<Node> vs;
353
32
          for (const Node& v : vars)
354
          {
355
19
            vs.push_back(nm->mkBoundVar(v.getType()));
356
          }
357
26
          Node lvl = nm->mkNode(BOUND_VAR_LIST, vs);
358
26
          std::vector<Node> eargs;
359
13
          eargs.push_back(ef);
360
13
          eargs.insert(eargs.end(), vs.begin(), vs.end());
361
13
          ret = nm->mkNode(LAMBDA, lvl, nm->mkNode(DT_SYGUS_EVAL, eargs));
362
        }
363
      }
364
16629
      else if (childChanged)
365
      {
366
6926
        ret = nm->mkNode(ret_k, children);
367
      }
368
18231
      visited[cur] = ret;
369
    }
370
50337
  } while (!visit.empty());
371
528
  Assert(visited.find(n) != visited.end());
372
528
  Assert(!visited.find(n)->second.isNull());
373
1056
  return visited[n];
374
}
375
376
1248
TypeNode CegGrammarConstructor::mkUnresolvedType(const std::string& name,
377
                                                 std::set<TypeNode>& unres)
378
{
379
  TypeNode unresolved = NodeManager::currentNM()->mkSort(
380
1248
      name, NodeManager::SORT_FLAG_PLACEHOLDER);
381
1248
  unres.insert(unresolved);
382
1248
  return unresolved;
383
}
384
385
1203
void CegGrammarConstructor::mkSygusConstantsForType(TypeNode type,
386
                                                    std::vector<Node>& ops)
387
{
388
1203
  NodeManager* nm = NodeManager::currentNM();
389
1203
  if (type.isReal())
390
  {
391
468
    ops.push_back(nm->mkConst(Rational(0)));
392
468
    ops.push_back(nm->mkConst(Rational(1)));
393
  }
394
735
  else if (type.isBitVector())
395
  {
396
41
    unsigned size = type.getBitVectorSize();
397
41
    ops.push_back(bv::utils::mkZero(size));
398
41
    ops.push_back(bv::utils::mkOne(size));
399
  }
400
694
  else if (type.isBoolean())
401
  {
402
597
    ops.push_back(nm->mkConst(true));
403
597
    ops.push_back(nm->mkConst(false));
404
  }
405
97
  else if (type.isStringLike())
406
  {
407
39
    ops.push_back(strings::Word::mkEmptyWord(type));
408
39
    if (type.isString())  // string-only
409
    {
410
      // Dummy character "A". This is not necessary for sequences which
411
      // have the generic constructor seq.unit.
412
39
      ops.push_back(nm->mkConst(String("A")));
413
    }
414
  }
415
58
  else if (type.isArray() || type.isSet())
416
  {
417
    // generate constant array over the first element of the constituent type
418
54
    Node c = type.mkGroundTerm();
419
27
    ops.push_back(c);
420
  }
421
31
  else if (type.isRoundingMode())
422
  {
423
    ops.push_back(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_AWAY));
424
    ops.push_back(nm->mkConst(RoundingMode::ROUND_NEAREST_TIES_TO_EVEN));
425
    ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_NEGATIVE));
426
    ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_POSITIVE));
427
    ops.push_back(nm->mkConst(RoundingMode::ROUND_TOWARD_ZERO));
428
  }
429
31
  else if (type.isFloatingPoint())
430
  {
431
    FloatingPointSize fp_size(type.getFloatingPointExponentSize(),
432
                              type.getFloatingPointSignificandSize());
433
    ops.push_back(nm->mkConst(FloatingPoint::makeNaN(fp_size)));
434
    ops.push_back(nm->mkConst(FloatingPoint::makeInf(fp_size, true)));
435
    ops.push_back(nm->mkConst(FloatingPoint::makeInf(fp_size, false)));
436
    ops.push_back(nm->mkConst(FloatingPoint::makeZero(fp_size, true)));
437
    ops.push_back(nm->mkConst(FloatingPoint::makeZero(fp_size, false)));
438
    ops.push_back(nm->mkConst(FloatingPoint::makeMinSubnormal(fp_size, true)));
439
    ops.push_back(nm->mkConst(FloatingPoint::makeMinSubnormal(fp_size, false)));
440
    ops.push_back(nm->mkConst(FloatingPoint::makeMaxSubnormal(fp_size, true)));
441
    ops.push_back(nm->mkConst(FloatingPoint::makeMaxSubnormal(fp_size, false)));
442
    ops.push_back(nm->mkConst(FloatingPoint::makeMinNormal(fp_size, true)));
443
    ops.push_back(nm->mkConst(FloatingPoint::makeMinNormal(fp_size, false)));
444
    ops.push_back(nm->mkConst(FloatingPoint::makeMaxNormal(fp_size, true)));
445
    ops.push_back(nm->mkConst(FloatingPoint::makeMaxNormal(fp_size, false)));
446
  }
447
1203
}
448
449
1938
void CegGrammarConstructor::collectSygusGrammarTypesFor(
450
    TypeNode range, std::vector<TypeNode>& types)
451
{
452
1938
  if( !range.isBoolean() ){
453
1502
    if( std::find( types.begin(), types.end(), range )==types.end() ){
454
768
      Trace("sygus-grammar-def") << "...will make grammar for " << range << std::endl;
455
768
      types.push_back( range );
456
768
      if( range.isDatatype() ){
457
27
        const DType& dt = range.getDType();
458
63
        for (unsigned i = 0, size = dt.getNumConstructors(); i < size; ++i)
459
        {
460
90
          for (unsigned j = 0, size_args = dt[i].getNumArgs(); j < size_args;
461
               ++j)
462
          {
463
108
            TypeNode tn = dt[i][j].getRangeType();
464
54
            collectSygusGrammarTypesFor(tn, types);
465
          }
466
        }
467
      }
468
741
      else if (range.isArray())
469
      {
470
        // add index and constituent type
471
23
        collectSygusGrammarTypesFor(range.getArrayIndexType(), types);
472
23
        collectSygusGrammarTypesFor(range.getArrayConstituentType(), types);
473
      }
474
718
      else if (range.isSet())
475
      {
476
12
        collectSygusGrammarTypesFor(range.getSetElementType(), types);
477
      }
478
706
      else if (range.isStringLike())
479
      {
480
        // theory of strings shares the integer type
481
118
        TypeNode intType = NodeManager::currentNM()->integerType();
482
59
        collectSygusGrammarTypesFor(intType,types);
483
59
        if (range.isSequence())
484
        {
485
          collectSygusGrammarTypesFor(range.getSequenceElementType(), types);
486
        }
487
      }
488
647
      else if (range.isFunction())
489
      {
490
54
        std::vector<TypeNode> atypes = range.getArgTypes();
491
57
        for (unsigned i = 0, ntypes = atypes.size(); i < ntypes; i++)
492
        {
493
30
          collectSygusGrammarTypesFor(atypes[i], types);
494
        }
495
27
        collectSygusGrammarTypesFor(range.getRangeType(), types);
496
      }
497
620
      else if (range.isFloatingPoint())
498
      {
499
        // FP also includes RoundingMode type
500
        TypeNode rmType = NodeManager::currentNM()->roundingModeType();
501
        collectSygusGrammarTypesFor(rmType, types);
502
      }
503
    }
504
  }
505
1938
}
506
507
148
bool CegGrammarConstructor::isHandledType(TypeNode t)
508
{
509
296
  std::vector<TypeNode> types;
510
148
  collectSygusGrammarTypesFor(t, types);
511
310
  for (const TypeNode& tn : types)
512
  {
513
164
    if (tn.isSort() || tn.isFloatingPoint())
514
    {
515
2
      return false;
516
    }
517
  }
518
146
  return true;
519
}
520
521
8
Node CegGrammarConstructor::createLambdaWithZeroArg(
522
    Kind k, TypeNode bArgType)
523
{
524
8
  NodeManager* nm = NodeManager::currentNM();
525
16
  std::vector<Node> opLArgs;
526
  // get the builtin type
527
8
  opLArgs.push_back(nm->mkBoundVar(bArgType));
528
  // build zarg
529
16
  Node zarg;
530
8
  Assert(bArgType.isReal() || bArgType.isBitVector());
531
8
  if (bArgType.isReal())
532
  {
533
8
    zarg = nm->mkConst(Rational(0));
534
  }
535
  else
536
  {
537
    unsigned size = bArgType.getBitVectorSize();
538
    zarg = bv::utils::mkZero(size);
539
  }
540
16
  Node body = nm->mkNode(k, zarg, opLArgs.back());
541
  // create operator
542
8
  Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), body);
543
8
  Trace("sygus-grammar-def") << "\t...building lambda op " << op << "\n";
544
16
  return op;
545
}
546
547
584
void CegGrammarConstructor::mkSygusDefaultGrammar(
548
    TypeNode range,
549
    Node bvl,
550
    const std::string& fun,
551
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons,
552
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
553
        exclude_cons,
554
    const std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
555
        include_cons,
556
    std::unordered_set<Node, NodeHashFunction>& term_irrelevant,
557
    std::vector<SygusDatatypeGenerator>& sdts,
558
    std::set<TypeNode>& unres)
559
{
560
584
  NodeManager* nm = NodeManager::currentNM();
561
1168
  Trace("sygus-grammar-def") << "Construct default grammar for " << fun << " "
562
584
                             << range << std::endl;
563
  // collect the variables
564
1168
  std::vector<Node> sygus_vars;
565
584
  if (!bvl.isNull())
566
  {
567
1366
    for (unsigned i = 0, size = bvl.getNumChildren(); i < size; ++i)
568
    {
569
1046
      if (term_irrelevant.find(bvl[i]) == term_irrelevant.end())
570
      {
571
978
        sygus_vars.push_back(bvl[i]);
572
      }
573
      else
574
      {
575
136
        Trace("sygus-grammar-def")
576
136
            << "...synth var " << bvl[i] << " has been marked irrelevant."
577
68
            << std::endl;
578
      }
579
    }
580
  }
581
  // index of top datatype, i.e. the datatype for the range type
582
584
  int startIndex = -1;
583
1168
  std::map<TypeNode, TypeNode> sygus_to_builtin;
584
585
1168
  std::vector<TypeNode> types;
586
  // Collect connected types for each of the variables.
587
1562
  for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
588
  {
589
1956
    TypeNode tni = sygus_vars[i].getType();
590
978
    collectSygusGrammarTypesFor(tni, types);
591
  }
592
  // collect connected types to range
593
584
  collectSygusGrammarTypesFor(range, types);
594
595
  // create placeholder for boolean type (kept apart since not collected)
596
597
  // create placeholders for collected types
598
1168
  std::vector<TypeNode> unres_types;
599
1168
  std::map<TypeNode, TypeNode> type_to_unres;
600
  std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::const_iterator
601
584
      itc;
602
  // maps types to the index of its "any term" grammar construction
603
1168
  std::map<TypeNode, std::pair<unsigned, bool>> typeToGAnyTerm;
604
584
  options::SygusGrammarConsMode sgcm = options::sygusGrammarConsMode();
605
1188
  for (unsigned i = 0, size = types.size(); i < size; ++i)
606
  {
607
1208
    std::stringstream ss;
608
604
    ss << fun << "_" << types[i];
609
1208
    std::string dname = ss.str();
610
604
    sdts.push_back(SygusDatatypeGenerator(dname));
611
604
    itc = exclude_cons.find(types[i]);
612
604
    if (itc != exclude_cons.end())
613
    {
614
      sdts.back().d_exclude_cons = itc->second;
615
    }
616
604
    itc = include_cons.find(types[i]);
617
604
    if (itc != include_cons.end())
618
    {
619
3
      sdts.back().d_include_cons = itc->second;
620
    }
621
    //make unresolved type
622
1208
    TypeNode unres_t = mkUnresolvedType(dname, unres);
623
604
    unres_types.push_back(unres_t);
624
604
    type_to_unres[types[i]] = unres_t;
625
604
    sygus_to_builtin[unres_t] = types[i];
626
  }
627
  // make Boolean type
628
1168
  std::stringstream ssb;
629
584
  ssb << fun << "_Bool";
630
1168
  std::string dbname = ssb.str();
631
584
  sdts.push_back(SygusDatatypeGenerator(dbname));
632
584
  unsigned boolIndex = types.size();
633
1168
  TypeNode bool_type = nm->booleanType();
634
1168
  TypeNode unres_bt = mkUnresolvedType(ssb.str(), unres);
635
584
  types.push_back(bool_type);
636
584
  unres_types.push_back(unres_bt);
637
584
  type_to_unres[bool_type] = unres_bt;
638
584
  sygus_to_builtin[unres_bt] = bool_type;
639
640
  // We ensure an ordering on types such that parametric types are processed
641
  // before their consitituents. Since parametric types were added before their
642
  // arguments in collectSygusGrammarTypesFor above, we will construct the
643
  // sygus grammars by iterating on types in reverse order. This ensures
644
  // that we know all constructors coming from other types (e.g. select(A,i))
645
  // by the time we process the type. We start with types.size()-2, since
646
  // we construct the grammar for the Boolean type last.
647
1188
  for (int i = (types.size() - 2); i >= 0; --i)
648
  {
649
1208
    Trace("sygus-grammar-def") << "Make grammar for " << types[i] << " "
650
604
                               << unres_types[i] << std::endl;
651
1208
    TypeNode unres_t = unres_types[i];
652
604
    options::SygusGrammarConsMode tsgcm = sgcm;
653
604
    if (tsgcm == options::SygusGrammarConsMode::ANY_TERM
654
596
        || tsgcm == options::SygusGrammarConsMode::ANY_TERM_CONCISE)
655
    {
656
      // If the type does not support any term, we do any constant instead.
657
      // We also fall back on any constant construction if the type has no
658
      // constructors at this point (e.g. it simply encodes all constants).
659
12
      if (!types[i].isReal())
660
      {
661
4
        tsgcm = options::SygusGrammarConsMode::ANY_CONST;
662
      }
663
      else
664
      {
665
        // Add a placeholder for the "any term" version of this datatype, to be
666
        // constructed later.
667
16
        std::stringstream ssat;
668
8
        ssat << sdts[i].d_sdt.getName() << "_any_term";
669
8
        sdts.push_back(SygusDatatypeGenerator(ssat.str()));
670
16
        TypeNode unresAnyTerm = mkUnresolvedType(ssat.str(), unres);
671
8
        unres_types.push_back(unresAnyTerm);
672
        // set tracking information for later addition at boolean type.
673
8
        std::pair<unsigned, bool> p(sdts.size() - 1, false);
674
8
        typeToGAnyTerm[types[i]] = p;
675
      }
676
    }
677
1208
    Trace("sygus-grammar-def")
678
604
        << "Grammar constructor mode for this type is " << tsgcm << std::endl;
679
    //add variables
680
1821
    for (const Node& sv : sygus_vars)
681
    {
682
2434
      TypeNode svt = sv.getType();
683
1217
      if (svt == types[i])
684
      {
685
1530
        std::stringstream ss;
686
765
        ss << sv;
687
1530
        Trace("sygus-grammar-def")
688
765
            << "...add for variable " << ss.str() << std::endl;
689
1530
        std::vector<TypeNode> cargsEmpty;
690
765
        sdts[i].addConstructor(sv, ss.str(), cargsEmpty);
691
      }
692
452
      else if (svt.isFunction() && svt.getRangeType() == types[i])
693
      {
694
        // We add an APPLY_UF for all function whose return type is this type
695
        // whose argument types are the other sygus types we are constructing.
696
8
        std::vector<TypeNode> argTypes = svt.getArgTypes();
697
8
        std::vector<TypeNode> stypes;
698
8
        for (unsigned k = 0, ntypes = argTypes.size(); k < ntypes; k++)
699
        {
700
          unsigned index =
701
4
              std::distance(types.begin(),
702
8
                            std::find(types.begin(), types.end(), argTypes[k]));
703
4
          stypes.push_back(unres_types[index]);
704
        }
705
8
        std::stringstream ss;
706
4
        ss << "apply_" << sv;
707
4
        sdts[i].addConstructor(sv, ss.str(), stypes);
708
      }
709
    }
710
    //add constants
711
1208
    std::vector<Node> consts;
712
604
    mkSygusConstantsForType(types[i], consts);
713
604
    if (tsgcm == options::SygusGrammarConsMode::ANY_CONST)
714
    {
715
      // Use the any constant constructor. Notice that for types that don't
716
      // have constants (e.g. uninterpreted or function types), we don't add
717
      // this constructor.
718
10
      if (!consts.empty())
719
      {
720
10
        sdts[i].d_sdt.addAnyConstantConstructor(types[i]);
721
      }
722
    }
723
    else
724
    {
725
      std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
726
594
          itec = extra_cons.find(types[i]);
727
594
      if (itec != extra_cons.end())
728
      {
729
346
        for (std::unordered_set<Node, NodeHashFunction>::iterator set_it =
730
96
                 itec->second.begin();
731
442
             set_it != itec->second.end();
732
             ++set_it)
733
        {
734
346
          if (std::find(consts.begin(), consts.end(), *set_it) == consts.end())
735
          {
736
176
            consts.push_back(*set_it);
737
          }
738
        }
739
      }
740
1871
      for (unsigned j = 0, size_j = consts.size(); j < size_j; ++j)
741
      {
742
2554
        std::stringstream ss;
743
1277
        ss << consts[j];
744
2554
        Trace("sygus-grammar-def")
745
1277
            << "...add for constant " << ss.str() << std::endl;
746
2554
        std::vector<TypeNode> cargsEmpty;
747
1277
        sdts[i].addConstructor(consts[j], ss.str(), cargsEmpty);
748
      }
749
    }
750
751
604
    if (types[i].isReal())
752
    {
753
      // Add PLUS, MINUS
754
468
      Kind kinds[2] = {PLUS, MINUS};
755
1404
      for (const Kind kind : kinds)
756
      {
757
936
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
758
1872
        std::vector<TypeNode> cargsOp;
759
936
        cargsOp.push_back(unres_t);
760
936
        cargsOp.push_back(unres_t);
761
936
        sdts[i].addConstructor(kind, cargsOp);
762
      }
763
468
      if (!types[i].isInteger())
764
      {
765
88
        Trace("sygus-grammar-def")
766
44
            << "  ...create auxiliary Positive Integers grammar\n";
767
        // Creating type for positive integers. Notice we can't use the any
768
        // constant constructor here, since it admits zero.
769
88
        std::stringstream ss;
770
44
        ss << fun << "_PosInt";
771
88
        std::string pos_int_name = ss.str();
772
        // make unresolved type
773
88
        TypeNode unresPosInt = mkUnresolvedType(pos_int_name, unres);
774
44
        unres_types.push_back(unresPosInt);
775
        // make data type for positive constant integers
776
44
        sdts.push_back(SygusDatatypeGenerator(pos_int_name));
777
        /* Add operator 1 */
778
44
        Trace("sygus-grammar-def") << "\t...add for 1 to Pos_Int\n";
779
88
        std::vector<TypeNode> cargsEmpty;
780
44
        sdts.back().addConstructor(nm->mkConst(Rational(1)), "1", cargsEmpty);
781
        /* Add operator PLUS */
782
44
        Kind kind = PLUS;
783
44
        Trace("sygus-grammar-def") << "\t...add for PLUS to Pos_Int\n";
784
88
        std::vector<TypeNode> cargsPlus;
785
44
        cargsPlus.push_back(unresPosInt);
786
44
        cargsPlus.push_back(unresPosInt);
787
44
        sdts.back().addConstructor(kind, cargsPlus);
788
44
        sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true);
789
88
        Trace("sygus-grammar-def")
790
44
            << "  ...built datatype " << sdts.back().d_sdt.getDatatype() << " ";
791
        /* Adding division at root */
792
44
        kind = DIVISION;
793
44
        Trace("sygus-grammar-def") << "\t...add for " << kind << std::endl;
794
88
        std::vector<TypeNode> cargsDiv;
795
44
        cargsDiv.push_back(unres_t);
796
44
        cargsDiv.push_back(unresPosInt);
797
44
        sdts[i].addConstructor(kind, cargsDiv);
798
      }
799
    }
800
136
    else if (types[i].isBitVector())
801
    {
802
      // unary ops
803
82
      std::vector<Kind> un_kinds = {BITVECTOR_NOT, BITVECTOR_NEG};
804
82
      std::vector<TypeNode> cargsUnary;
805
41
      cargsUnary.push_back(unres_t);
806
123
      for (const Kind kind : un_kinds)
807
      {
808
82
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
809
82
        sdts[i].addConstructor(kind, cargsUnary);
810
      }
811
      // binary ops
812
      std::vector<Kind> bin_kinds = {BITVECTOR_AND,
813
                                     BITVECTOR_OR,
814
                                     BITVECTOR_XOR,
815
                                     BITVECTOR_PLUS,
816
                                     BITVECTOR_SUB,
817
                                     BITVECTOR_MULT,
818
                                     BITVECTOR_UDIV,
819
                                     BITVECTOR_UREM,
820
                                     BITVECTOR_SDIV,
821
                                     BITVECTOR_SREM,
822
                                     BITVECTOR_SHL,
823
                                     BITVECTOR_LSHR,
824
82
                                     BITVECTOR_ASHR};
825
82
      std::vector<TypeNode> cargsBinary;
826
41
      cargsBinary.push_back(unres_t);
827
41
      cargsBinary.push_back(unres_t);
828
574
      for (const Kind kind : bin_kinds)
829
      {
830
533
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
831
533
        sdts[i].addConstructor(kind, cargsBinary);
832
      }
833
    }
834
95
    else if (types[i].isFloatingPoint())
835
    {
836
      // unary ops
837
      std::vector<Kind> unary_kinds = {
838
          FLOATINGPOINT_ABS,
839
          FLOATINGPOINT_NEG,
840
      };
841
      std::vector<TypeNode> cargs = {unres_t};
842
      for (const Kind kind : unary_kinds)
843
      {
844
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
845
        sdts[i].addConstructor(kind, cargs);
846
      }
847
      // binary ops
848
      {
849
        const Kind kind = FLOATINGPOINT_REM;
850
        cargs.push_back(unres_t);
851
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
852
        sdts[i].addConstructor(kind, cargs);
853
      }
854
      // binary ops with RM
855
      std::vector<Kind> binary_rm_kinds = {
856
          FLOATINGPOINT_SQRT,
857
          FLOATINGPOINT_RTI,
858
      };
859
      TypeNode rmType = nm->roundingModeType();
860
      Assert(std::find(types.begin(), types.end(), rmType) != types.end());
861
      TypeNode unres_rm_t = type_to_unres[rmType];
862
      std::vector<TypeNode> cargs_rm = {unres_rm_t, unres_t};
863
      for (const Kind kind : binary_rm_kinds)
864
      {
865
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
866
        sdts[i].addConstructor(kind, cargs_rm);
867
      }
868
      // ternary ops with RM
869
      std::vector<Kind> ternary_rm_kinds = {
870
          FLOATINGPOINT_PLUS,
871
          FLOATINGPOINT_SUB,
872
          FLOATINGPOINT_MULT,
873
          FLOATINGPOINT_DIV,
874
      };
875
      cargs_rm.push_back(unres_t);
876
      for (const Kind kind : ternary_rm_kinds)
877
      {
878
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
879
        sdts[i].addConstructor(kind, cargs_rm);
880
      }
881
      // quaternary ops
882
      {
883
        cargs_rm.push_back(unres_t);
884
        const Kind kind = FLOATINGPOINT_FMA;
885
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
886
        sdts[i].addConstructor(kind, cargs_rm);
887
      }
888
    }
889
95
    else if (types[i].isStringLike())
890
    {
891
      // concatenation
892
78
      std::vector<TypeNode> cargsBinary;
893
39
      cargsBinary.push_back(unres_t);
894
39
      cargsBinary.push_back(unres_t);
895
39
      sdts[i].addConstructor(STRING_CONCAT, cargsBinary);
896
      // length
897
78
      TypeNode intType = nm->integerType();
898
39
      Assert(std::find(types.begin(), types.end(), intType) != types.end());
899
39
      unsigned i_intType = std::distance(
900
          types.begin(),
901
          std::find(types.begin(),
902
                    types.end(),
903
39
                    intType));
904
78
      std::vector<TypeNode> cargsLen;
905
39
      cargsLen.push_back(unres_t);
906
39
      sdts[i_intType].addConstructor(STRING_LENGTH, cargsLen);
907
39
      if (types[i].isSequence())
908
      {
909
        TypeNode etype = types[i].getSequenceElementType();
910
        // retrieve element unresolved type
911
        Assert(type_to_unres.find(etype) != type_to_unres.end());
912
        TypeNode unresElemType = type_to_unres[etype];
913
914
        Trace("sygus-grammar-def") << "...add for seq.unit" << std::endl;
915
        std::vector<TypeNode> cargsSeqUnit;
916
        cargsSeqUnit.push_back(unresElemType);
917
        sdts[i].addConstructor(SEQ_UNIT, cargsSeqUnit);
918
      }
919
    }
920
56
    else if (types[i].isArray())
921
    {
922
34
      Trace("sygus-grammar-def")
923
17
          << "...building for array type " << types[i] << "\n";
924
34
      TypeNode indexType = types[i].getArrayIndexType();
925
34
      TypeNode elemType = types[i].getArrayConstituentType();
926
34
      Trace("sygus-grammar-def")
927
17
          << "......finding unres type for index type " << indexType << "\n";
928
      // retrieve index and constituent unresolved types
929
17
      Assert(type_to_unres.find(indexType) != type_to_unres.end());
930
34
      TypeNode unres_indexType = type_to_unres[indexType];
931
17
      Assert(std::find(types.begin(), types.end(), elemType) != types.end());
932
      // must get this index since we add to sdt[i_constituentType] below.
933
17
      unsigned i_constituentType = std::distance(
934
17
          types.begin(), std::find(types.begin(), types.end(), elemType));
935
34
      TypeNode unres_constituentType = unres_types[i_constituentType];
936
      // add (store ArrayType IndexType ConstituentType)
937
17
      Trace("sygus-grammar-def") << "...add for STORE\n";
938
939
34
      std::vector<TypeNode> cargsStore;
940
17
      cargsStore.push_back(unres_t);
941
17
      cargsStore.push_back(unres_indexType);
942
17
      cargsStore.push_back(unres_constituentType);
943
17
      sdts[i].addConstructor(STORE, cargsStore);
944
      // add to constituent type : (select ArrayType IndexType)
945
34
      Trace("sygus-grammar-def") << "...add select for constituent type"
946
17
                                 << unres_constituentType << "\n";
947
34
      std::vector<TypeNode> cargsSelect;
948
17
      cargsSelect.push_back(unres_t);
949
17
      cargsSelect.push_back(unres_indexType);
950
17
      sdts[i_constituentType].addConstructor(SELECT, cargsSelect);
951
    }
952
39
    else if (types[i].isSet())
953
    {
954
16
      TypeNode etype = types[i].getSetElementType();
955
      // retrieve element unresolved type
956
8
      Assert(type_to_unres.find(etype) != type_to_unres.end());
957
16
      TypeNode unresElemType = type_to_unres[etype];
958
959
      // add for singleton
960
8
      Trace("sygus-grammar-def") << "...add for singleton" << std::endl;
961
16
      std::vector<TypeNode> cargsSingleton;
962
8
      cargsSingleton.push_back(unresElemType);
963
964
      // lambda x . (singleton (singleton_op T) x) where T = x.getType()
965
16
      Node x = nm->mkBoundVar(etype);
966
16
      Node vars = nm->mkNode(BOUND_VAR_LIST, x);
967
16
      Node singleton = nm->mkSingleton(etype, x);
968
16
      Node lambda = nm->mkNode(LAMBDA,vars, singleton);
969
8
      sdts[i].addConstructor(lambda, "singleton", cargsSingleton);
970
971
      // add for union, difference, intersection
972
16
      std::vector<Kind> bin_kinds = {UNION, INTERSECTION, SETMINUS};
973
16
      std::vector<TypeNode> cargsBinary;
974
8
      cargsBinary.push_back(unres_t);
975
8
      cargsBinary.push_back(unres_t);
976
32
      for (const Kind kind : bin_kinds)
977
      {
978
24
        Trace("sygus-grammar-def") << "...add for " << kind << std::endl;
979
24
        sdts[i].addConstructor(kind, cargsBinary);
980
      }
981
    }
982
31
    else if (types[i].isDatatype())
983
    {
984
27
      Trace("sygus-grammar-def") << "...add for constructors" << std::endl;
985
27
      const DType& dt = types[i].getDType();
986
63
      for (unsigned l = 0, size_l = dt.getNumConstructors(); l < size_l; ++l)
987
      {
988
36
        Trace("sygus-grammar-def") << "...for " << dt[l].getName() << std::endl;
989
72
        Node cop = dt[l].getConstructor();
990
36
        if (dt[l].getNumArgs() == 0)
991
        {
992
          // Nullary constructors are interpreted as terms, not operators.
993
          // Thus, we apply them to no arguments here.
994
9
          cop = nm->mkNode(APPLY_CONSTRUCTOR, cop);
995
        }
996
72
        std::vector<TypeNode> cargsCons;
997
36
        Trace("sygus-grammar-def") << "...add for selectors" << std::endl;
998
90
        for (unsigned j = 0, size_j = dt[l].getNumArgs(); j < size_j; ++j)
999
        {
1000
108
          Trace("sygus-grammar-def")
1001
54
              << "...for " << dt[l][j].getName() << std::endl;
1002
108
          TypeNode crange = dt[l][j].getRangeType();
1003
54
          Assert(type_to_unres.find(crange) != type_to_unres.end());
1004
54
          cargsCons.push_back(type_to_unres[crange]);
1005
          // add to the selector type the selector operator
1006
1007
54
          Assert(std::find(types.begin(), types.end(), crange) != types.end());
1008
54
          unsigned i_selType = std::distance(
1009
54
              types.begin(), std::find(types.begin(), types.end(), crange));
1010
108
          TypeNode arg_type = dt[l][j].getType();
1011
54
          arg_type = arg_type.getSelectorDomainType();
1012
54
          Assert(type_to_unres.find(arg_type) != type_to_unres.end());
1013
108
          std::vector<TypeNode> cargsSel;
1014
54
          cargsSel.push_back(type_to_unres[arg_type]);
1015
108
          Node sel = dt[l][j].getSelector();
1016
54
          sdts[i_selType].addConstructor(sel, dt[l][j].getName(), cargsSel);
1017
        }
1018
36
        sdts[i].addConstructor(cop, dt[l].getName(), cargsCons);
1019
      }
1020
    }
1021
12
    else if (types[i].isSort() || types[i].isFunction()
1022
4
             || types[i].isRoundingMode())
1023
    {
1024
      // do nothing
1025
    }
1026
    else
1027
    {
1028
      Warning()
1029
          << "Warning: No implementation for default Sygus grammar of type "
1030
          << types[i] << std::endl;
1031
    }
1032
1033
604
    if (sdts[i].d_sdt.getNumConstructors() == 0)
1034
    {
1035
      // if there are not constructors yet by this point, which can happen,
1036
      // e.g. for unimplemented types that have no variables in the argument
1037
      // list of the function-to-synthesize, create a fresh ground term
1038
      sdts[i].addConstructor(types[i].mkGroundTerm(), "", {});
1039
    }
1040
1041
    // always add ITE
1042
604
    Kind k = ITE;
1043
604
    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
1044
1208
    std::vector<TypeNode> cargsIte;
1045
604
    cargsIte.push_back(unres_bt);
1046
604
    cargsIte.push_back(unres_t);
1047
604
    cargsIte.push_back(unres_t);
1048
604
    sdts[i].addConstructor(k, cargsIte);
1049
  }
1050
584
  std::map<TypeNode, std::pair<unsigned, bool>>::iterator itgat;
1051
  // initialize the datatypes (except for the last one, reserved for Bool)
1052
1188
  for (unsigned i = 0, size = types.size() - 1; i < size; ++i)
1053
  {
1054
604
    sdts[i].d_sdt.initializeDatatype(types[i], bvl, true, true);
1055
1208
    Trace("sygus-grammar-def")
1056
604
        << "...built datatype " << sdts[i].d_sdt.getDatatype() << " ";
1057
    //set start index if applicable
1058
604
    if( types[i]==range ){
1059
415
      startIndex = i;
1060
    }
1061
604
    itgat = typeToGAnyTerm.find(types[i]);
1062
604
    if (itgat == typeToGAnyTerm.end())
1063
    {
1064
      // no any term datatype, we are done
1065
596
      continue;
1066
    }
1067
8
    unsigned iat = itgat->second.first;
1068
16
    Trace("sygus-grammar-def")
1069
8
        << "Build any-term datatype for " << types[i] << "..." << std::endl;
1070
1071
    // for now, only real has any term construction
1072
8
    Assert(types[i].isReal());
1073
    // We have initialized the given type sdts[i], which should now contain
1074
    // a constructor for each relevant arithmetic term/variable. We now
1075
    // construct a sygus datatype of one of the following two forms.
1076
    //
1077
    // (1) The "sum of monomials" grammar:
1078
    //   I -> C*x1 | ... | C*xn | C | I + I | ite( B, I, I )
1079
    //   C -> any_constant
1080
    // where x1, ..., xn are the arithmetic terms/variables (non-arithmetic
1081
    // builtin operators) terms we have considered thus far.
1082
    //
1083
    // (2) The "polynomial" grammar:
1084
    //   I -> C*x1 + ... + C*xn + C | ite( B, I, I )
1085
    //   C -> any_constant
1086
    //
1087
    // The advantage of the first is that it allows for sums of terms
1088
    // constructible from other theories that share sorts with arithmetic, e.g.
1089
    //   c1*str.len(x) + c2*str.len(y)
1090
    // The advantage of the second is that there are fewer constructors, and
1091
    // hence may be more efficient.
1092
1093
    // Before proceeding, we build the any constant datatype
1094
16
    Trace("sygus-grammar-def")
1095
8
        << "Build any-constant datatype for " << types[i] << std::endl;
1096
16
    std::stringstream ss;
1097
8
    ss << fun << "_AnyConst";
1098
    // Make sygus datatype for any constant.
1099
16
    TypeNode unresAnyConst = mkUnresolvedType(ss.str(), unres);
1100
8
    unres_types.push_back(unresAnyConst);
1101
8
    sdts.push_back(SygusDatatypeGenerator(ss.str()));
1102
8
    sdts.back().d_sdt.addAnyConstantConstructor(types[i]);
1103
8
    sdts.back().d_sdt.initializeDatatype(types[i], bvl, true, true);
1104
1105
    // Now get the reference to the sygus datatype at position i (important that
1106
    // this comes after the modification to sdts above, which may modify
1107
    // the references).
1108
8
    const SygusDatatype& sdti = sdts[i].d_sdt;
1109
    // whether we will use the polynomial grammar
1110
8
    bool polynomialGrammar =
1111
        sgcm == options::SygusGrammarConsMode::ANY_TERM_CONCISE;
1112
    // A set of constructor indices that will be used in the overall sum we
1113
    // are constructing; indices of constructors corresponding to builtin
1114
    // arithmetic operators will be excluded from this set.
1115
16
    std::set<unsigned> useConstructor;
1116
16
    Trace("sygus-grammar-def")
1117
16
        << "Look at operators, num = " << sdti.getNumConstructors() << "..."
1118
8
        << std::endl;
1119
62
    for (unsigned k = 0, ncons = sdti.getNumConstructors(); k < ncons; k++)
1120
    {
1121
54
      const SygusDatatypeConstructor& sdc = sdti.getConstructor(k);
1122
108
      Node sop = sdc.d_op;
1123
54
      bool isBuiltinArithOp = (sop.getKind() == CONST_RATIONAL);
1124
54
      bool hasExternalType = false;
1125
66
      for (unsigned j = 0, nargs = sdc.d_argTypes.size(); j < nargs; j++)
1126
      {
1127
        // Since we are accessing the fields of the sygus datatype, this
1128
        // already corresponds to the correct sygus datatype type.
1129
50
        TypeNode atype = sdc.d_argTypes[j];
1130
38
        if (atype == unres_types[i])
1131
        {
1132
          // It is recursive, thus is (likely) a builtin arithmetic operator
1133
          // as constructed above. It may also be an operator from another
1134
          // theory that has both an arithmetic return type and an arithmetic
1135
          // argument (e.g. str.indexof). In either case, we ignore it for the
1136
          // sake of well-foundedness.
1137
26
          isBuiltinArithOp = true;
1138
26
          break;
1139
        }
1140
12
        else if (atype != unres_bt)
1141
        {
1142
          // It is an external type. This is the case of an operator of another
1143
          // theory whose return type is arithmetic, e.g. select.
1144
4
          hasExternalType = true;
1145
        }
1146
      }
1147
54
      if (!isBuiltinArithOp)
1148
      {
1149
12
        useConstructor.insert(k);
1150
12
        if (hasExternalType)
1151
        {
1152
          // If we have an external term in the sum, e.g. select(A,i), we
1153
          // cannot use a fixed polynomial template. As mentioned above, we
1154
          // cannot use a polynomial grammar when external terms (those built
1155
          // from the symbols of other theories) are involved.
1156
8
          Trace("sygus-grammar-def")
1157
4
              << "Cannot use polynomial grammar due to " << sop << std::endl;
1158
4
          polynomialGrammar = false;
1159
        }
1160
      }
1161
    }
1162
16
    Trace("sygus-grammar-def")
1163
16
        << "Done look at operators, num = " << sdti.getNumConstructors()
1164
8
        << "..." << std::endl;
1165
    // we have now decided whether we will use sum-of-monomials or polynomial
1166
    // Now, extract the terms and set up the polynomial
1167
16
    std::vector<Node> sumChildren;
1168
16
    std::vector<TypeNode> cargsAnyTerm;
1169
16
    std::vector<Node> lambdaVars;
1170
62
    for (unsigned k = 0, ncons = sdti.getNumConstructors(); k < ncons; k++)
1171
    {
1172
54
      Trace("sygus-grammar-def") << "Process #" << k << std::endl;
1173
96
      if (useConstructor.find(k) == useConstructor.end())
1174
      {
1175
42
        Trace("sygus-grammar-def") << "Skip variable #" << k << std::endl;
1176
        // builtin operator, as computed above, we skip
1177
42
        continue;
1178
      }
1179
12
      const SygusDatatypeConstructor& sdc = sdti.getConstructor(k);
1180
24
      Node sop = sdc.d_op;
1181
24
      Trace("sygus-grammar-def")
1182
12
          << "Monomial variable: #" << k << ": " << sop << std::endl;
1183
12
      unsigned nargs = sdc.d_argTypes.size();
1184
24
      std::vector<TypeNode> opCArgs;
1185
24
      std::vector<Node> opLArgs;
1186
12
      if (nargs > 0)
1187
      {
1188
        // Take its arguments. For example, if we are building a polynomial
1189
        // over str.len(s), then our any term constructor would include an
1190
        // argument of string type, e.g.:
1191
        //   (lambda s : String, c1, c2 : Int. c1*len(s) + c2)
1192
8
        for (unsigned j = 0; j < nargs; j++)
1193
        {
1194
          // this is already corresponds to the correct sygus datatype type
1195
8
          TypeNode atype = sdc.d_argTypes[j];
1196
4
          opCArgs.push_back(atype);
1197
          // get the builtin type
1198
8
          TypeNode btype = sygus_to_builtin[atype];
1199
4
          opLArgs.push_back(nm->mkBoundVar(btype));
1200
        }
1201
        // Do beta reduction on the operator so that its arguments match the
1202
        // fresh variables of the lambda (op) we are constructing below.
1203
4
        sop = datatypes::utils::mkSygusTerm(sop, opLArgs);
1204
4
        sop = Rewriter::rewrite(sop);
1205
      }
1206
12
      opCArgs.push_back(unresAnyConst);
1207
24
      Node coeff = nm->mkBoundVar(types[i]);
1208
12
      opLArgs.push_back(coeff);
1209
24
      Node monomial = nm->mkNode(MULT, coeff, sop);
1210
12
      if (polynomialGrammar)
1211
      {
1212
        // add the monomial c*t to the sum
1213
8
        sumChildren.push_back(monomial);
1214
8
        lambdaVars.insert(lambdaVars.end(), opLArgs.begin(), opLArgs.end());
1215
8
        cargsAnyTerm.insert(cargsAnyTerm.end(), opCArgs.begin(), opCArgs.end());
1216
      }
1217
      else
1218
      {
1219
        Node op =
1220
8
            nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, opLArgs), monomial);
1221
        // add it as a constructor
1222
8
        std::stringstream ssop;
1223
4
        ssop << "monomial_" << sdc.d_name;
1224
        // we use 0 as the weight, since this constructor should be seen as
1225
        // a generalization of a non-Boolean variable (which has weight 0).
1226
        // This ensures that e.g. ( c1*x >= 0 ) has the same weight as
1227
        // ( x >= 0 ).
1228
4
        sdts[iat].d_sdt.addConstructor(op, ssop.str(), opCArgs, 0);
1229
      }
1230
    }
1231
8
    if (polynomialGrammar)
1232
    {
1233
      // add the constant
1234
8
      Node coeff = nm->mkBoundVar(types[i]);
1235
4
      lambdaVars.push_back(coeff);
1236
4
      sumChildren.push_back(coeff);
1237
4
      cargsAnyTerm.push_back(unresAnyConst);
1238
      // make the sygus operator lambda X. c1*t1 + ... + cn*tn + c
1239
4
      Assert(sumChildren.size() > 1);
1240
8
      Node ops = nm->mkNode(PLUS, sumChildren);
1241
8
      Node op = nm->mkNode(LAMBDA, nm->mkNode(BOUND_VAR_LIST, lambdaVars), ops);
1242
4
      Trace("sygus-grammar-def") << "any term operator is " << op << std::endl;
1243
      // make the any term datatype, add to back
1244
      // do not consider the exclusion criteria of the generator
1245
      // we use 0 as the weight, since this constructor should be seen as
1246
      // a simultaneous generalization of set of non-Boolean variables.
1247
      // This ensures that ( c1*x + c2*y >= 0 ) has the same weight as
1248
      // e.g. ( x >= 0 ) or ( y >= 0 ).
1249
4
      sdts[iat].d_sdt.addConstructor(op, "polynomial", cargsAnyTerm, 0);
1250
      // mark that predicates should be of the form (= pol 0) and (<= pol 0)
1251
4
      itgat->second.second = true;
1252
    }
1253
    else
1254
    {
1255
      // add the any constant constructor as a separate constructor
1256
4
      sdts[iat].d_sdt.addAnyConstantConstructor(types[i]);
1257
      // add plus
1258
8
      std::vector<TypeNode> cargsPlus;
1259
4
      cargsPlus.push_back(unres_types[iat]);
1260
4
      cargsPlus.push_back(unres_types[iat]);
1261
4
      sdts[iat].d_sdt.addConstructor(PLUS, cargsPlus);
1262
    }
1263
    // add the ITE, regardless of sum-of-monomials vs polynomial
1264
16
    std::vector<TypeNode> cargsIte;
1265
8
    cargsIte.push_back(unres_bt);
1266
8
    cargsIte.push_back(unres_types[iat]);
1267
8
    cargsIte.push_back(unres_types[iat]);
1268
8
    sdts[iat].d_sdt.addConstructor(ITE, cargsIte);
1269
8
    sdts[iat].d_sdt.initializeDatatype(types[i], bvl, true, true);
1270
16
    Trace("sygus-grammar-def")
1271
8
        << "...built datatype " << sdts[iat].d_sdt.getDatatype() << std::endl;
1272
    // if the type is range, use it as the default type
1273
8
    if (types[i] == range)
1274
    {
1275
8
      startIndex = iat;
1276
    }
1277
  }
1278
  //------ make Boolean type
1279
584
  SygusDatatypeGenerator& sdtBool = sdts[boolIndex];
1280
584
  Trace("sygus-grammar-def") << "Make grammar for " << bool_type << std::endl;
1281
  //add variables
1282
1562
  for (unsigned i = 0, size = sygus_vars.size(); i < size; ++i)
1283
  {
1284
978
    if( sygus_vars[i].getType().isBoolean() ){
1285
426
      std::stringstream ss;
1286
213
      ss << sygus_vars[i];
1287
213
      Trace("sygus-grammar-def") << "...add for variable " << ss.str() << std::endl;
1288
426
      std::vector<TypeNode> cargsEmpty;
1289
      // make boolean variables weight as non-nullary constructors
1290
213
      sdtBool.addConstructor(sygus_vars[i], ss.str(), cargsEmpty, 1);
1291
    }
1292
  }
1293
  // add constants
1294
1168
  std::vector<Node> consts;
1295
584
  mkSygusConstantsForType(bool_type, consts);
1296
1752
  for (unsigned i = 0, size = consts.size(); i < size; ++i)
1297
  {
1298
2336
    std::stringstream ss;
1299
1168
    ss << consts[i];
1300
2336
    Trace("sygus-grammar-def") << "...add for constant " << ss.str()
1301
1168
                               << std::endl;
1302
2336
    std::vector<TypeNode> cargsEmpty;
1303
1168
    sdtBool.addConstructor(consts[i], ss.str(), cargsEmpty);
1304
  }
1305
  // add predicates for non-Boolean types
1306
1188
  for (unsigned i = 0, size = types.size() - 1; i < size; ++i)
1307
  {
1308
604
    if (!types[i].isFirstClass())
1309
    {
1310
      continue;
1311
    }
1312
604
    unsigned iuse = i;
1313
604
    bool zarg = false;
1314
    // use the any-term type if it exists and a zero argument if it is a
1315
    // polynomial grammar
1316
604
    itgat = typeToGAnyTerm.find(types[i]);
1317
604
    if (itgat != typeToGAnyTerm.end())
1318
    {
1319
8
      iuse = itgat->second.first;
1320
8
      zarg = itgat->second.second;
1321
16
      Trace("sygus-grammar-def")
1322
8
          << "...unres type " << unres_types[i] << " became "
1323
16
          << (!zarg ? "polynomial " : "") << "unres anyterm type "
1324
8
          << unres_types[iuse] << "\n";
1325
    }
1326
604
    Trace("sygus-grammar-def") << "...add predicates for " << types[i] << std::endl;
1327
    //add equality per type
1328
604
    Kind k = EQUAL;
1329
604
    Trace("sygus-grammar-def") << "...add for " << k << std::endl;
1330
1208
    std::stringstream ss;
1331
1208
    std::vector<TypeNode> cargs;
1332
604
    cargs.push_back(unres_types[iuse]);
1333
    // if polynomial grammar, generate (= anyterm 0) and (<= anyterm 0) as the
1334
    // predicates
1335
604
    if (zarg)
1336
    {
1337
8
      Node op = createLambdaWithZeroArg(k, types[i]);
1338
4
      ss << "eq_" << types[i];
1339
4
      sdtBool.addConstructor(op, ss.str(), cargs);
1340
    }
1341
    else
1342
    {
1343
600
      ss << kindToString(k) << "_" << types[i];
1344
600
      cargs.push_back(unres_types[iuse]);
1345
600
      sdtBool.addConstructor(nm->operatorOf(k), ss.str(), cargs);
1346
600
      cargs.pop_back();
1347
    }
1348
    // type specific predicates
1349
1208
    std::stringstream ssop;
1350
604
    if (types[i].isReal())
1351
    {
1352
468
      Kind kind = LEQ;
1353
468
      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
1354
468
      if (zarg)
1355
      {
1356
8
        Node op = createLambdaWithZeroArg(kind, types[i]);
1357
4
        ssop << "leq_" << types[i];
1358
4
        sdtBool.addConstructor(op, ssop.str(), cargs);
1359
      }
1360
      else
1361
      {
1362
464
        cargs.push_back(unres_types[iuse]);
1363
464
        sdtBool.addConstructor(kind, cargs);
1364
      }
1365
    }
1366
136
    else if (types[i].isBitVector())
1367
    {
1368
41
      Kind kind = BITVECTOR_ULT;
1369
41
      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
1370
41
      if (zarg)
1371
      {
1372
        Node op = createLambdaWithZeroArg(kind, types[i]);
1373
        ssop << "leq_" << types[i];
1374
        sdtBool.addConstructor(op, ssop.str(), cargs);
1375
      }
1376
      else
1377
      {
1378
41
        cargs.push_back(unres_types[iuse]);
1379
41
        sdtBool.addConstructor(kind, cargs);
1380
      }
1381
    }
1382
95
    else if (types[i].isFloatingPoint())
1383
    {
1384
      Trace("sygus-grammar-def") << "...add FP predicates" << std::endl;
1385
      std::vector<Kind> fp_unary_predicates = {FLOATINGPOINT_ISN,
1386
                                               FLOATINGPOINT_ISSN,
1387
                                               FLOATINGPOINT_ISZ,
1388
                                               FLOATINGPOINT_ISINF,
1389
                                               FLOATINGPOINT_ISNAN,
1390
                                               FLOATINGPOINT_ISNEG,
1391
                                               FLOATINGPOINT_ISPOS};
1392
      for (const Kind kind : fp_unary_predicates)
1393
      {
1394
        sdtBool.addConstructor(kind, cargs);
1395
      }
1396
      std::vector<Kind> fp_binary_predicates = {FLOATINGPOINT_LEQ,
1397
                                                FLOATINGPOINT_LT};
1398
      cargs.push_back(unres_types[iuse]);
1399
      for (const Kind kind : fp_binary_predicates)
1400
      {
1401
        sdtBool.addConstructor(kind, cargs);
1402
      }
1403
    }
1404
95
    else if (types[i].isDatatype())
1405
    {
1406
      //add for testers
1407
27
      Trace("sygus-grammar-def") << "...add for testers" << std::endl;
1408
27
      const DType& dt = types[i].getDType();
1409
54
      std::vector<TypeNode> cargsTester;
1410
27
      cargsTester.push_back(unres_types[iuse]);
1411
63
      for (unsigned kind = 0, size_k = dt.getNumConstructors(); kind < size_k;
1412
           ++kind)
1413
      {
1414
72
        Trace("sygus-grammar-def")
1415
36
            << "...for " << dt[kind].getTester() << std::endl;
1416
72
        std::stringstream sst;
1417
36
        sst << dt[kind].getTester();
1418
36
        sdtBool.addConstructor(dt[kind].getTester(), sst.str(), cargsTester);
1419
      }
1420
    }
1421
68
    else if (types[i].isSet())
1422
    {
1423
      // add for member
1424
16
      TypeNode etype = types[i].getSetElementType();
1425
8
      Assert(type_to_unres.find(etype) != type_to_unres.end());
1426
16
      TypeNode unresElemType = type_to_unres[etype];
1427
16
      std::vector<TypeNode> cargsMember;
1428
8
      cargsMember.push_back(unresElemType);
1429
8
      cargsMember.push_back(unres_types[iuse]);
1430
8
      Trace("sygus-grammar-def") << "...for MEMBER" << std::endl;
1431
8
      sdtBool.addConstructor(MEMBER, cargsMember);
1432
    }
1433
  }
1434
  // add Boolean connectives, if not in a degenerate case of (recursively)
1435
  // having only constant constructors
1436
1168
  Trace("sygus-grammar-def")
1437
584
      << "...add Boolean connectives for unres type " << unres_bt << std::endl;
1438
584
  if (sdtBool.d_sdt.getNumConstructors() > consts.size())
1439
  {
1440
2520
    for (unsigned i = 0; i < 4; i++)
1441
    {
1442
2016
      Kind k = i == 0 ? NOT : (i == 1 ? AND : (i == 2 ? OR : ITE));
1443
      // TODO #1935 ITEs are added to Boolean grammars so that we can infer
1444
      // unification strategies. We can do away with this if we can infer
1445
      // unification strategies from and/or/not
1446
2016
      if (k == ITE && options::sygusUnifPi() == options::SygusUnifPiMode::NONE)
1447
      {
1448
494
        continue;
1449
      }
1450
1522
      Trace("sygus-grammar-def") << "...add for " << k << std::endl;
1451
3044
      std::vector<TypeNode> cargs;
1452
1522
      cargs.push_back(unres_bt);
1453
1522
      if (k != NOT)
1454
      {
1455
1018
        cargs.push_back(unres_bt);
1456
1018
        if (k == ITE)
1457
        {
1458
10
          cargs.push_back(unres_bt);
1459
        }
1460
      }
1461
1522
      sdtBool.addConstructor(k, cargs);
1462
    }
1463
  }
1464
584
  if (range == bool_type)
1465
  {
1466
169
    startIndex = boolIndex;
1467
  }
1468
584
  sdtBool.d_sdt.initializeDatatype(bool_type, bvl, true, true);
1469
1168
  Trace("sygus-grammar-def")
1470
584
      << "...built datatype for Bool " << sdtBool.d_sdt.getDatatype() << " ";
1471
584
  Trace("sygus-grammar-def") << "...finished make default grammar for " << fun << " " << range << std::endl;
1472
  // make first datatype be the top level datatype
1473
584
  if( startIndex>0 ){
1474
230
    SygusDatatypeGenerator tmp_dt = sdts[0];
1475
115
    sdts[0] = sdts[startIndex];
1476
115
    sdts[startIndex] = tmp_dt;
1477
  }
1478
584
}
1479
1480
584
TypeNode CegGrammarConstructor::mkSygusDefaultType(
1481
    TypeNode range,
1482
    Node bvl,
1483
    const std::string& fun,
1484
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>& extra_cons,
1485
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
1486
        exclude_cons,
1487
    std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>&
1488
        include_cons,
1489
    std::unordered_set<Node, NodeHashFunction>& term_irrelevant)
1490
{
1491
584
  Trace("sygus-grammar-def") << "*** Make sygus default type " << range << ", make datatypes..." << std::endl;
1492
203
  for (std::map<TypeNode, std::unordered_set<Node, NodeHashFunction>>::iterator
1493
584
           it = extra_cons.begin();
1494
787
       it != extra_cons.end();
1495
       ++it)
1496
  {
1497
203
    Trace("sygus-grammar-def") << "    ...using " << it->second.size() << " extra constants for " << it->first << std::endl;
1498
  }
1499
1168
  std::set<TypeNode> unres;
1500
1168
  std::vector<SygusDatatypeGenerator> sdts;
1501
584
  mkSygusDefaultGrammar(range,
1502
                        bvl,
1503
                        fun,
1504
                        extra_cons,
1505
                        exclude_cons,
1506
                        include_cons,
1507
                        term_irrelevant,
1508
                        sdts,
1509
                        unres);
1510
  // extract the datatypes from the sygus datatype generator objects
1511
1168
  std::vector<DType> datatypes;
1512
1832
  for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
1513
  {
1514
1248
    datatypes.push_back(sdts[i].d_sdt.getDatatype());
1515
  }
1516
584
  Trace("sygus-grammar-def")  << "...made " << datatypes.size() << " datatypes, now make mutual datatype types..." << std::endl;
1517
584
  Assert(!datatypes.empty());
1518
  std::vector<TypeNode> types = NodeManager::currentNM()->mkMutualDatatypeTypes(
1519
1168
      datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
1520
584
  Trace("sygus-grammar-def") << "...finished" << std::endl;
1521
584
  Assert(types.size() == datatypes.size());
1522
1168
  return types[0];
1523
}
1524
1525
TypeNode CegGrammarConstructor::mkSygusTemplateTypeRec( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl,
1526
                                              const std::string& fun, unsigned& tcount ) {
1527
  if( templ==templ_arg ){
1528
    //Assert( templ_arg.getType()==sygusToBuiltinType( templ_arg_sygus_type ) );
1529
    return templ_arg_sygus_type;
1530
  }else{
1531
    tcount++;
1532
    std::set<TypeNode> unres;
1533
    std::vector<SygusDatatype> sdts;
1534
    std::stringstream ssd;
1535
    ssd << fun << "_templ_" << tcount;
1536
    std::string dbname = ssd.str();
1537
    sdts.push_back(SygusDatatype(dbname));
1538
    Node op;
1539
    std::vector<TypeNode> argTypes;
1540
    if( templ.getNumChildren()==0 ){
1541
      // TODO : can short circuit to this case when !TermUtil::containsTerm( templ, templ_arg )
1542
      op = templ;
1543
    }else{
1544
      Assert(templ.hasOperator());
1545
      op = templ.getOperator();
1546
      // make constructor taking arguments types from children
1547
      for( unsigned i=0; i<templ.getNumChildren(); i++ ){
1548
        //recursion depth bound by the depth of SyGuS template expressions (low)
1549
        TypeNode tnc = mkSygusTemplateTypeRec( templ[i], templ_arg, templ_arg_sygus_type, bvl, fun, tcount );
1550
        argTypes.push_back(tnc);
1551
      }
1552
    }
1553
    std::stringstream ssdc;
1554
    ssdc << fun << "_templ_cons_" << tcount;
1555
    // we have a single sygus constructor that encodes the template
1556
    sdts.back().addConstructor(op, ssdc.str(), argTypes);
1557
    sdts.back().initializeDatatype(templ.getType(), bvl, true, true);
1558
    // extract the datatypes from the sygus datatype objects
1559
    std::vector<DType> datatypes;
1560
    for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
1561
    {
1562
      datatypes.push_back(sdts[i].getDatatype());
1563
    }
1564
    std::vector<TypeNode> types =
1565
        NodeManager::currentNM()->mkMutualDatatypeTypes(
1566
            datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
1567
    Assert(types.size() == 1);
1568
    return types[0];
1569
  }
1570
}
1571
1572
TypeNode CegGrammarConstructor::mkSygusTemplateType( Node templ, Node templ_arg, TypeNode templ_arg_sygus_type, Node bvl,
1573
                                                     const std::string& fun ) {
1574
  unsigned tcount = 0;
1575
  return mkSygusTemplateTypeRec( templ, templ_arg, templ_arg_sygus_type, bvl, fun, tcount );
1576
}
1577
1578
1248
CegGrammarConstructor::SygusDatatypeGenerator::SygusDatatypeGenerator(
1579
1248
    const std::string& name)
1580
1248
    : d_sdt(name)
1581
{
1582
1248
}
1583
8627
void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor(
1584
    Node op,
1585
    const std::string& name,
1586
    const std::vector<TypeNode>& consTypes,
1587
    int weight)
1588
{
1589
8627
  if (shouldInclude(op))
1590
  {
1591
8586
    d_sdt.addConstructor(op, name, consTypes, weight);
1592
  }
1593
8627
}
1594
4414
void CegGrammarConstructor::SygusDatatypeGenerator::addConstructor(
1595
    Kind k,
1596
    const std::vector<TypeNode>& consTypes,
1597
    int weight)
1598
{
1599
4414
  NodeManager* nm = NodeManager::currentNM();
1600
4414
  addConstructor(nm->operatorOf(k), kindToString(k), consTypes, weight);
1601
4414
}
1602
8627
bool CegGrammarConstructor::SygusDatatypeGenerator::shouldInclude(Node op) const
1603
{
1604
8627
  if (d_exclude_cons.find(op) != d_exclude_cons.end())
1605
  {
1606
    return false;
1607
  }
1608
8627
  if (!d_include_cons.empty())
1609
  {
1610
    // special case, variables and terms of certain types are always included
1611
60
    if (!op.isVar() && op.getType().getKind() == TYPE_CONSTANT)
1612
    {
1613
48
      if (d_include_cons.find(op) == d_include_cons.end())
1614
      {
1615
41
        return false;
1616
      }
1617
    }
1618
  }
1619
8586
  return true;
1620
}
1621
1622
}/* namespace CVC4::theory::quantifiers */
1623
}/* namespace CVC4::theory */
1624
26676
}/* namespace CVC4 */