mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

fix up convertion and printing

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-12-29 10:24:48 -08:00
parent c80f34102f
commit 444e178a01
2 changed files with 10 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_solver.cpp
View file

@ -131,6 +131,7 @@ extern "C" {
void Z3_API Z3_solver_import_model_converter(Z3_context c, Z3_solver src, Z3_solver dst) {
Z3_TRY;
LOG_Z3_solver_import_model_converter(c, src, dst);
std::cout << "import converter\n";
model_converter_ref mc = to_solver_ref(src)->get_model_converter();
to_solver_ref(dst)->set_model_converter(mc.get());
Z3_CATCH;

13
src/tactic/model_converter.cpp
View file

@ -24,16 +24,21 @@ Notes:
* Add or overwrite value in model.
*/
void model_converter::display_add(std::ostream& out, ast_manager& m, func_decl* f, expr* e) const {
VERIFY(m_env);
ast_smt2_pp(out, f, e, *m_env, params_ref(), 0, "model-add") << "\n";
smt2_pp_environment_dbg env(m);
smt2_pp_environment* _env = m_env ? m_env : &env;
ast_smt2_pp(out, f, e, *_env, params_ref(), 0, "model-add") << "\n";
}
/*
* A value is removed from the model.
*/
void model_converter::display_del(std::ostream& out, func_decl* f) const {
VERIFY(m_env);
ast_smt2_pp(out << "(model-del ", f->get_name(), f->is_skolem(), *m_env) << ")\n";
if (m_env) {
ast_smt2_pp(out << "(model-del ", f->get_name(), f->is_skolem(), *m_env) << ")\n";
}
else {
out << "(model-del " << f->get_name() << ")\n";
}
}
void model_converter::display_add(std::ostream& out, ast_manager& m) {