summaryrefslogtreecommitdiff
path: root/src/expr/uninterpreted_constant.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/expr/uninterpreted_constant.cpp')
-rw-r--r--src/expr/uninterpreted_constant.cpp10
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();
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback