GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/operator_elim.cpp Lines: 202 216 93.5 %
Date: 2021-03-22 Branches: 497 1019 48.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file operator_elim.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Andrew Reynolds, Andres Noetzli, 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 operator elimination for arithmetic
13
 **/
14
15
#include "theory/arith/operator_elim.h"
16
17
#include "expr/attribute.h"
18
#include "expr/bound_var_manager.h"
19
#include "expr/skolem_manager.h"
20
#include "expr/term_conversion_proof_generator.h"
21
#include "options/arith_options.h"
22
#include "smt/logic_exception.h"
23
#include "theory/arith/arith_utilities.h"
24
#include "theory/rewriter.h"
25
#include "theory/theory.h"
26
27
using namespace CVC4::kind;
28
29
namespace CVC4 {
30
namespace theory {
31
namespace arith {
32
33
/**
34
 * Attribute used for constructing unique bound variables that are binders
35
 * for witness terms below. In other words, this attribute maps nodes to
36
 * the bound variable of a witness term for eliminating that node.
37
 *
38
 * Notice we use the same attribute for most bound variables below, since using
39
 * a node itself is a sufficient cache key for constructing a bound variable.
40
 * The exception is to_int / is_int, which share a skolem based on their
41
 * argument.
42
 */
43
struct ArithWitnessVarAttributeId
44
{
45
};
46
using ArithWitnessVarAttribute = expr::Attribute<ArithWitnessVarAttributeId, Node>;
47
/**
48
 * Similar to above, shared for to_int and is_int. This is used for introducing
49
 * an integer bound variable used to construct the witness term for t in the
50
 * contexts (to_int t) and (is_int t).
51
 */
52
struct ToIntWitnessVarAttributeId
53
{
54
};
55
using ToIntWitnessVarAttribute
56
 = expr::Attribute<ToIntWitnessVarAttributeId, Node>;
57
58
8995
OperatorElim::OperatorElim(ProofNodeManager* pnm, const LogicInfo& info)
59
8995
    : EagerProofGenerator(pnm), d_info(info)
60
{
61
8995
}
62
63
717
void OperatorElim::checkNonLinearLogic(Node term)
64
{
65
717
  if (d_info.isLinear())
66
  {
67
12
    Trace("arith-logic") << "ERROR: Non-linear term in linear logic: " << term
68
6
                         << std::endl;
69
12
    std::stringstream serr;
70
6
    serr << "A non-linear fact was asserted to arithmetic in a linear logic."
71
6
         << std::endl;
72
6
    serr << "The fact in question: " << term << std::endl;
73
6
    throw LogicException(serr.str());
74
  }
75
711
}
76
77
697476
TrustNode OperatorElim::eliminate(Node n,
78
                                  std::vector<SkolemLemma>& lems,
79
                                  bool partialOnly)
80
{
81
697476
  TConvProofGenerator* tg = nullptr;
82
1394946
  Node nn = eliminateOperators(n, lems, tg, partialOnly);
83
697470
  if (nn != n)
84
  {
85
1757
    return TrustNode::mkTrustRewrite(n, nn, nullptr);
86
  }
87
695713
  return TrustNode::null();
88
}
89
90
697476
Node OperatorElim::eliminateOperators(Node node,
91
                                      std::vector<SkolemLemma>& lems,
92
                                      TConvProofGenerator* tg,
93
                                      bool partialOnly)
94
{
95
697476
  NodeManager* nm = NodeManager::currentNM();
96
697476
  BoundVarManager* bvm = nm->getBoundVarManager();
97
697476
  Kind k = node.getKind();
98
697476
  switch (k)
99
  {
100
    case TANGENT:
101
    case COSECANT:
102
    case SECANT:
103
    case COTANGENT:
104
    {
105
      // these are eliminated by rewriting
106
      return Rewriter::rewrite(node);
107
      break;
108
    }
109
32
    case TO_INTEGER:
110
    case IS_INTEGER:
111
    {
112
32
      if (partialOnly)
113
      {
114
        // not eliminating total operators
115
        return node;
116
      }
117
      // node[0] - 1 < toIntSkolem <= node[0]
118
      // -1 < toIntSkolem - node[0] <= 0
119
      // 0 <= node[0] - toIntSkolem < 1
120
      Node v =
121
64
          bvm->mkBoundVar<ToIntWitnessVarAttribute>(node[0], nm->integerType());
122
64
      Node one = mkRationalNode(1);
123
64
      Node zero = mkRationalNode(0);
124
64
      Node diff = nm->mkNode(MINUS, node[0], v);
125
64
      Node lem = mkInRange(diff, zero, one);
126
      Node toIntSkolem =
127
          mkWitnessTerm(v,
128
                        lem,
129
                        "toInt",
130
                        "a conversion of a Real term to its Integer part",
131
64
                        lems);
132
32
      if (k == IS_INTEGER)
133
      {
134
6
        return nm->mkNode(EQUAL, node[0], toIntSkolem);
135
      }
136
26
      Assert(k == TO_INTEGER);
137
26
      return toIntSkolem;
138
    }
139
140
1198
    case INTS_DIVISION_TOTAL:
141
    case INTS_MODULUS_TOTAL:
142
    {
143
1198
      if (partialOnly)
144
      {
145
        // not eliminating total operators
146
1200
        return node;
147
      }
148
1196
      Node den = Rewriter::rewrite(node[1]);
149
1196
      Node num = Rewriter::rewrite(node[0]);
150
1196
      Node rw = nm->mkNode(k, num, den);
151
1196
      Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->integerType());
152
1196
      Node lem;
153
1196
      Node leqNum = nm->mkNode(LEQ, nm->mkNode(MULT, den, v), num);
154
1196
      if (den.isConst())
155
      {
156
1007
        const Rational& rat = den.getConst<Rational>();
157
1007
        if (num.isConst() || rat == 0)
158
        {
159
          // just rewrite
160
          return Rewriter::rewrite(node);
161
        }
162
1007
        if (rat > 0)
163
        {
164
1007
          lem = nm->mkNode(
165
              AND,
166
              leqNum,
167
2014
              nm->mkNode(
168
                  LT,
169
                  num,
170
2014
                  nm->mkNode(MULT,
171
                             den,
172
2014
                             nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))));
173
        }
174
        else
175
        {
176
          lem = nm->mkNode(
177
              AND,
178
              leqNum,
179
              nm->mkNode(
180
                  LT,
181
                  num,
182
                  nm->mkNode(MULT,
183
                             den,
184
                             nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))));
185
        }
186
      }
187
      else
188
      {
189
189
        checkNonLinearLogic(node);
190
567
        lem = nm->mkNode(
191
            AND,
192
756
            nm->mkNode(
193
                IMPLIES,
194
378
                nm->mkNode(GT, den, nm->mkConst(Rational(0))),
195
378
                nm->mkNode(
196
                    AND,
197
                    leqNum,
198
378
                    nm->mkNode(
199
                        LT,
200
                        num,
201
378
                        nm->mkNode(
202
                            MULT,
203
                            den,
204
378
                            nm->mkNode(PLUS, v, nm->mkConst(Rational(1))))))),
205
756
            nm->mkNode(
206
                IMPLIES,
207
378
                nm->mkNode(LT, den, nm->mkConst(Rational(0))),
208
378
                nm->mkNode(
209
                    AND,
210
                    leqNum,
211
378
                    nm->mkNode(
212
                        LT,
213
                        num,
214
378
                        nm->mkNode(
215
                            MULT,
216
                            den,
217
378
                            nm->mkNode(PLUS, v, nm->mkConst(Rational(-1))))))));
218
      }
219
      Node intVar = mkWitnessTerm(
220
1196
          v, lem, "linearIntDiv", "the result of an intdiv-by-k term", lems);
221
1196
      if (k == INTS_MODULUS_TOTAL)
222
      {
223
1372
        Node nn = nm->mkNode(MINUS, num, nm->mkNode(MULT, den, intVar));
224
686
        return nn;
225
      }
226
      else
227
      {
228
510
        return intVar;
229
      }
230
      break;
231
    }
232
122
    case DIVISION_TOTAL:
233
    {
234
122
      if (partialOnly)
235
      {
236
        // not eliminating total operators
237
2
        return node;
238
      }
239
240
      Node num = Rewriter::rewrite(node[0]);
240
240
      Node den = Rewriter::rewrite(node[1]);
241
120
      if (den.isConst())
242
      {
243
        // No need to eliminate here, can eliminate via rewriting later.
244
        // Moreover, rewriting may change the type of this node from real to
245
        // int, which impacts certain issues with subtyping.
246
        return node;
247
      }
248
120
      checkNonLinearLogic(node);
249
240
      Node rw = nm->mkNode(k, num, den);
250
240
      Node v = bvm->mkBoundVar<ArithWitnessVarAttribute>(rw, nm->realType());
251
      Node lem = nm->mkNode(IMPLIES,
252
240
                            den.eqNode(nm->mkConst(Rational(0))).negate(),
253
480
                            nm->mkNode(MULT, den, v).eqNode(num));
254
      return mkWitnessTerm(
255
120
          v, lem, "nonlinearDiv", "the result of a non-linear div term", lems);
256
      break;
257
    }
258
154
    case DIVISION:
259
    {
260
308
      Node num = Rewriter::rewrite(node[0]);
261
308
      Node den = Rewriter::rewrite(node[1]);
262
308
      Node ret = nm->mkNode(DIVISION_TOTAL, num, den);
263
154
      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
264
      {
265
157
        checkNonLinearLogic(node);
266
290
        Node divByZeroNum = getArithSkolemApp(num, ArithSkolemId::DIV_BY_ZERO);
267
290
        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
268
145
        ret = nm->mkNode(ITE, denEq0, divByZeroNum, ret);
269
      }
270
148
      return ret;
271
      break;
272
    }
273
274
114
    case INTS_DIVISION:
275
    {
276
      // partial function: integer div
277
228
      Node num = Rewriter::rewrite(node[0]);
278
228
      Node den = Rewriter::rewrite(node[1]);
279
228
      Node ret = nm->mkNode(INTS_DIVISION_TOTAL, num, den);
280
114
      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
281
      {
282
114
        checkNonLinearLogic(node);
283
        Node intDivByZeroNum =
284
228
            getArithSkolemApp(num, ArithSkolemId::INT_DIV_BY_ZERO);
285
228
        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
286
114
        ret = nm->mkNode(ITE, denEq0, intDivByZeroNum, ret);
287
      }
288
114
      return ret;
289
      break;
290
    }
291
292
89
    case INTS_MODULUS:
293
    {
294
      // partial function: mod
295
178
      Node num = Rewriter::rewrite(node[0]);
296
178
      Node den = Rewriter::rewrite(node[1]);
297
178
      Node ret = nm->mkNode(INTS_MODULUS_TOTAL, num, den);
298
89
      if (!den.isConst() || den.getConst<Rational>().sgn() == 0)
299
      {
300
89
        checkNonLinearLogic(node);
301
178
        Node modZeroNum = getArithSkolemApp(num, ArithSkolemId::MOD_BY_ZERO);
302
178
        Node denEq0 = nm->mkNode(EQUAL, den, nm->mkConst(Rational(0)));
303
89
        ret = nm->mkNode(ITE, denEq0, modZeroNum, ret);
304
      }
305
89
      return ret;
306
      break;
307
    }
308
309
4
    case ABS:
310
    {
311
      return nm->mkNode(ITE,
312
8
                        nm->mkNode(LT, node[0], nm->mkConst(Rational(0))),
313
8
                        nm->mkNode(UMINUS, node[0]),
314
20
                        node[0]);
315
      break;
316
    }
317
54
    case SQRT:
318
    case ARCSINE:
319
    case ARCCOSINE:
320
    case ARCTANGENT:
321
    case ARCCOSECANT:
322
    case ARCSECANT:
323
    case ARCCOTANGENT:
324
    {
325
54
      if (partialOnly)
326
      {
327
        // not eliminating total operators
328
        return node;
329
      }
330
54
      checkNonLinearLogic(node);
331
      // eliminate inverse functions here
332
      Node var =
333
108
          bvm->mkBoundVar<ArithWitnessVarAttribute>(node, nm->realType());
334
108
      Node lem;
335
54
      if (k == SQRT)
336
      {
337
76
        Node skolemApp = getArithSkolemApp(node[0], ArithSkolemId::SQRT);
338
76
        Node uf = skolemApp.eqNode(var);
339
        Node nonNeg =
340
76
            nm->mkNode(AND, nm->mkNode(MULT, var, var).eqNode(node[0]), uf);
341
342
        // sqrt(x) reduces to:
343
        // witness y. ite(x >= 0.0, y * y = x ^ y = Uf(x), y = Uf(x))
344
        //
345
        // Uf(x) makes sure that the reduction still behaves like a function,
346
        // otherwise the reduction of (x = 1) ^ (sqrt(x) != sqrt(1)) would be
347
        // satisfiable. On the original formula, this would require that we
348
        // simultaneously interpret sqrt(1) as 1 and -1, which is not a valid
349
        // model.
350
114
        lem = nm->mkNode(ITE,
351
76
                         nm->mkNode(GEQ, node[0], nm->mkConst(Rational(0))),
352
                         nonNeg,
353
                         uf);
354
      }
355
      else
356
      {
357
32
        Node pi = mkPi();
358
359
        // range of the skolem
360
32
        Node rlem;
361
16
        if (k == ARCSINE || k == ARCTANGENT || k == ARCCOSECANT)
362
        {
363
24
          Node half = nm->mkConst(Rational(1) / Rational(2));
364
24
          Node pi2 = nm->mkNode(MULT, half, pi);
365
24
          Node npi2 = nm->mkNode(MULT, nm->mkConst(Rational(-1)), pi2);
366
          // -pi/2 < var <= pi/2
367
36
          rlem = nm->mkNode(
368
60
              AND, nm->mkNode(LT, npi2, var), nm->mkNode(LEQ, var, pi2));
369
        }
370
        else
371
        {
372
          // 0 <= var < pi
373
12
          rlem = nm->mkNode(AND,
374
8
                            nm->mkNode(LEQ, nm->mkConst(Rational(0)), var),
375
8
                            nm->mkNode(LT, var, pi));
376
        }
377
378
16
        Kind rk =
379
            k == ARCSINE
380
28
                ? SINE
381
                : (k == ARCCOSINE
382
20
                       ? COSINE
383
                       : (k == ARCTANGENT
384
8
                              ? TANGENT
385
                              : (k == ARCCOSECANT
386
                                     ? COSECANT
387
                                     : (k == ARCSECANT ? SECANT : COTANGENT))));
388
32
        Node invTerm = nm->mkNode(rk, var);
389
16
        lem = nm->mkNode(AND, rlem, invTerm.eqNode(node[0]));
390
      }
391
54
      Assert(!lem.isNull());
392
      return mkWitnessTerm(
393
          var,
394
          lem,
395
          "tfk",
396
          "Skolem to eliminate a non-standard transcendental function",
397
54
          lems);
398
      break;
399
    }
400
401
695709
    default: break;
402
  }
403
695709
  return node;
404
}
405
406
Node OperatorElim::getAxiomFor(Node n) { return Node::null(); }
407
408
386
Node OperatorElim::getArithSkolem(ArithSkolemId asi)
409
{
410
386
  std::map<ArithSkolemId, Node>::iterator it = d_arith_skolem.find(asi);
411
386
  if (it == d_arith_skolem.end())
412
  {
413
196
    NodeManager* nm = NodeManager::currentNM();
414
415
392
    TypeNode tn;
416
392
    std::string name;
417
392
    std::string desc;
418
196
    switch (asi)
419
    {
420
90
      case ArithSkolemId::DIV_BY_ZERO:
421
90
        tn = nm->realType();
422
90
        name = std::string("divByZero");
423
90
        desc = std::string("partial real division");
424
90
        break;
425
59
      case ArithSkolemId::INT_DIV_BY_ZERO:
426
59
        tn = nm->integerType();
427
59
        name = std::string("intDivByZero");
428
59
        desc = std::string("partial int division");
429
59
        break;
430
33
      case ArithSkolemId::MOD_BY_ZERO:
431
33
        tn = nm->integerType();
432
33
        name = std::string("modZero");
433
33
        desc = std::string("partial modulus");
434
33
        break;
435
14
      case ArithSkolemId::SQRT:
436
14
        tn = nm->realType();
437
14
        name = std::string("sqrtUf");
438
14
        desc = std::string("partial sqrt");
439
14
        break;
440
      default: Unhandled();
441
    }
442
443
392
    Node skolem;
444
784
    if (options::arithNoPartialFun())
445
    {
446
      // partial function: division
447
4
      skolem = nm->mkSkolem(name, tn, desc, NodeManager::SKOLEM_EXACT_NAME);
448
    }
449
    else
450
    {
451
      // partial function: division
452
192
      skolem = nm->mkSkolem(name,
453
384
                            nm->mkFunctionType(tn, tn),
454
                            desc,
455
                            NodeManager::SKOLEM_EXACT_NAME);
456
    }
457
196
    d_arith_skolem[asi] = skolem;
458
196
    return skolem;
459
  }
460
190
  return it->second;
461
}
462
463
386
Node OperatorElim::getArithSkolemApp(Node n, ArithSkolemId asi)
464
{
465
386
  Node skolem = getArithSkolem(asi);
466
386
  if (!options::arithNoPartialFun())
467
  {
468
378
    skolem = NodeManager::currentNM()->mkNode(APPLY_UF, skolem, n);
469
  }
470
386
  return skolem;
471
}
472
473
1402
Node OperatorElim::mkWitnessTerm(Node v,
474
                                 Node pred,
475
                                 const std::string& prefix,
476
                                 const std::string& comment,
477
                                 std::vector<SkolemLemma>& lems)
478
{
479
1402
  NodeManager* nm = NodeManager::currentNM();
480
1402
  SkolemManager* sm = nm->getSkolemManager();
481
  // we mark that we should send a lemma
482
  Node k =
483
1402
      sm->mkSkolem(v, pred, prefix, comment, NodeManager::SKOLEM_DEFAULT, this);
484
1402
  if (d_pnm != nullptr)
485
  {
486
474
    Node lem = SkolemLemma::getSkolemLemmaFor(k);
487
    TrustNode tlem =
488
474
        mkTrustNode(lem, PfRule::THEORY_PREPROCESS_LEMMA, {}, {lem});
489
237
    lems.push_back(SkolemLemma(tlem, k));
490
  }
491
  else
492
  {
493
1165
    lems.push_back(SkolemLemma(k, nullptr));
494
  }
495
1402
  return k;
496
}
497
498
}  // namespace arith
499
}  // namespace theory
500
27264
}  // namespace CVC4