diff options
Diffstat (limited to 'src/util')
92 files changed, 723 insertions, 264 deletions
diff --git a/src/util/Makefile.am b/src/util/Makefile.am index bf3f1a873..5cf5da1e0 100644 --- a/src/util/Makefile.am +++ b/src/util/Makefile.am @@ -95,6 +95,7 @@ libutil_la_SOURCES = \ sort_inference.cpp \ regexp.h \ regexp.cpp \ + bin_heap.h \ didyoumean.h \ didyoumean.cpp @@ -147,6 +148,7 @@ EXTRA_DIST = \ language.i \ array.i \ array_store_all.i \ + emptyset.i \ ascription_type.i \ rational.i \ hash.i \ diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index 3ed372848..d99353b74 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index 39fd9e368..78a1e9975 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/array.h b/src/util/array.h index 892e28a86..ab554171f 100644 --- a/src/util/array.h +++ b/src/util/array.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/array_store_all.cpp b/src/util/array_store_all.cpp index 7c9086276..dfd021e75 100644 --- a/src/util/array_store_all.cpp +++ b/src/util/array_store_all.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/array_store_all.h b/src/util/array_store_all.h index 6e60cc2cb..bccefdd58 100644 --- a/src/util/array_store_all.h +++ b/src/util/array_store_all.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/ascription_type.h b/src/util/ascription_type.h index 1f7ba0aaa..42906e557 100644 --- a/src/util/ascription_type.h +++ b/src/util/ascription_type.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/backtrackable.h b/src/util/backtrackable.h index 57ed94771..5492dd8b5 100644 --- a/src/util/backtrackable.h +++ b/src/util/backtrackable.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h new file mode 100644 index 000000000..53c2a9bb6 --- /dev/null +++ b/src/util/bin_heap.h @@ -0,0 +1,367 @@ +/********************* */ +/*! \file bin_heap.h + ** \verbatim + ** Original author: Tim King + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief An implementation of a binary heap + ** + ** An implementation of a binary heap. + ** Attempts to roughly follow the contract of Boost's d_ary_heap. + ** (http://www.boost.org/doc/libs/1_49_0/doc/html/boost/heap/d_ary_heap.html) + ** Also attempts to generalize ext/pd_bs/priority_queue. + ** (http://gcc.gnu.org/onlinedocs/libstdc++/ext/pb_ds/priority_queue.html) + **/ + +#include "cvc4_private.h" + +#ifndef __CVC4__BIN_HEAP_H +#define __CVC4__BIN_HEAP_H + +#include <limits> +#include <functional> + +#include "util/exception.h" + +namespace CVC4 { + +/** + * BinaryHeap that orders its elements greatest-first (i.e., in the opposite + * direction of the provided comparator). Update of elements is permitted + * via handles, which are not invalidated by mutation (pushes and pops etc.). + * Handles are invalidted when their element is no longer a member of the + * heap. Iteration over elements is supported but iteration is unsorted and + * iterators are immutable. + */ +template <class Elem, class CmpFcn = std::less<Elem> > +class BinaryHeap { +private: + typedef Elem T; + struct HElement; + + typedef std::vector<HElement*> ElementVector; + + struct HElement { + HElement(size_t pos, const T& elem): d_pos(pos), d_elem(elem) {} + size_t d_pos; + T d_elem; + };/* struct HElement */ + + /** A 0 indexed binary heap. */ + ElementVector d_heap; + + /** The comparator. */ + CmpFcn d_cmp; + + // disallow copy and assignment + BinaryHeap(const BinaryHeap&) CVC4_UNDEFINED; + BinaryHeap& operator=(const BinaryHeap&) CVC4_UNDEFINED; + +public: + BinaryHeap(const CmpFcn& c = CmpFcn()) + : d_heap() + , d_cmp(c) + {} + + ~BinaryHeap(){ + clear(); + } + + class handle { + private: + HElement* d_pointer; + handle(HElement* p) : d_pointer(p){} + friend class BinaryHeap; + public: + handle() : d_pointer(NULL) {} + const T& operator*() const { + Assert(d_pointer != NULL); + return d_pointer->d_elem; + } + + bool operator==(const handle& h) const { + return d_pointer == h.d_pointer; + } + + bool operator!=(const handle& h) const { + return d_pointer != h.d_pointer; + } + + }; /* BinaryHeap<>::handle */ + + class const_iterator : public std::iterator<std::input_iterator_tag, Elem> { + private: + typename ElementVector::const_iterator d_iter; + friend class BinaryHeap; + const_iterator(const typename ElementVector::const_iterator& iter) + : d_iter(iter) + {} + public: + const_iterator(){} + inline bool operator==(const const_iterator& ci) const{ + return d_iter == ci.d_iter; + } + inline bool operator!=(const const_iterator& ci) const{ + return d_iter != ci.d_iter; + } + inline const_iterator& operator++(){ + ++d_iter; + return *this; + } + inline const_iterator operator++(int){ + const_iterator i = *this; + ++d_iter; + return i; + } + inline const T& operator*() const{ + const HElement* he = *d_iter; + return he->d_elem; + } + + };/* BinaryHeap<>::const_iterator */ + + typedef const_iterator iterator; + + inline size_t size() const { return d_heap.size(); } + inline bool empty() const { return d_heap.empty(); } + + inline const_iterator begin() const { + return const_iterator(d_heap.begin()); + } + + inline const_iterator end() const { + return const_iterator(d_heap.end()); + } + + void clear(){ + typename ElementVector::iterator i=d_heap.begin(), iend=d_heap.end(); + for(; i!=iend; ++i){ + HElement* he = *i; + delete he; + } + d_heap.clear(); + } + + void swap(BinaryHeap& heap){ + std::swap(d_heap, heap.d_heap); + std::swap(d_cmp, heap.d_cmp); + } + + handle push(const T& toAdded){ + Assert(size() < MAX_SIZE); + HElement* he = new HElement(size(), toAdded); + d_heap.push_back(he); + up_heap(he); + return handle(he); + } + + void erase(handle h){ + Assert(!empty()); + Assert(debugHandle(h)); + + HElement* he = h.d_pointer; + size_t pos = he->d_pos; + if(pos == root()){ + // the top element can be efficiently removed by pop + pop(); + }else if(pos == last()){ + // the last element can be safely removed + d_heap.pop_back(); + delete he; + }else{ + // This corresponds to + // 1) swapping the elements at pos with the element at last: + // 2) deleting the new last element + // 3) updating the position of the new element at pos + swapIndices(pos, last()); + d_heap.pop_back(); + delete he; + update(handle(d_heap[pos])); + } + } + + void pop(){ + Assert(!empty()); + swapIndices(root(), last()); + HElement* b = d_heap.back(); + d_heap.pop_back(); + delete b; + + if(!empty()){ + down_heap(d_heap.front()); + } + } + + const T& top() const { + Assert(!empty()); + return (d_heap.front())->d_elem; + } + +private: + void update(handle h){ + Assert(!empty()); + Assert(debugHandle(h)); + + // The relationship between h and its parent, left and right has become unknown. + // But it is assumed that parent <= left, and parent <= right still hold. + // Figure out whether to up_heap or down_heap. + + Assert(!empty()); + HElement* he = h.d_pointer; + + size_t pos = he->d_pos; + if(pos == root()){ + // no parent + down_heap(he); + }else{ + size_t par = parent(pos); + HElement* at_parent = d_heap[par]; + if(gt(he->d_elem, at_parent->d_elem)){ + // he > parent + up_heap(he); + }else{ + down_heap(he); + } + } + } + +public: + void update(handle h, const T& val){ + Assert(!empty()); + Assert(debugHandle(h)); + h.d_pointer->d_elem = val; + update(h); + } + + /** (std::numeric_limits<size_t>::max()-2)/2; */ + static const size_t MAX_SIZE; + +private: + inline bool gt(const T& a, const T& b) const{ + // cmp acts like an operator< + return d_cmp(b, a); + } + + inline bool lt(const T& a, const T& b) const{ + return d_cmp(a, b); + } + + inline static size_t parent(size_t p){ + Assert(p != root()); + return (p-1)/2; + } + inline static size_t right(size_t p){ return 2*p+2; } + inline static size_t left(size_t p){ return 2*p+1; } + inline static size_t root(){ return 0; } + inline size_t last() const{ + Assert(!empty()); + return size() - 1; + } + + inline void swapIndices(size_t i, size_t j){ + HElement* at_i = d_heap[i]; + HElement* at_j = d_heap[j]; + swap(i,j,at_i,at_j); + } + + inline void swapPointers(HElement* at_i, HElement* at_j){ + // still works if at_i == at_j + size_t i = at_i->d_pos; + size_t j = at_j->d_pos; + swap(i,j,at_i,at_j); + } + + inline void swap(size_t i, size_t j, HElement* at_i, HElement* at_j){ + // still works if i == j + Assert(i == at_i->d_pos); + Assert(j == at_j->d_pos); + d_heap[i] = at_j; + d_heap[j] = at_i; + at_i->d_pos = j; + at_j->d_pos = i; + } + + void up_heap(HElement* he){ + const size_t& curr = he->d_pos; + // The value of curr changes implicitly during swap operations. + while(curr != root()){ + // he->d_elem > parent + size_t par = parent(curr); + HElement* at_parent = d_heap[par]; + if(gt(he->d_elem, at_parent->d_elem)){ + swap(curr, par, he, at_parent); + }else{ + break; + } + } + } + + void down_heap(HElement* he){ + const size_t& curr = he->d_pos; + // The value of curr changes implicitly during swap operations. + size_t N = size(); + size_t r, l; + + while((r = right(curr)) < N){ + l = left(curr); + + // if at_left == at_right, favor left + HElement* at_left = d_heap[l]; + HElement* at_right = d_heap[r]; + if(lt(he->d_elem, at_left->d_elem)){ + // he < at_left + if(lt(at_left->d_elem, at_right->d_elem)){ + // he < at_left < at_right + swap(curr, r, he, at_right); + }else{ + // he < at_left + // at_right <= at_left + swap(curr, l, he, at_left); + } + }else{ + // at_left <= he + if(lt(he->d_elem, at_right->d_elem)){ + // at_left <= he < at_right + swap(curr, r, he, at_right); + }else{ + // at_left <= he + // at_right <= he + break; + } + } + } + l = left(curr); + if(r >= N && l < N){ + // there is a left but not a right + HElement* at_left = d_heap[l]; + if(lt(he->d_elem, at_left->d_elem)){ + // he < at_left + swap(curr, l, he, at_left); + } + } + } + + bool debugHandle(handle h) const{ + HElement* he = h.d_pointer; + if( he == NULL ){ + return true; + }else if(he->d_pos >= size()){ + return false; + }else{ + return he == d_heap[he->d_pos]; + } + } + +}; /* class BinaryHeap<> */ + +template <class Elem, class CmpFcn> +const size_t BinaryHeap<Elem,CmpFcn>::MAX_SIZE = (std::numeric_limits<size_t>::max()-2)/2; + +}/* CVC4 namespace */ + +#endif /* __CVC4__BIN_HEAP_H */ diff --git a/src/util/bitvector.h b/src/util/bitvector.h index 35b052531..798dd63c7 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Liana Hadarean ** Minor contributors (to current version): Christopher L. Conway ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/bool.h b/src/util/bool.h index 373b4fdec..2d5e15777 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/boolean_simplification.cpp b/src/util/boolean_simplification.cpp index 8e077fe1d..62ef46339 100644 --- a/src/util/boolean_simplification.cpp +++ b/src/util/boolean_simplification.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/boolean_simplification.h b/src/util/boolean_simplification.h index be39f69c1..d0ca3646f 100644 --- a/src/util/boolean_simplification.h +++ b/src/util/boolean_simplification.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/cache.h b/src/util/cache.h index 8c2f9abca..5183c439b 100644 --- a/src/util/cache.h +++ b/src/util/cache.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index 42f8519c1..dfee0aae2 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 34aa9c08b..524d9cda4 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/chain.h b/src/util/chain.h index e9216724e..e052a2ed8 100644 --- a/src/util/chain.h +++ b/src/util/chain.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/channel.h b/src/util/channel.h index 676371cbc..3644f786a 100644 --- a/src/util/channel.h +++ b/src/util/channel.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 05f5c7678..5bd607d94 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -113,6 +113,10 @@ std::string Configuration::about() { return CVC4_ABOUT_STRING; } +bool Configuration::licenseIsGpl() { + return IS_GPL_BUILD; +} + bool Configuration::isBuiltWithGmp() { return IS_GMP_BUILD; } @@ -129,6 +133,10 @@ bool Configuration::isBuiltWithAbc() { return IS_ABC_BUILD; } +bool Configuration::isBuiltWithReadline() { + return IS_READLINE_BUILD; +} + bool Configuration::isBuiltWithCudd() { return false; } diff --git a/src/util/cvc4_assert.cpp b/src/util/cvc4_assert.cpp index 08e2867f6..3db285182 100644 --- a/src/util/cvc4_assert.cpp +++ b/src/util/cvc4_assert.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/cvc4_assert.h b/src/util/cvc4_assert.h index 7d359a56b..cc854278b 100644 --- a/src/util/cvc4_assert.h +++ b/src/util/cvc4_assert.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): ACSYS ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index f0ddc2cf6..9e07c746a 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/datatype.h b/src/util/datatype.h index befb3428d..32fae8235 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -2,10 +2,10 @@ /*! \file datatype.h ** \verbatim ** Original author: Morgan Deters - ** Major contributors: none - ** Minor contributors (to current version): Andrew Reynolds + ** Major contributors: Andrew Reynolds + ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/debug.h b/src/util/debug.h index 97c176f02..6ef196111 100644 --- a/src/util/debug.h +++ b/src/util/debug.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/dense_map.h b/src/util/dense_map.h index 10ca9f72f..39cee5b9e 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): Morgan Deters, Dejan Jovanovic + ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/didyoumean_test.cpp b/src/util/didyoumean_test.cpp index 2fe3331d9..0c46d5ffe 100644 --- a/src/util/didyoumean_test.cpp +++ b/src/util/didyoumean_test.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file didyoumean_test.cpp + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + // Compile: g++ didyoumean_test.cpp didyoumean.cpp // For debug compile with -DDIDYOUMEAN_DEBUG or -DDIDYOUMEAN_DEBUG1 or both diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp index 4e20d6b5f..ee085d25b 100644 --- a/src/util/divisible.cpp +++ b/src/util/divisible.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/divisible.h b/src/util/divisible.h index 0c0c7bc5b..6917bf2a6 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/dump.cpp b/src/util/dump.cpp index e3baf10c5..53c5eae6a 100644 --- a/src/util/dump.cpp +++ b/src/util/dump.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/dump.h b/src/util/dump.h index a85062af1..2cf5877d4 100644 --- a/src/util/dump.h +++ b/src/util/dump.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/dynamic_array.h b/src/util/dynamic_array.h index 1f6e07cc7..18b1b645b 100644 --- a/src/util/dynamic_array.h +++ b/src/util/dynamic_array.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/emptyset.cpp b/src/util/emptyset.cpp index fa1bb8f10..7905f11fb 100644 --- a/src/util/emptyset.cpp +++ b/src/util/emptyset.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file emptyset.cpp + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "util/emptyset.h" #include <iostream> diff --git a/src/util/emptyset.h b/src/util/emptyset.h index 2f6c54173..4b3bb204f 100644 --- a/src/util/emptyset.h +++ b/src/util/emptyset.h @@ -2,7 +2,7 @@ /*! \file emptyset.h ** \verbatim ** Original author: Kshitij Bansal - ** Major contributors: none + ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. ** Copyright (c) 2009-2014 New York University and The University of Iowa @@ -35,10 +35,14 @@ class CVC4_PUBLIC EmptySet { const SetType d_type; + EmptySet() { } public: - EmptySet() { } /* Null typed */ - EmptySet(SetType t):d_type(t) { } + /** + * Constructs an emptyset of the specified type. Note that the argument + * is the type of the set itself, NOT the type of the elements. + */ + EmptySet(SetType setType):d_type(setType) { } ~EmptySet() throw() { diff --git a/src/util/emptyset.i b/src/util/emptyset.i new file mode 100644 index 000000000..ce4f3a4b7 --- /dev/null +++ b/src/util/emptyset.i @@ -0,0 +1,17 @@ +%{ +#include "util/emptyset.h" +%} + +%rename(equals) CVC4::EmptySet::operator==(const EmptySet&) const; +%ignore CVC4::EmptySet::operator!=(const EmptySet&) const; + +%rename(less) CVC4::EmptySet::operator<(const EmptySet&) const; +%rename(lessEqual) CVC4::EmptySet::operator<=(const EmptySet&) const; +%rename(greater) CVC4::EmptySet::operator>(const EmptySet&) const; +%rename(greaterEqual) CVC4::EmptySet::operator>=(const EmptySet&) const; + +%rename(apply) CVC4::EmptySetHashFunction::operator()(const EmptySet&) const; + +%ignore CVC4::operator<<(std::ostream& out, const EmptySet& es); + +%include "util/emptyset.h" diff --git a/src/util/exception.cpp b/src/util/exception.cpp index 08405c501..ab510c27d 100644 --- a/src/util/exception.cpp +++ b/src/util/exception.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/exception.h b/src/util/exception.h index cd4b763ef..937729f0c 100644 --- a/src/util/exception.h +++ b/src/util/exception.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index b5654e9cb..d3f0d09d4 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/hash.h b/src/util/hash.h index 0cdc96fcb..218cf0aab 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/index.h b/src/util/index.h index be3e2918b..ea0802b2d 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/integer.h.in b/src/util/integer.h.in index c3c6a70cd..3db9998a7 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index bd23b48c9..02086494b 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -1,3 +1,20 @@ +/********************* */ +/*! \file integer_cln_imp.cpp + ** \verbatim + ** Original author: Tim King + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + #include "cvc4autoconfig.h" #include "util/integer.h" #include <string> diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 8b56c4b19..9f7f4a06b 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Dejan Jovanovic, Liana Hadarean ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index bb6166523..2717d03f4 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -2,10 +2,10 @@ /*! \file integer_gmp_imp.cpp ** \verbatim ** Original author: Tim King - ** Major contributors: Morgan Deters, Christopher L. Conway + ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 68d335aec..d1f5050d5 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Liana Hadarean ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp index f1dce413c..68d7d9a34 100644 --- a/src/util/ite_removal.cpp +++ b/src/util/ite_removal.cpp @@ -2,10 +2,10 @@ /*! \file ite_removal.cpp ** \verbatim ** Original author: Dejan Jovanovic - ** Major contributors: Morgan Deters, Andrew Reynolds, Tim King - ** Minor contributors (to current version): Clark Barrett + ** Major contributors: Tim King, Morgan Deters + ** Minor contributors (to current version): Kshitij Bansal, Andrew Reynolds, Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h index de5f83f27..83c55dab7 100644 --- a/src/util/ite_removal.h +++ b/src/util/ite_removal.h @@ -2,10 +2,10 @@ /*! \file ite_removal.h ** \verbatim ** Original author: Dejan Jovanovic - ** Major contributors: Kshitij Bansal, Morgan Deters, Tim King - ** Minor contributors (to current version): Andrew Reynolds, Clark Barrett + ** Major contributors: Kshitij Bansal, Tim King, Morgan Deters + ** Minor contributors (to current version): Clark Barrett ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/language.cpp b/src/util/language.cpp index c5c9828df..f19f20c03 100644 --- a/src/util/language.cpp +++ b/src/util/language.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -68,6 +68,8 @@ OutputLanguage toOutputLanguage(std::string language) { language == "presentation" || language == "native" || language == "LANG_CVC4") { return output::LANG_CVC4; + } else if(language == "cvc3" || language == "LANG_CVC3") { + return output::LANG_CVC3; } else if(language == "smtlib1" || language == "smt1" || language == "LANG_SMTLIB_V1") { return output::LANG_SMTLIB_V1; @@ -110,7 +112,7 @@ InputLanguage toInputLanguage(std::string language) { return input::LANG_AUTO; } - throw OptionException(std::string("unknown input language " + language + "'")); + throw OptionException(std::string("unknown input language `" + language + "'")); }/* toInputLanguage() */ }/* CVC4::language namespace */ diff --git a/src/util/language.h b/src/util/language.h index c79c4d9aa..be962bf3e 100644 --- a/src/util/language.h +++ b/src/util/language.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Francois Bobot ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -121,6 +121,8 @@ enum CVC4_PUBLIC Language { /** The AST output language */ LANG_AST = 10, + /** The CVC3-compatibility output language */ + LANG_CVC3, /** LANG_MAX is > any valid OutputLanguage id */ LANG_MAX @@ -147,6 +149,9 @@ inline std::ostream& operator<<(std::ostream& out, Language lang) { case LANG_AST: out << "LANG_AST"; break; + case LANG_CVC3: + out << "LANG_CVC3"; + break; default: out << "undefined_output_language"; } diff --git a/src/util/lemma_input_channel.h b/src/util/lemma_input_channel.h index 319de942c..44f0b87f5 100644 --- a/src/util/lemma_input_channel.h +++ b/src/util/lemma_input_channel.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/lemma_output_channel.h b/src/util/lemma_output_channel.h index 8f4f7461d..df7abd1e9 100644 --- a/src/util/lemma_output_channel.h +++ b/src/util/lemma_output_channel.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/matcher.h b/src/util/matcher.h index 4a3233261..107891a54 100644 --- a/src/util/matcher.h +++ b/src/util/matcher.h @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/maybe.h b/src/util/maybe.h index b1c81f76e..4d279a0c7 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Tim King ** Major contributors: none - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/model.cpp b/src/util/model.cpp index e25065c21..c1254ab47 100644 --- a/src/util/model.cpp +++ b/src/util/model.cpp @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/model.h b/src/util/model.h index 1d80b0308..98794a53d 100644 --- a/src/util/model.h +++ b/src/util/model.h @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/nary_builder.cpp b/src/util/nary_builder.cpp index 08aceef6f..d89121fd7 100644 --- a/src/util/nary_builder.cpp +++ b/src/util/nary_builder.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/nary_builder.h b/src/util/nary_builder.h index 7676cadbc..c98e01b1b 100644 --- a/src/util/nary_builder.h +++ b/src/util/nary_builder.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/node_visitor.h b/src/util/node_visitor.h index 1d2bf0b9d..66a58efd1 100644 --- a/src/util/node_visitor.h +++ b/src/util/node_visitor.h @@ -5,7 +5,7 @@ ** Major contributors: Liana Hadarean, Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/ntuple.h b/src/util/ntuple.h index a342a11c1..b9e1100f1 100644 --- a/src/util/ntuple.h +++ b/src/util/ntuple.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/output.cpp b/src/util/output.cpp index d60330b0c..462043805 100644 --- a/src/util/output.cpp +++ b/src/util/output.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/output.h b/src/util/output.h index 7394f24ab..0974591db 100644 --- a/src/util/output.h +++ b/src/util/output.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King, Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/predicate.cpp b/src/util/predicate.cpp index 1b473d5ad..787d329aa 100644 --- a/src/util/predicate.cpp +++ b/src/util/predicate.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/predicate.h b/src/util/predicate.h index 686e92dc8..5ead2f090 100644 --- a/src/util/predicate.h +++ b/src/util/predicate.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -52,7 +52,7 @@ public: bool operator==(const Predicate& p) const; - friend std::ostream& operator<<(std::ostream& out, const Predicate& p); + friend std::ostream& CVC4::operator<<(std::ostream& out, const Predicate& p); friend size_t PredicateHashFunction::operator()(const Predicate& p) const; };/* class Predicate */ diff --git a/src/util/predicate.i b/src/util/predicate.i index f29cd16d5..eedbb2e83 100644 --- a/src/util/predicate.i +++ b/src/util/predicate.i @@ -7,6 +7,6 @@ %rename(apply) CVC4::PredicateHashFunction::operator()(const Predicate&) const; -%ignore CVC4::operator<<(std::ostream& out, const Predicate& p); +%ignore CVC4::operator<<(std::ostream&, const Predicate&); %include "util/predicate.h" diff --git a/src/util/proof.h b/src/util/proof.h index aa81d3294..be1e2a8e2 100644 --- a/src/util/proof.h +++ b/src/util/proof.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/rational.h.in b/src/util/rational.h.in index c02886906..6f9c29c19 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index f674481de..e5e3608cb 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Christopher L. Conway ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index b144ab419..895fc1c9b 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 25c7dab59..155faebf2 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters, Christopher L. Conway ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 273b3072d..6288be050 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/record.cpp b/src/util/record.cpp index 136f190a1..ea9b5495a 100644 --- a/src/util/record.cpp +++ b/src/util/record.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/record.h b/src/util/record.h index 63c54930e..5689a4209 100644 --- a/src/util/record.h +++ b/src/util/record.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/recursion_breaker.h b/src/util/recursion_breaker.h index a4177f600..3369c5c23 100644 --- a/src/util/recursion_breaker.h +++ b/src/util/recursion_breaker.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index cbc0b843b..b1b454cfa 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -1,159 +1,159 @@ -/********************* */
-/*! \file regexp.cpp
- ** \verbatim
- ** Original author: Tianyi Liang
- ** Major contributors: none
- ** Minor contributors (to current version): Morgan Deters
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2013 New York University and The University of Iowa
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "util/regexp.h"
-#include <iostream>
-#include <iomanip>
-
-using namespace std;
-
-namespace CVC4 {
-
-void String::toInternal(const std::string &s) {
- d_str.clear();
- unsigned i=0;
- while(i < s.size()) {
- if(s[i] == '\\') {
- i++;
- if(i < s.size()) {
- switch(s[i]) {
- case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break;
- case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break;
- case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break;
- case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break;
- case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break;
- case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break;
- case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break;
- case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break;
- case 'x': {
- if(i + 2 < s.size()) {
- if(isxdigit(s[i+1]) && isxdigit(s[i+2])) {
- d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) );
- i += 3;
- } else {
- throw CVC4::Exception( "Illegal String Literal: \"" + s + "\"" );
- }
- } else {
- throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must have two digits after \\x" );
- }
- }
- break;
- default: {
- if(isdigit(s[i])) {
- int num = (int)s[i] - (int)'0';
- bool flag = num < 4;
- if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') {
- num = num * 8 + (int)s[i+1] - (int)'0';
- if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') {
- num = num * 8 + (int)s[i+2] - (int)'0';
- d_str.push_back( convertCharToUnsignedInt((char)num) );
- i += 3;
- } else {
- d_str.push_back( convertCharToUnsignedInt((char)num) );
- i += 2;
- }
- } else {
- d_str.push_back( convertCharToUnsignedInt((char)num) );
- i++;
- }
- } else if((unsigned)s[i] > 127) {
- throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" );
- } else {
- d_str.push_back( convertCharToUnsignedInt(s[i]) );
- i++;
- }
- }
- }
- } else {
- throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" );
- //d_str.push_back( convertCharToUnsignedInt('\\') );
- }
- } else if((unsigned)s[i] > 127) {
- throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" );
- } else {
- d_str.push_back( convertCharToUnsignedInt(s[i]) );
- i++;
- }
- }
-}
-
-void String::getCharSet(std::set<unsigned int> &cset) const {
- for(std::vector<unsigned int>::const_iterator itr = d_str.begin();
- itr != d_str.end(); itr++) {
- cset.insert( *itr );
- }
-}
-
-std::size_t String::overlap(String &y) const {
- std::size_t i = d_str.size() < y.size() ? d_str.size() : y.size();
- for(; i>0; i--) {
- String s = suffix(i);
- String p = y.prefix(i);
- if(s == p) {
- return i;
- }
- }
- return i;
-}
-
-std::string String::toString() const {
- std::string str;
- for(unsigned int i=0; i<d_str.size(); ++i) {
- char c = convertUnsignedIntToChar( d_str[i] );
- if(isprint( c )) {
- if(c == '\\') {
- str += "\\\\";
- } else if(c == '\"') {
- str += "\\\"";
- } else {
- str += c;
- }
- } else {
- std::string s;
- switch(c) {
- case '\a': s = "\\a"; break;
- case '\b': s = "\\b"; break;
- case '\t': s = "\\t"; break;
- case '\r': s = "\\r"; break;
- case '\v': s = "\\v"; break;
- case '\f': s = "\\f"; break;
- case '\n': s = "\\n"; break;
- case '\e': s = "\\e"; break;
- default : {
- std::stringstream ss;
- ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c);
- std::string t = ss.str();
- t = t.substr(t.size()-2, 2);
- s = "\\x" + t;
- //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str();
- }
- }
- str += s;
- }
- }
- return str;
-}
-
-std::ostream& operator <<(std::ostream& os, const String& s) {
- return os << "\"" << s.toString() << "\"";
-}
-
-std::ostream& operator<<(std::ostream& out, const RegExp& s) {
- return out << "regexp(" << s.getType() << ')';
-}
-
-}/* CVC4 namespace */
+/********************* */ +/*! \file regexp.cpp + ** \verbatim + ** Original author: Tianyi Liang + ** Major contributors: Morgan Deters + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief [[ Add one-line brief description here ]] + ** + ** [[ Add lengthier description here ]] + ** \todo document this file + **/ + +#include "util/regexp.h" +#include <iostream> +#include <iomanip> + +using namespace std; + +namespace CVC4 { + +void String::toInternal(const std::string &s) { + d_str.clear(); + unsigned i=0; + while(i < s.size()) { + if(s[i] == '\\') { + i++; + if(i < s.size()) { + switch(s[i]) { + case 'n': {d_str.push_back( convertCharToUnsignedInt('\n') );i++;} break; + case 't': {d_str.push_back( convertCharToUnsignedInt('\t') );i++;} break; + case 'v': {d_str.push_back( convertCharToUnsignedInt('\v') );i++;} break; + case 'b': {d_str.push_back( convertCharToUnsignedInt('\b') );i++;} break; + case 'r': {d_str.push_back( convertCharToUnsignedInt('\r') );i++;} break; + case 'f': {d_str.push_back( convertCharToUnsignedInt('\f') );i++;} break; + case 'a': {d_str.push_back( convertCharToUnsignedInt('\a') );i++;} break; + case '\\': {d_str.push_back( convertCharToUnsignedInt('\\') );i++;} break; + case 'x': { + if(i + 2 < s.size()) { + if(isxdigit(s[i+1]) && isxdigit(s[i+2])) { + d_str.push_back( convertCharToUnsignedInt( hexToDec(s[i+1]) * 16 + hexToDec(s[i+2]) ) ); + i += 3; + } else { + throw CVC4::Exception( "Illegal String Literal: \"" + s + "\"" ); + } + } else { + throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must have two digits after \\x" ); + } + } + break; + default: { + if(isdigit(s[i])) { + int num = (int)s[i] - (int)'0'; + bool flag = num < 4; + if(i+1 < s.size() && num < 8 && isdigit(s[i+1]) && s[i+1] < '8') { + num = num * 8 + (int)s[i+1] - (int)'0'; + if(flag && i+2 < s.size() && isdigit(s[i+2]) && s[i+2] < '8') { + num = num * 8 + (int)s[i+2] - (int)'0'; + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i += 3; + } else { + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i += 2; + } + } else { + d_str.push_back( convertCharToUnsignedInt((char)num) ); + i++; + } + } else if((unsigned)s[i] > 127) { + throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" ); + } else { + d_str.push_back( convertCharToUnsignedInt(s[i]) ); + i++; + } + } + } + } else { + throw CVC4::Exception( "should be handled by lexer: \"" + s + "\"" ); + //d_str.push_back( convertCharToUnsignedInt('\\') ); + } + } else if((unsigned)s[i] > 127) { + throw CVC4::Exception( "Illegal String Literal: \"" + s + "\", must use escaped sequence" ); + } else { + d_str.push_back( convertCharToUnsignedInt(s[i]) ); + i++; + } + } +} + +void String::getCharSet(std::set<unsigned int> &cset) const { + for(std::vector<unsigned int>::const_iterator itr = d_str.begin(); + itr != d_str.end(); itr++) { + cset.insert( *itr ); + } +} + +std::size_t String::overlap(String &y) const { + std::size_t i = d_str.size() < y.size() ? d_str.size() : y.size(); + for(; i>0; i--) { + String s = suffix(i); + String p = y.prefix(i); + if(s == p) { + return i; + } + } + return i; +} + +std::string String::toString() const { + std::string str; + for(unsigned int i=0; i<d_str.size(); ++i) { + char c = convertUnsignedIntToChar( d_str[i] ); + if(isprint( c )) { + if(c == '\\') { + str += "\\\\"; + } else if(c == '\"') { + str += "\\\""; + } else { + str += c; + } + } else { + std::string s; + switch(c) { + case '\a': s = "\\a"; break; + case '\b': s = "\\b"; break; + case '\t': s = "\\t"; break; + case '\r': s = "\\r"; break; + case '\v': s = "\\v"; break; + case '\f': s = "\\f"; break; + case '\n': s = "\\n"; break; + case '\e': s = "\\e"; break; + default : { + std::stringstream ss; + ss << std::setfill ('0') << std::setw(2) << std::hex << ((int)c); + std::string t = ss.str(); + t = t.substr(t.size()-2, 2); + s = "\\x" + t; + //std::string s2 = static_cast<std::ostringstream*>( &(std::ostringstream() << (int)c) )->str(); + } + } + str += s; + } + } + return str; +} + +std::ostream& operator <<(std::ostream& os, const String& s) { + return os << "\"" << s.toString() << "\""; +} + +std::ostream& operator<<(std::ostream& out, const RegExp& s) { + return out << "regexp(" << s.getType() << ')'; +} + +}/* CVC4 namespace */ diff --git a/src/util/regexp.h b/src/util/regexp.h index 1ee5dcc13..e75ca1fad 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -20,8 +20,7 @@ #ifndef __CVC4__REGEXP_H #define __CVC4__REGEXP_H -#include <iostream> -#include <iomanip> +#include <vector> #include <string> #include <set> #include <sstream> diff --git a/src/util/result.cpp b/src/util/result.cpp index 909a7d8c6..91b671262 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/result.h b/src/util/result.h index 21bf563bd..8c804daa7 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 52d992d4b..64b898d45 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/sexpr.h b/src/util/sexpr.h index 0222382b0..a121b5195 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King, Morgan Deters ** Minor contributors (to current version): Dejan Jovanovic ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/sort_inference.cpp b/src/util/sort_inference.cpp index b38ed7d63..179bb1a23 100644 --- a/src/util/sort_inference.cpp +++ b/src/util/sort_inference.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Andrew Reynolds ** Major contributors: Morgan Deters - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -580,6 +580,8 @@ Node SortInference::simplify( Node n, std::map< Node, Node >& var_bound ){ ss << "io_" << op; TypeNode typ = NodeManager::currentNM()->mkFunctionType( argTypes, retType ); d_symbol_map[op] = NodeManager::currentNM()->mkSkolem( ss.str(), typ, "op created during sort inference" ); + Trace("setp-model") << "Function " << op << " is replaced with " << d_symbol_map[op] << std::endl; + d_model_replace_f[op] = d_symbol_map[op]; }else{ d_symbol_map[op] = op; } diff --git a/src/util/sort_inference.h b/src/util/sort_inference.h index cd80f57d8..4bb1a072e 100644 --- a/src/util/sort_inference.h +++ b/src/util/sort_inference.h @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** @@ -26,7 +26,7 @@ namespace CVC4 { -class SortInference{ +class SortInference { private: //all subsorts std::vector< int > d_sub_sorts; @@ -69,7 +69,6 @@ private: void printSort( const char* c, int t ); //process int process( Node n, std::map< Node, Node >& var_bound ); - //for monotonicity inference private: void processMonotonic( Node n, bool pol, bool hasPol, std::map< Node, Node >& var_bound ); @@ -107,6 +106,9 @@ public: bool isWellSorted( Node n ); //get constraints for being well-typed according to computed sub-types void getSortConstraints( Node n, SortInference::UnionFind& uf ); +public: + //list of all functions and the uninterpreted symbols they were replaced with + std::map< Node, Node > d_model_replace_f; }; } diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index d632933b4..ff31e7b4b 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/statistics.h b/src/util/statistics.h index 5b9e75837..a7088f5c5 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index 61762b84d..097869bc7 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -2,10 +2,10 @@ /*! \file statistics_registry.cpp ** \verbatim ** Original author: Morgan Deters - ** Major contributors: Tim King - ** Minor contributors (to current version): none + ** Major contributors: none + ** Minor contributors (to current version): Kshitij Bansal, Tim King ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index 186433c5a..b9e3eaf8b 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: Morgan Deters ** Major contributors: Tim King - ** Minor contributors (to current version): none + ** Minor contributors (to current version): Kshitij Bansal ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/subrange_bound.h b/src/util/subrange_bound.h index 82dc940ea..b90656f33 100644 --- a/src/util/subrange_bound.h +++ b/src/util/subrange_bound.h @@ -5,7 +5,7 @@ ** Major contributors: Tim King ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/tls.h.in b/src/util/tls.h.in index e13149c3a..88969e250 100644 --- a/src/util/tls.h.in +++ b/src/util/tls.h.in @@ -5,7 +5,7 @@ ** Major contributors: Morgan Deters ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/trans_closure.cpp b/src/util/trans_closure.cpp index 970d2542e..02b51d751 100644 --- a/src/util/trans_closure.cpp +++ b/src/util/trans_closure.cpp @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/trans_closure.h b/src/util/trans_closure.h index 14e7ab95f..27f32377e 100644 --- a/src/util/trans_closure.h +++ b/src/util/trans_closure.h @@ -5,7 +5,7 @@ ** Major contributors: Andrew Reynolds ** Minor contributors (to current version): Dejan Jovanovic, Morgan Deters ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/tuple.h b/src/util/tuple.h index 375a1aba3..fe016db2c 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/uninterpreted_constant.cpp b/src/util/uninterpreted_constant.cpp index 6b98a7be8..f0d9a42d2 100644 --- a/src/util/uninterpreted_constant.cpp +++ b/src/util/uninterpreted_constant.cpp @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/uninterpreted_constant.h b/src/util/uninterpreted_constant.h index 869491538..c4fb776bc 100644 --- a/src/util/uninterpreted_constant.h +++ b/src/util/uninterpreted_constant.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** diff --git a/src/util/utility.h b/src/util/utility.h index 9b15adecd..59522901a 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -5,7 +5,7 @@ ** Major contributors: none ** Minor contributors (to current version): none ** This file is part of the CVC4 project. - ** Copyright (c) 2009-2013 New York University and The University of Iowa + ** Copyright (c) 2009-2014 New York University and The University of Iowa ** See the file COPYING in the top-level source directory for licensing ** information.\endverbatim ** |