From 7d9254f122534cee9df27a8526271cbcc36a9f7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 22 Nov 2012 13:46:12 -0800 Subject: [PATCH] fix multiple bugs in interfacing with fixedpoint context Signed-off-by: Nikolaj Bjorner --- src/api/api_datalog.cpp | 18 ++++++++++++------ src/api/python/z3.py | 3 ++- src/muz_qe/dl_context.cpp | 39 +++++++++++++++++++++++---------------- src/muz_qe/dl_context.h | 4 +++- 4 files changed, 40 insertions(+), 24 deletions(-) diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp index 52cdeaec9..0200a4405 100644 --- a/src/api/api_datalog.cpp +++ b/src/api/api_datalog.cpp @@ -363,6 +363,12 @@ extern "C" { for (unsigned i = 0; i < coll.m_rules.size(); ++i) { to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]); } + ptr_vector::const_iterator it = ctx.begin_assertions(); + ptr_vector::const_iterator end = ctx.end_assertions(); + for (; it != end; ++it) { + to_fixedpoint_ref(d)->ctx().assert_expr(*it); + } + return of_ast_vector(v); } @@ -439,12 +445,12 @@ extern "C" { ast_manager& m = mk_c(c)->m(); Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m); mk_c(c)->save_object(v); - datalog::rule_set const& rules = to_fixedpoint_ref(d)->ctx().get_rules(); - datalog::rule_set::iterator it = rules.begin(), end = rules.end(); - for (; it != end; ++it) { - expr_ref fml(m); - (*it)->to_formula(fml); - v->m_ast_vector.push_back(fml); + expr_ref_vector rules(m); + svector names; + + to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, names); + for (unsigned i = 0; i < rules.size(); ++i) { + v->m_ast_vector.push_back(rules[i].get()); } RETURN_Z3(of_ast_vector(v)); Z3_CATCH_RETURN(0); diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 21666f569..537717c40 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -825,7 +825,8 @@ class ExprRef(AstRef): if is_app(self): return [self.arg(i) for i in range(self.num_args())] else: - return [] + return [] + def _to_expr_ref(a, ctx): if isinstance(a, Pattern): diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp index 9a5f7280c..47d0dbe75 100644 --- a/src/muz_qe/dl_context.cpp +++ b/src/muz_qe/dl_context.cpp @@ -352,11 +352,12 @@ namespace datalog { svector names; for (unsigned i = 0; i < sorts.size(); ++i) { if (!sorts[i]) { - sorts[i] = m.mk_bool_sort(); + sorts[i] = vars[i]->get_decl()->get_range(); } - names.push_back(symbol(i)); + names.push_back(vars[i]->get_decl()->get_name()); } quantifier_ref q(m); + sorts.reverse(); q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result); elim_unused_vars(m, q, result); } @@ -1602,11 +1603,27 @@ namespace datalog { for (unsigned i = 0; i < sz; ++i) { expr* e = exprs[i]; for_each_expr(v, visited, e); - while (is_quantifier(e)) e = to_quantifier(e)->get_expr(); + while (is_quantifier(e)) { + e = to_quantifier(e)->get_expr(); + } fresh_names.add(e); } } - + + void context::get_rules_as_formulas(expr_ref_vector& rules, svector& names) { + expr_ref fml(m); + rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); + for (; it != end; ++it) { + (*it)->to_formula(fml); + rules.push_back(fml); + names.push_back((*it)->name()); + } + for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { + rules.push_back(m_rule_fmls[i].get()); + names.push_back(m_rule_names[i]); + } + } + void context::display_smt2( unsigned num_queries, expr* const* queries, @@ -1621,18 +1638,8 @@ namespace datalog { expr_ref_vector rules(m); svector names; bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true); - { - rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end(); - for (; it != end; ++it) { - (*it)->to_formula(fml); - rules.push_back(fml); - names.push_back((*it)->name()); - } - } - for (unsigned i = 0; i < m_rule_fmls.size(); ++i) { - rules.push_back(m_rule_fmls[i].get()); - names.push_back(m_rule_names[i]); - } + + get_rules_as_formulas(rules, names); smt2_pp_environment_dbg env(m); pp_params params; diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h index 3818052e2..903500cda 100644 --- a/src/muz_qe/dl_context.h +++ b/src/muz_qe/dl_context.h @@ -250,7 +250,9 @@ namespace datalog { bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); } const decl_set & get_output_predicates() const { return m_output_preds; } - rule_set const & get_rules() { return m_rule_set; } + rule_set const & get_rules() { flush_add_rules(); return m_rule_set; } + + void get_rules_as_formulas(expr_ref_vector& fmls, svector& names); void add_fact(app * head); void add_fact(func_decl * pred, const relation_fact & fact);