1 /********************* */
2 /*! \file normal_form.cpp
4 ** Original author: Tim King
5 ** Major contributors: none
6 ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters
7 ** This file is part of the CVC4 project.
8 ** Copyright (c) 2009-2013 New York University and The University of Iowa
9 ** See the file COPYING in the top-level source directory for licensing
10 ** information.\endverbatim
12 ** \brief [[ Add one-line brief description here ]]
14 ** [[ Add lengthier description here ]]
15 ** \todo document this file
18 #include "theory/arith/normal_form.h"
19 #include "theory/arith/arith_utilities.h"
28 bool Variable::isDivMember(Node n
){
31 case kind::INTS_DIVISION
:
32 case kind::INTS_MODULUS
:
33 case kind::DIVISION_TOTAL
:
34 case kind::INTS_DIVISION_TOTAL
:
35 case kind::INTS_MODULUS_TOTAL
:
36 return Polynomial::isMember(n
[0]) && Polynomial::isMember(n
[1]);
42 bool VarList::isSorted(iterator start
, iterator end
) {
43 return __gnu_cxx::is_sorted(start
, end
);
46 bool VarList::isMember(Node n
) {
47 if(Variable::isMember(n
)) {
50 if(n
.getKind() == kind::MULT
) {
51 Node::iterator curr
= n
.begin(), end
= n
.end();
53 if(!Variable::isMember(prev
)) return false;
55 while( (++curr
) != end
) {
56 if(!Variable::isMember(*curr
)) return false;
57 if(!(prev
<= *curr
)) return false;
65 int VarList::cmp(const VarList
& vl
) const {
66 int dif
= this->size() - vl
.size();
68 return this->getNode().getId() - vl
.getNode().getId();
76 VarList
VarList::parseVarList(Node n
) {
77 if(Variable::isMember(n
)) {
78 return VarList(Variable(n
));
80 Assert(n
.getKind() == kind::MULT
);
81 for(Node::iterator i
=n
.begin(), end
= n
.end(); i
!=end
; ++i
) {
82 Assert(Variable::isMember(*i
));
88 VarList
VarList::operator*(const VarList
& other
) const {
91 } else if(other
.empty()) {
97 thisBegin
= this->internalBegin(),
98 thisEnd
= this->internalEnd(),
99 otherBegin
= other
.internalBegin(),
100 otherEnd
= other
.internalEnd();
102 merge_ranges(thisBegin
, thisEnd
, otherBegin
, otherEnd
, result
);
104 Assert(result
.size() >= 2);
105 Node mult
= NodeManager::currentNM()->mkNode(kind::MULT
, result
);
106 return VarList::parseVarList(mult
);
110 bool Monomial::isMember(TNode n
){
111 if(n
.getKind() == kind::CONST_RATIONAL
) {
113 } else if(multStructured(n
)) {
114 return VarList::isMember(n
[1]);
116 return VarList::isMember(n
);
120 Monomial
Monomial::mkMonomial(const Constant
& c
, const VarList
& vl
) {
121 if(c
.isZero() || vl
.empty() ) {
123 } else if(c
.isOne()) {
126 return Monomial(c
, vl
);
129 Monomial
Monomial::parseMonomial(Node n
) {
130 if(n
.getKind() == kind::CONST_RATIONAL
) {
131 return Monomial(Constant(n
));
132 } else if(multStructured(n
)) {
133 return Monomial::mkMonomial(Constant(n
[0]),VarList::parseVarList(n
[1]));
135 return Monomial(VarList::parseVarList(n
));
138 Monomial
Monomial::operator*(const Rational
& q
) const {
142 Constant newConstant
= this->getConstant() * q
;
143 return Monomial::mkMonomial(newConstant
, getVarList());
147 Monomial
Monomial::operator*(const Constant
& c
) const {
148 return (*this) * c
.getValue();
152 // Constant newConstant = this->getConstant() * c;
153 // return Monomial::mkMonomial(newConstant, getVarList());
157 Monomial
Monomial::operator*(const Monomial
& mono
) const {
158 Constant newConstant
= this->getConstant() * mono
.getConstant();
159 VarList newVL
= this->getVarList() * mono
.getVarList();
161 return Monomial::mkMonomial(newConstant
, newVL
);
164 vector
<Monomial
> Monomial::sumLikeTerms(const std::vector
<Monomial
> & monos
) {
165 Assert(isSorted(monos
));
166 vector
<Monomial
> outMonomials
;
167 typedef vector
<Monomial
>::const_iterator iterator
;
168 for(iterator rangeIter
= monos
.begin(), end
=monos
.end(); rangeIter
!= end
;) {
169 Rational constant
= (*rangeIter
).getConstant().getValue();
170 VarList varList
= (*rangeIter
).getVarList();
172 while(rangeIter
!= end
&& varList
== (*rangeIter
).getVarList()) {
173 constant
+= (*rangeIter
).getConstant().getValue();
177 Constant asConstant
= Constant::mkConstant(constant
);
178 Monomial nonZero
= Monomial::mkMonomial(asConstant
, varList
);
179 outMonomials
.push_back(nonZero
);
183 Assert(isStrictlySorted(outMonomials
));
187 void Monomial::print() const {
188 Debug("normal-form") << getNode() << std::endl
;
191 void Monomial::printList(const std::vector
<Monomial
>& list
) {
192 for(vector
<Monomial
>::const_iterator i
= list
.begin(), end
= list
.end(); i
!= end
; ++i
) {
193 const Monomial
& m
=*i
;
197 Polynomial
Polynomial::operator+(const Polynomial
& vl
) const {
199 std::vector
<Monomial
> sortedMonos
;
200 merge_ranges(begin(), end(), vl
.begin(), vl
.end(), sortedMonos
);
202 std::vector
<Monomial
> combined
= Monomial::sumLikeTerms(sortedMonos
);
204 Polynomial result
= mkPolynomial(combined
);
208 Polynomial
Polynomial::operator-(const Polynomial
& vl
) const {
209 Constant negOne
= Constant::mkConstant(Rational(-1));
211 return *this + (vl
*negOne
);
214 Polynomial
Polynomial::operator*(const Rational
& q
) const{
216 return Polynomial::mkZero();
220 std::vector
<Monomial
> newMonos
;
221 for(iterator i
= this->begin(), end
= this->end(); i
!= end
; ++i
) {
222 newMonos
.push_back((*i
)*q
);
225 Assert(Monomial::isStrictlySorted(newMonos
));
226 return Polynomial::mkPolynomial(newMonos
);
230 Polynomial
Polynomial::operator*(const Constant
& c
) const{
231 return (*this) * c
.getValue();
233 // return Polynomial::mkZero();
234 // }else if(c.isOne()){
237 // std::vector<Monomial> newMonos;
238 // for(iterator i = this->begin(), end = this->end(); i != end; ++i) {
239 // newMonos.push_back((*i)*c);
242 // Assert(Monomial::isStrictlySorted(newMonos));
243 // return Polynomial::mkPolynomial(newMonos);
247 Polynomial
Polynomial::operator*(const Monomial
& mono
) const {
249 return Polynomial(mono
); //Don't multiply by zero
251 std::vector
<Monomial
> newMonos
;
252 for(iterator i
= this->begin(), end
= this->end(); i
!= end
; ++i
) {
253 newMonos
.push_back(mono
* (*i
));
256 // We may need to sort newMonos.
257 // Suppose this = (+ x y), mono = x, (* x y).getId() < (* x x).getId()
258 // newMonos = <(* x x), (* x y)> after this loop.
259 // This is not sorted according to the current VarList order.
260 std::sort(newMonos
.begin(), newMonos
.end());
261 return Polynomial::mkPolynomial(newMonos
);
265 Polynomial
Polynomial::operator*(const Polynomial
& poly
) const {
266 Polynomial res
= Polynomial::mkZero();
267 for(iterator i
= this->begin(), end
= this->end(); i
!= end
; ++i
) {
269 Polynomial prod
= poly
* curr
;
270 Polynomial sum
= res
+ prod
;
276 Monomial
Polynomial::selectAbsMinimum() const {
277 iterator iter
= begin(), myend
= end();
278 Assert(iter
!= myend
);
280 Monomial min
= *iter
;
282 for(; iter
!= end(); ++iter
){
283 Monomial curr
= *iter
;
284 if(curr
.absLessThan(min
)){
291 bool Polynomial::leadingCoefficientIsAbsOne() const {
292 return getHead().absCoefficientIsOne();
294 bool Polynomial::leadingCoefficientIsPositive() const {
295 return getHead().getConstant().isPositive();
298 bool Polynomial::denominatorLCMIsOne() const {
299 return denominatorLCM().isOne();
302 bool Polynomial::numeratorGCDIsOne() const {
303 return gcd().isOne();
306 Integer
Polynomial::gcd() const {
307 Assert(isIntegral());
308 return numeratorGCD();
311 Integer
Polynomial::numeratorGCD() const {
312 //We'll use the standardization that gcd(0, 0) = 0
313 //So that the gcd of the zero polynomial is gcd{0} = 0
314 iterator i
=begin(), e
=end();
317 Integer d
= (*i
).getConstant().getValue().getNumerator().abs();
320 Integer c
= (*i
).getConstant().getValue().getNumerator();
326 Integer
Polynomial::denominatorLCM() const {
328 for(iterator i
=begin(), e
=end(); i
!=e
; ++i
){
329 const Constant
& c
= (*i
).getConstant();
330 tmp
= tmp
.lcm(c
.getValue().getDenominator());
336 Constant
Polynomial::getCoefficient(const VarList
& vl
) const{
337 //TODO improve to binary search...
338 for(iterator iter
=begin(), myend
=end(); iter
!= myend
; ++iter
){
340 VarList curr
= m
.getVarList();
342 return m
.getConstant();
345 return Constant::mkConstant(0);
348 Node
Polynomial::computeQR(const Polynomial
& p
, const Integer
& div
){
349 Assert(p
.isIntegral());
350 std::vector
<Monomial
> q_vec
, r_vec
;
351 Integer tmp_q
, tmp_r
;
352 for(iterator iter
= p
.begin(), pend
= p
.end(); iter
!= pend
; ++iter
){
353 Monomial curr
= *iter
;
354 VarList vl
= curr
.getVarList();
355 Constant c
= curr
.getConstant();
357 const Integer
& a
= c
.getValue().getNumerator();
358 Integer::floorQR(tmp_q
, tmp_r
, a
, div
);
359 Constant q
=Constant::mkConstant(tmp_q
);
360 Constant r
=Constant::mkConstant(tmp_r
);
362 q_vec
.push_back(Monomial::mkMonomial(q
, vl
));
365 r_vec
.push_back(Monomial::mkMonomial(r
, vl
));
369 Polynomial p_q
= Polynomial::mkPolynomial(q_vec
);
370 Polynomial p_r
= Polynomial::mkPolynomial(r_vec
);
372 return NodeManager::currentNM()->mkNode(kind::PLUS
, p_q
.getNode(), p_r
.getNode());
376 Monomial
Polynomial::minimumVariableMonomial() const{
377 Assert(!isConstant());
381 iterator i
= begin();
383 if( first
.isConstant() ){
393 bool Polynomial::variableMonomialAreStrictlyGreater(const Monomial
& m
) const{
397 Monomial minimum
= minimumVariableMonomial();
398 Debug("nf::tmp") << "minimum " << minimum
.getNode() << endl
;
399 Debug("nf::tmp") << "m " << m
.getNode() << endl
;
404 Node
SumPair::computeQR(const SumPair
& sp
, const Integer
& div
){
405 Assert(sp
.isIntegral());
407 const Integer
& constant
= sp
.getConstant().getValue().getNumerator();
409 Integer constant_q
, constant_r
;
410 Integer::floorQR(constant_q
, constant_r
, constant
, div
);
412 Node p_qr
= Polynomial::computeQR(sp
.getPolynomial(), div
);
413 Assert(p_qr
.getKind() == kind::PLUS
);
414 Assert(p_qr
.getNumChildren() == 2);
416 Polynomial p_q
= Polynomial::parsePolynomial(p_qr
[0]);
417 Polynomial p_r
= Polynomial::parsePolynomial(p_qr
[1]);
419 SumPair
sp_q(p_q
, Constant::mkConstant(constant_q
));
420 SumPair
sp_r(p_r
, Constant::mkConstant(constant_r
));
422 return NodeManager::currentNM()->mkNode(kind::PLUS
, sp_q
.getNode(), sp_r
.getNode());
425 SumPair
SumPair::mkSumPair(const Polynomial
& p
){
427 Constant leadingConstant
= p
.getHead().getConstant();
428 return SumPair(Polynomial::mkZero(), leadingConstant
);
429 }else if(p
.containsConstant()){
430 Assert(!p
.singleton());
431 return SumPair(p
.getTail(), p
.getHead().getConstant());
433 return SumPair(p
, Constant::mkZero());
437 Comparison::Comparison(TNode n
)
440 Assert(isNormalForm());
445 SumPair
Comparison::toSumPair() const {
446 Kind cmpKind
= comparisonKind();
453 TNode lit
= getNode();
454 TNode atom
= (cmpKind
== kind::LT
|| cmpKind
== kind::LEQ
) ? lit
[0] : lit
;
455 Polynomial p
= Polynomial::parsePolynomial(atom
[0]);
456 Constant c
= Constant::mkConstant(atom
[1]);
457 if(p
.leadingCoefficientIsPositive()){
458 return SumPair(p
, -c
);
460 return SumPair(-p
, c
);
466 Polynomial left
= getLeft();
467 Polynomial right
= getRight();
468 Debug("nf::tmp") << "left: " << left
.getNode() << endl
;
469 Debug("nf::tmp") << "right: " << right
.getNode() << endl
;
470 if(right
.isConstant()){
471 return SumPair(left
, -right
.getHead().getConstant());
472 }else if(right
.containsConstant()){
473 Assert(!right
.singleton());
475 Polynomial noConstant
= right
.getTail();
476 return SumPair(left
- noConstant
, -right
.getHead().getConstant());
478 return SumPair(left
- right
, Constant::mkZero());
486 Polynomial
Comparison::normalizedVariablePart() const {
487 Kind cmpKind
= comparisonKind();
494 TNode lit
= getNode();
495 TNode atom
= (cmpKind
== kind::LT
|| cmpKind
== kind::LEQ
) ? lit
[0] : lit
;
496 Polynomial p
= Polynomial::parsePolynomial(atom
[0]);
497 if(p
.leadingCoefficientIsPositive()){
506 Polynomial left
= getLeft();
507 Polynomial right
= getRight();
508 if(right
.isConstant()){
511 Polynomial noConstant
= right
.containsConstant() ? right
.getTail() : right
;
512 Polynomial diff
= left
- noConstant
;
513 if(diff
.leadingCoefficientIsPositive()){
525 DeltaRational
Comparison::normalizedDeltaRational() const {
526 Kind cmpKind
= comparisonKind();
527 int delta
= deltaCoeff(cmpKind
);
534 Node lit
= getNode();
535 Node atom
= (cmpKind
== kind::LT
|| cmpKind
== kind::LEQ
) ? lit
[0] : lit
;
536 Polynomial left
= Polynomial::parsePolynomial(atom
[0]);
537 const Rational
& q
= atom
[1].getConst
<Rational
>();
538 if(left
.leadingCoefficientIsPositive()){
539 return DeltaRational(q
, delta
);
541 return DeltaRational(-q
, -delta
);
547 Polynomial right
= getRight();
548 Monomial firstRight
= right
.getHead();
549 if(firstRight
.isConstant()){
550 DeltaRational c
= DeltaRational(firstRight
.getConstant().getValue(), 0);
551 Polynomial left
= getLeft();
552 if(!left
.allIntegralVariables()){
554 //this is a qpolynomial and the sign of the leading
555 //coefficient will not change after the diff below
557 // the polynomial may be a z polynomial in which case
558 // taking the diff is the simplest and obviously correct means
559 Polynomial diff
= right
.singleton() ? left
: left
- right
.getTail();
560 if(diff
.leadingCoefficientIsPositive()){
566 }else{ // The constant is 0 sign cannot change
567 return DeltaRational(0, 0);
575 Comparison
Comparison::parseNormalForm(TNode n
) {
576 Comparison
result(n
);
577 Assert(result
.isNormalForm());
581 Node
Comparison::toNode(Kind k
, const Polynomial
& l
, const Constant
& r
) {
582 Assert(isRelationOperator(k
));
586 return NodeManager::currentNM()->mkNode(k
, l
.getNode(), r
.getNode());
592 Node
Comparison::toNode(Kind k
, const Polynomial
& l
, const Polynomial
& r
) {
593 Assert(isRelationOperator(k
));
598 return NodeManager::currentNM()->mkNode(k
, l
.getNode(), r
.getNode());
600 return toNode(kind::GEQ
, r
, l
).notNode();
602 return toNode(kind::GT
, r
, l
).notNode();
604 return toNode(kind::EQUAL
, r
, l
).notNode();
610 bool Comparison::rightIsConstant() const {
611 if(getNode().getKind() == kind::NOT
){
612 return getNode()[0][1].getKind() == kind::CONST_RATIONAL
;
614 return getNode()[1].getKind() == kind::CONST_RATIONAL
;
618 Polynomial
Comparison::getLeft() const {
620 Kind k
= comparisonKind();
625 left
= getNode()[0][0];
635 return Polynomial::parsePolynomial(left
);
638 Polynomial
Comparison::getRight() const {
640 Kind k
= comparisonKind();
645 right
= getNode()[0][1];
650 right
= getNode()[1];
655 return Polynomial::parsePolynomial(right
);
658 // Polynomial Comparison::getLeft() const {
659 // Node n = getNode();
660 // Node left = (n.getKind() == kind::NOT ? n[0]: n)[0];
661 // return Polynomial::parsePolynomial(left);
664 // Polynomial Comparison::getRight() const {
665 // Node n = getNode();
666 // Node right = (n.getKind() == kind::NOT ? n[0]: n)[1];
667 // return Polynomial::parsePolynomial(right);
670 bool Comparison::isNormalForm() const {
672 Kind cmpKind
= comparisonKind(n
);
673 Debug("nf::tmp") << "isNormalForm " << n
<< " " << cmpKind
<< endl
;
675 case kind::CONST_BOOLEAN
:
680 return isNormalGEQ();
682 return isNormalEquality();
686 return isNormalLEQ();
688 return isNormalDistinct();
694 /** This must be (> qpolynomial constant) */
695 bool Comparison::isNormalGT() const {
697 Assert(n
.getKind() == kind::GT
);
698 if(!rightIsConstant()){
701 Polynomial left
= getLeft();
702 if(left
.containsConstant()){
704 }else if(!left
.leadingCoefficientIsAbsOne()){
707 return !left
.isIntegral();
712 /** This must be (not (> qpolynomial constant)) */
713 bool Comparison::isNormalLEQ() const {
715 Debug("nf::tmp") << "isNormalLEQ " << n
<< endl
;
716 Assert(n
.getKind() == kind::NOT
);
717 Assert(n
[0].getKind() == kind::GT
);
718 if(!rightIsConstant()){
721 Polynomial left
= getLeft();
722 if(left
.containsConstant()){
724 }else if(!left
.leadingCoefficientIsAbsOne()){
727 return !left
.isIntegral();
733 /** This must be (>= qpolynomial constant) or (>= zpolynomial constant) */
734 bool Comparison::isNormalGEQ() const {
736 Assert(n
.getKind() == kind::GEQ
);
738 Debug("nf::tmp") << "isNormalGEQ " << n
<< " " << rightIsConstant() << endl
;
740 if(!rightIsConstant()){
743 Polynomial left
= getLeft();
744 if(left
.containsConstant()){
747 if(left
.isIntegral()){
748 return left
.signNormalizedReducedSum();
750 return left
.leadingCoefficientIsAbsOne();
756 /** This must be (not (>= qpolynomial constant)) or (not (>= zpolynomial constant)) */
757 bool Comparison::isNormalLT() const {
759 Assert(n
.getKind() == kind::NOT
);
760 Assert(n
[0].getKind() == kind::GEQ
);
762 if(!rightIsConstant()){
765 Polynomial left
= getLeft();
766 if(left
.containsConstant()){
769 if(left
.isIntegral()){
770 return left
.signNormalizedReducedSum();
772 return left
.leadingCoefficientIsAbsOne();
779 bool Comparison::isNormalEqualityOrDisequality() const {
780 Polynomial pleft
= getLeft();
782 if(pleft
.numMonomials() == 1){
783 Monomial mleft
= pleft
.getHead();
784 if(mleft
.isConstant()){
787 Polynomial pright
= getRight();
788 if(allIntegralVariables()){
789 const Rational
& lcoeff
= mleft
.getConstant().getValue();
790 if(pright
.isConstant()){
791 return pright
.isIntegral() && lcoeff
.isOne();
793 Polynomial varRight
= pright
.containsConstant() ? pright
.getTail() : pright
;
794 if(lcoeff
.sgn() <= 0){
797 Integer lcm
= lcoeff
.getDenominator().lcm(varRight
.denominatorLCM());
798 Integer g
= lcoeff
.getNumerator().gcd(varRight
.numeratorGCD());
799 Debug("nf::tmp") << lcm
<< " " << g
<< endl
;
802 }else if(!g
.isOne()){
805 Monomial absMinRight
= varRight
.selectAbsMinimum();
806 Debug("nf::tmp") << mleft
.getNode() << " " << absMinRight
.getNode() << endl
;
807 if( mleft
.absLessThan(absMinRight
) ){
810 return (!absMinRight
.absLessThan(mleft
)) && mleft
< absMinRight
;
815 if(mleft
.coefficientIsOne()){
817 << "dfklj " << mleft
.getNode() << endl
818 << pright
.getNode() << endl
819 << pright
.variableMonomialAreStrictlyGreater(mleft
)
821 return pright
.variableMonomialAreStrictlyGreater(mleft
);
832 /** This must be (= qvarlist qpolynomial) or (= zmonomial zpolynomial)*/
833 bool Comparison::isNormalEquality() const {
834 Assert(getNode().getKind() == kind::EQUAL
);
836 return isNormalEqualityOrDisequality();
840 * This must be (not (= qvarlist qpolynomial)) or
841 * (not (= zmonomial zpolynomial)).
843 bool Comparison::isNormalDistinct() const {
844 Assert(getNode().getKind() == kind::NOT
);
845 Assert(getNode()[0].getKind() == kind::EQUAL
);
847 return isNormalEqualityOrDisequality();
850 Node
Comparison::mkRatEquality(const Polynomial
& p
){
851 Assert(!p
.isConstant());
852 Assert(!p
.allIntegralVariables());
854 Monomial minimalVList
= p
.minimumVariableMonomial();
855 Constant coeffInv
= -(minimalVList
.getConstant().inverse());
857 Polynomial newRight
= (p
- minimalVList
) * coeffInv
;
858 Polynomial
newLeft(minimalVList
.getVarList());
860 return toNode(kind::EQUAL
, newLeft
, newRight
);
863 Node
Comparison::mkRatInequality(Kind k
, const Polynomial
& p
){
864 Assert(k
== kind::GEQ
|| k
== kind::GT
);
865 Assert(!p
.isConstant());
866 Assert(!p
.allIntegralVariables());
868 SumPair sp
= SumPair::mkSumPair(p
);
869 Polynomial left
= sp
.getPolynomial();
870 Constant right
= - sp
.getConstant();
872 Monomial minimalVList
= left
.getHead();
873 Assert(!minimalVList
.isConstant());
875 Constant coeffInv
= minimalVList
.getConstant().inverse().abs();
876 Polynomial newLeft
= left
* coeffInv
;
877 Constant newRight
= right
* (coeffInv
);
879 return toNode(k
, newLeft
, newRight
);
882 Node
Comparison::mkIntInequality(Kind k
, const Polynomial
& p
){
883 Assert(kind::GT
== k
|| kind::GEQ
== k
);
884 Assert(!p
.isConstant());
885 Assert(p
.allIntegralVariables());
887 SumPair sp
= SumPair::mkSumPair(p
);
888 Polynomial left
= sp
.getPolynomial();
889 Rational right
= - (sp
.getConstant().getValue());
892 Monomial m
= left
.getHead();
893 Assert(!m
.isConstant());
895 Integer lcm
= left
.denominatorLCM();
896 Integer g
= left
.numeratorGCD();
897 Rational
mult(lcm
,g
);
899 Polynomial newLeft
= left
* mult
;
900 Rational rightMult
= right
* mult
;
902 bool negateResult
= false;
903 if(!newLeft
.leadingCoefficientIsPositive()){
905 // a: left >= right or b: left > right
907 // a: -left <= -right or b: -left < -right
908 // a: not (-left > -right) or b: (not -left >= -right)
910 rightMult
= -rightMult
;
911 k
= (kind::GT
== k
) ? kind::GEQ
: kind::GT
;
913 // the later stages handle:
914 // a: not (-left >= -right + 1) or b: (not -left >= -right)
917 Node result
= Node::null();
918 if(rightMult
.isIntegral()){
922 Constant rightMultPlusOne
= Constant::mkConstant(rightMult
+ 1);
923 result
= toNode(kind::GEQ
, newLeft
, rightMultPlusOne
);
925 Constant newRight
= Constant::mkConstant(rightMult
);
926 result
= toNode(kind::GEQ
, newLeft
, newRight
);
930 //(>= l (ceil (/ n d)))
931 //This also hold for GT as (ceil (/ n d)) > (/ n d)
932 Integer ceilr
= rightMult
.ceiling();
933 Constant ceilRight
= Constant::mkConstant(ceilr
);
934 result
= toNode(kind::GEQ
, newLeft
, ceilRight
);
936 Assert(!result
.isNull());
938 return result
.notNode();
944 Node
Comparison::mkIntEquality(const Polynomial
& p
){
945 Assert(!p
.isConstant());
946 Assert(p
.allIntegralVariables());
948 SumPair sp
= SumPair::mkSumPair(p
);
949 Polynomial varPart
= sp
.getPolynomial();
950 Constant constPart
= sp
.getConstant();
952 Integer lcm
= varPart
.denominatorLCM();
953 Integer g
= varPart
.numeratorGCD();
954 Constant mult
= Constant::mkConstant(Rational(lcm
,g
));
956 Constant constMult
= constPart
* mult
;
958 if(constMult
.isIntegral()){
959 Polynomial varPartMult
= varPart
* mult
;
961 Monomial m
= varPartMult
.selectAbsMinimum();
962 bool mIsPositive
= m
.getConstant().isPositive();
964 Polynomial noM
= (varPartMult
+ (- m
)) + Polynomial(constMult
);
967 Polynomial newRight
= mIsPositive
? -noM
: noM
;
968 Polynomial newLeft
= mIsPositive
? m
: -m
;
970 Assert(newRight
.isIntegral());
971 return toNode(kind::EQUAL
, newLeft
, newRight
);
973 return mkBoolNode(false);
977 Comparison
Comparison::mkComparison(Kind k
, const Polynomial
& l
, const Polynomial
& r
){
979 //Make this special case fast for sharing!
980 if((k
== kind::EQUAL
|| k
== kind::DISTINCT
) && l
.isVarList() && r
.isVarList()){
981 VarList vLeft
= l
.asVarList();
982 VarList vRight
= r
.asVarList();
985 return Comparison(k
== kind::EQUAL
);
987 Node eqNode
= vLeft
< vRight
? toNode( kind::EQUAL
, l
, r
) : toNode( kind::EQUAL
, r
, l
);
988 Node forK
= (k
== kind::DISTINCT
) ? eqNode
.notNode() : eqNode
;
989 return Comparison(forK
);
994 Polynomial diff
= l
- r
;
995 if(diff
.isConstant()){
996 bool res
= evaluateConstantPredicate(k
, diff
.asConstant(), Rational(0));
997 return Comparison(res
);
999 Node result
= Node::null();
1000 bool isInteger
= diff
.allIntegralVariables();
1003 result
= isInteger
? mkIntEquality(diff
) : mkRatEquality(diff
);
1005 case kind::DISTINCT
:
1007 Node eq
= isInteger
? mkIntEquality(diff
) : mkRatEquality(diff
);
1008 result
= eq
.notNode();
1014 Polynomial neg
= - diff
;
1015 Kind negKind
= (k
== kind::LEQ
? kind::GEQ
: kind::GT
);
1016 result
= isInteger
?
1017 mkIntInequality(negKind
, neg
) : mkRatInequality(negKind
, neg
);
1022 result
= isInteger
?
1023 mkIntInequality(k
, diff
) : mkRatInequality(k
, diff
);
1028 Assert(!result
.isNull());
1029 if(result
.getKind() == kind::NOT
&& result
[0].getKind() == kind::CONST_BOOLEAN
){
1030 return Comparison(!(result
[0].getConst
<bool>()));
1032 Comparison
cmp(result
);
1033 Assert(cmp
.isNormalForm());
1039 bool Comparison::isBoolean() const {
1040 return getNode().getKind() == kind::CONST_BOOLEAN
;
1044 bool Comparison::debugIsIntegral() const{
1045 return getLeft().isIntegral() && getRight().isIntegral();
1048 Kind
Comparison::comparisonKind(TNode literal
){
1049 switch(literal
.getKind()){
1050 case kind::CONST_BOOLEAN
:
1054 return literal
.getKind();
1057 TNode negatedAtom
= literal
[0];
1058 switch(negatedAtom
.getKind()){
1059 case kind::GT
: //(not (GT x c)) <=> (LEQ x c)
1061 case kind::GEQ
: //(not (GEQ x c)) <=> (LT x c)
1064 return kind::DISTINCT
;
1066 return kind::UNDEFINED_KIND
;
1070 return kind::UNDEFINED_KIND
;
1075 Node
Polynomial::makeAbsCondition(Variable v
, Polynomial p
){
1076 Polynomial zerop
= Polynomial::mkZero();
1078 Polynomial varp
= Polynomial::mkPolynomial(v
);
1079 Comparison pLeq0
= Comparison::mkComparison(kind::LEQ
, p
, zerop
);
1080 Comparison negP
= Comparison::mkComparison(kind::EQUAL
, varp
, -p
);
1081 Comparison posP
= Comparison::mkComparison(kind::EQUAL
, varp
, p
);
1083 Node absCnd
= (pLeq0
.getNode()).iteNode(negP
.getNode(), posP
.getNode());
1088 } //namespace theory