mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-13 17:36:15 +00:00
Code Activity

fix multiple bugs in interfacing with fixedpoint context

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-22 13:46:12 -08:00
parent fcdde59438
commit 7d9254f122
4 changed files with 40 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

18
src/api/api_datalog.cpp
View file

@ -363,6 +363,12 @@ extern "C" {
for (unsigned i = 0; i < coll.m_rules.size(); ++i) { 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]); to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
} }
ptr_vector<expr>::const_iterator it = ctx.begin_assertions();
ptr_vector<expr>::const_iterator end = ctx.end_assertions();
for (; it != end; ++it) {
to_fixedpoint_ref(d)->ctx().assert_expr(*it);
}
return of_ast_vector(v); return of_ast_vector(v);
} }
@ -439,12 +445,12 @@ extern "C" {
ast_manager& m = mk_c(c)->m(); ast_manager& m = mk_c(c)->m();
Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m); Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
mk_c(c)->save_object(v); mk_c(c)->save_object(v);
datalog::rule_set const& rules = to_fixedpoint_ref(d)->ctx().get_rules(); expr_ref_vector rules(m);
datalog::rule_set::iterator it = rules.begin(), end = rules.end(); svector<symbol> names;
for (; it != end; ++it) {
expr_ref fml(m); to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, names);
(*it)->to_formula(fml); for (unsigned i = 0; i < rules.size(); ++i) {
v->m_ast_vector.push_back(fml); v->m_ast_vector.push_back(rules[i].get());
} }
RETURN_Z3(of_ast_vector(v)); RETURN_Z3(of_ast_vector(v));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);

3
src/api/python/z3.py
View file

@ -825,7 +825,8 @@ class ExprRef(AstRef):
if is_app(self): if is_app(self):
return [self.arg(i) for i in range(self.num_args())] return [self.arg(i) for i in range(self.num_args())]
else: else:
return [] return []
def _to_expr_ref(a, ctx): def _to_expr_ref(a, ctx):
if isinstance(a, Pattern): if isinstance(a, Pattern):

39
src/muz_qe/dl_context.cpp
View file

@ -352,11 +352,12 @@ namespace datalog {
svector<symbol> names; svector<symbol> names;
for (unsigned i = 0; i < sorts.size(); ++i) { for (unsigned i = 0; i < sorts.size(); ++i) {
if (!sorts[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); quantifier_ref q(m);
sorts.reverse();
q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result); q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result);
elim_unused_vars(m, q, result); elim_unused_vars(m, q, result);
} }
@ -1602,11 +1603,27 @@ namespace datalog {
for (unsigned i = 0; i < sz; ++i) { for (unsigned i = 0; i < sz; ++i) {
expr* e = exprs[i]; expr* e = exprs[i];
for_each_expr(v, visited, e); 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); fresh_names.add(e);
} }
} }
void context::get_rules_as_formulas(expr_ref_vector& rules, svector<symbol>& 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( void context::display_smt2(
unsigned num_queries, unsigned num_queries,
expr* const* queries, expr* const* queries,
@ -1621,18 +1638,8 @@ namespace datalog {
expr_ref_vector rules(m); expr_ref_vector rules(m);
svector<symbol> names; svector<symbol> names;
bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true); 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(); get_rules_as_formulas(rules, names);
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]);
}
smt2_pp_environment_dbg env(m); smt2_pp_environment_dbg env(m);
pp_params params; pp_params params;

4
src/muz_qe/dl_context.h
View file

@ -250,7 +250,9 @@ namespace datalog {
bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); } bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
const decl_set & get_output_predicates() const { return m_output_preds; } 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<symbol>& names);
void add_fact(app * head); void add_fact(app * head);
void add_fact(func_decl * pred, const relation_fact & fact); void add_fact(func_decl * pred, const relation_fact & fact);