GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/normal_form.cpp Lines: 641 793 80.8 %
Date: 2021-03-23 Branches: 1088 2958 36.8 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file normal_form.cpp
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Gereon Kremer, 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 [[ Add one-line brief description here ]]
13
 **
14
 ** [[ Add lengthier description here ]]
15
 ** \todo document this file
16
 **/
17
#include "theory/arith/normal_form.h"
18
19
#include <list>
20
21
#include "base/output.h"
22
#include "theory/arith/arith_utilities.h"
23
#include "theory/theory.h"
24
25
using namespace std;
26
27
namespace CVC4 {
28
namespace theory {
29
namespace arith {
30
31
128962562
Constant Constant::mkConstant(const Rational& rat) {
32
128962562
  return Constant(mkRationalNode(rat));
33
}
34
35
size_t Variable::getComplexity() const{
36
  return 1u;
37
}
38
39
size_t VarList::getComplexity() const{
40
  if(empty()){
41
    return 1;
42
  }else if(singleton()){
43
    return 1;
44
  }else{
45
    return size() + 1;
46
  }
47
}
48
49
size_t Monomial::getComplexity() const{
50
  return getConstant().getComplexity() + getVarList().getComplexity();
51
}
52
53
size_t Polynomial::getComplexity() const{
54
  size_t cmp = 0;
55
  iterator i = begin(), e = end();
56
  for(; i != e; ++i){
57
    Monomial m = *i;
58
    cmp += m.getComplexity();
59
  }
60
  return cmp;
61
}
62
63
size_t Constant::getComplexity() const{
64
  return getValue().complexity();
65
}
66
67
179537153
bool Variable::isLeafMember(Node n){
68
538611459
  return (!isRelationOperator(n.getKind())) &&
69
538611459
    (Theory::isLeafOf(n, theory::THEORY_ARITH));
70
}
71
72
156919353
VarList::VarList(Node n) : NodeWrapper(n) { Assert(isSorted(begin(), end())); }
73
74
325184
bool Variable::isIAndMember(Node n)
75
{
76
975552
  return n.getKind() == kind::IAND && Polynomial::isMember(n[0])
77
1300736
         && Polynomial::isMember(n[1]);
78
}
79
80
195198
bool Variable::isDivMember(Node n){
81
195198
  switch(n.getKind()){
82
112595
  case kind::DIVISION:
83
  case kind::INTS_DIVISION:
84
  case kind::INTS_MODULUS:
85
  case kind::DIVISION_TOTAL:
86
  case kind::INTS_DIVISION_TOTAL:
87
  case kind::INTS_MODULUS_TOTAL:
88
112595
    return Polynomial::isMember(n[0]) && Polynomial::isMember(n[1]);
89
82603
  default:
90
82603
    return false;
91
  }
92
}
93
94
2141558
bool Variable::isTranscendentalMember(Node n) {
95
2141558
  switch(n.getKind()){
96
1290987
  case kind::EXPONENTIAL:
97
  case kind::SINE:
98
  case kind::COSINE:
99
  case kind::TANGENT:
100
  case kind::COSECANT:
101
  case kind::SECANT:
102
  case kind::COTANGENT:
103
  case kind::ARCSINE:
104
  case kind::ARCCOSINE:
105
  case kind::ARCTANGENT:
106
  case kind::ARCCOSECANT:
107
  case kind::ARCSECANT:
108
  case kind::ARCCOTANGENT:
109
1290987
  case kind::SQRT: return Polynomial::isMember(n[0]);
110
850571
  case kind::PI:
111
850571
    return true;
112
  default:
113
    return false;
114
  }
115
}
116
117
118
161032142
bool VarList::isSorted(iterator start, iterator end) {
119
161032142
  return std::is_sorted(start, end);
120
}
121
122
119637774
bool VarList::isMember(Node n) {
123
119637774
  if(Variable::isMember(n)) {
124
88734212
    return true;
125
  }
126
30903562
  if(n.getKind() == kind::NONLINEAR_MULT) {
127
3699707
    Node::iterator curr = n.begin(), end = n.end();
128
7399414
    Node prev = *curr;
129
3699707
    if(!Variable::isMember(prev)) return false;
130
131
    Variable::VariableNodeCmp cmp;
132
133
13754327
    while( (++curr) != end) {
134
5027310
      if(!Variable::isMember(*curr)) return false;
135
      // prev <= curr : accept
136
      // !(prev <= curr) : reject
137
      // !(!(prev > curr)) : reject
138
      // curr < prev : reject
139
5027310
      if((cmp(*curr, prev))) return false;
140
5027310
      prev = *curr;
141
    }
142
3699707
    return true;
143
  } else {
144
27203855
    return false;
145
  }
146
}
147
148
101453171
int VarList::cmp(const VarList& vl) const {
149
101453171
  int dif = this->size() - vl.size();
150
101453171
  if (dif == 0) {
151
72671558
    if(this->getNode() == vl.getNode()) {
152
9991374
      return 0;
153
    }
154
155
62680184
    Assert(!empty());
156
62680184
    Assert(!vl.empty());
157
62680184
    if(this->size() == 1){
158
59579991
      return Variable::VariableNodeCmp::cmp(this->getNode(), vl.getNode());
159
    }
160
161
162
6200386
    internal_iterator ii=this->internalBegin(), ie=this->internalEnd();
163
6200386
    internal_iterator ci=vl.internalBegin(), ce=vl.internalEnd();
164
11662367
    for(; ii != ie; ++ii, ++ci){
165
8808309
      Node vi = *ii;
166
8808309
      Node vc = *ci;
167
5954251
      int tmp = Variable::VariableNodeCmp::cmp(vi, vc);
168
5954251
      if(tmp != 0){
169
3100193
        return tmp;
170
      }
171
    }
172
    Unreachable();
173
28781613
  } else if(dif < 0) {
174
16455349
    return -1;
175
  } else {
176
12326264
    return 1;
177
  }
178
}
179
180
156919353
VarList VarList::parseVarList(Node n) {
181
156919353
  return VarList(n);
182
  // if(Variable::isMember(n)) {
183
  //   return VarList(Variable(n));
184
  // } else {
185
  //   Assert(n.getKind() == kind::MULT);
186
  //   for(Node::iterator i=n.begin(), end = n.end(); i!=end; ++i) {
187
  //     Assert(Variable::isMember(*i));
188
  //   }
189
  //   return VarList(n);
190
  // }
191
}
192
193
1288452
VarList VarList::operator*(const VarList& other) const {
194
1288452
  if(this->empty()) {
195
1152073
    return other;
196
136379
  } else if(other.empty()) {
197
89769
    return *this;
198
  } else {
199
93220
    vector<Node> result;
200
201
    internal_iterator
202
93220
      thisBegin = this->internalBegin(),
203
93220
      thisEnd = this->internalEnd(),
204
93220
      otherBegin = other.internalBegin(),
205
93220
      otherEnd = other.internalEnd();
206
207
    Variable::VariableNodeCmp cmp;
208
46610
    std::merge(thisBegin, thisEnd, otherBegin, otherEnd, std::back_inserter(result), cmp);
209
210
46610
    Assert(result.size() >= 2);
211
93220
    Node mult = NodeManager::currentNM()->mkNode(kind::NONLINEAR_MULT, result);
212
46610
    return VarList::parseVarList(mult);
213
  }
214
}
215
216
136378733
bool Monomial::isMember(TNode n){
217
136378733
  if(n.getKind() == kind::CONST_RATIONAL) {
218
20275673
    return true;
219
116103060
  } else if(multStructured(n)) {
220
20774092
    return VarList::isMember(n[1]);
221
  } else {
222
95328968
    return VarList::isMember(n);
223
  }
224
}
225
226
60808341
Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl) {
227
60808341
  if(c.isZero() || vl.empty() ) {
228
4405624
    return Monomial(c);
229
56402717
  } else if(c.isOne()) {
230
1308519
    return Monomial(vl);
231
  } else {
232
55094198
    return Monomial(c, vl);
233
  }
234
}
235
236
69004
Monomial Monomial::mkMonomial(const VarList& vl) {
237
  // acts like Monomial::mkMonomial( 1, vl)
238
69004
  if( vl.empty() ) {
239
    return Monomial::mkOne();
240
  } else if(true){
241
69004
    return Monomial(vl);
242
  }
243
}
244
245
191839314
Monomial Monomial::parseMonomial(Node n) {
246
191839314
  if(n.getKind() == kind::CONST_RATIONAL) {
247
34966605
    return Monomial(Constant(n));
248
156872709
  } else if(multStructured(n)) {
249
51874482
    return Monomial::mkMonomial(Constant(n[0]),VarList::parseVarList(n[1]));
250
  } else {
251
104998227
    return Monomial(VarList::parseVarList(n));
252
  }
253
}
254
6218725
Monomial Monomial::operator*(const Rational& q) const {
255
6218725
  if(q.isZero()){
256
    return mkZero();
257
  }else{
258
12437450
    Constant newConstant = this->getConstant() * q;
259
6218725
    return Monomial::mkMonomial(newConstant, getVarList());
260
  }
261
}
262
263
Monomial Monomial::operator*(const Constant& c) const {
264
  return (*this) * c.getValue();
265
  // if(c.isZero()){
266
  //   return mkZero();
267
  // }else{
268
  //   Constant newConstant = this->getConstant() * c;
269
  //   return Monomial::mkMonomial(newConstant, getVarList());
270
  // }
271
}
272
273
1288452
Monomial Monomial::operator*(const Monomial& mono) const {
274
2576904
  Constant newConstant = this->getConstant() * mono.getConstant();
275
2576904
  VarList newVL = this->getVarList() * mono.getVarList();
276
277
2576904
  return Monomial::mkMonomial(newConstant, newVL);
278
}
279
280
// vector<Monomial> Monomial::sumLikeTerms(const std::vector<Monomial> & monos)
281
// {
282
//   Assert(isSorted(monos));
283
//   vector<Monomial> outMonomials;
284
//   typedef vector<Monomial>::const_iterator iterator;
285
//   for(iterator rangeIter = monos.begin(), end=monos.end(); rangeIter != end;)
286
//   {
287
//     Rational constant = (*rangeIter).getConstant().getValue();
288
//     VarList varList  = (*rangeIter).getVarList();
289
//     ++rangeIter;
290
//     while(rangeIter != end && varList == (*rangeIter).getVarList()) {
291
//       constant += (*rangeIter).getConstant().getValue();
292
//       ++rangeIter;
293
//     }
294
//     if(constant != 0) {
295
//       Constant asConstant = Constant::mkConstant(constant);
296
//       Monomial nonZero = Monomial::mkMonomial(asConstant, varList);
297
//       outMonomials.push_back(nonZero);
298
//     }
299
//   }
300
301
//   Assert(isStrictlySorted(outMonomials));
302
//   return outMonomials;
303
// }
304
305
2714595
void Monomial::sort(std::vector<Monomial>& m){
306
2714595
  if(!isSorted(m)){
307
120607
    std::sort(m.begin(), m.end());
308
  }
309
2714595
}
310
311
7645026
void Monomial::combineAdjacentMonomials(std::vector<Monomial>& monos) {
312
7645026
  Assert(isSorted(monos));
313
  size_t writePos, readPos, N;
314
24206958
  for(writePos = 0, readPos = 0, N = monos.size(); readPos < N;){
315
16561932
    Monomial& atRead = monos[readPos];
316
16561932
    const VarList& varList  = atRead.getVarList();
317
318
16561932
    size_t rangeEnd = readPos+1;
319
23161016
    for(; rangeEnd < N; rangeEnd++){
320
12225452
      if(!(varList == monos[rangeEnd].getVarList())){ break; }
321
    }
322
    // monos[i] for i in [readPos, rangeEnd) has the same var list
323
16561932
    if(readPos+1 == rangeEnd){ // no addition needed
324
13403423
      if(!atRead.getConstant().isZero()){
325
23738146
        Monomial cpy = atRead; // being paranoid here
326
11869073
        monos[writePos] = cpy;
327
11869073
        writePos++;
328
      }
329
    }else{
330
6317018
      Rational constant(monos[readPos].getConstant().getValue());
331
6458051
      for(size_t i=readPos+1; i < rangeEnd; ++i){
332
3299542
        constant += monos[i].getConstant().getValue();
333
      }
334
3158509
      if(!constant.isZero()){
335
2851904
        Constant asConstant = Constant::mkConstant(constant);
336
2851904
        Monomial nonZero = Monomial::mkMonomial(asConstant, varList);
337
1425952
        monos[writePos] = nonZero;
338
1425952
        writePos++;
339
      }
340
    }
341
16561932
    Assert(rangeEnd > readPos);
342
16561932
    readPos = rangeEnd;
343
  }
344
7645026
  if(writePos > 0 ){
345
13419364
    Monomial cp = monos[0];
346
6709682
    Assert(writePos <= N);
347
6709682
    monos.resize(writePos, cp);
348
  }else{
349
935344
    monos.clear();
350
  }
351
7645026
  Assert(isStrictlySorted(monos));
352
7645026
}
353
354
void Monomial::print() const {
355
  Debug("normal-form") <<  getNode() << std::endl;
356
}
357
358
void Monomial::printList(const std::vector<Monomial>& list) {
359
  for(vector<Monomial>::const_iterator i = list.begin(), end = list.end(); i != end; ++i) {
360
    const Monomial& m =*i;
361
    m.print();
362
  }
363
}
364
6086908
Polynomial Polynomial::operator+(const Polynomial& vl) const {
365
366
12173816
  std::vector<Monomial> sortedMonos;
367
6086908
  std::merge(begin(), end(), vl.begin(), vl.end(), std::back_inserter(sortedMonos));
368
369
6086908
  Monomial::combineAdjacentMonomials(sortedMonos);
370
  //std::vector<Monomial> combined = Monomial::sumLikeTerms(sortedMonos);
371
372
6086908
  Polynomial result = mkPolynomial(sortedMonos);
373
12173816
  return result;
374
}
375
376
Polynomial Polynomial::exactDivide(const Integer& z) const {
377
  Assert(isIntegral());
378
  if(z.isOne()){
379
    return (*this);
380
  }else {
381
    Constant invz = Constant::mkConstant(Rational(1,z));
382
    Polynomial prod = (*this) * Monomial::mkMonomial(invz);
383
    Assert(prod.isIntegral());
384
    return prod;
385
  }
386
}
387
388
1568254
Polynomial Polynomial::sumPolynomials(const std::vector<Polynomial>& ps){
389
1568254
  if(ps.empty()){
390
    return mkZero();
391
1568254
  }else if(ps.size() <= 4){
392
    // if there are few enough polynomials just add them
393
3118500
    Polynomial p = ps[0];
394
1734712
    for(size_t i = 1; i < ps.size(); ++i){
395
175462
      p = p + ps[i];
396
    }
397
1559250
    return p;
398
  }else{
399
    // general case
400
18008
    std::map<Node, Rational> coeffs;
401
73850
    for(size_t i = 0, N = ps.size(); i<N; ++i){
402
64846
      const Polynomial& p = ps[i];
403
234101
      for(iterator pi = p.begin(), pend = p.end(); pi != pend; ++pi) {
404
338510
        Monomial m = *pi;
405
169255
        coeffs[m.getVarList().getNode()] += m.getConstant().getValue();
406
      }
407
    }
408
18008
    std::vector<Monomial> monos;
409
9004
    std::map<Node, Rational>::const_iterator ci = coeffs.begin(), cend = coeffs.end();
410
146660
    for(; ci != cend; ++ci){
411
68828
      if(!(*ci).second.isZero()){
412
        Constant c = Constant::mkConstant((*ci).second);
413
        Node n = (*ci).first;
414
        VarList vl = VarList::parseVarList(n);
415
        monos.push_back(Monomial::mkMonomial(c, vl));
416
      }
417
    }
418
9004
    Monomial::sort(monos);
419
9004
    Monomial::combineAdjacentMonomials(monos);
420
421
18008
    Polynomial result = mkPolynomial(monos);
422
9004
    return result;
423
  }
424
}
425
426
2462958
Polynomial Polynomial::operator-(const Polynomial& vl) const {
427
4925916
  Constant negOne = Constant::mkConstant(Rational(-1));
428
429
4925916
  return *this + (vl*negOne);
430
}
431
432
5744437
Polynomial Polynomial::operator*(const Rational& q) const{
433
5744437
  if(q.isZero()){
434
    return Polynomial::mkZero();
435
5744437
  }else if(q.isOne()){
436
1840891
    return *this;
437
  }else{
438
7807092
    std::vector<Monomial> newMonos;
439
9328666
    for(iterator i = this->begin(), end = this->end(); i != end; ++i) {
440
5425120
      newMonos.push_back((*i)*q);
441
    }
442
443
3903546
    Assert(Monomial::isStrictlySorted(newMonos));
444
3903546
    return Polynomial::mkPolynomial(newMonos);
445
  }
446
}
447
448
3686106
Polynomial Polynomial::operator*(const Constant& c) const{
449
3686106
  return (*this) * c.getValue();
450
  // if(c.isZero()){
451
  //   return Polynomial::mkZero();
452
  // }else if(c.isOne()){
453
  //   return *this;
454
  // }else{
455
  //   std::vector<Monomial> newMonos;
456
  //   for(iterator i = this->begin(), end = this->end(); i != end; ++i) {
457
  //     newMonos.push_back((*i)*c);
458
  //   }
459
460
  //   Assert(Monomial::isStrictlySorted(newMonos));
461
  //   return Polynomial::mkPolynomial(newMonos);
462
  // }
463
}
464
465
1156713
Polynomial Polynomial::operator*(const Monomial& mono) const {
466
1156713
  if(mono.isZero()) {
467
236
    return Polynomial(mono); //Don't multiply by zero
468
  } else {
469
2312954
    std::vector<Monomial> newMonos;
470
2444929
    for(iterator i = this->begin(), end = this->end(); i != end; ++i) {
471
1288452
      newMonos.push_back(mono * (*i));
472
    }
473
474
    // We may need to sort newMonos.
475
    // Suppose this = (+ x y), mono = x, (* x y).getId() < (* x x).getId()
476
    // newMonos = <(* x x), (* x y)> after this loop.
477
    // This is not sorted according to the current VarList order.
478
1156477
    Monomial::sort(newMonos);
479
1156477
    return Polynomial::mkPolynomial(newMonos);
480
  }
481
}
482
483
1105808
Polynomial Polynomial::operator*(const Polynomial& poly) const {
484
1105808
  Polynomial res = Polynomial::mkZero();
485
2262521
  for(iterator i = this->begin(), end = this->end(); i != end; ++i) {
486
2313426
    Monomial curr = *i;
487
2313426
    Polynomial prod = poly * curr;
488
2313426
    Polynomial sum  = res + prod;
489
1156713
    res = sum;
490
  }
491
1105808
  return res;
492
}
493
494
3755380
Monomial Polynomial::selectAbsMinimum() const {
495
7510760
  iterator iter = begin(), myend = end();
496
3755380
  Assert(iter != myend);
497
498
3755380
  Monomial min = *iter;
499
3755380
  ++iter;
500
6580774
  for(; iter != end(); ++iter){
501
2825394
    Monomial curr = *iter;
502
1412697
    if(curr.absCmp(min) < 0){
503
70279
      min = curr;
504
    }
505
  }
506
7510760
  return min;
507
}
508
509
1889583
bool Polynomial::leadingCoefficientIsAbsOne() const {
510
1889583
  return getHead().absCoefficientIsOne();
511
}
512
5809807
bool Polynomial::leadingCoefficientIsPositive() const {
513
5809807
  return getHead().getConstant().isPositive();
514
}
515
516
3258780
bool Polynomial::denominatorLCMIsOne() const {
517
3258780
  return denominatorLCM().isOne();
518
}
519
520
3258780
bool Polynomial::numeratorGCDIsOne() const {
521
3258780
  return gcd().isOne();
522
}
523
524
3477180
Integer Polynomial::gcd() const {
525
3477180
  Assert(isIntegral());
526
3477180
  return numeratorGCD();
527
}
528
529
7576813
Integer Polynomial::numeratorGCD() const {
530
  //We'll use the standardization that gcd(0, 0) = 0
531
  //So that the gcd of the zero polynomial is gcd{0} = 0
532
15153626
  iterator i=begin(), e=end();
533
7576813
  Assert(i != e);
534
535
7576813
  Integer d = (*i).getConstant().getValue().getNumerator().abs();
536
7576813
  if(d.isOne()){
537
7314483
    return d;
538
  }
539
262330
  ++i;
540
444324
  for(; i!=e; ++i){
541
362451
    Integer c = (*i).getConstant().getValue().getNumerator();
542
271454
    d = d.gcd(c);
543
271454
    if(d.isOne()){
544
180457
      return d;
545
    }
546
  }
547
81873
  return d;
548
}
549
550
7358413
Integer Polynomial::denominatorLCM() const {
551
7358413
  Integer tmp(1);
552
18200565
  for (iterator i = begin(), e = end(); i != e; ++i) {
553
21684304
    const Integer denominator = (*i).getConstant().getValue().getDenominator();
554
10842152
    tmp = tmp.lcm(denominator);
555
  }
556
7358413
  return tmp;
557
}
558
559
4100083
Constant Polynomial::getCoefficient(const VarList& vl) const{
560
  //TODO improve to binary search...
561
10837076
  for(iterator iter=begin(), myend=end(); iter != myend; ++iter){
562
13526571
    Monomial m = *iter;
563
13526571
    VarList curr = m.getVarList();
564
6789578
    if(curr == vl){
565
52585
      return m.getConstant();
566
    }
567
  }
568
4047498
  return Constant::mkConstant(0);
569
}
570
571
190
Node Polynomial::computeQR(const Polynomial& p, const Integer& div){
572
190
  Assert(p.isIntegral());
573
380
  std::vector<Monomial> q_vec, r_vec;
574
380
  Integer tmp_q, tmp_r;
575
658
  for(iterator iter = p.begin(), pend = p.end(); iter != pend; ++iter){
576
936
    Monomial curr = *iter;
577
936
    VarList vl = curr.getVarList();
578
936
    Constant c = curr.getConstant();
579
580
936
    const Integer& a = c.getValue().getNumerator();
581
468
    Integer::floorQR(tmp_q, tmp_r, a, div);
582
936
    Constant q=Constant::mkConstant(tmp_q);
583
936
    Constant r=Constant::mkConstant(tmp_r);
584
468
    if(!q.isZero()){
585
468
      q_vec.push_back(Monomial::mkMonomial(q, vl));
586
    }
587
468
    if(!r.isZero()){
588
262
      r_vec.push_back(Monomial::mkMonomial(r, vl));
589
    }
590
  }
591
592
380
  Polynomial p_q = Polynomial::mkPolynomial(q_vec);
593
380
  Polynomial p_r = Polynomial::mkPolynomial(r_vec);
594
595
380
  return NodeManager::currentNM()->mkNode(kind::PLUS, p_q.getNode(), p_r.getNode());
596
}
597
598
599
719758
Monomial Polynomial::minimumVariableMonomial() const{
600
719758
  Assert(!isConstant());
601
719758
  if(singleton()){
602
442620
    return getHead();
603
  }else{
604
554276
    iterator i = begin();
605
554276
    Monomial first = *i;
606
277138
    if( first.isConstant() ){
607
190854
      ++i;
608
190854
      Assert(i != end());
609
190854
      return *i;
610
    }else{
611
86284
      return first;
612
    }
613
  }
614
}
615
616
1105598
bool Polynomial::variableMonomialAreStrictlyGreater(const Monomial& m) const{
617
1105598
  if(isConstant()){
618
454844
    return true;
619
  }else{
620
1301508
    Monomial minimum = minimumVariableMonomial();
621
650754
    Debug("nf::tmp") << "minimum " << minimum.getNode() << endl;
622
650754
    Debug("nf::tmp") << "m " << m.getNode() << endl;
623
650754
    return m < minimum;
624
  }
625
}
626
627
51652856
bool Polynomial::isMember(TNode n) {
628
51652856
  if(Monomial::isMember(n)){
629
37868608
    return true;
630
13784248
  }else if(n.getKind() == kind::PLUS){
631
13784248
    Assert(n.getNumChildren() >= 2);
632
13784248
    Node::iterator currIter = n.begin(), end = n.end();
633
27568496
    Node prev = *currIter;
634
13784248
    if(!Monomial::isMember(prev)){
635
      return false;
636
    }
637
638
27568496
    Monomial mprev = Monomial::parseMonomial(prev);
639
13784248
    ++currIter;
640
53645354
    for(; currIter != end; ++currIter){
641
39861106
      Node curr = *currIter;
642
19930553
      if(!Monomial::isMember(curr)){
643
        return false;
644
      }
645
39861106
      Monomial mcurr = Monomial::parseMonomial(curr);
646
19930553
      if(!(mprev < mcurr)){
647
        return false;
648
      }
649
19930553
      mprev = mcurr;
650
    }
651
13784248
    return true;
652
  } else {
653
    return false;
654
  }
655
}
656
657
190
Node SumPair::computeQR(const SumPair& sp, const Integer& div){
658
190
  Assert(sp.isIntegral());
659
660
380
  const Integer& constant = sp.getConstant().getValue().getNumerator();
661
662
380
  Integer constant_q, constant_r;
663
190
  Integer::floorQR(constant_q, constant_r, constant, div);
664
665
380
  Node p_qr = Polynomial::computeQR(sp.getPolynomial(), div);
666
190
  Assert(p_qr.getKind() == kind::PLUS);
667
190
  Assert(p_qr.getNumChildren() == 2);
668
669
380
  Polynomial p_q = Polynomial::parsePolynomial(p_qr[0]);
670
380
  Polynomial p_r = Polynomial::parsePolynomial(p_qr[1]);
671
672
380
  SumPair sp_q(p_q, Constant::mkConstant(constant_q));
673
380
  SumPair sp_r(p_r, Constant::mkConstant(constant_r));
674
675
380
  return NodeManager::currentNM()->mkNode(kind::PLUS, sp_q.getNode(), sp_r.getNode());
676
}
677
678
1385744
SumPair SumPair::mkSumPair(const Polynomial& p){
679
1385744
  if(p.isConstant()){
680
    Constant leadingConstant = p.getHead().getConstant();
681
    return SumPair(Polynomial::mkZero(), leadingConstant);
682
1385744
  }else if(p.containsConstant()){
683
849416
    Assert(!p.singleton());
684
849416
    return SumPair(p.getTail(), p.getHead().getConstant());
685
  }else{
686
536328
    return SumPair(p, Constant::mkZero());
687
  }
688
}
689
690
4267495
Comparison::Comparison(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); }
691
692
33674
SumPair Comparison::toSumPair() const {
693
33674
  Kind cmpKind = comparisonKind();
694
33674
  switch(cmpKind){
695
  case kind::LT:
696
  case kind::LEQ:
697
  case kind::GT:
698
  case kind::GEQ:
699
    {
700
      TNode lit = getNode();
701
      TNode atom = (cmpKind == kind::LT || cmpKind == kind::LEQ) ? lit[0] : lit;
702
      Polynomial p = Polynomial::parsePolynomial(atom[0]);
703
      Constant c = Constant::mkConstant(atom[1]);
704
      if(p.leadingCoefficientIsPositive()){
705
        return SumPair(p, -c);
706
      }else{
707
        return SumPair(-p, c);
708
      }
709
    }
710
33674
  case kind::EQUAL:
711
  case kind::DISTINCT:
712
    {
713
67348
      Polynomial left = getLeft();
714
67348
      Polynomial right = getRight();
715
33674
      Debug("nf::tmp") << "left: " << left.getNode() << endl;
716
33674
      Debug("nf::tmp") << "right: " << right.getNode() << endl;
717
33674
      if(right.isConstant()){
718
13549
        return SumPair(left, -right.getHead().getConstant());
719
20125
      }else if(right.containsConstant()){
720
8776
        Assert(!right.singleton());
721
722
17552
        Polynomial noConstant = right.getTail();
723
8776
        return SumPair(left - noConstant, -right.getHead().getConstant());
724
      }else{
725
11349
        return SumPair(left - right, Constant::mkZero());
726
      }
727
    }
728
    default: Unhandled() << cmpKind;
729
  }
730
}
731
732
977865
Polynomial Comparison::normalizedVariablePart() const {
733
977865
  Kind cmpKind = comparisonKind();
734
977865
  switch(cmpKind){
735
545121
  case kind::LT:
736
  case kind::LEQ:
737
  case kind::GT:
738
  case kind::GEQ:
739
    {
740
1090242
      TNode lit = getNode();
741
1090242
      TNode atom = (cmpKind == kind::LT || cmpKind == kind::LEQ) ? lit[0] : lit;
742
1090242
      Polynomial p = Polynomial::parsePolynomial(atom[0]);
743
545121
      if(p.leadingCoefficientIsPositive()){
744
449124
        return p;
745
      }else{
746
95997
        return -p;
747
      }
748
    }
749
432744
  case kind::EQUAL:
750
  case kind::DISTINCT:
751
    {
752
865488
      Polynomial left = getLeft();
753
865488
      Polynomial right = getRight();
754
432744
      if(right.isConstant()){
755
198832
        return left;
756
      }else{
757
467824
        Polynomial noConstant = right.containsConstant() ? right.getTail() : right;
758
467824
        Polynomial diff = left - noConstant;
759
233912
        if(diff.leadingCoefficientIsPositive()){
760
231596
          return diff;
761
        }else{
762
2316
          return -diff;
763
        }
764
      }
765
    }
766
    default: Unhandled() << cmpKind;
767
  }
768
}
769
770
976485
DeltaRational Comparison::normalizedDeltaRational() const {
771
976485
  Kind cmpKind = comparisonKind();
772
976485
  int delta = deltaCoeff(cmpKind);
773
976485
  switch(cmpKind){
774
543958
  case kind::LT:
775
  case kind::LEQ:
776
  case kind::GT:
777
  case kind::GEQ:
778
    {
779
1087916
      Node lit = getNode();
780
1087916
      Node atom = (cmpKind == kind::LT || cmpKind == kind::LEQ) ? lit[0] : lit;
781
1087916
      Polynomial left = Polynomial::parsePolynomial(atom[0]);
782
543958
      const Rational& q = atom[1].getConst<Rational>();
783
543958
      if(left.leadingCoefficientIsPositive()){
784
448169
        return DeltaRational(q, delta);
785
      }else{
786
95789
        return DeltaRational(-q, -delta);
787
      }
788
    }
789
432527
  case kind::EQUAL:
790
  case kind::DISTINCT:
791
    {
792
865054
      Polynomial right = getRight();
793
865054
      Monomial firstRight = right.getHead();
794
432527
      if(firstRight.isConstant()){
795
494040
        DeltaRational c = DeltaRational(firstRight.getConstant().getValue(), 0);
796
494040
        Polynomial left = getLeft();
797
247020
        if(!left.allIntegralVariables()){
798
21980
          return c;
799
          //this is a qpolynomial and the sign of the leading
800
          //coefficient will not change after the diff below
801
        } else{
802
          // the polynomial may be a z polynomial in which case
803
          // taking the diff is the simplest and obviously correct means
804
450080
          Polynomial diff = right.singleton() ? left : left - right.getTail();
805
225040
          if(diff.leadingCoefficientIsPositive()){
806
224648
            return c;
807
          }else{
808
392
            return -c;
809
          }
810
        }
811
      }else{ // The constant is 0 sign cannot change
812
185507
        return DeltaRational(0, 0);
813
      }
814
    }
815
    default: Unhandled() << cmpKind;
816
  }
817
}
818
819
304712
std::tuple<Polynomial, Kind, Constant> Comparison::decompose(
820
    bool split_constant) const
821
{
822
304712
  Kind rel = getNode().getKind();
823
304712
  if (rel == Kind::NOT)
824
  {
825
141749
    switch (getNode()[0].getKind())
826
    {
827
      case kind::LEQ: rel = Kind::GT; break;
828
      case kind::LT: rel = Kind::GEQ; break;
829
47904
      case kind::EQUAL: rel = Kind::DISTINCT; break;
830
      case kind::DISTINCT: rel = Kind::EQUAL; break;
831
93845
      case kind::GEQ: rel = Kind::LT; break;
832
      case kind::GT: rel = Kind::LEQ; break;
833
      default:
834
        Assert(false) << "Unsupported relation: " << getNode()[0].getKind();
835
    }
836
  }
837
838
609424
  Polynomial poly = getLeft() - getRight();
839
840
304712
  if (!split_constant)
841
  {
842
    return std::tuple<Polynomial, Kind, Constant>{
843
        poly, rel, Constant::mkZero()};
844
  }
845
846
609424
  Constant right = Constant::mkZero();
847
304712
  if (poly.containsConstant())
848
  {
849
123777
    right = -poly.getHead().getConstant();
850
123777
    poly = poly + Polynomial::mkPolynomial(right);
851
  }
852
853
609424
  Constant lcoeff = poly.getHead().getConstant();
854
304712
  if (!lcoeff.isOne())
855
  {
856
91032
    Constant invlcoeff = lcoeff.inverse();
857
45516
    if (lcoeff.isNegative())
858
    {
859
40662
      switch (rel)
860
      {
861
        case kind::LEQ: rel = Kind::GEQ; break;
862
22493
        case kind::LT: rel = Kind::GT; break;
863
247
        case kind::EQUAL: break;
864
131
        case kind::DISTINCT: break;
865
17791
        case kind::GEQ: rel = Kind::LEQ; break;
866
        case kind::GT: rel = Kind::LT; break;
867
        default: Assert(false) << "Unsupported relation: " << rel;
868
      }
869
    }
870
45516
    poly = poly * invlcoeff;
871
45516
    right = right * invlcoeff;
872
  }
873
874
304712
  return std::tuple<Polynomial, Kind, Constant>{poly, rel, right};
875
}
876
877
2261917
Comparison Comparison::parseNormalForm(TNode n) {
878
2261917
  Debug("polynomial") << "Comparison::parseNormalForm(" << n << ")";
879
2261917
  Comparison result(n);
880
2261917
  Assert(result.isNormalForm());
881
2261917
  return result;
882
}
883
884
703082
Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r) {
885
703082
  Assert(isRelationOperator(k));
886
703082
  switch(k) {
887
703082
  case kind::GEQ:
888
  case kind::GT:
889
1406164
    return NodeManager::currentNM()->mkNode(k, l.getNode(), r.getNode());
890
  default: Unhandled() << k;
891
  }
892
}
893
894
1301920
Node Comparison::toNode(Kind k, const Polynomial& l, const Polynomial& r) {
895
1301920
  Assert(isRelationOperator(k));
896
1301920
  switch(k) {
897
1301920
  case kind::GEQ:
898
  case kind::EQUAL:
899
  case kind::GT:
900
1301920
    return NodeManager::currentNM()->mkNode(k, l.getNode(), r.getNode());
901
  case kind::LEQ:
902
    return toNode(kind::GEQ, r, l).notNode();
903
  case kind::LT:
904
    return toNode(kind::GT, r, l).notNode();
905
  case kind::DISTINCT:
906
    return toNode(kind::EQUAL, r, l).notNode();
907
  default:
908
    Unreachable();
909
  }
910
}
911
912
8907430
bool Comparison::rightIsConstant() const {
913
8907430
  if(getNode().getKind() == kind::NOT){
914
1389296
    return getNode()[0][1].getKind() == kind::CONST_RATIONAL;
915
  }else{
916
7518134
    return getNode()[1].getKind() == kind::CONST_RATIONAL;
917
  }
918
}
919
920
size_t Comparison::getComplexity() const{
921
  switch(comparisonKind()){
922
  case kind::CONST_BOOLEAN: return 1;
923
  case kind::LT:
924
  case kind::LEQ:
925
  case kind::DISTINCT:
926
  case kind::EQUAL:
927
  case kind::GT:
928
  case kind::GEQ:
929
    return getLeft().getComplexity() +  getRight().getComplexity();
930
  default: Unhandled() << comparisonKind(); return -1;
931
  }
932
}
933
934
17548387
Polynomial Comparison::getLeft() const {
935
35096774
  TNode left;
936
17548387
  Kind k = comparisonKind();
937
17548387
  switch(k){
938
3603211
  case kind::LT:
939
  case kind::LEQ:
940
  case kind::DISTINCT:
941
3603211
    left = getNode()[0][0];
942
3603211
    break;
943
13945176
  case kind::EQUAL:
944
  case kind::GT:
945
  case kind::GEQ:
946
13945176
    left = getNode()[0];
947
13945176
    break;
948
  default: Unhandled() << k;
949
  }
950
35096774
  return Polynomial::parsePolynomial(left);
951
}
952
953
11760539
Polynomial Comparison::getRight() const {
954
23521078
  TNode right;
955
11760539
  Kind k = comparisonKind();
956
11760539
  switch(k){
957
2071101
  case kind::LT:
958
  case kind::LEQ:
959
  case kind::DISTINCT:
960
2071101
    right = getNode()[0][1];
961
2071101
    break;
962
9689438
  case kind::EQUAL:
963
  case kind::GT:
964
  case kind::GEQ:
965
9689438
    right = getNode()[1];
966
9689438
    break;
967
  default: Unhandled() << k;
968
  }
969
23521078
  return Polynomial::parsePolynomial(right);
970
}
971
972
// Polynomial Comparison::getLeft() const {
973
//   Node n = getNode();
974
//   Node left = (n.getKind() == kind::NOT ? n[0]: n)[0];
975
//   return Polynomial::parsePolynomial(left);
976
// }
977
978
// Polynomial Comparison::getRight() const {
979
//   Node n = getNode();
980
//   Node right = (n.getKind() == kind::NOT ? n[0]: n)[1];
981
//   return Polynomial::parsePolynomial(right);
982
// }
983
984
11024882
bool Comparison::isNormalForm() const {
985
22049764
  Node n = getNode();
986
11024882
  Kind cmpKind = comparisonKind(n);
987
11024882
  Debug("nf::tmp") << "isNormalForm " << n << " " << cmpKind << endl;
988
11024882
  switch(cmpKind){
989
339545
  case kind::CONST_BOOLEAN:
990
339545
    return true;
991
  case kind::GT:
992
    return isNormalGT();
993
3759067
  case kind::GEQ:
994
3759067
    return isNormalGEQ();
995
4684298
  case kind::EQUAL:
996
4684298
    return isNormalEquality();
997
1389296
  case kind::LT:
998
1389296
    return isNormalLT();
999
  case kind::LEQ:
1000
    return isNormalLEQ();
1001
852676
  case kind::DISTINCT:
1002
852676
    return isNormalDistinct();
1003
  default:
1004
    return false;
1005
  }
1006
}
1007
1008
/** This must be (> qpolynomial constant) */
1009
bool Comparison::isNormalGT() const {
1010
  Node n = getNode();
1011
  Assert(n.getKind() == kind::GT);
1012
  if(!rightIsConstant()){
1013
    return false;
1014
  }else{
1015
    Polynomial left = getLeft();
1016
    if(left.containsConstant()){
1017
      return false;
1018
    }else if(!left.leadingCoefficientIsAbsOne()){
1019
      return false;
1020
    }else{
1021
      return !left.isIntegral();
1022
    }
1023
  }
1024
}
1025
1026
/** This must be (not (> qpolynomial constant)) */
1027
bool Comparison::isNormalLEQ() const {
1028
  Node n = getNode();
1029
  Debug("nf::tmp") << "isNormalLEQ " << n << endl;
1030
  Assert(n.getKind() == kind::NOT);
1031
  Assert(n[0].getKind() == kind::GT);
1032
  if(!rightIsConstant()){
1033
    return false;
1034
  }else{
1035
    Polynomial left = getLeft();
1036
    if(left.containsConstant()){
1037
      return false;
1038
    }else if(!left.leadingCoefficientIsAbsOne()){
1039
      return false;
1040
    }else{
1041
      return !left.isIntegral();
1042
    }
1043
  }
1044
}
1045
1046
1047
/** This must be (>= qpolynomial constant) or  (>= zpolynomial constant) */
1048
3759067
bool Comparison::isNormalGEQ() const {
1049
7518134
  Node n = getNode();
1050
3759067
  Assert(n.getKind() == kind::GEQ);
1051
1052
3759067
  Debug("nf::tmp") << "isNormalGEQ " << n << " " << rightIsConstant() << endl;
1053
1054
3759067
  if(!rightIsConstant()){
1055
    return false;
1056
  }else{
1057
7518134
    Polynomial left = getLeft();
1058
3759067
    if(left.containsConstant()){
1059
      return false;
1060
    }else{
1061
3759067
      if(left.isIntegral()){
1062
2297448
        return left.signNormalizedReducedSum();
1063
      }else{
1064
1461619
        return left.leadingCoefficientIsAbsOne();
1065
      }
1066
    }
1067
  }
1068
}
1069
1070
/** This must be (not (>= qpolynomial constant)) or (not (>= zpolynomial constant)) */
1071
1389296
bool Comparison::isNormalLT() const {
1072
2778592
  Node n = getNode();
1073
1389296
  Assert(n.getKind() == kind::NOT);
1074
1389296
  Assert(n[0].getKind() == kind::GEQ);
1075
1076
1389296
  if(!rightIsConstant()){
1077
    return false;
1078
  }else{
1079
2778592
    Polynomial left = getLeft();
1080
1389296
    if(left.containsConstant()){
1081
      return false;
1082
    }else{
1083
1389296
      if(left.isIntegral()){
1084
961332
        return left.signNormalizedReducedSum();
1085
      }else{
1086
427964
        return left.leadingCoefficientIsAbsOne();
1087
      }
1088
    }
1089
  }
1090
}
1091
1092
1093
5536974
bool Comparison::isNormalEqualityOrDisequality() const {
1094
11073948
  Polynomial pleft = getLeft();
1095
1096
5536974
  if(pleft.numMonomials() == 1){
1097
11073948
    Monomial mleft = pleft.getHead();
1098
5536974
    if(mleft.isConstant()){
1099
      return false;
1100
    }else{
1101
11073948
      Polynomial pright = getRight();
1102
5536974
      if(allIntegralVariables()){
1103
4984175
        const Rational& lcoeff = mleft.getConstant().getValue();
1104
4984175
        if(pright.isConstant()){
1105
2015720
          return pright.isIntegral() && lcoeff.isOne();
1106
        }
1107
5936910
        Polynomial varRight = pright.containsConstant() ? pright.getTail() : pright;
1108
2968455
        if(lcoeff.sgn() <= 0){
1109
          return false;
1110
        }else{
1111
5936910
          Integer lcm = lcoeff.getDenominator().lcm(varRight.denominatorLCM());
1112
5936910
          Integer g = lcoeff.getNumerator().gcd(varRight.numeratorGCD());
1113
2968455
          Debug("nf::tmp") << lcm << " " << g << endl;
1114
2968455
          if(!lcm.isOne()){
1115
            return false;
1116
2968455
          }else if(!g.isOne()){
1117
            return false;
1118
          }else{
1119
5936910
            Monomial absMinRight = varRight.selectAbsMinimum();
1120
2968455
            Debug("nf::tmp") << mleft.getNode() << " " << absMinRight.getNode() << endl;
1121
2968455
            if( mleft.absCmp(absMinRight) < 0){
1122
71441
              return true;
1123
            }else{
1124
2897014
              return (!(absMinRight.absCmp(mleft)< 0)) && mleft < absMinRight;
1125
            }
1126
          }
1127
        }
1128
      }else{
1129
552799
        if(mleft.coefficientIsOne()){
1130
1105598
          Debug("nf::tmp")
1131
552799
            << "dfklj " << mleft.getNode() << endl
1132
552799
            << pright.getNode() << endl
1133
1105598
            << pright.variableMonomialAreStrictlyGreater(mleft)
1134
552799
            << endl;
1135
552799
          return pright.variableMonomialAreStrictlyGreater(mleft);
1136
        }else{
1137
          return false;
1138
        }
1139
      }
1140
    }
1141
  }else{
1142
    return false;
1143
  }
1144
}
1145
1146
/** This must be (= qvarlist qpolynomial) or (= zmonomial zpolynomial)*/
1147
4684298
bool Comparison::isNormalEquality() const {
1148
4684298
  Assert(getNode().getKind() == kind::EQUAL);
1149
14052894
  return Theory::theoryOf(getNode()[0].getType()) == THEORY_ARITH &&
1150
14052894
         isNormalEqualityOrDisequality();
1151
}
1152
1153
/**
1154
 * This must be (not (= qvarlist qpolynomial)) or
1155
 * (not (= zmonomial zpolynomial)).
1156
 */
