GCC Code Coverage Report
Directory: . Exec Total Coverage
File: src/theory/arith/normal_form.h Lines: 371 383 96.9 %
Date: 2021-03-23 Branches: 406 1108 36.6 %

Line Exec Source
1
/*********************                                                        */
2
/*! \file normal_form.h
3
 ** \verbatim
4
 ** Top contributors (to current version):
5
 **   Tim King, Morgan Deters, Gereon Kremer
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
18
#include "cvc4_private.h"
19
20
#ifndef CVC4__THEORY__ARITH__NORMAL_FORM_H
21
#define CVC4__THEORY__ARITH__NORMAL_FORM_H
22
23
#include <algorithm>
24
25
#include "base/output.h"
26
#include "expr/node.h"
27
#include "expr/node_self_iterator.h"
28
#include "theory/arith/delta_rational.h"
29
#include "util/rational.h"
30
31
32
namespace CVC4 {
33
namespace theory {
34
namespace arith {
35
36
/***********************************************/
37
/***************** Normal Form *****************/
38
/***********************************************/
39
/***********************************************/
40
41
/**
42
 * Section 1: Languages
43
 * The normal form for arithmetic nodes is defined by the language
44
 * accepted by the following BNFs with some guard conditions.
45
 * (The guard conditions are in Section 3 for completeness.)
46
 *
47
 * variable := n
48
 *   where
49
 *     n.isVar() or is foreign
50
 *     n.getType() \in {Integer, Real}
51
 *
52
 * constant := n
53
 *   where
54
 *     n.getKind() == kind::CONST_RATIONAL
55
 *
56
 * var_list := variable | (* [variable])
57
 *   where
58
 *     len [variable] >= 2
59
 *     isSorted varOrder [variable]
60
 *
61
 * monomial := constant | var_list | (* constant' var_list')
62
 *   where
63
 *     \f$ constant' \not\in {0,1} \f$
64
 *
65
 * polynomial := monomial' | (+ [monomial])
66
 *   where
67
 *     len [monomial] >= 2
68
 *     isStrictlySorted monoOrder [monomial]
69
 *     forall (\x -> x != 0) [monomial]
70
 *
71
 * rational_cmp := (|><| qpolynomial constant)
72
 *   where
73
 *     |><| is GEQ, or GT
74
 *     not (exists constantMonomial (monomialList qpolynomial))
75
 *     (exists realMonomial (monomialList qpolynomial))
76
 *     abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
77
 *
78
 * integer_cmp := (>= zpolynomial constant)
79
 *   where
80
 *     not (exists constantMonomial (monomialList zpolynomial))
81
 *     (forall integerMonomial (monomialList zpolynomial))
82
 *     the gcd of all numerators of coefficients is 1
83
 *     the denominator of all coefficients and the constant is 1
84
 *     the leading coefficient is positive
85
 *
86
 * rational_eq := (= qvarlist qpolynomial)
87
 *   where
88
 *     let allMonomials = (cons qvarlist (monomialList zpolynomial))
89
 *     let variableMonomials = (drop constantMonomial allMonomials)
90
 *     isStrictlySorted variableMonomials
91
 *     exists realMonomial variableMonomials
92
 *     is not empty qvarlist
93
 *
94
 * integer_eq := (= zmonomial zpolynomial)
95
 *   where
96
 *     let allMonomials = (cons zmonomial (monomialList zpolynomial))
97
 *     let variableMonomials = (drop constantMonomial allMonomials)
98
 *     not (constantMonomial zmonomial)
99
 *     (forall integerMonomial allMonomials)
100
 *     isStrictlySorted variableMonomials
101
 *     the gcd of all numerators of coefficients is 1
102
 *     the denominator of all coefficients and the constant is 1
103
 *     the coefficient of monomial is positive
104
 *     the value of the coefficient of monomial is minimal in variableMonomials
105
 *
106
 * comparison := TRUE | FALSE
107
 *   | rational_cmp | (not rational_cmp)
108
 *   | rational_eq | (not rational_eq)
109
 *   | integer_cmp | (not integer_cmp)
110
 *   | integer_eq | (not integer_eq)
111
 *
112
 * Normal Form for terms := polynomial
113
 * Normal Form for atoms := comparison
114
 */
115
116
/**
117
 * Section 2: Helper Classes
118
 * The langauges accepted by each of these defintions
119
 * roughly corresponds to one of the following helper classes:
120
 *  Variable
121
 *  Constant
122
 *  VarList
123
 *  Monomial
124
 *  Polynomial
125
 *  Comparison
126
 *
127
 * Each of the classes obeys the following contracts/design decisions:
128
 * -Calling isMember(Node node) on a node returns true iff that node is a
129
 *  a member of the language. Note: isMember is O(n).
130
 * -Calling isNormalForm() on a helper class object returns true iff that
131
 *  helper class currently represents a normal form object.
132
 * -If isNormalForm() is false, then this object must have been made
133
 *  using a mk*() factory function.
134
 * -If isNormalForm() is true, calling getNode() on all of these classes
135
 *  returns a node that would be accepted by the corresponding language.
136
 *  And if isNormalForm() is false, returns Node::null().
137
 * -Each of the classes is immutable.
138
 * -Public facing constuctors have a 1-to-1 correspondence with one of
139
 *  production rules in the above grammar.
140
 * -Public facing constuctors are required to fail in debug mode when the
141
 *  guards of the production rule are not strictly met.
142
 *  For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
143
 * -When a class has a Class parseClass(Node node) function,
144
 *  if isMember(node) is true, the function is required to return an instance
145
 *  of the helper class, instance, s.t. instance.getNode() == node.
146
 *  And if isMember(node) is false, this throws an assertion failure in debug
147
 *  mode and has undefined behaviour if not in debug mode.
148
 * -Only public facing constructors, parseClass(node), and mk*() functions are
149
 *  considered privileged functions for the helper class.
150
 * -Only privileged functions may use private constructors, and access
151
 *  private data members.
152
 * -All non-privileged functions are considered utility functions and
153
 *  must use a privileged function in order to create an instance of the class.
154
 */
