GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/arith_utilities.cpp Lines: 127 161 78.9 %
Date: 2021-03-23 Branches: 230 654 35.2 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file arith_utilities.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Alex Ozdemir, Tim King
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 common functions for dealing with nodes.
13
 **/
14
15
#include "arith_utilities.h"
16
17
#include <cmath>
18
19
using namespace CVC4::kind;
20
21
namespace CVC4 {
22
namespace theory {
23
namespace arith {
24
25
175
Kind joinKinds(Kind k1, Kind k2)
26
{
27
175
  if (k2 < k1)
28
  {
29
28
    return joinKinds(k2, k1);
30
  }
31
147
  else if (k1 == k2)
32
  {
33
    return k1;
34
  }
35
147
  Assert(isRelationOperator(k1));
36
147
  Assert(isRelationOperator(k2));
37
147
  if (k1 == EQUAL)
38
  {
39
    if (k2 == LEQ || k2 == GEQ)
40
    {
41
      return k1;
42
    }
43
  }
44
147
  else if (k1 == LT)
45
  {
46
29
    if (k2 == LEQ)
47
    {
48
29
      return k1;
49
    }
50
  }
51
118
  else if (k1 == LEQ)
52
  {
53
    if (k2 == GEQ)
54
    {
55
      return EQUAL;
56
    }
57
  }
58
118
  else if (k1 == GT)
59
  {
60
118
    if (k2 == GEQ)
61
    {
62
118
      return k1;
63
    }
64
  }
65
  return UNDEFINED_KIND;
66
}
67
68
Kind transKinds(Kind k1, Kind k2)
69
{
70
  if (k2 < k1)
71
  {
72
    return transKinds(k2, k1);
73
  }
74
  else if (k1 == k2)
75
  {
76
    return k1;
77
  }
78
  Assert(isRelationOperator(k1));
79
  Assert(isRelationOperator(k2));
80
  if (k1 == EQUAL)
81
  {
82
    return k2;
83
  }
84
  else if (k1 == LT)
85
  {
86
    if (k2 == LEQ)
87
    {
88
      return k1;
89
    }
90
  }
91
  else if (k1 == GT)
92
  {
93
    if (k2 == GEQ)
94
    {
95
      return k1;
96
    }
97
  }
98
  return UNDEFINED_KIND;
99
}
100
101
36802
bool isTranscendentalKind(Kind k)
102
{
103
  // many operators are eliminated during rewriting
104
36802
  Assert(k != TANGENT && k != COSINE && k != COSECANT
105
         && k != SECANT && k != COTANGENT);
106
36802
  return k == EXPONENTIAL || k == SINE || k == PI;
107
}
108
109
1951
Node getApproximateConstant(Node c, bool isLower, unsigned prec)
110
{
111
1951
  if (!c.isConst())
112
  {
113
    Assert(false) << "getApproximateConstant: non-constant input " << c;
114
    return Node::null();
115
  }
116
3902
  Rational cr = c.getConst<Rational>();
117
118
1951
  unsigned lower = 0;
119
1951
  unsigned upper = std::pow(10, prec);
120
121
3902
  Rational den = Rational(upper);
122
1951
  if (cr.getDenominator() < den.getNumerator())
123
  {
124
    // denominator is not more than precision, we return it
125
916
    return c;
126
  }
127
128
1035
  int csign = cr.sgn();
129
1035
  Assert(csign != 0);
130
1035
  if (csign == -1)
131
  {
132
20
    cr = -cr;
133
  }
134
2070
  Rational one = Rational(1);
135
2070
  Rational ten = Rational(10);
136
2070
  Rational pow_ten = Rational(1);
137
  // inefficient for large numbers
138
5061
  while (cr >= one)
139
  {
140
2013
    cr = cr / ten;
141
2013
    pow_ten = pow_ten * ten;
142
  }
143
2070
  Rational allow_err = one / den;
144
145
  // now do binary search
146
2070
  Rational two = Rational(2);
147
1035
  NodeManager* nm = NodeManager::currentNM();
148
2070
  Node cret;
149
14309
  do
150
  {
151
15344
    unsigned curr = (lower + upper) / 2;
152
30688
    Rational curr_r = Rational(curr) / den;
153
30688
    Rational err = cr - curr_r;
154
15344
    int esign = err.sgn();
155
15344
    if (err.abs() <= allow_err)
156
    {
157
1035
      if (esign == 1 && !isLower)
158
      {
159
        curr_r = Rational(curr + 1) / den;
160
      }
161
1035
      else if (esign == -1 && isLower)
162
      {
163
225
        curr_r = Rational(curr - 1) / den;
164
      }
165
1035
      curr_r = curr_r * pow_ten;
166
1035
      cret = nm->mkConst(csign == 1 ? curr_r : -curr_r);
167
    }
168
    else
169
    {
170
14309
      Assert(esign != 0);
171
      // update lower/upper
172
14309
      if (esign == -1)
173
      {
174
7144
        upper = curr;
175
      }
176
7165
      else if (esign == 1)
177
      {
178
7165
        lower = curr;
179
      }
180
    }
181
15344
  } while (cret.isNull());
182
1035
  return cret;
183
}
184
185
1951
void printRationalApprox(const char* c, Node cr, unsigned prec)
186
{
187
1951
  if (!cr.isConst())
188
  {
189
    Assert(false) << "printRationalApprox: non-constant input " << cr;
190
    Trace(c) << cr;
191
    return;
192
  }
193
3902
  Node ca = getApproximateConstant(cr, true, prec);
194
1951
  if (ca != cr)
195
  {
196
1035
    Trace(c) << "(+ ";
197
  }
198
1951
  Trace(c) << ca;
199
1951
  if (ca != cr)
200
  {
201
1035
    Trace(c) << " [0,10^" << prec << "])";
202
  }
203
}
204
205
4930
Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs)
206
{
207
4930
  Assert(vars.size() == subs.size());
208
4930
  NodeManager* nm = NodeManager::currentNM();
209
9860
  std::unordered_map<TNode, Node, TNodeHashFunction> visited;
210
4930
  std::unordered_map<TNode, Node, TNodeHashFunction>::iterator it;
211
4930
  std::vector<Node>::iterator itv;
212
9860
  std::vector<TNode> visit;
213
9860
  TNode cur;
214
  Kind ck;
215
4930
  visit.push_back(n);
216
34321
  do
217
  {
218
39251
    cur = visit.back();
219
39251
    visit.pop_back();
220
39251
    it = visited.find(cur);
221
222
39251
    if (it == visited.end())
223
    {
224
25623
      visited[cur] = Node::null();
225
25623
      ck = cur.getKind();
226
25623
      itv = std::find(vars.begin(), vars.end(), cur);
227
25623
      if (itv != vars.end())
228
      {
229
4014
        visited[cur] = subs[std::distance(vars.begin(), itv)];
230
      }
231
21609
      else if (cur.getNumChildren() == 0)
232
      {
233
8375
        visited[cur] = cur;
234
      }
235
      else
236
      {
237
13234
        TheoryId ctid = theory::kindToTheoryId(ck);
238
17148
        if ((ctid != THEORY_ARITH && ctid != THEORY_BOOL
239
1423
             && ctid != THEORY_BUILTIN)
240
26434
            || isTranscendentalKind(ck))
241
        {
242
          // Do not traverse beneath applications that belong to another theory
243
          // besides (core) arithmetic. Notice that transcendental function
244
          // applications are also not traversed here.
245
1140
          visited[cur] = cur;
246
        }
247
        else
248
        {
249
12094
          visit.push_back(cur);
250
34321
          for (const Node& cn : cur)
251
          {
252
22227
            visit.push_back(cn);
253
          }
254
        }
255
      }
256
    }
257
13628
    else if (it->second.isNull())
258
    {
259
24188
      Node ret = cur;
260
12094
      bool childChanged = false;
261
24188
      std::vector<Node> children;
262
12094
      if (cur.getMetaKind() == kind::metakind::PARAMETERIZED)
263
      {
264
        children.push_back(cur.getOperator());
265
      }
266
34321
      for (const Node& cn : cur)
267
      {
268
22227
        it = visited.find(cn);
269
22227
        Assert(it != visited.end());
270
22227
        Assert(!it->second.isNull());
271
22227
        childChanged = childChanged || cn != it->second;
272
22227
        children.push_back(it->second);
273
      }
274
12094
      if (childChanged)
275
      {
276
5740
        ret = nm->mkNode(cur.getKind(), children);
277
      }
278
12094
      visited[cur] = ret;
279
    }
280
39251
  } while (!visit.empty());
281
4930
  Assert(visited.find(n) != visited.end());
282
4930
  Assert(!visited.find(n)->second.isNull());
283
9860
  return visited[n];
284
}
285
286
492
Node mkBounded(Node l, Node a, Node u)
287
{
288
492
  NodeManager* nm = NodeManager::currentNM();
289
492
  return nm->mkNode(AND, nm->mkNode(GEQ, a, l), nm->mkNode(LEQ, a, u));
290
}
291
292
1200
Rational leastIntGreaterThan(const Rational& q) { return q.floor() + 1; }
293
294
56541
Rational greatestIntLessThan(const Rational& q) { return q.ceiling() - 1; }
295
296
87434
Node negateProofLiteral(TNode n)
297
{
298
87434
  auto nm = NodeManager::currentNM();
299
87434
  switch (n.getKind())
300
  {
301
    case Kind::GT:
302
    {
303
      return nm->mkNode(Kind::LEQ, n[0], n[1]);
304
    }
305
    case Kind::LT:
306
    {
307
      return nm->mkNode(Kind::GEQ, n[0], n[1]);
308
    }
309
42166
    case Kind::LEQ:
310
    {
311
42166
      return nm->mkNode(Kind::GT, n[0], n[1]);
312
    }
313
41079
    case Kind::GEQ:
314
    {
315
41079
      return nm->mkNode(Kind::LT, n[0], n[1]);
316
    }
317
4189
    case Kind::EQUAL:
318
    case Kind::NOT:
319
    {
320
4189
      return n.negate();
321
    }
322
    default: Unhandled() << n;
323
  }
324
}
325
326
}  // namespace arith
327
}  // namespace theory
328
26685
}  // namespace CVC4