summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/expr/node_manager.cpp3
-rw-r--r--src/theory/arith/kinds2
-rw-r--r--src/theory/arith/normal_form.cpp16
-rw-r--r--src/theory/arith/normal_form.h118
-rw-r--r--src/theory/arith/theory_arith.cpp3
5 files changed, 96 insertions, 46 deletions
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index 8ff83bb94..edb3a1592 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -263,9 +263,6 @@ TypeNode NodeManager::getType(TNode n, bool check)
case kind::APPLY_UF:
typeNode = CVC4::theory::uf::UfTypeRule::computeType(this, n, check);
break;
- case kind::IDENTITY:
- typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
- break;
case kind::PLUS:
typeNode = CVC4::theory::arith::ArithOperatorTypeRule::computeType(this, n, check);
break;
diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 5cd4719b1..6808e3d8f 100644
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -12,8 +12,6 @@ operator MINUS 2 "arithmetic binary subtraction operator"
operator UMINUS 1 "arithmetic unary negation"
operator DIVISION 2 "arithmetic division"
-operator IDENTITY 1 "identity function"
-
constant CONST_RATIONAL \
::CVC4::Rational \
::CVC4::RationalHashStrategy \
diff --git a/src/theory/arith/normal_form.cpp b/src/theory/arith/normal_form.cpp
index 60f6fa022..1449226db 100644
--- a/src/theory/arith/normal_form.cpp
+++ b/src/theory/arith/normal_form.cpp
@@ -70,22 +70,14 @@ VarList VarList::parseVarList(Node n) {
}
}
-VarList VarList::operator*(const VarList& vl) const {
+VarList VarList::operator*(const VarList& other) const {
if(this->empty()) {
- return vl;
- } else if(vl.empty()) {
+ return other;
+ } else if(other.empty()) {
return *this;
} else {
vector<Node> result;
- back_insert_iterator< vector<Node> > bii(result);
-
- Node::iterator
- thisBegin = this->backingNode.begin(),
- thisEnd = this->backingNode.end(),
- v1Begin = vl.backingNode.begin(),
- v1End = vl.backingNode.end();
-
- merge(thisBegin, thisEnd, v1Begin, v1End, bii);
+ merge(other, result);
Assert(result.size() >= 2);
Node mult = NodeManager::currentNM()->mkNode(kind::MULT, result);
return VarList::parseVarList(mult);
diff --git a/src/theory/arith/normal_form.h b/src/theory/arith/normal_form.h
index 2e20c62c5..291929f8f 100644
--- a/src/theory/arith/normal_form.h
+++ b/src/theory/arith/normal_form.h
@@ -23,6 +23,7 @@
#define __CVC4__THEORY__ARITH__NORMAL_FORM_H
#include "expr/node.h"
+#include "expr/node_self_iterator.h"
#include "util/rational.h"
#include "theory/arith/arith_constants.h"
#include "theory/arith/arith_utilities.h"
@@ -247,6 +248,34 @@ inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
}/* makeNode<GetNodeIterator>(Kind, iterator, iterator) */
+template <class GetNodeIterator>
+static void copy_range(GetNodeIterator begin, GetNodeIterator end, std::vector<Node>& result){
+ while(begin != end){
+ result.push_back(*begin);
+ ++begin;
+ }
+}
+
+template <class GetNodeIterator>
+static void merge_ranges(GetNodeIterator first1,
+ GetNodeIterator last1,
+ GetNodeIterator first2,
+ GetNodeIterator last2,
+ std::vector<Node>& result) {
+
+ while(first1 != last1 && first2 != last2){
+ if( (*first1) < (*first2) ){
+ result.push_back(*first1);
+ ++ first1;
+ }else{
+ result.push_back(*first2);
+ ++ first2;
+ }
+ }
+ copy_range(first1, last1, result);
+ copy_range(first2, last2, result);
+}
+
/**
* A VarList is a sorted list of variables representing a product.
* If the VarList is empty, it represents an empty product or 1.
@@ -254,34 +283,56 @@ inline Node makeNode(Kind k, GetNodeIterator start, GetNodeIterator end) {
*
* A non-sorted VarList can never be successfully made in debug mode.
*/
-class VarList {
+class VarList : public NodeWrapper {
private:
- Node backingNode;
static Node multList(const std::vector<Variable>& list) {
Assert(list.size() >= 2);
return makeNode(kind::MULT, list.begin(), list.end());
}
- static Node makeTuple(Node n) {
- // MGD FOR REVIEW: drop IDENTITY kind ?
- return NodeManager::currentNM()->mkNode(kind::IDENTITY, n);
+
+ VarList() : NodeWrapper(Node::null()) {}
+
+ VarList(Node n) : NodeWrapper(n) {
+ Assert(isSorted(begin(), end()));
}
- VarList() : backingNode(Node::null()) {}
+ typedef expr::NodeSelfIterator internal_iterator;
- VarList(Node n) {
- backingNode = (Variable::isMember(n)) ? makeTuple(n) : n;
+ internal_iterator internalBegin() const {
+ if(singleton()){
+ return expr::NodeSelfIterator::self(getNode());
+ }else{
+ return getNode().begin();
+ }
+ }
- Assert(isSorted(begin(), end()));
+ internal_iterator internalEnd() const {
+ if(singleton()){
+ return expr::NodeSelfIterator::selfEnd(getNode());
+ }else{
+ return getNode().end();
+ }
+ }
+ void merge(const VarList& other, std::vector<Node>& result) const{
+ internal_iterator
+ thisBegin = this->internalBegin(),
+ thisEnd = this->internalEnd(),
+ otherBegin = other.internalBegin(),
+ otherEnd = other.internalEnd();
+
+ merge_ranges(thisBegin, thisEnd, otherBegin, otherEnd, result);
}
public:
- class iterator {
+
+ class iterator {
private:
- Node::iterator d_iter;
+ internal_iterator d_iter;
+
public:
- explicit iterator(Node::iterator i) : d_iter(i) {}
+ explicit iterator(internal_iterator i) : d_iter(i) {}
inline Variable operator*() {
return Variable(*d_iter);
@@ -305,25 +356,32 @@ public:
}
};
- Node getNode() const {
- if(singleton()) {
- return backingNode[0];
- } else {
- return backingNode;
+ iterator begin() const {
+ expr::NodeSelfIterator iter;
+ if(singleton()){
+ iter = expr::NodeSelfIterator::self(getNode());
+ }else{
+ iter = getNode().begin();
}
+ return iterator(iter);
}
- iterator begin() const {
- return iterator(backingNode.begin());
- }
iterator end() const {
- return iterator(backingNode.end());
+ expr::NodeSelfIterator iter;
+ if(singleton()){
+ iter = expr::NodeSelfIterator::self(getNode());
+ }else{
+ iter = getNode().end();
+ }
+
+ return iterator(iter);
}
- VarList(Variable v) : backingNode(makeTuple(v.getNode())) {
+ VarList(Variable v) : NodeWrapper(v.getNode()) {
Assert(isSorted(begin(), end()));
}
- VarList(const std::vector<Variable>& l) : backingNode(multList(l)) {
+
+ VarList(const std::vector<Variable>& l) : NodeWrapper(multList(l)) {
Assert(l.size() >= 2);
Assert(isSorted(begin(), end()));
}
@@ -350,9 +408,17 @@ public:
}
}
- int size() const { return backingNode.getNumChildren(); }
- bool empty() const { return size() == 0; }
- bool singleton() const { return backingNode.getKind() == kind::IDENTITY; }
+ bool empty() const { return getNode().isNull(); }
+ bool singleton() const {
+ return !empty() && getNode().getKind() != kind::MULT;
+ }
+
+ int size() const {
+ if(singleton())
+ return 1;
+ else
+ return getNode().getNumChildren();
+ }
static VarList parseVarList(Node n);
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index ac3dc3d40..4a783a6a4 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -980,9 +980,6 @@ Node TheoryArith::getValue(TNode n, TheoryEngine* engine) {
return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() /
engine->getValue(n[1]).getConst<Rational>() );
- case kind::IDENTITY: // 1 arg
- return engine->getValue(n[0]);
-
case kind::LT: // 2 args
return nodeManager->mkConst( engine->getValue(n[0]).getConst<Rational>() <
engine->getValue(n[1]).getConst<Rational>() );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback