diff options
Diffstat (limited to 'src/expr/uninterpreted_constant.cpp')
-rw-r--r-- | src/expr/uninterpreted_constant.cpp | 10 |
1 files changed, 10 insertions, 0 deletions
diff --git a/src/expr/uninterpreted_constant.cpp b/src/expr/uninterpreted_constant.cpp index d41ab1045..97bc3ae4b 100644 --- a/src/expr/uninterpreted_constant.cpp +++ b/src/expr/uninterpreted_constant.cpp @@ -20,10 +20,20 @@ #include <sstream> #include <string> +#include "base/cvc4_assert.h" + using namespace std; namespace CVC4 { +UninterpretedConstant::UninterpretedConstant(Type type, Integer index) throw(IllegalArgumentException) + : d_type(type) + , d_index(index) +{ + //PrettyCheckArgument(type.isSort(), type, "uninterpreted constants can only be created for uninterpreted sorts, not `%s'", type.toString().c_str()); + PrettyCheckArgument(index >= 0, index, "index >= 0 required for uninterpreted constant index, not `%s'", index.toString().c_str()); +} + std::ostream& operator<<(std::ostream& out, const UninterpretedConstant& uc) { stringstream ss; ss << uc.getType(); |