mirror of
https://github.com/Z3Prover/z3
synced 2025-04-05 17:14:07 +00:00
This commit is contained in:
parent
ae24b73b19
commit
d4ca7e5374
|
@ -1265,6 +1265,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environmen
|
|||
return out;
|
||||
}
|
||||
|
||||
|
||||
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd, bool reverse) {
|
||||
if (!f) return out << "null";
|
||||
ast_manager & m = env.get_manager();
|
||||
|
@ -1276,6 +1277,13 @@ std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_e
|
|||
return out;
|
||||
}
|
||||
|
||||
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd) {
|
||||
return ast_smt2_pp(out, f, e, env, p, indent, cmd, false);
|
||||
}
|
||||
|
||||
std::ostream & ast_smt2_pp_rev(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p, unsigned indent, char const* cmd) {
|
||||
return ast_smt2_pp(out, f, e, env, p, indent, cmd, true);
|
||||
}
|
||||
|
||||
std::ostream & ast_smt2_pp(std::ostream & out, unsigned sz, expr * const* es, smt2_pp_environment & env, params_ref const & p, unsigned indent,
|
||||
unsigned num_vars, char const * var_prefix) {
|
||||
|
|
|
@ -105,6 +105,7 @@ std::ostream & ast_smt2_pp(std::ostream & out, expr * n, smt2_pp_environment & e
|
|||
std::ostream & ast_smt2_pp(std::ostream & out, sort * s, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0);
|
||||
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "declare-fun");
|
||||
std::ostream & ast_smt2_pp(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun", bool reverse = false);
|
||||
std::ostream & ast_smt2_pp_rev(std::ostream & out, func_decl * f, expr* e, smt2_pp_environment & env, params_ref const & p = params_ref(), unsigned indent = 0, char const* cmd = "define-fun");
|
||||
std::ostream & ast_smt2_pp(std::ostream & out, symbol const& s, bool is_skolem, smt2_pp_environment & env, params_ref const& p = params_ref());
|
||||
std::ostream & ast_smt2_pp_recdefs(std::ostream & out, vector<std::pair<func_decl*, expr*>> const& funs, smt2_pp_environment & env, params_ref const & p = params_ref());
|
||||
|
||||
|
|
|
@ -26,7 +26,7 @@ Notes:
|
|||
void model_converter::display_add(std::ostream& out, smt2_pp_environment& env, ast_manager& m, func_decl* f, expr* e) {
|
||||
VERIFY(e);
|
||||
VERIFY(f->get_range() == e->get_sort());
|
||||
ast_smt2_pp(out, f, e, env, params_ref(), 0, "model-add", true) << "\n";
|
||||
ast_smt2_pp_rev(out, f, e, env, params_ref(), 0, "model-add") << "\n";
|
||||
}
|
||||
|
||||
void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {
|
||||
|
|
Loading…
Reference in a new issue