GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/arith_utilities.h Lines: 74 115 64.3 %
Date: 2021-03-23 Branches: 52 155 33.5 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file arith_utilities.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Andrew Reynolds, 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 Common functions for dealing with nodes.
13
 **/
14
15
#include "cvc4_private.h"
16
17
#ifndef CVC4__THEORY__ARITH__ARITH_UTILITIES_H
18
#define CVC4__THEORY__ARITH__ARITH_UTILITIES_H
19
20
#include <unordered_map>
21
#include <unordered_set>
22
#include <vector>
23
24
#include "context/cdhashset.h"
25
#include "expr/node.h"
26
#include "theory/arith/arithvar.h"
27
#include "util/dense_map.h"
28
#include "util/integer.h"
29
#include "util/rational.h"
30
31
namespace CVC4 {
32
namespace theory {
33
namespace arith {
34
35
//Sets of Nodes
36
typedef std::unordered_set<Node, NodeHashFunction> NodeSet;
37
typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet;
38
typedef context::CDHashSet<Node, NodeHashFunction> CDNodeSet;
39
40
//Maps from Nodes -> ArithVars, and vice versa
41
typedef std::unordered_map<Node, ArithVar, NodeHashFunction> NodeToArithVarMap;
42
typedef DenseMap<Node> ArithVarToNodeMap;
43
44
130527096
inline Node mkRationalNode(const Rational& q){
45
130527096
  return NodeManager::currentNM()->mkConst<Rational>(q);
46
}
47
48
5804
inline Node mkBoolNode(bool b){
49
5804
  return NodeManager::currentNM()->mkConst<bool>(b);
50
}
51
52
inline Node mkIntSkolem(const std::string& name){
53
  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->integerType());
54
}
55
56
inline Node mkRealSkolem(const std::string& name){
57
  return NodeManager::currentNM()->mkSkolem(name, NodeManager::currentNM()->realType());
58
}
59
60
inline Node skolemFunction(const std::string& name, TypeNode dom, TypeNode range){
61
  NodeManager* currNM = NodeManager::currentNM();
62
  TypeNode functionType = currNM->mkFunctionType(dom, range);
63
  return currNM->mkSkolem(name, functionType);
64
}
65
66
/** \f$ k \in {LT, LEQ, EQ, GEQ, GT} \f$ */
67
195781919
inline bool isRelationOperator(Kind k){
68
  using namespace kind;
69
70
195781919
  switch(k){
71
11874193
  case LT:
72
  case LEQ:
73
  case EQUAL:
74
  case GEQ:
75
  case GT:
76
11874193
    return true;
77
183907726
  default:
78
183907726
    return false;
79
  }
80
}
81
82
/**
83
 * Given a relational kind, k, return the kind k' s.t.
84
 * swapping the lefthand and righthand side is equivalent.
85
 *
86
 * The following equivalence should hold,
87
 *   (k l r) <=> (k' r l)
88
 */
89
9684
inline Kind reverseRelationKind(Kind k){
90
  using namespace kind;
91
92
9684
  switch(k){
93
1086
  case LT:    return GT;
94
144
  case LEQ:   return GEQ;
95
457
  case EQUAL: return EQUAL;
96
6276
  case GEQ:   return LEQ;
97
1721
  case GT:    return LT;
98
99
  default:
100
    Unreachable();
101
  }
102
}
103
104
337135
inline bool evaluateConstantPredicate(Kind k, const Rational& left, const Rational& right){
105
  using namespace kind;
106
107
337135
  switch(k){
108
  case LT:    return left <  right;
109
21005
  case LEQ:   return left <= right;
110
213157
  case EQUAL: return left == right;
111
102973
  case GEQ:   return left >= right;
112
  case GT:    return left >  right;
113
  default:
114
    Unreachable();
115
    return true;
116
  }
117
}
118
119
/**
120
 * Returns the appropriate coefficient for the infinitesimal given the kind
121
 * for an arithmetic atom inorder to represent strict inequalities as inequalities.
122
 *   x < c  becomes  x <= c + (-1) * \f$ \delta \f$
123
 *   x > c  becomes  x >= x + ( 1) * \f$ \delta \f$
124
 * Non-strict inequalities have a coefficient of zero.
125
 */
126
976485
inline int deltaCoeff(Kind k){
127
976485
  switch(k){
128
271398
  case kind::LT:
129
271398
    return -1;
130
  case kind::GT:
131
    return 1;
132
705087
  default:
133
705087
    return 0;
134
  }
135
}
136
137
/**
138
 * Given a literal to TheoryArith return a single kind to
139
 * to indicate its underlying structure.
140
 * The function returns the following in each case:
141
 * - (K left right) -> K where is a wildcard for EQUAL, LT, GT, LEQ, or GEQ:
142
 * - (NOT (EQUAL left right)) -> DISTINCT
143
 * - (NOT (LEQ left right))   -> GT
144
 * - (NOT (GEQ left right))   -> LT
145
 * - (NOT (LT left right))    -> GEQ
146
 * - (NOT (GT left right))    -> LEQ
147
 * If none of these match, it returns UNDEFINED_KIND.
148
 */
149
2103
inline Kind oldSimplifiedKind(TNode literal){
150
2103
  switch(literal.getKind()){
151
2103
  case kind::LT:
152
  case kind::GT:
153
  case kind::LEQ:
154
  case kind::GEQ:
155
  case kind::EQUAL:
156
2103
    return literal.getKind();
157
  case  kind::NOT:
158
    {
159
      TNode atom = literal[0];
160
      switch(atom.getKind()){
161
      case  kind::LEQ: //(not (LEQ x c)) <=> (GT x c)
162
        return  kind::GT;
163
      case  kind::GEQ: //(not (GEQ x c)) <=> (LT x c)
164
        return  kind::LT;
165
      case  kind::LT: //(not (LT x c)) <=> (GEQ x c)
166
        return  kind::GEQ;
167
      case  kind::GT: //(not (GT x c) <=> (LEQ x c)
168
        return  kind::LEQ;
169
      case  kind::EQUAL:
170
        return  kind::DISTINCT;
171
      default:
172
        Unreachable();
173
        return  kind::UNDEFINED_KIND;
174
      }
175
    }
176
  default:
177
    Unreachable();
178
    return kind::UNDEFINED_KIND;
179
  }
180
}
181
182
25499
inline Kind negateKind(Kind k){
183
25499
  switch(k){
184
  case kind::LT:       return kind::GEQ;
185
  case kind::GT:       return kind::LEQ;
186
11771
  case kind::LEQ:      return kind::GT;
187
13717
  case kind::GEQ:      return kind::LT;
188
11
  case kind::EQUAL:    return kind::DISTINCT;
189
  case kind::DISTINCT: return kind::EQUAL;
190
  default:
191
    return kind::UNDEFINED_KIND;
192
  }
193
}
194
195
inline Node negateConjunctionAsClause(TNode conjunction){
196
  Assert(conjunction.getKind() == kind::AND);
197
  NodeBuilder<> orBuilder(kind::OR);
198
199
  for(TNode::iterator i = conjunction.begin(), end=conjunction.end(); i != end; ++i){
200
    TNode child = *i;
201
    Node negatedChild = NodeBuilder<1>(kind::NOT)<<(child);
202
    orBuilder << negatedChild;
203
  }
204
  return orBuilder;
205
}
206
207
inline Node maybeUnaryConvert(NodeBuilder<>& builder){
208
  Assert(builder.getKind() == kind::OR || builder.getKind() == kind::AND
209
         || builder.getKind() == kind::PLUS || builder.getKind() == kind::MULT);
210
  Assert(builder.getNumChildren() >= 1);
211
  if(builder.getNumChildren() == 1){
212
    return builder[0];
213
  }else{
214
    return builder;
215
  }
216
}
217
218
6150
inline void flattenAnd(Node n, std::vector<TNode>& out){
219
6150
  Assert(n.getKind() == kind::AND);
220
23417
  for(Node::iterator i=n.begin(), i_end=n.end(); i != i_end; ++i){
221
34534
    Node curr = *i;
222
17267
    if(curr.getKind() == kind::AND){
223
3762
      flattenAnd(curr, out);
224
    }else{
225
13505
      out.push_back(curr);
226
    }
227
  }
228
6150
}
229
230
2388
inline Node flattenAnd(Node n){
231
4776
  std::vector<TNode> out;
232
2388
  flattenAnd(n, out);
233
4776
  return NodeManager::currentNM()->mkNode(kind::AND, out);
234
}
235
236
// Returns an node that is the identity of a select few kinds.
237
1497
inline Node getIdentity(Kind k){
238
1497
  switch(k){
239
  case kind::AND:
240
    return mkBoolNode(true);
241
  case kind::PLUS:
242
    return mkRationalNode(0);
243
1497
  case kind::MULT:
244
  case kind::NONLINEAR_MULT:
245
1497
    return mkRationalNode(1);
246
  default: Unreachable(); return {};  // silence warning
247
  }
248
}
249
250
3209561
inline Node safeConstructNary(NodeBuilder<>& nb) {
251
3209561
  switch (nb.getNumChildren()) {
252
    case 0:
253
      return getIdentity(nb.getKind());
254
2512186
    case 1:
255
2512186
      return nb[0];
256
697375
    default:
257
697375
      return (Node)nb;
258
  }
259
}
260
261
30770
inline Node safeConstructNary(Kind k, const std::vector<Node>& children) {
262
30770
  switch (children.size()) {
263
1497
    case 0:
264
1497
      return getIdentity(k);
265
12625
    case 1:
266
12625
      return children[0];
267
16648
    default:
268
16648
      return NodeManager::currentNM()->mkNode(k, children);
269
  }
270
}
271
272
// Returns the multiplication of a and b.
273
inline Node mkMult(Node a, Node b) {
274
  return NodeManager::currentNM()->mkNode(kind::MULT, a, b);
275
}
276
277
// Return a constraint that is equivalent to term being is in the range
278
// [start, end). This includes start and excludes end.
279
40
inline Node mkInRange(Node term, Node start, Node end) {
280
40
  NodeManager* nm = NodeManager::currentNM();
281
80
  Node above_start = nm->mkNode(kind::LEQ, start, term);
282
80
  Node below_end = nm->mkNode(kind::LT, term, end);
283
80
  return nm->mkNode(kind::AND, above_start, below_end);
284
}
285
286
// Creates an expression that constrains q to be equal to one of two expressions
287
// when n is 0 or not. Useful for division by 0 logic.
288
//   (ite (= n 0) (= q if_zero) (= q not_zero))
289
inline Node mkOnZeroIte(Node n, Node q, Node if_zero, Node not_zero) {
290
  Node zero = mkRationalNode(0);
291
  return n.eqNode(zero).iteNode(q.eqNode(if_zero), q.eqNode(not_zero));
292
}
293
294
1699
inline Node mkPi()
295
{
296
  return NodeManager::currentNM()->mkNullaryOperator(
297
1699
      NodeManager::currentNM()->realType(), kind::PI);
298
}
299
/** Join kinds, where k1 and k2 are arithmetic relations returns an
300
 * arithmetic relation ret such that
301
 * if (a <k1> b) and (a <k2> b), then (a <ret> b).
302
 */
303
Kind joinKinds(Kind k1, Kind k2);
304
305
/** Transitive kinds, where k1 and k2 are arithmetic relations returns an
306
 * arithmetic relation ret such that
307
 * if (a <k1> b) and (b <k2> c) then (a <ret> c).
308
 */
309
Kind transKinds(Kind k1, Kind k2);
310
311
/** Is k a transcendental function kind? */
312
bool isTranscendentalKind(Kind k);
313
/**
314
 * Get a lower/upper approximation of the constant r within the given
315
 * level of precision. In other words, this returns a constant c' such that
316
 *   c' <= c <= c' + 1/(10^prec) if isLower is true, or
317
 *   c' + 1/(10^prec) <= c <= c' if isLower is false.
318
 * where c' is a rational of the form n/d for some n and d <= 10^prec.
319
 */
320
Node getApproximateConstant(Node c, bool isLower, unsigned prec);
321
322
/** print rational approximation of cr with precision prec on trace c */
323
void printRationalApprox(const char* c, Node cr, unsigned prec = 5);
324
325
/** Arithmetic substitute
326
 *
327
 * This computes the substitution n { vars -> subs }, but with the caveat
328
 * that subterms of n that belong to a theory other than arithmetic are
329
 * not traversed. In other words, terms that belong to other theories are
330
 * treated as atomic variables. For example:
331
 *   (5*f(x) + 7*x ){ x -> 3 } returns 5*f(x) + 7*3.
332
 */
333
Node arithSubstitute(Node n, std::vector<Node>& vars, std::vector<Node>& subs);
334
335
/** Make the node u >= a ^ a >= l */
336
Node mkBounded(Node l, Node a, Node u);
337
338
Rational leastIntGreaterThan(const Rational&);
339
340
Rational greatestIntLessThan(const Rational&);
341
342
/** Negates a node in arithmetic proof normal form. */
343
Node negateProofLiteral(TNode n);
344
345
}/* CVC4::theory::arith namespace */
346
}/* CVC4::theory namespace */
347
}/* CVC4 namespace */
348
349
#endif /* CVC4__THEORY__ARITH__ARITH_UTILITIES_H */