remove refs to bare_str

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("");
     }

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;
 }

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("");
     }
 

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<unsigned>(str.length());
         return mk_string(m, str);
     }
-    else if (s.is_numerical()) {
-        std::string str = s.str();
-        len = static_cast<unsigned>(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<unsigned>(strlen(s.bare_str()));
-        return mk_string(m, s.bare_str());
+        std::string str = s.str();
+        len = static_cast<unsigned>(str.length());
+        return mk_string(m, str);
     }
 }
 

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);

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());
                 }
             }
         }

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());
     }
 

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 {
         }

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());
     }
 

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);

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) {