1 /********************* */
2 /*! \file normal_form.h
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 "cvc4_private.h"
20 #ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H
21 #define __CVC4__THEORY__ARITH__NORMAL_FORM_H
23 #include "expr/node.h"
24 #include "expr/node_self_iterator.h"
25 #include "util/rational.h"
26 #include "theory/arith/delta_rational.h"
27 //#include "theory/arith/arith_utilities.h"
31 #include <ext/algorithm>
37 /***********************************************/
38 /***************** Normal Form *****************/
39 /***********************************************/
40 /***********************************************/
43 * Section 1: Languages
44 * The normal form for arithmetic nodes is defined by the language
45 * accepted by the following BNFs with some guard conditions.
46 * (The guard conditions are in Section 3 for completeness.)
50 * n.isVar() or is foreign
51 * n.getType() \in {Integer, Real}
55 * n.getKind() == kind::CONST_RATIONAL
57 * var_list := variable | (* [variable])
60 * isSorted varOrder [variable]
62 * monomial := constant | var_list | (* constant' var_list')
64 * \f$ constant' \not\in {0,1} \f$
66 * polynomial := monomial' | (+ [monomial])
69 * isStrictlySorted monoOrder [monomial]
70 * forall (\x -> x != 0) [monomial]
72 * rational_cmp := (|><| qpolynomial constant)
75 * not (exists constantMonomial (monomialList qpolynomial))
76 * (exists realMonomial (monomialList qpolynomial))
77 * abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
79 * integer_cmp := (>= zpolynomial constant)
81 * not (exists constantMonomial (monomialList zpolynomial))
82 * (forall integerMonomial (monomialList zpolynomial))
83 * the gcd of all numerators of coefficients is 1
84 * the denominator of all coefficients and the constant is 1
85 * the leading coefficient is positive
87 * rational_eq := (= qvarlist qpolynomial)
89 * let allMonomials = (cons qvarlist (monomialList zpolynomial))
90 * let variableMonomials = (drop constantMonomial allMonomials)
91 * isStrictlySorted variableMonomials
92 * exists realMonomial variableMonomials
93 * is not empty qvarlist
95 * integer_eq := (= zmonomial zpolynomial)
97 * let allMonomials = (cons zmonomial (monomialList zpolynomial))
98 * let variableMonomials = (drop constantMonomial allMonomials)
99 * not (constantMonomial zmonomial)
100 * (forall integerMonomial allMonomials)
101 * isStrictlySorted variableMonomials
102 * the gcd of all numerators of coefficients is 1
103 * the denominator of all coefficients and the constant is 1
104 * the coefficient of monomial is positive
105 * the value of the coefficient of monomial is minimal in variableMonomials
107 * comparison := TRUE | FALSE
108 * | rational_cmp | (not rational_cmp)
109 * | rational_eq | (not rational_eq)
110 * | integer_cmp | (not integer_cmp)
111 * | integer_eq | (not integer_eq)
113 * Normal Form for terms := polynomial
114 * Normal Form for atoms := comparison
118 * Section 2: Helper Classes
119 * The langauges accepted by each of these defintions
120 * roughly corresponds to one of the following helper classes:
128 * Each of the classes obeys the following contracts/design decisions:
129 * -Calling isMember(Node node) on a node returns true iff that node is a
130 * a member of the language. Note: isMember is O(n).
131 * -Calling isNormalForm() on a helper class object returns true iff that
132 * helper class currently represents a normal form object.
133 * -If isNormalForm() is false, then this object must have been made
134 * using a mk*() factory function.
135 * -If isNormalForm() is true, calling getNode() on all of these classes
136 * returns a node that would be accepted by the corresponding language.
137 * And if isNormalForm() is false, returns Node::null().
138 * -Each of the classes is immutable.
139 * -Public facing constuctors have a 1-to-1 correspondence with one of
140 * production rules in the above grammar.
141 * -Public facing constuctors are required to fail in debug mode when the
142 * guards of the production rule are not strictly met.
143 * For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
144 * -When a class has a Class parseClass(Node node) function,
145 * if isMember(node) is true, the function is required to return an instance
146 * of the helper class, instance, s.t. instance.getNode() == node.
147 * And if isMember(node) is false, this throws an assertion failure in debug
148 * mode and has undefined behaviour if not in debug mode.
149 * -Only public facing constructors, parseClass(node), and mk*() functions are
150 * considered privileged functions for the helper class.
151 * -Only privileged functions may use private constructors, and access
152 * private data members.
153 * -All non-privileged functions are considered utility functions and
154 * must use a privileged function in order to create an instance of the class.
158 * Section 3: Guard Conditions Misc.
161 * variable_order x y =
162 * if (meta_kind_variable x) and (meta_kind_variable y)
163 * then node_order x y
164 * else if (meta_kind_variable x)
166 * else if (meta_kind_variable y)
168 * else node_order x y
173 * | (* [variable]) -> len [variable]
177 * Empty -> (0,Node::null())
178 * | NonEmpty(vl) -> (var_list_len vl, vl)
180 * var_listOrder a b = tuple_cmp (order a) (order b)
182 * monomialVarList monomial =
183 * match monomial with
185 * | var_list -> NonEmpty(var_list)
186 * | (* constant' var_list') -> NonEmpty(var_list')
188 * monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
190 * integerMonomial mono =
191 * forall varHasTypeInteger (monomialVarList mono)
193 * realMonomial mono = not (integerMonomial mono)
195 * constantMonomial monomial =
196 * match monomial with
198 * | var_list -> false
199 * | (* constant' var_list') -> false
201 * monomialCoefficient monomial =
202 * match monomial with
203 * constant -> constant
204 * | var_list -> Constant(1)
205 * | (* constant' var_list') -> constant'
207 * monomialList polynomial =
208 * match polynomial with
209 * monomial -> monomial::[]
210 * | (+ [monomial]) -> [monomial]
214 * A NodeWrapper is a class that is a thinly veiled container of a Node object.
220 NodeWrapper(Node n
) : node(n
) {}
221 const Node
& getNode() const { return node
; }
222 };/* class NodeWrapper */
225 class Variable
: public NodeWrapper
{
227 Variable(Node n
) : NodeWrapper(n
) {
228 Assert(isMember(getNode()));
231 // TODO: check if it's a theory leaf also
232 static bool isMember(Node n
) {
233 Kind k
= n
.getKind();
235 case kind::CONST_RATIONAL
:
237 case kind::INTS_DIVISION
:
238 case kind::INTS_MODULUS
:
240 case kind::INTS_DIVISION_TOTAL
:
241 case kind::INTS_MODULUS_TOTAL
:
242 case kind::DIVISION_TOTAL
:
243 return isDivMember(n
);
245 case kind::TO_INTEGER
:
246 // Treat to_int as a variable; it is replaced in early preprocessing
250 return isLeafMember(n
);
254 static bool isLeafMember(Node n
);
255 static bool isDivMember(Node n
);
256 bool isDivLike() const{
257 return isDivMember(getNode());
260 bool isNormalForm() { return isMember(getNode()); }
262 bool isIntegral() const {
263 return getNode().getType().isInteger();
266 bool isMetaKindVariable() const {
267 return getNode().isVar();
270 bool operator<(const Variable
& v
) const {
272 return cmp(this->getNode(), v
.getNode());
274 // bool thisIsVariable = isMetaKindVariable();
275 // bool vIsVariable = v.isMetaKindVariable();
277 // if(thisIsVariable == vIsVariable){
278 // bool thisIsInteger = isIntegral();
279 // bool vIsInteger = v.isIntegral();
280 // if(thisIsInteger == vIsInteger){
281 // return getNode() < v.getNode();
283 // return thisIsInteger && !vIsInteger;
286 // return thisIsVariable && !vIsVariable;
290 struct VariableNodeCmp
{
291 bool operator()(Node n
, Node m
) const {
292 bool nIsVariable
= n
.isVar();
293 bool mIsVariable
= m
.isVar();
295 if(nIsVariable
== mIsVariable
){
296 bool nIsInteger
= n
.getType().isInteger();
297 bool mIsInteger
= m
.getType().isInteger();
298 if(nIsInteger
== mIsInteger
){
301 return nIsInteger
&& !mIsInteger
;
304 return nIsVariable
&& !mIsVariable
;
309 bool operator==(const Variable
& v
) const { return getNode() == v
.getNode();}
311 size_t getComplexity() const;
312 };/* class Variable */
315 class Constant
: public NodeWrapper
{
317 Constant(Node n
) : NodeWrapper(n
) {
318 Assert(isMember(getNode()));
321 static bool isMember(Node n
) {
322 return n
.getKind() == kind::CONST_RATIONAL
;
325 bool isNormalForm() { return isMember(getNode()); }
327 static Constant
mkConstant(Node n
) {
328 Assert(n
.getKind() == kind::CONST_RATIONAL
);
332 static Constant
mkConstant(const Rational
& rat
);
334 static Constant
mkZero() {
335 return mkConstant(Rational(0));
338 static Constant
mkOne() {
339 return mkConstant(Rational(1));
342 const Rational
& getValue() const {
343 return getNode().getConst
<Rational
>();
346 static int absCmp(const Constant
& a
, const Constant
& b
);
347 bool isIntegral() const { return getValue().isIntegral(); }
349 int sgn() const { return getValue().sgn(); }
351 bool isZero() const { return sgn() == 0; }
352 bool isNegative() const { return sgn() < 0; }
353 bool isPositive() const { return sgn() > 0; }
355 bool isOne() const { return getValue() == 1; }
357 Constant
operator*(const Rational
& other
) const {
358 return mkConstant(getValue() * other
);
361 Constant
operator*(const Constant
& other
) const {
362 return mkConstant(getValue() * other
.getValue());
364 Constant
operator+(const Constant
& other
) const {
365 return mkConstant(getValue() + other
.getValue());
367 Constant
operator-() const {
368 return mkConstant(-getValue());
371 Constant
inverse() const{
373 return mkConstant(getValue().inverse());
376 bool operator<(const Constant
& other
) const {
377 return getValue() < other
.getValue();
380 bool operator==(const Constant
& other
) const {
381 //Rely on node uniqueness.
382 return getNode() == other
.getNode();
385 Constant
abs() const {
393 uint32_t length() const{
394 Assert(isIntegral());
395 return getValue().getNumerator().length();
398 size_t getComplexity() const;
400 };/* class Constant */
403 template <class GetNodeIterator
>
404 inline Node
makeNode(Kind k
, GetNodeIterator start
, GetNodeIterator end
) {
407 while(start
!= end
) {
408 nb
<< (*start
).getNode();
413 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
416 template <class GetNodeIterator
, class T
>
417 static void copy_range(GetNodeIterator begin
, GetNodeIterator end
, std::vector
<T
>& result
){
419 result
.push_back(*begin
);
424 template <class GetNodeIterator
, class T
>
425 static void merge_ranges(GetNodeIterator first1
,
426 GetNodeIterator last1
,
427 GetNodeIterator first2
,
428 GetNodeIterator last2
,
429 std::vector
<T
>& result
) {
431 while(first1
!= last1
&& first2
!= last2
){
432 if( (*first1
) < (*first2
) ){
433 result
.push_back(*first1
);
436 result
.push_back(*first2
);
440 copy_range(first1
, last1
, result
);
441 copy_range(first2
, last2
, result
);
444 template <class GetNodeIterator
, class T
, class Cmp
>
445 static void merge_ranges(GetNodeIterator first1
,
446 GetNodeIterator last1
,
447 GetNodeIterator first2
,
448 GetNodeIterator last2
,
449 std::vector
<T
>& result
,
452 while(first1
!= last1
&& first2
!= last2
){
453 if( cmp(*first1
, *first2
) ){
454 result
.push_back(*first1
);
457 result
.push_back(*first2
);
461 copy_range(first1
, last1
, result
);
462 copy_range(first2
, last2
, result
);
466 * A VarList is a sorted list of variables representing a product.
467 * If the VarList is empty, it represents an empty product or 1.
468 * If the VarList has size 1, it represents a single variable.
470 * A non-sorted VarList can never be successfully made in debug mode.
472 class VarList
: public NodeWrapper
{
475 static Node
multList(const std::vector
<Variable
>& list
) {
476 Assert(list
.size() >= 2);
478 return makeNode(kind::MULT
, list
.begin(), list
.end());
481 VarList() : NodeWrapper(Node::null()) {}
485 typedef expr::NodeSelfIterator internal_iterator
;
487 internal_iterator
internalBegin() const {
489 return expr::NodeSelfIterator::self(getNode());
491 return getNode().begin();
495 internal_iterator
internalEnd() const {
497 return expr::NodeSelfIterator::selfEnd(getNode());
499 return getNode().end();
507 internal_iterator d_iter
;
510 explicit iterator(internal_iterator i
) : d_iter(i
) {}
512 inline Variable
operator*() {
513 return Variable(*d_iter
);
516 bool operator==(const iterator
& i
) {
517 return d_iter
== i
.d_iter
;
520 bool operator!=(const iterator
& i
) {
521 return d_iter
!= i
.d_iter
;
524 iterator
operator++() {
529 iterator
operator++(int) {
530 return iterator(d_iter
++);
534 iterator
begin() const {
535 return iterator(internalBegin());
538 iterator
end() const {
539 return iterator(internalEnd());
542 Variable
getHead() const {
547 VarList(Variable v
) : NodeWrapper(v
.getNode()) {
548 Assert(isSorted(begin(), end()));
551 VarList(const std::vector
<Variable
>& l
) : NodeWrapper(multList(l
)) {
552 Assert(l
.size() >= 2);
553 Assert(isSorted(begin(), end()));
556 static bool isMember(Node n
);
558 bool isNormalForm() const {
562 static VarList
mkEmptyVarList() {
567 /** There are no restrictions on the size of l */
568 static VarList
mkVarList(const std::vector
<Variable
>& l
) {
570 return mkEmptyVarList();
571 } else if(l
.size() == 1) {
572 return VarList((*l
.begin()).getNode());
578 bool empty() const { return getNode().isNull(); }
579 bool singleton() const {
580 return !empty() && getNode().getKind() != kind::MULT
;
587 return getNode().getNumChildren();
590 static VarList
parseVarList(Node n
);
592 VarList
operator*(const VarList
& vl
) const;
594 int cmp(const VarList
& vl
) const;
596 bool operator<(const VarList
& vl
) const { return cmp(vl
) < 0; }
598 bool operator==(const VarList
& vl
) const { return cmp(vl
) == 0; }
600 bool isIntegral() const {
601 for(iterator i
= begin(), e
=end(); i
!= e
; ++i
){
603 if(!var
.isIntegral()){
609 size_t getComplexity() const;
612 bool isSorted(iterator start
, iterator end
);
614 };/* class VarList */
617 class Monomial
: public NodeWrapper
{
621 Monomial(Node n
, const Constant
& c
, const VarList
& vl
):
622 NodeWrapper(n
), constant(c
), varList(vl
)
624 Assert(!c
.isZero() || vl
.empty() );
625 Assert( c
.isZero() || !vl
.empty() );
627 Assert(!c
.isOne() || !multStructured(n
));
630 static Node
makeMultNode(const Constant
& c
, const VarList
& vl
) {
634 return NodeManager::currentNM()->mkNode(kind::MULT
, c
.getNode(), vl
.getNode());
637 static bool multStructured(Node n
) {
638 return n
.getKind() == kind::MULT
&&
639 n
[0].getKind() == kind::CONST_RATIONAL
&&
640 n
.getNumChildren() == 2;
645 Monomial(const Constant
& c
):
646 NodeWrapper(c
.getNode()), constant(c
), varList(VarList::mkEmptyVarList())
649 Monomial(const VarList
& vl
):
650 NodeWrapper(vl
.getNode()), constant(Constant::mkConstant(1)), varList(vl
)
652 Assert( !varList
.empty() );
655 Monomial(const Constant
& c
, const VarList
& vl
):
656 NodeWrapper(makeMultNode(c
,vl
)), constant(c
), varList(vl
)
658 Assert( !c
.isZero() );
659 Assert( !c
.isOne() );
660 Assert( !varList
.empty() );
662 Assert(multStructured(getNode()));
665 static bool isMember(TNode n
);
667 /** Makes a monomial with no restrictions on c and vl. */
668 static Monomial
mkMonomial(const Constant
& c
, const VarList
& vl
);
670 static Monomial
mkMonomial(const Variable
& v
){
671 return Monomial(VarList(v
));
674 static Monomial
parseMonomial(Node n
);
676 static Monomial
mkZero() {
677 return Monomial(Constant::mkConstant(0));
679 static Monomial
mkOne() {
680 return Monomial(Constant::mkConstant(1));
682 const Constant
& getConstant() const { return constant
; }
683 const VarList
& getVarList() const { return varList
; }
685 bool isConstant() const {
686 return varList
.empty();
689 bool isZero() const {
690 return constant
.isZero();
693 bool coefficientIsOne() const {
694 return constant
.isOne();
697 bool absCoefficientIsOne() const {
698 return coefficientIsOne() || constant
.getValue() == -1;
701 bool constantIsPositive() const {
702 return getConstant().isPositive();
705 Monomial
operator*(const Rational
& q
) const;
706 Monomial
operator*(const Constant
& c
) const;
707 Monomial
operator*(const Monomial
& mono
) const;
709 Monomial
operator-() const{
710 return (*this) * Rational(-1);
714 int cmp(const Monomial
& mono
) const {
715 return getVarList().cmp(mono
.getVarList());
718 bool operator<(const Monomial
& vl
) const {
722 bool operator==(const Monomial
& vl
) const {
726 static bool isSorted(const std::vector
<Monomial
>& m
) {
727 return __gnu_cxx::is_sorted(m
.begin(), m
.end());
730 static bool isStrictlySorted(const std::vector
<Monomial
>& m
) {
731 return isSorted(m
) && std::adjacent_find(m
.begin(),m
.end()) == m
.end();
734 static void sort(std::vector
<Monomial
>& m
);
735 static void combineAdjacentMonomials(std::vector
<Monomial
>& m
);
738 * The variable product
740 bool integralVariables() const {
741 return getVarList().isIntegral();
745 * The coefficient of the monomial is integral.
747 bool integralCoefficient() const {
748 return getConstant().isIntegral();
752 * A Monomial is an "integral" monomial if the constant is integral.
754 bool isIntegral() const {
755 return integralCoefficient() && integralVariables();
758 /** Returns true if the VarList is a product of at least 2 Variables.*/
759 bool isNonlinear() const {
760 return getVarList().size() >= 2;
764 * Given a sorted list of monomials, this function transforms this
765 * into a strictly sorted list of monomials that does not contain zero.
767 //static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
769 int absCmp(const Monomial
& other
) const{
770 return getConstant().getValue().absCmp(other
.getConstant().getValue());
772 // bool absLessThan(const Monomial& other) const{
773 // return getConstant().abs() < other.getConstant().abs();
776 uint32_t coefficientLength() const{
777 return getConstant().length();
781 static void printList(const std::vector
<Monomial
>& list
);
783 size_t getComplexity() const;
784 };/* class Monomial */
789 class Polynomial
: public NodeWrapper
{
793 Polynomial(TNode n
) : NodeWrapper(n
), d_singleton(Monomial::isMember(n
)) {
794 Assert(isMember(getNode()));
797 static Node
makePlusNode(const std::vector
<Monomial
>& m
) {
798 Assert(m
.size() >= 2);
800 return makeNode(kind::PLUS
, m
.begin(), m
.end());
803 typedef expr::NodeSelfIterator internal_iterator
;
805 internal_iterator
internalBegin() const {
807 return expr::NodeSelfIterator::self(getNode());
809 return getNode().begin();
813 internal_iterator
internalEnd() const {
815 return expr::NodeSelfIterator::selfEnd(getNode());
817 return getNode().end();
821 bool singleton() const { return d_singleton
; }
824 static bool isMember(TNode n
) {
825 if(Monomial::isMember(n
)){
827 }else if(n
.getKind() == kind::PLUS
){
828 Assert(n
.getNumChildren() >= 2);
829 Node::iterator currIter
= n
.begin(), end
= n
.end();
830 Node prev
= *currIter
;
831 if(!Monomial::isMember(prev
)){
835 Monomial mprev
= Monomial::parseMonomial(prev
);
837 for(; currIter
!= end
; ++currIter
){
838 Node curr
= *currIter
;
839 if(!Monomial::isMember(curr
)){
842 Monomial mcurr
= Monomial::parseMonomial(curr
);
843 if(!(mprev
< mcurr
)){
856 internal_iterator d_iter
;
859 explicit iterator(internal_iterator i
) : d_iter(i
) {}
861 inline Monomial
operator*() {
862 return Monomial::parseMonomial(*d_iter
);
865 bool operator==(const iterator
& i
) {
866 return d_iter
== i
.d_iter
;
869 bool operator!=(const iterator
& i
) {
870 return d_iter
!= i
.d_iter
;
873 iterator
operator++() {
878 iterator
operator++(int) {
879 return iterator(d_iter
++);
883 iterator
begin() const { return iterator(internalBegin()); }
884 iterator
end() const { return iterator(internalEnd()); }
886 Polynomial(const Monomial
& m
):
887 NodeWrapper(m
.getNode()), d_singleton(true)
890 Polynomial(const std::vector
<Monomial
>& m
):
891 NodeWrapper(makePlusNode(m
)), d_singleton(false)
893 Assert( m
.size() >= 2);
894 Assert( Monomial::isStrictlySorted(m
) );
897 static Polynomial
mkPolynomial(const Variable
& v
){
898 return Monomial::mkMonomial(v
);
901 static Polynomial
mkPolynomial(const std::vector
<Monomial
>& m
) {
903 return Polynomial(Monomial::mkZero());
904 } else if(m
.size() == 1) {
905 return Polynomial((*m
.begin()));
907 return Polynomial(m
);
911 static Polynomial
parsePolynomial(Node n
) {
912 return Polynomial(n
);
915 static Polynomial
mkZero() {
916 return Polynomial(Monomial::mkZero());
918 static Polynomial
mkOne() {
919 return Polynomial(Monomial::mkOne());
921 bool isZero() const {
922 return singleton() && (getHead().isZero());
925 bool isConstant() const {
926 return singleton() && (getHead().isConstant());
929 bool containsConstant() const {
930 return getHead().isConstant();
933 uint32_t size() const{
937 Assert(getNode().getKind() == kind::PLUS
);
938 return getNode().getNumChildren();
942 Monomial
getHead() const {
946 Polynomial
getTail() const {
947 Assert(! singleton());
949 iterator tailStart
= begin();
951 std::vector
<Monomial
> subrange
;
952 copy_range(tailStart
, end(), subrange
);
953 return mkPolynomial(subrange
);
956 Monomial
minimumVariableMonomial() const;
957 bool variableMonomialAreStrictlyGreater(const Monomial
& m
) const;
959 void printList() const {
960 if(Debug
.isOn("normal-form")){
961 Debug("normal-form") << "start list" << std::endl
;
962 for(iterator i
= begin(), oend
= end(); i
!= oend
; ++i
) {
963 const Monomial
& m
=*i
;
966 Debug("normal-form") << "end list" << std::endl
;
970 /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
971 bool allIntegralVariables() const {
972 for(iterator i
= begin(), e
=end(); i
!=e
; ++i
){
973 if(!(*i
).integralVariables()){
981 * A Polynomial is an "integral" polynomial if all of the monomials are integral
982 * and all of the coefficients are Integral. */
983 bool isIntegral() const {
984 for(iterator i
= begin(), e
=end(); i
!=e
; ++i
){
985 if(!(*i
).isIntegral()){
992 static Polynomial
sumPolynomials(const std::vector
<Polynomial
>& polynomials
);
994 /** Returns true if the polynomial contains a non-linear monomial.*/
995 bool isNonlinear() const;
999 * Selects a minimal monomial in the polynomial by the absolute value of
1002 Monomial
selectAbsMinimum() const;
1004 /** Returns true if the absolute value of the head coefficient is one. */
1005 bool leadingCoefficientIsAbsOne() const;
1006 bool leadingCoefficientIsPositive() const;
1007 bool denominatorLCMIsOne() const;
1008 bool numeratorGCDIsOne() const;
1010 bool signNormalizedReducedSum() const {
1011 return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne();
1015 * Returns the Least Common Multiple of the denominators of the coefficients
1018 Integer
denominatorLCM() const;
1021 * Returns the GCD of the numerators of the monomials.
1022 * Requires this to be an isIntegral() polynomial.
1024 Integer
numeratorGCD() const;
1027 * Returns the GCD of the coefficients of the monomials.
1028 * Requires this to be an isIntegral() polynomial.
1030 Integer
gcd() const;
1032 Polynomial
exactDivide(const Integer
& z
) const {
1033 Assert(isIntegral());
1034 Constant invz
= Constant::mkConstant(Rational(1,z
));
1035 Polynomial prod
= (*this) * Monomial(invz
);
1036 Assert(prod
.isIntegral());
1040 Polynomial
operator+(const Polynomial
& vl
) const;
1041 Polynomial
operator-(const Polynomial
& vl
) const;
1042 Polynomial
operator-() const{
1043 return (*this) * Rational(-1);
1046 Polynomial
operator*(const Rational
& q
) const;
1047 Polynomial
operator*(const Constant
& c
) const;
1048 Polynomial
operator*(const Monomial
& mono
) const;
1050 Polynomial
operator*(const Polynomial
& poly
) const;
1053 * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
1054 * The quotient and remainder of p divided by the non-zero integer z is:
1055 * q := [(* floor(coeff_i/z) mono_i )]
1056 * r := [(* rem(coeff_i/z) mono_i)]
1057 * computeQR(p,z) returns the node (+ q r).
1059 * q and r are members of the Polynomial class.
1061 * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
1062 * (+ (+ 2 x (* 4 y)) (+ 1 x))
1064 static Node
computeQR(const Polynomial
& p
, const Integer
& z
);
1066 /** Returns the coefficient associated with the VarList in the polynomial. */
1067 Constant
getCoefficient(const VarList
& vl
) const;
1069 uint32_t maxLength() const{
1070 iterator i
= begin(), e
=end();
1074 uint32_t max
= (*i
).coefficientLength();
1077 uint32_t curr
= (*i
).coefficientLength();
1086 uint32_t numMonomials() const {
1087 if( getNode().getKind() == kind::PLUS
){
1088 return getNode().getNumChildren();
1096 const Rational
& asConstant() const{
1097 Assert(isConstant());
1098 return getNode().getConst
<Rational
>();
1099 //return getHead().getConstant().getValue();
1102 bool isVarList() const {
1104 return VarList::isMember(getNode());
1110 VarList
asVarList() const {
1111 Assert(isVarList());
1112 return getHead().getVarList();
1115 size_t getComplexity() const;
1117 friend class SumPair
;
1118 friend class Comparison
;
1120 /** Returns a node that if asserted ensures v is the abs of this polynomial.*/
1121 Node
makeAbsCondition(Variable v
){
1122 return makeAbsCondition(v
, *this);
1125 /** Returns a node that if asserted ensures v is the abs of p.*/
1126 static Node
makeAbsCondition(Variable v
, Polynomial p
);
1128 };/* class Polynomial */
1132 * SumPair is a utility class that extends polynomials for use in computations.
1133 * A SumPair is always a combination of (+ p c) where
1134 * c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1136 * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1137 * is known to implicitly be equal to 0.
1139 * SumPairs do not have unique representations due to the potential for p = 0.
1140 * This makes them inappropriate for normal forms.
1142 class SumPair
: public NodeWrapper
{
1144 static Node
toNode(const Polynomial
& p
, const Constant
& c
){
1145 return NodeManager::currentNM()->mkNode(kind::PLUS
, p
.getNode(), c
.getNode());
1151 Assert(isNormalForm());
1156 SumPair(const Polynomial
& p
):
1157 NodeWrapper(toNode(p
, Constant::mkConstant(0)))
1159 Assert(isNormalForm());
1162 SumPair(const Polynomial
& p
, const Constant
& c
):
1163 NodeWrapper(toNode(p
, c
))
1165 Assert(isNormalForm());
1168 static bool isMember(TNode n
) {
1169 if(n
.getKind() == kind::PLUS
&& n
.getNumChildren() == 2){
1170 if(Constant::isMember(n
[1])){
1171 if(Polynomial::isMember(n
[0])){
1172 Polynomial p
= Polynomial::parsePolynomial(n
[0]);
1173 return p
.isZero() || (!p
.containsConstant());
1185 bool isNormalForm() const {
1186 return isMember(getNode());
1189 Polynomial
getPolynomial() const {
1190 return Polynomial::parsePolynomial(getNode()[0]);
1193 Constant
getConstant() const {
1194 return Constant::mkConstant((getNode())[1]);
1197 SumPair
operator+(const SumPair
& other
) const {
1198 return SumPair(getPolynomial() + other
.getPolynomial(),
1199 getConstant() + other
.getConstant());
1202 SumPair
operator*(const Constant
& c
) const {
1203 return SumPair(getPolynomial() * c
, getConstant() * c
);
1206 SumPair
operator-(const SumPair
& other
) const {
1207 return (*this) + (other
* Constant::mkConstant(-1));
1210 static SumPair
mkSumPair(const Polynomial
& p
);
1212 static SumPair
mkSumPair(const Variable
& var
){
1213 return SumPair(Polynomial::mkPolynomial(var
));
1216 static SumPair
parseSumPair(TNode n
){
1220 bool isIntegral() const{
1221 return getConstant().isIntegral() && getPolynomial().isIntegral();
1224 bool isConstant() const {
1225 return getPolynomial().isZero();
1228 bool isZero() const {
1229 return getConstant().isZero() && isConstant();
1232 uint32_t size() const{
1233 return getPolynomial().size();
1236 bool isNonlinear() const{
1237 return getPolynomial().isNonlinear();
1241 * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1242 * The SumPair must be integral.
1244 Integer
gcd() const {
1245 Assert(isIntegral());
1246 return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1249 uint32_t maxLength() const {
1250 Assert(isIntegral());
1251 return std::max(getPolynomial().maxLength(), getConstant().length());
1254 static SumPair
mkZero() {
1255 return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1258 static Node
computeQR(const SumPair
& sp
, const Integer
& div
);
1260 };/* class SumPair */
1262 /* class OrderedPolynomialPair { */
1264 /* Polynomial d_first; */
1265 /* Polynomial d_second; */
1267 /* OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1272 /* /\** Returns the first part of the pair. *\/ */
1273 /* const Polynomial& getFirst() const { */
1274 /* return d_first; */
1277 /* /\** Returns the second part of the pair. *\/ */
1278 /* const Polynomial& getSecond() const { */
1279 /* return d_second; */
1282 /* OrderedPolynomialPair operator*(const Constant& c) const; */
1283 /* OrderedPolynomialPair operator+(const Polynomial& p) const; */
1285 /* /\** Returns true if both of the polynomials are constant. *\/ */
1286 /* bool isConstant() const; */
1289 /* * Evaluates an isConstant() ordered pair as if */
1290 /* * (k getFirst() getRight()) */
1292 /* bool evaluateConstant(Kind k) const; */
1295 /* * Returns the Least Common Multiple of the monomials */
1296 /* * on the lefthand side and the constant on the right. */
1298 /* Integer denominatorLCM() const; */
1300 /* /\** Constructs a SumPair. *\/ */
1301 /* SumPair toSumPair() const; */
1304 /* OrderedPolynomialPair divideByGCD() const; */
1305 /* OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1308 /* * Returns true if all of the variables are integers, */
1309 /* * and the coefficients are integers. */
1311 /* bool isIntegral() const; */
1313 /* /\** Returns true if all of the variables are integers. *\/ */
1314 /* bool allIntegralVariables() const { */
1315 /* return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1319 class Comparison
: public NodeWrapper
{
1322 static Node
toNode(Kind k
, const Polynomial
& l
, const Constant
& c
);
1323 static Node
toNode(Kind k
, const Polynomial
& l
, const Polynomial
& r
);
1325 Comparison(TNode n
);
1328 * Creates a node in normal form equivalent to (= l 0).
1329 * All variables in l are integral.
1331 static Node
mkIntEquality(const Polynomial
& l
);
1334 * Creates a comparison equivalent to (k l 0).
1335 * k is either GT or GEQ.
1336 * All variables in l are integral.
1338 static Node
mkIntInequality(Kind k
, const Polynomial
& l
);
1341 * Creates a node equivalent to (= l 0).
1342 * It is not the case that all variables in l are integral.
1344 static Node
mkRatEquality(const Polynomial
& l
);
1347 * Creates a comparison equivalent to (k l 0).
1348 * k is either GT or GEQ.
1349 * It is not the case that all variables in l are integral.
1351 static Node
mkRatInequality(Kind k
, const Polynomial
& l
);
1355 Comparison(bool val
) :
1356 NodeWrapper(NodeManager::currentNM()->mkConst(val
))
1360 * Given a literal to TheoryArith return a single kind to
1361 * to indicate its underlying structure.
1362 * The function returns the following in each case:
1363 * - (K left right) -> K where is either EQUAL, GT, or GEQ
1364 * - (CONST_BOOLEAN b) -> CONST_BOOLEAN
1365 * - (NOT (EQUAL left right)) -> DISTINCT
1366 * - (NOT (GT left right)) -> LEQ
1367 * - (NOT (GEQ left right)) -> LT
1368 * If none of these match, it returns UNDEFINED_KIND.
1370 static Kind
comparisonKind(TNode literal
);
1372 Kind
comparisonKind() const { return comparisonKind(getNode()); }
1374 static Comparison
mkComparison(Kind k
, const Polynomial
& l
, const Polynomial
& r
);
1376 /** Returns true if the comparison is a boolean constant. */
1377 bool isBoolean() const;
1380 * Returns true if the comparison is either a boolean term,
1381 * in integer normal form or mixed normal form.
1383 bool isNormalForm() const;
1386 bool isNormalGT() const;
1387 bool isNormalGEQ() const;
1389 bool isNormalLT() const;
1390 bool isNormalLEQ() const;
1392 bool isNormalEquality() const;
1393 bool isNormalDistinct() const;
1394 bool isNormalEqualityOrDisequality() const;
1396 bool allIntegralVariables() const {
1397 return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1399 bool rightIsConstant() const;
1402 Polynomial
getLeft() const;
1403 Polynomial
getRight() const;
1405 /* /\** Normal form check if at least one variable is real. *\/ */
1406 /* bool isMixedCompareNormalForm() const; */
1408 /* /\** Normal form check if at least one variable is real. *\/ */
1409 /* bool isMixedEqualsNormalForm() const; */
1411 /* /\** Normal form check is all variables are integer.*\/ */
1412 /* bool isIntegerCompareNormalForm() const; */
1414 /* /\** Normal form check is all variables are integer.*\/ */
1415 /* bool isIntegerEqualsNormalForm() const; */
1419 * Returns true if all of the variables are integers, the coefficients are integers,
1420 * and the right hand coefficient is an integer.
1422 bool debugIsIntegral() const;
1424 static Comparison
parseNormalForm(TNode n
);
1426 inline static bool isNormalAtom(TNode n
){
1427 Comparison parse
= Comparison::parseNormalForm(n
);
1428 return parse
.isNormalForm();
1431 size_t getComplexity() const;
1433 SumPair
toSumPair() const;
1435 Polynomial
normalizedVariablePart() const;
1436 DeltaRational
normalizedDeltaRational() const;
1438 };/* class Comparison */
1440 }/* CVC4::theory::arith namespace */
1441 }/* CVC4::theory namespace */
1442 }/* CVC4 namespace */
1444 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */