mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-05 21:53:23 +00:00
Code Activity

delay rule flushing so that pretty printing retains original format of rules

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-11-20 15:30:22 -08:00
parent 2c54bbba5f
commit a38a7ab506
2 changed files with 24 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

22
src/muz_qe/dl_context.cpp
View file

@ -238,6 +238,7 @@ namespace datalog {
m_pinned(m), m_pinned(m),
m_vars(m), m_vars(m),
m_rule_set(*this), m_rule_set(*this),
m_rule_fmls(m),
m_background(m), m_background(m),
m_closed(false), m_closed(false),
m_saturation_was_run(false), m_saturation_was_run(false),
@ -521,10 +522,19 @@ namespace datalog {
} }
void context::add_rule(expr* rl, symbol const& name) { void context::add_rule(expr* rl, symbol const& name) {
m_rule_fmls.push_back(rl);
m_rule_names.push_back(name);
}
void context::flush_add_rules() {
datalog::rule_manager& rm = get_rule_manager(); datalog::rule_manager& rm = get_rule_manager();
datalog::rule_ref_vector rules(rm); datalog::rule_ref_vector rules(rm);
rm.mk_rule(rl, rules, name); for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]);
}
add_rules(rules); add_rules(rules);
m_rule_fmls.reset();
m_rule_names.reset();
} }
// //
@ -1223,6 +1233,7 @@ namespace datalog {
} }
void context::new_query() { void context::new_query() {
flush_add_rules();
if (m_last_result_relation) { if (m_last_result_relation) {
m_last_result_relation->deallocate(); m_last_result_relation->deallocate();
m_last_result_relation = 0; m_last_result_relation = 0;
@ -1618,6 +1629,10 @@ namespace datalog {
names.push_back((*it)->name()); 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;
@ -1674,8 +1689,11 @@ namespace datalog {
declare_vars(rules, fresh_names, out); declare_vars(rules, fresh_names, out);
} }
if (num_axioms > 0 && !use_fixedpoint_extensions) {
throw default_exception("Background axioms cannot be used with SMT-LIB2 HORN format");
}
for (unsigned i = 0; i < num_axioms; ++i) { for (unsigned i = 0; i < num_axioms; ++i) {
SASSERT(use_fixedpoint_extensions);
out << "(assert "; out << "(assert ";
ast_smt2_pp(out, axioms[i], env, params); ast_smt2_pp(out, axioms[i], env, params);
out << ")\n"; out << ")\n";

4
src/muz_qe/dl_context.h
View file

@ -96,6 +96,8 @@ namespace datalog {
pred2syms m_argument_var_names; pred2syms m_argument_var_names;
decl_set m_output_preds; decl_set m_output_preds;
rule_set m_rule_set; rule_set m_rule_set;
expr_ref_vector m_rule_fmls;
svector<symbol> m_rule_names;
expr_ref_vector m_background; expr_ref_vector m_background;
scoped_ptr<pdr::dl_interface> m_pdr; scoped_ptr<pdr::dl_interface> m_pdr;
@ -454,6 +456,8 @@ namespace datalog {
private: private:
void flush_add_rules();
void ensure_pdr(); void ensure_pdr();
void ensure_bmc(); void ensure_bmc();