1 /********************* */
2 /*! \file normal_form.h
4 ** Top contributors (to current version):
5 ** Tim King, Morgan Deters, Dejan Jovanovic
6 ** This file is part of the CVC4 project.
7 ** Copyright (c) 2009-2016 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
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
26 #if IS_SORTED_IN_GNUCXX_NAMESPACE
27 # include <ext/algorithm>
28 #endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
30 #include "base/output.h"
31 #include "expr/node.h"
32 #include "expr/node_self_iterator.h"
33 #include "theory/arith/delta_rational.h"
34 #include "util/rational.h"
41 /***********************************************/
42 /***************** Normal Form *****************/
43 /***********************************************/
44 /***********************************************/
47 * Section 1: Languages
48 * The normal form for arithmetic nodes is defined by the language
49 * accepted by the following BNFs with some guard conditions.
50 * (The guard conditions are in Section 3 for completeness.)
54 * n.isVar() or is foreign
55 * n.getType() \in {Integer, Real}
59 * n.getKind() == kind::CONST_RATIONAL
61 * var_list := variable | (* [variable])
64 * isSorted varOrder [variable]
66 * monomial := constant | var_list | (* constant' var_list')
68 * \f$ constant' \not\in {0,1} \f$
70 * polynomial := monomial' | (+ [monomial])
73 * isStrictlySorted monoOrder [monomial]
74 * forall (\x -> x != 0) [monomial]
76 * rational_cmp := (|><| qpolynomial constant)
79 * not (exists constantMonomial (monomialList qpolynomial))
80 * (exists realMonomial (monomialList qpolynomial))
81 * abs(monomialCoefficient (head (monomialList qpolynomial))) == 1
83 * integer_cmp := (>= zpolynomial constant)
85 * not (exists constantMonomial (monomialList zpolynomial))
86 * (forall integerMonomial (monomialList zpolynomial))
87 * the gcd of all numerators of coefficients is 1
88 * the denominator of all coefficients and the constant is 1
89 * the leading coefficient is positive
91 * rational_eq := (= qvarlist qpolynomial)
93 * let allMonomials = (cons qvarlist (monomialList zpolynomial))
94 * let variableMonomials = (drop constantMonomial allMonomials)
95 * isStrictlySorted variableMonomials
96 * exists realMonomial variableMonomials
97 * is not empty qvarlist
99 * integer_eq := (= zmonomial zpolynomial)
101 * let allMonomials = (cons zmonomial (monomialList zpolynomial))
102 * let variableMonomials = (drop constantMonomial allMonomials)
103 * not (constantMonomial zmonomial)
104 * (forall integerMonomial allMonomials)
105 * isStrictlySorted variableMonomials
106 * the gcd of all numerators of coefficients is 1
107 * the denominator of all coefficients and the constant is 1
108 * the coefficient of monomial is positive
109 * the value of the coefficient of monomial is minimal in variableMonomials
111 * comparison := TRUE | FALSE
112 * | rational_cmp | (not rational_cmp)
113 * | rational_eq | (not rational_eq)
114 * | integer_cmp | (not integer_cmp)
115 * | integer_eq | (not integer_eq)
117 * Normal Form for terms := polynomial
118 * Normal Form for atoms := comparison
122 * Section 2: Helper Classes
123 * The langauges accepted by each of these defintions
124 * roughly corresponds to one of the following helper classes:
132 * Each of the classes obeys the following contracts/design decisions:
133 * -Calling isMember(Node node) on a node returns true iff that node is a
134 * a member of the language. Note: isMember is O(n).
135 * -Calling isNormalForm() on a helper class object returns true iff that
136 * helper class currently represents a normal form object.
137 * -If isNormalForm() is false, then this object must have been made
138 * using a mk*() factory function.
139 * -If isNormalForm() is true, calling getNode() on all of these classes
140 * returns a node that would be accepted by the corresponding language.
141 * And if isNormalForm() is false, returns Node::null().
142 * -Each of the classes is immutable.
143 * -Public facing constuctors have a 1-to-1 correspondence with one of
144 * production rules in the above grammar.
145 * -Public facing constuctors are required to fail in debug mode when the
146 * guards of the production rule are not strictly met.
147 * For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
148 * -When a class has a Class parseClass(Node node) function,
149 * if isMember(node) is true, the function is required to return an instance
150 * of the helper class, instance, s.t. instance.getNode() == node.
151 * And if isMember(node) is false, this throws an assertion failure in debug
152 * mode and has undefined behaviour if not in debug mode.
153 * -Only public facing constructors, parseClass(node), and mk*() functions are
154 * considered privileged functions for the helper class.
155 * -Only privileged functions may use private constructors, and access
156 * private data members.
157 * -All non-privileged functions are considered utility functions and
158 * must use a privileged function in order to create an instance of the class.
162 * Section 3: Guard Conditions Misc.
165 * variable_order x y =
166 * if (meta_kind_variable x) and (meta_kind_variable y)
167 * then node_order x y
168 * else if (meta_kind_variable x)
170 * else if (meta_kind_variable y)
172 * else node_order x y
177 * | (* [variable]) -> len [variable]
181 * Empty -> (0,Node::null())
182 * | NonEmpty(vl) -> (var_list_len vl, vl)
184 * var_listOrder a b = tuple_cmp (order a) (order b)
186 * monomialVarList monomial =
187 * match monomial with
189 * | var_list -> NonEmpty(var_list)
190 * | (* constant' var_list') -> NonEmpty(var_list')
192 * monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
194 * integerMonomial mono =
195 * forall varHasTypeInteger (monomialVarList mono)
197 * realMonomial mono = not (integerMonomial mono)
199 * constantMonomial monomial =
200 * match monomial with
202 * | var_list -> false
203 * | (* constant' var_list') -> false
205 * monomialCoefficient monomial =
206 * match monomial with
207 * constant -> constant
208 * | var_list -> Constant(1)
209 * | (* constant' var_list') -> constant'
211 * monomialList polynomial =
212 * match polynomial with
213 * monomial -> monomial::[]
214 * | (+ [monomial]) -> [monomial]
218 * A NodeWrapper is a class that is a thinly veiled container of a Node object.
224 NodeWrapper(Node n
) : node(n
) {}
225 const Node
& getNode() const { return node
; }
226 };/* class NodeWrapper */
229 class Variable
: public NodeWrapper
{
231 Variable(Node n
) : NodeWrapper(n
) {
232 Assert(isMember(getNode()));
235 // TODO: check if it's a theory leaf also
236 static bool isMember(Node n
) {
237 Kind k
= n
.getKind();
239 case kind::CONST_RATIONAL
:
241 case kind::INTS_DIVISION
:
242 case kind::INTS_MODULUS
:
244 case kind::INTS_DIVISION_TOTAL
:
245 case kind::INTS_MODULUS_TOTAL
:
246 case kind::DIVISION_TOTAL
:
247 return isDivMember(n
);
249 case kind::TO_INTEGER
:
250 // Treat to_int as a variable; it is replaced in early preprocessing
254 return isLeafMember(n
);
258 static bool isLeafMember(Node n
);
259 static bool isDivMember(Node n
);
260 bool isDivLike() const{
261 return isDivMember(getNode());
264 bool isNormalForm() { return isMember(getNode()); }
266 bool isIntegral() const {
267 return getNode().getType().isInteger();
270 bool isMetaKindVariable() const {
271 return getNode().isVar();
274 bool operator<(const Variable
& v
) const {
276 return cmp(this->getNode(), v
.getNode());
279 struct VariableNodeCmp
{
280 static inline int cmp(Node n
, Node m
) {
281 if ( n
== m
) { return 0; }
283 // this is now slightly off of the old variable order.
285 bool nIsInteger
= n
.getType().isInteger();
286 bool mIsInteger
= m
.getType().isInteger();
288 if(nIsInteger
== mIsInteger
){
289 bool nIsVariable
= n
.isVar();
290 bool mIsVariable
= m
.isVar();
292 if(nIsVariable
== mIsVariable
){
301 return -1; // nIsVariable => !mIsVariable
303 return 1; // !nIsVariable => mIsVariable
307 Assert(nIsInteger
!= mIsInteger
);
309 return 1; // nIsInteger => !mIsInteger
311 return -1; // !nIsInteger => mIsInteger
316 bool operator()(Node n
, Node m
) const {
317 return VariableNodeCmp::cmp(n
,m
) < 0;
321 bool operator==(const Variable
& v
) const { return getNode() == v
.getNode();}
323 size_t getComplexity() const;
324 };/* class Variable */
327 class Constant
: public NodeWrapper
{
329 Constant(Node n
) : NodeWrapper(n
) {
330 Assert(isMember(getNode()));
333 static bool isMember(Node n
) {
334 return n
.getKind() == kind::CONST_RATIONAL
;
337 bool isNormalForm() { return isMember(getNode()); }
339 static Constant
mkConstant(Node n
) {
340 Assert(n
.getKind() == kind::CONST_RATIONAL
);
344 static Constant
mkConstant(const Rational
& rat
);
346 static Constant
mkZero() {
347 return mkConstant(Rational(0));
350 static Constant
mkOne() {
351 return mkConstant(Rational(1));
354 const Rational
& getValue() const {
355 return getNode().getConst
<Rational
>();
358 static int absCmp(const Constant
& a
, const Constant
& b
);
359 bool isIntegral() const { return getValue().isIntegral(); }
361 int sgn() const { return getValue().sgn(); }
363 bool isZero() const { return sgn() == 0; }
364 bool isNegative() const { return sgn() < 0; }
365 bool isPositive() const { return sgn() > 0; }
367 bool isOne() const { return getValue() == 1; }
369 Constant
operator*(const Rational
& other
) const {
370 return mkConstant(getValue() * other
);
373 Constant
operator*(const Constant
& other
) const {
374 return mkConstant(getValue() * other
.getValue());
376 Constant
operator+(const Constant
& other
) const {
377 return mkConstant(getValue() + other
.getValue());
379 Constant
operator-() const {
380 return mkConstant(-getValue());
383 Constant
inverse() const{
385 return mkConstant(getValue().inverse());
388 bool operator<(const Constant
& other
) const {
389 return getValue() < other
.getValue();
392 bool operator==(const Constant
& other
) const {
393 //Rely on node uniqueness.
394 return getNode() == other
.getNode();
397 Constant
abs() const {
405 uint32_t length() const{
406 Assert(isIntegral());
407 return getValue().getNumerator().length();
410 size_t getComplexity() const;
412 };/* class Constant */
415 template <class GetNodeIterator
>
416 inline Node
makeNode(Kind k
, GetNodeIterator start
, GetNodeIterator end
) {
419 while(start
!= end
) {
420 nb
<< (*start
).getNode();
425 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
428 template <class GetNodeIterator
, class T
>
429 static void copy_range(GetNodeIterator begin
, GetNodeIterator end
, std::vector
<T
>& result
){
431 result
.push_back(*begin
);
436 template <class GetNodeIterator
, class T
>
437 static void merge_ranges(GetNodeIterator first1
,
438 GetNodeIterator last1
,
439 GetNodeIterator first2
,
440 GetNodeIterator last2
,
441 std::vector
<T
>& result
) {
443 while(first1
!= last1
&& first2
!= last2
){
444 if( (*first1
) < (*first2
) ){
445 result
.push_back(*first1
);
448 result
.push_back(*first2
);
452 copy_range(first1
, last1
, result
);
453 copy_range(first2
, last2
, result
);
456 template <class GetNodeIterator
, class T
, class Cmp
>
457 static void merge_ranges(GetNodeIterator first1
,
458 GetNodeIterator last1
,
459 GetNodeIterator first2
,
460 GetNodeIterator last2
,
461 std::vector
<T
>& result
,
464 while(first1
!= last1
&& first2
!= last2
){
465 if( cmp(*first1
, *first2
) ){
466 result
.push_back(*first1
);
469 result
.push_back(*first2
);
473 copy_range(first1
, last1
, result
);
474 copy_range(first2
, last2
, result
);
478 * A VarList is a sorted list of variables representing a product.
479 * If the VarList is empty, it represents an empty product or 1.
480 * If the VarList has size 1, it represents a single variable.
482 * A non-sorted VarList can never be successfully made in debug mode.
484 class VarList
: public NodeWrapper
{
487 static Node
multList(const std::vector
<Variable
>& list
) {
488 Assert(list
.size() >= 2);
490 return makeNode(kind::NONLINEAR_MULT
, list
.begin(), list
.end());
493 VarList() : NodeWrapper(Node::null()) {}
497 typedef expr::NodeSelfIterator internal_iterator
;
499 internal_iterator
internalBegin() const {
501 return expr::NodeSelfIterator::self(getNode());
503 return getNode().begin();
507 internal_iterator
internalEnd() const {
509 return expr::NodeSelfIterator::selfEnd(getNode());
511 return getNode().end();
517 class iterator
: public std::iterator
<std::input_iterator_tag
, Variable
> {
519 internal_iterator d_iter
;
522 explicit iterator(internal_iterator i
) : d_iter(i
) {}
524 inline Variable
operator*() {
525 return Variable(*d_iter
);
528 bool operator==(const iterator
& i
) {
529 return d_iter
== i
.d_iter
;
532 bool operator!=(const iterator
& i
) {
533 return d_iter
!= i
.d_iter
;
536 iterator
operator++() {
541 iterator
operator++(int) {
542 return iterator(d_iter
++);
546 iterator
begin() const {
547 return iterator(internalBegin());
550 iterator
end() const {
551 return iterator(internalEnd());
554 Variable
getHead() const {
559 VarList(Variable v
) : NodeWrapper(v
.getNode()) {
560 Assert(isSorted(begin(), end()));
563 VarList(const std::vector
<Variable
>& l
) : NodeWrapper(multList(l
)) {
564 Assert(l
.size() >= 2);
565 Assert(isSorted(begin(), end()));
568 static bool isMember(Node n
);
570 bool isNormalForm() const {
574 static VarList
mkEmptyVarList() {
579 /** There are no restrictions on the size of l */
580 static VarList
mkVarList(const std::vector
<Variable
>& l
) {
582 return mkEmptyVarList();
583 } else if(l
.size() == 1) {
584 return VarList((*l
.begin()).getNode());
590 bool empty() const { return getNode().isNull(); }
591 bool singleton() const {
592 return !empty() && getNode().getKind() != kind::NONLINEAR_MULT
;
599 return getNode().getNumChildren();
602 static VarList
parseVarList(Node n
);
604 VarList
operator*(const VarList
& vl
) const;
606 int cmp(const VarList
& vl
) const;
608 bool operator<(const VarList
& vl
) const { return cmp(vl
) < 0; }
610 bool operator==(const VarList
& vl
) const { return cmp(vl
) == 0; }
612 bool isIntegral() const {
613 for(iterator i
= begin(), e
=end(); i
!= e
; ++i
){
615 if(!var
.isIntegral()){
621 size_t getComplexity() const;
624 bool isSorted(iterator start
, iterator end
);
626 };/* class VarList */
629 /** Constructors have side conditions. Use the static mkMonomial functions instead. */
630 class Monomial
: public NodeWrapper
{
634 Monomial(Node n
, const Constant
& c
, const VarList
& vl
):
635 NodeWrapper(n
), constant(c
), varList(vl
)
637 Assert(!c
.isZero() || vl
.empty() );
638 Assert( c
.isZero() || !vl
.empty() );
640 Assert(!c
.isOne() || !multStructured(n
));
643 static Node
makeMultNode(const Constant
& c
, const VarList
& vl
) {
647 return NodeManager::currentNM()->mkNode(kind::MULT
, c
.getNode(), vl
.getNode());
650 static bool multStructured(Node n
) {
651 return n
.getKind() == kind::MULT
&&
652 n
[0].getKind() == kind::CONST_RATIONAL
&&
653 n
.getNumChildren() == 2;
656 Monomial(const Constant
& c
):
657 NodeWrapper(c
.getNode()), constant(c
), varList(VarList::mkEmptyVarList())
660 Monomial(const VarList
& vl
):
661 NodeWrapper(vl
.getNode()), constant(Constant::mkConstant(1)), varList(vl
)
663 Assert( !varList
.empty() );
666 Monomial(const Constant
& c
, const VarList
& vl
):
667 NodeWrapper(makeMultNode(c
,vl
)), constant(c
), varList(vl
)
669 Assert( !c
.isZero() );
670 Assert( !c
.isOne() );
671 Assert( !varList
.empty() );
673 Assert(multStructured(getNode()));
676 static bool isMember(TNode n
);
678 /** Makes a monomial with no restrictions on c and vl. */
679 static Monomial
mkMonomial(const Constant
& c
, const VarList
& vl
);
681 /** If vl is empty, this make one. */
682 static Monomial
mkMonomial(const VarList
& vl
);
684 static Monomial
mkMonomial(const Constant
& c
){
688 static Monomial
mkMonomial(const Variable
& v
){
689 return Monomial(VarList(v
));
692 static Monomial
parseMonomial(Node n
);
694 static Monomial
mkZero() {
695 return Monomial(Constant::mkConstant(0));
697 static Monomial
mkOne() {
698 return Monomial(Constant::mkConstant(1));
700 const Constant
& getConstant() const { return constant
; }
701 const VarList
& getVarList() const { return varList
; }
703 bool isConstant() const {
704 return varList
.empty();
707 bool isZero() const {
708 return constant
.isZero();
711 bool coefficientIsOne() const {
712 return constant
.isOne();
715 bool absCoefficientIsOne() const {
716 return coefficientIsOne() || constant
.getValue() == -1;
719 bool constantIsPositive() const {
720 return getConstant().isPositive();
723 Monomial
operator*(const Rational
& q
) const;
724 Monomial
operator*(const Constant
& c
) const;
725 Monomial
operator*(const Monomial
& mono
) const;
727 Monomial
operator-() const{
728 return (*this) * Rational(-1);
732 int cmp(const Monomial
& mono
) const {
733 return getVarList().cmp(mono
.getVarList());
736 bool operator<(const Monomial
& vl
) const {
740 bool operator==(const Monomial
& vl
) const {
744 static bool isSorted(const std::vector
<Monomial
>& m
) {
745 #if IS_SORTED_IN_GNUCXX_NAMESPACE
746 return __gnu_cxx::is_sorted(m
.begin(), m
.end());
747 #else /* IS_SORTED_IN_GNUCXX_NAMESPACE */
748 return std::is_sorted(m
.begin(), m
.end());
749 #endif /* IS_SORTED_IN_GNUCXX_NAMESPACE */
752 static bool isStrictlySorted(const std::vector
<Monomial
>& m
) {
753 return isSorted(m
) && std::adjacent_find(m
.begin(),m
.end()) == m
.end();
756 static void sort(std::vector
<Monomial
>& m
);
757 static void combineAdjacentMonomials(std::vector
<Monomial
>& m
);
760 * The variable product
762 bool integralVariables() const {
763 return getVarList().isIntegral();
767 * The coefficient of the monomial is integral.
769 bool integralCoefficient() const {
770 return getConstant().isIntegral();
774 * A Monomial is an "integral" monomial if the constant is integral.
776 bool isIntegral() const {
777 return integralCoefficient() && integralVariables();
780 /** Returns true if the VarList is a product of at least 2 Variables.*/
781 bool isNonlinear() const {
782 return getVarList().size() >= 2;
786 * Given a sorted list of monomials, this function transforms this
787 * into a strictly sorted list of monomials that does not contain zero.
789 //static std::vector<Monomial> sumLikeTerms(const std::vector<Monomial>& monos);
791 int absCmp(const Monomial
& other
) const{
792 return getConstant().getValue().absCmp(other
.getConstant().getValue());
794 // bool absLessThan(const Monomial& other) const{
795 // return getConstant().abs() < other.getConstant().abs();
798 uint32_t coefficientLength() const{
799 return getConstant().length();
803 static void printList(const std::vector
<Monomial
>& list
);
805 size_t getComplexity() const;
806 };/* class Monomial */
811 class Polynomial
: public NodeWrapper
{
815 Polynomial(TNode n
) : NodeWrapper(n
), d_singleton(Monomial::isMember(n
)) {
816 Assert(isMember(getNode()));
819 static Node
makePlusNode(const std::vector
<Monomial
>& m
) {
820 Assert(m
.size() >= 2);
822 return makeNode(kind::PLUS
, m
.begin(), m
.end());
825 typedef expr::NodeSelfIterator internal_iterator
;
827 internal_iterator
internalBegin() const {
829 return expr::NodeSelfIterator::self(getNode());
831 return getNode().begin();
835 internal_iterator
internalEnd() const {
837 return expr::NodeSelfIterator::selfEnd(getNode());
839 return getNode().end();
843 bool singleton() const { return d_singleton
; }
846 static bool isMember(TNode n
);
850 internal_iterator d_iter
;
853 explicit iterator(internal_iterator i
) : d_iter(i
) {}
855 inline Monomial
operator*() {
856 return Monomial::parseMonomial(*d_iter
);
859 bool operator==(const iterator
& i
) {
860 return d_iter
== i
.d_iter
;
863 bool operator!=(const iterator
& i
) {
864 return d_iter
!= i
.d_iter
;
867 iterator
operator++() {
872 iterator
operator++(int) {
873 return iterator(d_iter
++);
877 iterator
begin() const { return iterator(internalBegin()); }
878 iterator
end() const { return iterator(internalEnd()); }
880 Polynomial(const Monomial
& m
):
881 NodeWrapper(m
.getNode()), d_singleton(true)
884 Polynomial(const std::vector
<Monomial
>& m
):
885 NodeWrapper(makePlusNode(m
)), d_singleton(false)
887 Assert( m
.size() >= 2);
888 Assert( Monomial::isStrictlySorted(m
) );
891 static Polynomial
mkPolynomial(const Constant
& c
){
892 return Polynomial(Monomial::mkMonomial(c
));
895 static Polynomial
mkPolynomial(const Variable
& v
){
896 return Polynomial(Monomial::mkMonomial(v
));
899 static Polynomial
mkPolynomial(const std::vector
<Monomial
>& m
) {
901 return Polynomial(Monomial::mkZero());
902 } else if(m
.size() == 1) {
903 return Polynomial((*m
.begin()));
905 return Polynomial(m
);
909 static Polynomial
parsePolynomial(Node n
) {
910 return Polynomial(n
);
913 static Polynomial
mkZero() {
914 return Polynomial(Monomial::mkZero());
916 static Polynomial
mkOne() {
917 return Polynomial(Monomial::mkOne());
919 bool isZero() const {
920 return singleton() && (getHead().isZero());
923 bool isConstant() const {
924 return singleton() && (getHead().isConstant());
927 bool containsConstant() const {
928 return getHead().isConstant();
931 uint32_t size() const{
935 Assert(getNode().getKind() == kind::PLUS
);
936 return getNode().getNumChildren();
940 Monomial
getHead() const {
944 Polynomial
getTail() const {
945 Assert(! singleton());
947 iterator tailStart
= begin();
949 std::vector
<Monomial
> subrange
;
950 copy_range(tailStart
, end(), subrange
);
951 return mkPolynomial(subrange
);
954 Monomial
minimumVariableMonomial() const;
955 bool variableMonomialAreStrictlyGreater(const Monomial
& m
) const;
957 void printList() const {
958 if(Debug
.isOn("normal-form")){
959 Debug("normal-form") << "start list" << std::endl
;
960 for(iterator i
= begin(), oend
= end(); i
!= oend
; ++i
) {
961 const Monomial
& m
=*i
;
964 Debug("normal-form") << "end list" << std::endl
;
968 /** A Polynomial is an "integral" polynomial if all of the monomials are integral. */
969 bool allIntegralVariables() const {
970 for(iterator i
= begin(), e
=end(); i
!=e
; ++i
){
971 if(!(*i
).integralVariables()){
979 * A Polynomial is an "integral" polynomial if all of the monomials are integral
980 * and all of the coefficients are Integral. */
981 bool isIntegral() const {
982 for(iterator i
= begin(), e
=end(); i
!=e
; ++i
){
983 if(!(*i
).isIntegral()){
990 static Polynomial
sumPolynomials(const std::vector
<Polynomial
>& polynomials
);
992 /** Returns true if the polynomial contains a non-linear monomial.*/
993 bool isNonlinear() const;
997 * Selects a minimal monomial in the polynomial by the absolute value of
1000 Monomial
selectAbsMinimum() const;
1002 /** Returns true if the absolute value of the head coefficient is one. */
1003 bool leadingCoefficientIsAbsOne() const;
1004 bool leadingCoefficientIsPositive() const;
1005 bool denominatorLCMIsOne() const;
1006 bool numeratorGCDIsOne() const;
1008 bool signNormalizedReducedSum() const {
1009 return leadingCoefficientIsPositive() && denominatorLCMIsOne() && numeratorGCDIsOne();
1013 * Returns the Least Common Multiple of the denominators of the coefficients
1016 Integer
denominatorLCM() const;
1019 * Returns the GCD of the numerators of the monomials.
1020 * Requires this to be an isIntegral() polynomial.
1022 Integer
numeratorGCD() const;
1025 * Returns the GCD of the coefficients of the monomials.
1026 * Requires this to be an isIntegral() polynomial.
1028 Integer
gcd() const;
1030 /** z must divide all of the coefficients of the polynomial. */
1031 Polynomial
exactDivide(const Integer
& z
) const;
1033 Polynomial
operator+(const Polynomial
& vl
) const;
1034 Polynomial
operator-(const Polynomial
& vl
) const;
1035 Polynomial
operator-() const{
1036 return (*this) * Rational(-1);
1039 Polynomial
operator*(const Rational
& q
) const;
1040 Polynomial
operator*(const Constant
& c
) const;
1041 Polynomial
operator*(const Monomial
& mono
) const;
1043 Polynomial
operator*(const Polynomial
& poly
) const;
1046 * Viewing the integer polynomial as a list [(* coeff_i mono_i)]
1047 * The quotient and remainder of p divided by the non-zero integer z is:
1048 * q := [(* floor(coeff_i/z) mono_i )]
1049 * r := [(* rem(coeff_i/z) mono_i)]
1050 * computeQR(p,z) returns the node (+ q r).
1052 * q and r are members of the Polynomial class.
1054 * computeQR( p = (+ 5 (* 3 x) (* 8 y)) , z = 2) returns
1055 * (+ (+ 2 x (* 4 y)) (+ 1 x))
1057 static Node
computeQR(const Polynomial
& p
, const Integer
& z
);
1059 /** Returns the coefficient associated with the VarList in the polynomial. */
1060 Constant
getCoefficient(const VarList
& vl
) const;
1062 uint32_t maxLength() const{
1063 iterator i
= begin(), e
=end();
1067 uint32_t max
= (*i
).coefficientLength();
1070 uint32_t curr
= (*i
).coefficientLength();
1079 uint32_t numMonomials() const {
1080 if( getNode().getKind() == kind::PLUS
){
1081 return getNode().getNumChildren();
1089 const Rational
& asConstant() const{
1090 Assert(isConstant());
1091 return getNode().getConst
<Rational
>();
1092 //return getHead().getConstant().getValue();
1095 bool isVarList() const {
1097 return VarList::isMember(getNode());
1103 VarList
asVarList() const {
1104 Assert(isVarList());
1105 return getHead().getVarList();
1108 size_t getComplexity() const;
1110 friend class SumPair
;
1111 friend class Comparison
;
1113 /** Returns a node that if asserted ensures v is the abs of this polynomial.*/
1114 Node
makeAbsCondition(Variable v
){
1115 return makeAbsCondition(v
, *this);
1118 /** Returns a node that if asserted ensures v is the abs of p.*/
1119 static Node
makeAbsCondition(Variable v
, Polynomial p
);
1121 };/* class Polynomial */
1125 * SumPair is a utility class that extends polynomials for use in computations.
1126 * A SumPair is always a combination of (+ p c) where
1127 * c is a constant and p is a polynomial such that p = 0 or !p.containsConstant().
1129 * These are a useful utility for representing the equation p = c as (+ p -c) where the pair
1130 * is known to implicitly be equal to 0.
1132 * SumPairs do not have unique representations due to the potential for p = 0.
1133 * This makes them inappropriate for normal forms.
1135 class SumPair
: public NodeWrapper
{
1137 static Node
toNode(const Polynomial
& p
, const Constant
& c
){
1138 return NodeManager::currentNM()->mkNode(kind::PLUS
, p
.getNode(), c
.getNode());
1144 Assert(isNormalForm());
1149 SumPair(const Polynomial
& p
):
1150 NodeWrapper(toNode(p
, Constant::mkConstant(0)))
1152 Assert(isNormalForm());
1155 SumPair(const Polynomial
& p
, const Constant
& c
):
1156 NodeWrapper(toNode(p
, c
))
1158 Assert(isNormalForm());
1161 static bool isMember(TNode n
) {
1162 if(n
.getKind() == kind::PLUS
&& n
.getNumChildren() == 2){
1163 if(Constant::isMember(n
[1])){
1164 if(Polynomial::isMember(n
[0])){
1165 Polynomial p
= Polynomial::parsePolynomial(n
[0]);
1166 return p
.isZero() || (!p
.containsConstant());
1178 bool isNormalForm() const {
1179 return isMember(getNode());
1182 Polynomial
getPolynomial() const {
1183 return Polynomial::parsePolynomial(getNode()[0]);
1186 Constant
getConstant() const {
1187 return Constant::mkConstant((getNode())[1]);
1190 SumPair
operator+(const SumPair
& other
) const {
1191 return SumPair(getPolynomial() + other
.getPolynomial(),
1192 getConstant() + other
.getConstant());
1195 SumPair
operator*(const Constant
& c
) const {
1196 return SumPair(getPolynomial() * c
, getConstant() * c
);
1199 SumPair
operator-(const SumPair
& other
) const {
1200 return (*this) + (other
* Constant::mkConstant(-1));
1203 static SumPair
mkSumPair(const Polynomial
& p
);
1205 static SumPair
mkSumPair(const Variable
& var
){
1206 return SumPair(Polynomial::mkPolynomial(var
));
1209 static SumPair
parseSumPair(TNode n
){
1213 bool isIntegral() const{
1214 return getConstant().isIntegral() && getPolynomial().isIntegral();
1217 bool isConstant() const {
1218 return getPolynomial().isZero();
1221 bool isZero() const {
1222 return getConstant().isZero() && isConstant();
1225 uint32_t size() const{
1226 return getPolynomial().size();
1229 bool isNonlinear() const{
1230 return getPolynomial().isNonlinear();
1234 * Returns the greatest common divisor of gcd(getPolynomial()) and getConstant().
1235 * The SumPair must be integral.
1237 Integer
gcd() const {
1238 Assert(isIntegral());
1239 return (getPolynomial().gcd()).gcd(getConstant().getValue().getNumerator());
1242 uint32_t maxLength() const {
1243 Assert(isIntegral());
1244 return std::max(getPolynomial().maxLength(), getConstant().length());
1247 static SumPair
mkZero() {
1248 return SumPair(Polynomial::mkZero(), Constant::mkConstant(0));
1251 static Node
computeQR(const SumPair
& sp
, const Integer
& div
);
1253 };/* class SumPair */
1255 /* class OrderedPolynomialPair { */
1257 /* Polynomial d_first; */
1258 /* Polynomial d_second; */
1260 /* OrderedPolynomialPair(const Polynomial& f, const Polynomial& s) */
1265 /* /\** Returns the first part of the pair. *\/ */
1266 /* const Polynomial& getFirst() const { */
1267 /* return d_first; */
1270 /* /\** Returns the second part of the pair. *\/ */
1271 /* const Polynomial& getSecond() const { */
1272 /* return d_second; */
1275 /* OrderedPolynomialPair operator*(const Constant& c) const; */
1276 /* OrderedPolynomialPair operator+(const Polynomial& p) const; */
1278 /* /\** Returns true if both of the polynomials are constant. *\/ */
1279 /* bool isConstant() const; */
1282 /* * Evaluates an isConstant() ordered pair as if */
1283 /* * (k getFirst() getRight()) */
1285 /* bool evaluateConstant(Kind k) const; */
1288 /* * Returns the Least Common Multiple of the monomials */
1289 /* * on the lefthand side and the constant on the right. */
1291 /* Integer denominatorLCM() const; */
1293 /* /\** Constructs a SumPair. *\/ */
1294 /* SumPair toSumPair() const; */
1297 /* OrderedPolynomialPair divideByGCD() const; */
1298 /* OrderedPolynomialPair multiplyConstant(const Constant& c) const; */
1301 /* * Returns true if all of the variables are integers, */
1302 /* * and the coefficients are integers. */
1304 /* bool isIntegral() const; */
1306 /* /\** Returns true if all of the variables are integers. *\/ */
1307 /* bool allIntegralVariables() const { */
1308 /* return getFirst().allIntegralVariables() && getSecond().allIntegralVariables(); */
1312 class Comparison
: public NodeWrapper
{
1315 static Node
toNode(Kind k
, const Polynomial
& l
, const Constant
& c
);
1316 static Node
toNode(Kind k
, const Polynomial
& l
, const Polynomial
& r
);
1318 Comparison(TNode n
);
1321 * Creates a node in normal form equivalent to (= l 0).
1322 * All variables in l are integral.
1324 static Node
mkIntEquality(const Polynomial
& l
);
1327 * Creates a comparison equivalent to (k l 0).
1328 * k is either GT or GEQ.
1329 * All variables in l are integral.
1331 static Node
mkIntInequality(Kind k
, const Polynomial
& l
);
1334 * Creates a node equivalent to (= l 0).
1335 * It is not the case that all variables in l are integral.
1337 static Node
mkRatEquality(const Polynomial
& l
);
1340 * Creates a comparison equivalent to (k l 0).
1341 * k is either GT or GEQ.
1342 * It is not the case that all variables in l are integral.
1344 static Node
mkRatInequality(Kind k
, const Polynomial
& l
);
1348 Comparison(bool val
) :
1349 NodeWrapper(NodeManager::currentNM()->mkConst(val
))
1353 * Given a literal to TheoryArith return a single kind to
1354 * to indicate its underlying structure.
1355 * The function returns the following in each case:
1356 * - (K left right) -> K where is either EQUAL, GT, or GEQ
1357 * - (CONST_BOOLEAN b) -> CONST_BOOLEAN
1358 * - (NOT (EQUAL left right)) -> DISTINCT
1359 * - (NOT (GT left right)) -> LEQ
1360 * - (NOT (GEQ left right)) -> LT
1361 * If none of these match, it returns UNDEFINED_KIND.
1363 static Kind
comparisonKind(TNode literal
);
1365 Kind
comparisonKind() const { return comparisonKind(getNode()); }
1367 static Comparison
mkComparison(Kind k
, const Polynomial
& l
, const Polynomial
& r
);
1369 /** Returns true if the comparison is a boolean constant. */
1370 bool isBoolean() const;
1373 * Returns true if the comparison is either a boolean term,
1374 * in integer normal form or mixed normal form.
1376 bool isNormalForm() const;
1379 bool isNormalGT() const;
1380 bool isNormalGEQ() const;
1382 bool isNormalLT() const;
1383 bool isNormalLEQ() const;
1385 bool isNormalEquality() const;
1386 bool isNormalDistinct() const;
1387 bool isNormalEqualityOrDisequality() const;
1389 bool allIntegralVariables() const {
1390 return getLeft().allIntegralVariables() && getRight().allIntegralVariables();
1392 bool rightIsConstant() const;
1395 Polynomial
getLeft() const;
1396 Polynomial
getRight() const;
1398 /* /\** Normal form check if at least one variable is real. *\/ */
1399 /* bool isMixedCompareNormalForm() const; */
1401 /* /\** Normal form check if at least one variable is real. *\/ */
1402 /* bool isMixedEqualsNormalForm() const; */
1404 /* /\** Normal form check is all variables are integer.*\/ */
1405 /* bool isIntegerCompareNormalForm() const; */
1407 /* /\** Normal form check is all variables are integer.*\/ */
1408 /* bool isIntegerEqualsNormalForm() const; */
1412 * Returns true if all of the variables are integers, the coefficients are integers,
1413 * and the right hand coefficient is an integer.
1415 bool debugIsIntegral() const;
1417 static Comparison
parseNormalForm(TNode n
);
1419 inline static bool isNormalAtom(TNode n
){
1420 Comparison parse
= Comparison::parseNormalForm(n
);
1421 return parse
.isNormalForm();
1424 size_t getComplexity() const;
1426 SumPair
toSumPair() const;
1428 Polynomial
normalizedVariablePart() const;
1429 DeltaRational
normalizedDeltaRational() const;
1431 };/* class Comparison */
1433 }/* CVC4::theory::arith namespace */
1434 }/* CVC4::theory namespace */
1435 }/* CVC4 namespace */
1437 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */