GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/expr/term_canonize.cpp Lines: 100 101 99.0 %
Date: 2021-03-23 Branches: 200 366 54.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file term_canonize.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds
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 term canonize.
13
 **/
14
15
#include "expr/term_canonize.h"
16
17
#include <sstream>
18
19
// TODO #1216: move the code in this include
20
#include "theory/quantifiers/term_util.h"
21
22
using namespace CVC4::kind;
23
24
namespace CVC4 {
25
namespace expr {
26
27
6066
TermCanonize::TermCanonize() : d_op_id_count(0), d_typ_id_count(0) {}
28
29
292024
int TermCanonize::getIdForOperator(Node op)
30
{
31
292024
  std::map<Node, int>::iterator it = d_op_id.find(op);
32
292024
  if (it == d_op_id.end())
33
  {
34
21973
    d_op_id[op] = d_op_id_count;
35
21973
    d_op_id_count++;
36
21973
    return d_op_id[op];
37
  }
38
270051
  return it->second;
39
}
40
41
34144
int TermCanonize::getIdForType(TypeNode t)
42
{
43
34144
  std::map<TypeNode, int>::iterator it = d_typ_id.find(t);
44
34144
  if (it == d_typ_id.end())
45
  {
46
1920
    d_typ_id[t] = d_typ_id_count;
47
1920
    d_typ_id_count++;
48
1920
    return d_typ_id[t];
49
  }
50
32224
  return it->second;
51
}
52
53
443650
bool TermCanonize::getTermOrder(Node a, Node b)
54
{
55
443650
  if (a.getKind() == BOUND_VARIABLE)
56
  {
57
54455
    if (b.getKind() == BOUND_VARIABLE)
58
    {
59
37651
      return getIndexForFreeVariable(a) < getIndexForFreeVariable(b);
60
    }
61
16804
    return true;
62
  }
63
389195
  if (b.getKind() != BOUND_VARIABLE)
64
  {
65
353747
    Node aop = a.hasOperator() ? a.getOperator() : a;
66
353747
    Node bop = b.hasOperator() ? b.getOperator() : b;
67
353263
    Trace("aeq-debug2") << a << "...op..." << aop << std::endl;
68
353263
    Trace("aeq-debug2") << b << "...op..." << bop << std::endl;
69
353263
    if (aop == bop)
70
    {
71
207251
      if (a.getNumChildren() == b.getNumChildren())
72
      {
73
260724
        for (unsigned i = 0, size = a.getNumChildren(); i < size; i++)
74
        {
75
260240
          if (a[i] != b[i])
76
          {
77
            // first distinct child determines the ordering
78
201266
            return getTermOrder(a[i], b[i]);
79
          }
80
        }
81
      }
82
      else
83
      {
84
5501
        return aop.getNumChildren() < bop.getNumChildren();
85
      }
86
    }
87
    else
88
    {
89
146012
      return getIdForOperator(aop) < getIdForOperator(bop);
90
    }
91
  }
92
36416
  return false;
93
}
94
95
108307
Node TermCanonize::getCanonicalFreeVar(TypeNode tn, unsigned i)
96
{
97
108307
  Assert(!tn.isNull());
98
108307
  NodeManager* nm = NodeManager::currentNM();
99
129131
  while (d_cn_free_var[tn].size() <= i)
100
  {
101
20824
    std::stringstream oss;
102
10412
    oss << tn;
103
20824
    std::string typ_name = oss.str();
104
14366
    while (typ_name[0] == '(')
105
    {
106
1977
      typ_name.erase(typ_name.begin());
107
    }
108
20824
    std::stringstream os;
109
10412
    os << typ_name[0] << i;
110
20824
    Node x = nm->mkBoundVar(os.str().c_str(), tn);
111
10412
    d_fvIndex[x] = d_cn_free_var[tn].size();
112
10412
    d_cn_free_var[tn].push_back(x);
113
  }
114
108307
  return d_cn_free_var[tn][i];
115
}
116
117
75302
size_t TermCanonize::getIndexForFreeVariable(Node v) const
118
{
119
75302
  std::map<Node, size_t>::const_iterator it = d_fvIndex.find(v);
120
75302
  if (it == d_fvIndex.end())
121
  {
122
75302
    return 0;
123
  }
124
  return it->second;
125
}
126
127
struct sortTermOrder
128
{
129
  TermCanonize* d_tu;
130
242384
  bool operator()(Node i, Node j) { return d_tu->getTermOrder(i, j); }
131
};
132
133
710135
Node TermCanonize::getCanonicalTerm(TNode n,
134
                                    bool apply_torder,
135
                                    bool doHoVar,
136
                                    std::map<TypeNode, unsigned>& var_count,
137
                                    std::map<TNode, Node>& visited)
138
{
139
710135
  std::map<TNode, Node>::iterator it = visited.find(n);
140
710135
  if (it != visited.end())
141
  {
142
158810
    return it->second;
143
  }
144
145
551325
  Trace("canon-term-debug") << "Get canonical term for " << n << std::endl;
146
551325
  if (n.getKind() == BOUND_VARIABLE)
147
  {
148
132558
    TypeNode tn = n.getType();
149
    // allocate variable
150
66279
    unsigned vn = var_count[tn];
151
66279
    var_count[tn]++;
152
132558
    Node fv = getCanonicalFreeVar(tn, vn);
153
66279
    visited[n] = fv;
154
66279
    Trace("canon-term-debug") << "...allocate variable." << std::endl;
155
66279
    return fv;
156
  }
157
485046
  else if (n.getNumChildren() > 0)
158
  {
159
    // collect children
160
273199
    Trace("canon-term-debug") << "Collect children" << std::endl;
161
546398
    std::vector<Node> cchildren;
162
846499
    for (const Node& cn : n)
163
    {
164
573300
      cchildren.push_back(cn);
165
    }
166
    // if applicable, first sort by term order
167
273199
    if (apply_torder && theory::quantifiers::TermUtil::isComm(n.getKind()))
168
    {
169
184486
      Trace("canon-term-debug")
170
92243
          << "Sort based on commutative operator " << n.getKind() << std::endl;
171
      sortTermOrder sto;
172
92243
      sto.d_tu = this;
173
92243
      std::sort(cchildren.begin(), cchildren.end(), sto);
174
    }
175
    // now make canonical
176
273199
    Trace("canon-term-debug") << "Make canonical children" << std::endl;
177
846499
    for (unsigned i = 0, size = cchildren.size(); i < size; i++)
178
    {
179
1146600
      cchildren[i] = getCanonicalTerm(
180
573300
          cchildren[i], apply_torder, doHoVar, var_count, visited);
181
    }
182
273199
    if (n.getMetaKind() == metakind::PARAMETERIZED)
183
    {
184
222710
      Node op = n.getOperator();
185
111355
      if (doHoVar)
186
      {
187
111355
        op = getCanonicalTerm(op, apply_torder, doHoVar, var_count, visited);
188
      }
189
111355
      Trace("canon-term-debug") << "Insert operator " << op << std::endl;
190
111355
      cchildren.insert(cchildren.begin(), op);
191
    }
192
546398
    Trace("canon-term-debug")
193
273199
        << "...constructing for " << n << "." << std::endl;
194
546398
    Node ret = NodeManager::currentNM()->mkNode(n.getKind(), cchildren);
195
546398
    Trace("canon-term-debug")
196
273199
        << "...constructed " << ret << " for " << n << "." << std::endl;
197
273199
    visited[n] = ret;
198
273199
    return ret;
199
  }
200
211847
  Trace("canon-term-debug") << "...return 0-child term." << std::endl;
201
211847
  return n;
202
}
203
204
25480
Node TermCanonize::getCanonicalTerm(TNode n, bool apply_torder, bool doHoVar)
205
{
206
50960
  std::map<TypeNode, unsigned> var_count;
207
50960
  std::map<TNode, Node> visited;
208
50960
  return getCanonicalTerm(n, apply_torder, doHoVar, var_count, visited);
209
}
210
211
}  // namespace expr
212
26685
}  // namespace CVC4