GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/sygus_datatype_utils.cpp Lines: 324 377 85.9 %
Date: 2021-03-22 Branches: 661 1722 38.4 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file sygus_datatype_utils.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 rewriter for the theory of (co)inductive datatypes.
13
 **
14
 ** Implementation of rewriter for the theory of (co)inductive datatypes.
15
 **/
16
17
#include "theory/datatypes/sygus_datatype_utils.h"
18
19
#include <sstream>
20
21
#include "expr/dtype.h"
22
#include "expr/dtype_cons.h"
23
#include "expr/node_algorithm.h"
24
#include "expr/sygus_datatype.h"
25
#include "smt/smt_engine.h"
26
#include "smt/smt_engine_scope.h"
27
#include "theory/evaluator.h"
28
#include "theory/rewriter.h"
29
30
using namespace CVC4;
31
using namespace CVC4::kind;
32
33
namespace CVC4 {
34
namespace theory {
35
namespace datatypes {
36
namespace utils {
37
38
81473
Node applySygusArgs(const DType& dt,
39
                    Node op,
40
                    Node n,
41
                    const std::vector<Node>& args)
42
{
43
  // optimization: if n is just a sygus bound variable, return immediately
44
  // by replacing with the proper argument, or returning unchanged if it is
45
  // a bound variable not corresponding to a formal argument.
46
81473
  if (n.getKind() == BOUND_VARIABLE)
47
  {
48
1578
    if (n.hasAttribute(SygusVarNumAttribute()))
49
    {
50
1546
      int vn = n.getAttribute(SygusVarNumAttribute());
51
1546
      Assert(dt.getSygusVarList()[vn] == n);
52
1546
      return args[vn];
53
    }
54
    // it is a different bound variable, it is unchanged
55
32
    return n;
56
  }
57
  // n is an application of operator op.
58
  // We must compute the free variables in op to determine if there are
59
  // any substitutions we need to make to n.
60
159790
  TNode val;
61
79895
  if (!op.hasAttribute(SygusVarFreeAttribute()))
62
  {
63
1942
    std::unordered_set<Node, NodeHashFunction> fvs;
64
971
    if (expr::getFreeVariables(op, fvs))
65
    {
66
20
      if (fvs.size() == 1)
67
      {
68
20
        for (const Node& v : fvs)
69
        {
70
10
          val = v;
71
        }
72
      }
73
      else
74
      {
75
10
        val = op;
76
      }
77
    }
78
971
    Trace("dt-sygus-fv") << "Free var in " << op << " : " << val << std::endl;
79
971
    op.setAttribute(SygusVarFreeAttribute(), val);
80
  }
81
  else
82
  {
83
78924
    val = op.getAttribute(SygusVarFreeAttribute());
84
  }
85
79895
  if (val.isNull())
86
  {
87
78189
    return n;
88
  }
89
1706
  if (val.getKind() == BOUND_VARIABLE)
90
  {
91
    // single substitution case
92
1372
    int vn = val.getAttribute(SygusVarNumAttribute());
93
2744
    TNode sub = args[vn];
94
1372
    return n.substitute(val, sub);
95
  }
96
  // do the full substitution
97
668
  std::vector<Node> vars;
98
668
  Node bvl = dt.getSygusVarList();
99
1110
  for (unsigned i = 0, nvars = bvl.getNumChildren(); i < nvars; i++)
100
  {
101
776
    vars.push_back(bvl[i]);
102
  }
103
334
  return n.substitute(vars.begin(), vars.end(), args.begin(), args.end());
104
}
105
106
156
Kind getOperatorKindForSygusBuiltin(Node op)
107
{
108
156
  Assert(op.getKind() != BUILTIN);
109
156
  if (op.getKind() == LAMBDA)
110
  {
111
    return APPLY_UF;
112
  }
113
156
  return NodeManager::getKindForFunction(op);
114
}
115
116
struct SygusOpRewrittenAttributeId
117
{
118
};
119
typedef expr::Attribute<SygusOpRewrittenAttributeId, Node>
120
    SygusOpRewrittenAttribute;
121
122
236096
Kind getEliminateKind(Kind ok)
123
{
124
236096
  Kind nk = ok;
125
  // We also must ensure that builtin operators which are eliminated
126
  // during expand definitions are replaced by the proper operator.
127
236096
  if (ok == DIVISION)
128
  {
129
70
    nk = DIVISION_TOTAL;
130
  }
131
236026
  else if (ok == INTS_DIVISION)
132
  {
133
1
    nk = INTS_DIVISION_TOTAL;
134
  }
135
236025
  else if (ok == INTS_MODULUS)
136
  {
137
5
    nk = INTS_MODULUS_TOTAL;
138
  }
139
236096
  return nk;
140
}
141
142
3010
Node eliminatePartialOperators(Node n)
143
{
144
3010
  NodeManager* nm = NodeManager::currentNM();
145
6020
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
146
3010
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
147
6020
  std::vector<TNode> visit;
148
6020
  TNode cur;
149
3010
  visit.push_back(n);
150
22662
  do
151
  {
152
25672
    cur = visit.back();
153
25672
    visit.pop_back();
154
25672
    it = visited.find(cur);
155
156
25672
    if (it == visited.end())
157
    {
158
11231
      visited[cur] = Node::null();
159
11231
      visit.push_back(cur);
160
22662
      for (const Node& cn : cur)
161
      {
162
11431
        visit.push_back(cn);
163
      }
164
    }
165
14441
    else if (it->second.isNull())
166
    {
167
22462
      Node ret = cur;
168
11231
      bool childChanged = false;
169
22462
      std::vector<Node> children;
170
11231
      if (cur.getMetaKind() == metakind::PARAMETERIZED)
171
      {
172
233
        children.push_back(cur.getOperator());
173
      }
174
22662
      for (const Node& cn : cur)
175
      {
176
11431
        it = visited.find(cn);
177
11431
        Assert(it != visited.end());
178
11431
        Assert(!it->second.isNull());
179
11431
        childChanged = childChanged || cn != it->second;
180
11431
        children.push_back(it->second);
181
      }
182
11231
      Kind ok = cur.getKind();
183
11231
      Kind nk = getEliminateKind(ok);
184
11231
      if (nk != ok || childChanged)
185
      {
186
12
        ret = nm->mkNode(nk, children);
187
      }
188
11231
      visited[cur] = ret;
189
    }
190
25672
  } while (!visit.empty());
191
3010
  Assert(visited.find(n) != visited.end());
192
3010
  Assert(!visited.find(n)->second.isNull());
193
6020
  return visited[n];
194
}
195
196
704521
Node mkSygusTerm(const DType& dt,
197
                 unsigned i,
198
                 const std::vector<Node>& children,
199
                 bool doBetaReduction,
200
                 bool isExternal)
201
{
202
1409042
  Trace("dt-sygus-util") << "Make sygus term " << dt.getName() << "[" << i
203
704521
                         << "] with children: " << children << std::endl;
204
704521
  Assert(i < dt.getNumConstructors());
205
704521
  Assert(dt.isSygus());
206
704521
  Assert(!dt[i].getSygusOp().isNull());
207
1409042
  Node op = dt[i].getSygusOp();
208
1409042
  Node opn = op;
209
704521
  if (!isExternal)
210
  {
211
    // Get the normalized version of the sygus operator. We do this by
212
    // expanding definitions, rewriting it, and eliminating partial operators.
213
698706
    if (!op.hasAttribute(SygusOpRewrittenAttribute()))
214
    {
215
227875
      if (op.isConst())
216
      {
217
        // If it is a builtin operator, convert to total version if necessary.
218
        // First, get the kind for the operator.
219
224865
        Kind ok = NodeManager::operatorToKind(op);
220
449730
        Trace("sygus-grammar-normalize-debug")
221
224865
            << "...builtin kind is " << ok << std::endl;
222
224865
        Kind nk = getEliminateKind(ok);
223
224865
        if (nk != ok)
224
        {
225
140
          Trace("sygus-grammar-normalize-debug")
226
70
              << "...replace by builtin operator " << nk << std::endl;
227
70
          opn = NodeManager::currentNM()->operatorOf(nk);
228
        }
229
      }
230
      else
231
      {
232
        // Only expand definitions if the operator is not constant, since
233
        // calling expandDefinitions on them should be a no-op. This check
234
        // ensures we don't try to expand e.g. bitvector extract operators,
235
        // whose type is undefined, and thus should not be passed to
236
        // expandDefinitions.
237
3010
        opn = smt::currentSmtEngine()->expandDefinitions(op);
238
3010
        opn = Rewriter::rewrite(opn);
239
3010
        opn = eliminatePartialOperators(opn);
240
        SygusOpRewrittenAttribute sora;
241
3010
        op.setAttribute(sora, opn);
242
      }
243
    }
244
    else
245
    {
246
470831
      opn = op.getAttribute(SygusOpRewrittenAttribute());
247
    }
248
  }
249
1409042
  return mkSygusTerm(opn, children, doBetaReduction);
250
}
251
252
704525
Node mkSygusTerm(Node op,
253
                 const std::vector<Node>& children,
254
                 bool doBetaReduction)
255
{
256
704525
  Trace("dt-sygus-util") << "Operator is " << op << std::endl;
257
704525
  if (children.empty())
258
  {
259
    // no children, return immediately
260
167376
    Trace("dt-sygus-util") << "...return direct op" << std::endl;
261
167376
    return op;
262
  }
263
  // if it is the any constant, we simply return the child
264
537149
  if (op.getAttribute(SygusAnyConstAttribute()))
265
  {
266
494
    Assert(children.size() == 1);
267
494
    return children[0];
268
  }
269
1073310
  std::vector<Node> schildren;
270
  // get the kind of the operator
271
536655
  Kind ok = op.getKind();
272
536655
  if (ok != BUILTIN)
273
  {
274
471020
    if (ok == LAMBDA && doBetaReduction)
275
    {
276
      // Do immediate beta reduction. It suffices to use a normal substitution
277
      // since neither op nor children have quantifiers, since they are
278
      // generated by sygus grammars.
279
938364
      std::vector<Node> vars{op[0].begin(), op[0].end()};
280
469182
      Assert(vars.size() == children.size());
281
      Node ret = op[1].substitute(
282
938364
          vars.begin(), vars.end(), children.begin(), children.end());
283
469182
      Trace("dt-sygus-util") << "...return (beta-reduce) " << ret << std::endl;
284
469182
      return ret;
285
    }
286
    else
287
    {
288
1838
      schildren.push_back(op);
289
    }
290
  }
291
67473
  schildren.insert(schildren.end(), children.begin(), children.end());
292
134946
  Node ret;
293
67473
  if (ok == BUILTIN)
294
  {
295
65635
    ret = NodeManager::currentNM()->mkNode(op, schildren);
296
65635
    Trace("dt-sygus-util") << "...return (builtin) " << ret << std::endl;
297
65635
    return ret;
298
  }
299
  // get the kind used for applying op
300
1838
  Kind otk = NodeManager::operatorToKind(op);
301
1838
  Trace("dt-sygus-util") << "operator kind is " << otk << std::endl;
302
1838
  if (otk != UNDEFINED_KIND)
303
  {
304
    // If it is an APPLY_UF operator, we should have at least an operator and
305
    // a child.
306
1682
    Assert(otk != APPLY_UF || schildren.size() != 1);
307
1682
    ret = NodeManager::currentNM()->mkNode(otk, schildren);
308
1682
    Trace("dt-sygus-util") << "...return (op) " << ret << std::endl;
309
1682
    return ret;
310
  }
311
156
  Kind tok = getOperatorKindForSygusBuiltin(op);
312
156
  if (schildren.size() == 1 && tok == UNDEFINED_KIND)
313
  {
314
    ret = schildren[0];
315
  }
316
  else
317
  {
318
156
    ret = NodeManager::currentNM()->mkNode(tok, schildren);
319
  }
320
156
  Trace("dt-sygus-util") << "...return " << ret << std::endl;
321
156
  return ret;
322
}
323
324
struct SygusToBuiltinTermAttributeId
325
{
326
};
327
typedef expr::Attribute<SygusToBuiltinTermAttributeId, Node>
328
    SygusToBuiltinTermAttribute;
329
330
// A variant of the above attribute for cases where we introduce a fresh
331
// variable. This is to support sygusToBuiltin on non-constant sygus terms,
332
// where sygus variables should be mapped to canonical builtin variables.
333
// It is important to cache this so that sygusToBuiltin is deterministic.
334
struct SygusToBuiltinVarAttributeId
335
{
336
};
337
typedef expr::Attribute<SygusToBuiltinVarAttributeId, Node>
338
    SygusToBuiltinVarAttribute;
339
340
// A variant of the above attribute for cases where we introduce a fresh
341
// variable. This is to support sygusToBuiltin on non-constant sygus terms,
342
// where sygus variables should be mapped to canonical builtin variables.
343
// It is important to cache this so that sygusToBuiltin is deterministic.
344
struct BuiltinVarToSygusAttributeId
345
{
346
};
347
typedef expr::Attribute<BuiltinVarToSygusAttributeId, Node>
348
    BuiltinVarToSygusAttribute;
349
350
329417
Node sygusToBuiltin(Node n, bool isExternal)
351
{
352
658834
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
353
329417
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
354
658834
  std::vector<TNode> visit;
355
658834
  TNode cur;
356
  unsigned index;
357
329417
  visit.push_back(n);
358
220364
  do
359
  {
360
549781
    cur = visit.back();
361
549781
    visit.pop_back();
362
549781
    it = visited.find(cur);
363
549781
    if (it == visited.end())
364
    {
365
      // Notice this condition succeeds in roughly 99% of the executions of this
366
      // method (based on our coverage tests), hence the else if / else cases
367
      // below do not significantly impact performance.
368
466947
      if (cur.getKind() == APPLY_CONSTRUCTOR)
369
      {
370
466653
        if (!isExternal && cur.hasAttribute(SygusToBuiltinTermAttribute()))
371
        {
372
388404
          visited[cur] = cur.getAttribute(SygusToBuiltinTermAttribute());
373
        }
374
        else
375
        {
376
78249
          visited[cur] = Node::null();
377
78249
          visit.push_back(cur);
378
220364
          for (const Node& cn : cur)
379
          {
380
142115
            visit.push_back(cn);
381
          }
382
        }
383
      }
384
294
      else if (cur.getType().isSygusDatatype())
385
      {
386
        Assert (cur.isVar());
387
        if (cur.hasAttribute(SygusToBuiltinVarAttribute()))
388
        {
389
          // use the previously constructed variable for it
390
          visited[cur] = cur.getAttribute(SygusToBuiltinVarAttribute());
391
        }
392
        else
393
        {
394
          std::stringstream ss;
395
          ss << cur;
396
          const DType& dt = cur.getType().getDType();
397
          // make a fresh variable
398
          NodeManager * nm = NodeManager::currentNM();
399
          Node var = nm->mkBoundVar(ss.str(), dt.getSygusType());
400
          SygusToBuiltinVarAttribute stbv;
401
          cur.setAttribute(stbv, var);
402
          visited[cur] = var;
403
          // create backwards mapping
404
          BuiltinVarToSygusAttribute bvtsa;
405
          var.setAttribute(bvtsa, cur);
406
        }
407
      }
408
      else
409
      {
410
        // non-datatypes are themselves
411
294
        visited[cur] = cur;
412
      }
413
    }
414
82834
    else if (it->second.isNull())
415
    {
416
156498
      Node ret = cur;
417
78249
      Assert(cur.getKind() == APPLY_CONSTRUCTOR);
418
78249
      const DType& dt = cur.getType().getDType();
419
      // Non sygus-datatype terms are also themselves. Notice we treat the
420
      // case of non-sygus datatypes this way since it avoids computing
421
      // the type / datatype of the node in the pre-traversal above. The
422
      // case of non-sygus datatypes is very rare, so the extra addition to
423
      // visited is justified performance-wise.
424
78249
      if (dt.isSygus())
425
      {
426
156498
        std::vector<Node> children;
427
220364
        for (const Node& cn : cur)
428
        {
429
142115
          it = visited.find(cn);
430
142115
          Assert(it != visited.end());
431
142115
          Assert(!it->second.isNull());
432
142115
          children.push_back(it->second);
433
        }
434
78249
        index = indexOf(cur.getOperator());
435
78249
        ret = mkSygusTerm(dt, index, children, true, isExternal);
436
      }
437
78249
      visited[cur] = ret;
438
      // cache
439
78249
      if (!isExternal)
440
      {
441
        SygusToBuiltinTermAttribute stbt;
442
72434
        cur.setAttribute(stbt, ret);
443
      }
444
    }
445
549781
  } while (!visit.empty());
446
329417
  Assert(visited.find(n) != visited.end());
447
329417
  Assert(!visited.find(n)->second.isNull());
448
658834
  return visited[n];
449
}
450
451
77205
Node sygusToBuiltinEval(Node n, const std::vector<Node>& args)
452
{
453
77205
  NodeManager* nm = NodeManager::currentNM();
454
  Evaluator eval;
455
  // constant arguments?
456
77205
  bool constArgs = true;
457
728423
  for (const Node& a : args)
458
  {
459
658265
    if (!a.isConst())
460
    {
461
7047
      constArgs = false;
462
7047
      break;
463
    }
464
  }
465
154410
  std::vector<Node> eargs;
466
77205
  bool svarsInit = false;
467
154410
  std::vector<Node> svars;
468
154410
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
469
77205
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
470
154410
  std::vector<TNode> visit;
471
154410
  TNode cur;
472
  unsigned index;
473
77205
  visit.push_back(n);
474
29697
  do
475
  {
476
106902
    cur = visit.back();
477
106902
    visit.pop_back();
478
106902
    it = visited.find(cur);
479
106902
    if (it == visited.end())
480
    {
481
192774
      TypeNode tn = cur.getType();
482
96387
      if (!tn.isDatatype() || !tn.getDType().isSygus())
483
      {
484
32
        visited[cur] = cur;
485
      }
486
96355
      else if (cur.isConst())
487
      {
488
        // convert to builtin term
489
157338
        Node bt = sygusToBuiltin(cur);
490
        // run the evaluator if possible
491
78669
        if (!svarsInit)
492
        {
493
77011
          svarsInit = true;
494
154022
          TypeNode type = cur.getType();
495
154022
          Node varList = type.getDType().getSygusVarList();
496
745996
          for (const Node& v : varList)
497
          {
498
668985
            svars.push_back(v);
499
          }
500
        }
501
78669
        Assert(args.size() == svars.size());
502
        // try evaluation if we have constant arguments
503
157338
        Node ret = constArgs ? eval.eval(bt, svars, args) : Node::null();
504
78669
        if (ret.isNull())
505
        {
506
          // if evaluation was not available, use a substitution
507
7051
          ret = bt.substitute(
508
              svars.begin(), svars.end(), args.begin(), args.end());
509
        }
510
78669
        visited[cur] = ret;
511
      }
512
      else
513
      {
514
17686
        if (cur.getKind() == APPLY_CONSTRUCTOR)
515
        {
516
9883
          visited[cur] = Node::null();
517
9883
          visit.push_back(cur);
518
29697
          for (const Node& cn : cur)
519
          {
520
19814
            visit.push_back(cn);
521
          }
522
        }
523
        else
524
        {
525
          // it is the evaluation of this term on the arguments
526
7803
          if (eargs.empty())
527
          {
528
7463
            eargs.push_back(cur);
529
7463
            eargs.insert(eargs.end(), args.begin(), args.end());
530
          }
531
          else
532
          {
533
340
            eargs[0] = cur;
534
          }
535
7803
          visited[cur] = nm->mkNode(DT_SYGUS_EVAL, eargs);
536
        }
537
      }
538
    }
539
10515
    else if (it->second.isNull())
540
    {
541
19766
      Node ret = cur;
542
9883
      Assert(cur.getKind() == APPLY_CONSTRUCTOR);
543
9883
      const DType& dt = cur.getType().getDType();
544
      // non sygus-datatype terms are also themselves
545
9883
      if (dt.isSygus())
546
      {
547
19766
        std::vector<Node> children;
548
29697
        for (const Node& cn : cur)
549
        {
550
19814
          it = visited.find(cn);
551
19814
          Assert(it != visited.end());
552
19814
          Assert(!it->second.isNull());
553
19814
          children.push_back(it->second);
554
        }
555
9883
        index = indexOf(cur.getOperator());
556
        // apply to children, which constructs the builtin term
557
9883
        ret = mkSygusTerm(dt, index, children);
558
        // now apply it to arguments in args
559
9883
        ret = applySygusArgs(dt, dt[index].getSygusOp(), ret, args);
560
      }
561
9883
      visited[cur] = ret;
562
    }
563
106902
  } while (!visit.empty());
564
77205
  Assert(visited.find(n) != visited.end());
565
77205
  Assert(!visited.find(n)->second.isNull());
566
154410
  return visited[n];
567
}
568
569
Node builtinVarToSygus(Node v)
570
{
571
  BuiltinVarToSygusAttribute bvtsa;
572
  if (v.hasAttribute(bvtsa))
573
  {
574
    return v.getAttribute(bvtsa);
575
  }
576
  return Node::null();
577
}
578
579
void getFreeSymbolsSygusType(TypeNode sdt,
580
                             std::unordered_set<Node, NodeHashFunction>& syms)
581
{
582
  // datatype types we need to process
583
  std::vector<TypeNode> typeToProcess;
584
  // datatype types we have processed
585
  std::map<TypeNode, TypeNode> typesProcessed;
586
  typeToProcess.push_back(sdt);
587
  while (!typeToProcess.empty())
588
  {
589
    std::vector<TypeNode> typeNextToProcess;
590
    for (const TypeNode& curr : typeToProcess)
591
    {
592
      Assert(curr.isDatatype() && curr.getDType().isSygus());
593
      const DType& dtc = curr.getDType();
594
      for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
595
      {
596
        // collect the symbols from the operator
597
        Node op = dtc[j].getSygusOp();
598
        expr::getSymbols(op, syms);
599
        // traverse the argument types
600
        for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
601
        {
602
          TypeNode argt = dtc[j].getArgType(k);
603
          if (!argt.isDatatype() || !argt.getDType().isSygus())
604
          {
605
            // not a sygus datatype
606
            continue;
607
          }
608
          if (typesProcessed.find(argt) == typesProcessed.end())
609
          {
610
            typeNextToProcess.push_back(argt);
611
          }
612
        }
613
      }
614
    }
615
    typeToProcess.clear();
616
    typeToProcess.insert(typeToProcess.end(),
617
                         typeNextToProcess.begin(),
618
                         typeNextToProcess.end());
619
  }
620
}
621
622
9
TypeNode substituteAndGeneralizeSygusType(TypeNode sdt,
623
                                          const std::vector<Node>& syms,
624
                                          const std::vector<Node>& vars)
625
{
626
9
  NodeManager* nm = NodeManager::currentNM();
627
9
  const DType& sdtd = sdt.getDType();
628
  // compute the new formal argument list
629
18
  std::vector<Node> formalVars;
630
18
  Node prevVarList = sdtd.getSygusVarList();
631
9
  if (!prevVarList.isNull())
632
  {
633
    for (const Node& v : prevVarList)
634
    {
635
      // if it is not being replaced
636
      if (std::find(syms.begin(), syms.end(), v) != syms.end())
637
      {
638
        formalVars.push_back(v);
639
      }
640
    }
641
  }
642
45
  for (const Node& v : vars)
643
  {
644
36
    if (v.getKind() == BOUND_VARIABLE)
645
    {
646
36
      formalVars.push_back(v);
647
    }
648
  }
649
  // make the sygus variable list for the formal argument list
650
18
  Node abvl = nm->mkNode(BOUND_VAR_LIST, formalVars);
651
9
  Trace("sygus-abduct-debug") << "...finish" << std::endl;
652
653
  // must convert all constructors to version with variables in "vars"
654
18
  std::vector<SygusDatatype> sdts;
655
18
  std::set<TypeNode> unres;
656
657
9
  Trace("dtsygus-gen-debug") << "Process sygus type:" << std::endl;
658
9
  Trace("dtsygus-gen-debug") << sdtd.getName() << std::endl;
659
660
  // datatype types we need to process
661
18
  std::vector<TypeNode> dtToProcess;
662
  // datatype types we have processed
663
18
  std::map<TypeNode, TypeNode> dtProcessed;
664
9
  dtToProcess.push_back(sdt);
665
18
  std::stringstream ssutn0;
666
9
  ssutn0 << sdtd.getName() << "_s";
667
  TypeNode abdTNew =
668
18
      nm->mkSort(ssutn0.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
669
9
  unres.insert(abdTNew);
670
9
  dtProcessed[sdt] = abdTNew;
671
672
  // We must convert all symbols in the sygus datatype type sdt to
673
  // apply the substitution { syms -> vars }, where syms is the free
674
  // variables of the input problem, and vars is the formal argument list
675
  // of the function-to-synthesize.
676
677
  // We are traversing over the subfield types of the datatype to convert
678
  // them into the form described above.
679
45
  while (!dtToProcess.empty())
680
  {
681
36
    std::vector<TypeNode> dtNextToProcess;
682
38
    for (const TypeNode& curr : dtToProcess)
683
    {
684
20
      Assert(curr.isDatatype() && curr.getDType().isSygus());
685
20
      const DType& dtc = curr.getDType();
686
40
      std::stringstream ssdtn;
687
20
      ssdtn << dtc.getName() << "_s";
688
20
      sdts.push_back(SygusDatatype(ssdtn.str()));
689
40
      Trace("dtsygus-gen-debug")
690
20
          << "Process datatype " << sdts.back().getName() << "..." << std::endl;
691
72
      for (unsigned j = 0, ncons = dtc.getNumConstructors(); j < ncons; j++)
692
      {
693
104
        Node op = dtc[j].getSygusOp();
694
        // apply the substitution to the argument
695
        Node ops =
696
104
            op.substitute(syms.begin(), syms.end(), vars.begin(), vars.end());
697
104
        Trace("dtsygus-gen-debug") << "  Process constructor " << op << " / "
698
52
                                   << ops << "..." << std::endl;
699
104
        std::vector<TypeNode> cargs;
700
90
        for (unsigned k = 0, nargs = dtc[j].getNumArgs(); k < nargs; k++)
701
        {
702
76
          TypeNode argt = dtc[j].getArgType(k);
703
38
          std::map<TypeNode, TypeNode>::iterator itdp = dtProcessed.find(argt);
704
76
          TypeNode argtNew;
705
38
          if (itdp == dtProcessed.end())
706
          {
707
22
            std::stringstream ssutn;
708
11
            ssutn << argt.getDType().getName() << "_s";
709
11
            argtNew =
710
22
                nm->mkSort(ssutn.str(), NodeManager::SORT_FLAG_PLACEHOLDER);
711
22
            Trace("dtsygus-gen-debug") << "    ...unresolved type " << argtNew
712
11
                                       << " for " << argt << std::endl;
713
11
            unres.insert(argtNew);
714
11
            dtProcessed[argt] = argtNew;
715
11
            dtNextToProcess.push_back(argt);
716
          }
717
          else
718
          {
719
27
            argtNew = itdp->second;
720
          }
721
76
          Trace("dtsygus-gen-debug")
722
38
              << "    Arg #" << k << ": " << argtNew << std::endl;
723
38
          cargs.push_back(argtNew);
724
        }
725
104
        std::stringstream ss;
726
52
        ss << ops.getKind();
727
52
        Trace("dtsygus-gen-debug") << "Add constructor : " << ops << std::endl;
728
52
        sdts.back().addConstructor(ops, ss.str(), cargs);
729
      }
730
40
      Trace("dtsygus-gen-debug")
731
20
          << "Set sygus : " << dtc.getSygusType() << " " << abvl << std::endl;
732
40
      TypeNode stn = dtc.getSygusType();
733
60
      sdts.back().initializeDatatype(
734
40
          stn, abvl, dtc.getSygusAllowConst(), dtc.getSygusAllowAll());
735
    }
736
18
    dtToProcess.clear();
737
18
    dtToProcess.insert(
738
36
        dtToProcess.end(), dtNextToProcess.begin(), dtNextToProcess.end());
739
  }
740
18
  Trace("dtsygus-gen-debug")
741
9
      << "Make " << sdts.size() << " datatype types..." << std::endl;
742
  // extract the datatypes
743
18
  std::vector<DType> datatypes;
744
29
  for (unsigned i = 0, ndts = sdts.size(); i < ndts; i++)
745
  {
746
20
    datatypes.push_back(sdts[i].getDatatype());
747
  }
748
  // make the datatype types
749
  std::vector<TypeNode> datatypeTypes = nm->mkMutualDatatypeTypes(
750
18
      datatypes, unres, NodeManager::DATATYPE_FLAG_PLACEHOLDER);
751
9
  TypeNode sdtS = datatypeTypes[0];
752
9
  if (Trace.isOn("dtsygus-gen-debug"))
753
  {
754
    Trace("dtsygus-gen-debug") << "Made datatype types:" << std::endl;
755
    for (unsigned j = 0, ndts = datatypeTypes.size(); j < ndts; j++)
756
    {
757
      const DType& dtj = datatypeTypes[j].getDType();
758
      Trace("dtsygus-gen-debug") << "#" << j << ": " << dtj << std::endl;
759
      for (unsigned k = 0, ncons = dtj.getNumConstructors(); k < ncons; k++)
760
      {
761
        for (unsigned l = 0, nargs = dtj[k].getNumArgs(); l < nargs; l++)
762
        {
763
          if (!dtj[k].getArgType(l).isDatatype())
764
          {
765
            Trace("dtsygus-gen-debug")
766
                << "Argument " << l << " of " << dtj[k]
767
                << " is not datatype : " << dtj[k].getArgType(l) << std::endl;
768
            AlwaysAssert(false);
769
          }
770
        }
771
      }
772
    }
773
  }
774
18
  return sdtS;
775
}
776
777
}  // namespace utils
778
}  // namespace datatypes
779
}  // namespace theory
780
26676
}  // namespace CVC4