155
156
/**
157
 * Section 3: Guard Conditions Misc.
158
 *
159
 *
160
 *  variable_order x y =
161
 *    if (meta_kind_variable x) and (meta_kind_variable y)
162
 *    then node_order x y
163
 *    else if (meta_kind_variable x)
164
 *    then false
165
 *    else if (meta_kind_variable y)
166
 *    then true
167
 *    else node_order x y
168
 *
169
 *  var_list_len vl =
170
 *    match vl with
171
 *       variable -> 1
172
 *     | (* [variable]) -> len [variable]
173
 *
174
 *  order res =
175
 *    match res with
176
 *       Empty -> (0,Node::null())
177
 *     | NonEmpty(vl) -> (var_list_len vl, vl)
178
 *
179
 *  var_listOrder a b = tuple_cmp (order a) (order b)
180
 *
181
 *  monomialVarList monomial =
182
 *    match monomial with
183
 *        constant -> Empty
184
 *      | var_list -> NonEmpty(var_list)
185
 *      | (* constant' var_list') -> NonEmpty(var_list')
186
 *
187
 *  monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
188
 *
189
 *  integerMonomial mono =
190
 *    forall varHasTypeInteger (monomialVarList mono)
191
 *
192
 *  realMonomial mono = not (integerMonomial mono)
193
 *
194
 *  constantMonomial monomial =
195
 *    match monomial with
196
 *        constant -> true
197
 *      | var_list -> false
198
 *      | (* constant' var_list') -> false
199
 *
200
 *  monomialCoefficient monomial =
201
 *    match monomial with
202
 *        constant -> constant
203
 *      | var_list -> Constant(1)
204
 *      | (* constant' var_list') -> constant'
205
 *
206
 *  monomialList polynomial =
207
 *    match polynomial with
208
 *        monomial -> monomial::[]
209
 *      | (+ [monomial]) -> [monomial]
210
 */
211
212
/**
213
 * A NodeWrapper is a class that is a thinly veiled container of a Node object.
214
 */
215
1844725015
class NodeWrapper {
216
private:
217
  Node node;
218
public:
219
753209898
  NodeWrapper(Node n) : node(n) {}
220
3966017443
  const Node& getNode() const { return node; }
221
};/* class NodeWrapper */
222
223
224
70904084
class Variable : public NodeWrapper {
225
public:
226
54404420
 Variable(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); }
227
228
 // TODO: check if it's a theory leaf also
229
182769211
 static bool isMember(Node n)
230
 {
231
182769211
   Kind k = n.getKind();
232
182769211
   switch (k)
233
   {
234
628258
     case kind::CONST_RATIONAL: return false;
235
112595
     case kind::INTS_DIVISION:
236
     case kind::INTS_MODULUS:
237
     case kind::DIVISION:
238
     case kind::INTS_DIVISION_TOTAL:
239
     case kind::INTS_MODULUS_TOTAL:
240
112595
     case kind::DIVISION_TOTAL: return isDivMember(n);
241
325184
     case kind::IAND: return isIAndMember(n);
242
2141558
     case kind::EXPONENTIAL:
243
     case kind::SINE:
244
     case kind::COSINE:
245
     case kind::TANGENT:
246
     case kind::COSECANT:
247
     case kind::SECANT:
248
     case kind::COTANGENT:
249
     case kind::ARCSINE:
250
     case kind::ARCCOSINE:
251
     case kind::ARCTANGENT:
252
     case kind::ARCCOSECANT:
253
     case kind::ARCSECANT:
254
     case kind::ARCCOTANGENT:
255
     case kind::SQRT:
256
2141558
     case kind::PI: return isTranscendentalMember(n);
257
24463
     case kind::ABS:
258
     case kind::TO_INTEGER:
259
       // Treat to_int as a variable; it is replaced in early preprocessing
260
       // by a variable.
261
24463
       return true;
262
179537153
     default: return isLeafMember(n);
263
   }
264
 }
265
266
  static bool isLeafMember(Node n);
267
  static bool isIAndMember(Node n);
268
  static bool isDivMember(Node n);
269
  bool isDivLike() const{
270
    return isDivMember(getNode());
271
  }
272
  static bool isTranscendentalMember(Node n);
273
274
  bool isNormalForm() { return isMember(getNode()); }
275
276
29766658
  bool isIntegral() const {
277
29766658
    return getNode().getType().isInteger();
278
  }
279
280
  bool isMetaKindVariable() const {
281
    return getNode().isVar();
282
  }
283
284
12271148
  bool operator<(const Variable& v) const {
285
    VariableNodeCmp cmp;
286
12271148
    return cmp(this->getNode(), v.getNode());
287
  }
288
289
  struct VariableNodeCmp {
290
82945564
    static inline int cmp(const Node& n, const Node& m) {
291
82945564
      if ( n == m ) { return 0; }
292
293
      // this is now slightly off of the old variable order.
294
295
73846685
      bool nIsInteger = n.getType().isInteger();
296
73846685
      bool mIsInteger = m.getType().isInteger();
297
298
73846685
      if(nIsInteger == mIsInteger){
299
72984835
        bool nIsVariable = n.isVar();
300
72984835
        bool mIsVariable = m.isVar();
301
302
72984835
        if(nIsVariable == mIsVariable){
303
64603977
          if(n < m){
304
35704128
            return -1;
305
          }else{
306
28899849
            Assert(n != m);
307
28899849
            return 1;
308
          }
309
        }else{
310
8380858
          if(nIsVariable){
311
4308356
            return -1; // nIsVariable => !mIsVariable
312
          }else{
313
4072502
            return 1; // !nIsVariable => mIsVariable
314
          }
315
        }
316
      }else{
317
861850
        Assert(nIsInteger != mIsInteger);
318
861850
        if(nIsInteger){
319
729177
          return 1; // nIsInteger => !mIsInteger
320
        }else{
321
132673
          return -1; // !nIsInteger => mIsInteger
322
        }
323
      }
324
    }
325
326
17411322
    bool operator()(const Node& n, const Node& m) const {
327
17411322
      return VariableNodeCmp::cmp(n,m) < 0;
328
    }
329
  };
330
331
  bool operator==(const Variable& v) const { return getNode() == v.getNode();}
332
333
  size_t getComplexity() const;