1157
852676
bool Comparison::isNormalDistinct() const {
1158
852676
  Assert(getNode().getKind() == kind::NOT);
1159
852676
  Assert(getNode()[0].getKind() == kind::EQUAL);
1160
1161
2558028
  return Theory::theoryOf(getNode()[0][0].getType()) == THEORY_ARITH &&
1162
2558028
         isNormalEqualityOrDisequality();
1163
}
1164
1165
69004
Node Comparison::mkRatEquality(const Polynomial& p){
1166
69004
  Assert(!p.isConstant());
1167
69004
  Assert(!p.allIntegralVariables());
1168
1169
138008
  Monomial minimalVList = p.minimumVariableMonomial();
1170
138008
  Constant coeffInv = -(minimalVList.getConstant().inverse());
1171
1172
138008
  Polynomial newRight = (p - minimalVList) * coeffInv;
1173
138008
  Polynomial newLeft(Monomial::mkMonomial(minimalVList.getVarList()));
1174
1175
138008
  return toNode(kind::EQUAL, newLeft, newRight);
1176
}
1177
1178
254566
Node Comparison::mkRatInequality(Kind k, const Polynomial& p){
1179
254566
  Assert(k == kind::GEQ || k == kind::GT);
1180
254566
  Assert(!p.isConstant());
1181
254566
  Assert(!p.allIntegralVariables());
1182
1183
509132
  SumPair sp = SumPair::mkSumPair(p);
1184
509132
  Polynomial left = sp.getPolynomial();
1185
509132
  Constant right = - sp.getConstant();
1186
1187
509132
  Monomial minimalVList = left.getHead();
1188
254566
  Assert(!minimalVList.isConstant());
1189
1190
509132
  Constant coeffInv = minimalVList.getConstant().inverse().abs();
1191
509132
  Polynomial newLeft = left * coeffInv;
1192
509132
  Constant newRight = right * (coeffInv);
1193
1194
509132
  return toNode(k, newLeft, newRight);
1195
}
1196
1197
448516
Node Comparison::mkIntInequality(Kind k, const Polynomial& p){
1198
448516
  Assert(kind::GT == k || kind::GEQ == k);
1199
448516
  Assert(!p.isConstant());
1200
448516
  Assert(p.allIntegralVariables());
1201
1202
897032
  SumPair sp = SumPair::mkSumPair(p);
1203
897032
  Polynomial left = sp.getPolynomial();
1204
897032
  Rational right = - (sp.getConstant().getValue());
1205
1206
1207
897032
  Monomial m = left.getHead();
1208
448516
  Assert(!m.isConstant());
1209
1210
897032
  Integer lcm = left.denominatorLCM();
1211
897032
  Integer g = left.numeratorGCD();
1212
897032
  Rational mult(lcm,g);
1213
1214
897032
  Polynomial newLeft = left * mult;
1215
897032
  Rational rightMult = right * mult;
1216
1217
448516
  bool negateResult = false;
1218
448516
  if(!newLeft.leadingCoefficientIsPositive()){
1219
    // multiply by -1
1220
    // a: left >= right or b: left > right
1221
    // becomes
1222
    // a: -left <= -right or b: -left < -right
1223
    // a: not (-left > -right) or b: (not -left >= -right)
1224
83723
    newLeft = -newLeft;
1225
83723
    rightMult = -rightMult;
1226
83723
    k = (kind::GT == k) ? kind::GEQ : kind::GT;
1227
83723
    negateResult = true;
1228
    // the later stages handle:
1229
    // a: not (-left >= -right + 1) or b: (not -left >= -right)
1230
  }
1231
1232
897032
  Node result = Node::null();
1233
448516
  if(rightMult.isIntegral()){
1234
444620
    if(k == kind::GT){
1235
      // (> p z)
1236
      // (>= p (+ z 1))
1237
163538
      Constant rightMultPlusOne = Constant::mkConstant(rightMult + 1);
1238
81769
      result = toNode(kind::GEQ, newLeft, rightMultPlusOne);
1239
    }else{
1240
725702
      Constant newRight = Constant::mkConstant(rightMult);
1241
362851
      result = toNode(kind::GEQ, newLeft, newRight);
1242
    }
1243
  }else{
1244
    //(>= l (/ n d))
1245
    //(>= l (ceil (/ n d)))
1246
    //This also hold for GT as (ceil (/ n d)) > (/ n d)
1247
7792
    Integer ceilr = rightMult.ceiling();
1248
7792
    Constant ceilRight = Constant::mkConstant(ceilr);
1249
3896
    result = toNode(kind::GEQ, newLeft, ceilRight);
1250
  }
1251
448516
  Assert(!result.isNull());
1252
448516
  if(negateResult){
1253
83723
    return result.notNode();
1254
  }else{
1255
364793
    return result;
1256
  }
1257
}
1258
1259
682662
Node Comparison::mkIntEquality(const Polynomial& p){
1260
682662
  Assert(!p.isConstant());
1261
682662
  Assert(p.allIntegralVariables());
1262
1263
1365324
  SumPair sp = SumPair::mkSumPair(p);
1264
1365324
  Polynomial varPart = sp.getPolynomial();
1265
1365324
  Constant constPart = sp.getConstant();
1266
1267
1365324
  Integer lcm = varPart.denominatorLCM();
1268
1365324
  Integer g = varPart.numeratorGCD();
1269
1365324
  Constant mult = Constant::mkConstant(Rational(lcm,g));
1270
1271
1365324
  Constant constMult = constPart * mult;
1272
1273
682662
  if(constMult.isIntegral()){
1274
1364172
    Polynomial varPartMult = varPart * mult;
1275
1276
1364172
    Monomial m = varPartMult.selectAbsMinimum();
1277
682086
    bool mIsPositive =  m.getConstant().isPositive();
1278
1279
1364172
    Polynomial noM = (varPartMult + (- m)) + Polynomial::mkPolynomial(constMult);
1280
1281
    // m + noM = 0
1282
1364172
    Polynomial newRight = mIsPositive ? -noM : noM;
1283
1364172
    Polynomial newLeft  = mIsPositive ? m  : -m;
1284
1285
682086
    Assert(newRight.isIntegral());
1286
682086
    return toNode(kind::EQUAL, newLeft, newRight);
1287
  }else{
1288
576
    return mkBoolNode(false);
1289
  }
1290
}
1291
1292
2343395
Comparison Comparison::mkComparison(Kind k, const Polynomial& l, const Polynomial& r){
1293
1294
  //Make this special case fast for sharing!
1295
2343395
  if((k == kind::EQUAL || k == kind::DISTINCT) && l.isVarList() && r.isVarList()){
1296
1103024
    VarList vLeft = l.asVarList();
1297
1103024
    VarList vRight = r.asVarList();
1298
1299
551512
    if(vLeft == vRight){
1300
      // return true for equalities and false for disequalities
1301
682
      return Comparison(k == kind::EQUAL);
1302
    }else{
1303
1101660
      Node eqNode = vLeft < vRight ? toNode( kind::EQUAL, l, r) : toNode( kind::EQUAL, r, l);
1304
1101660
      Node forK = (k == kind::DISTINCT) ? eqNode.notNode() : eqNode;
1305
550830
      return Comparison(forK);
1306
    }
1307
  }
1308
1309
  //General case
1310
3583766
  Polynomial diff = l - r;
1311
1791883
  if(diff.isConstant()){
1312
337135
    bool res = evaluateConstantPredicate(k, diff.asConstant(), Rational(0));
1313
337135
    return Comparison(res);
1314
  }else{
1315
2909496
    Node result = Node::null();
1316
1454748
    bool isInteger = diff.allIntegralVariables();
1317
1454748
    switch(k){
1318
751666
    case kind::EQUAL:
1319
751666
      result = isInteger ? mkIntEquality(diff) : mkRatEquality(diff);
1320
751666
      break;
1321
    case kind::DISTINCT:
1322
      {
1323
        Node eq = isInteger ? mkIntEquality(diff) : mkRatEquality(diff);
1324
        result = eq.notNode();
1325
      }
1326
      break;
1327
108914
    case kind::LEQ:
1328
    case kind::LT:
1329
      {
1330
217828
        Polynomial neg = - diff;
1331
108914
        Kind negKind = (k == kind::LEQ ? kind::GEQ : kind::GT);
1332
108914
        result = isInteger ?
1333
108914
          mkIntInequality(negKind, neg) : mkRatInequality(negKind, neg);
1334
      }
1335
108914
      break;
1336
594168
    case kind::GEQ:
1337
    case kind::GT:
1338
594168
      result = isInteger ?
1339
        mkIntInequality(k, diff) : mkRatInequality(k, diff);
1340
594168
      break;
1341
    default: Unhandled() << k;
1342
    }
1343
1454748
    Assert(!result.isNull());
1344
1454748
    if(result.getKind() == kind::NOT && result[0].getKind() == kind::CONST_BOOLEAN){
1345
      return Comparison(!(result[0].getConst<bool>()));
1346
    }else{
1347
2909496
      Comparison cmp(result);
1348
1454748
      Assert(cmp.isNormalForm());
1349
1454748
      return cmp;
1350
    }
1351
  }
1352
}
1353
1354
33674
bool Comparison::isBoolean() const {
1355
33674
  return getNode().getKind() == kind::CONST_BOOLEAN;
1356
}
1357
1358
1359
33674
bool Comparison::debugIsIntegral() const{
1360
33674
  return getLeft().isIntegral() && getRight().isIntegral();
1361
}
1362
1363
49273653
Kind Comparison::comparisonKind(TNode literal){
1364
49273653
  switch(literal.getKind()){
1365
37447702
  case kind::CONST_BOOLEAN:
1366
  case kind::GT:
1367
  case kind::GEQ:
1368
  case kind::EQUAL:
1369
37447702
    return literal.getKind();
1370
11825951
  case  kind::NOT:
1371
    {
1372
23651902
      TNode negatedAtom = literal[0];
1373
11825951
      switch(negatedAtom.getKind()){
1374
      case kind::GT: //(not (GT x c)) <=> (LEQ x c)
1375
        return kind::LEQ;
1376
5612553
      case kind::GEQ: //(not (GEQ x c)) <=> (LT x c)
1377
5612553
        return kind::LT;
1378
6213398
      case kind::EQUAL:
1379
6213398
        return kind::DISTINCT;
1380
      default:
1381
        return  kind::UNDEFINED_KIND;
1382
      }
1383
    }
1384
  default:
1385
    return kind::UNDEFINED_KIND;
1386
  }
1387
}
1388
1389
1390
Node Polynomial::makeAbsCondition(Variable v, Polynomial p){
1391
  Polynomial zerop = Polynomial::mkZero();
1392
1393
  Polynomial varp = Polynomial::mkPolynomial(v);
1394
  Comparison pLeq0 = Comparison::mkComparison(kind::LEQ, p, zerop);
1395
  Comparison negP = Comparison::mkComparison(kind::EQUAL, varp, -p);
1396
  Comparison posP = Comparison::mkComparison(kind::EQUAL, varp, p);
1397
1398
  Node absCnd = (pLeq0.getNode()).iteNode(negP.getNode(), posP.getNode());
1399
  return absCnd;
1400
}
1401
1402
33674
bool Polynomial::isNonlinear() const {
1403
1404
98874
  for(iterator i=begin(), iend =end(); i != iend; ++i){
1405
131900
    Monomial m = *i;
1406
66700
    if(m.isNonlinear()){
1407
1500
      return true;
1408
    }
1409
  }
1410
32174
  return false;
1411
}
1412
1413
} //namespace arith
1414
} //namespace theory
1415
26685
} //namespace CVC4