1 /********************* */
2 /*! \file normal_form.h
4 ** Original author: taking
5 ** Major contributors: mdeters
6 ** Minor contributors (to current version): dejan
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
9 ** Courant Institute of Mathematical Sciences
10 ** New York University
11 ** See the file COPYING in the top-level source directory for licensing
12 ** information.\endverbatim
14 ** \brief [[ Add one-line brief description here ]]
16 ** [[ Add lengthier description here ]]
17 ** \todo document this file
20 #include "cvc4_private.h"
22 #ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
23 #define __CVC4__THEORY__ARITH__NORMAL_FORM_H
25 #include "expr/node.h"
26 #include "expr/node_self_iterator.h"
27 #include "util/rational.h"
28 #include "theory/theory.h"
29 #include "theory/arith/arith_utilities.h"
33 #include <ext/algorithm>
39 /***********************************************/
40 /***************** Normal Form *****************/
41 /***********************************************/
42 /***********************************************/
45 * Section 1: Languages
46 * The normal form for arithmetic nodes is defined by the language
47 * accepted by the following BNFs with some guard conditions.
48 * (The guard conditions are in Section 3 for completeness.)
52 * n.isVar() or is foreign
53 * n.getType() \in {Integer, Real}
57 * n.getKind() == kind::CONST_RATIONAL
59 * var_list := variable | (* [variable])
62 * isSorted varOrder [variable]
64 * monomial := constant | var_list | (* constant' var_list')
66 * \f$ constant' \not\in {0,1} \f$
68 * polynomial := monomial' | (+ [monomial])
71 * isStrictlySorted monoOrder [monomial]
72 * forall (\x -> x != 0) [monomial]
74 * rational_cmp := (|><| qpolynomial constant)
77 * not (exists constantMonomial (monomialList qpolynomial))
78 * (exists realMonomial (monomialList qpolynomial))
79 * abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
81 * integer_cmp := (<= zpolynomial constant)
83 * not (exists constantMonomial (monomialList zpolynomial))
84 * (forall integerMonomial (monomialList zpolynomial))
85 * the gcd of all numerators of coefficients is 1
86 * the denominator of all coefficients and the constant is 1
88 * rational_eq := (= qvarlist qpolynomial)
90 * let allMonomials = (cons qvarlist (monomialList zpolynomial))
91 * let variableMonomials = (drop constantMonomial allMonomials)
92 * isStrictlySorted variableMonomials
93 * exists realMonomial variableMonomials
94 * is not empty qvarlist
96 * integer_eq := (= zmonomial zpolynomial)
98 * let allMonomials = (cons zmonomial (monomialList zpolynomial))
99 * let variableMonomials = (drop constantMonomial allMonomials)
100 * not (constantMonomial zmonomial)
101 * (forall integerMonomial allMonomials)
102 * isStrictlySorted variableMonomials
103 * the gcd of all numerators of coefficients is 1
104 * the denominator of all coefficients and the constant is 1
105 * the coefficient of monomial is positive
106 * the value of the coefficient of monomial is minimal in variableMonomials
108 * comparison := TRUE | FALSE
109 * | rational_cmp | (not rational_cmp)
110 * | rational_eq | (not rational_eq)
111 * | integer_cmp | (not integer_cmp)
112 * | integer_eq | (not integer_eq)
114 * Normal Form for terms := polynomial
115 * Normal Form for atoms := comparison
119 * Section 2: Helper Classes
120 * The langauges accepted by each of these defintions
121 * roughly corresponds to one of the following helper classes:
129 * Each of the classes obeys the following contracts/design decisions:
130 * -Calling isMember(Node node) on a node returns true iff that node is a
131 * a member of the language. Note: isMember is O(n).
132 * -Calling isNormalForm() on a helper class object returns true iff that
133 * helper class currently represents a normal form object.
134 * -If isNormalForm() is false, then this object must have been made
135 * using a mk*() factory function.
136 * -If isNormalForm() is true, calling getNode() on all of these classes
137 * returns a node that would be accepted by the corresponding language.
138 * And if isNormalForm() is false, returns Node::null().
139 * -Each of the classes is immutable.
140 * -Public facing constuctors have a 1-to-1 correspondence with one of
141 * production rules in the above grammar.
142 * -Public facing constuctors are required to fail in debug mode when the
143 * guards of the production rule are not strictly met.
144 * For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
145 * -When a class has a Class parseClass(Node node) function,
146 * if isMember(node) is true, the function is required to return an instance
147 * of the helper class, instance, s.t. instance.getNode() == node.
148 * And if isMember(node) is false, this throws an assertion failure in debug
149 * mode and has undefined behaviour if not in debug mode.
150 * -Only public facing constructors, parseClass(node), and mk*() functions are
151 * considered privileged functions for the helper class.
152 * -Only privileged functions may use private constructors, and access
153 * private data members.
154 * -All non-privileged functions are considered utility functions and
155 * must use a privileged function in order to create an instance of the class.
159 * Section 3: Guard Conditions Misc.
162 * variable_order x y =
163 * if (meta_kind_variable x) and (meta_kind_variable y)
164 * then node_order x y
165 * else if (meta_kind_variable x)
167 * else if (meta_kind_variable y)
169 * else node_order x y
174 * | (* [variable]) -> len [variable]
178 * Empty -> (0,Node::null())
179 * | NonEmpty(vl) -> (var_list_len vl, vl)
181 * var_listOrder a b = tuple_cmp (order a) (order b)
183 * monomialVarList monomial =
184 * match monomial with
186 * | var_list -> NonEmpty(var_list)
187 * | (* constant' var_list') -> NonEmpty(var_list')
189 * monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
191 * integerMonomial mono =
192 * forall varHasTypeInteger (monomialVarList mono)
194 * realMonomial mono = not (integerMonomial mono)
196 * constantMonomial monomial =
197 * match monomial with
199 * | var_list -> false
200 * | (* constant' var_list') -> false
202 * monomialCoefficient monomial =
203 * match monomial with
204 * constant -> constant
205 * | var_list -> Constant(1)
206 * | (* constant' var_list') -> constant'
208 * monomialList polynomial =
209 * match polynomial with
210 * monomial -> monomial::[]
211 * | (+ [monomial]) -> [monomial]
216 * A NodeWrapper is a class that is a thinly veiled container of a Node object.
222 NodeWrapper(Node n
) : node(n
) {}
223 const Node
& getNode() const { return node
; }
224 };/* class NodeWrapper */
227 class Variable
: public NodeWrapper
{
229 Variable(Node n
) : NodeWrapper(n
) {
230 Assert(isMember(getNode()));
233 // TODO: check if it's a theory leaf also
234 static bool isMember(Node n
) {
235 if (n
.getKind() == kind::CONST_RATIONAL
) return false;
236 if (isRelationOperator(n
.getKind())) return false;
237 return Theory::isLeafOf(n
, theory::THEORY_ARITH
);
240 bool isNormalForm() { return isMember(getNode()); }
242 bool isIntegral() const {
243 return getNode().getType().isInteger();
246 bool isMetaKindVariable() const {
247 return getNode().isVar();
250 bool operator<(const Variable
& v
) const {
251 bool thisIsVariable
= isMetaKindVariable();
252 bool vIsVariable
= v
.isMetaKindVariable();
254 if(thisIsVariable
== vIsVariable
){
255 bool thisIsInteger
= isIntegral();
256 bool vIsInteger
= v
.isIntegral();
257 if(thisIsInteger
== vIsInteger
){
258 return getNode() < v
.getNode();
260 return thisIsInteger
&& !vIsInteger
;
263 return thisIsVariable
&& !vIsVariable
;
267 bool operator==(const Variable
& v
) const { return getNode() == v
.getNode();}
269 };/* class Variable */
272 class Constant
: public NodeWrapper
{
274 Constant(Node n
) : NodeWrapper(n
) {
275 Assert(isMember(getNode()));
278 static bool isMember(Node n
) {
279 return n
.getKind() == kind::CONST_RATIONAL
;
282 bool isNormalForm() { return isMember(getNode()); }
284 static Constant
mkConstant(Node n
) {
285 Assert(n
.getKind() == kind::CONST_RATIONAL
);
289 static Constant
mkConstant(const Rational
& rat
) {
290 return Constant(mkRationalNode(rat
));
293 static Constant
mkZero() {
294 return mkConstant(Rational(0));
297 static Constant
mkOne() {
298 return mkConstant(Rational(1));
301 const Rational
& getValue() const {
302 return getNode().getConst
<Rational
>();
305 bool isIntegral() const { return getValue().isIntegral(); }
307 int sgn() const { return getValue().sgn(); }
309 bool isZero() const { return sgn() == 0; }
310 bool isNegative() const { return sgn() < 0; }
311 bool isPositive() const { return sgn() > 0; }
313 bool isOne() const { return getValue() == 1; }
315 Constant
operator*(const Rational
& other
) const {
316 return mkConstant(getValue() * other
);
319 Constant
operator*(const Constant
& other
) const {
320 return mkConstant(getValue() * other
.getValue());
322 Constant
operator+(const Constant
& other
) const {
323 return mkConstant(getValue() + other
.getValue());
325 Constant
operator-() const {
326 return mkConstant(-getValue());
329 Constant
inverse() const{
331 return mkConstant(getValue().inverse());
334 bool operator<(const Constant
& other
) const {
335 return getValue() < other
.getValue();
338 bool operator==(const Constant
& other
) const {
339 //Rely on node uniqueness.
340 return getNode() == other
.getNode();
343 Constant
abs() const {
351 uint32_t length() const{
352 Assert(isIntegral());
353 return getValue().getNumerator().length();
356 };/* class Constant */
359 template <class GetNodeIterator
>
360 inline Node
makeNode(Kind k
, GetNodeIterator start
, GetNodeIterator end
) {
363 while(start
!= end
) {
364 nb
<< (*start
).getNode();
369 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
372 template <class GetNodeIterator
, class T
>
373 static void copy_range(GetNodeIterator begin
, GetNodeIterator end
, std::vector
<T
>& result
){
375 result
.push_back(*begin
);
380 template <class GetNodeIterator
, class T
>
381 static void merge_ranges(GetNodeIterator first1
,
382 GetNodeIterator last1
,
383 GetNodeIterator first2
,
384 GetNodeIterator last2
,
385 std::vector
<T
>& result
) {
387 while(first1
!= last1
&& first2
!= last2
){
388 if( (*first1
) < (*first2
) ){
389 result
.push_back(*first1
);
392 result
.push_back(*first2
);
396 copy_range(first1
, last1
, result
);
397 copy_range(first2
, last2
, result
);
401 * A VarList is a sorted list of variables representing a product.
402 * If the VarList is empty, it represents an empty product or 1.
403 * If the VarList has size 1, it represents a single variable.
405 * A non-sorted VarList can never be successfully made in debug mode.
407 class VarList
: public NodeWrapper
{
410 static Node
multList(const std::vector
<Variable
>& list
) {
411 Assert(list
.size() >= 2);
413 return makeNode(kind::MULT
, list
.begin(), list
.end());
416 VarList() : NodeWrapper(Node::null()) {}
418 VarList(Node n
) : NodeWrapper(n
) {
419 Assert(isSorted(begin(), end()));
422 typedef expr::NodeSelfIterator internal_iterator
;
424 internal_iterator
internalBegin() const {
426 return expr::NodeSelfIterator::self(getNode());
428 return getNode().begin();
432 internal_iterator
internalEnd() const {
434 return expr::NodeSelfIterator::selfEnd(getNode());
436 return getNode().end();
444 internal_iterator d_iter
;
447 explicit iterator(internal_iterator i
) : d_iter(i
) {}
449 inline Variable
operator*() {
450 return Variable(*d_iter
);
453 bool operator==(const iterator
& i
) {
454 return d_iter
== i
.d_iter
;
457 bool operator!=(const iterator
& i
) {
458 return d_iter
!= i
.d_iter
;
461 iterator
operator++() {
466 iterator
operator++(int) {
467 return iterator(d_iter
++);
471 iterator
begin() const {
472 return iterator(internalBegin());
475 iterator
end() const {
476 return iterator(internalEnd());
479 Variable
getHead() const {
484 VarList(Variable v
) : NodeWrapper(v
.getNode()) {
485 Assert(isSorted(begin(), end()));
488 VarList(const std::vector
<Variable
>& l
) : NodeWrapper(multList(l
)) {
489 Assert(l
.size() >= 2);
490 Assert(isSorted(begin(), end()));
493 static bool isMember(Node n
);
495 bool isNormalForm() const {
499 static VarList
mkEmptyVarList() {
504 /** There are no restrictions on the size of l */
505 static VarList
mkVarList(const std::vector
<Variable
>& l
) {
507 return mkEmptyVarList();
508 } else if(l
.size() == 1) {
509 return VarList((*l
.begin()).getNode());
515 bool empty() const { return getNode().isNull(); }
516 bool singleton() const {
517 return !empty() && getNode().getKind() != kind::MULT
;
524 return getNode().getNumChildren();
527 static VarList
parseVarList(Node n
);
529 VarList
operator*(const VarList
& vl
) const;
531 int cmp(const VarList
& vl
) const;
533 bool operator<(const VarList
& vl
) const { return cmp(vl
) < 0; }
535 bool operator==(const VarList
& vl
) const { return cmp(vl
) == 0; }
537 bool isIntegral() const {
538 for(iterator i
= begin(), e
=end(); i
!= e
; ++i
){
540 if(!var
.isIntegral()){
548 bool isSorted(iterator start
, iterator end
);
550 };/* class VarList */
553 class Monomial
: public NodeWrapper
{
557 Monomial(Node n
, const Constant
& c
, const VarList
& vl
):
558 NodeWrapper(n
), constant(c
), varList(vl
)
560 Assert(!c
.isZero() || vl
.empty() );
561 Assert( c
.isZero() || !vl
.empty() );
563 Assert(!c
.isOne() || !multStructured(n
));
566 static Node
makeMultNode(const Constant
& c
, const VarList
& vl
) {
570 return NodeManager::currentNM()->mkNode(kind::MULT
, c
.getNode(), vl
.getNode());
573 static bool multStructured(Node n
) {
574 return n
.getKind() == kind::MULT
&&
575 n
[0].getKind() == kind::CONST_RATIONAL
&&
576 n
.getNumChildren() == 2;
581 Monomial(const Constant
& c
):
582 NodeWrapper(c
.getNode()), constant(c
), varList(VarList::mkEmptyVarList())
585 Monomial(const VarList
& vl
):
586 NodeWrapper(vl
.getNode()), constant(Constant::mkConstant(1)), varList(vl
)
588 Assert( !varList
.empty() );
591 Monomial(const Constant
& c
, const VarList
& vl
):
592 NodeWrapper(makeMultNode(c
,vl
)), constant(c
), varList(vl
)
594 Assert( !c
.isZero() );
595 Assert( !c
.isOne() );
596 Assert( !varList
.empty() );
598 Assert(multStructured(getNode()));
601 static bool isMember(TNode n
);
603 /** Makes a monomial with no restrictions on c and vl. */
604 static Monomial
mkMonomial(const Constant
& c
, const VarList
& vl
);
606 static Monomial
mkMonomial(const Variable
& v
){
607 return Monomial(VarList(v
));
610 static Monomial
parseMonomial(Node n
);
612 static Monomial
mkZero() {
613 return Monomial(Constant::mkConstant(0));
615 static Monomial
mkOne() {
616 return Monomial(Constant::mkConstant(1));
618 const Constant
& getConstant() const { return constant
; }
619 const VarList
& getVarList() const { return varList
; }
621 bool isConstant() const {
622 return varList
.empty();
625 bool isZero() const {
626 return constant
.isZero();
629 bool coefficientIsOne() const {
630 return constant
.isOne();
633 bool absCoefficientIsOne() const {
634 return coefficientIsOne() || constant
.getValue() == -1;
637 bool constantIsPositive() const {
638 return getConstant().isPositive();
641 Monomial
operator*(const Rational
& q
) const;
642 Monomial
operator*(const Constant
& c
) const;
643 Monomial
operator*(const Monomial
& mono
) const;
645 Monomial
operator-() const{
646 return (*this) * Rational(-1);
650 int cmp(const Monomial
& mono
) const {
651 return getVarList().cmp(mono
.getVarList());
654 bool operator<(const Monomial
& vl
) const {
658 bool operator==(const Monomial
& vl
) const {
662 static bool isSorted(const std::vector
<Monomial
>& m
) {
663 return __gnu_cxx::is_sorted(m
.begin(), m
.end());
666 static bool isStrictlySorted(const std::vector
<Monomial
>& m
) {
667 return isSorted(m
) && std::adjacent_find(m
.begin(),m
.end()) == m
.end();
671 * The variable product
673 bool integralVariables() const {
674 return getVarList().isIntegral();
678 * The coefficient of the monomial is integral.
680 bool integralCoefficient() const {
681 return getConstant().isIntegral();
685 * A Monomial is an "integral" monomial if the constant is integral.
687 bool isIntegral() const {
688 return integralCoefficient() && integralVariables();
692 * Given a sorted list of monomials, this function transforms this
693 * into a strictly sorted list of monomials that does not contain zero.
695 static std::vector
<Monomial
> sumLikeTerms(const std::vector
<Monomial
>& monos
);
697 bool absLessThan(const Monomial
& other
) const{
698 return getConstant().abs() < other
.getConstant().abs();
701 uint32_t coefficientLength() const{
702 return getConstant().length();
706 static void printList(const std::vector
<Monomial
>& list
);
708 };/* class Monomial */
713 class Polynomial
: public NodeWrapper
{
717 Polynomial(TNode n
) : NodeWrapper(n
), d_singleton(Monomial::isMember(n
)) {
718 Assert(isMember(getNode()));
721 static Node
makePlusNode(const std::vector
<Monomial
>& m
) {
722 Assert(m
.size() >= 2);
724 return makeNode(kind::PLUS
, m
.begin(), m
.end());
727 typedef expr::NodeSelfIterator internal_iterator
;
729 internal_iterator
internalBegin() const {
731 return expr::NodeSelfIterator::self(getNode());
733 return getNode().begin();
737 internal_iterator
internalEnd() const {
739 return expr::NodeSelfIterator::selfEnd(getNode());
741 return getNode().end();
745 bool singleton() const { return d_singleton
; }
748 static bool isMember(TNode n
) {
749 if(Monomial::isMember(n
)){
751 }else if(n
.getKind() == kind::PLUS
){
752 Assert(n
.getNumChildren() >= 2);
753 Node::iterator currIter
= n
.begin(), end
= n
.end();
754 Node prev
= *currIter
;
755 if(!Monomial::isMember(prev
)){
759 Monomial mprev
= Monomial::parseMonomial(prev
);
761 for(; currIter
!= end
; ++currIter
){
762 Node curr
= *currIter
;
763 if(!Monomial::isMember(curr
)){
766 Monomial mcurr
= Monomial::parseMonomial(curr
);
767 if(!(mprev
< mcurr
)){
780 internal_iterator d_iter
;
783 explicit iterator(internal_iterator i
) : d_iter(i
) {}
785 inline Monomial
operator*() {
786 return Monomial::parseMonomial(*d_iter
);
789 bool operator==(const iterator
& i
) {
790 return d_iter
== i
.d_iter
;
793 bool operator!=(const iterator
& i
) {
794 return d_iter
!= i
.d_iter
;
797 iterator
operator++() {
802 iterator
operator++(int) {
803 return iterator(d_iter
++);
807 iterator
begin() const { return iterator(internalBegin()); }
808 iterator
end() const { return iterator(internalEnd()); }
810 Polynomial(const Monomial
& m
):
811 NodeWrapper(m
.getNode()), d_singleton(true)
814 Polynomial(const std::vector
<Monomial
>& m
):
815 NodeWrapper(makePlusNode(m
)), d_singleton(false)
817 Assert( m
.size() >= 2);
818 Assert( Monomial::isStrictlySorted(m
) );
821 static Polynomial
mkPolynomial(const Variable
& v
){
822 return Monomial::mkMonomial(v
);
825 static Polynomial
mkPolynomial(const std::vector
<Monomial
>& m
) {
827 return Polynomial(Monomial::mkZero());
828 } else if(m
.size() == 1) {
829 return Polynomial((*m
.begin()));
831 return Polynomial(m
);
835 static Polynomial
parsePolynomial(Node n
) {
836 return Polynomial(n
);
839 static Polynomial
mkZero() {
840 return Polynomial(Monomial::mkZero());
842 static Polynomial
mkOne() {
843 return Polynomial(Monomial::mkOne());
845 bool isZero() const {
846 return singleton() && (getHead().isZero());
849 bool isConstant() const {
850 return singleton() && (getHead().isConstant());
853 bool containsConstant() const {
854 return getHead().isConstant();
857 uint32_t size() const{
861 Assert(getNode().getKind() == kind::PLUS
);
862 return getNode().getNumChildren();
866 Monomial
getHead() const {
870 Polynomial
getTail() const {
871 Assert(! singleton());
873 iterator tailStart
= begin();
875 std::vector
<Monomial
> subrange
;
876 copy_range(tailStart
, end(), subrange
);
877 return mkPolynomial(subrange
);
880 Monomial
minimumVariableMonomial() const;
881 bool variableMonomialAreStrictlyGreater(const Monomial
& m
) const;
883 void printList() const {
884 if(Debug
.isOn("normal-form")){
885 Debug("normal-form") << "start list" << std::endl
;
886 for(iterator i
= begin(), oend
= end(); i
!= oend
; ++i
) {
887 const Monomial
& m
=*i
;
890 Debug("normal-form") << "end list" << std::endl
;
894 /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
895 bool allIntegralVariables() const {
896 for(iterator i
= begin(), e
=end(); i
!=e
; ++i
){
897 if(!(*i
).integralVariables()){
905 * A Polynomial is an "integral" polynomial if all of the monomials are integral
906 * and all of the coefficients are Integral. */
907 bool isIntegral() const {
908 for(iterator i
= begin(), e
=end(); i
!=e
; ++i
){
909 if(!(*i
).isIntegral()){
917 * Selects a minimal monomial in the polynomial by the absolute value of
920 Monomial
selectAbsMinimum() const;
922 /** Returns true if the absolute value of the head coefficient is one. */
923 bool leadingCoefficientIsAbsOne() const;
924 bool leadingCoefficientIsPositive() const;
925 bool denominatorLCMIsOne() const;
926 bool numeratorGCDIsOne() const;
929 * Returns the Least Common Multiple of the denominators of the coefficients
932 Integer
denominatorLCM() const;
935 * Returns the GCD of the numerators of the monomials.
936 * Requires this to be an isIntegral() polynomial.
938 Integer
numeratorGCD() const;
941 * Returns the GCD of the coefficients of the monomials.
942 * Requires this to be an isIntegral() polynomial.
946 Polynomial
exactDivide(const Integer
& z
) const {
947 Assert(isIntegral());
948 Constant invz
= Constant::mkConstant(Rational(1,z
));
949 Polynomial prod
= (*this) * Monomial(invz
);
950 Assert(prod
.isIntegral());
954 Polynomial
operator+(const Polynomial
& vl
) const;
955 Polynomial
operator-(const Polynomial
& vl
) const;
956 Polynomial
operator-() const{
957 return (*this) * Rational(-1);
960 Polynomial
operator*(const Rational
& q
) const;
961 Polynomial
operator*(const Constant
& c
) const;
962 Polynomial
operator*(const Monomial
& mono
) const;
964 Polynomial
operator*(const Polynomial
& poly
) const;
967 * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
968 * The quotient and remainder of p divided by the non-zero integer z is:
969 * q := [(* floor(coeff_i/z) mono_i )]
970 * r := [(* rem(coeff_i/z) mono_i)]
971 * computeQR(p,z) returns the node (+ q r).
973 * q and r are members of the Polynomial class.
975 * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
976 * (+ (+ 2 x (* 4 y)) (+ 1 x))
978 static Node
computeQR(const Polynomial
& p
, const Integer
& z
);
980 /** Returns the coefficient associated with the VarList in the polynomial. */
981 Constant
getCoefficient(const VarList
& vl
) const;
983 uint32_t maxLength() const{
984 iterator i
= begin(), e
=end();
988 uint32_t max
= (*i
).coefficientLength();
991 uint32_t curr
= (*i
).coefficientLength();
1000 uint32_t numMonomials() const {
1001 if( getNode().getKind() == kind::PLUS
){
1002 return getNode().getNumChildren();
1010 const Rational
& asConstant() const{
1011 Assert(isConstant());
1012 return getNode().getConst
<Rational
>();
1013 //return getHead().getConstant().getValue();
1016 bool isVarList() const {
1018 return VarList::isMember(getNode());
1024 VarList
asVarList() const {
1025 Assert(isVarList());
1026 return getHead().getVarList();
1029 friend class SumPair
;
1030 friend class Comparison
;;
1032 };/* class Polynomial */
1036 * SumPair is a utility class that extends polynomials for use in computations.
1037 * A SumPair is always a combination of (+ p c) where
1038 * c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1040 * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1041 * is known to implicitly be equal to 0.
1043 * SumPairs do not have unique representations due to the potential for p = 0.
1044 * This makes them inappropriate for normal forms.
1046 class SumPair
: public NodeWrapper
{
1048 static Node
toNode(const Polynomial
& p
, const Constant
& c
){
1049 return NodeManager::currentNM()->mkNode(kind::PLUS
, p
.getNode(), c
.getNode());
1055 Assert(isNormalForm());
1060 SumPair(const Polynomial
& p
):
1061 NodeWrapper(toNode(p
, Constant::mkConstant(0)))
1063 Assert(isNormalForm());
1066 SumPair(const Polynomial
& p
, const Constant
& c
):
1067 NodeWrapper(toNode(p
, c
))
1069 Assert(isNormalForm());
1072 static bool isMember(TNode n
) {
1073 if(n
.getKind() == kind::PLUS
&& n
.getNumChildren() == 2){
1074 if(Constant::isMember(n
[1])){
1075 if(Polynomial::isMember(n
[0])){
1076 Polynomial p
= Polynomial::parsePolynomial(n
[0]);
1077 return p
.isZero() || (!p
.containsConstant());
1089 bool isNormalForm() const {
1090 return isMember(getNode());
1093 Polynomial
getPolynomial() const {
1094 return Polynomial::parsePolynomial(getNode()[0]);
1097 Constant
getConstant() const {
1098 return Constant::mkConstant((getNode())[1]);
1101 SumPair
operator+(const SumPair
& other
) const {
1102 return SumPair(getPolynomial() + other
.getPolynomial(),
1103 getConstant() + other
.getConstant());
1106 SumPair
operator*(const Constant
& c
) const {
1107 return SumPair(getPolynomial() * c
, getConstant() * c
);
1110 SumPair
operator-(const SumPair
& other
) const {
1111 return (*this) + (other
* Constant::mkConstant(-1));
1114 static SumPair
mkSumPair(const Polynomial
& p
);
1116 static SumPair
mkSumPair(const Variable
& var
){
1117 return SumPair(Polynomial::mkPolynomial(var
));
1120 static SumPair
parseSumPair(TNode n
){
1124 bool isIntegral() const{
1125 return getConstant().isIntegral() && getPolynomial().isIntegral();
1128 bool isConstant() const {
1129 return getPolynomial().isZero();
1132 bool isZero() const {
1133 return getConstant().isZero() && isConstant();
1137 * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1138 * The SumPair must be integral.
1140 Integer
gcd() const {
1141 Assert(isIntegral());
1142 return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1145 uint32_t maxLength() const {
1146 Assert(isIntegral());
1147 return std::max(getPolynomial().maxLength(), getConstant().length());
1150 static SumPair
mkZero() {
1151 return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1154 static Node
computeQR(const SumPair
& sp
, const Integer
& div
);
1156 };/* class SumPair */
1158 /* class OrderedPolynomialPair { */
1160 /* Polynomial d_first; */
1161 /* Polynomial d_second; */
1163 /* OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1168 /* /\** Returns the first part of the pair. *\/ */
1169 /* const Polynomial& getFirst() const { */
1170 /* return d_first; */
1173 /* /\** Returns the second part of the pair. *\/ */
1174 /* const Polynomial& getSecond() const { */
1175 /* return d_second; */
1178 /* OrderedPolynomialPair operator*(const Constant& c) const; */
1179 /* OrderedPolynomialPair operator+(const Polynomial& p) const; */
1181 /* /\** Returns true if both of the polynomials are constant. *\/ */
1182 /* bool isConstant() const; */
1185 /* * Evaluates an isConstant() ordered pair as if */
1186 /* * (k getFirst() getRight()) */
1188 /* bool evaluateConstant(Kind k) const; */
1191 /* * Returns the Least Common Multiple of the monomials */
1192 /* * on the lefthand side and the constant on the right. */
1194 /* Integer denominatorLCM() const; */
1196 /* /\** Constructs a SumPair. *\/ */
1197 /* SumPair toSumPair() const; */
1200 /* OrderedPolynomialPair divideByGCD() const; */
1201 /* OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1204 /* * Returns true if all of the variables are integers, */
1205 /* * and the coefficients are integers. */
1207 /* bool isIntegral() const; */
1209 /* /\** Returns true if all of the variables are integers. *\/ */
1210 /* bool allIntegralVariables() const { */
1211 /* return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1215 class Comparison
: public NodeWrapper
{
1218 static Node
toNode(Kind k
, const Polynomial
& l
, const Constant
& c
);
1219 static Node
toNode(Kind k
, const Polynomial
& l
, const Polynomial
& r
);
1221 Comparison(TNode n
);
1224 * Creates a node in normal form equivalent to (= l 0).
1225 * All variables in l are integral.
1227 static Node
mkIntEquality(const Polynomial
& l
);
1230 * Creates a comparison equivalent to (k l 0).
1231 * k is either GT or GEQ.
1232 * All variables in l are integral.
1234 static Node
mkIntInequality(Kind k
, const Polynomial
& l
);
1237 * Creates a node equivalent to (= l 0).
1238 * It is not the case that all variables in l are integral.
1240 static Node
mkRatEquality(const Polynomial
& l
);
1243 * Creates a comparison equivalent to (k l 0).
1244 * k is either GT or GEQ.
1245 * It is not the case that all variables in l are integral.
1247 static Node
mkRatInequality(Kind k
, const Polynomial
& l
);
1251 Comparison(bool val
) :
1252 NodeWrapper(NodeManager::currentNM()->mkConst(val
))
1256 * Given a literal to TheoryArith return a single kind to
1257 * to indicate its underlying structure.
1258 * The function returns the following in each case:
1259 * - (K left right) -> K where is either EQUAL, GT, or GEQ
1260 * - (CONST_BOOLEAN b) -> CONST_BOOLEAN
1261 * - (NOT (EQUAL left right)) -> DISTINCT
1262 * - (NOT (GT left right)) -> LEQ
1263 * - (NOT (GEQ left right)) -> LT
1264 * If none of these match, it returns UNDEFINED_KIND.
1266 static Kind
comparisonKind(TNode literal
);
1268 Kind
comparisonKind() const { return comparisonKind(getNode()); }
1270 static Comparison
mkComparison(Kind k
, const Polynomial
& l
, const Polynomial
& r
);
1272 /** Returns true if the comparison is a boolean constant. */
1273 bool isBoolean() const;
1276 * Returns true if the comparison is either a boolean term,
1277 * in integer normal form or mixed normal form.
1279 bool isNormalForm() const;
1282 bool isNormalGT() const;
1283 bool isNormalGEQ() const;
1285 bool isNormalLT() const;
1286 bool isNormalLEQ() const;
1288 bool isNormalEquality() const;
1289 bool isNormalDistinct() const;
1290 bool isNormalEqualityOrDisequality() const;
1292 bool allIntegralVariables() const {
1293 return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1295 bool rightIsConstant() const;
1298 Polynomial
getLeft() const;
1299 Polynomial
getRight() const;
1301 /* /\** Normal form check if at least one variable is real. *\/ */
1302 /* bool isMixedCompareNormalForm() const; */
1304 /* /\** Normal form check if at least one variable is real. *\/ */
1305 /* bool isMixedEqualsNormalForm() const; */
1307 /* /\** Normal form check is all variables are integer.*\/ */
1308 /* bool isIntegerCompareNormalForm() const; */
1310 /* /\** Normal form check is all variables are integer.*\/ */
1311 /* bool isIntegerEqualsNormalForm() const; */
1315 * Returns true if all of the variables are integers, the coefficients are integers,
1316 * and the right hand coefficient is an integer.
1318 bool debugIsIntegral() const;
1320 static Comparison
parseNormalForm(TNode n
);
1322 inline static bool isNormalAtom(TNode n
){
1323 Comparison parse
= Comparison::parseNormalForm(n
);
1324 return parse
.isNormalForm();
1327 SumPair
toSumPair() const;
1329 Polynomial
normalizedVariablePart() const;
1330 DeltaRational
normalizedDeltaRational() const;
1332 };/* class Comparison */
1334 }/* CVC4::theory::arith namespace */
1335 }/* CVC4::theory namespace */
1336 }/* CVC4 namespace */
1338 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */