From a00a9fbdfd1e9545c26d8cb5114832dc13849114 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 2 Mar 2014 17:10:48 -0800
Subject: [PATCH] generate error on duplicated data-type accessors. Issue 85

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/pdecl.cpp       | 19 +++++++++++++++++++
 src/cmd_context/pdecl.h         |  2 ++
 src/parsers/smt2/smt2parser.cpp |  7 +++++++
 3 files changed, 28 insertions(+)

diff --git a/src/cmd_context/pdecl.cpp b/src/cmd_context/pdecl.cpp
index 44ba2b4d2..4a51e4943 100644
--- a/src/cmd_context/pdecl.cpp
+++ b/src/cmd_context/pdecl.cpp
@@ -515,6 +515,25 @@ bool pdatatype_decl::has_missing_refs(symbol & missing) const {
     return false;
 }
 
+bool pdatatype_decl::has_duplicate_accessors(symbol & duplicated) const {
+    hashtable<symbol, symbol_hash_proc, symbol_eq_proc> names;
+    ptr_vector<pconstructor_decl>::const_iterator it  = m_constructors.begin();
+    ptr_vector<pconstructor_decl>::const_iterator end = m_constructors.end();
+    for (; it != end; ++it) {
+        ptr_vector<paccessor_decl> const& acc = (*it)->m_accessors;
+        for (unsigned i = 0; i < acc.size(); ++i) {
+            symbol const& name = acc[i]->get_name();
+            if (names.contains(name)) {
+                duplicated = name;
+                return true;
+            }
+            names.insert(name);
+        }
+    }
+    return false;
+}
+
+
 bool pdatatype_decl::fix_missing_refs(dictionary<int> const & symbol2idx, symbol & missing) {
     ptr_vector<pconstructor_decl>::iterator it  = m_constructors.begin();
     ptr_vector<pconstructor_decl>::iterator end = m_constructors.end();
diff --git a/src/cmd_context/pdecl.h b/src/cmd_context/pdecl.h
index 76ad2a020..83d881f57 100644
--- a/src/cmd_context/pdecl.h
+++ b/src/cmd_context/pdecl.h
@@ -169,6 +169,7 @@ public:
 class paccessor_decl : public pdecl {
     friend class pdecl_manager;
     friend class pconstructor_decl;
+    friend class pdatatype_decl;
     symbol   m_name;
     ptype    m_type;
     paccessor_decl(unsigned id, unsigned num_params, pdecl_manager & m, symbol const & n, ptype const & r);
@@ -222,6 +223,7 @@ public:
     sort * instantiate(pdecl_manager & m, unsigned n, sort * const * s);
     virtual void display(std::ostream & out) const;
     bool has_missing_refs(symbol & missing) const;
+    bool has_duplicate_accessors(symbol & repeated) const;
 };
 
 /**
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index b5af6353e..546fd3819 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -850,6 +850,13 @@ namespace smt2 {
             for (unsigned i = 0; i < sz; i++) {
                 pdatatype_decl * d = new_dt_decls[i];
                 SASSERT(d != 0);
+                symbol duplicated;
+                if (d->has_duplicate_accessors(duplicated)) {
+                    std::string err_msg = "invalid datatype declaration, repeated accessor identifier '";
+                    err_msg += duplicated.str();
+                    err_msg += "'";
+                    throw parser_exception(err_msg, line, pos);
+                }
                 m_ctx.insert(d);
                 if (d->get_num_params() == 0) {
                     // if datatype is not parametric... then force instantiation to register accessor, recognizers and constructors...