diff options
Diffstat (limited to 'lib/omega/include')
41 files changed, 5929 insertions, 0 deletions
diff --git a/lib/omega/include/basic/Bag.h b/lib/omega/include/basic/Bag.h new file mode 100644 index 0000000..a3d07a0 --- /dev/null +++ b/lib/omega/include/basic/Bag.h @@ -0,0 +1,405 @@ +#if ! defined _Bag_h +#define _Bag_h 1 + +#include <stdio.h> +#include <basic/Iterator.h> +#include <basic/Collection.h> +#include <basic/Link.h> +#include <assert.h> + +namespace omega { + +template<class T> class Bag : public Collection<T> { +public: +virtual ~Bag(); + Bag(); + Bag(const Bag<T>&); + Bag & operator=(const Bag<T>&); + //! add elements in b + virtual void operator |= (const Bag<T> & b); + Iterator<T> *new_iterator(); + bool empty() const; + void remove(T); + virtual void insert(T); + void clear(); + virtual bool contains(T) const; + int size() const; + T extract(); +// protected: breaks g++ 261 + List_Element<T>* contents; +}; + + +template<class T> class Ordered_Bag : public Bag<T> { +public: + Ordered_Bag(); + Ordered_Bag(const Ordered_Bag<T>& B) : Bag<T>(B) {} + void insert(T); + //! add elements in b + virtual void operator |= (const Ordered_Bag<T> & b); + //! add elements in b + void operator |= (const Bag<T> & b); + bool contains(T) const; + bool operator == (const Ordered_Bag<T>&) const; + bool operator != (const Ordered_Bag<T>&) const; + bool operator < (const Ordered_Bag<T>&) const; +}; + +template <class T> class Set : public Ordered_Bag <T> { +public: + Set(); + Set(T); + Set(const Set<T>& S) : Ordered_Bag<T>(S) {} + + bool contains (const Set<T>& b) const; + bool contains (T t) const { return Ordered_Bag<T>::contains(t); } + // the above makes "standard" C++ happy + + //! add elements in b + virtual void operator |= (const Set<T> & b); + //! add elements in b + void operator |= (const Ordered_Bag<T> & b); + //! add elements in b + void operator |= (const Bag<T> & b); + + //! delete items also in b + void operator -= (const Set<T> & b); + //! delete items not in b + void operator &= (const Set<T> & b); + //! check for elements in common + bool operator & (const Set<T> &) const; +}; + +} // namespace + +#define instantiate_Bag(T) template class Bag<T>; \ + instantiate_List_Element(T); +#define instantiate_Ordered_Bag(T) template class Ordered_Bag<T>; \ + instantiate_Bag(T) +#define instantiate_Set(T) template class Set<T>; \ + instantiate_Ordered_Bag(T) + + +namespace omega { + +template<class T> Bag<T>::Bag() { + contents = new List_Element <T>; + contents->tail = 0; + } +template<class T> Bag<T>::~Bag() { + delete contents; + } + +template<class T> Ordered_Bag<T>::Ordered_Bag() {} + +template<class T> Set<T>::Set() {} + +template<class T> Bag<T>::Bag(const Bag<T> &L) { + contents = new List_Element<T>(*L.contents); + } + +template<class T> Bag<T> & Bag<T>::operator=(const Bag<T> &L) { + if (this != &L) { + delete contents; + contents = new List_Element<T>(*L.contents); + } + return *this; + } + + + +template<class T> Set<T>::Set(T e) { + assert(this->contents); + this->contents->tail = new List_Element<T>(e, 0); + } + + +/**************************************************************** + * * + * Misc. simple Collection operations * + * * + ****************************************************************/ + +template<class T> bool Bag<T>::empty() const { + return contents->tail == 0; + } + +template<class T> Iterator<T> *Bag<T>::new_iterator() + { + return new List_Element_Iterator<T>(contents->tail); + } + + +template<class T> void Bag<T>::clear() { + if (contents->tail) delete contents->tail; + contents->tail = 0; + } + +template<class T> int Bag<T>::size() const { + int i = 0; + List_Element<T> * p = contents->tail; + while (p) { + p = p->tail; + i++; + }; + return i; + } + + +/**************************************************************** + * * + * Collection/Element operations (e.g. insert, contains) * + * * + ****************************************************************/ + +template<class T> void Bag<T>::remove(T e) { + List_Element<T> * p = contents; + while (p->tail && p->tail->head != e) p = p->tail; + if (p->tail && p->tail->head == e) { + List_Element<T> * q = p->tail; + p->tail = q->tail; + q->tail = 0; + delete q; + } + } + +template<class T> T Bag<T>::extract() { + List_Element<T> * p = contents->tail; + T e = p->head; + contents->tail = p->tail; + p->tail = 0; + delete p; + return e; + } + + +template<class T> void Bag<T>::insert(T e) { + List_Element<T> * q = new List_Element<T>(e,contents->tail); + contents->tail = q; + } + +template<class T> void Ordered_Bag<T>::insert(T e) { + List_Element<T> * p = this->contents; + while (p->tail && p->tail->head < e) p = p->tail; + if (!p->tail || p->tail->head != e) { + List_Element<T> * q = new List_Element<T>(e,p->tail); + p->tail = q; + } + } + + +template<class T> bool Bag<T>::contains(T e) const { + List_Element<T> * p = contents; + while (p->tail && p->tail->head != e) p = p->tail; + return (p->tail && p->tail->head == e); + } + +template<class T> bool Ordered_Bag<T>::contains(T e) const { + List_Element<T> * p = this->contents; + while (p->tail && p->tail->head < e) p = p->tail; + return (p->tail && p->tail->head == e); + } + + +template<class T> bool Set<T>::contains (const Set<T>& b) const { + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents; + do { + /* consume matched elements in p and q */ + p = p->tail; + q = q->tail; + if (!q) return 1; /* no more elements to match */ + if (!p) return 0; /* nothing left in p to match with */ + if (q->head < p->head) { + /* nothing smaller than + p->head left in p, so q->head + can't be matched */ + return 0; + }; + while (p && p->head < q->head) { + /* toss away some elements from p */ + p = p->tail; + } + if (!p || q->head < p->head) return 0; + } while (q); + + return 1; + } + + + +/**************************************************************** + * * + * Collection/Collection operations (e.g. |=) * + * * + ****************************************************************/ + +template<class T> void Bag<T>::operator |= (const Bag<T> & b) { + assert(this != &b); + List_Element<T> * q = b.contents->tail; + + while (q) { + List_Element<T> * r = new List_Element<T>(q->head,contents->tail); + contents->tail = r; + q = q->tail; + } + } + +template<class T> void Ordered_Bag<T>::operator |= (const Ordered_Bag<T> & b) { + if (this == &b) return; + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents->tail; + + while (q) { + while (p->tail && p->tail->head < q->head) p = p->tail; + List_Element<T> * r = new List_Element<T>(q->head,p->tail); + p->tail = r; + q = q->tail; + } + } + +template<class T> void Ordered_Bag<T>::operator |= (const Bag<T> & b) { + Ordered_Bag<T> tmp; + for (List_Element<T> *p = b.contents; p; p=p->tail) { + tmp.insert(p->head); + } + *this |= tmp; +} + +template<class T> void Set<T>::operator |= (const Set<T> & b) { + if (this == &b) return; + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents->tail; + + while (q) { + while (p->tail && p->tail->head < q->head) p = p->tail; + if (!p->tail || p->tail->head != q->head) { + List_Element<T> * r = new List_Element<T>(q->head,p->tail); + p->tail = r; + } + q = q->tail; + } + } + +template<class T> void Set<T>::operator |= (const Ordered_Bag<T> & b) { + Set<T> tmp; + for (List_Element<T> *p = b.contents; p; p=p->tail) { + tmp.insert(p->head); + } + *this |= tmp; +} + +template<class T> void Set<T>::operator |= (const Bag<T> & b) { + Set<T> tmp; + for (List_Element<T> *p = b.contents; p; p=p->tail) { + tmp.insert(p->head); + } + *this |= tmp; +} + + + +// delete items also in b +template<class T> void Set<T>::operator -= (const Set<T> & b) { + if (this == &b) { + this->clear(); + return; + } + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents->tail; + + while (q) { + while (p->tail && p->tail->head < q->head) p = p->tail; + if (p->tail && p->tail->head == q->head) { + List_Element<T> * r = p->tail; + p->tail = r->tail; + r->tail = 0; + delete r; + } + q = q->tail; + } + } + + +// delete items not in b +template<class T> void Set<T>::operator &= (const Set<T> & b) + { + if (this == &b) return; + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents->tail; + + while (q) { + while (p->tail && p->tail->head < q->head) { + List_Element<T> * r = p->tail; + p->tail = r->tail; + r->tail = 0; + delete r; + }; + if (p->tail && p->tail->head == q->head) { + /* allow p->tail->head into the result */ + p = p->tail; + } + /* q->head has matched anything it is going to match */ + q = q->tail; + } + if (p->tail) { + delete p->tail; + p->tail = 0; + }; + + } + + +template<class T> bool Set<T>::operator & (const Set<T>& b) const { + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents; + do { + p = p->tail; + q = q->tail; + while (p && q && p->head != q->head) { + while (p && p->head < q->head) p = p->tail; + while (p && q && q->head < p->head) q = q->tail; + }; + if (p && q && p->head == q->head) return 1; + } while (p && q); + + return 0; + } + + +template<class T> bool Ordered_Bag<T>::operator == (const Ordered_Bag<T>& b) const { + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents; + while (1) { + p = p->tail; + q = q->tail; + if (!p && !q) return 1; + if (!p || !q) return 0; + if (p->head != q->head) return 0; + }; + + } + +template<class T> bool Ordered_Bag<T>::operator != (const Ordered_Bag<T>& b) const { + return !(*this == b); + } + +template<class T> bool Ordered_Bag<T>::operator < (const Ordered_Bag<T>& b) const { + List_Element<T> * p = this->contents; + List_Element<T> * q = b.contents; + while (1) { + p = p->tail; + q = q->tail; + if (!p && !q) return 0; + if (!p) return 1; + if (!q) return 0; + if (p->head < q->head) return 1; + if (q->head < p->head) return 0; + }; + + return 1; + } + +} // namespace + +#endif diff --git a/lib/omega/include/basic/BoolSet.h b/lib/omega/include/basic/BoolSet.h new file mode 100755 index 0000000..a78af2e --- /dev/null +++ b/lib/omega/include/basic/BoolSet.h @@ -0,0 +1,641 @@ +/***************************************************************************** + Copyright (C) 2009-2011 Chun Chen + All Rights Reserved. + + Purpose: + BoolSet class, used as a set of integers from 0..n-1 where n is a very + small integer. + + Notes: + Set operands of binary operations can be of different sizes, missing + elements are treated as false. + + History: + 03/30/09 Created by Chun Chen. + 03/26/11 iterator added, -chun +*****************************************************************************/ + +#ifndef _BOOLSET_H +#define _BOOLSET_H + +#include <vector> +#include <iostream> +#include <assert.h> +#include <stdexcept> +#include <iterator> + +namespace omega { + + //! BoolSet class, used as a set of integers from 0 to n-1 where n is a very small integer. +template<typename T = unsigned int> +class BoolSet { +protected: + unsigned int size_; + std::vector<T> set_; + +public: + BoolSet(unsigned int size = 0); + ~BoolSet() {} + + void set(unsigned int); + void unset(unsigned int); + void set_all(); + void unset_all(); + bool get(unsigned int) const; + unsigned int size() const {return size_;} + unsigned int num_elem() const; + bool imply(const BoolSet<T> &) const; + bool empty() const; + void dump() const; + + BoolSet<T> &operator|=(const BoolSet<T> &); + BoolSet<T> &operator&=(const BoolSet<T> &); + BoolSet<T> &operator-=(const BoolSet<T> &); + + //! union + template<typename TT> friend BoolSet<TT> operator|(const BoolSet<TT> &, const BoolSet<TT> &); + //! intersection + template<typename TT> friend BoolSet<TT> operator&(const BoolSet<TT> &, const BoolSet<TT> &); + //! difference + template<typename TT> friend BoolSet<TT> operator-(const BoolSet<TT> &, const BoolSet<TT> &); + //! complement + template<typename TT> friend BoolSet<TT> operator~(const BoolSet<TT> &); + template<typename TT> friend bool operator==(const BoolSet<TT> &, const BoolSet<TT> &); + template<typename TT> friend bool operator!=(const BoolSet<TT> &, const BoolSet<TT> &); + template<typename TT> friend std::ostream& operator<<(std::ostream &, const BoolSet<TT> &); + template<typename TT> friend bool operator<(const BoolSet<TT> &, const BoolSet<TT> &); + +public: + class iterator; + class const_iterator; + iterator begin(); + iterator end(); + const_iterator begin() const; + const_iterator end() const; +}; + + +template<typename T> +BoolSet<T>::BoolSet(unsigned int size) { + assert(size >= 0); + size_ = size; + unsigned int n = size / (sizeof(T)*8); + unsigned int r = size % (sizeof(T)*8); + if (r != 0) + n++; + set_ = std::vector<T>(n, static_cast<T>(0)); +} + + +template<typename T> +void BoolSet<T>::set(unsigned int i) { + assert(i < size_ && i >= 0); + unsigned int n = i / (sizeof(T)*8); + unsigned int r = i % (sizeof(T)*8); + + T t = static_cast<T>(1) << r; + set_[n] |= t; +} + + +template<typename T> +void BoolSet<T>::unset(unsigned int i) { + assert(i < size_ && i >= 0); + unsigned int n = i / (sizeof(T)*8); + unsigned int r = i % (sizeof(T)*8); + + T t = static_cast<T>(1) << r; + t = ~t; + set_[n] &= t; +} + + +template<typename T> +void BoolSet<T>::set_all() { + unsigned int r = size_ % (sizeof(T)*8); + if (r == 0) { + for (unsigned int i = 0; i < set_.size(); i++) + set_[i] = ~static_cast<T>(0); + } + else { + for (unsigned int i = 0; i < set_.size()-1; i++) + set_[i] = ~static_cast<T>(0); + set_[set_.size()-1] = static_cast<T>(0); + T t = static_cast<T>(1); + for (unsigned int i = 0; i < r; i++) { + set_[set_.size()-1] |= t; + t = t<<1; + } + } +} + + +template<typename T> +void BoolSet<T>::unset_all() { + for (unsigned int i = 0; i < set_.size(); i++) + set_[i] = static_cast<T>(0); +} + + +template<typename T> +bool BoolSet<T>::get(unsigned int i) const { + assert(i < size_ && i >= 0); + unsigned int n = i / (sizeof(T)*8); + unsigned int r = i % (sizeof(T)*8); + + T t = static_cast<T>(1) << r; + t = set_[n] & t; + if (t) + return true; + else + return false; +} + + +template<typename T> +unsigned int BoolSet<T>::num_elem() const { + unsigned int n = size_; + unsigned int c = 0; + unsigned int p = 0; + while (n != 0) { + unsigned int m; + if (n >= sizeof(T)*8) { + m = sizeof(T)*8; + n -= sizeof(T)*8; + } + else { + m = n; + n = 0; + } + + T v = set_[p++]; + if (v != static_cast<T>(0)) { + for (unsigned int i = 0; i < m; i++) { + if (v & static_cast<T>(1)) + c++; + v >>= 1; + } + } + } + + return c; +} + + +template<typename T> +bool BoolSet<T>::imply(const BoolSet<T> &b) const { + if (size_ >= b.size_) { + for (unsigned int i = 0; i < b.set_.size(); i++) + if ((set_[i] & b.set_[i]) != b.set_[i]) + return false; + } + else { + for (unsigned int i = 0; i < set_.size(); i++) + if ((set_[i] & b.set_[i]) != b.set_[i]) + return false; + for (unsigned int i = set_.size(); i < b.set_.size(); i++) + if (b.set_[i] != static_cast<T>(0)) + return false; + } + + return true; +} + + +template<typename T> +bool BoolSet<T>::empty() const { + for (int i = 0; i < set_.size(); i++) + if (set_[i] != static_cast<T>(0)) + return false; + + return true; +} + + +template<typename T> +void BoolSet<T>::dump() const { + int j = 1; + for (unsigned int i = 0; i < size(); i++) { + if (get(i)) + std::cout << '1'; + else + std::cout << '0'; + if (j%10 == 0 && i != size() - 1) { + std::cout << ' '; + j = 1; + } + else + j++; + } + std::cout << std::endl; + std::cout.flush(); +} + + +template<typename T> +BoolSet<T> operator|(const BoolSet<T> &a, const BoolSet<T> &b) { + if (a.size_ >= b.size_) { + BoolSet<T> c = a; + for (unsigned int i = 0; i < b.set_.size(); i++) + c.set_[i] |= b.set_[i]; + return c; + } + else { + BoolSet<T> c = b; + for (unsigned int i = 0; i < a.set_.size(); i++) + c.set_[i] |= a.set_[i]; + return c; + } +} + + +template<typename T> +BoolSet<T> operator&(const BoolSet<T> &a, const BoolSet<T> &b) { + if (a.size_ >= b.size_) { + BoolSet<T> c = a; + for (unsigned int i = 0; i < b.set_.size(); i++) + c.set_[i] &= b.set_[i]; + for (unsigned int i = b.set_.size(); i < a.set_.size(); i++) + c.set_[i] = static_cast<T>(0); + return c; + } + else { + BoolSet<T> c = b; + for (unsigned int i = 0; i < a.set_.size(); i++) + c.set_[i] &= a.set_[i]; + for (unsigned int i = a.set_.size(); i < b.set_.size(); i++) + c.set_[i] = static_cast<T>(0); + return c; + } +} + + +template<typename T> +BoolSet<T> operator-(const BoolSet<T> &a, const BoolSet<T> &b) { + BoolSet<T> c(a.size_); + + int sz = a.set_.size(); + if (sz > b.set_.size()) + sz = b.set_.size(); + for (int i = 0; i < sz; i++) + c.set_[i] = a.set_[i] ^ (a.set_[i] & b.set_[i]); + for (int i = sz; i < a.set_.size(); i++) + c.set_[i] = a.set_[i]; + + return c; +} + + +template<typename T> +BoolSet<T> operator~(const BoolSet<T> &b) { + unsigned int r = b.size_ % (sizeof(T)*8); + BoolSet<T> a(b.size_); + for (unsigned int i = 0; i < b.set_.size(); i++) + a.set_[i] = ~b.set_[i]; + + if (r != 0) { + T t = static_cast<T>(1); + for (unsigned int i = 1; i < r; i++) + t = (t << 1) | static_cast<T>(1); + a.set_[a.set_.size()-1] &= t; + } + return a; +} + + +template<typename T> +bool operator==(const BoolSet<T> &a, const BoolSet<T> &b) { + return (a.size_ == b.size_) && (a.set_ == b.set_); +} + + +template<typename T> +bool operator!=(const BoolSet<T> &a, const BoolSet<T> &b) { + return !(a == b); +} + + + +template<typename T> +BoolSet<T> & BoolSet<T>::operator|=(const BoolSet<T> &b) { + *this = *this | b; + return *this; +} + + +template<typename T> +BoolSet<T> & BoolSet<T>::operator&=(const BoolSet<T> &b) { + *this = *this & b; + return *this; +} + + +template<typename T> +BoolSet<T> & BoolSet<T>::operator-=(const BoolSet<T> &b) { + *this = *this - b; + return *this; +} + + +template<typename T> +std::ostream& operator<<(std::ostream &os, const BoolSet<T> &b) { + os << '{'; + for (typename BoolSet<T>::const_iterator i = b.begin(); i != b.end(); i++) { + os << *i; + if (i+1 != b.end()) + os << ','; + } + os << '}'; + + return os; +} + + +template<typename T> +bool operator<(const BoolSet<T> &a, const BoolSet<T> &b) { + unsigned int t1, t2; + t1 = a.num_elem(); + t2 = b.num_elem(); + if (t1 < t2) + return true; + else if (t1 > t2) + return false; + else { + t1 = a.size(); + t2 = b.size(); + if (t1 < t2) + return true; + else if (t1 > t2) + return false; + else + for (unsigned int i = 0; i < a.set_.size(); i++) + if (a.set_[i] < b.set_[i]) + return true; + } + return false; +} + + +// +// iterator for BoolSet +// + +template<typename T> +typename BoolSet<T>::iterator BoolSet<T>::begin() { + typename BoolSet<T>::iterator it(this, 0); + if (size_ == 0) + return it; + else if (set_[0] & static_cast<T>(1)) + return it; + else + return ++it; +} + + +template<typename T> +typename BoolSet<T>::iterator BoolSet<T>::end() { + return typename BoolSet<T>::iterator(this, size_); +} + + +template<typename T> +typename BoolSet<T>::const_iterator BoolSet<T>::begin() const { + typename BoolSet<T>::const_iterator it(this, 0); + if (size_ == 0) + return it; + else if (set_[0] & static_cast<T>(1)) + return it; + else + return ++it; +} + + +template<typename T> +typename BoolSet<T>::const_iterator BoolSet<T>::end() const { + return typename BoolSet<T>::const_iterator(this, size_); +} + + +template<typename T> +class BoolSet<T>::iterator: public std::iterator<std::forward_iterator_tag, T> { +protected: + BoolSet<T> *s_; + unsigned int pos_; + +protected: + iterator(BoolSet<T> *s, unsigned int pos) { s_ = s; pos_ = pos; } + +public: + ~iterator() {} + + typename BoolSet<T>::iterator &operator++(); + typename BoolSet<T>::iterator operator++(int); + typename BoolSet<T>::iterator operator+(int) const; + unsigned int operator*() const; + bool operator==(const BoolSet<T>::iterator &) const; + bool operator!=(const BoolSet<T>::iterator &) const; + operator typename BoolSet<T>::const_iterator(); + + friend class BoolSet<T>; +}; + + +template<typename T> +typename BoolSet<T>::iterator &BoolSet<T>::iterator::operator++() { + assert(pos_ < s_->size_); + + pos_++; + unsigned int n = pos_ / (sizeof(T)*8); + unsigned int r = pos_ % (sizeof(T)*8); + while (pos_ < s_->size_) { + if (s_->set_[n] == static_cast<T>(0)) { + pos_ += sizeof(T)*8-r; + n++; + r = 0; + if (pos_ >= s_->size_) + break; + } + + if (r == 0) { + while (pos_ < s_->size_) { + if (s_->set_[n] == static_cast<T>(0)) { + pos_ += sizeof(T)*8; + n++; + } + else + break; + } + if (pos_ >= s_->size_) + break; + } + + for (unsigned int i = r; i < sizeof(T)*8; i++) + if (s_->set_[n] & static_cast<T>(1) << i) { + pos_ = pos_+i-r; + return *this; + } + + pos_ += sizeof(T)*8-r; + n++; + r = 0; + } + + pos_ = s_->size_; + return *this; +} + + +template<typename T> +typename BoolSet<T>::iterator BoolSet<T>::iterator::operator++(int) { + typename BoolSet<T>::iterator it(*this); + ++(*this); + return it; +} + + +template<typename T> +typename BoolSet<T>::iterator BoolSet<T>::iterator::operator+(int n) const { + assert(n >= 0); + typename BoolSet<T>::iterator it(*this); + while (n > 0) { + ++it; + --n; + } + return it; +} + + +template<typename T> +unsigned int BoolSet<T>::iterator::operator*() const { + assert(pos_ < s_->size_); + return pos_; +} + + +template<typename T> +bool BoolSet<T>::iterator::operator==(const BoolSet<T>::iterator &other) const { + return s_ == other.s_ && pos_ == other.pos_; +} + + +template<typename T> +bool BoolSet<T>::iterator::operator!=(const BoolSet<T>::iterator &other) const { + return !((*this) == other); +} + + +template<typename T> +BoolSet<T>::iterator::operator typename BoolSet<T>::const_iterator() { + return BoolSet<T>::const_iterator(s_, pos_); +} + + +template<typename T> +class BoolSet<T>::const_iterator: public std::iterator<std::forward_iterator_tag, T> { +protected: + const BoolSet<T> *s_; + unsigned int pos_; + +protected: + const_iterator(const BoolSet<T> *s, unsigned int pos) { s_ = s; pos_ = pos; } + +public: + ~const_iterator() {} + + typename BoolSet<T>::const_iterator &operator++(); + typename BoolSet<T>::const_iterator operator++(int); + typename BoolSet<T>::const_iterator operator+(int) const; + unsigned int operator*() const; + bool operator==(const BoolSet<T>::const_iterator &) const; + bool operator!=(const BoolSet<T>::const_iterator &) const; + + friend class BoolSet<T>; +}; + + +template<typename T> +typename BoolSet<T>::const_iterator &BoolSet<T>::const_iterator::operator++() { + assert(pos_ < s_->size_); + + pos_++; + unsigned int n = pos_ / (sizeof(T)*8); + unsigned int r = pos_ % (sizeof(T)*8); + while (pos_ < s_->size_) { + if (s_->set_[n] == static_cast<T>(0)) { + pos_ += sizeof(T)*8-r; + n++; + r = 0; + if (pos_ >= s_->size_) + break; + } + + if (r == 0) { + while (pos_ < s_->size_) { + if (s_->set_[n] == static_cast<T>(0)) { + pos_ += sizeof(T)*8; + n++; + } + else + break; + } + if (pos_ >= s_->size_) + break; + } + + for (unsigned int i = r; i < sizeof(T)*8; i++) + if (s_->set_[n] & static_cast<T>(1) << i) { + pos_ = pos_+i-r; + return *this; + } + + pos_ += sizeof(T)*8-r; + n++; + r = 0; + } + + pos_ = s_->size_; + return *this; +} + + +template<typename T> +typename BoolSet<T>::const_iterator BoolSet<T>::const_iterator::operator++(int) { + typename BoolSet<T>::const_iterator it(*this); + ++(*this); + return it; +} + + +template<typename T> +typename BoolSet<T>::const_iterator BoolSet<T>::const_iterator::operator+(int n) const { + assert(n >= 0); + typename BoolSet<T>::const_iterator it(*this); + while (n > 0) { + ++it; + --n; + } + return it; +} + + +template<typename T> +unsigned int BoolSet<T>::const_iterator::operator*() const { + assert(pos_ < s_->size_); + return pos_; +} + + +template<typename T> +bool BoolSet<T>::const_iterator::operator==(const BoolSet<T>::const_iterator &other) const { + return s_ == other.s_ && pos_ == other.pos_; +} + + +template<typename T> +bool BoolSet<T>::const_iterator::operator!=(const BoolSet<T>::const_iterator &other) const { + return !((*this) == other); +} + +} + +#endif diff --git a/lib/omega/include/basic/Collection.h b/lib/omega/include/basic/Collection.h new file mode 100644 index 0000000..80ddf48 --- /dev/null +++ b/lib/omega/include/basic/Collection.h @@ -0,0 +1,43 @@ +#if !defined Already_Included_Collection +#define Already_Included_Collection + +namespace omega { + +template<class T> class Iterator; +template<class T> class Any_Iterator; + + +//! protocol for any kind of collection +template<class T> class Collection { +public: + virtual Iterator<T> *new_iterator() = 0; + virtual Any_Iterator<T> any_iterator() { return Any_Iterator<T>(new_iterator()); } + + virtual int size() const = 0; +}; + + +/*! + * protocol for collections whose elements are ordered + * by the way they are entered into the collection, and + * whose elements can be accessed by "index" + * + * note that the implementation need not be a linked list + */ +template<class T> class Sequence : public Collection<T> { +public: + virtual const T &operator[](int) const = 0; + virtual T &operator[](int) = 0; + + /*! Y in X --> X[X.index(Y)] == Y */ + virtual int index(const T &) const = 0; }; + +} // namespace + +#define instantiate_Collection(T) template class Collection<T>; \ + instantiate_Any_Iterator(T) +#define instantiate_Sequence(T) template class Sequence<T>; \ + instantiate_Collection(T) + +#endif + diff --git a/lib/omega/include/basic/Collections.h b/lib/omega/include/basic/Collections.h new file mode 100644 index 0000000..1e68031 --- /dev/null +++ b/lib/omega/include/basic/Collections.h @@ -0,0 +1,12 @@ +#if !defined Already_Included_Collections +#define Already_Included_Collections + +#include <stdio.h> +#include <basic/Collection.h> +#include <basic/Iterator.h> +#include <basic/List.h> +#include <basic/Bag.h> +#include <basic/Map.h> + +#endif + diff --git a/lib/omega/include/basic/ConstString.h b/lib/omega/include/basic/ConstString.h new file mode 100644 index 0000000..f149c9d --- /dev/null +++ b/lib/omega/include/basic/ConstString.h @@ -0,0 +1,57 @@ +#if ! defined _Const_String_h +#define _Const_String_h 1 + +#include <string> + +namespace omega { + +// should be inside Const_String, but I can't get it to +// compile the hashTable when it is: hashTable can't be +// global, but if it and its size are static to Const_String, +// the compiler still doesn't seem to like the definition, +// or the declaration either for that matter. +class ConstStringRep { +public: + const char *name; + int count; + ConstStringRep *nextInBucket; + ConstStringRep(const char *t); +}; + +class Const_String { +private: + ConstStringRep *rep; + void buildRep(const char *t); + +public: + Const_String(); + Const_String(const char* t); + Const_String(const std::string &s); + Const_String(const Const_String & t) {rep = t.rep;} + + operator int() const; + int null() const; + + operator const char*() const; + operator std::string() const; + int operator++(int); + int operator++(); + int operator--(int); + int operator--(); + friend int operator==(const Const_String &x, const Const_String &y); + friend int operator!=(const Const_String &x, const Const_String &y); + friend int operator<(const Const_String &x, const Const_String &y); + friend int operator >(const Const_String &x, const Const_String &y); + +}; + +#if defined SCREWED_UP_CASTING_RULES +static int operator==(const Const_String &x, const char *y) +{ return x == (Const_String) y; } +static int operator!=(const Const_String &x, const char *y) +{ return x != (Const_String) y; } +#endif + +} // namespace + +#endif diff --git a/lib/omega/include/basic/DynamicArray.h b/lib/omega/include/basic/DynamicArray.h new file mode 100644 index 0000000..08f8b91 --- /dev/null +++ b/lib/omega/include/basic/DynamicArray.h @@ -0,0 +1,318 @@ +#ifndef Already_Included_DynamicArray +#define Already_Included_DynamicArray + +#include <assert.h> + +namespace omega { + +template <class T> class DynamicArray2; +template <class T> class DynamicArray3; +template <class T> class DynamicArray4; + +template <class T, int d> class DynamicArray + { + public: + DynamicArray(DynamicArray<T,d> &D); + ~DynamicArray(); + + protected: + DynamicArray(); + bool partial; + int *bounds; + T *elements; + + void do_constr(); + void do_destruct(); + }; + + +template <class T> class DynamicArray1 : public DynamicArray<T,1> + { + public: + DynamicArray1(const char *s0 = 0); + DynamicArray1(int d0); + void resize(int d0); + T& operator[](int d); + + friend class DynamicArray2<T>; + + private: + void do_construct(int d0); + }; + + +template <class T> class DynamicArray2 : public DynamicArray<T,2> + { + public: + DynamicArray2(const char *s0 = 0, const char *s1 = 0); + DynamicArray2(int d0, int d1); + void resize(int d0, int d1); + DynamicArray1<T> operator[](int d); + + friend class DynamicArray3<T>; + + private: + void do_construct(int d0, int d1); + }; + + +template <class T> class DynamicArray3 : public DynamicArray<T,3> + { + public: + DynamicArray3(const char *s0 = 0, const char *s1 = 0, const char *s2 = 0); + DynamicArray3(int d0, int d1, int d2); + void resize(int d0, int d1, int d2); + DynamicArray2<T> operator[](int d); + + friend class DynamicArray4<T>; + + private: + void do_construct(int d0, int d1, int d2); + }; + +template <class T> class DynamicArray4 : public DynamicArray<T,4> + { + public: + DynamicArray4(const char *s0 = 0, const char *s1 = 0, const char *s2 = 0, const char *s3 = 0); + DynamicArray4(int d0, int d1, int d2, int d3); + void resize(int d0, int d1, int d2, int d3); + DynamicArray3<T> operator[](int d); + + private: + void do_construct(int d0, int d1, int d2, int d3); + }; + +} // namespace + +#define instantiate_DynamicArray1(T) template class DynamicArray1<T>; \ + template class DynamicArray<T,1>; + +#define instantiate_DynamicArray2(T) template class DynamicArray2<T>; \ + template class DynamicArray<T,2>; \ + instantiate_DynamicArray1(T); + +#define instantiate_DynamicArray3(T) template class DynamicArray3<T>; \ + template class DynamicArray<T,3>; \ + instantiate_DynamicArray2(T); + +#define instantiate_DynamicArray4(T) template class DynamicArray4<T>; \ + template class DynamicArray<T,4>; \ + instantiate_DynamicArray3(T); + +namespace omega { + +template<class T, int d> void DynamicArray<T,d>::do_constr() + { +// #if ! defined SHUT_UP_ABOUT_STATEMENT_WITH_NO_EFFECT_IN_DYNAMIC_ARRAY_CREATION +// assert(d > 0); +// #endif + bounds = 0; + elements = 0; + partial = false; + } + + +template<class T> void DynamicArray1<T>::do_construct(int d0) + { + this->bounds = new int[1]; + this->bounds[0] = d0; + this->elements = new T [d0]; + this->partial = false; + } + +template<class T> void DynamicArray2<T>::do_construct(int d0, int d1) + { + this->bounds = new int[2]; + this->bounds[0] = d0; + this->bounds[1] = d1; + this->elements = new T [d0 * d1]; + this->partial = false; + } + +template<class T> void DynamicArray3<T>::do_construct(int d0,int d1,int d2) + { + this->bounds = new int[3]; + this->bounds[0] = d0; + this->bounds[1] = d1; + this->bounds[2] = d2; + this->elements = new T [d0 * d1 * d2]; + this->partial = false; + } + +template<class T> void DynamicArray4<T>::do_construct(int d0,int d1,int d2,int d3) + { + this->bounds = new int[4]; + this->bounds[0] = d0; + this->bounds[1] = d1; + this->bounds[2] = d2; + this->bounds[3] = d3; + this->elements = new T [d0 * d1 * d2 * d3]; + this->partial = false; + } + +template<class T, int d> DynamicArray<T,d>::DynamicArray() + { + do_constr(); + } + +template<class T> DynamicArray1<T>::DynamicArray1(const char *) + { + this->do_constr(); + } + +template<class T> DynamicArray2<T>::DynamicArray2(const char *,const char *) + { + this->do_constr(); + } + +template<class T> DynamicArray3<T>::DynamicArray3(const char *,const char *,const char *) + { + this->do_constr(); + } + +template<class T> DynamicArray4<T>::DynamicArray4(const char *,const char *,const char *,const char *) + { + this->do_constr(); + } + +template<class T> DynamicArray1<T>::DynamicArray1(int d0) + { + do_construct(d0); + } + +template<class T> DynamicArray2<T>::DynamicArray2(int d0, int d1) + { + do_construct(d0, d1); + } + +template<class T> DynamicArray3<T>::DynamicArray3(int d0,int d1,int d2) + { + do_construct(d0, d1, d2); + } + +template<class T> DynamicArray4<T>::DynamicArray4(int d0,int d1,int d2,int d3) + { + do_construct(d0, d1, d2, d3); + } + + +template<class T, int d> void DynamicArray<T,d>::do_destruct() + { + if (! partial) + { + delete [] bounds; + delete [] elements; + } + } + + +template<class T, int d> DynamicArray<T,d>::~DynamicArray() + { + do_destruct(); + } + + +template<class T> void DynamicArray1<T>::resize(int d0) + { + assert(!this->partial); + this->do_destruct(); + if (d0 == 0) + this->do_constr(); + else + do_construct(d0); + } + +template<class T> void DynamicArray2<T>::resize(int d0, int d1) + { + assert(!this->partial); + this->do_destruct(); + if (d0 == 0 && d1 == 0) + this->do_constr(); + else + do_construct(d0, d1); + } + +template<class T> void DynamicArray3<T>::resize(int d0, int d1, int d2) + { + assert(!this->partial); + this->do_destruct(); + if (d0 == 0 && d1 == 0 && d2 == 0) + this->do_constr(); + else + do_construct(d0, d1, d2); + } + +template<class T> void DynamicArray4<T>::resize(int d0, int d1, int d2, int d3) + { + assert(!this->partial); + this->do_destruct(); + if (d0 == 0 && d1 == 0 && d2 == 0 && d3 == 0) + this->do_constr(); + else + do_construct(d0, d1, d2, d3); + } + + +template<class T> T& DynamicArray1<T>::operator[](int d0) + { +#if !defined (NDEBUG) + assert(this->elements != 0 && "Trying to dereference undefined array"); + assert(0 <= d0 && d0 < this->bounds[0] && "Array subscript out of bounds"); +#endif + + return this->elements[d0]; + } + +template<class T> DynamicArray1<T> DynamicArray2<T>::operator[](int d0) + { +#if !defined (NDEBUG) + assert(this->elements != 0 && "Trying to dereference undefined array"); + assert(0 <= d0 && d0 < this->bounds[0] && "Array subscript out of bounds"); +#endif + + DynamicArray1<T> result; + result.bounds = this->bounds+1; + result.elements = this->elements + this->bounds[1] * d0; + result.partial = true; + return result; + } + +template<class T> DynamicArray2<T> DynamicArray3<T>::operator[](int d0) + { +#if !defined (NDEBUG) + assert(this->elements != 0 && "Trying to dereference undefined array"); + assert(0 <= d0 && d0 < this->bounds[0] && "Array subscript out of bounds"); +#endif + DynamicArray2<T> result; + result.bounds = this->bounds+1; + result.elements = this->elements + this->bounds[1] * this->bounds[2] * d0; + result.partial = true; + return result; + } + +template<class T> DynamicArray3<T> DynamicArray4<T>::operator[](int d0) + { +#if !defined (NDEBUG) + assert(this->elements != 0 && "Trying to dereference undefined array"); + assert(0 <= d0 && d0 < this->bounds[0] && "Array subscript out of bounds"); +#endif + + DynamicArray3<T> result; + result.bounds = this->bounds+1; + result.elements = this->elements + this->bounds[1] * this->bounds[2] * this->bounds[3] * d0; + result.partial = true; + return result; + } + + +template<class T, int d> + DynamicArray<T,d>::DynamicArray(DynamicArray<T,d> &D) + { + assert(D.elements != 0 && "Trying to copy an undefined array"); + partial = true; + bounds = D.bounds; + elements = D.elements; + } + +} // namespace +#endif diff --git a/lib/omega/include/basic/Iterator.h b/lib/omega/include/basic/Iterator.h new file mode 100644 index 0000000..f62874c --- /dev/null +++ b/lib/omega/include/basic/Iterator.h @@ -0,0 +1,129 @@ +/* + * Base classes for iterators, generators + * + * These don't really work yet for constant collections. + * I'm not sure how to make that happen. + */ + +#if ! defined _Iterator_h +#define _Iterator_h 1 + +#include <basic/Collection.h> + +namespace omega { + +#define foreach(x,T,S,A) do {for (omega::Any_Iterator<T> __P_##x = (S).any_iterator();__P_##x;__P_##x++) {T & x = *__P_##x; A;}} while (0) + +#define foreachSeparated(x,T,S,A,B) do {for (omega::Any_Iterator<T> __P_##x = (S).any_iterator();__P_##x;) {T & x = *__P_##x; A; __P_##x++; if (__P_##x) B;}} while (0) + +/*! + * \brief Abstract base class Iterator<type> + * + * Supports two styles of iteration: + * ~~~ + * for ( ... initialize i (typically i = collection) ... ; i ; i++ ) + * operate_on(*i) + * ~~~ + * or + * ~~~ + * for ( ... initialize i ... ; i.live() ; i.next() ) + * operate_on(i.curr()) + * ~~~ + * **IF THE COLLECTION IS CHANGED, THE ITERATOR IS NO LONGER VALID** + * + * For collections that are not "Sequence"s, the order in + * which the elements are returned may not be consistent. + */ +template<class T> class Iterator { +public: + virtual const T & operator*() const = 0; + virtual T & operator*() = 0; + + virtual void operator++(int) = 0; + virtual void operator++() = 0; + + virtual bool live() const = 0; + operator bool() const { return live(); } + + const T & curr() const { return *(*this); } + T & curr() { return *(*this); } + void next() { (*this)++; } + + virtual Iterator<T> *new_copy() const = 0; + virtual ~Iterator() {} +}; + + +//! A generator is like an iterator but it gives out values +/*! Values may or may not exist in some writable collection */ +template<class T> class Generator { +public: + virtual T operator*() const = 0; + + virtual void operator++(int) = 0; + virtual void operator++() = 0; + + virtual int live() const = 0; + operator int() const { return live(); } + + const T curr() const { return *(*this); } + T curr() { return *(*this); } + void next() { (*this)++; } +}; + + + +//! Delegate to any kind of iterator (on the heap) +/*! + * * If created via a reference, become a copy of the iterator + * * If created via a pointer, manipulate that pointer and free *p when this dies + * + * Mostly useful for Collection::iterator `Iterator::Iterator(Collection)` + */ +template<class T> class Any_Iterator : public Iterator<T> { +public: + Any_Iterator(Collection<T> &c); + Any_Iterator(const Iterator<T> &i); // copy of i + + virtual ~Any_Iterator() { delete me; } + + Any_Iterator<T> &operator=(const Any_Iterator<T> &rhs) + { delete me; me = rhs.me->new_copy(); return *this; } + + const T & operator*() const { return *(*me); } + T & operator*() { return *(*me); } + void operator++(int) { (*me)++; } + void operator++() { ++(*me); } + bool live() const { return (*me).live(); } + + Iterator<T> *new_copy() const { return new Any_Iterator<T>((*me).new_copy()); } + +private: + //! take over *p, *p MUST BE ON THE HEAP + Any_Iterator(Iterator<T> *p) { me = p; } + friend class Collection<T>; +/* + * // Couldn't make this work with g++258 + * friend Any_Iterator<T> Collection<T>::any_iterator(); + */ + Iterator<T> *me; +}; + +template <class T> inline Any_Iterator<T>::Any_Iterator(Collection<T> &c) + { + me = c.new_iterator(); + } + +template <class T> inline Any_Iterator<T>::Any_Iterator(const Iterator<T> &i) + { + me = i.new_copy(); + } + +} // namespace + +#define instantiate_Iterator(T) template class Iterator<T>; +#define instantiate_Generator(T) template class Generator<T>; +#define instantiate_Any_Iterator(T) template class Any_Iterator<T>; \ + instantiate_Iterator(T) + +#endif diff --git a/lib/omega/include/basic/Link.h b/lib/omega/include/basic/Link.h new file mode 100644 index 0000000..bdf169c --- /dev/null +++ b/lib/omega/include/basic/Link.h @@ -0,0 +1,97 @@ +#if ! defined _Link_h +#define _Link_h 1 + +#include <basic/Iterator.h> +#include <stddef.h> + +namespace omega { + +// By default, if ndebug is not set, do not do free list + +#if ! defined ListElementFreeList +#if ! defined NDEBUG || defined ASSERTIONS_ANYWAY +#define ListElementFreeList 0 +#else +#define ListElementFreeList 1 +#endif +#endif + +#if ListElementFreeList + // g++ 2.5.8 does not allow static data in template classes, so... + extern void *kludgy_List_Element_new(size_t size); + extern void kludgy_List_Element_delete(void *ptr, size_t size); +#endif +/*! + * \brief List_Element: one item in a list and the pointer to the next. + * + * Each such object should be pointed to by either exactly one + * other List_Element or by some other pointer(s), exactly one + * of which will delete the List_Element. + * ListElements should ONLY be allocated on the heap. + */ +template <class T> class List_Element { +public: +#if ListElementFreeList + void *operator new(size_t size) + { + return kludgy_List_Element_new(size); + } + void operator delete(void *ptr, size_t size) + { + kludgy_List_Element_delete(ptr, size); + } +#endif + + T head; + List_Element<T> *tail; + + List_Element() { + tail = 0; + } + List_Element(T h, List_Element<T> * t) { + head = h; + tail = t; + } + List_Element(const List_Element<T> & L) { + head = L.head; + if (L.tail) tail = new List_Element<T>(*L.tail); + else tail = 0; + } + List_Element & operator=(const List_Element<T> &L) { + if (this != &L) { + head = L.head; + if (tail) delete tail; + if (L.tail) tail = new List_Element<T>(*L.tail); + else tail = 0; + } + return *this; + } + virtual ~List_Element() { // virtual ensures 2nd arg of delete is right + delete tail; + } +}; + + + +template<class T> class List_Element_Iterator : public Iterator<T> { +public: + List_Element_Iterator(List_Element<T>* j) { i = j; } + virtual const T & operator*() const { return i->head; } + virtual T & operator*() { return i->head; } + virtual void operator++(int) { i = i->tail; } + virtual void operator++() { i = i->tail; } + virtual bool live() const { return i != 0; } + Iterator<T> * new_copy() const { return new List_Element_Iterator<T>(i);} + +protected: + List_Element<T> *i; +}; + +} // namespace + +#define instantiate_Only_List_Element(T) template class List_Element<T>; \ + template class List_Element_Iterator<T>; +#define instantiate_List_Element(T) instantiate_Only_List_Element(T)\ + instantiate_Collection(T) + +#endif diff --git a/lib/omega/include/basic/List.h b/lib/omega/include/basic/List.h new file mode 100644 index 0000000..28ab1d5 --- /dev/null +++ b/lib/omega/include/basic/List.h @@ -0,0 +1,233 @@ +#if ! defined _List_h +#define _List_h 1 + +/* + * Linked lists with an interface like a bit of libg++'s SLList class + */ +#include <stdio.h> // for NULL +#include <basic/Iterator.h> +#include <basic/Collection.h> +#include <basic/Link.h> +#include <assert.h> + +namespace omega { + +template<class T> class List_Iterator; + +// +// indexing of Lists starts at 1, index == 0 means not there +// + +template<class T> class List : public Sequence<T> { +public: + List(const List<T> &l) + { contents = l.contents ? new List_Element<T>(*l.contents) : 0; } + List() { contents = 0; } + virtual ~List() { delete contents; } + + Iterator<T> *new_iterator(); + const T &operator[](int) const; + T &operator[](int); + + int index(const T &) const; + + int size() const; + int length() const { return size(); } + bool empty() const { return size() == 0; } + + T &front() const; + +// insertion/deletion on a list invalidates any iterators +// that are on/after the element added/removed + + T remove_front(); + + void prepend(const T &item); + void append(const T &item); + void ins_after(List_Iterator<T> i, const T &item); + + void del_front(); + void del_after(List_Iterator<T> i); + void clear(); + + void join(List<T> &consumed); + +private: + friend class List_Iterator<T>; + List_Element<T> **end() + { + List_Element<T> **e = &contents; + while (*e) + e = &((*e)->tail); + return e; + } + + List_Element<T> *contents; +}; + + +template<class T> class List_Iterator : public List_Element_Iterator<T> { +public: + List_Iterator(List<T> &l); + List_Iterator(const List<T> &l); + List_Iterator(); +private: + List_Element<T> &element() { return *List_Element_Iterator<T>::i; } ; + friend class List<T>; +}; + +} // namespace + +#define instantiate_List(T) template class List<T>; \ + template class List_Iterator<T>; \ + instantiate_Only_List_Element(T) \ + instantiate_Sequence(T) + +namespace omega { + +template<class T> List_Iterator<T>::List_Iterator(List<T> &l) +: List_Element_Iterator<T>(l.contents) {} + +template<class T> List_Iterator<T>::List_Iterator(const List<T> &l) +: List_Element_Iterator<T>(l.contents) {} + +template<class T> List_Iterator<T>::List_Iterator() +: List_Element_Iterator<T>(0) {} + +template<class T> Iterator<T> *List<T>::new_iterator() +{ + return new List_Iterator<T>(*this); +} + +template<class T> const T &List<T>::operator[](int i) const +{ + assert(i > 0 && "Subscript out of bounds"); + List_Iterator<T> p(*this); + + while(--i > 0 && p) + p++; + + if (p) + return *p; + else + return *((T *)0); +} + +template<class T> T &List<T>::operator[](int i) +{ + assert(i > 0 && "Subscript out of bounds"); + List_Iterator<T> p(*this); + + while(--i > 0 && p) + p++; + + if (p) + return *p; + else + return *((T *)0); +} + +template<class T> int List<T>::index(const T &item) const +{ + List_Iterator<T> p(*this); + int i = 1; + + while(p && *p != item) + { + p++; + i++; + } + + if (p) + return i; + else + return 0; +} + +template<class T> int List<T>::size() const + { + int i = 0; + List_Element<T> * p = contents; + while (p) + { + p = p->tail; + i++; + } + return i; + } + +template<class T> T &List<T>::front() const + { + return contents->head; + } + +template<class T> T List<T>::remove_front() + { + List_Element<T> *frunt = contents; + contents = contents->tail; + T fruntT = frunt->head; + frunt->tail = 0; + delete frunt; + return fruntT; + } + +template<class T> void List<T>::prepend(const T &item) + { + contents = new List_Element<T>(item, contents); + } + + +template<class T> void List<T>::append(const T &item) + { + *(end()) = new List_Element<T>(item, 0); + } + +template<class T> void List<T>::ins_after(List_Iterator<T> i, + const T &item) + { +#if ! defined NDEBUG + for (List_Element<T> *e = contents; e != &(i.element()); e=e->tail) + { + assert(e); + } +#endif + i.element().tail = new List_Element<T>(item, i.element().tail); + } + +template<class T> void List<T>::del_front() + { + List_Element<T> *e = contents; + contents = contents->tail; + e->tail = 0; + delete e; + } + +template<class T> void List<T>::del_after(List_Iterator<T> i) + { +#if ! defined NDEBUG + for (List_Element<T> *e0 = contents; e0 != &(i.element()); e0=e0->tail) + { + assert(e0); + } +#endif + List_Element<T> *e = i.element().tail; + i.element().tail = e->tail; + e->tail = 0; + delete e; + } + +template<class T> void List<T>::clear() + { + delete contents; + contents = 0; + } + +template<class T> void List<T>::join(List<T> &consumed) + { + List_Element<T> *e = consumed.contents; + consumed.contents = 0; + *(end()) = e; + } + +} // namespace +#endif diff --git a/lib/omega/include/basic/Map.h b/lib/omega/include/basic/Map.h new file mode 100644 index 0000000..25a116d --- /dev/null +++ b/lib/omega/include/basic/Map.h @@ -0,0 +1,127 @@ +#if ! defined _Map_h +#define _Map_h 1 + +#include <basic/Link.h> +#include <stdio.h> // for NULL + +namespace omega { + +#define foreach_map(k,K,v,V,M,A) {for (omega::MapElementIterator<K,V> __M_##k = (M).iterator();__M_##k;__M_##k++) {K & k = *__M_##k; V & v = __M_##k.value(); A;}} + +template <class K, class V> class MapElement { +public: + K k; + V v; + MapElement<K,V> *tail; + MapElement(const MapElement<K,V>&); + MapElement() {} + MapElement & operator=(const MapElement<K,V>&); + ~MapElement() { delete tail; } +}; + +template<class K, class V> class MapElementIterator { +public: + MapElementIterator(MapElement<K,V>* j) { i = j;} + virtual const K & operator*() const { return i->k; } + virtual K & operator*() { return i->k;} + virtual const V & value() const { return i->v; } + virtual V & value() { return i->v; } + virtual void operator++(int) { i = i->tail; } + virtual void operator++() { i = i->tail; } + virtual bool live() const { return i != NULL; } + operator bool() const { return live(); } +protected: +MapElement<K,V> *i; +}; + +template <class K, class V> class Map { +public: +#if ! defined linux + Map(const V &default_value); +#else + // work around for '386 g++ on Linux + Map(V default_value); +#endif + ~Map(); + MapElementIterator<K,V> iterator() + {return MapElementIterator<K,V>(contents);} + int empty() const {return contents == NULL;} + V operator()(K) const; + V& operator[](K); +private: + MapElement<K,V> * contents; + V _default_value; +}; + +} // namespace + +#define instantiate_Map(T1,T2) template class Map<T1,T2>; \ + template class MapElement<T1,T2>; \ + template class MapElementIterator<T1,T2>; +#define instantiate_MapElement(T1,T2) instantiate_Map(T1,T2) +#define instantiate_MapElementIterator(T1,T2) instantiate_Map(T1,T2) + +namespace omega { + +template<class K, class V> MapElement<K,V>:: MapElement(const MapElement<K,V>& M) { + if (M.tail) tail = new MapElement<K,V>(*M.tail); + else tail = 0; + k = M.k; + v = M.v; + } + +template<class K, class V> MapElement<K,V> & + MapElement<K,V>:: operator=(const MapElement<K,V>& M) { + if (this != &M) { + if (tail) delete tail; + if (M.tail) tail = new MapElement<K,V>(*M.tail); + else tail = 0; + k = M.k; + v = M.v; + } + return *this; + } + + + + +#if ! defined linux +template <class K, class V> Map <K,V>::Map(const V &default_value) +#else +template <class K, class V> Map <K,V>::Map(V default_value) +#endif + : _default_value(default_value) + { + contents = 0; + } + +template <class K, class V> Map <K,V>::~Map() + { + delete contents; + } + +template <class K, class V> V Map<K,V>::operator()(K k) const { + MapElement <K,V> * P = contents; + while (P) { + if (P->k == k) return P->v; + P = P->tail; + }; + return _default_value; + } + +template <class K, class V> V & Map<K,V>::operator[](K k) { + MapElement <K,V> * P = contents; + while (P) { + if (P->k == k) return P->v; + P = P->tail; + }; + P = new MapElement <K,V>; + P->k = k; + P->v = _default_value; + P->tail = contents; + contents = P; + return P->v; + } + +} // namespace +#endif diff --git a/lib/omega/include/basic/Section.h b/lib/omega/include/basic/Section.h new file mode 100644 index 0000000..7a4d241 --- /dev/null +++ b/lib/omega/include/basic/Section.h @@ -0,0 +1,138 @@ +#if ! defined _Section_h +#define _Section_h 1 +/* + Section of an existing collection viewed as a collection + */ + +#include <basic/Collection.h> +#include <assert.h> + +namespace omega { + +template<class T> class Section_Iterator; + +template <class T> class Section : public Sequence<T> { +public: + Section(Sequence<T> *, int start, int length); + + Iterator<T> *new_iterator(); + + const T &operator[](int) const; + T &operator[](int); + + int index(const T &) const; + int size() const; + + friend class Section_Iterator<T>; + +private: + Sequence<T> *it; + int _start, _length; +}; + +template <class T> class Section_Iterator : public Iterator<T> { +public: + Section_Iterator(Section<T> &sec); + virtual ~Section_Iterator() { delete it; } + + const T & operator*() const { return *(*it); } + T & operator*() { return *(*it); } + + void operator++(int); + void operator++(); + + bool live() const; + Iterator<T> *new_copy() const; + +private: + Section_Iterator(const Section_Iterator<T> &si); + Iterator<T> *it; + int remaining; +}; + +} // namespace + +#define instantiate_Section(T) template class Section<T>; \ + template class Section_Iterator<T>; \ + instantiate_Sequence(T) +#define instantiate_Section_Iterator(T) instantiate_Section(T) + + +namespace omega { + +template <class T> Section<T>::Section(Sequence<T> *s, int start, int length) + { + assert(s->size() >= start-1 + length); + it = s; + _start = start; + _length = length; + } + +template <class T> Iterator<T> *Section<T>::new_iterator() + { + return new Section_Iterator<T>(*this); + } + +template <class T> const T &Section<T>::operator[](int i) const + { + assert(1 <= i && i <= size()); + return (*it)[i+(_start-1)]; + } + +template <class T> T &Section<T>::operator[](int i) + { + assert(1 <= i && i <= size()); + return (*it)[i+(_start-1)]; + } + +template <class T> int Section<T>::index(const T &var) const + { + int i; + for (i=1; i<=size(); i++) + if ((*this)[i] == var) + return i; + return 0; + } + +template <class T> int Section<T>::size() const + { + return _length; + } + + +template <class T> Section_Iterator<T>::Section_Iterator(Section<T> &sec) + { + it = sec.it->new_iterator(); + for (int i = 1; i < sec._start; i++) + (*it)++; + remaining = sec.size(); + } + + +template <class T> Section_Iterator<T>::Section_Iterator(const Section_Iterator<T> &si) : it(si.it), remaining(si.remaining) {} + + +template <class T> void Section_Iterator<T>::operator++() + { this->operator++(0); } + +template <class T> void Section_Iterator<T>::operator++(int) + { + if (remaining > 0) + { + (*it)++; + remaining--; + } + } + +template <class T> bool Section_Iterator<T>::live() const + { + return (remaining > 0); + } + +template <class T> Iterator<T> *Section_Iterator<T>::new_copy() const + { + return new Section_Iterator<T>(*this); + } + +} // namespace +#endif diff --git a/lib/omega/include/basic/SimpleList.h b/lib/omega/include/basic/SimpleList.h new file mode 100644 index 0000000..104390d --- /dev/null +++ b/lib/omega/include/basic/SimpleList.h @@ -0,0 +1,194 @@ +#if ! defined _Simple_List_h +#define _Simple_List_h 1 + +/* + * Linked lists with an interface like a bit of libg++'s SLSimple_List class + */ + +#include <assert.h> +#include <basic/Iterator.h> +#include <basic/Collection.h> +#include <basic/Link.h> + +namespace omega { + +#define Simple_List Omega_Simple_List +#define Simple_List_Iterator Omega_Simple_List_Iterator + +template<class T> class Simple_List_Iterator; + +// A TEMPORARY HACK - ERROR IF YOU TRY TO USE "INDEX" - FERD + +template<class T> class Simple_List : public Sequence<T> { +public: + Simple_List(const Simple_List<T> &l) + { contents = l.contents ? new List_Element<T>(*l.contents) : 0; } + Simple_List() { contents = 0; } + virtual ~Simple_List() { delete contents; } + + Iterator<T> *new_iterator(); + const T &operator[](int) const; + T &operator[](int); + + + int size() const; + int length() const { return size(); } + int empty() const { return size() == 0; } + + T &front() const; + +// insertion/deletion on a list invalidates any iterators +// that are on/after the element added/removed + + T remove_front(); + + void prepend(const T &item); + void append(const T &item); + + void del_front(); + void clear(); + + void join(Simple_List<T> &consumed); + + int index(const T &) const { + assert(0&&"ILLEGAL SimpleList operation\n"); + return -1; + } + +private: + friend class Simple_List_Iterator<T>; + List_Element<T> **end() + { + List_Element<T> **e = &contents; + while (*e) + e = &((*e)->tail); + return e; + } + + List_Element<T> *contents; +}; + + +template<class T> class Simple_List_Iterator : public List_Element_Iterator<T> { +public: + Simple_List_Iterator(Simple_List<T> &l); + Simple_List_Iterator(const Simple_List<T> &l); + Simple_List_Iterator(); +private: + List_Element<T> &element() { return *this->i; } ; + friend class Simple_List<T>; +}; + +} // namespace + +#define instantiate_Simple_List(T) template class Simple_List<T>; \ + template class Simple_List_Iterator<T>; \ + instantiate_Only_List_Element(T) \ + instantiate_Sequence(T) + +namespace omega { + +template<class T> Simple_List_Iterator<T>::Simple_List_Iterator(Simple_List<T> &l) +: List_Element_Iterator<T>(l.contents) {} + +template<class T> Simple_List_Iterator<T>::Simple_List_Iterator(const Simple_List<T> &l) +: List_Element_Iterator<T>(l.contents) {} + +template<class T> Simple_List_Iterator<T>::Simple_List_Iterator() +: List_Element_Iterator<T>(0) {} + +template<class T> Iterator<T> *Simple_List<T>::new_iterator() +{ + return new Simple_List_Iterator<T>(*this); +} + +template<class T> const T &Simple_List<T>::operator[](int i) const +{ + Simple_List_Iterator<T> p(*this); + + while(--i > 0 && p) + p++; + + if (p) + return *p; + else + return *((T *)0); +} + +template<class T> T &Simple_List<T>::operator[](int i) +{ + Simple_List_Iterator<T> p(*this); + + while(--i > 0 && p) + p++; + + if (p) + return *p; + else + return *((T *)0); +} + + +template<class T> int Simple_List<T>::size() const + { + int i = 0; + List_Element<T> * p = contents; + while (p) + { + p = p->tail; + i++; + } + return i; + } + +template<class T> T &Simple_List<T>::front() const + { + return contents->head; + } + +template<class T> T Simple_List<T>::remove_front() + { + List_Element<T> *frunt = contents; + contents = contents->tail; + T fruntT = frunt->head; + frunt->tail = 0; + delete frunt; + return fruntT; + } + +template<class T> void Simple_List<T>::prepend(const T &item) + { + contents = new List_Element<T>(item, contents); + } + + +template<class T> void Simple_List<T>::append(const T &item) + { + *(end()) = new List_Element<T>(item, 0); + } + + +template<class T> void Simple_List<T>::del_front() + { + List_Element<T> *e = contents; + contents = contents->tail; + e->tail = 0; + delete e; + } + + +template<class T> void Simple_List<T>::clear() + { + delete contents; + contents = 0; + } + +template<class T> void Simple_List<T>::join(Simple_List<T> &consumed) + { + List_Element<T> *e = consumed.contents; + consumed.contents = 0; + *(end()) = e; + } + +} // namespace +#endif diff --git a/lib/omega/include/basic/Tuple.h b/lib/omega/include/basic/Tuple.h new file mode 100644 index 0000000..e9aae84 --- /dev/null +++ b/lib/omega/include/basic/Tuple.h @@ -0,0 +1,336 @@ +#if !defined _Already_defined_tuple +#define _Already_defined_tuple + +#include <stdio.h> + +#include <basic/Collection.h> +#include <basic/Iterator.h> +#include <basic/util.h> + +namespace omega { + +template<class T> class Tuple_Iterator; + +// TUPLES ARE INDEXED STARTING AT 1 +// index\(i\) == 0 MEANS i IS NOT IN THE TUPLE + +template <class T> class Tuple : public Sequence<T> { +public: + Tuple(); + Tuple(int size); + Tuple (const Tuple<T>& tpl); + virtual ~Tuple(); + Tuple<T>& operator=(const Tuple<T>& tpl); + int size() const { return sz; } + int length() const { return sz; } + bool operator==(const Tuple<T> &b) const; + void reallocate(const int); + void delete_last(); + void append(const Tuple<T> &v); + void append(const T &v); + void join(Tuple<T> &v); + void clear(); + int empty() const; + + Iterator<T> *new_iterator(); + + virtual T &operator[](int index); + virtual const T &operator[](int index) const; + + int index(const T &) const; + + friend class Tuple_Iterator<T>; + +private: + int prealloc_size(const int req_size) + { return max(req_size+prealloc_pad,prealloc_min); } + int realloc_size(const int oldsize) { return 2*oldsize; } + + + int sz, alloc_sz; // Number of elements, size of allocated array + int prealloc_min,prealloc_pad; // These should be static, but that + // causes portability prob. for initialization + +protected: + T * data; +}; + +template <class T> class Tuple_Iterator : public Iterator <T> { +public: + Tuple_Iterator(const Tuple<T> &tpl); + const T & operator*() const; + T & operator*(); + void set_position(const int req_pos); + void operator++(int); + void operator++(); + void operator--(int); + void operator--(); + void set_to_last(); + void set_to_first(); +// void set_position(const int req_pos); Don't do this, compiler bug + bool live() const; + Iterator<T> *new_copy() const; + +private: + Tuple_Iterator(T * cr, T * frst, T *lst, int insz); + T * current, * lastptr, *firstptr; + int sz; +}; + +} // namespace + +#define instantiate_Tuple(T) template class Tuple<T>; \ + template class Tuple_Iterator<T>; \ + instantiate_Sequence(T) + +namespace omega { + +template<class T> T &Tuple<T>::operator[](int index) + { + assert(1 <= index && index <= sz); return data[index-1]; + } + +template<class T> const T &Tuple<T>::operator[](int index) const + { + assert(1 <= index && index <= sz); return data[index-1]; + } + + +template<class T> Tuple<T>::~Tuple() + { + if (data) + delete [] data; + } + +template<class T> Tuple<T>::Tuple() : sz(0), alloc_sz(0), + prealloc_min(20),prealloc_pad(5), data(0) +{ + // nothing needs be done + } + +template<class T> Tuple<T>::Tuple(int size) : sz(size), + prealloc_min(20),prealloc_pad(5) +{ + if (sz > 0) + { + alloc_sz = prealloc_size(sz); + data = new T[alloc_sz]; + assert(alloc_sz >= sz); + //Need some handling for out of memory. + assert (data!=0); + } + else { + alloc_sz = 0; + data = 0; + } +} + + +template<class T> Tuple<T>::Tuple(const Tuple<T>& t) + : sz(t.sz), alloc_sz(t.alloc_sz), prealloc_min(20),prealloc_pad(5) +{ + if (sz > 0) { + data = new T[alloc_sz]; + assert (data!=0); + assert (alloc_sz >= sz); + for (int i=0; i<sz; i++) + data[i] = t.data[i]; + } else { + data = 0; + alloc_sz = 0; // THis might not be 0 if it was a "clear"ed Tuple +// assert(alloc_sz == 0); + } +} + + +template<class T> Tuple<T>& Tuple<T>::operator=(const Tuple<T>& t) +{ + if (this != &t) { // Delete this + if (data) + delete [] data; + sz = t.sz; + alloc_sz = t.alloc_sz; + assert(alloc_sz >= sz); + if (sz > 0) { // Copy old + data = new T[alloc_sz]; + assert (data!=0); + for (int i=0; i<sz; i++) + data[i] = t.data[i]; + } else { + data=0; + alloc_sz = 0; // THis might not be 0 if it was a "clear"ed Tuple +// assert(alloc_sz == 0); + } + } + return *this; +} + + +template<class T> void Tuple<T>::reallocate(const int req_size) +{ + if (alloc_sz >= req_size) { // if (sz >= req_size), does this. + sz = req_size; + return; + } + alloc_sz = prealloc_size(req_size); + T* tmp_data = new T[alloc_sz]; + for(int i=0;i<sz;i++) + tmp_data[i] = data[i]; + delete [] data; + data = tmp_data; + sz = req_size; + assert(alloc_sz >= req_size); +} + +template<class T> void Tuple<T>::delete_last() +{ +assert(sz > 0); +sz --; +} + +template<class T> void Tuple<T>::append(const T &v) +{ + // Check if reallocation is necessary. + if (sz == 0) { // Empty Tuple + assert(alloc_sz >= 0); // May be nonzero for cleared tuple + + if(alloc_sz == 0) { // If it's > 1 no allocation is necessary + alloc_sz = prealloc_size(1); + data = new T[alloc_sz]; + } + assert (alloc_sz > 0 && data != 0); + } else { + if(sz == alloc_sz) { // Requires new allocation + alloc_sz = realloc_size(alloc_sz); + T * data_tmp = new T[alloc_sz]; + assert (data_tmp!=0); + assert (alloc_sz > sz); + for (int i=0; i<sz; i++) + data_tmp[i] = data[i]; + delete [] data; + data=data_tmp; + } // Otherwise big enough, no reallocation necessary + } + // Make assignment + assert(alloc_sz >= sz); + data[sz++] = v; +} + +template<class T> void Tuple<T>::append(const Tuple<T>& t) { + int old_sz = sz; + reallocate(t.size()+size()); + assert(alloc_sz >= sz); + for(int i=0; i<t.sz; i++) + data[i+old_sz] = t.data[i]; +} + +template<class T> void Tuple<T>::join(Tuple<T>& t) { + int old_sz = sz; + reallocate(t.size()+size()); + assert(alloc_sz >= sz); + for(int i=0; i<t.sz; i++) + data[i+old_sz] = t.data[i]; + t.clear(); +} + +template<class T> void Tuple<T>::clear() { if (sz) delete [] data; data = 0; alloc_sz = 0; sz = 0; } + +template<class T> int Tuple<T>::empty() const { return (sz == 0); } + +template<class T> Iterator<T> *Tuple<T>::new_iterator() +{ + return new Tuple_Iterator<T>(*this); +} + +template<class T> int Tuple<T>::index(const T & var) const +/* returns index or 0 if var isn't in the tuple */ +{ + int i; + for (i=0; i<sz; i++) + if (data[i]== var) + return i+1; + return 0; +} + +template<class T> bool Tuple<T>::operator == (const Tuple<T>& b) const +{ + int i; + if (sz != b.size()) return false; + for (i=0; i<sz; i++) + if (!(data[i] == b[i+1])) return false; + return true; +} + +/* class Tuple_Iterator */ + +template<class T> Tuple_Iterator<T>::Tuple_Iterator(const Tuple<T> &tpl) : +current(tpl.data), lastptr(tpl.data+tpl.sz-1), firstptr(tpl.data), sz(tpl.sz) +{ +} + +template<class T> Tuple_Iterator<T>::Tuple_Iterator(T * cr, T *frst, T * lst, + int insz) + : current(cr), lastptr(lst), firstptr(frst), sz(insz) +{ +} + +template<class T> const T & Tuple_Iterator<T>::operator*() const +{ + assert (current<=lastptr && current>=firstptr); + return *current; +} + +template<class T> T & Tuple_Iterator<T>::operator*() +{ + assert (current<=lastptr && current >=firstptr); + return *current; +} + +template<class T> void Tuple_Iterator<T>::operator++(int) +{ + current++; +} + +template<class T> void Tuple_Iterator<T>::operator++() +{ + current++; +} + +template<class T> void Tuple_Iterator<T>::operator--(int) +{ + current--; +} + +template<class T> void Tuple_Iterator<T>::operator--() +{ + current--; +} + +template<class T> void Tuple_Iterator<T>::set_to_last() +{ + current = lastptr; +} + +template<class T> void Tuple_Iterator<T>::set_to_first() +{ + current = firstptr; +} + +template<class T> void Tuple_Iterator<T>::set_position(const int req_pos) +{ + assert(req_pos <= sz && 1 <= req_pos); + current = firstptr + (req_pos - 1); +} + + +template<class T> bool Tuple_Iterator<T>::live() const +{ + return (current !=0 && current<=lastptr && current >= firstptr); +} + +template<class T> Iterator<T> *Tuple_Iterator<T>::new_copy() const { + return new Tuple_Iterator<T>(current, firstptr, lastptr, sz); +} + +} // namespace +#endif diff --git a/lib/omega/include/basic/omega_error.h b/lib/omega/include/basic/omega_error.h new file mode 100644 index 0000000..e342efb --- /dev/null +++ b/lib/omega/include/basic/omega_error.h @@ -0,0 +1,14 @@ +#ifndef OMEGA_ERROR_H +#define OMEGA_ERROR_H + +namespace omega { + +struct presburger_error: public std::runtime_error { + presburger_error(const std::string &msg): std::runtime_error("presburger error: " + msg) {} +}; + + + +} +#endif + diff --git a/lib/omega/include/basic/util.h b/lib/omega/include/basic/util.h new file mode 100644 index 0000000..4e807cd --- /dev/null +++ b/lib/omega/include/basic/util.h @@ -0,0 +1,263 @@ +#if ! defined Already_Included_Util +#define Already_Included_Util + +#include <stdio.h> +#include <stdlib.h> +#include <assert.h> +#include <string> +#include <sstream> +#include <stdexcept> + +namespace omega { + +#define LONG_LONG_COEF 1 + +#if LONG_LONG_COEF +#if defined BOGUS_LONG_DOUBLE_COEF +typedef long double coef_t; // type of coefficients +#define coef_fmt "%llf" +#define posInfinity (1e+24) +#define negInfinity (-1e+24) +#else +#ifdef WIN32 +typedef _int64 coef_t; // type of coefficients +#else +typedef long long coef_t; +#endif +#define coef_fmt "%lld" +#define posInfinity (0x7ffffffffffffffLL) +#define negInfinity (-0x7ffffffffffffffLL) +#endif +#else +typedef int coef_t; // type of coefficients +#define coef_fmt "%d" +#define posInfinity (0x7ffffff) +#define negInfinity (-0x7ffffff) +#endif + + +template<typename T> inline const T& max(const T &x, const T &y) { + if (x >= y) return x; else return y; +} + + +template<typename T> inline const T& max(const T &x, const T &y, const T &z) { + return max(x, max(y, z)); +} + +template<typename T> inline const T& min(const T &x, const T &y) { + if (x <= y) return x; else return y; +} + +template<typename T> inline const T& min(const T &x, const T &y, const T &z) { + return min(x, min(y, z)); +} + +template<class T> inline void set_max(T &m, const T &x) { + if (m < x) m = x; +} + +template<class T> inline void set_min(T &m, const T &x) { + if (m > x) m = x; +} + +/* template<class T> inline void swap(T &i, T &j) { */ +/* T tmp; */ +/* tmp = i; */ +/* i = j; */ +/* j = tmp; */ +/* } */ + +/* template<class T> inline T copy(const T &t) { return t; } */ + + +/* inline coef_t check_pos_mul(coef_t x, coef_t y) { */ +/* if (y >= 48051280 && y < posInfinity) */ +/* fprintf(stderr, "%d %d\n", x, y); */ +/* /\* #if !defined NDEBUG *\/ */ +/* /\* if (x != 0) *\/ */ +/* /\* assert(((MAXINT)/4) / x > y); *\/ */ +/* /\* #elif defined STILL_CHECK_MULT *\/ */ +/* /\* if (x != 0 && !(((MAXINT)/4) / x > y)) { *\/ */ +/* /\* assert(0&&"Integer overflow during multiplication (util.h)"); *\/ */ +/* /\* } *\/ */ +/* /\* #endif *\/ */ +/* #if !defined NDEBUG */ +/* if (x != 0 && y != 0) */ +/* assert(x*y > 0); */ +/* #elif defined STILL_CHECK_MULT */ +/* if (x != 0 && y != 0 && x*y < 0) */ +/* assert(0&&"Integer overflow during multiplication (util.h)"); */ +/* #endif */ +/* return x * y; */ +/* } */ + + +/* inline int */ +/* check_pos_mul(int x, int y) { */ +/* #if !defined NDEBUG */ +/* if (x != 0) */ +/* assert(((posInfinity)/4) / x > y); */ +/* #elif defined STILL_CHECK_MULT */ +/* if (x != 0 && !(((posInfinity)/4) / x > y)) { */ +/* assert(0&&"Integer overflow during multiplication (util.h)"); */ +/* } */ +/* #endif */ +/* return x * y; */ +/* } */ + +/* inline LONGLONG */ +/* check_pos_mul(LONGLONG x, LONGLONG y) { */ +/* #if !defined NDEBUG */ +/* if (x != 0) */ +/* assert(((posInfinity)/4) / x > y); */ +/* #elif defined STILL_CHECK_MULT */ +/* if (x != 0 && !(((posInfinity)/4) / x > y)) { */ +/* assert(0&&"Integer overflow during multiplication (util.h)"); */ +/* } */ +/* #endif */ +/* return x * y; */ +/* } */ + +/* inline LONGLONG abs(LONGLONG c) { return (c>=0?c:(-c)); } */ + +template<typename T> inline T check_mul(const T &x, const T &y) { +#if defined NDEBUG && ! defined STILL_CHECK_MULT + return x*y; +#else + if (x == 0 || y == 0) + return 0; + + T z = x*y; + int sign_x = (x>0)?1:-1; + int sign_y = (y>0)?1:-1; + int sign_z = (z>0)?1:-1; + + if (sign_x * sign_y != sign_z) + throw std::overflow_error("coefficient multiply overflow"); + + return z; + + /* if (x > 0) { */ + /* if (y > 0) { */ + /* assert(x*y > 0); */ + /* } */ + /* else */ + /* assert(x*y < 0); */ + /* } */ + /* else { */ + /* if (y > 0) */ + /* assert(x*y < 0); */ + /* else */ + /* assert(x*y > 0); */ + /* } */ + /* return x*y; */ +#endif +} + +template<typename T> inline T abs(const T &v) { + return (v >= static_cast<T>(0))?v:-v; +} + +template<class T> inline T int_div(const T &a, const T &b) { + T result; + assert(b > 0); + if (a>0) result = a/b; + else result = -((-a+b-1)/b); + return result; +} + +template<class T> inline T int_mod(const T &a, const T &b) { + return a-b*int_div(a,b); +} + +template<class T> inline T int_mod_hat(const T &a, const T &b) { + T r; + assert(b > 0); + r = a-b*int_div(a,b); + if (r > -(r-b)) r -= b; + return r; +} + +template<typename T> inline T gcd(T b, T a) {/* First argument is non-negative */ + assert(a >= 0); + assert(b >= 0); + if (b == 1) + return (1); + while (b != 0) { + T t = b; + b = a % b; + a = t; + } + return (a); +} + +template<typename T> inline T lcm(T b, T a) { /* First argument is non-negative */ + assert(a >= 0); + assert(b >= 0); + return check_mul(a/gcd(a,b), b); +} + +template<typename T> T square_root(const T &n, T precision = 1) { + T guess = 1; + + while (true) { + T next_guess = 0.5*(guess+n/guess); + if (abs(next_guess-guess) <= precision) + return next_guess; + else + guess = next_guess; + } +} + +template<typename T> T factor(const T &n) { + assert(n >= 0); + if (n == 1) return 1; + + static int prime[30] = {2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, 89, 97, 101, 103, 107, 109, 113}; + + if (n <= 113*113) { + for (int i = 0; i < 30; i++) + if (n % static_cast<T>(prime[i]) == 0) + return static_cast<T>(prime[i]); + + return n; + } + + T i = 1; + T k = 2; + T x = static_cast<T>(rand())%n; + T y = x; + while(i < square_root<float>(n, 1)) { + i++; + x = (x*x-1) % n; + T d = gcd(abs(y-x), n); + if(d != 1 && d != n) + return factor(d); + if(i == k) { + y = x; + k *= 2; + } + } + return n; +} + +/* #define implies(A,B) (A==(A&B)) */ + +template<typename T> std::string to_string(const T &t) { + std::ostringstream ss; + ss << t; + return ss.str(); +} + +template<typename T> T from_string(const std::string &s) { + std::istringstream ss(s); + ss.exceptions(std::ios::failbit); + T t; + ss >> t; + return t; +} + +} // namespace + +#endif diff --git a/lib/omega/include/omega.h b/lib/omega/include/omega.h new file mode 100644 index 0000000..8aa2c08 --- /dev/null +++ b/lib/omega/include/omega.h @@ -0,0 +1,71 @@ +/********************************************************************* + Old license information from the Omega Project, updated one can be + found in LICENSE file. + + Copyright (C) 1994-1996 by the Omega Project + All rights reserved. + + NOTICE: This software is provided ``as is'', without any + warranty, including any implied warranty for merchantability or + fitness for a particular purpose. Under no circumstances shall + the Omega Project or its agents be liable for any use of, misuse + of, or inability to use this software, including incidental and + consequential damages. + + License is hereby given to use, modify, and redistribute this + software, in whole or in part, for any purpose, commercial or + non-commercial, provided that the user agrees to the terms of this + copyright notice, including disclaimer of warranty, and provided + that this copyright notice, including disclaimer of warranty, is + preserved in the source code and documentation of anything derived + from this software. Any redistributor of this software or + anything derived from this software assumes responsibility for + ensuring that any parties to whom such a redistribution is made + are fully aware of the terms of this license and disclaimer. + + The Omega project can be contacted at omega@cs.umd.edu + or http://www.cs.umd.edu/projects/omega +*********************************************************************/ + +#ifndef Already_Included_Omega +#define Already_Included_Omega + +/* + * The presburger interface is divided into the following parts. + * These parts are all included together, but are in separate + * files to keep things organized a bit. + * + * In many files, you can include just some of the following, + * specifically: if you are building a presburger tree, just + * include "pres_tree.h"; if you are querying it, include + * "pres_dnf.d" and "pres_conj.h"; if you are doing relational + * operations, include "Relation.h" + * + * Most of the function definitions are in the .c files with + * the same name as the .h that declares them, except: + * the remap and push_exists functions are in pres_var.c + * the DNFize functions are in pres_dnf.c + * the functions involving printing are in pres_print.c + * the beautify functions are in pres_beaut.c + * the rearrange functions are in pres_rear.c + * the compression functions are in pres_cmpr.c + */ + +#include <omega/omega_core/debugging.h> +#include <omega/pres_var.h> +#include <omega/pres_cnstr.h> +#include <omega/pres_subs.h> +#include <omega/pres_form.h> +#include <omega/pres_logic.h> +#include <omega/pres_decl.h> +#include <omega/pres_quant.h> +#include <omega/pres_conj.h> +#include <omega/pres_cmpr.h> +#include <omega/Relation.h> + +#include <omega/Rel_map.h> +#include <omega/farkas.h> +#include <omega/hull.h> +#include <omega/closure.h> + +#endif diff --git a/lib/omega/include/omega/RelBody.h b/lib/omega/include/omega/RelBody.h new file mode 100644 index 0000000..3c11702 --- /dev/null +++ b/lib/omega/include/omega/RelBody.h @@ -0,0 +1,165 @@ +#if ! defined _RelBody_h +#define _RelBody_h 1 + +#include <omega/pres_form.h> +#include <omega/pres_dnf.h> + +namespace omega { + +typedef enum {under_construction, compressed, uncompressed} Rel_Body_Status; +typedef unsigned char Rel_Unknown_Uses; +const Rel_Unknown_Uses no_u = 1; +const Rel_Unknown_Uses and_u = 2; +const Rel_Unknown_Uses or_u = 4; + +// +// Relation body. +// Body and representative are separated to do reference counting. +// + +class Rel_Body : public Formula { +public: + bool is_null() const; + + inline Node_Type node_type() { return Op_Relation; } + + inline bool is_set() const { return number_output == 0; } + int n_inp() const; + int n_out() const; + int n_set() const; + + inline Variable_ID_Tuple *global_decls() { return &Symbolic; } + int max_ufs_arity(); + int max_shared_ufs_arity(); + int max_ufs_arity_of_set(); + int max_ufs_arity_of_in(); + int max_ufs_arity_of_out(); + + Variable_ID input_var(int nth); + Variable_ID output_var(int nth); + Variable_ID set_var(int nth); + Variable_ID get_local(const Variable_ID v); + Variable_ID get_local(const Global_Var_ID G); + Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of); + bool has_local(const Global_Var_ID G); + bool has_local(const Global_Var_ID G, Argument_Tuple of); + void name_input_var(int, Const_String); + void name_output_var(int, Const_String); + void name_set_var(int, Const_String); + + F_And *and_with_and(); + EQ_Handle and_with_EQ(); + EQ_Handle and_with_EQ(const Constraint_Handle &c); + GEQ_Handle and_with_GEQ(); + GEQ_Handle and_with_GEQ(const Constraint_Handle &c); + + void print(); + void print(FILE *output_file) { print(output_file, true); } + void print(FILE *output_file, bool printSym); + std::string print_variables_to_string(bool printSym); + void print_with_subs(FILE *output_file, bool printSym, bool newline); + void print_with_subs(); + std::string print_with_subs_to_string(bool printSym, bool newline); + std::string print_outputs_with_subs_to_string(); + std::string print_outputs_with_subs_to_string(int i); + std::string print_formula_to_string(); + void prefix_print(); + void prefix_print(FILE *output_file, int debug = 1); + + bool is_satisfiable(); + bool is_lower_bound_satisfiable(); + bool is_upper_bound_satisfiable(); + bool is_obvious_tautology(); + bool is_definite_tautology(); + bool is_unknown(); + DNF* query_DNF(); + DNF* query_DNF(int rdt_conjs, int rdt_constrs); + void simplify(int rdt_conjs = 0, int rdt_constrs = 0); + void finalize(); + inline bool is_finalized() { return finalized; } + inline bool is_shared() { return ref_count > 1; } + + void query_difference(Variable_ID v1, Variable_ID v2, + coef_t &lowerBound, coef_t &upperBound, + bool &quaranteed); + void query_variable_bounds(Variable_ID, coef_t &lowerBound, coef_t &upperBound); + coef_t query_variable_mod(Variable_ID v, coef_t factor); + + Relation extract_dnf_by_carried_level(int level, int direction); + void make_level_carried_to(int level); + + // these are only public to allow the creation of "null_rel" + Rel_Body(); + ~Rel_Body(); + void setup_names(); + +private: + + // These are manipulated primarily as parts of Relations + friend class Relation; + friend_rel_ops; + + friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel); + + Rel_Unknown_Uses unknown_uses(); + + inline bool is_simplified() const { return (simplified_DNF!=NULL && get_children().empty()); } + bool is_compressed(); + Conjunct *rm_first_conjunct(); + Conjunct *single_conjunct(); + bool has_single_conjunct(); + + void beautify(); + void rearrange(); + + friend class EQ_Handle; // these set up names for printing + friend class GEQ_Handle; // and check if simplified + friend class Constraint_Handle; // and update coefficients + + void compress(); + void uncompress(); + + void interpret_unknown_as_true(); + void interpret_unknown_as_false(); + + Rel_Body(int n_input, int n_output); + /* Rel_Body(Rel_Body *r); */ + Rel_Body(Rel_Body *r, Conjunct *c); + Rel_Body &operator=(Rel_Body &r); + Rel_Body *clone(); + + inline Formula *formula() { return children().front(); } + inline Formula *rm_formula() { return children().remove_front(); } + bool can_add_child(); + + void reverse_leading_dir_info(); + void invalidate_leading_info(int changed = -1) { Formula::invalidate_leading_info(changed); } + void enforce_leading_info(int guaranteed, int possible, int dir) { Formula::enforce_leading_info(guaranteed, possible, dir); } + // re-declare this so that Relation (a friend) can call it + + DNF* DNFize(); + void DNF_to_formula(); + + Conjunct *find_available_conjunct(); + F_And *find_available_And(); + + +/* === data === */ +private: + + int ref_count; + Rel_Body_Status status; + + int number_input, number_output; + Tuple<Const_String> In_Names, Out_Names; + Variable_ID_Tuple Symbolic; + + DNF* simplified_DNF; + short r_conjs; // are redundant conjuncts eliminated? + bool finalized; + bool _is_set; +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/Rel_map.h b/lib/omega/include/omega/Rel_map.h new file mode 100644 index 0000000..5641cb3 --- /dev/null +++ b/lib/omega/include/omega/Rel_map.h @@ -0,0 +1,161 @@ +#if ! defined _Rel_map_h +#define _Rel_map_h 1 + +#include <omega/pres_gen.h> +#include <omega/pres_var.h> + +namespace omega { + +// +// Mapping for relations +// When a relation operation needs to re-arrange the variables, +// it describes the re-arragement with a mapping, and then calls +// align to re-arrange them. +// +// In a mapping, map_in (map_out/map_set) gives the new type and +// position of each of the old input (output/set) variables. +// For variables being mapped to Input, Output, or Set variables, +// the position is the new position in the tuple. +// For variables being mapped to Exists_Var, Forall_Var, or +// Wildcard_Var, the positions can be used to map multiple +// variables to the same quantified variable, by providing +// the same position. Each variable with a negative position +// is given a unique quantified variable that is NOT listed +// in the seen_exists_ids list. +// I'm not sure what the positions mean for Global_Vars - perhaps +// they are ignored? +// +// Currently, align seems to support only mapping to Set, Input, +// Output, and Exists vars. +// + +class Mapping { +public: + inline Mapping(int no_in, int no_out): n_input(no_in), n_output(no_out) {} + inline Mapping(int no_set): n_input(no_set), n_output(0){} + inline Mapping(const Mapping &m): n_input(m.n_input), n_output(m.n_output) { + int i; + for(i=1; i<=n_input; i++) map_in_kind[i] = m.map_in_kind[i]; + for(i=1; i<=n_input; i++) map_in_pos[i] = m.map_in_pos[i]; + for(i=1; i<=n_output;i++) map_out_kind[i] = m.map_out_kind[i]; + for(i=1; i<=n_output;i++) map_out_pos[i] = m.map_out_pos[i]; + } + + inline void set_map (Var_Kind in_kind, int pos, Var_Kind type, int map) { + if(in_kind==Input_Var) + set_map_in(pos,type,map); + else if(in_kind==Set_Var) + set_map_in(pos,type,map); + else if(in_kind==Output_Var) + set_map_out(pos,type,map); + else + assert(0); + } + + inline void set_map_in (int pos, Var_Kind type, int map) { + assert(pos>=1 && pos<=n_input); + map_in_kind[pos] = type; + map_in_pos[pos] = map; + } + inline void set_map_set (int pos, Var_Kind type, int map) { + assert(pos>=1 && pos<=n_input); + map_in_kind[pos] = type; + map_in_pos[pos] = map; + } + + inline void set_map_out(int pos, Var_Kind type, int map) { + assert(pos>=1 && pos<=n_output); + map_out_kind[pos] = type; + map_out_pos[pos] = map; + } + + inline Var_Kind get_map_in_kind(int pos) const { + assert(pos>=1 && pos<=n_input); + return map_in_kind[pos]; + } + + inline int get_map_in_pos(int pos) const { + assert(pos>=1 && pos<=n_input); + return map_in_pos[pos]; + } + + inline Var_Kind get_map_out_kind(int pos) const { + assert(pos>=1 && pos<=n_output); + return map_out_kind[pos]; + } + + inline int get_map_out_pos(int pos) const { + assert(pos>=1 && pos<=n_output); + return map_out_pos[pos]; + } + + inline int n_in() const { return n_input; } + inline int n_out() const { return n_output; } + + // If a tuple as a whole becomes the new Input or Output tuple, + // return the Tuple of they will become (Input, Output) + // Return Unknown_Tuple otherwise + + inline Argument_Tuple get_tuple_fate(Argument_Tuple t, int prefix = -1) const { + return t== Input_Tuple ? get_input_fate(prefix) : + (t==Output_Tuple ? get_output_fate(prefix) : Unknown_Tuple); } + + inline Argument_Tuple get_set_fate(int prefix = -1) const { + return get_input_fate(prefix); } + + inline Argument_Tuple get_input_fate(int prefix = -1) const { + if (prefix < 0) prefix = n_input; + assert(n_input >= prefix); + if (n_input < prefix) + return Unknown_Tuple; + Var_Kind vf = map_in_kind[1]; + for (int i = 1; i<=prefix; i++) + if (map_in_pos[i]!=i || map_in_kind[i]!=vf) + return Unknown_Tuple; + + return vf == Input_Var ? Input_Tuple + : vf == Set_Var ? Set_Tuple + : vf == Output_Var ? Output_Tuple + : Unknown_Tuple; + } + + inline Argument_Tuple get_output_fate(int prefix = -1) const { + if (prefix < 0) prefix = n_output; + assert(n_output >= prefix); + if (n_output < 1) + return Unknown_Tuple; + Var_Kind vf = map_out_kind[1]; + for (int i = 1; i<=prefix; i++) + if (map_out_pos[i]!=i || map_out_kind[i]!=vf) + return Unknown_Tuple; + return vf == Input_Var ? Input_Tuple + : vf == Set_Var ? Set_Tuple + : vf == Output_Var ? Output_Tuple + : Unknown_Tuple; + } + + inline static Mapping Identity(int inp, int outp) { + Mapping m(inp, outp); int i; + for(i=1; i<=m.n_input; i++) m.set_map(Input_Var, i, Input_Var, i); + for(i=1; i<=m.n_output;i++) m.set_map(Output_Var, i, Output_Var, i); + return m; + } + + inline static Mapping Identity(int setvars) { + Mapping m(setvars); int i; + for(i=1; i<=setvars; i++) m.set_map(Set_Var, i, Set_Var, i); + return m; + } + +private: + int n_input; + int n_output; + Var_Kind map_in_kind[maxVars]; + int map_in_pos[maxVars]; + Var_Kind map_out_kind[maxVars]; + int map_out_pos[maxVars]; +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/Relation.h b/lib/omega/include/omega/Relation.h new file mode 100644 index 0000000..b41bef5 --- /dev/null +++ b/lib/omega/include/omega/Relation.h @@ -0,0 +1,299 @@ +#if ! defined _Relation_h +#define _Relation_h 1 + +#include <omega/RelBody.h> +#include <omega/pres_cnstr.h> +#include <iostream> +#include <limits.h> + +namespace omega { + +// +// Relation representative. +// Body and representative are separated to do reference counting. +// +class Relation { +public: + Relation(); + + Relation(int n_input, int n_output = 0); + Relation(const Relation &r); + Relation(const Relation &r, Conjunct *c); + Relation &operator=(const Relation &r); + Relation(Rel_Body &r, int foo); + + static Relation Null(); + static Relation Empty(const Relation &R); + static Relation True(const Relation &R); + static Relation True(int setvars); + static Relation True(int in, int out); + static Relation False(const Relation &R); + static Relation False(int setvars); + static Relation False(int in, int out); + static Relation Unknown(const Relation &R); + static Relation Unknown(int setvars); + static Relation Unknown(int in, int out); + + + bool is_null() const; + + ~Relation(); + + inline F_Forall *add_forall() + { return rel_body->add_forall(); } + inline F_Exists *add_exists() + { return rel_body->add_exists(); } + inline F_And *add_and() + { return rel_body->add_and(); } + inline F_And *and_with() + { return rel_body->and_with(); } + inline F_Or *add_or() + { return rel_body->add_or(); } + inline F_Not *add_not() + { return rel_body->add_not(); } + inline void finalize() + { rel_body->finalize(); } + inline bool is_finalized() const + { return rel_body->finalized; } + inline bool is_set() const + { return rel_body->is_set(); } + inline int n_inp() const + { return rel_body->n_inp(); } + inline int n_out() const + { return rel_body->n_out(); } + inline int n_set() const + { return rel_body->n_set(); } + + inline const Variable_ID_Tuple *global_decls() const + { return rel_body->global_decls(); } + inline int max_ufs_arity() const + { return rel_body->max_ufs_arity(); } + inline int max_ufs_arity_of_in() const + { return rel_body->max_ufs_arity_of_in(); } + inline int max_ufs_arity_of_set() const + { return rel_body->max_ufs_arity_of_set(); } + inline int max_ufs_arity_of_out() const + { return rel_body->max_ufs_arity_of_out(); } + inline int max_shared_ufs_arity() const + { return rel_body->max_shared_ufs_arity(); } + + inline Variable_ID input_var(int nth) + { return rel_body->input_var(nth); } + inline Variable_ID output_var(int nth) + { return rel_body->output_var(nth); } + inline Variable_ID set_var(int nth) + { return rel_body->set_var(nth); } + inline bool has_local(const Global_Var_ID G) + { return rel_body->has_local(G); } + inline bool has_local(const Global_Var_ID G, Argument_Tuple of) + { return rel_body->has_local(G, of); } + inline Variable_ID get_local(const Variable_ID v) + { return split()->get_local(v); } + inline Variable_ID get_local(const Global_Var_ID G) + { return split()->get_local(G); } + inline Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of) + { return split()->get_local(G, of); } + + inline void name_input_var(int nth, Const_String S) + { split()->name_input_var(nth, S); } + inline void name_output_var(int nth, Const_String S) + { split()->name_output_var(nth, S); } + inline void name_set_var(int nth, Const_String S) + { split()->name_set_var(nth, S); } + + + inline F_And *and_with_and() + { return split()->and_with_and(); } + inline EQ_Handle and_with_EQ() + { return split()->and_with_EQ(); } + inline EQ_Handle and_with_EQ(const Constraint_Handle &c) + { return split()->and_with_EQ(c); } + inline GEQ_Handle and_with_GEQ() + { return split()->and_with_GEQ(); } + inline GEQ_Handle and_with_GEQ(const Constraint_Handle &c) + { return split()->and_with_GEQ(c); } + + inline void print() + { rel_body->print(); } + inline void print(FILE *output_file) + { rel_body->print(output_file); } + inline void print_with_subs() + { rel_body->print_with_subs(); } + inline void print_with_subs(FILE *output_file, bool printSym=false, + bool newline=true) + { rel_body->print_with_subs(output_file, printSym, newline); } + inline std::string print_with_subs_to_string(bool printSym=false, + bool newline=true) + { return rel_body->print_with_subs_to_string(printSym, newline); } + inline std::string print_outputs_with_subs_to_string() + { return rel_body->print_outputs_with_subs_to_string(); } + inline std::string print_outputs_with_subs_to_string(int i) + { return rel_body->print_outputs_with_subs_to_string(i); } + inline void prefix_print() + { rel_body->prefix_print(); } + inline void prefix_print(FILE *output_file, int debug = 1) + { rel_body->prefix_print(output_file, debug); } + inline std::string print_formula_to_string() { + return rel_body->print_formula_to_string(); + } + void dimensions(int & ndim_all, int &ndim_domain); + + inline bool is_lower_bound_satisfiable() + { return rel_body->is_lower_bound_satisfiable(); } + inline bool is_upper_bound_satisfiable() + { return rel_body->is_upper_bound_satisfiable(); } + inline bool is_satisfiable() + { return rel_body->is_satisfiable(); } + + inline bool is_tautology() + { return rel_body->is_obvious_tautology(); } // for compatibility + inline bool is_obvious_tautology() + { return rel_body->is_obvious_tautology(); } + inline bool is_definite_tautology() + { return rel_body->is_definite_tautology(); } + + // return x s.t. forall conjuncts c, c has >= x leading 0s + // for set, return -1 (pass this in, in case there are no conjuncts + inline int number_of_conjuncts() + { return rel_body->query_DNF()->length(); } + + // return x s.t. forall conjuncts c, c has >= x leading 0s + // for set, return -1 (pass this in, in case there are no conjuncts + inline int query_guaranteed_leading_0s() + { return rel_body->query_DNF()->query_guaranteed_leading_0s(this->is_set() ? -1 : 0); } + + // return x s.t. forall conjuncts c, c has <= x leading 0s + // if no conjuncts return min of input and output tuple sizes, or -1 if relation is a set + inline int query_possible_leading_0s() + { return rel_body->query_DNF()->query_possible_leading_0s( + this->is_set()? -1 : min(n_inp(),n_out())); } + + // return +-1 according to sign of leading dir, or 0 if we don't know + inline int query_leading_dir() + { return rel_body->query_DNF()->query_leading_dir(); } + + inline DNF* query_DNF() + { return rel_body->query_DNF(); } + inline DNF* query_DNF(int rdt_conjs, int rdt_constrs) + { return rel_body->query_DNF(rdt_conjs, rdt_constrs); } + inline void simplify(int rdt_conjs = 0, int rdt_constrs = 0) + { rel_body->simplify(rdt_conjs, rdt_constrs); } + inline bool is_simplified() + { return rel_body->is_simplified(); } + inline bool is_compressed() const + { return rel_body->is_compressed(); } + inline Conjunct *rm_first_conjunct() + { return rel_body->rm_first_conjunct(); } + inline Conjunct *single_conjunct() + { return rel_body->single_conjunct(); } + inline bool has_single_conjunct() + { return rel_body->has_single_conjunct(); } + + + void query_difference(Variable_ID v1, Variable_ID v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed) { + rel_body->query_difference(v1, v2, lowerBound, upperBound, guaranteed); + } + void query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound) { + rel_body->query_variable_bounds(v,lowerBound,upperBound); + } + coef_t query_variable_mod(Variable_ID v, coef_t factor) { + assert(factor > 0); + return rel_body->query_variable_mod(v, factor); + } + int query_variable_mod(Variable_ID v, int factor) { + assert(sizeof(int) <= sizeof(coef_t)); + coef_t result = rel_body->query_variable_mod(v, static_cast<coef_t>(factor)); + if (result == posInfinity) + return INT_MAX; + else + return static_cast<int>(result); + } + + + inline void make_level_carried_to(int level) + { + split()->make_level_carried_to(level); + } + + inline Relation extract_dnf_by_carried_level(int level, int direction) + { + return split()->extract_dnf_by_carried_level(level, direction); + } + + inline void compress() + { +#if defined(INCLUDE_COMPRESSION) + split()->compress(); +#endif + } + void uncompress() + { rel_body->uncompress(); } + + inline bool is_exact() const + { return !(rel_body->unknown_uses() & (and_u | or_u)) ; } + inline bool is_inexact() const + { return !is_exact(); } + inline bool is_unknown() const + { return rel_body->is_unknown(); } + inline Rel_Unknown_Uses unknown_uses() const + { return rel_body->unknown_uses(); } + + void setup_names() {rel_body->setup_names();} + void copy_names(const Relation &r) { + copy_names(*r.rel_body); + }; + void copy_names(Rel_Body &r); + +private: + // Functions that have to create sets from relations: + friend class Rel_Body; + friend_rel_ops; + + + Rel_Body *split(); + + DNF* simplified_DNF() { + simplify(); + return rel_body->simplified_DNF; + }; + + inline void invalidate_leading_info(int changed = -1) + { split()->invalidate_leading_info(changed); } + inline void enforce_leading_info(int guaranteed, int possible, int dir) + { + split()->enforce_leading_info(guaranteed, possible, dir); + } + + + void makeSet(); + void markAsSet(); + void markAsRelation(); + + friend bool operator==(const Relation &, const Relation &); + + void reverse_leading_dir_info() + { split()->reverse_leading_dir_info(); } + void interpret_unknown_as_true() + { split()->interpret_unknown_as_true(); } + void interpret_unknown_as_false() + { split()->interpret_unknown_as_false(); } + + + Rel_Body *rel_body; + + + friend Relation merge_rels(Tuple<Relation> &R, const Tuple<std::map<Variable_ID, std::pair<Var_Kind, int> > > &mapping, const Tuple<bool> &inverse, Combine_Type ctype, int number_input, int number_output); +}; + +inline std::ostream & operator<<(std::ostream &o, Relation &R) +{ + return o << R.print_with_subs_to_string(); +} + +Relation copy(const Relation &r); + +} // namespace + +#include <omega/Relations.h> + +#endif diff --git a/lib/omega/include/omega/Relations.h b/lib/omega/include/omega/Relations.h new file mode 100644 index 0000000..4fd81e6 --- /dev/null +++ b/lib/omega/include/omega/Relations.h @@ -0,0 +1,88 @@ +#if ! defined _Relations_h +#define _Relations_h 1 + +#include <map> +#include <omega/Relation.h> + +namespace omega { + +// UPDATE friend_rel_ops IN pres_gen.h WHEN ADDING TO THIS LIST +// REMEMBER TO TAKE OUT DEFAULT ARGUMENTS IN THAT FILE + +/* The following allows us to avoid warnings about passing + temporaries as non-const references. This is useful but + has suddenly become illegal. */ +Relation consume_and_regurgitate(NOT_CONST Relation &R); + +// +// Operations over relations +// +Relation Union(NOT_CONST Relation &r1, NOT_CONST Relation &r2); +Relation Intersection(NOT_CONST Relation &r1, NOT_CONST Relation &r2); +Relation Extend_Domain(NOT_CONST Relation &R); +Relation Extend_Domain(NOT_CONST Relation &R, int more); +Relation Extend_Range(NOT_CONST Relation &R); +Relation Extend_Range(NOT_CONST Relation &R, int more); +Relation Extend_Set(NOT_CONST Relation &R); +Relation Extend_Set(NOT_CONST Relation &R, int more); +Relation Restrict_Domain(NOT_CONST Relation &r1, NOT_CONST Relation &r2); // Takes set as 2nd +Relation Restrict_Range(NOT_CONST Relation &r1, NOT_CONST Relation &r2); // Takes set as 2nd +Relation Domain(NOT_CONST Relation &r); // Returns set +Relation Range(NOT_CONST Relation &r); // Returns set +Relation Cross_Product(NOT_CONST Relation &A, NOT_CONST Relation &B); // Takes two sets +Relation Inverse(NOT_CONST Relation &r); +Relation After(NOT_CONST Relation &r, int carried_by, int new_output,int dir=1); +Relation Deltas(NOT_CONST Relation &R); // Returns set +Relation Deltas(NOT_CONST Relation &R, int eq_no); // Returns set +Relation DeltasToRelation(NOT_CONST Relation &R, int n_input, int n_output); +Relation Complement(NOT_CONST Relation &r); +Relation Project(NOT_CONST Relation &R, Global_Var_ID v); +Relation Project(NOT_CONST Relation &r, int pos, Var_Kind vkind); +Relation Project(NOT_CONST Relation &S, Variable_ID v); +Relation Project(NOT_CONST Relation &S, Sequence<Variable_ID> &s); +Relation Project_Sym(NOT_CONST Relation &R); +Relation Project_On_Sym(NOT_CONST Relation &R, + NOT_CONST Relation &context = Relation::Null()); +Relation GistSingleConjunct(NOT_CONST Relation &R, NOT_CONST Relation &R2, int effort=0); +Relation Gist(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort=0); +Relation Difference(NOT_CONST Relation &r1, NOT_CONST Relation &r2); +Relation Approximate(NOT_CONST Relation &R, bool strides_allowed = false); +Relation Identity(int n_inp); +Relation Identity(NOT_CONST Relation &r); +bool Must_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); +bool Might_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); +// May is the same as might, just another name +bool May_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); +bool Is_Obvious_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); +Relation Composition(NOT_CONST Relation &F, NOT_CONST Relation &G); +bool prepare_relations_for_composition(Relation &F, Relation &G); +Relation Join(NOT_CONST Relation &G, NOT_CONST Relation &F); +Relation EQs_to_GEQs(NOT_CONST Relation &, bool excludeStrides=false); +Relation Symbolic_Solution(NOT_CONST Relation &S); +Relation Symbolic_Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); +Relation Sample_Solution(NOT_CONST Relation &S); +Relation Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); +Relation Upper_Bound(NOT_CONST Relation &r); +Relation Lower_Bound(NOT_CONST Relation &r); + +Relation merge_rels(Tuple<Relation> &R, const Tuple<std::map<Variable_ID, std::pair<Var_Kind, int> > > &mapping, const Tuple<bool> &inverse, Combine_Type ctype, int number_input = -1, int number_output = -1); + +// The followings might retire in the futrue!!! +void MapRel1(Relation &inputRel, + const Mapping &map, + Combine_Type ctype, + int number_input=-1, int number_output=-1, + bool invalidate_resulting_leading_info = true, + bool finalize = true); +Relation MapAndCombineRel2(Relation &R1, Relation &R2, + const Mapping &mapping1, const Mapping &mapping2, + Combine_Type ctype, + int number_input=-1, int number_output=-1); +void align(Rel_Body *originalr, Rel_Body *newr, F_Exists *fe, + Formula *f, const Mapping &mapping, bool &newrIsSet, + List<int> &seen_exists, + Variable_ID_Tuple &seen_exists_ids); + +} // namespace + +#endif diff --git a/lib/omega/include/omega/closure.h b/lib/omega/include/omega/closure.h new file mode 100644 index 0000000..67088dd --- /dev/null +++ b/lib/omega/include/omega/closure.h @@ -0,0 +1,31 @@ +#if ! defined _closure_h +#define _closure_h + +#include <omega/Relation.h> + +namespace omega { + +Relation VennDiagramForm( + Tuple<Relation> &Rs, + NOT_CONST Relation &Context_In); +Relation VennDiagramForm( + NOT_CONST Relation &R_In, + NOT_CONST Relation &Context_In = Relation::Null()); + +// Given a Relation R, returns a relation deltas +// that correspond to the ConicHull of the detlas of R +Relation ConicClosure (NOT_CONST Relation &R); + +Relation TransitiveClosure (NOT_CONST Relation &r, + int maxExpansion = 1, + NOT_CONST Relation &IterationSpace=Relation::Null()); + +/* Tomasz Klimek */ +Relation calculateTransitiveClosure(NOT_CONST Relation &r); + +/* Tomasz Klimek */ +Relation ApproxClosure(NOT_CONST Relation &r); + +} // namespace + +#endif diff --git a/lib/omega/include/omega/evac.h b/lib/omega/include/omega/evac.h new file mode 100644 index 0000000..a561f8c --- /dev/null +++ b/lib/omega/include/omega/evac.h @@ -0,0 +1,15 @@ +#if defined STUDY_EVACUATIONS + +namespace omega { + +// study the evacuation from one side of C to the other for UFS's of +// arity up to max_arity +extern void study_evacuation(Conjunct *C, which_way dir, int max_arity); + +// study the evacuation from the joined C2's output and C1's input to +// either of the other possible tuples +extern void study_evacuation(Conjunct *C1, Conjunct *C2, int max_arity); + +} // namespace + +#endif diff --git a/lib/omega/include/omega/farkas.h b/lib/omega/include/omega/farkas.h new file mode 100644 index 0000000..e77ed66 --- /dev/null +++ b/lib/omega/include/omega/farkas.h @@ -0,0 +1,19 @@ +#ifndef Already_Included_Affine_Closure +#define Already_Included_Affine_Closure + +#include <omega/Relation.h> + +namespace omega { + +enum Farkas_Type {Basic_Farkas, Decoupled_Farkas, + Linear_Combination_Farkas, Positive_Combination_Farkas, + Affine_Combination_Farkas, Convex_Combination_Farkas }; + +Relation Farkas(NOT_CONST Relation &R, Farkas_Type op, bool early_bailout = false); + +extern coef_t farkasDifficulty; +extern Global_Var_ID coefficient_of_constant_term; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/hull.h b/lib/omega/include/omega/hull.h new file mode 100644 index 0000000..928d0c6 --- /dev/null +++ b/lib/omega/include/omega/hull.h @@ -0,0 +1,89 @@ +#ifndef Already_Included_Hull +#define Already_Included_Hull + +#include <omega/farkas.h> + +namespace omega { + +Relation SimpleHull(const Relation &R, bool allow_stride_constraint = false, bool allow_irregular_constraint = false); +Relation SimpleHull(const std::vector<Relation> &Rs, bool allow_stride_constraint = false, bool allow_irregular_constraint = false); + + +// All of the following first call approximate on R to +// eliminate any wildcards and strides. + +// x in Convex Hull of R +// iff +// exist a_i, y_i s.t. +// x = Sum_i a_i y_i s.t. +// forall i, y_i in R +// forall i, a_i >=0 +// sum_i a_i = 1 +Relation ConvexHull(NOT_CONST Relation &R); + +// DecoupledConvexHull is the same as ConvexHull, +// except that it only finds constraints that involve +// both variables x&y if there is a constraint +// that involves both x&y in one of the conjuncts +// of R. +Relation DecoupledConvexHull(NOT_CONST Relation &R); + +// The affine hull just consists of equality constraints +// but is otherwise the tightest hull on R. +// x in Affine Hull of R +// iff +// exist a_i, y_i s.t. +// x = Sum_i a_i y_i s.t. +// forall i, y_i in R +// sum_i a_i = 1 +Relation AffineHull(NOT_CONST Relation &R); + +// x in Linear Hull of R +// iff +// exist a_i, y_i s.t. +// x = Sum_i a_i y_i s.t. +// forall i, y_i in R +Relation LinearHull(NOT_CONST Relation &R); + +// The conic hull is the tighest cone that contains R +// x in Conic Hull of R. +// iff +// exist a_i, y_i s.t. +// x = Sum_i a_i y_i s.t. +// forall i, y_i in R +// forall i, a_i >=0 +Relation ConicHull(NOT_CONST Relation &R); + +// RectHull includes readily-available constraints from relation +// that can be part of hull, plus rectangular bounds calculated +// from input/output/set variables' range. +Relation RectHull(NOT_CONST Relation &Rel); + +// A constraint is in the result of QuickHull only if it appears in one of +// the relations and is directly implied by a single constraint in each of +// the other relations. +Relation QuickHull(Relation &R); // deprecated +Relation QuickHull(Tuple<Relation> &Rs); // deprecated + +Relation FastTightHull(NOT_CONST Relation &input_R, + NOT_CONST Relation &input_H); +Relation Hull(NOT_CONST Relation &R, + bool stridesAllowed = false, + int effort=1, + NOT_CONST Relation &knownHull = Relation::Null() + ); +Relation Hull(Tuple<Relation> &Rs, + const std::vector<bool> &validMask, + int effort = 1, + bool stridesAllowed = false, + NOT_CONST Relation &knownHull = Relation::Null()); + +// If a union of several conjuncts is a convex, their union +// representaition can be simplified by their convex hull. +Relation ConvexRepresentation(NOT_CONST Relation &R); +Relation CheckForConvexPairs(NOT_CONST Relation &S); // deprecated +Relation CheckForConvexRepresentation(NOT_CONST Relation &R_In); // deprecated + +} + +#endif diff --git a/lib/omega/include/omega/omega_core/debugging.h b/lib/omega/include/omega/omega_core/debugging.h new file mode 100644 index 0000000..e217ae9 --- /dev/null +++ b/lib/omega/include/omega/omega_core/debugging.h @@ -0,0 +1,30 @@ +#if !defined(Already_included_debugging) +#define Already_included_debugging + +// Debugging flags. Can set any of these. + +#include <stdio.h> +#include <ctype.h> + +namespace omega { + + + +extern int omega_core_debug; +extern int pres_debug; +extern int relation_debug; +extern int closure_presburger_debug; +extern int hull_debug; +extern int farkas_debug; +extern int code_gen_debug; + +enum negation_control { any_negation, one_geq_or_eq, one_geq_or_stride }; +extern negation_control pres_legal_negations; + +#if defined STUDY_EVACUATIONS +extern int evac_debug; +#endif + +} // namespace + +#endif diff --git a/lib/omega/include/omega/omega_core/oc.h b/lib/omega/include/omega/omega_core/oc.h new file mode 100644 index 0000000..e4f5444 --- /dev/null +++ b/lib/omega/include/omega/omega_core/oc.h @@ -0,0 +1,350 @@ +#ifndef Already_Included_OC +#define Already_Included_OC 1 + +#include <stdio.h> +#include <string> +#include <basic/util.h> +#include <omega/omega_core/debugging.h> +#include <basic/Tuple.h> + +namespace omega { + +// Manu:: commented the line below -- fortran bug workaround +//#define maxVars 256 /* original 56, increased by chun */ +#define maxVars 100 + +extern int maxGEQs; +extern int maxEQs; + +// Manu:: commented the lines below -- fortran bug workaround +//const int maxmaxGEQs = 2048; // original 512, increaded by chun +//const int maxmaxEQs = 512; // original 256, increased by chun +const int maxmaxGEQs = 512; +const int maxmaxEQs = 256; + +/* #if ! defined maxmaxGEQs */ +/* #define maxmaxGEQs 2048 /\* original 512, increaded by chun *\/ */ +/* #endif */ +/* #if ! defined maxmaxEQs */ +/* #define maxmaxEQs 512 /\* original 256, increased by chun *\/ */ +/* #endif */ + + +#if 0 +#if ! defined Already_Included_Portable +typedef unsigned char bool; /* what a gross thing to do */ +#endif +#endif + +typedef int EqnKey; + +enum {EQ_BLACK = 0, EQ_RED = 1}; +enum {OC_SOLVE_UNKNOWN = 2, OC_SOLVE_SIMPLIFY = 3}; + +struct eqn { + EqnKey key; + coef_t touched; // see oc_simple.c + int color; + int essential; + int varCount; + coef_t coef[maxVars + 1]; +}; + +// typedef eqn * Eqn; +enum redType {notRed=0, redEQ, redGEQ, redLEQ, redStride}; +enum redCheck {noRed=0, redFalse, redConstraints}; +enum normalizeReturnType {normalize_false, normalize_uncoupled, + normalize_coupled}; + +extern char wildName[200][20]; + +extern FILE *outputFile; /* printProblem writes its output to this file */ +#define doTrace (trace && TRACE) +#define isRed(e) (desiredResult == OC_SOLVE_SIMPLIFY && (e)->color) +// #define eqnncpy(e1,e2,s) {int *p00,*q00,*r00; p00 = (int *)(e1); q00 = (int *)(e2); r00 = &p00[headerWords+1+s]; while(p00 < r00) *p00++ = *q00++; } +// #define eqncpy(e1,e2) eqnncpy(e1,e2,nVars) +// #define eqnnzero(e,s) {int *p00,*r00; p00 = (int *)(e); r00 = &p00[headerWords+1+(s)]; while(p00 < r00) *p00++ = 0;} +// #define eqnzero(e) eqnnzero(e,nVars) + +//void eqnncpy(eqn *dest, eqn *src, int); +//void eqnnzero(eqn *e, int); + +inline void eqnncpy(eqn *dest, eqn *src, int nVars) { + dest->key = src->key; + dest->touched = src->touched; + dest->color = src->color; + dest->essential = src->essential; + dest->varCount = src->varCount; + for (int i = 0; i <= nVars; i++) + dest->coef[i] = src->coef[i]; +} + + +inline void eqnnzero(eqn *e, int nVars) { + e->key = 0; + e->touched = 0; + e->color = EQ_BLACK; + e->essential = 0; + e->varCount = 0; + for (int i = 0; i <= nVars; i++) + e->coef[i] = 0; +} + +extern int mayBeRed; + +#ifdef SPEED +#define TRACE 0 +#define DBUG 0 +#define DEBUG 0 +#else +#define TRACE (omega_core_debug) +#define DBUG (omega_core_debug > 1) +#define DEBUG (omega_core_debug > 2) +#endif + + +class Memory { +public: + int length; + coef_t stride; + redType kind; + coef_t constantTerm; + coef_t coef[maxVars + 1]; + int var[maxVars + 1]; +}; + +/* #define headerWords ((4*sizeof(int) + sizeof(coef_t))/sizeof(int)) */ + +void check_number_EQs(int); +void check_number_GEQs(int); +extern eqn SUBs[]; +extern Memory redMemory[]; + +class Problem { +public: + short nVars, safeVars; + short nEQs, nGEQs,nSUBs,nMemories,allocEQs,allocGEQs; + short varsOfInterest; + bool variablesInitialized; + bool variablesFreed; + short var[maxVars+2]; + short forwardingAddress[maxVars+2]; + // int variableColor[maxVars+2]; + int hashVersion; + const char *(*get_var_name)(unsigned int var, void *args); + void *getVarNameArgs; + eqn *GEQs; + eqn *EQs; + bool isTemporary; + + Problem(int in_eqs=0, int in_geqs=0); + Problem(const Problem &); + ~Problem(); + Problem & operator=(const Problem &); + +/* Allocation parameters and functions */ + + static const int min_alloc,first_alloc_pad; + int padEQs(int oldalloc, int newreq) { + check_number_EQs(newreq); + return min((newreq < 2*oldalloc ? 2*oldalloc : 2*newreq),maxmaxEQs); + } + int padGEQs(int oldalloc, int newreq) { + check_number_GEQs(newreq); + return min((newreq < 2*oldalloc ? 2*oldalloc : 2*newreq),maxmaxGEQs); + } + int padEQs(int newreq) { + check_number_EQs(newreq); + return min(max(newreq+first_alloc_pad,min_alloc), maxmaxEQs); + } + int padGEQs(int newreq) { + check_number_GEQs(newreq); + return min(max(newreq+first_alloc_pad,min_alloc), maxmaxGEQs); + } + + + void zeroVariable(int i); + + void putVariablesInStandardOrder(); + void noteEssential(int onlyWildcards); + int findDifference(int e, int &v1, int &v2); + int chainKill(int color,int onlyWildcards); + + int newGEQ(); + int newEQ(); + int newSUB(){ + return nSUBs++; + } + + + void initializeProblem(); + void initializeVariables() const; + void printProblem(int debug = 1) const; + void printSub(int v) const; + std::string print_sub_to_string(int v) const; + void clearSubs(); + void printRedEquations() const; + int countRedEquations() const; + int countRedGEQs() const; + int countRedEQs() const; + int countRedSUBs() const; + void difficulty(int &numberNZs, coef_t &maxMinAbsCoef, coef_t &sumMinAbsCoef) const; + int prettyPrintProblem() const; + std::string prettyPrintProblemToString() const; + int prettyPrintRedEquations() const; + int simplifyProblem(int verify, int subs, int redundantElimination); + int simplifyProblem(); + int simplifyAndVerifyProblem(); + int simplifyApproximate(bool strides_allowed); + void coalesce(); + void partialElimination(); + void unprotectVariable(int var); + void negateGEQ(int); + void convertEQstoGEQs(bool excludeStrides); + void convertEQtoGEQs(int eq); + void nameWildcard(int i); + void useWildNames(); + void ordered_elimination(int symbolic); + int eliminateRedundant (bool expensive); + void eliminateRed(bool expensive); + void constrainVariableSign(int color, int var, int sign); + void constrainVariableValue(int color, int var, int value); + void query_difference(int v1, int v2, coef_t &lowerBound, coef_t &upperBound, bool &guaranteed); + int solve(int desiredResult); + std::string print_term_to_string(const eqn *e, int c) const; + void printTerm(const eqn * e, int c) const; + std::string printEqnToString(const eqn * e, int test, int extra) const; + void sprintEqn(char *str, const eqn * e, int is_geq,int extra) const; + void printEqn(const eqn * e, int is_geq, int extra) const; + void printEQ(const eqn *e) const {printEqn(e,0,0); } + std::string print_EQ_to_string(const eqn *e) const {return printEqnToString(e,0,0);} + std::string print_GEQ_to_string(const eqn *e) const {return printEqnToString(e,1,0);} + void printGEQ(const eqn *e) const {printEqn(e,1,0); } + void printGEQextra(const eqn *e) const {printEqn(e,1,1); } + void printSubstitution(int s) const; + void printVars(int debug = 1) const; + void swapVars(int i, int j); + void reverseProtectedVariables(); + redCheck redSimplifyProblem(int effort, int computeGist); + + // calculate value of variable mod integer from set of equations -- by chun 12/14/2006 + coef_t query_variable_mod(int v, coef_t factor, int color=EQ_BLACK, int nModularEQs=0, int nModularVars=0) const; + coef_t query_variable_mod(int v, coef_t factor, int color, int nModularEQs, int nModularVars, Tuple<bool> &working_on) const; // helper function + + int queryVariable(int i, coef_t *lowerBound, coef_t *upperBound); + int query_variable_bounds(int i, coef_t *l, coef_t *u); + void queryCoupledVariable(int i, coef_t *l, coef_t *u, int *couldBeZero, coef_t lowerBound, coef_t upperBound); + int queryVariableSigns(int i, int dd_lt, int dd_eq, int dd_gt, coef_t lowerBound, coef_t upperBound, bool *distKnown, coef_t *dist); + void addingEqualityConstraint(int e); + normalizeReturnType normalize(); + void normalize_ext(); + void cleanoutWildcards(); + void substitute(eqn *sub, int i, coef_t c); + void deleteVariable( int i); + void deleteBlack(); + int addNewProtectedWildcard(); + int addNewUnprotectedWildcard(); + int protectWildcard( int i); + void doMod( coef_t factor, int e, int j); + void freeEliminations( int fv); + int verifyProblem(); + void resurrectSubs(); + int solveEQ(); + int combineToTighten() ; + int quickKill(int onlyWildcards, bool desperate = false); + int expensiveEqualityCheck(); + int expensiveRedKill(); + int expensiveKill(); + int smoothWeirdEquations(); + void quickRedKill(int computeGist); + void chainUnprotect(); + void freeRedEliminations(); + void doElimination( int e, int i); + void analyzeElimination( + int &v, + int &darkConstraints, + int &darkShadowFeasible, + int &unit, + coef_t ¶llelSplinters, + coef_t &disjointSplinters, + coef_t &lbSplinters, + coef_t &ubSplinters, + int ¶llelLB); + int parallelSplinter(int e, int diff, int desiredResult); + int solveGEQ( int desiredResult); + void setInternals(); + void setExternals(); + int reduceProblem(); + void problem_merge(Problem &); + void deleteRed(); + void turnRedBlack(); + void checkGistInvariant() const; + void check() const; + coef_t checkSum() const; + void rememberRedConstraint(eqn *e, redType type, coef_t stride); + void recallRedMemories(); + void simplifyStrideConstraints(); + const char * orgVariable(int i) const { + return ((i == 0) ? // cfront likes this form better + "1" : + ((i < 0) ? + wildName[-i] : + (*get_var_name)(i,getVarNameArgs))); + }; + const char * variable(int i) const { + return orgVariable(var[i]) ; + }; + + void deleteGEQ(int e) { + if (DEBUG) { + fprintf(outputFile,"Deleting %d (last:%d): ",e,nGEQs-1); + printGEQ(&GEQs[e]); + fprintf(outputFile,"\n"); + }; + if (e < nGEQs-1) + eqnncpy (&GEQs[e], &GEQs[nGEQs - 1],(nVars)); + nGEQs--; + }; + void deleteEQ(int e) { + if (DEBUG) { + fprintf(outputFile,"Deleting %d (last:%d): ",e,nEQs-1); + printGEQ(&EQs[e]); + fprintf(outputFile,"\n"); + }; + if (e < nEQs-1) + eqnncpy (&EQs[e], &EQs[nEQs - 1],(nVars)); + nEQs--; + }; + +}; + + + +/* #define UNKNOWN 2 */ +/* #define SIMPLIFY 3 */ +/* #define _red 1 */ +/* #define black 0 */ + + +extern int print_in_code_gen_style; + + +void initializeOmega(void); + + +/* set extra to 0 for normal use */ +int singleVarGEQ(eqn *e); + +void setPrintLevel(int level); + +void printHeader(); + +void setOutputFile(FILE *file); + +extern void check_number_EQs(int nEQs); +extern void check_number_GEQs(int nGEQs); +extern void checkVars(int nVars); + +} // namespace + +#endif diff --git a/lib/omega/include/omega/omega_core/oc_i.h b/lib/omega/include/omega/omega_core/oc_i.h new file mode 100644 index 0000000..9533a40 --- /dev/null +++ b/lib/omega/include/omega/omega_core/oc_i.h @@ -0,0 +1,79 @@ +#if !defined(Already_included_oc_i) +#define Already_included_oc_i + +#include <basic/util.h> +#include <omega/omega_core/oc.h> +#include <stdlib.h> +#include <assert.h> +#include <string> +#include <vector> + +namespace omega { + +#define maxWildcards 18 + +extern int findingImplicitEqualities; +extern int firstCheckForRedundantEquations; +extern int use_ugly_names; +extern int doItAgain; +extern int newVar; +extern int conservative; +extern FILE *outputFile; /* printProblem writes its output to this file */ +extern int nextWildcard; +extern int trace; +extern int depth; +extern int packing[maxVars]; +extern int headerLevel; +extern int inApproximateMode; +extern int inStridesAllowedMode; +extern int addingOuterEqualities; +extern int outerColor; + +const int keyMult = 31; +const int hashTableSize =5*maxmaxGEQs; +const int maxKeys = 8*maxmaxGEQs; +extern int hashVersion; +extern eqn hashMaster[hashTableSize]; +extern int fastLookup[maxKeys*2]; +extern int nextKey; + +extern int reduceWithSubs; +extern int pleaseNoEqualitiesInSimplifiedProblems; + +#define noProblem ((Problem *) 0) + +extern Problem *originalProblem; +int checkIfSingleVar(eqn *e, int i); +/* Solve e = factor alpha for x_j and substitute */ + +void negateCoefficients(eqn * eqn, int nV); + +extern int omegaInitialized; +extern Problem full_answer, context,redProblem; + +#if defined BRAIN_DAMAGED_FREE +static inline void free(const Problem *p) +{ + free((char *)p); +} +#endif + +#if defined NDEBUG +#define CHECK_FOR_DUPLICATE_VARIABLE_NAMES +#else +#define CHECK_FOR_DUPLICATE_VARIABLE_NAMES \ + { \ + std::vector<std::string> name(nVars); \ + for(int i=1; i<=nVars; i++) { \ + name[i-1] = variable(i); \ + assert(!name[i-1].empty()); \ + for(int j=1; j<i; j++) \ + assert(!(name[i-1] == name[j-1])); \ + } \ + } +#endif + + +} // namespace + +#endif diff --git a/lib/omega/include/omega/omega_i.h b/lib/omega/include/omega/omega_i.h new file mode 100644 index 0000000..e5d9230 --- /dev/null +++ b/lib/omega/include/omega/omega_i.h @@ -0,0 +1,30 @@ +#if ! defined _omega_i_h +#define _omega_i_h 1 + +#include <omega/pres_var.h> + +namespace omega { + +/* #define Assert(c,t) if(!(c)) PresErrAssert(t) */ +/* void PresErrAssert(const char *t); */ + +extern Rel_Body null_rel; + +extern int skip_finalization_check; +// extern int skip_set_checks; + +// Global input and output variable tuples. + +extern Global_Input_Output_Tuple input_vars; +extern Global_Input_Output_Tuple output_vars; +extern Global_Input_Output_Tuple &set_vars; + +} // namespace + +#if ! defined DONT_INCLUDE_TEMPLATE_CODE +// with g++258, everything will need to make Tuple<Relation>, as a +// function taking it as an argument is a friend of lots of classes +#include <omega/Relation.h> +#endif + +#endif diff --git a/lib/omega/include/omega/pres_cmpr.h b/lib/omega/include/omega/pres_cmpr.h new file mode 100644 index 0000000..fb3e6f0 --- /dev/null +++ b/lib/omega/include/omega/pres_cmpr.h @@ -0,0 +1,49 @@ +#if ! defined _pres_cmpr_h +#define _pres_cmpr_h 1 + +#include <omega/omega_core/oc.h> + +namespace omega { + +// +// Compressed problem: rectangular non-0 cut from the big problem. +// +class Comp_Constraints { +public: + Comp_Constraints(eqn *constrs, int no_constrs, int no_vars); + void UncompressConstr(eqn *constrs, short &pn_constrs); + ~Comp_Constraints(); + bool no_constraints() const + { return n_constrs == 0; } + int n_constraints() const + { return n_constrs; } + +protected: + inline int coef_index(int e, int v) + {return e*(n_vars+1) + v;} + +private: + int n_constrs; + int n_vars; + coef_t *coefs; +}; + +class Comp_Problem { +public: + Comp_Problem(Problem *problem); + Problem *UncompressProblem(); + bool no_constraints() const + { return eqs.no_constraints() && geqs.no_constraints(); } + +private: +/* === data === */ + int _nVars, _safeVars; + const char *(*_get_var_name)(unsigned int var, void *args); + void *_getVarNameArgs; + Comp_Constraints eqs; + Comp_Constraints geqs; +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_cnstr.h b/lib/omega/include/omega/pres_cnstr.h new file mode 100644 index 0000000..7b2d98d --- /dev/null +++ b/lib/omega/include/omega/pres_cnstr.h @@ -0,0 +1,192 @@ +#if ! defined _pres_cnstr_h +#define _pres_cnstr_h 1 + +#include <omega/pres_var.h> +#include <vector> + +namespace omega { + +// +// Constraint handles +// + + + +void copy_constraint(Constraint_Handle H, const Constraint_Handle initial); + +class Constraint_Handle { +public: + Constraint_Handle() {} + virtual ~Constraint_Handle() {} + + void update_coef(Variable_ID, coef_t delta); + void update_const(coef_t delta); + coef_t get_coef(Variable_ID v) const; + coef_t get_const() const; + bool has_wildcards() const; + int max_tuple_pos() const; + int min_tuple_pos() const; + bool is_const(Variable_ID v); + bool is_const_except_for_global(Variable_ID v); + + virtual std::string print_to_string() const; + virtual std::string print_term_to_string() const; + + Variable_ID get_local(const Global_Var_ID G); + Variable_ID get_local(const Global_Var_ID G, Argument_Tuple of); + // not sure that the second one can be used in a meaningful + // way if the conjunct is in multiple relations + + void finalize(); + void multiply(int multiplier); + Rel_Body *relation() const; + + +protected: + Conjunct *c; + eqn **eqns; + int e; + + friend class Constr_Vars_Iter; + friend class Constraint_Iterator; + + Constraint_Handle(Conjunct *, eqn **, int); + +#if defined PROTECTED_DOESNT_WORK + friend class EQ_Handle; + friend class GEQ_Handle; +#endif + + void update_coef_during_simplify(Variable_ID, coef_t delta); + void update_const_during_simplify(coef_t delta); + coef_t get_const_during_simplify() const; + coef_t get_coef_during_simplify(Variable_ID v) const; + + +public: + friend class Conjunct; // assert_leading_info updates coef's + // as does move_UFS_to_input + friend class DNF; // and DNF::make_level_carried_to + + friend void copy_constraint(Constraint_Handle H, + const Constraint_Handle initial); + // copy_constraint does updates and gets at c and e + +}; + +class GEQ_Handle : public Constraint_Handle { +public: + inline GEQ_Handle() {} + + virtual std::string print_to_string() const; + virtual std::string print_term_to_string() const; + bool operator==(const Constraint_Handle &that); + + void negate(); + +private: + friend class Conjunct; + friend class GEQ_Iterator; + + GEQ_Handle(Conjunct *, int); +}; + + +class EQ_Handle : public Constraint_Handle { +public: + inline EQ_Handle() {} + + virtual std::string print_to_string() const; + virtual std::string print_term_to_string() const; + bool operator==(const Constraint_Handle &that); + +private: + friend class Conjunct; + friend class EQ_Iterator; + + EQ_Handle(Conjunct *, int); +}; + + +// +// Conjuct iterators -- for querying resulting DNF. +// +class Constraint_Iterator : public Generator<Constraint_Handle> { +public: + Constraint_Iterator(Conjunct *); + int live() const; + void operator++(int); + void operator++(); + Constraint_Handle operator* (); + Constraint_Handle operator* () const; + +private: + Conjunct *c; + int current,last; + eqn **eqns; +}; + + +class EQ_Iterator : public Generator<EQ_Handle> { +public: + EQ_Iterator(Conjunct *); + int live() const; + void operator++(int); + void operator++(); + EQ_Handle operator* (); + EQ_Handle operator* () const; + +private: + Conjunct *c; + int current, last; +}; + + +class GEQ_Iterator : public Generator<GEQ_Handle> { +public: + GEQ_Iterator(Conjunct *); + int live() const; + void operator++(int); + void operator++(); + GEQ_Handle operator* (); + GEQ_Handle operator* () const; + +private: + Conjunct *c; + int current, last; +}; + + +// +// Variables of constraint iterator. +// +struct Variable_Info { + Variable_ID var; + coef_t coef; + Variable_Info(Variable_ID _var, coef_t _coef) + { var = _var; coef = _coef; } +}; + +class Constr_Vars_Iter : public Generator<Variable_Info> { +public: + Constr_Vars_Iter(const Constraint_Handle &ch, bool _wild_only = false); + int live() const; + void operator++(int); + void operator++(); + Variable_Info operator*() const; + + Variable_ID curr_var() const; + coef_t curr_coef() const; + +private: + eqn **eqns; + int e; + Problem *prob; + Variable_ID_Tuple &vars; + bool wild_only; + int current; +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_conj.h b/lib/omega/include/omega/pres_conj.h new file mode 100644 index 0000000..ea10a2c --- /dev/null +++ b/lib/omega/include/omega/pres_conj.h @@ -0,0 +1,299 @@ +#if ! defined _pres_conj_h +#define _pres_conj_h 1 + +#include <limits.h> +#include <omega/pres_decl.h> +#include <omega/pres_logic.h> +#include <omega/pres_cnstr.h> + +namespace omega { + +// +// Conjunct +// +// About variables in Conjunct: +// All varaibles appear in exactly one declaration. +// All variables used in Conjunct are referenced in mappedVars. +// Wildcard variables are referenced both in mappedVars and in myLocals, +// since they are declared in the conjunct. +// All other variables are declared at the levels above. +// Column number is: +// in forwardingAddress in Problem if variablesInitialized is set, +// equal to position of Variable_ID in mappedVars list otherwise. +// + +class Conjunct : public F_Declaration { +public: + Constraint_Iterator constraints(); + Variable_ID_Tuple *variables(); + EQ_Iterator EQs(); + GEQ_Iterator GEQs(); + inline int n_EQs() { return problem->nEQs; } + inline int n_GEQs() { return problem->nGEQs; } + + void promise_that_ub_solutions_exist(Relation &R); + + inline Node_Type node_type() {return Op_Conjunct;} + + inline int is_true() {return problem->nEQs==0 && problem->nGEQs==0 + && exact;} + + void query_difference(Variable_ID v1, Variable_ID v2, + coef_t &lowerBound, coef_t &upperBound, bool &guaranteed); + void query_variable_bounds(Variable_ID v, coef_t &lowerBound, coef_t &upperBound); + coef_t query_variable_mod(Variable_ID v, coef_t factor); + bool query_variable_used(Variable_ID v); + + int countNonzeros() const { + int numberNZs; + coef_t maxCoef, SumAbsCoef; + problem->difficulty(numberNZs,maxCoef,SumAbsCoef); + return numberNZs; + } + + void difficulty(int &numberNZs, coef_t &maxCoef, coef_t &SumAbsCoef) const { + problem->difficulty(numberNZs,maxCoef,SumAbsCoef); + } + + int query_guaranteed_leading_0s() { + count_leading_0s(); + return guaranteed_leading_0s; + } + + int query_possible_leading_0s() { + count_leading_0s(); + return possible_leading_0s; + } + + int query_leading_dir() { + count_leading_0s(); + return leading_dir; + } + + void calculate_dimensions(Relation &R, int &ndim_all, int &ndim_domain); + int max_ufs_arity_of_set(); + int max_ufs_arity_of_in(); + int max_ufs_arity_of_out(); + + int rank(); + + ~Conjunct(); + + bool is_unknown() const; + inline bool is_exact() const { return exact;} + inline bool is_inexact() const { return !exact;} + inline void make_inexact() { exact=false;} + + +#if ! defined NDEBUG + void assert_leading_info(); +#else + void assert_leading_info() {} +#endif + + + // PRINTING FUNCTIONS + void print(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); + std::string print_to_string(int true_printed); + std::string print_EQ_to_string(eqn *e) { return problem->print_EQ_to_string(e); } + std::string print_GEQ_to_string(eqn *e) { return problem->print_GEQ_to_string(e); } + std::string print_EQ_to_string(int e) + { return problem->print_EQ_to_string(&(problem->EQs[e])); } + std::string print_GEQ_to_string(int e) + { return problem->print_GEQ_to_string(&(problem->GEQs[e])); } + std::string print_term_to_string(eqn *e) { return problem->print_term_to_string(e,1); } + std::string print_EQ_term_to_string(int e) + { return problem->print_term_to_string(&(problem->EQs[e]),1); } + std::string print_GEQ_term_to_string(int e) + { return problem->print_term_to_string(&(problem->GEQs[e]),1); } + std::string print_sub_to_string(int col) { return problem->print_sub_to_string(col); } + +private: + + inline void interpret_unknown_as_true() { exact=true;} + + friend Relation approx_closure(NOT_CONST Relation &r, int n); + + virtual Conjunct *really_conjunct(); + + + // create new constraints with all co-efficients 0 + // These are public in F_And, use them from there. + EQ_Handle add_stride(int step, int preserves_level = 0); + EQ_Handle add_EQ(int preserves_level = 0); + GEQ_Handle add_GEQ(int preserves_level = 0); + EQ_Handle add_EQ(const Constraint_Handle &c, int preserves_level = 0); + GEQ_Handle add_GEQ(const Constraint_Handle &c, int preserves_level = 0); + + friend class GEQ_Handle; + friend class EQ_Handle; + friend class Sub_Handle; + friend class Constraint_Handle; + friend class Constraint_Iterator; + friend class GEQ_Iterator; + friend class EQ_Iterator; + friend class Sub_Iterator; + friend class Constr_Vars_Iter; + + + // FUNCTIONS HAVING TO DO WITH BUILDING FORMULAS/DNFs + bool can_add_child(); + void remap(); + void beautify(); + DNF* DNFize(); + int priority(); + virtual Conjunct *find_available_conjunct(); + void finalize(); + + friend class DNF; + + + + // CREATING CONJUNCTS + Conjunct(); + Conjunct(Conjunct &); + Conjunct(Formula *, Rel_Body *); + + friend class Formula; // add_conjunct (a private function) creates Conjuncts + friend class F_Not; + friend class F_Or; + // class F_And; is a friend below + + + // VARIOUS FUNCTIONS TO CREATE / WORK WITH VARIABLES + Variable_ID declare(Const_String s); + Variable_ID declare(); + Variable_ID declare(Variable_ID v); + + friend const char *get_var_name(unsigned int, void *); + void push_exists(Variable_ID_Tuple &S); + int get_column(Variable_ID); + int find_column(Variable_ID); + int map_to_column(Variable_ID); + void combine_columns(); + void reorder(); + void reorder_for_print(bool reverseOrder=false, + int first_pass_input=0, + int first_pass_output=0, + bool sort=false); + + friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel); + + void localize_var(Variable_ID D); + + + // this creates variables in conjuncts for us: + friend int new_WC(Conjunct *nc, Problem *np); + + + // UFS/LEADING ZEROS STUFF + + void move_UFS_to_input(); + + void count_leading_0s(); + void invalidate_leading_info(int changed = -1); + void enforce_leading_info(int guaranteed, int possible, int dir); + + void reverse_leading_dir_info(); + + + + // CONJUNCT SPECIFIC STUFF + + void rm_color_constrs(); + inline int N_protected() { return problem->safeVars; } + + + void ordered_elimination(int symLen) { problem->ordered_elimination(symLen);} + void convertEQstoGEQs(bool excludeStrides); + + int cost(); + + inline Formula* copy(Formula *parent, Rel_Body *reln) + { return copy_conj_diff_relation(parent,reln); } + Conjunct* copy_conj_diff_relation(Formula *parent, Rel_Body *reln); + inline Conjunct* copy_conj_same_relation() + { return copy_conj_diff_relation(&(parent()), relation()); } + friend void internal_copy_conjunct(Conjunct* to, Conjunct* fr); + friend void copy_constraint(Constraint_Handle H, + const Constraint_Handle initial); + +#if defined STUDY_EVACUATIONS + // The core function of "evac.c" does lots of work with conjuncts: + friend bool check_subseq_n(Conjunct *c, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity, int n, bool allow_offset); + friend void assert_subbed_syms(Conjunct *c); + friend bool check_affine(Conjunct *d, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity); + friend evac study(Conjunct *C, Sequence<Variable_ID> &evac_from, Sequence<Variable_ID> &evac_to, int n_from, int n_to, int max_arity); +#endif + + // The relational ops tend to do lots of demented things to Conjuncts: + friend class Rel_Body; + friend_rel_ops; + + // F_And sometimes absorbs conjuncts + friend class F_And; + + // Various DNFize functions also get a the problem: + + friend DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak); + friend class F_Exists; + + // Substitutions are a wrapper around a low-level Problem operation + friend class Substitutions; + + // private functions to call problem functions + int simplifyProblem(); + int simplifyProblem(int verify, int subs, int redundantElimination); + int redSimplifyProblem(int effort, int computeGist); + + friend int simplify_conj(Conjunct* conj, int ver_sim, int elim_red, int color); + friend DNF* negate_conj(Conjunct* conj); + friend Conjunct* merge_conjs(Conjunct* conj1, Conjunct* conj2, + Merge_Action action, Rel_Body *body = 0); + friend void copy_conj_header(Conjunct* to, Conjunct* fr); + + + // === at last, the data === + + Variable_ID_Tuple mappedVars; + + int n_open_constraints; + bool cols_ordered; + bool simplified; + bool verified; + + int guaranteed_leading_0s; // -1 if unknown + int possible_leading_0s; // -1 if unknown + int leading_dir; // 0 if unknown, else +/- 1 + int leading_dir_valid_and_known(); + + bool exact; + + short r_constrs; // are redundant constraints eliminated? + Problem *problem; + + bool is_compressed(); + void compress(); + void uncompress(); + + friend class Comp_Problem; + Comp_Problem *comp_problem; +}; + + +/* === Misc. problem manipulation utilities === */ + +const int CantBeNegated = INT_MAX-10; +const int AvoidNegating = INT_MAX-11; + +void copy_column(Problem *tp, int to_col, + Problem *fp, int fr_col, + int start_EQ, int start_GEQ); +void zero_column(Problem *tp, int to_col, + int start_EQ, int start_GEQ, + int no_EQs, int no_GEQs); + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_decl.h b/lib/omega/include/omega/pres_decl.h new file mode 100644 index 0000000..7fec0bc --- /dev/null +++ b/lib/omega/include/omega/pres_decl.h @@ -0,0 +1,55 @@ +#if ! defined _pres_decl_h +#define _pres_decl_h 1 + +#include <omega/pres_var.h> +#include <omega/pres_form.h> +#include <basic/Section.h> + +namespace omega { + +// +// Base class for presburger formula nodes with variables +// + +class F_Declaration : public Formula { +public: + virtual Variable_ID declare(Const_String s)=0; + virtual Variable_ID declare()=0; + virtual Variable_ID declare(Variable_ID)=0; + virtual Section<Variable_ID> declare_tuple(int size); + + void finalize(); + + inline Variable_ID_Tuple &locals() {return myLocals;} + +protected: + F_Declaration(Formula *, Rel_Body *); + F_Declaration(Formula *, Rel_Body *, Variable_ID_Tuple &); + ~F_Declaration(); + + Variable_ID do_declare(Const_String s, Var_Kind var_kind); + + void prefix_print(FILE *output_file, int debug = 1); + void print(FILE *output_file); + + void setup_names(); + void setup_anonymous_wildcard_names(); + + Variable_ID_Tuple myLocals; + friend class F_Forall; // rearrange needs to access myLocals + friend class F_Or; // push_exists + +private: + virtual bool can_add_child(); + + int priority(); + + friend void align(Rel_Body *originalr, Rel_Body *newr, F_Exists *fe, + Formula *f, const Mapping &mapping, bool &newrIsSet, + List<int> &seen_exists, + Variable_ID_Tuple &seen_exists_ids); +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_dnf.h b/lib/omega/include/omega/pres_dnf.h new file mode 100644 index 0000000..93d5942 --- /dev/null +++ b/lib/omega/include/omega/pres_dnf.h @@ -0,0 +1,87 @@ +#if ! defined _pres_dnf_h +#define _pres_dnf_h 1 + +#include <omega/pres_gen.h> + +namespace omega { + +// +// Disjunctive Normal Form -- list of Conjuncts +// +class DNF { +public: + void print(FILE *out_file); + void prefix_print(FILE *out_file, int debug = 1, bool parent_names_setup=false); + + bool is_definitely_false() const; + bool is_definitely_true() const; + int length() const; + + Conjunct *single_conjunct() const; + bool has_single_conjunct() const; + Conjunct *rm_first_conjunct(); + void clear(); + int query_guaranteed_leading_0s(int what_to_return_for_empty_dnf); + int query_possible_leading_0s(int what_to_return_for_empty_dnf); + int query_leading_dir(); + +private: + // all DNFize functions need to access the dnf builders: + friend class F_And; + friend class F_Or; + friend class Conjunct; + friend DNF * negate_conj(Conjunct *); + + friend class Rel_Body; + friend_rel_ops; + + DNF(); + ~DNF(); + + DNF* copy(Rel_Body *); + + void simplify(); + void make_level_carried_to(int level); + void count_leading_0s(); + + void add_conjunct(Conjunct*); + void join_DNF(DNF*); + void rm_conjunct(Conjunct *c); + + void rm_redundant_conjs(int effort); + void rm_redundant_inexact_conjs(); + void DNF_to_formula(Formula* root); + + + friend void remap_DNF_vars(Rel_Body *new_rel, Rel_Body *old_rel); + void remap(); + + void setup_names(); + + void remove_inexact_conj(); + + // These may need to get at the conjList itself: + friend DNF* DNF_and_DNF(DNF*, DNF*); + friend DNF* DNF_and_conj(DNF*, Conjunct*); + friend DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak); + + friend class DNF_Iterator; + + List<Conjunct*> conjList; +}; + +DNF* conj_and_not_dnf(Conjunct *pos_conj, DNF *neg_conjs, bool weak=false); + +// +// DNF iterator +// +class DNF_Iterator : public List_Iterator<Conjunct*> { +public: + DNF_Iterator(DNF*dnf) : List_Iterator<Conjunct*>(dnf->conjList) {} + DNF_Iterator() {} + void curr_set(Conjunct *c) { *(*this) = c; } +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_form.h b/lib/omega/include/omega/pres_form.h new file mode 100644 index 0000000..ed3258e --- /dev/null +++ b/lib/omega/include/omega/pres_form.h @@ -0,0 +1,112 @@ +#if ! defined _pres_form_h +#define _pres_form_h 1 + +#include <omega/pres_gen.h> + +namespace omega { + +typedef enum {Op_Relation, Op_Not, Op_And, Op_Or, + Op_Conjunct, Op_Forall, Op_Exists} Node_Type; + + +// +// Presburger Formula base class +// + +class Formula { +public: + virtual Node_Type node_type()=0; + + F_Forall *add_forall(); + F_Exists *add_exists(); + virtual F_And *and_with(); + F_And *add_and(); + F_Or *add_or(); + F_Not *add_not(); + void add_unknown(); + + virtual void finalize(); + virtual void print(FILE *output_file); + + Rel_Body *relation() { return myRelation; } + +protected: + virtual ~Formula(); +private: + Formula(Formula *, Rel_Body *); + + // The relational operations need to work with formula trees + friend class Relation; + friend_rel_ops; + // as do the functions that build DNF's + friend class DNF; + // or other parts of the tree + friend class Conjunct; + friend class F_Declaration; + friend class F_Exists; + friend class F_Forall; + friend class F_Or; + friend class F_And; + friend class F_Not; + friend class Rel_Body; + + + // Operations needed for manipulation of formula trees: + + void remove_child(Formula *); + void replace_child(Formula *child, Formula *new_child); + virtual bool can_add_child(); + void add_child(Formula *); + + Conjunct *add_conjunct(); + virtual Conjunct *find_available_conjunct() = 0; + + virtual Formula *copy(Formula *parent, Rel_Body *reln); + F_Exists *add_exists(Variable_ID_Tuple &S); + virtual void push_exists(Variable_ID_Tuple &S); + + // Accessor functions for tree building + + List<Formula*> &children() {return myChildren;} + int n_children() const {return myChildren.length();} + const List<Formula*> &get_children() const {return myChildren;} + Formula &parent() {return *myParent;} + void set_parent(Formula *p) {myParent = p;} + + + virtual int priority(); + + void verify_tree(); // should be const, but iterators are used + + virtual void reverse_leading_dir_info(); + virtual void invalidate_leading_info(int changed = -1); + virtual void enforce_leading_info(int guaranteed, int possible, int dir); + + virtual void remap(); + virtual DNF* DNFize() = 0; + virtual void beautify(); + virtual void rearrange(); + virtual void setup_names(); + + virtual void print_separator(FILE *output_file); + virtual void combine_columns(); + virtual void prefix_print(FILE *output_file, int debug = 1); + void print_head(FILE *output_file); + + void set_relation(Rel_Body *r); + void set_parent(Formula *parent, Rel_Body *reln); + + void assert_not_finalized(); + + virtual Conjunct *really_conjunct(); // until we get RTTI + +private: + List<Formula*> myChildren; + Formula *myParent; + Rel_Body *myRelation; + +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_gen.h b/lib/omega/include/omega/pres_gen.h new file mode 100644 index 0000000..ba6a793 --- /dev/null +++ b/lib/omega/include/omega/pres_gen.h @@ -0,0 +1,192 @@ +#if ! defined _pres_gen_h +#define _pres_gen_h 1 + +#include <omega/omega_core/oc.h> +#include <basic/ConstString.h> +#include <basic/Iterator.h> +#include <basic/List.h> +#include <basic/Tuple.h> +#include <assert.h> +#include <stdlib.h> + +namespace omega { + +// +// general presburger stuff thats needed everywhere +// + +/* The following allows us to avoid warnings about passing + temporaries as non-const references. This is useful but + has suddenly become illegal. */ + +#if !defined(LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY) +#if defined(__GNUC__) && (__GNUC__ > 2 || (__GNUC__ == 2 && __GNUC_MINOR__ >= 7)) +#define LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY 1 +#else +#define LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY 0 +#endif +#endif + +#if LIE_ABOUT_CONST_TO_MAKE_ANSI_COMMITTEE_HAPPY +#define NOT_CONST const +#else +#define NOT_CONST +#endif + +// +// I/O and error processing and control flags (also in omega_core/debugging.h) +// + +extern FILE *DebugFile; +extern int pres_debug; + +extern int mega_total; +extern int use_ugly_names; + +extern negation_control pres_legal_negations; + + +// +// Lots of things refer to each other, +// so we forward declare these classes: +// + +class Var_Decl; +typedef enum {Input_Var, Set_Var = Input_Var, Output_Var, + Global_Var, Forall_Var, Exists_Var, Wildcard_Var} Var_Kind; +class Global_Var_Decl; +typedef enum {Unknown_Tuple = 0, Input_Tuple = 1, Output_Tuple = 2, + Set_Tuple = Input_Tuple } Argument_Tuple; + +class Constraint_Handle; +class EQ_Handle; +class GEQ_Handle; +typedef EQ_Handle Stride_Handle; + +class Formula; +class F_Declaration; +class F_Forall; +class F_Exists; +class F_And; +class F_Or; +class F_Not; +class Conjunct; +class Relation; +class Rel_Body; +class DNF; +class Mapping; +class Omega_Var; +class Coef_Var_Decl; + +typedef Var_Decl *Variable_ID; +typedef Global_Var_Decl *Global_Var_ID; + +typedef Tuple<Variable_ID> Variable_ID_Tuple; +typedef Sequence<Variable_ID> Variable_ID_Sequence; // use only for rvalues +typedef Tuple_Iterator<Variable_ID> Variable_ID_Tuple_Iterator; +typedef Tuple_Iterator<Variable_ID> Variable_ID_Iterator; + +typedef Variable_ID_Iterator Variable_Iterator; + +typedef enum {Comb_Id, Comb_And, Comb_Or, Comb_AndNot} Combine_Type; + + +// things that are (hopefully) used only privately +class Comp_Problem; +class Comp_Constraints; + +// this has to be here rather than in pres_conj.h because +// MergeConj has to be a friend of Constraint_Handle +typedef enum {MERGE_REGULAR, MERGE_COMPOSE, MERGE_GIST} Merge_Action; + + +// Conjunct can be exact or lower or upper bound. +// For lower bound conjunct, the upper bound is assumed to be true; +// For upper bound conjunct, the lower bound is assumed to be false + +typedef enum {EXACT_BOUND, UPPER_BOUND, LOWER_BOUND, UNSET_BOUND} Bound_Type; + + +#if defined STUDY_EVACUATIONS +typedef enum { in_to_out = 0, out_to_in = 1} which_way; + +enum evac { evac_trivial = 0, + evac_offset = 1, + evac_subseq = 2, + evac_offset_subseq = 3, +// evac_permutation = , + evac_affine = 4, + evac_nasty = 5 }; + +extern char *evac_names[]; + +#endif + +// the following list should be updated in sync with Relations.h + +#define friend_rel_ops \ +friend Relation Union(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend Relation Intersection(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend Relation After(NOT_CONST Relation &R, int carried_by, int new_output, int dir);\ +friend Relation Extend_Domain(NOT_CONST Relation &R); \ +friend Relation Extend_Domain(NOT_CONST Relation &R, int more); \ +friend Relation Extend_Range(NOT_CONST Relation &R); \ +friend Relation Extend_Range(NOT_CONST Relation &R, int more); \ +friend Relation Extend_Set(NOT_CONST Relation &R); \ +friend Relation Extend_Set(NOT_CONST Relation &R, int more); \ +friend Relation Restrict_Domain(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend Relation Restrict_Range(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend Relation Domain(NOT_CONST Relation &r); \ +friend Relation Range(NOT_CONST Relation &r); \ +friend Relation Cross_Product(NOT_CONST Relation &A, NOT_CONST Relation &B); \ +friend Relation Inverse(NOT_CONST Relation &r); \ +friend Relation Deltas(NOT_CONST Relation &R); \ +friend Relation Deltas(NOT_CONST Relation &R, int eq_no); \ +friend Relation DeltasToRelation(NOT_CONST Relation &R, int n_input, int n_output); \ +friend Relation Complement(NOT_CONST Relation &r); \ +friend Relation Project(NOT_CONST Relation &R, Global_Var_ID v); \ +friend Relation Project(NOT_CONST Relation &r, int pos, Var_Kind vkind); \ +friend Relation Project(NOT_CONST Relation &S, Sequence<Variable_ID> &s); \ +friend Relation Project_Sym(NOT_CONST Relation &R); \ +friend Relation Project_On_Sym(NOT_CONST Relation &R, NOT_CONST Relation &context); \ +friend Relation GistSingleConjunct(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort); \ +friend Relation Gist(NOT_CONST Relation &R1, NOT_CONST Relation &R2, int effort); \ +friend Relation Difference(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend Relation Approximate(NOT_CONST Relation &R, bool strides_allowed); \ +friend Relation Identity(int n_inp); \ +friend Relation Identity(NOT_CONST Relation &r); \ +friend bool do_subset_check(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend bool Must_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend bool Might_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend bool May_Be_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend bool Is_Obvious_Subset(NOT_CONST Relation &r1, NOT_CONST Relation &r2); \ +friend Relation Join(NOT_CONST Relation &G, NOT_CONST Relation &F); \ +friend Relation Composition(NOT_CONST Relation &F, NOT_CONST Relation &G); \ +friend bool can_do_exact_composition(NOT_CONST Relation &F, NOT_CONST Relation &G); \ +friend Relation EQs_to_GEQs(NOT_CONST Relation &, bool excludeStrides); \ +friend Relation Symbolic_Solution(NOT_CONST Relation &S); \ +friend Relation Symbolic_Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); \ +friend Relation Sample_Solution(NOT_CONST Relation &S); \ +friend Relation Solution(NOT_CONST Relation &S, Sequence<Variable_ID> &T); \ +friend void MapRel1(Relation &inputRel, const Mapping &map, \ + Combine_Type ctype, int number_input, \ + int number_output, bool, bool); \ +friend Relation MapAndCombineRel2(Relation &R1, Relation &R2, \ + const Mapping &mapping1, \ + const Mapping &mapping2, \ + Combine_Type ctype, \ + int number_input, \ + int number_output); \ +friend void align(Rel_Body *, Rel_Body *, F_Exists *, \ + Formula *, const Mapping &, bool &, \ + List<int> &, Variable_ID_Tuple &); \ +friend Relation Lower_Bound(NOT_CONST Relation &r); \ +friend Relation Upper_Bound(NOT_CONST Relation &r) + + +// REMEMBER - THE LAST LINE OF THE MACRO SHOULD NOT HAVE A ; +/* TransitiveClosure doesn't need to be in friend_rel_ops */ + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_logic.h b/lib/omega/include/omega/pres_logic.h new file mode 100644 index 0000000..27c4553 --- /dev/null +++ b/lib/omega/include/omega/pres_logic.h @@ -0,0 +1,90 @@ +#if ! defined _pres_logic_h +#define _pres_logic_h 1 + +#include <omega/pres_form.h> + +namespace omega { +// +// Presburger formula classes for logical operations: and, or not +// + +class F_And : public Formula { +public: + inline Node_Type node_type() {return Op_And;} + + // "preserves level" should be 0 unless we know this will not + // change the "level" of the constraints - ie the number of + // leading corresponding in,out variables known to be equal + GEQ_Handle add_GEQ(int preserves_level = 0); + EQ_Handle add_EQ(int preserves_level = 0); + Stride_Handle add_stride(int step, int preserves_level = 0); + EQ_Handle add_EQ(const Constraint_Handle &c, int preserves_level = 0); + GEQ_Handle add_GEQ(const Constraint_Handle &c, int preserves_level = 0); + + F_And *and_with(); + void add_unknown(); + +private: + friend class Formula; // add_and() + F_And(Formula *p, Rel_Body *r); + +private: + Formula *copy(Formula *parent, Rel_Body *reln); + virtual Conjunct *find_available_conjunct(); + int priority(); + void print_separator(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); + void beautify(); + DNF* DNFize(); + + Conjunct *pos_conj; +}; + + +class F_Or : public Formula { +public: + inline Node_Type node_type() {return Op_Or;} + +private: + friend class Formula; // add_or + F_Or(Formula *, Rel_Body *); + +private: + Formula *copy(Formula *parent, Rel_Body *reln); + + virtual Conjunct *find_available_conjunct(); + void print_separator(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); + void beautify(); + int priority(); + DNF* DNFize(); + void push_exists(Variable_ID_Tuple &S); +}; + + +class F_Not : public Formula { +public: + inline Node_Type node_type() {return Op_Not;} + void finalize(); + +private: + friend class Formula; + F_Not(Formula *, Rel_Body *); + +private: + Formula *copy(Formula *parent, Rel_Body *reln); + + virtual Conjunct *find_available_conjunct(); + friend class F_Forall; + bool can_add_child(); + void beautify(); + void rearrange(); + int priority(); + DNF* DNFize(); + void print(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_quant.h b/lib/omega/include/omega/pres_quant.h new file mode 100644 index 0000000..98c30df --- /dev/null +++ b/lib/omega/include/omega/pres_quant.h @@ -0,0 +1,63 @@ +#if ! defined _pres_quant_h +#define _pres_quant_h 1 + +#include <omega/pres_decl.h> + +namespace omega { + +// +// Presburger formula nodes for quantifiers +// + +class F_Exists : public F_Declaration { +public: + inline Node_Type node_type() {return Op_Exists;} + Variable_ID declare(Const_String s); + Variable_ID declare(); + Variable_ID declare(Variable_ID v); + virtual void push_exists(Variable_ID_Tuple &S); + +protected: + friend class Formula; + + F_Exists(Formula *, Rel_Body *); + F_Exists(Formula *, Rel_Body *, Variable_ID_Tuple &); + +private: + Formula *copy(Formula *parent, Rel_Body *reln); + + virtual Conjunct *find_available_conjunct(); + void print(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); + void beautify(); + void rearrange(); + DNF* DNFize(); +}; + + +class F_Forall : public F_Declaration { +public: + inline Node_Type node_type() {return Op_Forall;} + Variable_ID declare(Const_String s); + Variable_ID declare(); + Variable_ID declare(Variable_ID v); + +protected: + friend class Formula; + + F_Forall(Formula *, Rel_Body *); + +private: + Formula *copy(Formula *parent, Rel_Body *reln); + + virtual Conjunct *find_available_conjunct(); + void print(FILE *output_file); + void prefix_print(FILE *output_file, int debug = 1); + void beautify(); + void rearrange(); + DNF* DNFize(); +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_subs.h b/lib/omega/include/omega/pres_subs.h new file mode 100644 index 0000000..8a9ee92 --- /dev/null +++ b/lib/omega/include/omega/pres_subs.h @@ -0,0 +1,88 @@ +#if !defined(pres_subs_h) +#define pres_subs_h + +/* Interface to omega core's substitutions. + + Creating an object of class Substitutions causes ordered elimination, + i.e. variables in the input and output tuples are substituted for by + functions of earlier variables. Could conceivablely create a more + flexible interface to orderedElimination if we developed a way to + specify the desired variable order. + + This is not an entirely consistent interface, since Sub_Handles + shouldn't really permit update_coef on SUBs. It is not a real + problem since subs are now no longer part of a conjunct, but it is + a slightly odd situation. + + Don't try to simplify r after performing orderedElimination. +*/ + + +#include <omega/pres_gen.h> +#include <omega/Relation.h> +#include <omega/pres_conj.h> +#include <omega/pres_cnstr.h> + +namespace omega { + +class Sub_Handle; +class Sub_Iterator; + +class Substitutions { +public: + Substitutions(Relation &input_R, Conjunct *input_c); + ~Substitutions(); + Sub_Handle get_sub(Variable_ID v); + bool substituted(Variable_ID v); + bool sub_involves(Variable_ID v, Var_Kind kind); +private: + friend class Sub_Iterator; + friend class Sub_Handle; + Relation *r; + Conjunct *c; + eqn *subs; + Variable_ID_Tuple subbed_vars; +}; + + +//:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: + + +class Sub_Handle: public Constraint_Handle { +public: + inline Sub_Handle() {} + + virtual std::string print_to_string() const; + virtual std::string print_term_to_string() const; + Variable_ID variable() {return v;} + +private: + friend class Substitutions; + friend class Sub_Iterator; + Sub_Handle(Substitutions *, int, Variable_ID); +// Sub_Handle(Substitutions *, int); + + Variable_ID v; +}; + +//:::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::::: + + +class Sub_Iterator : public Generator<Sub_Handle> { +public: + Sub_Iterator(Substitutions *input_s): s(input_s), current(0), + last(s->c->problem->nSUBs-1) {} + int live() const; + void operator++(int); + void operator++(); + Sub_Handle operator* (); + Sub_Handle operator* () const; + +private: + Substitutions *s; + int current, last; +}; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/pres_tree.h b/lib/omega/include/omega/pres_tree.h new file mode 100644 index 0000000..ad78ad0 --- /dev/null +++ b/lib/omega/include/omega/pres_tree.h @@ -0,0 +1,15 @@ +#if ! defined _pres_tree_h +#define _pres_tree_h 1 + +// +// Header to include if you need all the classes to build +// a Presburger formula: +// variables, constraints, nodes for logical operations & quantifiers +// + +#include <omega/pres_var.h> +#include <omega/pres_cnstr.h> +#include <omega/pres_logic.h> +#include <omega/pres_quant.h> + +#endif diff --git a/lib/omega/include/omega/pres_var.h b/lib/omega/include/omega/pres_var.h new file mode 100644 index 0000000..bf60dcb --- /dev/null +++ b/lib/omega/include/omega/pres_var.h @@ -0,0 +1,230 @@ +#if ! defined _pres_var_h +#define _pres_var_h 1 + +#include <omega/pres_gen.h> +#include <map> + +namespace omega { + +// +// Variable declaration. +// Variables are free or quantified. +// Free variables are classified as input, output and global. +// Quantified variables are classified as forall, exists and wildcard. +// All global variables are functions symbols of (possibly 0) arguments +// Local variables that correspond to >0-ary functions are identified +// as functions of a prefix of the input, output, or both tuples +// +// +// typedef enum {Input_Var, Output_Var, Set_Var, +// Global_Var, Forall_Var, Exists_Var, Wildcard_Var} Var_Kind; + +typedef enum {Free_Var, Coef_Var, Bomega_Var} Global_Kind; + +// NOW IN PRES_GEN.H, as its used as an argument and can't +// be forward declared: +// typedef enum {Unknown_Tuple = 0, Input_Tuple = 1, Output_Tuple = 2, +// Set_Tuple = Input_Tuple } Argument_Tuple; +// Only Input, Output, and Set can be passed to get_local, +// but the values 0 and 3 are also used internally. + + +class Var_Decl { +public: + inline Var_Kind kind() { return var_kind; } + int get_position(); + Global_Var_ID get_global_var(); + Argument_Tuple function_of(); // valid iff kind() == Global_var + + Const_String base_name; + void name_variable(char *newname); + + // The following should be used with care, as they are only valid + // after setup_names has been used on the relation containing this + // variable. + std::string name(); + const char* char_name(); + void set_kind(Var_Kind v) { var_kind = v; } + + // Operation to allow the remap field to be used for + // union-find operations on variables. + // Be sure to reset the remap fields afterward + void UF_union(Variable_ID v); + Variable_ID UF_owner(); + +private: + Var_Decl(Const_String name, Var_Kind vkind, int pos); + Var_Decl(Var_Kind vkind, int pos); + Var_Decl(Variable_ID v); + Var_Decl(Const_String name, Global_Var_ID v); + Var_Decl(Const_String name, Global_Var_ID v, Argument_Tuple function_of); + + friend class F_Declaration; // creates local variables + friend class Global_Var_Decl; // its constructors create Var_Decls. + + friend class Global_Input_Output_Tuple; + friend void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl); + +private: + int instance; + void setup_name(); + + // these set up the names + friend class Rel_Body; +// friend class F_Declaration; already a friend + +private: + Variable_ID remap; // pointer to new copy of this node + + // lots of things need to get at "remap" - lots of relation ops, + // and functions that move UFS's around: + // dnf::make_level_carried_to and Conjunct::move_UFS_to_input() + // Also of course Conjunct::remap and push_exists + friend_rel_ops; + friend class DNF; + friend class Conjunct; + + // this prints remap to the debugging output + friend void print_var_addrs(std::string &s, Variable_ID v); + + friend void reset_remap_field(Variable_ID v); + friend void reset_remap_field(Sequence<Variable_ID> &S); + friend void reset_remap_field(Sequence<Variable_ID> &S, int var_no); + friend void reset_remap_field(Variable_ID_Tuple &S); + friend void reset_remap_field(Variable_ID_Tuple &S, int var_no); + +private: + + Var_Kind var_kind; + int position; // only for Input_Var, Output_Var + Global_Var_ID global_var; // only for Global_Var + Argument_Tuple of; // only for Global_Var +}; + +bool rm_variable(Variable_ID_Tuple &vl, Variable_ID v); +void reset_remap_field(Sequence<Variable_ID> &S); +void reset_remap_field(Sequence<Variable_ID> &S, int var_no); +void reset_remap_field(Variable_ID v); +void reset_remap_field(Variable_ID_Tuple &S); +void reset_remap_field(Variable_ID_Tuple &S, int var_no); + +class Global_Input_Output_Tuple: public Tuple<Variable_ID> { +public: + Global_Input_Output_Tuple(Var_Kind in_my_kind, int init=-1); + ~Global_Input_Output_Tuple(); + virtual Variable_ID &operator[](int index); + virtual const Variable_ID &operator[](int index) const; +private: + Var_Kind my_kind; + static const int initial_allocation; +}; + +extern Global_Input_Output_Tuple input_vars; +extern Global_Input_Output_Tuple output_vars; +// This allows the user to refer to set_vars to query sets, w/o knowing +// they are really inputs. +extern Global_Input_Output_Tuple &set_vars; + +Variable_ID input_var(int nth); +Variable_ID output_var(int nth); +Variable_ID set_var(int nth); + + + +// +// Global_Var_ID uniquely identifies global var-s through the whole program. +// Global_Var_Decl is an ADT with the following operations: +// - create global variable, +// - find the arity of the variable, (default = 0, for symbolic consts) +// - get the name of global variable, +// - tell if two variables are the same (if they are the same object) +// + +class Global_Var_Decl { +public: + Global_Var_Decl(Const_String baseName); + + virtual Const_String base_name() const + { + return loc_rep1.base_name; + } + + virtual void set_base_name(Const_String newName) + { + loc_rep1.base_name = newName; + loc_rep2.base_name = newName; + } + + virtual int arity() const + { + return 0; // default compatible with old symbolic constant stuff + } + + virtual Omega_Var *really_omega_var(); // until we get RTTI in C++ + virtual Coef_Var_Decl *really_coef_var(); // until we get RTTI in C++ + virtual Global_Kind kind() const; + +private: + + friend class Rel_Body; // Rel_Body::get_local calls this get_local + + Variable_ID get_local() + { + assert(arity() == 0); + return &loc_rep1; + } + Variable_ID get_local(Argument_Tuple of) + { + assert(arity() == 0 || of == Input_Tuple || of == Output_Tuple); + return ((arity() == 0 || of == Input_Tuple) ? &loc_rep1 : &loc_rep2); + } + + // local representative, there is just 1 for every 0-ary global variable + Var_Decl loc_rep1; // arity == 0, or arity > 0 and of == In + Var_Decl loc_rep2; // arity > 0 and of == Out + +public: +// friend class Rel_Body; // Rel_Body::setup_names sets instance + friend class Var_Decl; + int instance; +}; + + +class Coef_Var_Decl : public Global_Var_Decl { +public: + Coef_Var_Decl(int id, int var); + int stmt() const; + int var() const; + virtual Global_Kind kind() const; + virtual Coef_Var_Decl *really_coef_var(); // until we get RTTI in C++ + +private: + int i, v; +}; + + + +// +// Test subclass for Global_Var: named global variable +// +class Free_Var_Decl : public Global_Var_Decl { +public: + Free_Var_Decl(Const_String name); + Free_Var_Decl(Const_String name, int arity); + int arity() const; + virtual Global_Kind kind() const; + +private: + int _arity; +}; + + +/* === implementation functions === */ +void copy_var_decls(Variable_ID_Tuple &new_vl, Variable_ID_Tuple &vl); +void free_var_decls(Variable_ID_Tuple &vl); + +extern int wildCardInstanceNumber; + +} // namespace + +#endif diff --git a/lib/omega/include/omega/reach.h b/lib/omega/include/omega/reach.h new file mode 100644 index 0000000..76d7dee --- /dev/null +++ b/lib/omega/include/omega/reach.h @@ -0,0 +1,23 @@ +#if ! defined _reach_h +#define _reach_h 1 + +namespace omega { + +class reachable_information { +public: + Tuple<std::string> node_names; + Tuple<int> node_arity; + DynamicArray1<Relation> start_nodes; + DynamicArray2<Relation> transitions; +}; + + +DynamicArray1<Relation> * +Reachable_Nodes(reachable_information * reachable_info); + +DynamicArray1<Relation> * +I_Reachable_Nodes(reachable_information * reachable_info); + +} // namespace + +#endif |