GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/datatypes/theory_datatypes_utils.cpp Lines: 83 99 83.8 %
Date: 2021-03-22 Branches: 188 453 41.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file theory_datatypes_utils.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Morgan Deters, Mathias Preiner
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/theory_datatypes_utils.h"
18
19
#include "expr/dtype.h"
20
#include "expr/dtype_cons.h"
21
22
using namespace CVC4;
23
using namespace CVC4::kind;
24
25
namespace CVC4 {
26
namespace theory {
27
namespace datatypes {
28
namespace utils {
29
30
/** get instantiate cons */
31
154822
Node getInstCons(Node n, const DType& dt, int index)
32
{
33
154822
  Assert(index >= 0 && index < (int)dt.getNumConstructors());
34
309644
  std::vector<Node> children;
35
154822
  NodeManager* nm = NodeManager::currentNM();
36
154822
  children.push_back(dt[index].getConstructor());
37
309644
  TypeNode tn = n.getType();
38
276187
  for (unsigned i = 0, nargs = dt[index].getNumArgs(); i < nargs; i++)
39
  {
40
    Node nc = nm->mkNode(
41
242730
        APPLY_SELECTOR_TOTAL, dt[index].getSelectorInternal(tn, i), n);
42
121365
    children.push_back(nc);
43
  }
44
154822
  Node n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
45
154822
  if (dt.isParametric())
46
  {
47
    // add type ascription for ambiguous constructor types
48
379
    if (!n_ic.getType().isComparableTo(tn))
49
    {
50
12
      Debug("datatypes-parametric")
51
6
          << "DtInstantiate: ambiguous type for " << n_ic << ", ascribe to "
52
6
          << n.getType() << std::endl;
53
12
      Debug("datatypes-parametric")
54
6
          << "Constructor is " << dt[index] << std::endl;
55
12
      TypeNode tspec = dt[index].getSpecializedConstructorType(n.getType());
56
12
      Debug("datatypes-parametric")
57
6
          << "Type specification is " << tspec << std::endl;
58
18
      children[0] = nm->mkNode(APPLY_TYPE_ASCRIPTION,
59
12
                               nm->mkConst(AscriptionType(tspec)),
60
6
                               children[0]);
61
6
      n_ic = nm->mkNode(APPLY_CONSTRUCTOR, children);
62
6
      Assert(n_ic.getType() == tn);
63
    }
64
  }
65
154822
  Assert(isInstCons(n, n_ic, dt) == index);
66
  // n_ic = Rewriter::rewrite( n_ic );
67
309644
  return n_ic;
68
}
69
70
154822
int isInstCons(Node t, Node n, const DType& dt)
71
{
72
154822
  if (n.getKind() == APPLY_CONSTRUCTOR)
73
  {
74
154822
    int index = indexOf(n.getOperator());
75
154822
    const DTypeConstructor& c = dt[index];
76
309644
    TypeNode tn = n.getType();
77
276187
    for (unsigned i = 0, size = n.getNumChildren(); i < size; i++)
78
    {
79
364095
      if (n[i].getKind() != APPLY_SELECTOR_TOTAL
80
364095
          || n[i].getOperator() != c.getSelectorInternal(tn, i) || n[i][0] != t)
81
      {
82
        return -1;
83
      }
84
    }
85
154822
    return index;
86
  }
87
  return -1;
88
}
89
90
2893950
int isTester(Node n, Node& a)
91
{
92
2893950
  if (n.getKind() == APPLY_TESTER)
93
  {
94
1511514
    a = n[0];
95
1511514
    return indexOf(n.getOperator());
96
  }
97
1382436
  return -1;
98
}
99
100
147910
int isTester(Node n)
101
{
102
147910
  if (n.getKind() == APPLY_TESTER)
103
  {
104
147910
    return indexOf(n.getOperator());
105
  }
106
  return -1;
107
}
108
109
4410609
size_t indexOf(Node n) { return DType::indexOf(n); }
110
111
3138
size_t cindexOf(Node n) { return DType::cindexOf(n); }
112
113
654076
const DType& datatypeOf(Node n)
114
{
115
1308152
  TypeNode t = n.getType();
116
654076
  switch (t.getKind())
117
  {
118
360189
    case CONSTRUCTOR_TYPE: return t[t.getNumChildren() - 1].getDType();
119
293887
    case SELECTOR_TYPE:
120
293887
    case TESTER_TYPE: return t[0].getDType();
121
    default:
122
      Unhandled() << "arg must be a datatype constructor, selector, or tester";
123
  }
124
}
125
126
311285
Node mkTester(Node n, int i, const DType& dt)
127
{
128
311285
  return NodeManager::currentNM()->mkNode(APPLY_TESTER, dt[i].getTester(), n);
129
}
130
131
3925
Node mkSplit(Node n, const DType& dt)
132
{
133
7850
  std::vector<Node> splits;
134
17741
  for (unsigned i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
135
  {
136
27632
    Node test = mkTester(n, i, dt);
137
13816
    splits.push_back(test);
138
  }
139
3925
  NodeManager* nm = NodeManager::currentNM();
140
7850
  return splits.size() == 1 ? splits[0] : nm->mkNode(OR, splits);
141
}
142
143
bool isNullaryApplyConstructor(Node n)
144
{
145
  Assert(n.getKind() == APPLY_CONSTRUCTOR);
146
  for (const Node& nc : n)
147
  {
148
    if (nc.getType().isDatatype())
149
    {
150
      return false;
151
    }
152
  }
153
  return true;
154
}
155
156
bool isNullaryConstructor(const DTypeConstructor& c)
157
{
158
  for (unsigned j = 0, nargs = c.getNumArgs(); j < nargs; j++)
159
  {
160
    if (c[j].getType().getRangeType().isDatatype())
161
    {
162
      return false;
163
    }
164
  }
165
  return true;
166
}
167
168
280785
bool checkClash(Node n1, Node n2, std::vector<Node>& rew)
169
{
170
561570
  Trace("datatypes-rewrite-debug")
171
280785
      << "Check clash : " << n1 << " " << n2 << std::endl;
172
280785
  if (n1.getKind() == APPLY_CONSTRUCTOR && n2.getKind() == APPLY_CONSTRUCTOR)
173
  {
174
70353
    if (n1.getOperator() != n2.getOperator())
175
    {
176
7948
      Trace("datatypes-rewrite-debug")
177
7948
          << "Clash operators : " << n1 << " " << n2 << " " << n1.getOperator()
178
3974
          << " " << n2.getOperator() << std::endl;
179
3974
      return true;
180
    }
181
66379
    Assert(n1.getNumChildren() == n2.getNumChildren());
182
156922
    for (unsigned i = 0, size = n1.getNumChildren(); i < size; i++)
183
    {
184
104946
      if (checkClash(n1[i], n2[i], rew))
185
      {
186
14403
        return true;
187
      }
188
    }
189
  }
190
210432
  else if (n1 != n2)
191
  {
192
205855
    if (n1.isConst() && n2.isConst())
193
    {
194
386
      Trace("datatypes-rewrite-debug")
195
193
          << "Clash constants : " << n1 << " " << n2 << std::endl;
196
193
      return true;
197
    }
198
    else
199
    {
200
411324
      Node eq = NodeManager::currentNM()->mkNode(EQUAL, n1, n2);
201
205662
      rew.push_back(eq);
202
    }
203
  }
204
262215
  return false;
205
}
206
207
}  // namespace utils
208
}  // namespace datatypes
209
}  // namespace theory
210
26676
}  // namespace CVC4