a09437160b2a8122f68346fc96c76b61983d66f3
1 /********************* */
2 /*! \file normal_form.h
4 ** Original author: taking
5 ** Major contributors: none
6 ** Minor contributors (to current version): none
7 ** This file is part of the CVC4 prototype.
8 ** Copyright (c) 2009, 2010 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 "util/rational.h"
27 #include "theory/arith/arith_constants.h"
28 #include "theory/arith/arith_utilities.h"
32 #include <ext/algorithm>
38 /***********************************************/
39 /***************** Normal Form *****************/
40 /***********************************************/
41 /***********************************************/
44 * Section 1: Languages
45 * The normal form for arithmetic nodes is defined by the language
46 * accepted by the following BNFs with some guard conditions.
47 * (The guard conditions are in Section 3 for completeness.)
51 * n.getMetaKind() == metakind::VARIABLE
55 * n.getKind() == kind::CONST_RATIONAL
57 * var_list := variable | (* [variable])
60 * isSorted varOrder [variable]
62 * monomial := constant | var_list | (* constant' var_list')
64 * constant' \not\in {0,1}
66 * polynomial := monomial' | (+ [monomial])
69 * isStrictlySorted monoOrder [monomial]
70 * forall (\x -> x != 0) [monomial]
72 * restricted_cmp := (|><| polynomial constant)
74 * |><| is GEQ, EQ, or EQ
75 * not (exists constantMonomial (monomialList polynomial))
76 * monomialCoefficient (head (monomialList polynomial)) == 1
78 * comparison := TRUE | FALSE | restricted_cmp | (not restricted_cmp)
80 * Normal Form for terms := polynomial
81 * Normal Form for atoms := comparison
85 * Section 2: Helper Classes
86 * The langauges accepted by each of these defintions
87 * roughly corresponds to one of the following helper classes:
95 * Each of the classes obeys the following contracts/design decisions:
96 * -Calling isMember(Node node) on a node returns true iff that node is a
97 * a member of the language. Note: isMember is O(n).
98 * -Calling isNormalForm() on a helper class object returns true iff that
99 * helper class currently represents a normal form object.
100 * -If isNormalForm() is false, then this object must have been made
101 * using a mk*() factory function.
102 * -If isNormalForm() is true, calling getNode() on all of these classes
103 * returns a node that would be accepted by the corresponding language.
104 * And if isNormalForm() is false, returns Node::null().
105 * -Each of the classes is immutable.
106 * -Public facing constuctors have a 1-to-1 correspondence with one of
107 * production rules in the above grammar.
108 * -Public facing constuctors are required to fail in debug mode when the
109 * guards of the production rule are not strictly met.
110 * For example: Monomial(Constant(1),VarList(Variable(x))) must fail.
111 * -When a class has a Class parseClass(Node node) function,
112 * if isMember(node) is true, the function is required to return an instance
113 * of the helper class, instance, s.t. instance.getNode() == node.
114 * And if isMember(node) is false, this throws an assertion failure in debug
115 * mode and has undefined behaviour if not in debug mode.
116 * -Only public facing constructors, parseClass(node), and mk*() functions are
117 * considered privileged functions for the helper class.
118 * -Only privileged functions may use private constructors, and access
119 * private data members.
120 * -All non-privileged functions are considered utility functions and
121 * must use a privileged function in order to create an instance of the class.
125 * Section 3: Guard Conditions Misc.
131 * | (* [variable]) -> len [variable]
135 * Empty -> (0,Node::null())
136 * | NonEmpty(vl) -> (var_list_len vl, vl)
138 * var_listOrder a b = tuple_cmp (order a) (order b)
140 * monomialVarList monomial =
141 * match monomial with
143 * | var_list -> NonEmpty(var_list)
144 * | (* constant' var_list') -> NonEmpty(var_list')
146 * monoOrder m0 m1 = var_listOrder (monomialVarList m0) (monomialVarList m1)
148 * constantMonomial monomial =
149 * match monomial with
151 * | var_list -> false
152 * | (* constant' var_list') -> false
154 * monomialCoefficient monomial =
155 * match monomial with
156 * constant -> constant
157 * | var_list -> Constant(1)
158 * | (* constant' var_list') -> constant'
160 * monomialList polynomial =
161 * match polynomial with
162 * monomial -> monomial::[]
163 * | (+ [monomial]) -> [monomial]
168 * A NodeWrapper is a class that is a thinly veiled container of a Node object.
174 NodeWrapper(Node n
) : node(n
) {}
175 const Node
& getNode() const { return node
; }
176 };/* class NodeWrapper */
179 class Variable
: public NodeWrapper
{
181 Variable(Node n
) : NodeWrapper(n
) {
182 Assert(isMember(getNode()));
185 static bool isMember(Node n
) {
186 return n
.getMetaKind() == kind::metakind::VARIABLE
;
189 bool isNormalForm() { return isMember(getNode()); }
191 bool operator<(const Variable
& v
) const { return getNode() < v
.getNode();}
192 bool operator==(const Variable
& v
) const { return getNode() == v
.getNode();}
194 };/* class Variable */
197 class Constant
: public NodeWrapper
{
199 Constant(Node n
) : NodeWrapper(n
) {
200 Assert(isMember(getNode()));
203 static bool isMember(Node n
) {
204 return n
.getKind() == kind::CONST_RATIONAL
;
207 bool isNormalForm() { return isMember(getNode()); }
209 static Constant
mkConstant(Node n
) {
210 return Constant(coerceToRationalNode(n
));
213 static Constant
mkConstant(const Rational
& rat
) {
214 return Constant(mkRationalNode(rat
));
217 const Rational
& getValue() const {
218 return getNode().getConst
<Rational
>();
221 bool isZero() const { return getValue() == 0; }
222 bool isOne() const { return getValue() == 1; }
224 Constant
operator*(const Constant
& other
) const {
225 return mkConstant(getValue() * other
.getValue());
227 Constant
operator+(const Constant
& other
) const {
228 return mkConstant(getValue() + other
.getValue());
230 Constant
operator-() const {
231 return mkConstant(-getValue());
234 };/* class Constant */
237 template <class GetNodeIterator
>
238 inline Node
makeNode(Kind k
, GetNodeIterator start
, GetNodeIterator end
) {
241 while(start
!= end
) {
242 nb
<< (*start
).getNode();
247 }/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
251 * A VarList is a sorted list of variables representing a product.
252 * If the VarList is empty, it represents an empty product or 1.
253 * If the VarList has size 1, it represents a single variable.
255 * A non-sorted VarList can never be successfully made in debug mode.
261 static Node
multList(const std::vector
<Variable
>& list
) {
262 Assert(list
.size() >= 2);
264 return makeNode(kind::MULT
, list
.begin(), list
.end());
266 static Node
makeTuple(Node n
) {
267 // MGD FOR REVIEW: drop IDENTITY kind ?
268 return NodeManager::currentNM()->mkNode(kind::IDENTITY
, n
);
271 VarList() : backingNode(Node::null()) {}
274 backingNode
= (Variable::isMember(n
)) ? makeTuple(n
) : n
;
276 Assert(isSorted(begin(), end()));
282 Node::iterator d_iter
;
284 explicit iterator(Node::iterator i
) : d_iter(i
) {}
286 inline Variable
operator*() {
287 return Variable(*d_iter
);
290 bool operator==(const iterator
& i
) {
291 return d_iter
== i
.d_iter
;
294 bool operator!=(const iterator
& i
) {
295 return d_iter
!= i
.d_iter
;
298 iterator
operator++() {
303 iterator
operator++(int) {
304 return iterator(d_iter
++);
308 Node
getNode() const {
310 return backingNode
[0];
316 iterator
begin() const {
317 return iterator(backingNode
.begin());
319 iterator
end() const {
320 return iterator(backingNode
.end());
323 VarList(Variable v
) : backingNode(makeTuple(v
.getNode())) {
324 Assert(isSorted(begin(), end()));
326 VarList(const std::vector
<Variable
>& l
) : backingNode(multList(l
)) {
327 Assert(l
.size() >= 2);
328 Assert(isSorted(begin(), end()));
331 static bool isMember(Node n
);
333 bool isNormalForm() const {
337 static VarList
mkEmptyVarList() {
342 /** There are no restrictions on the size of l */
343 static VarList
mkVarList(const std::vector
<Variable
>& l
) {
345 return mkEmptyVarList();
346 } else if(l
.size() == 1) {
347 return VarList((*l
.begin()).getNode());
353 int size() const { return backingNode
.getNumChildren(); }
354 bool empty() const { return size() == 0; }
355 bool singleton() const { return backingNode
.getKind() == kind::IDENTITY
; }
357 static VarList
parseVarList(Node n
);
359 VarList
operator*(const VarList
& vl
) const;
361 int cmp(const VarList
& vl
) const;
363 bool operator<(const VarList
& vl
) const { return cmp(vl
) < 0; }
365 bool operator==(const VarList
& vl
) const { return cmp(vl
) == 0; }
368 bool isSorted(iterator start
, iterator end
);
370 };/* class VarList */
373 class Monomial
: public NodeWrapper
{
377 Monomial(Node n
, const Constant
& c
, const VarList
& vl
):
378 NodeWrapper(n
), constant(c
), varList(vl
)
380 Assert(!c
.isZero() || vl
.empty() );
381 Assert( c
.isZero() || !vl
.empty() );
383 Assert(!c
.isOne() || !multStructured(n
));
386 static Node
makeMultNode(const Constant
& c
, const VarList
& vl
) {
390 return NodeManager::currentNM()->mkNode(kind::MULT
, c
.getNode(), vl
.getNode());
393 static bool multStructured(Node n
) {
394 return n
.getKind() == kind::MULT
&&
395 n
[0].getKind() == kind::CONST_RATIONAL
&&
396 n
.getNumChildren() == 2;
401 Monomial(const Constant
& c
):
402 NodeWrapper(c
.getNode()), constant(c
), varList(VarList::mkEmptyVarList())
405 Monomial(const VarList
& vl
):
406 NodeWrapper(vl
.getNode()), constant(Constant::mkConstant(1)), varList(vl
)
408 Assert( !varList
.empty() );
411 Monomial(const Constant
& c
, const VarList
& vl
):
412 NodeWrapper(makeMultNode(c
,vl
)), constant(c
), varList(vl
)
414 Assert( !c
.isZero() );
415 Assert( !c
.isOne() );
416 Assert( !varList
.empty() );
418 Assert(multStructured(getNode()));
421 /** Makes a monomial with no restrictions on c and vl. */
422 static Monomial
mkMonomial(const Constant
& c
, const VarList
& vl
);
425 static Monomial
parseMonomial(Node n
);
427 static Monomial
mkZero() {
428 return Monomial(Constant::mkConstant(0));
430 static Monomial
mkOne() {
431 return Monomial(Constant::mkConstant(1));
433 const Constant
& getConstant() const { return constant
; }
434 const VarList
& getVarList() const { return varList
; }
436 bool isConstant() const {
437 return varList
.empty();
440 bool isZero() const {
441 return constant
.isZero();
444 bool coefficientIsOne() const {
445 return constant
.isOne();
448 Monomial
operator*(const Monomial
& mono
) const;
451 int cmp(const Monomial
& mono
) const {
452 return getVarList().cmp(mono
.getVarList());
455 bool operator<(const Monomial
& vl
) const {
459 bool operator==(const Monomial
& vl
) const {
463 static bool isSorted(const std::vector
<Monomial
>& m
) {
464 return __gnu_cxx::is_sorted(m
.begin(), m
.end());
467 static bool isStrictlySorted(const std::vector
<Monomial
>& m
) {
468 return isSorted(m
) && std::adjacent_find(m
.begin(),m
.end()) == m
.end();
472 * Given a sorted list of monomials, this function transforms this
473 * into a strictly sorted list of monomials that does not contain zero.
475 static std::vector
<Monomial
> sumLikeTerms(const std::vector
<Monomial
>& monos
);
477 static void printList(const std::vector
<Monomial
>& monos
);
478 };/* class Monomial */
481 class Polynomial
: public NodeWrapper
{
483 // MGD FOR REVIEW: do not create this vector<>!
484 std::vector
<Monomial
> monos
;
486 Polynomial(Node n
, const std::vector
<Monomial
>& m
):
487 NodeWrapper(n
), monos(m
)
489 Assert( !monos
.empty() );
490 Assert( Monomial::isStrictlySorted(monos
) );
493 static Node
makePlusNode(const std::vector
<Monomial
>& m
) {
494 Assert(m
.size() >= 2);
496 return makeNode(kind::PLUS
, m
.begin(), m
.end());
500 typedef std::vector
<Monomial
>::const_iterator iterator
;
502 iterator
begin() const { return monos
.begin(); }
503 iterator
end() const { return monos
.end(); }
505 Polynomial(const Monomial
& m
):
506 NodeWrapper(m
.getNode()), monos()
510 Polynomial(const std::vector
<Monomial
>& m
):
511 NodeWrapper(makePlusNode(m
)), monos(m
)
513 Assert( monos
.size() >= 2);
514 Assert( Monomial::isStrictlySorted(monos
) );
518 static Polynomial
mkPolynomial(const std::vector
<Monomial
>& m
) {
520 return Polynomial(Monomial::mkZero());
521 } else if(m
.size() == 1) {
522 return Polynomial((*m
.begin()));
524 return Polynomial(m
);
528 // MGD FOR REVIEW: make this constant time (for non-debug mode)
529 static Polynomial
parsePolynomial(Node n
) {
530 std::vector
<Monomial
> monos
;
531 if(n
.getKind() == kind::PLUS
) {
532 for(Node::iterator i
=n
.begin(), end
=n
.end(); i
!= end
; ++i
) {
533 monos
.push_back(Monomial::parseMonomial(*i
));
536 monos
.push_back(Monomial::parseMonomial(n
));
538 return Polynomial(n
,monos
);
541 static Polynomial
mkZero() {
542 return Polynomial(Monomial::mkZero());
544 static Polynomial
mkOne() {
545 return Polynomial(Monomial::mkOne());
547 bool isZero() const {
548 return (monos
.size() == 1) && (getHead().isZero());
551 bool isConstant() const {
552 return (monos
.size() == 1) && (getHead().isConstant());
555 bool containsConstant() const {
556 return getHead().isConstant();
559 Monomial
getHead() const {
563 Polynomial
getTail() const {
564 Assert(monos
.size() >= 1);
566 iterator start
= begin()+1;
567 std::vector
<Monomial
> subrange(start
, end());
568 return mkPolynomial(subrange
);
571 void printList() const {
572 Debug("normal-form") << "start list" << std::endl
;
573 Monomial::printList(monos
);
574 Debug("normal-form") << "end list" << std::endl
;
577 Polynomial
operator+(const Polynomial
& vl
) const;
579 Polynomial
operator*(const Monomial
& mono
) const;
581 Polynomial
operator*(const Polynomial
& poly
) const;
583 };/* class Polynomial */
586 class Comparison
: public NodeWrapper
{
592 static Node
toNode(Kind k
, const Polynomial
& l
, const Constant
& r
);
594 Comparison(TNode n
, Kind k
, const Polynomial
& l
, const Constant
& r
):
595 NodeWrapper(n
), oper(k
), left(l
), right(r
)
598 Comparison(bool val
) :
599 NodeWrapper(NodeManager::currentNM()->mkConst(val
)),
600 oper(kind::CONST_BOOLEAN
),
601 left(Polynomial::mkZero()),
602 right(Constant::mkConstant(0))
605 Comparison(Kind k
, const Polynomial
& l
, const Constant
& r
):
606 NodeWrapper(toNode(k
, l
, r
)), oper(k
), left(l
), right(r
)
608 Assert(isRelationOperator(oper
));
609 Assert(!left
.containsConstant());
610 Assert(left
.getHead().getConstant().isOne());
613 static Comparison
mkComparison(Kind k
, const Polynomial
& left
, const Constant
& right
);
615 bool isBoolean() const {
616 return (oper
== kind::CONST_BOOLEAN
);
619 bool isNormalForm() const {
622 } else if(left
.containsConstant()) {
624 } else if(left
.getHead().getConstant().isOne()) {
631 const Polynomial
& getLeft() const { return left
; }
632 const Constant
& getRight() const { return right
; }
634 Comparison
addConstant(const Constant
& constant
) const;
635 Comparison
multiplyConstant(const Constant
& constant
) const;
637 static Comparison
parseNormalForm(TNode n
);
639 };/* class Comparison */
641 }/* CVC4::theory::arith namespace */
642 }/* CVC4::theory namespace */
643 }/* CVC4 namespace */
645 #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */