diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-01-28 17:31:57 -0500 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-03-22 18:54:52 -0400 |
| commit | f44a81d1b62058fa56af952aa92be965690481e5 (patch) | |
| tree | dc4b56e27701abd61ebd69675f86a9366d90998f /src/util | |
| parent | 36816ad2537a2e6163037e9592c513b9a69aa9dc (diff) | |
Support for Boolean term conversion in datatypes.
Diffstat (limited to 'src/util')
| -rw-r--r-- | src/util/datatype.cpp | 13 | ||||
| -rw-r--r-- | src/util/datatype.h | 4 |
2 files changed, 14 insertions, 3 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(), |