From 541658fe02163f120e229e983894eafc0f75814e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 10 Jan 2020 12:14:13 -0800 Subject: [PATCH] move to abstract symbols Signed-off-by: Nikolaj Bjorner --- src/api/api_util.h | 4 +-- src/api/z3_logger.h | 4 +-- src/api/z3_replayer.cpp | 12 ++++--- src/ast/ast.h | 8 ++--- src/ast/dl_decl_plugin.cpp | 54 +++++++++++++++++-------------- src/ast/dl_decl_plugin.h | 36 +++++++-------------- src/ast/fpa/bv2fpa_converter.cpp | 8 ++--- src/ast/pp.cpp | 4 +-- src/ast/seq_decl_plugin.cpp | 2 +- src/muz/fp/dl_cmds.cpp | 9 ++++-- src/muz/rel/rel_context.cpp | 6 ++-- src/muz/spacer/spacer_context.cpp | 6 ++-- src/solver/solver.cpp | 2 +- src/util/params.cpp | 29 ++++++++++++----- src/util/symbol.cpp | 10 +++++- src/util/symbol.h | 16 +++++---- 16 files changed, 117 insertions(+), 93 deletions(-) diff --git a/src/api/api_util.h b/src/api/api_util.h index 37d9880bc..ba8255837 100644 --- a/src/api/api_util.h +++ b/src/api/api_util.h @@ -76,8 +76,8 @@ inline Z3_func_decl of_func_decl(func_decl* f) { return reinterpret_cast(f); } -inline symbol to_symbol(Z3_symbol s) { return symbol::mk_symbol_from_c_ptr(reinterpret_cast(s)); } -inline Z3_symbol of_symbol(symbol s) { return reinterpret_cast(const_cast(s.c_ptr())); } +inline symbol to_symbol(Z3_symbol s) { return symbol::c_api_ext2symbol(s); } +inline Z3_symbol of_symbol(symbol s) { return static_cast(s.c_api_symbol2ext()); } inline Z3_pattern of_pattern(ast* a) { return reinterpret_cast(a); } inline app* to_pattern(Z3_pattern p) { return reinterpret_cast(p); } diff --git a/src/api/z3_logger.h b/src/api/z3_logger.h index 8f0eb5371..264644c45 100644 --- a/src/api/z3_logger.h +++ b/src/api/z3_logger.h @@ -28,8 +28,8 @@ static void __declspec(noinline) U(uint64_t u) { *g_z3_log << "U " << u << "\n static void __declspec(noinline) D(double d) { *g_z3_log << "D " << d << "\n"; g_z3_log->flush(); } static void __declspec(noinline) S(Z3_string str) { *g_z3_log << "S \"" << ll_escaped(str) << "\"\n"; g_z3_log->flush(); } static void __declspec(noinline) Sy(Z3_symbol sym) { - symbol s = symbol::mk_symbol_from_c_ptr(reinterpret_cast(sym)); - if (s == symbol::null) { + symbol s = symbol::c_api_ext2symbol(sym); + if (s.is_null()) { *g_z3_log << "N\n"; } else if (s.is_numerical()) { diff --git a/src/api/z3_replayer.cpp b/src/api/z3_replayer.cpp index 09cc8bba4..3f7e17cc0 100644 --- a/src/api/z3_replayer.cpp +++ b/src/api/z3_replayer.cpp @@ -90,12 +90,14 @@ struct z3_replayer::imp { uint64_t m_uint; double m_double; char const * m_str; + void const* m_sym; // uint64_t void * m_obj; float m_float; }; value():m_kind(OBJECT), m_int(0) {} value(void * obj):m_kind(OBJECT), m_obj(obj) {} value(value_kind k, char const * str):m_kind(k), m_str(str) {} + value(value_kind k, symbol const& s):m_kind(k), m_sym(s.c_api_symbol2ext()) {} value(value_kind k, uint64_t u):m_kind(k), m_uint(u) {} value(value_kind k, int64_t i):m_kind(k), m_int(i) {} value(value_kind k, double d):m_kind(k), m_double(d) {} @@ -135,7 +137,7 @@ struct z3_replayer::imp { out << v.m_str; break; case SYMBOL: - out << symbol::mk_symbol_from_c_ptr(v.m_str); + out << symbol::c_api_ext2symbol(v.m_sym); break; case OBJECT: out << v.m_obj; @@ -455,13 +457,13 @@ struct z3_replayer::imp { // push null symbol next(); TRACE("z3_replayer", tout << "[" << m_line << "] " << "N\n";); - m_args.push_back(value(SYMBOL, static_cast(nullptr))); + m_args.push_back(value(SYMBOL, symbol::null)); break; case '$': { // push symbol next(); skip_blank(); read_quoted_symbol(); TRACE("z3_replayer", tout << "[" << m_line << "] " << "$ " << m_id << "\n";); - m_args.push_back(value(SYMBOL, m_id.bare_str())); + m_args.push_back(value(SYMBOL, m_id)); break; } case '#': { @@ -469,7 +471,7 @@ struct z3_replayer::imp { next(); skip_blank(); read_uint64(); TRACE("z3_replayer", tout << "[" << m_line << "] " << "# " << m_uint64 << "\n";); symbol sym(static_cast(m_uint64)); - m_args.push_back(value(SYMBOL, static_cast(sym.c_ptr()))); + m_args.push_back(value(SYMBOL, sym)); break; } case 'I': @@ -615,7 +617,7 @@ struct z3_replayer::imp { Z3_symbol get_symbol(unsigned pos) const { check_arg(pos, SYMBOL); - return reinterpret_cast(const_cast(m_args[pos].m_str)); + return (Z3_symbol)m_args[pos].m_sym; } void * get_obj(unsigned pos) const { diff --git a/src/ast/ast.h b/src/ast/ast.h index 97c64ddd0..4bd5b4bae 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -109,7 +109,7 @@ private: union { int m_int; // for PARAM_INT ast* m_ast; // for PARAM_AST - void const* m_symbol; // for PARAM_SYMBOL + symbol m_symbol; // for PARAM_SYMBOL rational* m_rational; // for PARAM_RATIONAL double m_dval; // for PARAM_DOUBLE (remark: this is not used in float_decl_plugin) unsigned m_ext_id; // for PARAM_EXTERNAL @@ -121,11 +121,11 @@ public: explicit parameter(int val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(unsigned val): m_kind(PARAM_INT), m_int(val) {} explicit parameter(ast * p): m_kind(PARAM_AST), m_ast(p) {} - explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s.c_ptr()) {} + explicit parameter(symbol const & s): m_kind(PARAM_SYMBOL), m_symbol(s) {} explicit parameter(rational const & r): m_kind(PARAM_RATIONAL), m_rational(alloc(rational, r)) {} explicit parameter(rational && r) : m_kind(PARAM_RATIONAL), m_rational(alloc(rational, std::move(r))) {} explicit parameter(double d):m_kind(PARAM_DOUBLE), m_dval(d) {} - explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s).c_ptr()) {} + explicit parameter(const char *s):m_kind(PARAM_SYMBOL), m_symbol(symbol(s)) {} explicit parameter(unsigned ext_id, bool):m_kind(PARAM_EXTERNAL), m_ext_id(ext_id) {} parameter(parameter const&); @@ -176,7 +176,7 @@ public: int get_int() const { SASSERT(is_int()); return m_int; } ast * get_ast() const { SASSERT(is_ast()); return m_ast; } - symbol get_symbol() const { SASSERT(is_symbol()); return symbol::mk_symbol_from_c_ptr(m_symbol); } + symbol get_symbol() const { SASSERT(is_symbol()); return m_symbol; } rational const & get_rational() const { SASSERT(is_rational()); return *m_rational; } double get_double() const { SASSERT(is_double()); return m_dval; } unsigned get_ext_id() const { SASSERT(is_external()); return m_ext_id; } diff --git a/src/ast/dl_decl_plugin.cpp b/src/ast/dl_decl_plugin.cpp index 745cc0675..29a1e5d74 100644 --- a/src/ast/dl_decl_plugin.cpp +++ b/src/ast/dl_decl_plugin.cpp @@ -632,24 +632,30 @@ namespace datalog { } void dl_decl_plugin::get_sort_names(svector & sort_names, symbol const & logic) { - - } - - - dl_decl_util::ast_plugin_registrator::ast_plugin_registrator(ast_manager& m) - { - // ensure required plugins are installed into the ast_manager - reg_decl_plugins(m); } dl_decl_util::dl_decl_util(ast_manager& m): - m_plugin_registrator(m), m(m), - m_arith(m), - m_bv(m), - m_fid(m.mk_family_id(symbol("datalog_relation"))) + m_fid(null_family_id) {} + bv_util& dl_decl_util::bv() const { + if (!m_bv) m_bv = alloc(bv_util, m); + return *m_bv; + } + + family_id dl_decl_util::get_family_id() const { + if (m_fid == null_family_id) { + m_fid = m.mk_family_id(symbol("datalog_relation")); + } + return m_fid; + }; + + arith_util& dl_decl_util::arith() const { + if (!m_arith) m_arith = alloc(arith_util, m); + return *m_arith; + } + // create a constant belonging to a given finite domain. app* dl_decl_util::mk_numeral(uint64_t value, sort* s) { @@ -659,13 +665,13 @@ namespace datalog { m.raise_exception("value is out of bounds"); } parameter params[2] = { parameter(rational(value, rational::ui64())), parameter(s) }; - return m.mk_const(m.mk_func_decl(m_fid, OP_DL_CONSTANT, 2, params, 0, (sort*const*)nullptr)); + return m.mk_const(m.mk_func_decl(get_family_id(), OP_DL_CONSTANT, 2, params, 0, (sort*const*)nullptr)); } - if (m_arith.is_int(s) || m_arith.is_real(s)) { - return m_arith.mk_numeral(rational(value, rational::ui64()), s); + if (arith().is_int(s) || arith().is_real(s)) { + return arith().mk_numeral(rational(value, rational::ui64()), s); } - if (m_bv.is_bv_sort(s)) { - return m_bv.mk_numeral(rational(value, rational::ui64()), s); + if (bv().is_bv_sort(s)) { + return bv().mk_numeral(rational(value, rational::ui64()), s); } if (m.is_bool(s)) { if (value == 0) { @@ -699,7 +705,7 @@ namespace datalog { } rational val; unsigned bv_size = 0; - if (m_bv.is_numeral(e, val, bv_size) && bv_size < 64) { + if (bv().is_numeral(e, val, bv_size) && bv_size < 64) { SASSERT(val.is_uint64()); v = val.get_uint64(); return true; @@ -719,8 +725,8 @@ namespace datalog { if (is_numeral(c)) return true; rational val; unsigned bv_size = 0; - if (m_arith.is_numeral(c, val) && val.is_uint64()) return true; - if (m_bv.is_numeral(c, val, bv_size) && bv_size < 64) return true; + if (arith().is_numeral(c, val) && val.is_uint64()) return true; + if (bv().is_numeral(c, val, bv_size) && bv_size < 64) return true; return m.is_true(c) || m.is_false(c); } @@ -731,7 +737,7 @@ namespace datalog { throw default_exception(sstm.str()); } parameter params[2] = { parameter(name), parameter(rational(domain_size, rational::ui64())) }; - return m.mk_sort(m_fid, DL_FINITE_SORT, 2, params); + return m.mk_sort(get_family_id(), DL_FINITE_SORT, 2, params); } bool dl_decl_util::try_get_size(const sort * s, uint64_t& size) const { @@ -745,16 +751,16 @@ namespace datalog { app* dl_decl_util::mk_lt(expr* a, expr* b) { expr* args[2] = { a, b }; - return m.mk_app(m_fid, OP_DL_LT, 0, nullptr, 2, args); + return m.mk_app(get_family_id(), OP_DL_LT, 0, nullptr, 2, args); } app* dl_decl_util::mk_le(expr* a, expr* b) { expr* args[2] = { b, a }; - return m.mk_not(m.mk_app(m_fid, OP_DL_LT, 0, nullptr, 2, args)); + return m.mk_not(m.mk_app(get_family_id(), OP_DL_LT, 0, nullptr, 2, args)); } sort* dl_decl_util::mk_rule_sort() { - return m.mk_sort(m_fid, DL_RULE_SORT); + return m.mk_sort(get_family_id(), DL_RULE_SORT); } app* dl_decl_util::mk_rule(symbol const& name, unsigned num_args, expr* const* args) { diff --git a/src/ast/dl_decl_plugin.h b/src/ast/dl_decl_plugin.h index 257404f70..8c094e4ec 100644 --- a/src/ast/dl_decl_plugin.h +++ b/src/ast/dl_decl_plugin.h @@ -139,28 +139,14 @@ namespace datalog { }; class dl_decl_util { - /** - Some plugins need to be registered in the ast_manager before we - create some of the member objects (the bv_util requires bv plugin - installed). - - Doing this in the constructor of the dl_decl_plugin object is too late (as - member objects are created before we get into the constructor), so we - have this auxiliary object that is the first object of the context, - so that it gets created first. It's only purpose is that in its - constructor the required plugins are added to the ast manager. - */ - class ast_plugin_registrator { - public: - ast_plugin_registrator(ast_manager& m); - }; - - ast_plugin_registrator m_plugin_registrator; ast_manager& m; - arith_util m_arith; - bv_util m_bv; - family_id m_fid; + mutable scoped_ptr m_arith; + mutable scoped_ptr m_bv; + mutable family_id m_fid; + + bv_util& bv() const; + arith_util& arith() const; public: dl_decl_util(ast_manager& m); @@ -172,9 +158,9 @@ namespace datalog { app* mk_le(expr* a, expr* b); - bool is_lt(const expr* a) const { return is_app_of(a, m_fid, OP_DL_LT); } + bool is_lt(const expr* a) const { return is_app_of(a, get_family_id(), OP_DL_LT); } - bool is_numeral(const expr* c) const { return is_app_of(c, m_fid, OP_DL_CONSTANT); } + bool is_numeral(const expr* c) const { return is_app_of(c, get_family_id(), OP_DL_CONSTANT); } bool is_numeral(const expr* e, uint64_t& v) const; @@ -191,7 +177,7 @@ namespace datalog { bool try_get_size(const sort *, uint64_t& size) const; bool is_finite_sort(sort* s) const { - return is_sort_of(s, m_fid, DL_FINITE_SORT); + return is_sort_of(s, get_family_id(), DL_FINITE_SORT); } bool is_finite_sort(expr* e) const { @@ -199,7 +185,7 @@ namespace datalog { } bool is_rule_sort(sort* s) const { - return is_sort_of(s, m_fid, DL_RULE_SORT); + return is_sort_of(s, get_family_id(), DL_RULE_SORT); } sort* mk_rule_sort(); @@ -210,7 +196,7 @@ namespace datalog { ast_manager& get_manager() const { return m; } - family_id get_family_id() const { return m_fid; } + family_id get_family_id() const; }; diff --git a/src/ast/fpa/bv2fpa_converter.cpp b/src/ast/fpa/bv2fpa_converter.cpp index a98564ae7..d4fd3d5f1 100644 --- a/src/ast/fpa/bv2fpa_converter.cpp +++ b/src/ast/fpa/bv2fpa_converter.cpp @@ -486,25 +486,25 @@ void bv2fpa_converter::display(std::ostream & out) { for (auto const& kv : m_const2bv) { const symbol & n = kv.m_key->get_name(); out << "\n (" << n << " "; - unsigned indent = n.size() + 4; + unsigned indent = n.display_size() + 4; out << mk_ismt2_pp(kv.m_value, m, indent) << ")"; } for (auto const& kv : m_rm_const2bv) { const symbol & n = kv.m_key->get_name(); out << "\n (" << n << " "; - unsigned indent = n.size() + 4; + unsigned indent = n.display_size() + 4; out << mk_ismt2_pp(kv.m_value, m, indent) << ")"; } for (auto const& kv : m_uf2bvuf) { const symbol & n = kv.m_key->get_name(); out << "\n (" << n << " "; - unsigned indent = n.size() + 4; + unsigned indent = n.display_size() + 4; out << mk_ismt2_pp(kv.m_value, m, indent) << ")"; } for (auto const& kv : m_min_max_specials) { const symbol & n = kv.m_key->get_name(); out << "\n (" << n << " "; - unsigned indent = n.size() + 4; + unsigned indent = n.display_size() + 4; out << mk_ismt2_pp(kv.m_value.first, m, indent) << "; " << mk_ismt2_pp(kv.m_value.second, m, indent) << ")"; } diff --git a/src/ast/pp.cpp b/src/ast/pp.cpp index 39f1986ee..e307989c9 100644 --- a/src/ast/pp.cpp +++ b/src/ast/pp.cpp @@ -26,8 +26,8 @@ static std::pair space_upto_line_break(ast_manager & m, format * decl_kind k = f->get_decl_kind(); switch(k) { case OP_STRING: { - size_t len = strlen(f->get_decl()->get_parameter(0).get_symbol().bare_str()); - return std::make_pair(static_cast(len), false); + unsigned len = f->get_decl()->get_parameter(0).get_symbol().display_size(); + return std::make_pair(len, false); } case OP_CHOICE: return space_upto_line_break(m, to_app(f->get_arg(0))); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 1745be9f4..3efbc85bb 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -523,7 +523,7 @@ void seq_decl_plugin::init() { if (m_init) return; ast_manager& m = *m_manager; m_init = true; - sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0)); + sort* A = m.mk_uninterpreted_sort(symbol(0u)); sort* strT = m_string; parameter paramA(A); parameter paramS(strT); diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp index 707417279..5595923b5 100644 --- a/src/muz/fp/dl_cmds.cpp +++ b/src/muz/fp/dl_cmds.cpp @@ -35,7 +35,7 @@ Notes: struct dl_context { - smt_params m_fparams; + scoped_ptr m_fparams; params_ref m_params_ref; fp_params m_params; cmd_context & m_cmd; @@ -70,10 +70,15 @@ struct dl_context { } } + smt_params& fparams() { + if (!m_fparams) m_fparams = alloc(smt_params); + return *m_fparams.get(); + } + void init() { ast_manager& m = m_cmd.m(); if (!m_context) { - m_context = alloc(datalog::context, m, m_register_engine, m_fparams, m_params_ref); + m_context = alloc(datalog::context, m, m_register_engine, fparams(), m_params_ref); } if (!m_decl_plugin) { symbol name("datalog_relation"); diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index b9e30b970..bc41a3265 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -156,8 +156,8 @@ namespace datalog { TRACE("dl", m_context.display(tout);); //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream());); - if (m_context.print_aig().size()) { - const char *filename = static_cast(m_context.print_aig().c_ptr()); + if (!m_context.print_aig().is_null()) { + const char *filename = m_context.print_aig().bare_str(); aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); std::ofstream strm(filename, std::ios_base::binary); aig(strm); @@ -549,7 +549,7 @@ namespace datalog { void rel_context::add_fact(func_decl* pred, relation_fact const& fact) { get_rmanager().reset_saturated_marks(); get_relation(pred).add_fact(fact); - if (m_context.print_aig().size()) { + if (!m_context.print_aig().is_null()) { m_table_facts.push_back(std::make_pair(pred, fact)); } } diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp index f8e774a03..12a607191 100644 --- a/src/muz/spacer/spacer_context.cpp +++ b/src/muz/spacer/spacer_context.cpp @@ -3271,7 +3271,7 @@ bool context::is_reachable(pob &n) void context::dump_json() { - if (m_params.spacer_print_json().size()) { + if (!m_params.spacer_print_json().is_null()) { std::ofstream of; of.open(m_params.spacer_print_json().bare_str()); m_json_marshaller.marshal(of); @@ -3950,7 +3950,7 @@ void context::add_constraint (expr *c, unsigned level) } void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { - if (m_params.spacer_print_json().size()) + if (!m_params.spacer_print_json().is_null()) m_json_marshaller.register_lemma(lem); bool handle=false; for (unsigned i = 0; i < m_callbacks.size(); i++) { @@ -3974,7 +3974,7 @@ void context::new_lemma_eh(pred_transformer &pt, lemma *lem) { } void context::new_pob_eh(pob *p) { - if (m_params.spacer_print_json().size()) + if (!m_params.spacer_print_json().is_null()) m_json_marshaller.register_pob(p); } diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp index 5852be0d1..bfa2b7da1 100644 --- a/src/solver/solver.cpp +++ b/src/solver/solver.cpp @@ -344,7 +344,7 @@ lbool solver::check_sat(unsigned num_assumptions, expr * const * assumptions) { void solver::dump_state(unsigned sz, expr* const* assumptions) { if ((symbol::null != m_cancel_backup_file) && !m_cancel_backup_file.is_numerical() && - m_cancel_backup_file.c_ptr() && + !m_cancel_backup_file.is_null() && m_cancel_backup_file.bare_str()[0]) { std::string file = m_cancel_backup_file.str(); std::ofstream ous(file); diff --git a/src/util/params.cpp b/src/util/params.cpp index 82376e965..79d2f0cea 100644 --- a/src/util/params.cpp +++ b/src/util/params.cpp @@ -319,9 +319,22 @@ class params { unsigned m_uint_value; double m_double_value; char const * m_str_value; - char const * m_sym_value; + symbol m_sym_value; rational * m_rat_value; }; + value() : m_kind(CPK_BOOL), m_bool_value(false) {} + value& operator=(value const& other) { + m_kind = other.m_kind; + switch (m_kind) { + case CPK_BOOL: m_bool_value = other.m_bool_value; break; + case CPK_UINT: m_uint_value = other.m_uint_value; break; + case CPK_DOUBLE: m_double_value = other.m_double_value; break; + case CPK_STRING: m_str_value = other.m_str_value; break; + case CPK_SYMBOL: m_sym_value = other.m_sym_value; break; + default: m_rat_value = other.m_rat_value; break; + } + return *this; + } }; typedef std::pair entry; svector m_entries; @@ -422,7 +435,7 @@ public: out << " " << *(e.second.m_rat_value); break; case CPK_SYMBOL: - out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); + out << " " << e.second.m_sym_value; break; case CPK_STRING: out << " " << e.second.m_str_value; @@ -455,7 +468,7 @@ public: out << " " << *(e.second.m_rat_value); break; case CPK_SYMBOL: - out << " " << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); + out << " " << e.second.m_sym_value; break; case CPK_STRING: out << " " << e.second.m_str_value; @@ -486,7 +499,7 @@ public: out << *(e.second.m_rat_value); return; case CPK_SYMBOL: - out << symbol::mk_symbol_from_c_ptr(e.second.m_sym_value); + out << e.second.m_sym_value; return; case CPK_STRING: out << e.second.m_str_value; @@ -576,7 +589,7 @@ void params_ref::copy_core(params const * src) { m_params->set_rat(p.first, *(p.second.m_rat_value)); break; case CPK_SYMBOL: - m_params->set_sym(p.first, symbol::mk_symbol_from_c_ptr(p.second.m_sym_value)); + m_params->set_sym(p.first, p.second.m_sym_value); break; case CPK_STRING: m_params->set_str(p.first, p.second.m_str_value); @@ -887,11 +900,11 @@ rational params::get_rat(char const * k, rational const & _default) const { } symbol params::get_sym(symbol const & k, symbol const & _default) const { - GET_VALUE(return symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);, CPK_SYMBOL); + GET_VALUE(return it->second.m_sym_value;, CPK_SYMBOL); } symbol params::get_sym(char const * k, symbol const & _default) const { - GET_VALUE(return symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);, CPK_SYMBOL); + GET_VALUE(return it->second.m_sym_value;, CPK_SYMBOL); } #define GET_VALUE2(MATCH_CODE, KIND) { \ @@ -925,7 +938,7 @@ char const * params::get_str(char const * k, params_ref const & fallback, char c } symbol params::get_sym(char const * k, params_ref const & fallback, symbol const & _default) const { - GET_VALUE2(return symbol::mk_symbol_from_c_ptr(it->second.m_sym_value);, CPK_SYMBOL); + GET_VALUE2(return it->second.m_sym_value;, CPK_SYMBOL); return fallback.get_sym(k, _default); } diff --git a/src/util/symbol.cpp b/src/util/symbol.cpp index 42663c050..febe79dbb 100644 --- a/src/util/symbol.cpp +++ b/src/util/symbol.cpp @@ -16,6 +16,11 @@ Author: Revision History: --*/ +#if 0 + + // include "util/new_symbol.cpp" +#else + #include "util/symbol.h" #include "util/mutex.h" #include "util/str_hashtable.h" @@ -25,6 +30,7 @@ Revision History: #include + symbol symbol::m_dummy(TAG(void*, nullptr, 2)); const symbol symbol::null; @@ -145,7 +151,7 @@ bool symbol::contains(char ch) const { } } -unsigned symbol::size() const { +unsigned symbol::display_size() const { SASSERT(!is_marked()); if (GET_TAG(m_data) == 0) { return static_cast(strlen(m_data)); @@ -183,3 +189,5 @@ bool lt(symbol const & s1, symbol const & s2) { SASSERT(cmp != 0); return cmp < 0; } + +#endif diff --git a/src/util/symbol.h b/src/util/symbol.h index 90a4eeb38..f902e80d7 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -16,6 +16,9 @@ Author: Revision History: --*/ +#if 0 + // include "util/new_symbol.h" +#else #ifndef SYMBOL_H_ #define SYMBOL_H_ #include @@ -66,6 +69,7 @@ public: friend bool operator==(symbol const & s1, symbol const & s2) { return s1.m_data == s2.m_data; } friend bool operator!=(symbol const & s1, symbol const & s2) { return s1.m_data != s2.m_data; } bool is_numerical() const { return GET_TAG(m_data) == 1; } + bool is_null() const { return m_data == nullptr; } unsigned int get_num() const { SASSERT(is_numerical()); return UNBOXINT(m_data); } std::string str() const; friend bool operator==(symbol const & s1, char const * s2) { @@ -78,11 +82,10 @@ public: return s1.str() == s2; } friend bool operator!=(symbol const & s1, char const * s2) { return !operator==(s1, s2); } - void const * c_ptr() const { return m_data; } - // Low level function. - // It is the inverse of c_ptr(). - // It was made public to simplify the implementation of the C API. - static symbol mk_symbol_from_c_ptr(void const * ptr) { + + // C-API only functions + void * c_api_symbol2ext() const { return const_cast(m_data); } + static symbol c_api_ext2symbol(void const * ptr) { return symbol(ptr); } unsigned hash() const { @@ -91,7 +94,7 @@ public: else return static_cast(reinterpret_cast(m_data)[-1]); } bool contains(char c) const; - unsigned size() const; + unsigned display_size() const; char const * bare_str() const { SASSERT(!is_numerical()); return m_data; } friend std::ostream & operator<<(std::ostream & target, symbol s) { SASSERT(!s.is_marked()); @@ -153,3 +156,4 @@ bool lt(symbol const & s1, symbol const & s2); #endif /* SYMBOL_H_ */ +#endif