334
};/* class Variable */
335
336
337
585575259
class Constant : public NodeWrapper {
338
public:
339
218225478
 Constant(Node n) : NodeWrapper(n) { Assert(isMember(getNode())); }
340
341
220095962
 static bool isMember(Node n) { return n.getKind() == kind::CONST_RATIONAL; }
342
343
 bool isNormalForm() { return isMember(getNode()); }
344
345
2091560
 static Constant mkConstant(Node n)
346
 {
347
2091560
   Assert(n.getKind() == kind::CONST_RATIONAL);
348
2091560
   return Constant(n);
349
 }
350
351
  static Constant mkConstant(const Rational& rat);
352
353
852389
  static Constant mkZero() {
354
852389
    return mkConstant(Rational(0));
355
  }
356
357
  static Constant mkOne() {
358
    return mkConstant(Rational(1));
359
  }
360
361
456087362
  const Rational& getValue() const {
362
456087362
    return getNode().getConst<Rational>();
363
  }
364
365
  static int absCmp(const Constant& a, const Constant& b);
366
18730301
  bool isIntegral() const { return getValue().isIntegral(); }
367
368
203751364
  int sgn() const { return getValue().sgn(); }
369
370
196940215
  bool isZero() const { return sgn() == 0; }
371
319256
  bool isNegative() const { return sgn() < 0; }
372
6491893
  bool isPositive() const { return sgn() > 0; }
373
374
169425258
  bool isOne() const { return getValue() == 1; }
375
376
6218725
  Constant operator*(const Rational& other) const {
377
6218725
    return mkConstant(getValue() * other);
378
  }
379
380
2358657
  Constant operator*(const Constant& other) const {
381
2358657
    return mkConstant(getValue() * other.getValue());
382
  }
383
33257
  Constant operator+(const Constant& other) const {
384
33257
    return mkConstant(getValue() + other.getValue());
385
  }
386
603032
  Constant operator-() const {
387
603032
    return mkConstant(-getValue());
388
  }
389
390
369086
  Constant inverse() const{
391
369086
    Assert(!isZero());
392
369086
    return mkConstant(getValue().inverse());
393
  }
394
395
  bool operator<(const Constant& other) const {
396
    return getValue() < other.getValue();
397
  }
398
399
19554
  bool operator==(const Constant& other) const {
400
    //Rely on node uniqueness.
401
19554
    return getNode() == other.getNode();
402
  }
403
404
254566
  Constant abs() const {
405
254566
    if(isNegative()){
406
133360
      return -(*this);
407
    }else{
408
121206
      return (*this);
409
    }
410
  }
411
412
259562
  uint32_t length() const{
413
259562
    Assert(isIntegral());
414
259562
    return getValue().getNumerator().length();
415
  }
416
417
  size_t getComplexity() const;
418
419
};/* class Constant */
420
421
422
template <class GetNodeIterator>
423
5822252
inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
424
11644504
  NodeBuilder<> nb(k);
425
426
36019950
  while(start != end) {
427
15098849
    nb << (*start).getNode();
428
15098849
    ++start;
429
  }
430
431
11644504
  return Node(nb);
432
}/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
433
434
/**
435
 * A VarList is a sorted list of variables representing a product.
436
 * If the VarList is empty, it represents an empty product or 1.
437
 * If the VarList has size 1, it represents a single variable.
438
 *
439
 * A non-sorted VarList can never be successfully made in debug mode.
440
 */
