From 011c1b2dd2bd394ac043668e289bfdabbe2b1f27 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 9 Apr 2022 12:06:27 +0200 Subject: [PATCH] remove refs to bare_str --- src/api/api_ast.cpp | 2 +- src/api/api_log.cpp | 2 +- src/api/api_tactic.cpp | 6 +-- src/ast/ast_smt2_pp.cpp | 12 ++---- src/cmd_context/basic_cmds.cpp | 2 +- src/muz/fp/datalog_parser.cpp | 40 ++++++++++--------- src/muz/rel/dl_finite_product_relation.cpp | 2 +- src/muz/rel/dl_instruction.cpp | 20 +++++----- src/muz/rel/dl_table_relation.cpp | 2 +- src/muz/rel/rel_context.cpp | 2 +- src/tactic/portfolio/smt_strategic_solver.cpp | 5 +-- 11 files changed, 46 insertions(+), 49 deletions(-) diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index d5de6b5fb32..8144c2baf6a 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -355,7 +355,7 @@ extern "C" { return mk_c(c)->mk_external_string(buffer.str()); } else { - return mk_c(c)->mk_external_string(_s.bare_str()); + return mk_c(c)->mk_external_string(_s.str()); } Z3_CATCH_RETURN(""); } diff --git a/src/api/api_log.cpp b/src/api/api_log.cpp index c1864ae8c8d..ed5f68e8a20 100644 --- a/src/api/api_log.cpp +++ b/src/api/api_log.cpp @@ -88,7 +88,7 @@ void Sy(Z3_symbol sym) { *g_z3_log << "# " << s.get_num(); } else { - *g_z3_log << "$ |" << ll_escaped{s.bare_str()} << '|'; + *g_z3_log << "$ |" << ll_escaped{s.str().c_str()} << '|'; } *g_z3_log << std::endl; } diff --git a/src/api/api_tactic.cpp b/src/api/api_tactic.cpp index 45073cdb1dd..f67a373dd14 100644 --- a/src/api/api_tactic.cpp +++ b/src/api/api_tactic.cpp @@ -331,8 +331,8 @@ extern "C" { if (idx >= mk_c(c)->num_tactics()) { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; - } - return mk_c(c)->get_tactic(idx)->get_name().bare_str(); + } + return mk_c(c)->mk_external_string(mk_c(c)->get_tactic(idx)->get_name().str().c_str()); Z3_CATCH_RETURN(""); } @@ -352,7 +352,7 @@ extern "C" { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; } - return mk_c(c)->get_probe(idx)->get_name().bare_str(); + return mk_c(c)->mk_external_string(mk_c(c)->get_probe(idx)->get_name().str().c_str()); Z3_CATCH_RETURN(""); } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index 9854195a477..59f9ecda639 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -47,18 +47,14 @@ format * smt2_pp_environment::pp_fdecl_name(symbol const & s, unsigned & len, bo len = static_cast(str.length()); return mk_string(m, str); } - else if (s.is_numerical()) { - std::string str = s.str(); - len = static_cast(str.length()); - return mk_string(m, str); - } - else if (!s.bare_str()) { + else if (s.is_null()) { len = 4; return mk_string(m, "null"); } else { - len = static_cast(strlen(s.bare_str())); - return mk_string(m, s.bare_str()); + std::string str = s.str(); + len = static_cast(str.length()); + return mk_string(m, str); } } diff --git a/src/cmd_context/basic_cmds.cpp b/src/cmd_context/basic_cmds.cpp index afe800af6dc..f3bd0ed5702 100644 --- a/src/cmd_context/basic_cmds.cpp +++ b/src/cmd_context/basic_cmds.cpp @@ -58,7 +58,7 @@ class help_cmd : public cmd { cmd * c = ctx.find_cmd(s); if (c == nullptr) { std::string err_msg("unknown command '"); - err_msg = err_msg + s.bare_str() + "'"; + err_msg = err_msg + s.str() + "'"; throw cmd_exception(std::move(err_msg)); } m_cmds.push_back(s); diff --git a/src/muz/fp/datalog_parser.cpp b/src/muz/fp/datalog_parser.cpp index 899ec497c2e..030d88d71d1 100644 --- a/src/muz/fp/datalog_parser.cpp +++ b/src/muz/fp/datalog_parser.cpp @@ -777,6 +777,7 @@ class dparser : public parser { // Sym ::= String | NUM | Var // dtoken parse_infix(dtoken tok1, char const* td, app_ref& pred) { + std::string td1_(td); symbol td1(td); expr_ref v1(m), v2(m); sort* s = nullptr; @@ -793,12 +794,12 @@ class dparser : public parser { if (tok1 == TK_ID) { expr* _v1 = nullptr; - m_vars.find(td1.bare_str(), _v1); + m_vars.find(td1_, _v1); v1 = _v1; } if (tok3 == TK_ID) { expr* _v2 = nullptr; - m_vars.find(td2.bare_str(), _v2); + m_vars.find(td, _v2); v2 = _v2; } if (!v1 && !v2) { @@ -950,18 +951,19 @@ class dparser : public parser { break; } case TK_ID: { - symbol data (m_lexer->get_token_data()); - if (is_var(data.bare_str())) { + char const* d = m_lexer->get_token_data(); + symbol data (d); + if (is_var(d)) { unsigned idx = 0; expr* v = nullptr; - if (!m_vars.find(data.bare_str(), v)) { + if (!m_vars.find(d, v)) { idx = m_num_vars++; v = m.mk_var(idx, s); - m_vars.insert(data.bare_str(), v); + m_vars.insert(d, v); } else if (s != v->get_sort()) { throw default_exception(default_exception::fmt(), "sort: %s expected, but got: %s\n", - s->get_name().bare_str(), v->get_sort()->get_name().bare_str()); + s->get_name().str().c_str(), v->get_sort()->get_name().str().c_str()); } args.push_back(v); } @@ -1075,21 +1077,21 @@ class dparser : public parser { } sort * register_finite_sort(symbol name, uint64_t domain_size, context::sort_kind k) { - if(m_sort_dict.contains(name.bare_str())) { - throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str()); + if(m_sort_dict.contains(name.str().c_str())) { + throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str()); } sort * s = m_decl_util.mk_sort(name, domain_size); m_context.register_finite_sort(s, k); - m_sort_dict.insert(name.bare_str(), s); + m_sort_dict.insert(name.str(), s); return s; } sort * register_int_sort(symbol name) { - if(m_sort_dict.contains(name.bare_str())) { - throw default_exception(default_exception::fmt(), "sort %s already declared", name.bare_str()); + if(m_sort_dict.contains(name.str().c_str())) { + throw default_exception(default_exception::fmt(), "sort %s already declared", name.str().c_str()); } sort * s = m_arith.mk_int(); - m_sort_dict.insert(name.bare_str(), s); + m_sort_dict.insert(name.str(), s); return s; } @@ -1105,8 +1107,8 @@ class dparser : public parser { app * res; if(m_arith.is_int(s)) { uint64_t val; - if (!string_to_uint64(name.bare_str(), val)) { - throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.bare_str()); + if (!string_to_uint64(name.str().c_str(), val)) { + throw default_exception(default_exception::fmt(), "Invalid integer: \"%s\"", name.str().c_str()); } res = m_arith.mk_numeral(rational(val, rational::ui64()), s); } @@ -1288,7 +1290,7 @@ class wpa_parser_impl : public wpa_parser, dparser { uint64_set & sort_content = *e->get_data().m_value; if(!sort_content.contains(num)) { warning_msg("symbol number %I64u on line %d in file %s does not belong to sort %s", - num, m_current_line, m_current_file.c_str(), s->get_name().bare_str()); + num, m_current_line, m_current_file.c_str(), s->get_name().str().c_str()); return false; } if(!m_use_map_names) { @@ -1366,7 +1368,7 @@ class wpa_parser_impl : public wpa_parser, dparser { func_decl * pred = m_context.try_get_predicate_decl(predicate_name); if(!pred) { throw default_exception(default_exception::fmt(), "tuple file %s for undeclared predicate %s", - m_current_file.c_str(), predicate_name.bare_str()); + m_current_file.c_str(), predicate_name.str().c_str()); } unsigned pred_arity = pred->get_arity(); sort * const * arg_sorts = pred->get_domain(); @@ -1531,9 +1533,9 @@ class wpa_parser_impl : public wpa_parser, dparser { if(m_use_map_names) { auto const & value = m_number_names.insert_if_not_there(num, el_name); - if (value!=el_name) { + if (value != el_name) { warning_msg("mismatch of number names on line %d in file %s. old: \"%s\" new: \"%s\"", - m_current_line, fname.c_str(), value.bare_str(), el_name.bare_str()); + m_current_line, fname.c_str(), value.str().c_str(), el_name.str().c_str()); } } } diff --git a/src/muz/rel/dl_finite_product_relation.cpp b/src/muz/rel/dl_finite_product_relation.cpp index 8a4b86e6d47..07921a3be26 100644 --- a/src/muz/rel/dl_finite_product_relation.cpp +++ b/src/muz/rel/dl_finite_product_relation.cpp @@ -64,7 +64,7 @@ namespace datalog { } symbol finite_product_relation_plugin::get_name(relation_plugin & inner_plugin) { - std::string str = std::string("fpr_")+inner_plugin.get_name().bare_str(); + std::string str = std::string("fpr_")+inner_plugin.get_name().str(); return symbol(str.c_str()); } diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index 0df03172fe2..63846e7d571 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -213,10 +213,10 @@ namespace datalog { return true; } void make_annotations(execution_context & ctx) override { - ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); + ctx.set_register_annotation(m_reg, m_pred->get_name().str().c_str()); } std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { - const char * rel_name = m_pred->get_name().bare_str(); + auto rel_name = m_pred->get_name(); if (m_store) { return out << "store " << m_reg << " into " << rel_name; } @@ -378,7 +378,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported join operation on relations of kinds %s and %s", - r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str()); + r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str()); } store_fn(r1, r2, fn); } @@ -441,7 +441,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_equal operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -490,7 +490,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_identical operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -537,7 +537,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_interpreted operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -594,7 +594,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported filter_interpreted_and_project operation on a relation of kind %s", - reg.get_plugin().get_name().bare_str()); + reg.get_plugin().get_name().str().c_str()); } store_fn(reg, fn); } @@ -837,7 +837,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported join-project operation on relations of kinds %s and %s", - r1.get_plugin().get_name().bare_str(), r2.get_plugin().get_name().bare_str()); + r1.get_plugin().get_name().str().c_str(), r2.get_plugin().get_name().str().c_str()); } store_fn(r1, r2, fn); } @@ -910,7 +910,7 @@ namespace datalog { if (!fn) { throw default_exception(default_exception::fmt(), "trying to perform unsupported select_equal_and_project operation on a relation of kind %s", - r.get_plugin().get_name().bare_str()); + r.get_plugin().get_name().str().c_str()); } store_fn(r, fn); } @@ -1076,7 +1076,7 @@ namespace datalog { return true; } std::ostream& display_head_impl(execution_context const& ctx, std::ostream & out) const override { - return out << "mark_saturated " << m_pred->get_name().bare_str(); + return out << "mark_saturated " << m_pred->get_name(); } void make_annotations(execution_context & ctx) override { } diff --git a/src/muz/rel/dl_table_relation.cpp b/src/muz/rel/dl_table_relation.cpp index de55998f88f..8a69f8f85a6 100644 --- a/src/muz/rel/dl_table_relation.cpp +++ b/src/muz/rel/dl_table_relation.cpp @@ -33,7 +33,7 @@ namespace datalog { // ----------------------------------- symbol table_relation_plugin::create_plugin_name(const table_plugin &p) { - std::string name = std::string("tr_") + p.get_name().bare_str(); + std::string name = std::string("tr_") + p.get_name().str(); return symbol(name.c_str()); } diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index 957c85adb0a..76411a290b1 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -157,7 +157,7 @@ namespace datalog { //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream());); if (m_context.print_aig().is_non_empty_string()) { - const char *filename = m_context.print_aig().bare_str(); + std::string filename = m_context.print_aig().str(); aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts); std::ofstream strm(filename, std::ios_base::binary); aig(strm); diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp index 52df3824753..0c304aa3f4c 100644 --- a/src/tactic/portfolio/smt_strategic_solver.cpp +++ b/src/tactic/portfolio/smt_strategic_solver.cpp @@ -143,10 +143,9 @@ class smt_strategic_solver_factory : public solver_factory { tactic_ref t; if (tp.default_tactic() != symbol::null && !tp.default_tactic().is_numerical() && - tp.default_tactic().bare_str() && - tp.default_tactic().bare_str()[0]) { + tp.default_tactic().str()[0]) { cmd_context ctx(false, &m, l); - std::istringstream is(tp.default_tactic().bare_str()); + std::istringstream is(tp.default_tactic().str()); char const* file_name = ""; sexpr_ref se = parse_sexpr(ctx, is, p, file_name); if (se) {