mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

fix formatting bug reported by Alex Nutz

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-05-30 22:19:42 +02:00
parent 621f1f8a85
commit d59bf55539
3 changed files with 16 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/cmd_context/cmd_context.cpp
View file

@ -508,7 +508,10 @@ public:
m_owner.m_func_decls.contains(s); m_owner.m_func_decls.contains(s);
} }
format_ns::format * pp_sort(sort * s) override { format_ns::format * pp_sort(sort * s) override {
return m_owner.pp(s); auto * f = m_owner.pp(s);
if (f)
return f;
return smt2_pp_environment::pp_sort(s);
} }
format_ns::format * pp_fdecl(func_decl * f, unsigned & len) override { format_ns::format * pp_fdecl(func_decl * f, unsigned & len) override {
symbol s = f->get_name(); symbol s = f->get_name();
@ -2262,7 +2265,7 @@ bool cmd_context::is_model_available(model_ref& md) const {
format_ns::format * cmd_context::pp(sort * s) const { format_ns::format * cmd_context::pp(sort * s) const {
TRACE("cmd_context", tout << "pp(sort * s), s: " << mk_pp(s, m()) << "\n";); TRACE("cmd_context", tout << "pp(sort * s), s: " << mk_pp(s, m()) << "\n";);
return pm().pp(s); return pm().pp(get_pp_env(), s);
} }
cmd_context::pp_env & cmd_context::get_pp_env() const { cmd_context::pp_env & cmd_context::get_pp_env() const {

35
src/cmd_context/pdecl.cpp
View file

@ -785,7 +785,7 @@ struct pdecl_manager::sort_info {
virtual unsigned obj_size() const { return sizeof(sort_info); } virtual unsigned obj_size() const { return sizeof(sort_info); }
virtual void finalize(pdecl_manager & m) { m.dec_ref(m_decl); } virtual void finalize(pdecl_manager & m) { m.dec_ref(m_decl); }
virtual void display(std::ostream & out, pdecl_manager const & m) const = 0; virtual void display(std::ostream & out, pdecl_manager const & m) const = 0;
virtual format * pp(pdecl_manager const & m) const = 0; virtual format * pp(smt2_pp_environment& env, pdecl_manager const & m) const = 0;
}; };
struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info { struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
@ -817,14 +817,14 @@ struct pdecl_manager::app_sort_info : public pdecl_manager::sort_info {
} }
} }
format * pp(pdecl_manager const & m) const override { format * pp(smt2_pp_environment& env, pdecl_manager const & m) const override {
if (m_args.empty()) { if (m_args.empty()) {
return mk_string(m.m(), m_decl->get_name().str()); return mk_string(m.m(), m_decl->get_name().str());
} }
else { else {
ptr_buffer<format> b; ptr_buffer<format> b;
for (auto arg : m_args) for (auto arg : m_args)
b.push_back(m.pp(arg)); b.push_back(m.pp(env, arg));
return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str()); return mk_seq1(m.m(), b.begin(), b.end(), f2f(), m_decl->get_name().str());
} }
} }
@ -853,7 +853,7 @@ struct pdecl_manager::indexed_sort_info : public pdecl_manager::sort_info {
} }
} }
format * pp(pdecl_manager const & m) const override { format * pp(smt2_pp_environment& env, pdecl_manager const & m) const override {
if (m_indices.empty()) { if (m_indices.empty()) {
return mk_string(m.m(), m_decl->get_name().str()); return mk_string(m.m(), m_decl->get_name().str());
} }
@ -1072,27 +1072,10 @@ void pdecl_manager::display(std::ostream & out, sort * s) const {
out << s->get_name(); out << s->get_name();
} }
format * pdecl_manager::pp(sort * s) const { format * pdecl_manager::pp(smt2_pp_environment& env, sort * s) const {
sort_info * info = nullptr; sort_info * info = nullptr;
if (m_sort2info.find(s, info)) { if (m_sort2info.find(s, info))
return info->pp(*this); return info->pp(env, *this);
} else
unsigned num_params = s->get_num_parameters(); return nullptr;
if (s->get_family_id() != null_family_id && num_params > 0) {
// Small hack to display FP and BitVec sorts that were not explicitly referenced by the user.
unsigned i = 0;
for (i = 0; i < num_params; i++) {
if (!s->get_parameter(i).is_int())
break;
}
if (i == num_params) {
// all parameters are integer
ptr_buffer<format> b;
b.push_back(mk_string(m(), s->get_name().str()));
for (unsigned i = 0; i < num_params; i++)
b.push_back(mk_unsigned(m(), s->get_parameter(i).get_int()));
return mk_seq1(m(), b.begin(), b.end(), f2f(), "_");
}
}
return mk_string(m(), s->get_name().str());
} }

3
src/cmd_context/pdecl.h
View file

@ -23,6 +23,7 @@ Revision History:
#include "util/dictionary.h" #include "util/dictionary.h"
#include "ast/format.h" #include "ast/format.h"
#include "ast/datatype_decl_plugin.h" #include "ast/datatype_decl_plugin.h"
#include "ast/ast_smt2_pp.h"
class pdecl_manager; class pdecl_manager;
@ -333,7 +334,7 @@ public:
void save_info(sort * s, psort_decl * d, unsigned num_args, sort * const * args); void save_info(sort * s, psort_decl * d, unsigned num_args, sort * const * args);
void save_info(sort * s, psort_decl * d, unsigned num_indices, unsigned const * indices); void save_info(sort * s, psort_decl * d, unsigned num_indices, unsigned const * indices);
void display(std::ostream & out, sort * s) const; void display(std::ostream & out, sort * s) const;
format_ns::format * pp(sort * s) const; format_ns::format * pp(smt2_pp_environment& env, sort * s) const;
}; };