441
714844569
class VarList : public NodeWrapper {
442
private:
443
444
  static Node multList(const std::vector<Variable>& list) {
445
    Assert(list.size() >= 2);
446
447
    return makeNode(kind::NONLINEAR_MULT, list.begin(), list.end());
448
  }
449
450
43121317
  VarList() : NodeWrapper(Node::null()) {}
451
452
  VarList(Node n);
453
454
  typedef expr::NodeSelfIterator internal_iterator;
455
456
202910238
  internal_iterator internalBegin() const {
457
202910238
    if(singleton()){
458
178527391
      return expr::NodeSelfIterator::self(getNode());
459
    }else{
460
24382847
      return getNode().begin();
461
    }
462
  }
463
464
202890419
  internal_iterator internalEnd() const {
465
202890419
    if(singleton()){
466
178507572
      return expr::NodeSelfIterator::selfEnd(getNode());
467
    }else{
468
24382847
      return getNode().end();
469
    }
470
  }
471
472
public:
473
474
3431087843
  class iterator : public std::iterator<std::input_iterator_tag, Variable> {
475
  private:
476
    internal_iterator d_iter;
477
478
  public:
479
393213445
    explicit iterator(internal_iterator i) : d_iter(i) {}
480
481
54396123
    inline Variable operator*() {
482
54396123
      return Variable(*d_iter);
483
    }
484
485
322064284
    bool operator==(const iterator& i) {
486
322064284
      return d_iter == i.d_iter;
487
    }
488
489
235566864
    bool operator!=(const iterator& i) {
490
235566864
      return d_iter != i.d_iter;
491
    }
492
493
200002193
    iterator operator++() {
494
200002193
      ++d_iter;
495
200002193
      return *this;
496
    }
497
498
    iterator operator++(int) {
499
      return iterator(d_iter++);
500
    }
501
  };
502
503
196616632
  iterator begin() const {
504
196616632
    return iterator(internalBegin());
505
  }
506
507
196596813
  iterator end() const {
508
196596813
    return iterator(internalEnd());
509
  }
510
511
19819
  Variable getHead() const {
512
19819
    Assert(!empty());
513
19819
    return *(begin());
514
  }
515
516
4112789
  VarList(Variable v) : NodeWrapper(v.getNode()) {
517
4112789
    Assert(isSorted(begin(), end()));
518
4112789
  }
519
520
  VarList(const std::vector<Variable>& l) : NodeWrapper(multList(l)) {
521
    Assert(l.size() >= 2);
522
    Assert(isSorted(begin(), end()));
523
  }
524
525
  static bool isMember(Node n);
526
527
  bool isNormalForm() const {
528
    return !empty();
529
  }
530
531
43121317
  static VarList mkEmptyVarList() {
532
43121317
    return VarList();
533
  }
534
535
536
  /** There are no restrictions on the size of l */
537
  static VarList mkVarList(const std::vector<Variable>& l) {
538
    if(l.size() == 0) {
539
      return mkEmptyVarList();
540
    } else if(l.size() == 1) {
541
      return VarList((*l.begin()).getNode());
542
    } else {
543
      return VarList(l);
544
    }
545
  }
546
547
1101899924
  bool empty() const { return getNode().isNull(); }
548
671652850
  bool singleton() const {
549
671652850
    return !empty() && getNode().getKind() != kind::NONLINEAR_MULT;
550
  }
551
552
265653226
  int size() const {
553
265653226
    if(singleton())
554
214642393
      return 1;
555
    else
556
51010833
      return getNode().getNumChildren();
557
  }
558
559
  static VarList parseVarList(Node n);
560
561
  VarList operator*(const VarList& vl) const;
562
563
  int cmp(const VarList& vl) const;
564
565
550830
  bool operator<(const VarList& vl) const { return cmp(vl) < 0; }
566
567
19566542
  bool operator==(const VarList& vl) const { return cmp(vl) == 0; }
568
569
35501665
  bool isIntegral() const {
570
62133218
    for(iterator i = begin(), e=end(); i != e; ++i ){
571
56398211
      Variable var = *i;
572
29766658
      if(!var.isIntegral()){
573
3135105
        return false;
574
      }
575
    }
576
32366560
    return true;
577
  }
578
  size_t getComplexity() const;
579
580
private:
581
  bool isSorted(iterator start, iterator end);
582
583
};/* class VarList */
584
585
586
/** Constructors have side conditions. Use the static mkMonomial functions instead. */
587
373765577
class Monomial : public NodeWrapper {
588
private:
589
  Constant constant;
590
  VarList varList;
591
  Monomial(Node n, const Constant& c, const VarList& vl):
592
    NodeWrapper(n), constant(c), varList(vl)
593
  {
594
    Assert(!c.isZero() || vl.empty());
595
    Assert(c.isZero() || !vl.empty());
596
597
    Assert(!c.isOne() || !multStructured(n));
598
  }
599
600
55094198
  static Node makeMultNode(const Constant& c, const VarList& vl) {
601
55094198
    Assert(!c.isZero());
602
55094198
    Assert(!c.isOne());
603
55094198
    Assert(!vl.empty());
604
55094198
    return NodeManager::currentNM()->mkNode(kind::MULT, c.getNode(), vl.getNode());
605
  }
606
607
328069967
  static bool multStructured(Node n) {
608
583555511
    return n.getKind() ==  kind::MULT &&
609
1239695445
      n[0].getKind() == kind::CONST_RATIONAL &&
610
783882706
      n.getNumChildren() == 2;
611
  }
612
613
43121317
  Monomial(const Constant& c):
614
43121317
    NodeWrapper(c.getNode()), constant(c), varList(VarList::mkEmptyVarList())
615
43121317
  { }
616
617
106408114
  Monomial(const VarList& vl):
618
106408114
    NodeWrapper(vl.getNode()), constant(Constant::mkConstant(1)), varList(vl)
619
  {
620
106408114
    Assert(!varList.empty());
621
106408114
  }
622
623
55094198
  Monomial(const Constant& c, const VarList& vl):
624
55094198
    NodeWrapper(makeMultNode(c,vl)), constant(c), varList(vl)
625
  {
626
55094198
    Assert(!c.isZero());
627
55094198
    Assert(!c.isOne());
628
55094198
    Assert(!varList.empty());
629
630
55094198
    Assert(multStructured(getNode()));
631
55094198
  }
632
public:
633
  static bool isMember(TNode n);
634
635
  /** Makes a monomial with no restrictions on c and vl. */
636
  static Monomial mkMonomial(const Constant& c, const VarList& vl);
637
638
  /** If vl is empty, this make one. */
639
  static Monomial mkMonomial(const VarList& vl);
640
641
840736
  static Monomial mkMonomial(const Constant& c){
642
840736
    return Monomial(c);
643
  }
644
645
32364
  static Monomial mkMonomial(const Variable& v){
646
32364
    return Monomial(VarList(v));
647
  }
648
649
  static Monomial parseMonomial(Node n);
650
651
2371939
  static Monomial mkZero() {
652
2371939
    return Monomial(Constant::mkConstant(0));
653
  }
654
536413
  static Monomial mkOne() {
655
536413
    return Monomial(Constant::mkConstant(1));
656
  }
657
93983530
  const Constant& getConstant() const { return constant; }
658
245092515
  const VarList& getVarList() const { return varList; }
659
660
26627761
  bool isConstant() const {
661
26627761
    return varList.empty();
662
  }
663
664
7753209
  bool isZero() const {
665
7753209
    return constant.isZero();
666
  }
667
668
2462336
  bool coefficientIsOne() const {
669
2462336
    return constant.isOne();
670
  }
671
672
1909537
  bool absCoefficientIsOne() const {
673
1909537
    return coefficientIsOne() || constant.getValue() == -1;
674
  }
675
676
  bool constantIsPositive() const {
677
    return getConstant().isPositive();
678
  }
679
680
  Monomial operator*(const Rational& q) const;
681
  Monomial operator*(const Constant& c) const;
682
  Monomial operator*(const Monomial& mono) const;
683
684
793605
  Monomial operator-() const{
685
793605
    return (*this) * Rational(-1);
686
  }
687
688
689
81335799
  int cmp(const Monomial& mono) const {
690
81335799
    return getVarList().cmp(mono.getVarList());
691
  }
692
693
63932921
  bool operator<(const Monomial& vl) const {
694
63932921
    return cmp(vl) < 0;
695
  }
696
697
17402878
  bool operator==(const Monomial& vl) const {
698
17402878
    return cmp(vl) == 0;
699
  }
700
701
27730445
  static bool isSorted(const std::vector<Monomial>& m) {
702
27730445
    return std::is_sorted(m.begin(), m.end());
703
  }
704
705
17370824
  static bool isStrictlySorted(const std::vector<Monomial>& m) {
706
17370824
    return isSorted(m) && std::adjacent_find(m.begin(),m.end()) == m.end();
707
  }
708
709
  static void sort(std::vector<Monomial>& m);
710
  static void combineAdjacentMonomials(std::vector<Monomial>& m);
711
712
  /**
713
   * The variable product
714
   */
715
35500157
  bool integralVariables() const {
716
35500157
    return getVarList().isIntegral();
717
  }
718
719
  /**
720
   * The coefficient of the monomial is integral.
721
   */
722
16788087
  bool integralCoefficient() const {
723
16788087
    return getConstant().isIntegral();
724
  }
725
726
  /**
727
   * A Monomial is an "integral" monomial if the constant is integral.
728
   */
729
16788087
  bool isIntegral() const {
730
16788087
    return integralCoefficient() && integralVariables();
731
  }
732
733
  /** Returns true if the VarList is a product of at least 2 Variables.*/
734
66700
  bool isNonlinear() const {
735
66700
    return getVarList().size() >= 2;
736
  }
737
738
  /**
739
   * Given a sorted list of monomials, this function transforms this
740
   * into a strictly sorted list of monomials that does not contain zero.
741
   */
742
  //static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
743
744
7866777
  int absCmp(const Monomial& other) const{
745
7866777
    return getConstant().getValue().absCmp(other.getConstant().getValue());
746
  }
747
  // bool absLessThan(const Monomial& other) const{
748
  //   return getConstant().abs() < other.getConstant().abs();
749
  // }
750
751
178572
  uint32_t coefficientLength() const{
752
178572
    return getConstant().length();
753
  }
754
755
  void print() const;
756
  static void printList(const std::vector<Monomial>& list);
757
758
  size_t getComplexity() const;
759
};/* class Monomial */
760
761
class SumPair;
762
class Comparison;;
763
764
90235741
class Polynomial : public NodeWrapper {
765
private:
766
  bool d_singleton;
767
768
46759081
  Polynomial(TNode n) : NodeWrapper(n), d_singleton(Monomial::isMember(n)) {
769
46759081
    Assert(isMember(getNode()));
770
46759081
  }
771
772
5822252
  static Node makePlusNode(const std::vector<Monomial>& m) {
773
5822252
    Assert(m.size() >= 2);
774
775
5822252
    return makeNode(kind::PLUS, m.begin(), m.end());
776
  }
777
778
  typedef expr::NodeSelfIterator internal_iterator;
779
780
112135163
  internal_iterator internalBegin() const {
781
112135163
    if(singleton()){
782
76537928
      return expr::NodeSelfIterator::self(getNode());
783
    }else{
784
35597235
      return getNode().begin();
785
    }
786
  }
787
788
74681980
  internal_iterator internalEnd() const {
789
74681980
    if(singleton()){
790
48972323
      return expr::NodeSelfIterator::selfEnd(getNode());
791
    }else{
792
25709657
      return getNode().end();
793
    }
794
  }
795
796
214329969
  bool singleton() const { return d_singleton; }
797
798
public:
799
  static bool isMember(TNode n);
800
801
773617967
  class iterator : public std::iterator<std::input_iterator_tag, Monomial> {
802
  private:
803
    internal_iterator d_iter;
804
805
  public:
806
186817143
    explicit iterator(internal_iterator i) : d_iter(i) {}
807
808
154339334
    inline Monomial operator*() {
809
154339334
      return Monomial::parseMonomial(*d_iter);
810
    }
811
812
163552
    bool operator==(const iterator& i) {
813
163552
      return d_iter == i.d_iter;
814
    }
815
816
170160300
    bool operator!=(const iterator& i) {
817
170160300
      return d_iter != i.d_iter;
818
    }
819
820
86291699
    iterator operator++() {
821
86291699
      ++d_iter;
822
86291699
      return *this;
823
    }
824
825
    iterator operator++(int) {
826
      return iterator(d_iter++);
827
    }
828
  };
829
830
112135163
  iterator begin() const { return iterator(internalBegin()); }
831
74681980
  iterator end() const {  return iterator(internalEnd()); }
832
833
13076052
  Polynomial(const Monomial& m):
834
13076052
    NodeWrapper(m.getNode()), d_singleton(true)
835
13076052
  {}
836
837
5822252
  Polynomial(const std::vector<Monomial>& m):
838
5822252
    NodeWrapper(makePlusNode(m)), d_singleton(false)
839
  {
840
5822252
    Assert(m.size() >= 2);
841
5822252
    Assert(Monomial::isStrictlySorted(m));
842
5822252
  }
843
844
840736
  static Polynomial mkPolynomial(const Constant& c){
845
840736
    return Polynomial(Monomial::mkMonomial(c));
846
  }
847
848
32364
  static Polynomial mkPolynomial(const Variable& v){
849
32364
    return Polynomial(Monomial::mkMonomial(v));
850
  }
851
852
14549780
  static Polynomial mkPolynomial(const std::vector<Monomial>& m) {
853
14549780
    if(m.size() == 0) {
854
935344
      return Polynomial(Monomial::mkZero());
855
13614436
    } else if(m.size() == 1) {
856
7792184
      return Polynomial((*m.begin()));
857
    } else {
858
5822252
      return Polynomial(m);
859
    }
860
  }
861
862
46759081
  static Polynomial parsePolynomial(Node n) {
863
46759081
    return Polynomial(n);
864
  }
865
866
1436595
  static Polynomial mkZero() {
867
1436595
    return Polynomial(Monomial::mkZero());
868
  }
869
536413
  static Polynomial mkOne() {
870
536413
    return Polynomial(Monomial::mkOne());
871
  }
872
7779012
  bool isZero() const {
873
7779012
    return singleton() && (getHead().isZero());
874
  }
875
876
12323213
  bool isConstant() const {
877
12323213
    return singleton() && (getHead().isConstant());
878
  }
879
880
11727343
  bool containsConstant() const {
881
11727343
    return getHead().isConstant();
882
  }
883
884
1609
  uint32_t size() const{
885
1609
    if(singleton()){
886
1277
      return 1;
887
    }else{
888
332
      Assert(getNode().getKind() == kind::PLUS);
889
332
      return getNode().getNumChildren();
890
    }
891
  }
892
893
42534976
  Monomial getHead() const {
894
42534976
    return *(begin());
895
  }
896
897
1844351
  Polynomial getTail() const {
898
1844351
    Assert(!singleton());
899
900
3688702
    iterator tailStart = begin();
901
1844351
    ++tailStart;
902
3688702
    std::vector<Monomial> subrange;
903
1844351
    std::copy(tailStart, end(), std::back_inserter(subrange));
904
3688702
    return mkPolynomial(subrange);
905
  }
906
907
  Monomial minimumVariableMonomial() const;
908
  bool variableMonomialAreStrictlyGreater(const Monomial& m) const;
909
910
  void printList() const {
911
    if(Debug.isOn("normal-form")){
912
      Debug("normal-form") << "start list" << std::endl;
913
      for(iterator i = begin(), oend = end(); i != oend; ++i) {
914
        const Monomial& m =*i;
915
        m.print();
916
      }
917
      Debug("normal-form") << "end list" << std::endl;
918
    }
919
  }
920
921
  /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
922
13688744
  bool allIntegralVariables() const {
923
31180597
    for(iterator i = begin(), e=end(); i!=e; ++i){
924
18713772
      if(!(*i).integralVariables()){
925
1221919
        return false;
926
      }
927
    }
928
12466825
    return true;
929
  }
930
931
  /**
932
   * A Polynomial is an "integral" polynomial if all of the monomials are integral
933
   * and all of the coefficients are Integral. */
934
11774093
  bool isIntegral() const {
935
26647973
    for(iterator i = begin(), e=end(); i!=e; ++i){
936
16788087
      if(!(*i).isIntegral()){
937
1914207
        return false;
938
      }
939
    }
940
9859886
    return true;
941
  }
942
943
  static Polynomial sumPolynomials(const std::vector<Polynomial>& polynomials);
944
945
  /** Returns true if the polynomial contains a non-linear monomial.*/
946
  bool isNonlinear() const;
947
948
  /** Check whether this polynomial is only a single variable. */
949
  bool isVariable() const
950
  {
951
    return singleton() && getHead().getVarList().singleton()
952
           && getHead().coefficientIsOne();
953
  }
954
  /** Return the variable, given that isVariable() holds. */
955
  Variable getVariable() const
956
  {
957
    Assert(isVariable());
958
    return getHead().getVarList().getHead();
959
  }
960
961
  /**
962
   * Selects a minimal monomial in the polynomial by the absolute value of
963
   * the coefficient.
964
   */
965
  Monomial selectAbsMinimum() const;
966
967
  /** Returns true if the absolute value of the head coefficient is one. */
968
  bool leadingCoefficientIsAbsOne() const;
969
  bool leadingCoefficientIsPositive() const;
970
  bool denominatorLCMIsOne() const;
971
  bool numeratorGCDIsOne() const;
972
973
3258780
  bool signNormalizedReducedSum() const {
974
3258780
    return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne();
975
  }
976
977
  /**
978
   * Returns the Least Common Multiple of the denominators of the coefficients
979
   * of the monomials.
980
   */
981
  Integer denominatorLCM() const;
982
983
  /**
984
   * Returns the GCD of the numerators of the monomials.
985
   * Requires this to be an isIntegral() polynomial.
986
   */
987
  Integer numeratorGCD() const;
988
989
  /**
990
   * Returns the GCD of the coefficients of the monomials.
991
   * Requires this to be an isIntegral() polynomial.
992
   */
993
  Integer gcd() const;
994
995
  /** z must divide all of the coefficients of the polynomial. */
996
  Polynomial exactDivide(const Integer& z) const;
997
998
  Polynomial operator+(const Polynomial& vl) const;
999
  Polynomial operator-(const Polynomial& vl) const;
1000
861517
  Polynomial operator-() const{
1001
861517
    return (*this) * Rational(-1);
1002
  }
1003
1004
  Polynomial operator*(const Rational& q) const;
1005
  Polynomial operator*(const Constant& c) const;
1006
  Polynomial operator*(const Monomial& mono) const;
1007
1008
  Polynomial operator*(const Polynomial& poly) const;
1009
1010
  /**
1011
   * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
1012
   * The quotient and remainder of p divided by the non-zero integer z is:
1013
   *   q := [(* floor(coeff_i/z) mono_i )]
1014
   *   r := [(* rem(coeff_i/z) mono_i)]
1015
   * computeQR(p,z) returns the node (+ q r).
1016
   *
1017
   * q and r are members of the Polynomial class.
1018
   * For example:
1019
   * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
1020
   *   (+ (+ 2 x (* 4 y)) (+ 1 x))
1021
   */
1022
  static Node computeQR(const Polynomial& p, const Integer& z);
1023
1024
  /** Returns the coefficient associated with the VarList in the polynomial. */
1025
  Constant getCoefficient(const VarList& vl) const;
1026
1027
80990
  uint32_t maxLength() const{
1028
161980
    iterator i = begin(), e=end();
1029
80990
    if( i == e){
1030
      return 1;
1031
    }else{
1032
80990
      uint32_t max = (*i).coefficientLength();
1033
80990
      ++i;
1034
276154
      for(; i!=e; ++i){
1035
97582
        uint32_t curr = (*i).coefficientLength();
1036
97582
        if(curr > max){
1037
19111
          max = curr;
1038
        }
1039
      }
1040
80990
      return max;
1041
    }
1042
  }
1043
1044
5585790
  uint32_t numMonomials() const {
1045
5585790
    if( getNode().getKind() == kind::PLUS ){
1046
27684
      return getNode().getNumChildren();
1047
5558106
    }else if(isZero()){
1048
      return 0;
1049
    }else{
1050
5558106
      return 1;
1051
    }
1052
  }
1053
1054
338334
  const Rational& asConstant() const{
1055
338334
    Assert(isConstant());
1056
338334
    return getNode().getConst<Rational>();
1057
    //return getHead().getConstant().getValue();
1058
  }
1059
1060
3761651
  bool isVarList() const {
1061
3761651
    if(singleton()){
1062
3439514
      return VarList::isMember(getNode());
1063
    }else{
1064
322137
      return false;
1065
    }
1066
  }
1067
1068
1103024
  VarList asVarList() const {
1069
1103024
    Assert(isVarList());
1070
1103024
    return getHead().getVarList();
1071
  }
1072
1073
  size_t getComplexity() const;
1074
1075
  friend class SumPair;
1076
  friend class Comparison;
1077
1078
  /** Returns a node that if asserted ensures v is the abs of this polynomial.*/
1079
  Node makeAbsCondition(Variable v){
1080
    return makeAbsCondition(v, *this);
1081
  }
1082
1083
  /** Returns a node that if asserted ensures v is the abs of p.*/
1084
  static Node makeAbsCondition(Variable v, Polynomial p);
1085
1086
};/* class Polynomial */
1087
1088
1089
/**
1090
 * SumPair is a utility class that extends polynomials for use in computations.
1091
 * A SumPair is always a combination of (+ p c) where
1092
 *  c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1093
 *
1094
 * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1095
 * is known to implicitly be equal to 0.
1096
 *
1097
 * SumPairs do not have unique representations due to the potential for p = 0.
1098
 * This makes them inappropriate for normal forms.
1099
 */
