declare-sort, define-sort working but not thoroughly tested; define-fun half working (just need to decide where to expand)

1 files changed, 6 insertions, 0 deletions

diff --git a/src/expr/expr_template.cpp b/src/expr/expr_template.cpp
index 83d5dc47f..803808b0f 100644
--- a/src/expr/expr_template.cpp
+++ b/src/expr/expr_template.cpp
@@ -151,6 +151,12 @@ bool Expr::operator>(const Expr& e) const {
   return *d_node > *e.d_node;
 }
 
+unsigned Expr::getId() const {
+  ExprManagerScope ems(*this);
+  Assert(d_node != NULL, "Unexpected NULL expression pointer!");
+  return d_node->getId();
+}
+
 Kind Expr::getKind() const {
   ExprManagerScope ems(*this);
   Assert(d_node != NULL, "Unexpected NULL expression pointer!");