From eef2bbadad9dd51a7c9ea0ded1a986dd7e0ba04a Mon Sep 17 00:00:00 2001 From: Murphy Berzish Date: Tue, 4 Apr 2017 20:29:48 -0400 Subject: [PATCH] remove obsolete PARAM_STRING from ast --- src/ast/ast.cpp | 4 ---- src/ast/ast.h | 9 ++------- 2 files changed, 2 insertions(+), 11 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 7271048b1..5f2de5170 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -59,7 +59,6 @@ parameter& parameter::operator=(parameter const& other) { case PARAM_SYMBOL: new (m_symbol) symbol(other.get_symbol()); break; case PARAM_RATIONAL: new (m_rational) rational(other.get_rational()); break; case PARAM_DOUBLE: m_dval = other.m_dval; break; - case PARAM_STRING: m_string = other.m_string; break; case PARAM_EXTERNAL: m_ext_id = other.m_ext_id; break; default: UNREACHABLE(); @@ -95,7 +94,6 @@ bool parameter::operator==(parameter const & p) const { case PARAM_SYMBOL: return get_symbol() == p.get_symbol(); case PARAM_RATIONAL: return get_rational() == p.get_rational(); case PARAM_DOUBLE: return m_dval == p.m_dval; - case PARAM_STRING: return (m_string == NULL && p.m_string == NULL) || strcmp(m_string, p.m_string)==0; case PARAM_EXTERNAL: return m_ext_id == p.m_ext_id; default: UNREACHABLE(); return false; } @@ -109,7 +107,6 @@ unsigned parameter::hash() const { case PARAM_SYMBOL: b = get_symbol().hash(); break; case PARAM_RATIONAL: b = get_rational().hash(); break; case PARAM_DOUBLE: b = static_cast(m_dval); break; - case PARAM_STRING: /* TODO */ b = 42; break; case PARAM_EXTERNAL: b = m_ext_id; break; } return (b << 2) | m_kind; @@ -122,7 +119,6 @@ std::ostream& parameter::display(std::ostream& out) const { case PARAM_RATIONAL: return out << get_rational(); case PARAM_AST: return out << "#" << get_ast()->get_id(); case PARAM_DOUBLE: return out << m_dval; - case PARAM_STRING: return out << m_string; case PARAM_EXTERNAL: return out << "@" << m_ext_id; default: UNREACHABLE(); diff --git a/src/ast/ast.h b/src/ast/ast.h index 066265bb8..6bb3b01c9 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -87,7 +87,6 @@ public: PARAM_SYMBOL, PARAM_RATIONAL, PARAM_DOUBLE, - PARAM_STRING, // PARAM_EXTERNAL is used for handling decl_plugin specific parameters. // For example, it is used for handling mpf numbers in float_decl_plugin, // and irrational algebraic numbers in arith_decl_plugin. @@ -106,7 +105,6 @@ private: char m_symbol[sizeof(symbol)]; // for PARAM_SYMBOL char m_rational[sizeof(rational)]; // for PARAM_RATIONAL double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin) - const char* m_string; // for PARAM_STRING unsigned m_ext_id; // for PARAM_EXTERNAL }; @@ -119,8 +117,8 @@ public: explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL) { new (m_symbol) symbol(s); } explicit parameter(rational const & r): m_kind(PARAM_RATIONAL) { new (m_rational) rational(r); } explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} - explicit parameter(const char *s):m_kind(PARAM_STRING), m_string(s) { - TRACE("parse_string", tout << "parameter(const char *): " << s << "\n";); + explicit parameter(const char *s):m_kind(PARAM_SYMBOL) { + new (m_symbol) symbol(s); } explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); @@ -135,7 +133,6 @@ public: bool is_symbol() const { return m_kind == PARAM_SYMBOL; } bool is_rational() const { return m_kind == PARAM_RATIONAL; } bool is_double() const { return m_kind == PARAM_DOUBLE; } - bool is_string() const { return m_kind == PARAM_STRING; } bool is_external() const { return m_kind == PARAM_EXTERNAL; } bool is_int(int & i) const { return is_int() && (i = get_int(), true); } @@ -143,7 +140,6 @@ public: bool is_symbol(symbol & s) const { return is_symbol() && (s = get_symbol(), true); } bool is_rational(rational & r) const { return is_rational() && (r = get_rational(), true); } bool is_double(double & d) const { return is_double() && (d = get_double(), true); } - // TODO is_string(char*) bool is_external(unsigned & id) const { return is_external() && (id = get_ext_id(), true); } /** @@ -163,7 +159,6 @@ public: symbol const & get_symbol() const { SASSERT(is_symbol()); return *(reinterpret_cast(m_symbol)); } rational const & get_rational() const { SASSERT(is_rational()); return *(reinterpret_cast(m_rational)); } double get_double() const { SASSERT(is_double()); return m_dval; } - const char * get_string() const { SASSERT(is_string()); return m_string; } unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; } bool operator==(parameter const & p) const;