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

make model and proof converters a reference

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2013-03-20 10:36:36 -07:00
parent 5455704af2
commit babfc701a6
7 changed files with 33 additions and 30 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/muz_qe/dl_bmc_engine.cpp
View file

@ -1420,13 +1420,15 @@ namespace datalog {
model_converter_ref mc = datalog::mk_skip_model_converter(); model_converter_ref mc = datalog::mk_skip_model_converter();
m_pc = datalog::mk_skip_proof_converter(); m_pc = datalog::mk_skip_proof_converter();
m_ctx.set_output_predicate(m_query_pred); m_ctx.set_output_predicate(m_query_pred);
m_ctx.apply_default_transformation(mc, m_pc); m_ctx.set_model_converter(mc);
m_ctx.set_proof_converter(m_pc);
m_ctx.apply_default_transformation();
if (m_ctx.get_params().slice()) { if (m_ctx.get_params().slice()) {
datalog::rule_transformer transformer(m_ctx); datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice); transformer.register_plugin(slice);
m_ctx.transform_rules(transformer, mc, m_pc); m_ctx.transform_rules(transformer);
m_query_pred = slice->get_predicate(m_query_pred.get()); m_query_pred = slice->get_predicate(m_query_pred.get());
m_ctx.set_output_predicate(m_query_pred); m_ctx.set_output_predicate(m_query_pred);
} }

12
src/muz_qe/dl_context.cpp
View file

@ -826,7 +826,7 @@ namespace datalog {
m_closed = false; m_closed = false;
} }
void context::transform_rules(model_converter_ref& mc, proof_converter_ref& pc) { void context::transform_rules() {
m_transf.reset(); m_transf.reset();
m_transf.register_plugin(alloc(mk_filter_rules,*this)); m_transf.register_plugin(alloc(mk_filter_rules,*this));
m_transf.register_plugin(alloc(mk_simple_joins,*this)); m_transf.register_plugin(alloc(mk_simple_joins,*this));
@ -841,13 +841,13 @@ namespace datalog {
} }
m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this)); m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
transform_rules(m_transf, mc, pc); transform_rules(m_transf);
} }
void context::transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc) { void context::transform_rules(rule_transformer& transf) {
SASSERT(m_closed); //we must finish adding rules before we start transforming them SASSERT(m_closed); //we must finish adding rules before we start transforming them
TRACE("dl", display_rules(tout);); TRACE("dl", display_rules(tout););
if (transf(m_rule_set, mc, pc)) { if (transf(m_rule_set, m_mc, m_pc)) {
//we have already ensured the negation is stratified and transformations //we have already ensured the negation is stratified and transformations
//should not break the stratification //should not break the stratification
m_rule_set.ensure_closed(); m_rule_set.ensure_closed();
@ -862,7 +862,7 @@ namespace datalog {
m_rule_set.add_rules(rs); m_rule_set.add_rules(rs);
} }
void context::apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc) { void context::apply_default_transformation() {
ensure_closed(); ensure_closed();
m_transf.reset(); m_transf.reset();
m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this)); m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this));
@ -890,7 +890,7 @@ namespace datalog {
m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000)); m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000)); m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010)); m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010));
transform_rules(m_transf, mc, pc); transform_rules(m_transf);
} }
void context::collect_params(param_descrs& p) { void context::collect_params(param_descrs& p) {

11
src/muz_qe/dl_context.h
View file

@ -97,6 +97,8 @@ namespace datalog {
expr_ref_vector m_rule_fmls; expr_ref_vector m_rule_fmls;
svector<symbol> m_rule_names; svector<symbol> m_rule_names;
expr_ref_vector m_background; expr_ref_vector m_background;
model_converter_ref m_mc;
proof_converter_ref m_pc;
scoped_ptr<pdr::dl_interface> m_pdr; scoped_ptr<pdr::dl_interface> m_pdr;
scoped_ptr<bmc> m_bmc; scoped_ptr<bmc> m_bmc;
@ -313,11 +315,14 @@ namespace datalog {
void reopen(); void reopen();
void ensure_opened(); void ensure_opened();
void transform_rules(model_converter_ref& mc, proof_converter_ref& pc); void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
void transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc); void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
void transform_rules(); // model_converter_ref& mc, proof_converter_ref& pc);
void transform_rules(rule_transformer& transf); // , model_converter_ref& mc, proof_converter_ref& pc);
void replace_rules(rule_set & rs); void replace_rules(rule_set & rs);
void apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc); void apply_default_transformation(); // model_converter_ref& mc, proof_converter_ref& pc);
void collect_params(param_descrs& r); void collect_params(param_descrs& r);

6
src/muz_qe/horn_tactic.cpp
View file

@ -282,14 +282,16 @@ class horn_tactic : public tactic {
func_decl* query_pred = to_app(q)->get_decl(); func_decl* query_pred = to_app(q)->get_decl();
m_ctx.set_output_predicate(query_pred); m_ctx.set_output_predicate(query_pred);
m_ctx.set_model_converter(mc);
m_ctx.set_proof_converter(pc);
m_ctx.get_rules(); // flush adding rules. m_ctx.get_rules(); // flush adding rules.
m_ctx.apply_default_transformation(mc, pc); m_ctx.apply_default_transformation();
if (m_ctx.get_params().slice()) { if (m_ctx.get_params().slice()) {
datalog::rule_transformer transformer(m_ctx); datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice); transformer.register_plugin(slice);
m_ctx.transform_rules(transformer, mc, pc); m_ctx.transform_rules(transformer);
} }
expr_substitution sub(m); expr_substitution sub(m);

12
src/muz_qe/pdr_dl_interface.cpp
View file

@ -111,13 +111,15 @@ lbool dl_interface::query(expr * query) {
pc = datalog::mk_skip_proof_converter(); pc = datalog::mk_skip_proof_converter();
} }
m_ctx.set_output_predicate(query_pred); m_ctx.set_output_predicate(query_pred);
m_ctx.apply_default_transformation(mc, pc); m_ctx.set_model_converter(mc);
m_ctx.set_proof_converter(pc);
m_ctx.apply_default_transformation();
if (m_ctx.get_params().slice()) { if (m_ctx.get_params().slice()) {
datalog::rule_transformer transformer(m_ctx); datalog::rule_transformer transformer(m_ctx);
datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx); datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
transformer.register_plugin(slice); transformer.register_plugin(slice);
m_ctx.transform_rules(transformer, mc, pc); m_ctx.transform_rules(transformer);
query_pred = slice->get_predicate(query_pred.get()); query_pred = slice->get_predicate(query_pred.get());
m_ctx.set_output_predicate(query_pred); m_ctx.set_output_predicate(query_pred);
@ -137,11 +139,11 @@ lbool dl_interface::query(expr * query) {
datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx); datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
if (m_ctx.get_params().coalesce_rules()) { if (m_ctx.get_params().coalesce_rules()) {
transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx)); transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
m_ctx.transform_rules(transformer1, mc, pc); m_ctx.transform_rules(transformer1);
} }
transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx)); transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
while (num_unfolds > 0) { while (num_unfolds > 0) {
m_ctx.transform_rules(transformer2, mc, pc); m_ctx.transform_rules(transformer2);
--num_unfolds; --num_unfolds;
} }
} }
@ -149,7 +151,7 @@ lbool dl_interface::query(expr * query) {
datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx); datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx);
datalog::rule_transformer extract_q_tr(m_ctx); datalog::rule_transformer extract_q_tr(m_ctx);
extract_q_tr.register_plugin(extract_quantifiers); extract_q_tr.register_plugin(extract_quantifiers);
m_ctx.transform_rules(extract_q_tr, mc, pc); m_ctx.transform_rules(extract_q_tr);
IF_VERBOSE(2, m_ctx.display_rules(verbose_stream());); IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););

