From d6de73a2d10135d5fb036787888380352c2bc3a0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Jul 2014 18:11:57 +0200 Subject: [PATCH] fix model converter in inliner. Bug reported by Sagar Chaki Signed-off-by: Nikolaj Bjorner --- src/api/z3_api.h | 3 ++- src/muz/base/dl_util.cpp | 2 +- src/muz/transforms/dl_mk_rule_inliner.cpp | 5 +++++ 3 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/api/z3_api.h b/src/api/z3_api.h index b29a9c87d..94e20eceb 100644 --- a/src/api/z3_api.h +++ b/src/api/z3_api.h @@ -5668,7 +5668,8 @@ END_MLAPI_EXCLUDE Each conjunct encodes values of the bound variables of the query that are satisfied. In PDR mode, the returned answer is a single conjunction. - The previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE. + When used in Datalog mode the previous call to Z3_fixedpoint_query must have returned Z3_L_TRUE. + When used with the PDR engine, the previous call must have been either Z3_L_TRUE or Z3_L_FALSE. def_API('Z3_fixedpoint_get_answer', AST, (_in(CONTEXT), _in(FIXEDPOINT))) */ diff --git a/src/muz/base/dl_util.cpp b/src/muz/base/dl_util.cpp index 218f9906a..a6647a1d2 100644 --- a/src/muz/base/dl_util.cpp +++ b/src/muz/base/dl_util.cpp @@ -290,7 +290,7 @@ namespace datalog { } } TRACE("dl_dr", - tout << r.get_decl()->get_name() << "\n"; + tout << mk_pp(r.get_head(), m) << " :- \n"; for (unsigned i = 0; i < body.size(); ++i) { tout << mk_pp(body[i].get(), m) << "\n"; }); diff --git a/src/muz/transforms/dl_mk_rule_inliner.cpp b/src/muz/transforms/dl_mk_rule_inliner.cpp index d9dad5c56..712c82feb 100644 --- a/src/muz/transforms/dl_mk_rule_inliner.cpp +++ b/src/muz/transforms/dl_mk_rule_inliner.cpp @@ -423,6 +423,11 @@ namespace datalog { } TRACE("dl", tout << "inlined rules after mutual inlining:\n" << m_inlined_rules; ); + + for (unsigned i = 0; i < m_inlined_rules.get_num_rules(); ++i) { + rule* r = m_inlined_rules.get_rule(i); + datalog::del_rule(m_mc, *r); + } } bool mk_rule_inliner::transform_rule(rule_set const& orig, rule * r0, rule_set& tgt) {