1100
1884977
class SumPair : public NodeWrapper {
1101
private:
1102
1539835
  static Node toNode(const Polynomial& p, const Constant& c){
1103
1539835
    return NodeManager::currentNM()->mkNode(kind::PLUS, p.getNode(), c.getNode());
1104
  }
1105
1106
380
  SumPair(TNode n) : NodeWrapper(n) { Assert(isNormalForm()); }
1107
1108
 public:
1109
190
  SumPair(const Polynomial& p):
1110
190
    NodeWrapper(toNode(p, Constant::mkConstant(0)))
1111
  {
1112
190
    Assert(isNormalForm());
1113
190
  }
1114
1115
1539645
  SumPair(const Polynomial& p, const Constant& c):
1116
1539645
    NodeWrapper(toNode(p, c))
1117
  {
1118
1539645
    Assert(isNormalForm());
1119
1539645
  }
1120
1121
1540215
  static bool isMember(TNode n) {
1122
1540215
    if(n.getKind() == kind::PLUS && n.getNumChildren() == 2){
1123
1540215
      if(Constant::isMember(n[1])){
1124
1540215
        if(Polynomial::isMember(n[0])){
1125
3080430
          Polynomial p = Polynomial::parsePolynomial(n[0]);
1126
1540215
          return p.isZero() || (!p.containsConstant());
1127
        }else{
1128
          return false;
1129
        }
1130
      }else{
1131
        return false;
1132
      }
1133
    }else{
1134
      return false;
1135
    }
1136
  }
1137
1138
1540215
  bool isNormalForm() const {
1139
1540215
    return isMember(getNode());
1140
  }
1141
1142
6809344
  Polynomial getPolynomial() const {
1143
6809344
    return Polynomial::parsePolynomial(getNode()[0]);
1144
  }
1145
1146
2091560
  Constant getConstant() const {
1147
2091560
    return Constant::mkConstant((getNode())[1]);
1148
  }
1149
1150
33257
  SumPair operator+(const SumPair& other) const {
1151
66514
    return SumPair(getPolynomial() + other.getPolynomial(),
1152
99771
                   getConstant() + other.getConstant());
1153
  }
1154
1155
86262
  SumPair operator*(const Constant& c) const {
1156
86262
    return SumPair(getPolynomial() * c, getConstant() * c);
1157
  }
1158
1159
190
  SumPair operator-(const SumPair& other) const {
1160
190
    return (*this) + (other * Constant::mkConstant(-1));
1161
  }
1162
1163
  static SumPair mkSumPair(const Polynomial& p);
1164
1165
190
  static SumPair mkSumPair(const Variable& var){
1166
190
    return SumPair(Polynomial::mkPolynomial(var));
1167
  }
1168
1169
380
  static SumPair parseSumPair(TNode n){
1170
380
    return SumPair(n);
1171
  }
1172
1173
257838
  bool isIntegral() const{
1174
257838
    return getConstant().isIntegral() && getPolynomial().isIntegral();
1175
  }
1176
1177
436224
  bool isConstant() const {
1178
436224
    return getPolynomial().isZero();
1179
  }
1180
1181
1717
  bool isZero() const {
1182
1717
    return getConstant().isZero() && isConstant();
1183
  }
1184
1185
  uint32_t size() const{
1186
    return getPolynomial().size();
1187
  }
1188
1189
33674
  bool isNonlinear() const{
1190
33674
    return getPolynomial().isNonlinear();
1191
  }
1192
1193
  /**
1194
   * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1195
   * The SumPair must be integral.
1196
   */
1197
156530
  Integer gcd() const {
1198
156530
    Assert(isIntegral());
1199
156530
    return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1200
  }
1201
1202
80990
  uint32_t maxLength() const {
1203
80990
    Assert(isIntegral());
1204
80990
    return std::max(getPolynomial().maxLength(), getConstant().length());
1205
  }
1206
1207
328
  static SumPair mkZero() {
1208
328
    return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1209
  }
1210
1211
  static Node computeQR(const SumPair& sp, const Integer& div);
1212
1213
};/* class SumPair */
1214
1215
/* class OrderedPolynomialPair { */
1216
/* private: */
1217
/*   Polynomial d_first; */
1218
/*   Polynomial d_second; */
1219
/* public: */
1220
/*   OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1221
/*     : d_first(f), */
1222
/*       d_second(s) */
1223
/*   {} */
1224
1225
/*   /\** Returns the first part of the pair. *\/ */
1226
/*   const Polynomial& getFirst() const { */
1227
/*     return d_first; */
1228
/*   } */
1229
1230
/*   /\** Returns the second part of the pair. *\/ */
1231
/*   const Polynomial& getSecond() const { */
1232
/*     return d_second; */
1233
/*   } */
1234
1235
/*   OrderedPolynomialPair operator*(const Constant& c) const; */
1236
/*   OrderedPolynomialPair operator+(const Polynomial& p) const; */
1237
1238
/*   /\** Returns true if both of the polynomials are constant. *\/ */
1239
/*   bool isConstant() const; */
1240
1241
/*   /\** */
1242
/*    * Evaluates an isConstant() ordered pair as if */
1243
/*    *   (k getFirst() getRight()) */
1244
/*    *\/ */
1245
/*   bool evaluateConstant(Kind k) const; */
1246
1247
/*   /\** */
1248
/*    * Returns the Least Common Multiple of the monomials */
1249
/*    * on the lefthand side and the constant on the right. */
1250
/*    *\/ */
1251
/*   Integer denominatorLCM() const; */
1252
1253
/*   /\** Constructs a SumPair. *\/ */
1254
/*   SumPair toSumPair() const; */
1255
1256
1257
/*   OrderedPolynomialPair divideByGCD() const; */
1258
/*   OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1259
1260
/*   /\** */
1261
/*    * Returns true if all of the variables are integers, */
1262
/*    * and the coefficients are integers. */
1263
/*    *\/ */
1264
/*   bool isIntegral() const; */
1265
1266
/*   /\** Returns true if all of the variables are integers. *\/ */
1267
/*   bool allIntegralVariables() const { */
1268
/*     return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1269
/*   } */
1270
/* }; */
1271
1272
7514808
class Comparison : public NodeWrapper {
1273
private:
1274
1275
  static Node toNode(Kind k, const Polynomial& l, const Constant& c);
1276
  static Node toNode(Kind k, const Polynomial& l, const Polynomial& r);
1277
1278
  Comparison(TNode n);
1279
1280
  /**
1281
   * Creates a node in normal form equivalent to (= l 0).
1282
   * All variables in l are integral.
1283
   */
1284
  static Node mkIntEquality(const Polynomial& l);
1285
1286
  /**
1287
   * Creates a comparison equivalent to (k l 0).
1288
   * k is either GT or GEQ.
1289
   * All variables in l are integral.
1290
   */
1291
  static Node mkIntInequality(Kind k, const Polynomial& l);
1292
1293
  /**
1294
   * Creates a node equivalent to (= l 0).
1295
   * It is not the case that all variables in l are integral.
1296
   */
1297
  static Node mkRatEquality(const Polynomial& l);
1298
1299
  /**
1300
   * Creates a comparison equivalent to (k l 0).
1301
   * k is either GT or GEQ.
1302
   * It is not the case that all variables in l are integral.
1303
   */
1304
  static Node mkRatInequality(Kind k, const Polynomial& l);
1305
1306
public:
1307
1308
337817
  Comparison(bool val) :
1309
337817
    NodeWrapper(NodeManager::currentNM()->mkConst(val))
1310
337817
  { }
1311
1312
  /**
1313
   * Given a literal to TheoryArith return a single kind to
1314
   * to indicate its underlying structure.
1315
   * The function returns the following in each case:
1316
   * - (K left right)           -> K where is either EQUAL, GT, or GEQ
1317
   * - (CONST_BOOLEAN b)        -> CONST_BOOLEAN
1318
   * - (NOT (EQUAL left right)) -> DISTINCT
1319
   * - (NOT (GT left right))    -> LEQ
1320
   * - (NOT (GEQ left right))   -> LT
1321
   * If none of these match, it returns UNDEFINED_KIND.
1322
   */
1323
  static Kind comparisonKind(TNode literal);
1324
1325
32273435
  Kind comparisonKind() const { return comparisonKind(getNode()); }
1326
1327
  static Comparison mkComparison(Kind k, const Polynomial& l, const Polynomial& r);
1328
1329
  /** Returns true if the comparison is a boolean constant. */
1330
  bool isBoolean() const;
1331
1332
  /**
1333
   * Returns true if the comparison is either a boolean term,
1334
   * in integer normal form or mixed normal form.
1335
   */
1336
  bool isNormalForm() const;
1337
1338
private:
1339
  bool isNormalGT() const;
1340
  bool isNormalGEQ() const;
1341
1342
  bool isNormalLT() const;
1343
  bool isNormalLEQ() const;
1344
1345
  bool isNormalEquality() const;
1346
  bool isNormalDistinct() const;
1347
  bool isNormalEqualityOrDisequality() const;
1348
1349
5536974
  bool allIntegralVariables() const {
1350
5536974
    return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1351
  }
1352
  bool rightIsConstant() const;
1353
1354
public:
1355
  Polynomial getLeft() const;
1356
  Polynomial getRight() const;
1357
1358
  /* /\** Normal form check if at least one variable is real. *\/ */
1359
  /* bool isMixedCompareNormalForm() const; */
1360
1361
  /* /\** Normal form check if at least one variable is real. *\/ */
1362
  /* bool isMixedEqualsNormalForm() const; */
1363
1364
  /* /\** Normal form check is all variables are integer.*\/ */
1365
  /* bool isIntegerCompareNormalForm() const; */
1366
1367
  /* /\** Normal form check is all variables are integer.*\/ */
1368
  /* bool isIntegerEqualsNormalForm() const; */
1369
1370
1371
  /**
1372
   * Returns true if all of the variables are integers, the coefficients are integers,
1373
   * and the right hand coefficient is an integer.
1374
   */
1375
  bool debugIsIntegral() const;
1376
1377
  static Comparison parseNormalForm(TNode n);
1378
1379
733399
  inline static bool isNormalAtom(TNode n){
1380
1466798
    Comparison parse = Comparison::parseNormalForm(n);
1381
1466798
    return parse.isNormalForm();
1382
  }
1383
1384
  size_t getComplexity() const;
1385
1386
  SumPair toSumPair() const;
1387
1388
  Polynomial normalizedVariablePart() const;
1389
  DeltaRational normalizedDeltaRational() const;
1390
1391
  /**
1392
   * Transforms a Comparison object into a stronger normal form:
1393
   *    Polynomial ~Kind~ Constant
1394
   *
1395
   * From the comparison, this method resolved a negation (if present) and
1396
   * moves everything to the left side.
1397
   * If split_constant is false, the constant is always zero.
1398
   * If split_constant is true, the polynomial has no constant term and is
1399
   * normalized to have leading coefficient one.
1400
   */
1401
  std::tuple<Polynomial, Kind, Constant> decompose(
1402
      bool split_constant = false) const;
1403
1404
};/* class Comparison */
1405
1406
}/* CVC4::theory::arith namespace */
1407
}/* CVC4::theory namespace */
1408
}/* CVC4 namespace */
1409
1410
#endif /* CVC4__THEORY__ARITH__NORMAL_FORM_H */