diff options
author | lianah <lianahady@gmail.com> | 2013-03-26 22:14:24 -0400 |
---|---|---|
committer | lianah <lianahady@gmail.com> | 2013-03-26 22:14:24 -0400 |
commit | 2bed73156740d7e93e303b02319c407a1d587109 (patch) | |
tree | 99876e3263f20b0c507caac27c147a991fc759dd /src/util | |
parent | 33a5c0897bdbfb8367dfa90342471615908df1bc (diff) | |
parent | 70d1a0171840cd62b5c1d89b875ffb50da216793 (diff) |
added model generation for bv subtheories and bv-inequality solver option
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/datatype.cpp | 13 | ||||
-rw-r--r-- | src/util/datatype.h | 4 | ||||
-rw-r--r-- | src/util/dense_map.h | 6 | ||||
-rw-r--r-- | src/util/hash.h | 2 | ||||
-rw-r--r-- | src/util/statistics.i | 4 |
5 files changed, 20 insertions, 9 deletions
diff --git a/src/util/datatype.cpp b/src/util/datatype.cpp index 18ecbc316..574a57f19 100644 --- a/src/util/datatype.cpp +++ b/src/util/datatype.cpp @@ -820,7 +820,18 @@ std::ostream& operator<<(std::ostream& os, const Datatype& dt) { // can only output datatypes in the CVC4 native language Expr::setlanguage::Scope ls(os, language::output::LANG_CVC4); - os << "DATATYPE " << dt.getName() << " =" << endl; + os << "DATATYPE " << dt.getName(); + if(dt.isParametric()) { + os << '['; + for(size_t i = 0; i < dt.getNumParameters(); ++i) { + if(i > 0) { + os << ','; + } + os << dt.getParameter(i); + } + os << ']'; + } + os << " =" << endl; Datatype::const_iterator i = dt.begin(), i_end = dt.end(); if(i != i_end) { os << " "; diff --git a/src/util/datatype.h b/src/util/datatype.h index de38d8835..4b6894ef8 100644 --- a/src/util/datatype.h +++ b/src/util/datatype.h @@ -450,7 +450,7 @@ public: * Create a new Datatype of the given name, with the given * parameterization. */ - inline Datatype(std::string name, std::vector<Type>& params); + inline Datatype(std::string name, const std::vector<Type>& params); /** * Add a constructor to this Datatype. Constructor names need not @@ -620,7 +620,7 @@ inline Datatype::Datatype(std::string name) : d_self() { } -inline Datatype::Datatype(std::string name, std::vector<Type>& params) : +inline Datatype::Datatype(std::string name, const std::vector<Type>& params) : d_name(name), d_params(params), d_constructors(), diff --git a/src/util/dense_map.h b/src/util/dense_map.h index 222a761c3..b7d690811 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -98,7 +98,7 @@ public: return false; }else{ Assert(x < allocated()); - return d_posVector[x] != POSITION_SENTINEL; + return d_posVector[x] != +POSITION_SENTINEL; } } @@ -160,7 +160,7 @@ public: void pop_back() { Assert(!empty()); Key atBack = back(); - d_posVector[atBack] = POSITION_SENTINEL; + d_posVector[atBack] = +POSITION_SENTINEL; d_image[atBack] = T(); d_list.pop_back(); } @@ -195,7 +195,7 @@ public: void increaseSize(Key max){ Assert(max >= allocated()); - d_posVector.resize(max+1, POSITION_SENTINEL); + d_posVector.resize(max+1, +POSITION_SENTINEL); d_image.resize(max+1); } diff --git a/src/util/hash.h b/src/util/hash.h index 4d4094143..913358512 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -48,7 +48,7 @@ namespace CVC4 { struct StringHashFunction { size_t operator()(const std::string& str) const { - return std::hash<const char*>()(str.c_str()); + return __gnu_cxx::hash<const char*>()(str.c_str()); } };/* struct StringHashFunction */ diff --git a/src/util/statistics.i b/src/util/statistics.i index 74cee5f37..7f3bbe526 100644 --- a/src/util/statistics.i +++ b/src/util/statistics.i @@ -4,7 +4,7 @@ #ifdef SWIGJAVA #include "bindings/java_iterator_adapter.h" -#include "bindings/java_output_stream_adapter.h" +#include "bindings/java_stream_adapters.h" #endif /* SWIGJAVA */ %} @@ -72,7 +72,7 @@ #ifdef SWIGJAVA %include "bindings/java_iterator_adapter.h" -%include "bindings/java_output_stream_adapter.h" +%include "bindings/java_stream_adapters.h" %template(JavaIteratorAdapter_StatisticsBase) CVC4::JavaIteratorAdapter<CVC4::StatisticsBase>; |