From 9dbc683d057288a23109075d806a5398252eaa12 Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Tue, 21 Sep 2010 21:50:26 +0000 Subject: part of review (bug #197): coding conventions, file-level documentation, re-ran update-copyright.pl, etc. --- src/theory/arith/arith_activity.h | 3 +- src/theory/arith/arith_constants.h | 6 +- src/theory/arith/arith_propagator.cpp | 2 +- src/theory/arith/arith_propagator.h | 4 +- src/theory/arith/arith_utilities.h | 6 +- src/theory/arith/next_arith_rewriter.cpp | 2 +- src/theory/arith/next_arith_rewriter.h | 2 +- src/theory/arith/normal_form.cpp | 122 ++++++++------- src/theory/arith/normal_form.h | 231 ++++++++++++++++------------- src/theory/arith/ordered_bounds_list.h | 2 +- src/theory/arith/tableau.h | 2 +- src/theory/arith/theory_arith.cpp | 2 +- src/theory/arith/theory_arith.h | 2 +- src/theory/arith/theory_arith_type_rules.h | 2 +- 14 files changed, 219 insertions(+), 169 deletions(-) diff --git a/src/theory/arith/arith_activity.h b/src/theory/arith/arith_activity.h index f347105e3..f336237a4 100644 --- a/src/theory/arith/arith_activity.h +++ b/src/theory/arith/arith_activity.h @@ -2,7 +2,7 @@ /*! \file arith_activity.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) @@ -17,7 +17,6 @@ ** \todo document this file **/ - #include "cvc4_private.h" #ifndef __CVC4__THEORY__ARITH__ARITH_ACTIVITY_H diff --git a/src/theory/arith/arith_constants.h b/src/theory/arith/arith_constants.h index 4a8fec56f..27abd8873 100644 --- a/src/theory/arith/arith_constants.h +++ b/src/theory/arith/arith_constants.h @@ -17,16 +17,16 @@ ** \todo document this file **/ +#include "cvc4_private.h" +#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H +#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H #include "expr/node.h" #include "expr/node_manager.h" #include "util/rational.h" #include "theory/arith/delta_rational.h" -#ifndef __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H -#define __CVC4__THEORY__ARITH__ARITH_CONSTANTS_H - namespace CVC4 { namespace theory { namespace arith { diff --git a/src/theory/arith/arith_propagator.cpp b/src/theory/arith/arith_propagator.cpp index 0f417bc41..bf14e882e 100644 --- a/src/theory/arith/arith_propagator.cpp +++ b/src/theory/arith/arith_propagator.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/arith_propagator.h b/src/theory/arith/arith_propagator.h index 7ffcec747..8ea628f25 100644 --- a/src/theory/arith/arith_propagator.h +++ b/src/theory/arith/arith_propagator.h @@ -2,7 +2,7 @@ /*! \file arith_propagator.h ** \verbatim ** Original author: taking - ** Major contributors: none + ** Major contributors: mdeters ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) @@ -17,8 +17,6 @@ ** \todo document this file **/ - - #include "cvc4_private.h" #ifndef __CVC4__THEORY__ARITH__ARITH_PROPAGATOR_H diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h index 6706ad76a..d2c07900d 100644 --- a/src/theory/arith/arith_utilities.h +++ b/src/theory/arith/arith_utilities.h @@ -2,8 +2,8 @@ /*! \file arith_utilities.h ** \verbatim ** Original author: taking - ** Major contributors: mdeters - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences @@ -17,6 +17,8 @@ ** \todo document this file **/ +#include "cvc4_private.h" + #ifndef __CVC4__THEORY__ARITH__ARITH_UTILITIES_H #define __CVC4__THEORY__ARITH__ARITH_UTILITIES_H diff --git a/src/theory/arith/next_arith_rewriter.cpp b/src/theory/arith/next_arith_rewriter.cpp index c14f806c9..29fae233b 100644 --- a/src/theory/arith/next_arith_rewriter.cpp +++ b/src/theory/arith/next_arith_rewriter.cpp @@ -1,5 +1,5 @@ /********************* */ -/*! \file arith_rewriter.cpp +/*! \file next_arith_rewriter.cpp ** \verbatim ** Original author: taking ** Major contributors: none diff --git a/src/theory/arith/next_arith_rewriter.h b/src/theory/arith/next_arith_rewriter.h index 7f1ec0fbd..1fb743f71 100644 --- a/src/theory/arith/next_arith_rewriter.h +++ b/src/theory/arith/next_arith_rewriter.h @@ -1,5 +1,5 @@ /********************* */ -/*! \file arith_rewriter.h +/*! \file next_arith_rewriter.h ** \verbatim ** Original author: taking ** Major contributors: mdeters diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp index 6e476bb7f..7baacd4f5 100644 --- a/src/theory/arith/normal_form.cpp +++ b/src/theory/arith/normal_form.cpp @@ -1,3 +1,21 @@ +/********************* */ +/*! \file normal_form.cpp + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ #include "theory/arith/normal_form.h" #include @@ -7,57 +25,57 @@ using namespace CVC4; using namespace CVC4::theory; using namespace CVC4::theory::arith; -bool VarList::isSorted(iterator start, iterator end){ +bool VarList::isSorted(iterator start, iterator end) { return __gnu_cxx::is_sorted(start, end); } -bool VarList::isMember(Node n){ - if(n.getNumChildren() == 0){ +bool VarList::isMember(Node n) { + if(n.getNumChildren() == 0) { return Variable::isMember(n); - }else if(n.getKind() == kind::MULT){ + } else if(n.getKind() == kind::MULT) { Node::iterator curr = n.begin(), end = n.end(); Node prev = *curr; if(!Variable::isMember(prev)) return false; - while( (++curr) != end){ + while( (++curr) != end) { if(!Variable::isMember(*curr)) return false; if(!(prev <= *curr)) return false; prev = *curr; } return true; - }else{ + } else { return false; } } -int VarList::cmp(const VarList& vl) const{ +int VarList::cmp(const VarList& vl) const { int dif = this->size() - vl.size(); - if (dif == 0){ + if (dif == 0) { return this->getNode().getId() - vl.getNode().getId(); - }else if(dif < 0){ + } else if(dif < 0) { return -1; - }else{ + } else { return 1; } } -VarList VarList::parseVarList(Node n){ - if(n.getNumChildren() == 0){ +VarList VarList::parseVarList(Node n) { + if(n.getNumChildren() == 0) { return VarList(Variable(n)); - }else{ + } else { Assert(n.getKind() == kind::MULT); - for(Node::iterator i=n.begin(), end = n.end(); i!=end; ++i){ + for(Node::iterator i=n.begin(), end = n.end(); i!=end; ++i) { Assert(Variable::isMember(*i)); } return VarList(n); } } -VarList VarList::operator*(const VarList& vl) const{ - if(this->empty()){ +VarList VarList::operator*(const VarList& vl) const { + if(this->empty()) { return vl; - }else if(vl.empty()){ + } else if(vl.empty()) { return *this; - }else{ + } else { vector result; back_insert_iterator< vector > bii(result); @@ -74,21 +92,21 @@ VarList VarList::operator*(const VarList& vl) const{ } } -Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl){ - if(c.isZero() || vl.empty() ){ +Monomial Monomial::mkMonomial(const Constant& c, const VarList& vl) { + if(c.isZero() || vl.empty() ) { return Monomial(c); - }else if(c.isOne()){ + } else if(c.isOne()) { return Monomial(vl); - }else{ + } else { return Monomial(c, vl); } } -Monomial Monomial::parseMonomial(Node n){ - if(n.getKind() == kind::CONST_RATIONAL){ +Monomial Monomial::parseMonomial(Node n) { + if(n.getKind() == kind::CONST_RATIONAL) { return Monomial(Constant(n)); - }else if(multStructured(n)){ + } else if(multStructured(n)) { return Monomial::mkMonomial(Constant(n[0]),VarList::parseVarList(n[1])); - }else{ + } else { return Monomial(VarList::parseVarList(n)); } } @@ -100,22 +118,22 @@ Monomial Monomial::operator*(const Monomial& mono) const { return Monomial::mkMonomial(newConstant, newVL); } -vector Monomial::sumLikeTerms(const vector & monos){ +vector Monomial::sumLikeTerms(const vector & monos) { Assert(isSorted(monos)); Debug("blah") << "start sumLikeTerms" << std::endl; printList(monos); vector outMonomials; typedef vector::const_iterator iterator; - for(iterator rangeIter = monos.begin(), end=monos.end(); rangeIter != end;){ + for(iterator rangeIter = monos.begin(), end=monos.end(); rangeIter != end;) { Rational constant = (*rangeIter).getConstant().getValue(); VarList varList = (*rangeIter).getVarList(); ++rangeIter; - while(rangeIter != end && varList == (*rangeIter).getVarList()){ + while(rangeIter != end && varList == (*rangeIter).getVarList()) { constant += (*rangeIter).getConstant().getValue(); ++rangeIter; } - if(constant != 0){ + if(constant != 0) { Constant asConstant = Constant::mkConstant(constant); Monomial nonZero = Monomial::mkMonomial(asConstant, varList); outMonomials.push_back(nonZero); @@ -129,14 +147,14 @@ vector Monomial::sumLikeTerms(const vector & monos){ return outMonomials; } -void Monomial::printList(const std::vector& monos){ +void Monomial::printList(const std::vector& monos) { typedef std::vector::const_iterator iterator; - for(iterator i = monos.begin(), end = monos.end(); i != end; ++i){ + for(iterator i = monos.begin(), end = monos.end(); i != end; ++i) { Debug("blah") << ((*i).getNode()) << std::endl; } } -Polynomial Polynomial::operator+(const Polynomial& vl) const{ +Polynomial Polynomial::operator+(const Polynomial& vl) const { this->printList(); vl.printList(); @@ -151,12 +169,12 @@ Polynomial Polynomial::operator+(const Polynomial& vl) const{ return result; } -Polynomial Polynomial::operator*(const Monomial& mono) const{ - if(mono.isZero()){ +Polynomial Polynomial::operator*(const Monomial& mono) const { + if(mono.isZero()) { return Polynomial(mono); //Don't multiply by zero - }else{ + } else { std::vector newMonos; - for(iterator i = this->begin(), end = this->end(); i != end; ++i){ + for(iterator i = this->begin(), end = this->end(); i != end; ++i) { newMonos.push_back(mono * (*i)); } @@ -169,9 +187,9 @@ Polynomial Polynomial::operator*(const Monomial& mono) const{ } } -Polynomial Polynomial::operator*(const Polynomial& poly) const{ +Polynomial Polynomial::operator*(const Polynomial& poly) const { Polynomial res = Polynomial::mkZero(); - for(iterator i = this->begin(), end = this->end(); i != end; ++i){ + for(iterator i = this->begin(), end = this->end(); i != end; ++i) { Monomial curr = *i; Polynomial prod = poly * curr; Polynomial sum = res + prod; @@ -181,10 +199,10 @@ Polynomial Polynomial::operator*(const Polynomial& poly) const{ } -Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r){ +Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r) { Assert(!l.isConstant()); Assert(isRelationOperator(k)); - switch(k){ + switch(k) { case kind::GEQ: case kind::EQUAL: case kind::LEQ: @@ -198,10 +216,10 @@ Node Comparison::toNode(Kind k, const Polynomial& l, const Constant& r){ } } -Comparison Comparison::parseNormalForm(TNode n){ - if(n.getKind() == kind::CONST_BOOLEAN){ +Comparison Comparison::parseNormalForm(TNode n) { + if(n.getKind() == kind::CONST_BOOLEAN) { return Comparison(n.getConst()); - }else{ + } else { bool negated = n.getKind() == kind::NOT; Node relation = negated ? n[0] : n; Assert( !negated || @@ -212,10 +230,10 @@ Comparison Comparison::parseNormalForm(TNode n){ Constant right(relation[1]); Kind newOperator = relation.getKind(); - if(negated){ - if(newOperator == kind::LEQ){ + if(negated) { + if(newOperator == kind::LEQ) { newOperator = kind::GT; - }else{ + } else { newOperator = kind::LT; } } @@ -223,19 +241,19 @@ Comparison Comparison::parseNormalForm(TNode n){ } } -Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right){ +Comparison Comparison::mkComparison(Kind k, const Polynomial& left, const Constant& right) { Assert(isRelationOperator(k)); - if(left.isConstant()){ + if(left.isConstant()) { const Rational& rConst = left.getNode().getConst(); const Rational& lConst = right.getNode().getConst(); bool res = evaluateConstantPredicate(k, lConst, rConst); return Comparison(res); - }else{ + } else { return Comparison(toNode(k, left, right), k, left, right); } } -Comparison Comparison::addConstant(const Constant& constant) const{ +Comparison Comparison::addConstant(const Constant& constant) const { Assert(!isBoolean()); Monomial mono(constant); Polynomial constAsPoly( mono ); @@ -244,7 +262,7 @@ Comparison Comparison::addConstant(const Constant& constant) const{ return mkComparison(oper, newLeft, newRight); } -Comparison Comparison::multiplyConstant(const Constant& constant) const{ +Comparison Comparison::multiplyConstant(const Constant& constant) const { Assert(!isBoolean()); Kind newOper = (constant.getValue() < 0) ? negateRelationKind(oper) : oper; diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h index 0762868cf..a09437160 100644 --- a/src/theory/arith/normal_form.h +++ b/src/theory/arith/normal_form.h @@ -1,3 +1,26 @@ +/********************* */ +/*! \file normal_form.h + ** \verbatim + ** Original author: taking + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H +#define __CVC4__THEORY__ARITH__NORMAL_FORM_H #include "expr/node.h" #include "util/rational.h" @@ -8,9 +31,6 @@ #include #include -#ifndef __CVC4__THEORY__ARITH__NORMAL_FORM_H -#define __CVC4__THEORY__ARITH__NORMAL_FORM_H - namespace CVC4 { namespace theory { namespace arith { @@ -29,34 +49,34 @@ namespace arith { * variable := n * where * n.getMetaKind() == metakind::VARIABLE - + * * constant := n * where * n.getKind() == kind::CONST_RATIONAL - + * * var_list := variable | (* [variable]) * where * len [variable] >= 2 * isSorted varOrder [variable] - + * * monomial := constant | var_list | (* constant' var_list') * where * constant' \not\in {0,1} - + * * polynomial := monomial' | (+ [monomial]) * where * len [monomial] >= 2 * isStrictlySorted monoOrder [monomial] * forall (\x -> x != 0) [monomial] - + * * restricted_cmp := (|><| polynomial constant) * where * |><| is GEQ, EQ, or EQ * not (exists constantMonomial (monomialList polynomial)) * monomialCoefficient (head (monomialList polynomial)) == 1 - + * * comparison := TRUE | FALSE | restricted_cmp | (not restricted_cmp) - + * * Normal Form for terms := polynomial * Normal Form for atoms := comparison */ @@ -94,11 +114,11 @@ namespace arith { * And if isMember(node) is false, this throws an assertion failure in debug * mode and has undefined behaviour if not in debug mode. * -Only public facing constructors, parseClass(node), and mk*() functions are - * considered privledged functions for the helper class. - * -Only privledged functions may use private constructors, and access + * considered privileged functions for the helper class. + * -Only privileged functions may use private constructors, and access * private data members. - * -All non-privledges functions are considered utility functions and - * must use a privledged function in order to create an instance of the class. + * -All non-privileged functions are considered utility functions and + * must use a privileged function in order to create an instance of the class. */ /** @@ -143,6 +163,7 @@ namespace arith { * | (+ [monomial]) -> [monomial] */ + /** * A NodeWrapper is a class that is a thinly veiled container of a Node object. */ @@ -152,7 +173,8 @@ private: public: NodeWrapper(Node n) : node(n) {} const Node& getNode() const { return node; } -}; +};/* class NodeWrapper */ + class Variable : public NodeWrapper { public: @@ -166,10 +188,11 @@ public: bool isNormalForm() { return isMember(getNode()); } - bool operator<(const Variable& v) const{ return getNode() < v.getNode();} - bool operator==(const Variable& v) const{ return getNode() == v.getNode();} + bool operator<(const Variable& v) const { return getNode() < v.getNode();} + bool operator==(const Variable& v) const { return getNode() == v.getNode();} + +};/* class Variable */ -}; class Constant : public NodeWrapper { public: @@ -187,7 +210,7 @@ public: return Constant(coerceToRationalNode(n)); } - static Constant mkConstant(const Rational& rat){ + static Constant mkConstant(const Rational& rat) { return Constant(mkRationalNode(rat)); } @@ -195,30 +218,34 @@ public: return getNode().getConst(); } - bool isZero() const{ return getValue() == 0; } - bool isOne() const{ return getValue() == 1; } + bool isZero() const { return getValue() == 0; } + bool isOne() const { return getValue() == 1; } - Constant operator*(const Constant& other) const{ + Constant operator*(const Constant& other) const { return mkConstant(getValue() * other.getValue()); } - Constant operator+(const Constant& other) const{ + Constant operator+(const Constant& other) const { return mkConstant(getValue() + other.getValue()); } - Constant operator-() const{ + Constant operator-() const { return mkConstant(-getValue()); } -}; + +};/* class Constant */ + template -inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end){ +inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) { NodeBuilder<> nb(k); - while(start != end){ + while(start != end) { nb << (*start).getNode(); ++start; } + return Node(nb); -} +}/* makeNode(Kind, iterator, iterator) */ + /** * A VarList is a sorted list of variables representing a product. @@ -231,18 +258,19 @@ class VarList { private: Node backingNode; - static Node multList(const std::vector& list){ + static Node multList(const std::vector& list) { Assert(list.size() >= 2); return makeNode(kind::MULT, list.begin(), list.end()); } - static Node makeTuple(Node n){ + static Node makeTuple(Node n) { + // MGD FOR REVIEW: drop IDENTITY kind ? return NodeManager::currentNM()->mkNode(kind::IDENTITY, n); } - VarList() : backingNode(Node::null()){} + VarList() : backingNode(Node::null()) {} - VarList(Node n){ + VarList(Node n) { backingNode = (Variable::isMember(n)) ? makeTuple(n) : n; Assert(isSorted(begin(), end())); @@ -255,15 +283,15 @@ public: public: explicit iterator(Node::iterator i) : d_iter(i) {} - inline Variable operator*(){ + inline Variable operator*() { return Variable(*d_iter); } - bool operator==(const iterator& i){ + bool operator==(const iterator& i) { return d_iter == i.d_iter; } - bool operator!=(const iterator& i){ + bool operator!=(const iterator& i) { return d_iter != i.d_iter; } @@ -277,52 +305,52 @@ public: } }; - Node getNode() const{ - if(singleton()){ + Node getNode() const { + if(singleton()) { return backingNode[0]; - }else{ + } else { return backingNode; } } - iterator begin() const{ + iterator begin() const { return iterator(backingNode.begin()); } - iterator end() const{ + iterator end() const { return iterator(backingNode.end()); } - VarList(Variable v) : backingNode(makeTuple(v.getNode())){ + VarList(Variable v) : backingNode(makeTuple(v.getNode())) { Assert(isSorted(begin(), end())); } - VarList(const std::vector& l) : backingNode(multList(l)){ + VarList(const std::vector& l) : backingNode(multList(l)) { Assert(l.size() >= 2); Assert(isSorted(begin(), end())); } static bool isMember(Node n); - bool isNormalForm() const{ + bool isNormalForm() const { return !empty(); } - static VarList mkEmptyVarList(){ + static VarList mkEmptyVarList() { return VarList(); } /** There are no restrictions on the size of l */ - static VarList mkVarList(const std::vector& l){ - if(l.size() == 0){ + static VarList mkVarList(const std::vector& l) { + if(l.size() == 0) { return mkEmptyVarList(); - }else if(l.size() == 1){ + } else if(l.size() == 1) { return VarList((*l.begin()).getNode()); - }else{ + } else { return VarList(l); } } - int size() const{ return backingNode.getNumChildren(); } + int size() const { return backingNode.getNumChildren(); } bool empty() const { return size() == 0; } bool singleton() const { return backingNode.getKind() == kind::IDENTITY; } @@ -332,13 +360,15 @@ public: int cmp(const VarList& vl) const; - bool operator<(const VarList& vl) const{ return cmp(vl) < 0; } + bool operator<(const VarList& vl) const { return cmp(vl) < 0; } - bool operator==(const VarList& vl) const{ return cmp(vl) == 0; } + bool operator==(const VarList& vl) const { return cmp(vl) == 0; } private: bool isSorted(iterator start, iterator end); -}; + +};/* class VarList */ + class Monomial : public NodeWrapper { private: @@ -353,14 +383,14 @@ private: Assert(!c.isOne() || !multStructured(n)); } - static Node makeMultNode(const Constant& c, const VarList& vl){ + static Node makeMultNode(const Constant& c, const VarList& vl) { Assert(!c.isZero()); Assert(!c.isOne()); Assert(!vl.empty()); return NodeManager::currentNM()->mkNode(kind::MULT, c.getNode(), vl.getNode()); } - static bool multStructured(Node n){ + static bool multStructured(Node n) { return n.getKind() == kind::MULT && n[0].getKind() == kind::CONST_RATIONAL && n.getNumChildren() == 2; @@ -394,20 +424,20 @@ public: static Monomial parseMonomial(Node n); - static Monomial mkZero(){ + static Monomial mkZero() { return Monomial(Constant::mkConstant(0)); } - static Monomial mkOne(){ + static Monomial mkOne() { return Monomial(Constant::mkConstant(1)); } - const Constant& getConstant() const{ return constant; } - const VarList& getVarList() const{ return varList; } + const Constant& getConstant() const { return constant; } + const VarList& getVarList() const { return varList; } - bool isConstant() const{ + bool isConstant() const { return varList.empty(); } - bool isZero() const{ + bool isZero() const { return constant.isZero(); } @@ -418,23 +448,23 @@ public: Monomial operator*(const Monomial& mono) const; - int cmp(const Monomial& mono) const{ + int cmp(const Monomial& mono) const { return getVarList().cmp(mono.getVarList()); } - bool operator<(const Monomial& vl) const{ + bool operator<(const Monomial& vl) const { return cmp(vl) < 0; } - bool operator==(const Monomial& vl) const{ + bool operator==(const Monomial& vl) const { return cmp(vl) == 0; } - static bool isSorted(const std::vector& m){ + static bool isSorted(const std::vector& m) { return __gnu_cxx::is_sorted(m.begin(), m.end()); } - static bool isStrictlySorted(const std::vector& m){ + static bool isStrictlySorted(const std::vector& m) { return isSorted(m) && std::adjacent_find(m.begin(),m.end()) == m.end(); } @@ -445,10 +475,12 @@ public: static std::vector sumLikeTerms(const std::vector& monos); static void printList(const std::vector& monos); -}; +};/* class Monomial */ + class Polynomial : public NodeWrapper { private: + // MGD FOR REVIEW: do not create this vector<>! std::vector monos; Polynomial(Node n, const std::vector& m): @@ -458,7 +490,7 @@ private: Assert( Monomial::isStrictlySorted(monos) ); } - static Node makePlusNode(const std::vector& m){ + static Node makePlusNode(const std::vector& m) { Assert(m.size() >= 2); return makeNode(kind::PLUS, m.begin(), m.end()); @@ -467,8 +499,8 @@ private: public: typedef std::vector::const_iterator iterator; - iterator begin() const{ return monos.begin(); } - iterator end() const{ return monos.end(); } + iterator begin() const { return monos.begin(); } + iterator end() const { return monos.end(); } Polynomial(const Monomial& m): NodeWrapper(m.getNode()), monos() @@ -483,51 +515,52 @@ public: } - static Polynomial mkPolynomial(const std::vector& m){ - if(m.size() == 0){ + static Polynomial mkPolynomial(const std::vector& m) { + if(m.size() == 0) { return Polynomial(Monomial::mkZero()); - }else if(m.size() == 1){ + } else if(m.size() == 1) { return Polynomial((*m.begin())); - }else{ + } else { return Polynomial(m); } } - static Polynomial parsePolynomial(Node n){ + // MGD FOR REVIEW: make this constant time (for non-debug mode) + static Polynomial parsePolynomial(Node n) { std::vector monos; - if(n.getKind() == kind::PLUS){ - for(Node::iterator i=n.begin(), end=n.end(); i != end; ++i){ + if(n.getKind() == kind::PLUS) { + for(Node::iterator i=n.begin(), end=n.end(); i != end; ++i) { monos.push_back(Monomial::parseMonomial(*i)); } - }else{ + } else { monos.push_back(Monomial::parseMonomial(n)); } return Polynomial(n,monos); } - static Polynomial mkZero(){ + static Polynomial mkZero() { return Polynomial(Monomial::mkZero()); } - static Polynomial mkOne(){ + static Polynomial mkOne() { return Polynomial(Monomial::mkOne()); } - bool isZero() const{ + bool isZero() const { return (monos.size() == 1) && (getHead().isZero()); } - bool isConstant() const{ + bool isConstant() const { return (monos.size() == 1) && (getHead().isConstant()); } - bool containsConstant() const{ + bool containsConstant() const { return getHead().isConstant(); } - Monomial getHead() const{ + Monomial getHead() const { return *(begin()); } - Polynomial getTail() const{ + Polynomial getTail() const { Assert(monos.size() >= 1); iterator start = begin()+1; @@ -535,10 +568,10 @@ public: return mkPolynomial(subrange); } - void printList() const{ - Debug("blah") << "start list" << std::endl; + void printList() const { + Debug("normal-form") << "start list" << std::endl; Monomial::printList(monos); - Debug("blah") << "end list" << std::endl; + Debug("normal-form") << "end list" << std::endl; } Polynomial operator+(const Polynomial& vl) const; @@ -547,7 +580,8 @@ public: Polynomial operator*(const Polynomial& poly) const; -}; +};/* class Polynomial */ + class Comparison : public NodeWrapper { private: @@ -578,18 +612,18 @@ public: static Comparison mkComparison(Kind k, const Polynomial& left, const Constant& right); - bool isBoolean() const{ + bool isBoolean() const { return (oper == kind::CONST_BOOLEAN); } - bool isNormalForm() const{ - if(isBoolean()){ + bool isNormalForm() const { + if(isBoolean()) { return true; - }else if(left.containsConstant()){ + } else if(left.containsConstant()) { return false; - }else if(left.getHead().getConstant().isOne()){ + } else if(left.getHead().getConstant().isOne()) { return true; - }else{ + } else { return false; } } @@ -601,12 +635,11 @@ public: Comparison multiplyConstant(const Constant& constant) const; static Comparison parseNormalForm(TNode n); -}; - +};/* class Comparison */ -}; /* namesapce arith */ -}; /* namespace theory */ -}; /* namespace CVC4 */ +}/* CVC4::theory::arith namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ #endif /* __CVC4__THEORY__ARITH__NORMAL_FORM_H */ diff --git a/src/theory/arith/ordered_bounds_list.h b/src/theory/arith/ordered_bounds_list.h index 4393a382e..f3bf3d58b 100644 --- a/src/theory/arith/ordered_bounds_list.h +++ b/src/theory/arith/ordered_bounds_list.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/tableau.h b/src/theory/arith/tableau.h index 603eb5278..768d9f39d 100644 --- a/src/theory/arith/tableau.h +++ b/src/theory/arith/tableau.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): dejan, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp index 8f17b01a9..41882e87c 100644 --- a/src/theory/arith/theory_arith.cpp +++ b/src/theory/arith/theory_arith.cpp @@ -3,7 +3,7 @@ ** \verbatim ** Original author: taking ** Major contributors: none - ** Minor contributors (to current version): mdeters + ** Minor contributors (to current version): barrett, dejan, mdeters ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h index 03be7a77b..450d5c608 100644 --- a/src/theory/arith/theory_arith.h +++ b/src/theory/arith/theory_arith.h @@ -3,7 +3,7 @@ ** \verbatim ** Original author: mdeters ** Major contributors: taking - ** Minor contributors (to current version): none + ** Minor contributors (to current version): barrett ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences diff --git a/src/theory/arith/theory_arith_type_rules.h b/src/theory/arith/theory_arith_type_rules.h index b8fa85c03..8bfd2aef6 100644 --- a/src/theory/arith/theory_arith_type_rules.h +++ b/src/theory/arith/theory_arith_type_rules.h @@ -2,7 +2,7 @@ /*! \file theory_arith_type_rules.h ** \verbatim ** Original author: dejan - ** Major contributors: mdeters + ** Major contributors: mdeters, cconway ** Minor contributors (to current version): none ** This file is part of the CVC4 prototype. ** Copyright (c) 2009, 2010 The Analysis of Computer Systems Group (ACSys) -- cgit v1.2.3