12
src/muz_qe/rel_context.cpp
View file

@ -103,9 +103,7 @@ namespace datalog {
TRACE("dl", m_context.display(tout);); TRACE("dl", m_context.display(tout););
while (true) { while (true) {
model_converter_ref mc; // Ignored in Datalog mode m_context.transform_rules();
proof_converter_ref pc; // Ignored in Datalog mode
m_context.transform_rules(mc, pc);
compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code); compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code);
TRACE("dl", rules_code.display(*this, tout); ); TRACE("dl", rules_code.display(*this, tout); );
@ -263,14 +261,12 @@ namespace datalog {
reset_negated_tables(); reset_negated_tables();
if (m_context.generate_explanations()) { if (m_context.generate_explanations()) {
model_converter_ref mc; // ignored in Datalog mode
proof_converter_ref pc; // ignored in Datalog mode
rule_transformer transformer(m_context); rule_transformer transformer(m_context);
//expl_plugin is deallocated when transformer goes out of scope //expl_plugin is deallocated when transformer goes out of scope
mk_explanations * expl_plugin = mk_explanations * expl_plugin =
alloc(mk_explanations, m_context, m_context.explanations_on_relation_level()); alloc(mk_explanations, m_context, m_context.explanations_on_relation_level());
transformer.register_plugin(expl_plugin); transformer.register_plugin(expl_plugin);
m_context.transform_rules(transformer, mc, pc); m_context.transform_rules(transformer);
//we will retrieve the predicate with explanations instead of the original query predicate //we will retrieve the predicate with explanations instead of the original query predicate
query_pred = expl_plugin->get_e_decl(query_pred); query_pred = expl_plugin->get_e_decl(query_pred);
@ -280,11 +276,9 @@ namespace datalog {
} }
if (m_context.magic_sets_for_queries()) { if (m_context.magic_sets_for_queries()) {
model_converter_ref mc; // Ignored in Datalog mode
proof_converter_ref pc; // Ignored in Datalog mode
rule_transformer transformer(m_context); rule_transformer transformer(m_context);
transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get())); transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get()));
m_context.transform_rules(transformer, mc, pc); m_context.transform_rules(transformer);
} }
lbool res = saturate(); lbool res = saturate();

4
src/shell/datalog_frontend.cpp
View file

@ -200,9 +200,7 @@ unsigned read_datalog(char const * file) {
timeout = UINT_MAX; timeout = UINT_MAX;
} }
do { do {
model_converter_ref mc; // ignored ctx.transform_rules();
proof_converter_ref pc; // ignored
ctx.transform_rules(mc, pc);
datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code); datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);