mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-14 04:48:45 +00:00
Code Activity

Datalog improvements:

Browse source 
- add cancel status
 - display statistics on cancel
(by me & Nikolaj)

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>
This commit is contained in:
Nuno Lopes 2013-03-27 10:38:50 -07:00
parent 25a41d48dc
commit 1cece1c1fb
10 changed files with 142 additions and 77 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

11
src/muz_qe/dl_cmds.cpp
View file

@ -234,7 +234,6 @@ public:
catch (z3_exception& ex) {
ctx.regular_stream() << "(error \"query failed: " << ex.msg() << "\")" << std::endl;
}
dlctx.cleanup();
}
switch (status) {
case l_false:
@ -250,6 +249,7 @@ public:
ctx.regular_stream() << "unknown\n";
switch(dlctx.get_status()) {
case datalog::INPUT_ERROR:
ctx.regular_stream() << "input error\n";
break;
case datalog::MEMOUT:
@ -261,14 +261,21 @@ public:
break;
case datalog::OK:
UNREACHABLE();
break;
case datalog::CANCELED:
ctx.regular_stream() << "canceled\n";
dlctx.display_profile(ctx.regular_stream());
break;
default:
// exception was raised.
UNREACHABLE();
break;
}
break;
}
dlctx.cleanup();
print_statistics(ctx);
m_target = 0;
}

25
src/muz_qe/dl_context.cpp
View file

@ -229,11 +229,13 @@ namespace datalog {
m_pinned(m),
m_vars(m),
m_rule_set(*this),
m_transformed_rule_set(*this),
m_rule_fmls(m),
m_background(m),
m_mc(0),
m_closed(false),
m_saturation_was_run(false),
m_last_status(OK),
m_last_answer(m),
m_engine(LAST_ENGINE),
m_cancel(false) {
@ -873,6 +875,11 @@ namespace datalog {
m_rule_set.add_rules(rs);
}
void context::record_transformed_rules() {
m_transformed_rule_set.reset();
m_transformed_rule_set.add_rules(m_rule_set);
}
void context::apply_default_transformation() {
ensure_closed();
m_transf.reset();
@ -942,18 +949,18 @@ namespace datalog {
void context::cancel() {
m_cancel = true;
m_last_status = CANCELED;
m_transf.cancel();
if (m_pdr.get()) m_pdr->cancel();
if (m_bmc.get()) m_bmc->cancel();
if (m_rel.get()) m_rel->cancel();
if (m_tab.get()) m_tab->cancel();
}
void context::cleanup() {
m_cancel = false;
m_last_status = OK;
if (m_pdr.get()) m_pdr->cleanup();
if (m_bmc.get()) m_bmc->cleanup();
if (m_rel.get()) m_rel->cleanup();
if (m_tab.get()) m_tab->cleanup();
}
@ -1178,6 +1185,20 @@ namespace datalog {
}
}
void context::display_profile(std::ostream& out) const {
out << "\n---------------\n";
out << "Original rules\n";
display_rules(out);
out << "\n---------------\n";
out << "Transformed rules\n";
m_transformed_rule_set.display(out);
if (m_rel) {
m_rel->display_profile(out);
}
}
void context::reset_statistics() {
if (m_pdr) {
m_pdr->reset_statistics();

8
src/muz_qe/dl_context.h
View file

@ -52,7 +52,8 @@ namespace datalog {
OK,
TIMEOUT,
MEMOUT,
INPUT_ERROR
INPUT_ERROR,
CANCELED
};
class context {
@ -92,6 +93,7 @@ namespace datalog {
sym2decl m_preds_by_name;
pred2syms m_argument_var_names;
rule_set m_rule_set;
rule_set m_transformed_rule_set;
expr_ref_vector m_rule_fmls;
svector<symbol> m_rule_names;
expr_ref_vector m_background;
@ -323,6 +325,7 @@ namespace datalog {
void transform_rules();
void transform_rules(rule_transformer& transf);
void replace_rules(rule_set & rs);
void record_transformed_rules();
void apply_default_transformation();
@ -349,6 +352,8 @@ namespace datalog {
void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out);
void display_profile(std::ostream& out) const;
// -----------------------------------
//
// basic usage methods
@ -356,6 +361,7 @@ namespace datalog {
// -----------------------------------
void cancel();
bool canceled() const { return m_cancel; }
void cleanup();
void reset_cancel() { cleanup(); }

59
src/muz_qe/dl_instruction.cpp
View file

@ -58,14 +58,18 @@ namespace datalog {
reset_timelimit();
}
rel_context& execution_context::get_rel_context() {
return m_context.get_rel_context();
}
struct compare_size_proc {
typedef std::pair<unsigned, unsigned> pr;
bool operator()(pr const& a, pr const& b) const {
return a.second > b.second;
}
};
void execution_context::report_big_relations(unsigned threshold, std::ostream & out) {
void execution_context::report_big_relations(unsigned threshold, std::ostream & out) const {
unsigned n = register_count();
svector<std::pair<unsigned, unsigned> > sizes;
size_t total_bytes = 0;
@ -110,6 +114,7 @@ namespace datalog {
bool execution_context::should_terminate() {
return
m_context.canceled() ||
memory::above_high_watermark() ||
(m_stopwatch &&
m_timelimit_ms != 0 &&
@ -135,7 +140,7 @@ namespace datalog {
process_costs();
}
void instruction::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const {
void instruction::display_indented(rel_context const & ctx, std::ostream & out, std::string indentation) const {
out << indentation;
display_head_impl(ctx, out);
if (ctx.output_profile()) {
@ -182,7 +187,7 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) {
ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str());
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
const char * rel_name = m_pred->get_name().bare_str();
if (m_store) {
out << "store " << m_reg << " into " << rel_name;
@ -213,7 +218,7 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) {
ctx.set_register_annotation(m_reg, "alloc");
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "dealloc " << m_reg;
}
};
@ -248,7 +253,7 @@ namespace datalog {
ctx.set_register_annotation(m_src, str);
}
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt;
}
};
@ -304,11 +309,11 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) {
m_body->make_annotations(ctx);
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const {
out << "while";
print_container(m_controls, out);
}
virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {
virtual void display_body_impl(rel_context const & ctx, std::ostream & out, std::string indentation) const {
m_body->display_indented(ctx, out, indentation+" ");
}
};
@ -385,7 +390,7 @@ namespace datalog {
ctx.get_register_annotation(m_rel1, a1);
ctx.set_register_annotation(m_res, "join " + a1 + " " + a2);
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const {
out << "join " << m_rel1;
print_container(m_cols1, out);
out << " and " << m_rel2;
@ -434,7 +439,7 @@ namespace datalog {
a << "filter_equal " << m_col << " val: " << ctx.get_rel_context().get_rmanager().to_nice_string(m_value);
ctx.set_register_annotation(m_reg, a.str());
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "filter_equal " << m_reg << " col: " << m_col << " val: "
<< ctx.get_rmanager().to_nice_string(m_value);
}
@ -476,7 +481,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "filter_identical " << m_reg << " ";
print_container(m_cols, out);
}
@ -519,7 +524,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "filter_interpreted " << m_reg << " using "
<< mk_pp(m_cond, m_cond.get_manager());
}
@ -619,12 +624,16 @@ namespace datalog {
return true;
}
virtual void make_annotations(execution_context & ctx) {
std::string str;
if (ctx.get_register_annotation(m_tgt, str) && m_delta!=execution_context::void_register) {
ctx.set_register_annotation(m_delta, "delta of "+str);
std::string str = "union";
if (!ctx.get_register_annotation(m_tgt, str)) {
ctx.set_register_annotation(m_tgt, "union");
}
if (m_delta != execution_context::void_register) {
str = "delta of " + str;
}
ctx.set_register_annotation(m_delta, str);
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt;
if (m_delta!=execution_context::void_register) {
out << " with delta " << m_delta;
@ -678,7 +687,7 @@ namespace datalog {
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt;
out << (m_projection ? " deleting columns " : " with cycle ");
print_container(m_cols, out);
@ -739,7 +748,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "join_project " << m_rel1;
print_container(m_cols1, out);
out << " and " << m_rel2;
@ -800,7 +809,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col
<< " val: " << ctx.get_rmanager().to_nice_string(m_value);
}
@ -854,7 +863,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "filter_by_negation on " << m_tgt;
print_container(m_cols1, out);
out << " with " << m_neg_rel;
@ -892,7 +901,7 @@ namespace datalog {
ctx.set_reg(m_tgt, rel);
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "mk_unary_singleton into " << m_tgt << " sort:"
<< ctx.get_rmanager().to_nice_string(m_sig[0]) << " val:"
<< ctx.get_rmanager().to_nice_string(m_sig[0], m_fact[0]);
@ -922,7 +931,7 @@ namespace datalog {
ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred));
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "mk_total into " << m_tgt << " sort:"
<< ctx.get_rmanager().to_nice_string(m_sig);
}
@ -947,7 +956,7 @@ namespace datalog {
ctx.get_rel_context().get_rmanager().mark_saturated(m_pred);
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "mark_saturated " << m_pred->get_name().bare_str();
}
virtual void make_annotations(execution_context & ctx) {
@ -970,7 +979,7 @@ namespace datalog {
}
return true;
}
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const& ctx, std::ostream & out) const {
out << "instr_assert_signature of " << m_tgt << " signature:";
print_container(m_sig, out);
}
@ -1042,7 +1051,7 @@ namespace datalog {
}
}
void instruction_block::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const {
void instruction_block::display_indented(rel_context const& ctx, std::ostream & out, std::string indentation) const {
instr_seq_type::const_iterator it = m_data.begin();
instr_seq_type::const_iterator end = m_data.end();
for(; it!=end; ++it) {

38
src/muz_qe/dl_instruction.h
View file

@ -31,6 +31,7 @@ namespace datalog {
class execution_context;
class instruction_block;
class rel_context;
inline void check_overflow(unsigned i) {
if (i == UINT_MAX) {
@ -78,7 +79,7 @@ namespace datalog {
void reset();
rel_context & get_rel_context() { return m_context.get_rel_context(); };
rel_context & get_rel_context();
void set_timelimit(unsigned time_in_ms);
void reset_timelimit();
@ -91,10 +92,9 @@ namespace datalog {
If register contains zero, it should be treated as if it contains an empty relation.
*/
reg_type reg(reg_idx i) {
if (i>=m_registers.size()) {
check_overflow(i);
m_registers.resize(i+1,0);
reg_type reg(reg_idx i) const {
if (i >= m_registers.size()) {
return 0;
}
return m_registers[i];
}
@ -102,27 +102,29 @@ namespace datalog {
\brief Return value of the register and assign zero into it place.
*/
reg_type release_reg(reg_idx i) {
SASSERT(i<m_registers.size());
SASSERT(i < m_registers.size());
SASSERT(m_registers[i]);
reg_type res = m_registers[i];
m_registers[i] = 0;
return res;
}
/**
\brief Assign value to a register. If it was non-empty, deallocate its content first.
*/
void set_reg(reg_idx i, reg_type val) {
if(i>=m_registers.size()) {
if (i >= m_registers.size()) {
check_overflow(i);
m_registers.resize(i+1,0);
}
if(m_registers[i]) {
if (m_registers[i]) {
m_registers[i]->deallocate();
}
m_registers[i]=val;
m_registers[i] = val;
}
void make_empty(reg_idx i) {
if(reg(i)) {
if (reg(i)) {
set_reg(i, 0);
}
}
@ -130,14 +132,16 @@ namespace datalog {
unsigned register_count() const {
return m_registers.size();
}
bool get_register_annotation(reg_idx reg, std::string & res) const {
return m_reg_annotation.find(reg, res);
}
void set_register_annotation(reg_idx reg, std::string str) {
m_reg_annotation.insert(reg, str);
}
void report_big_relations(unsigned threshold, std::ostream & out);
void report_big_relations(unsigned threshold, std::ostream & out) const;
};
@ -208,7 +212,7 @@ namespace datalog {
The newline character at the end should not be printed.
*/
virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
virtual void display_head_impl(rel_context const & ctx, std::ostream & out) const {
out << "<instruction>";
}
/**
@ -216,7 +220,7 @@ namespace datalog {
Each line must be prepended by \c indentation and ended by a newline character.
*/
virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {}
virtual void display_body_impl(rel_context const & ctx, std::ostream & out, std::string indentation) const {}
public:
typedef execution_context::reg_type reg_type;
typedef execution_context::reg_idx reg_idx;
@ -227,10 +231,10 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) = 0;
void display(rel_context & ctx, std::ostream & out) const {
void display(rel_context const& ctx, std::ostream & out) const {
display_indented(ctx, out, "");
}
void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
void display_indented(rel_context const & ctx, std::ostream & out, std::string indentation) const;
static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt);
/**
@ -329,10 +333,10 @@ namespace datalog {
void make_annotations(execution_context & ctx);
void display(rel_context & ctx, std::ostream & out) const {
void display(rel_context const & ctx, std::ostream & out) const {
display_indented(ctx, out, "");
}
void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
void display_indented(rel_context const & ctx, std::ostream & out, std::string indentation) const;
};

2
src/muz_qe/dl_mk_array_blast.cpp
View file

@ -213,7 +213,7 @@ namespace datalog {
rule_set* rules = alloc(rule_set, m_ctx);
rule_set::iterator it = source.begin(), end = source.end();
bool change = false;
for (; it != end; ++it) {
for (; !m_ctx.canceled() && it != end; ++it) {
change = blast(**it, *rules) || change;
}
if (!change) {

2
src/muz_qe/dl_mk_bit_blast.cpp
View file

@ -265,7 +265,7 @@ namespace datalog {
expr_ref fml(m);
reset();
rule_set * result = alloc(rule_set, m_context);
for (unsigned i = 0; i < sz; ++i) {
for (unsigned i = 0; !m_context.canceled() && i < sz; ++i) {
rule * r = source.get_rule(i);
r->to_formula(fml);
if (blast(r, fml)) {

59
src/muz_qe/rel_context.cpp
View file

@ -39,8 +39,8 @@ namespace datalog {
m(ctx.get_manager()),
m_rmanager(ctx),
m_answer(m),
m_cancel(false),
m_last_result_relation(0) {
m_last_result_relation(0),
m_ectx(ctx) {
// register plugins for builtin tables
@ -94,9 +94,9 @@ namespace datalog {
decl_set original_predicates;
m_context.collect_predicates(original_predicates);
instruction_block rules_code;
m_code.reset();
instruction_block termination_code;
execution_context ex_ctx(m_context);
m_ectx.reset();
lbool result;
@ -104,9 +104,13 @@ namespace datalog {
while (true) {
m_context.transform_rules();
compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code);
if (m_context.canceled()) {
result = l_undef;
break;
}
compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
TRACE("dl", rules_code.display(*this, tout); );
TRACE("dl", m_code.display(*this, tout); );
bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
@ -114,29 +118,32 @@ namespace datalog {
unsigned timeout = time_limit ? (restart_time!=0) ?
std::min(remaining_time_limit, restart_time)
: remaining_time_limit : restart_time;
ex_ctx.set_timelimit(timeout);
m_ectx.set_timelimit(timeout);
}
bool early_termination = !rules_code.perform(ex_ctx);
ex_ctx.reset_timelimit();
VERIFY( termination_code.perform(ex_ctx) );
bool early_termination = !m_code.perform(m_ectx);
m_ectx.reset_timelimit();
VERIFY( termination_code.perform(m_ectx) || m_context.canceled());
rules_code.process_all_costs();
m_code.process_all_costs();
IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream()););
IF_VERBOSE(10, m_ectx.report_big_relations(1000, verbose_stream()););
if (m_context.canceled()) {
result = l_undef;
break;
}
if (!early_termination) {
m_context.set_status(OK);
result = l_true;
break;
}
if (memory::above_high_watermark()) {
m_context.set_status(MEMOUT);
result = l_undef;
break;
}
if (timeout_after_this_round || m_cancel) {
if (timeout_after_this_round) {
m_context.set_status(TIMEOUT);
result = l_undef;
break;
@ -154,9 +161,7 @@ namespace datalog {
restart_time = static_cast<unsigned>(new_restart_time);
}
rules_code.reset();
termination_code.reset();
ex_ctx.reset();
termination_code.reset();
m_context.reopen();
restrict_predicates(original_predicates);
m_context.replace_rules(original_rules);
@ -164,10 +169,12 @@ namespace datalog {
}
m_context.reopen();
restrict_predicates(original_predicates);
m_context.record_transformed_rules();
m_context.replace_rules(original_rules);
m_context.close();
TRACE("dl", ex_ctx.report_big_relations(100, tout););
m_cancel = false;
TRACE("dl", m_ectx.report_big_relations(100, tout););
m_code.process_all_costs();
m_code.make_annotations(m_ectx);
return result;
}
@ -504,5 +511,17 @@ namespace datalog {
get_rmanager().display(out);
}
void rel_context::display_profile(std::ostream& out) const {
out << "\n--------------\n";
out << "Instructions\n";
m_code.display(*this, out);
out << "\n--------------\n";
out << "Big relations\n";
m_ectx.report_big_relations(1000, out);
get_rmanager().display_relation_sizes(out);
}
};

14
src/muz_qe/rel_context.h
View file

@ -22,6 +22,7 @@ Revision History:
#define _REL_CONTEXT_H_
#include "ast.h"
#include "dl_relation_manager.h"
#include "dl_instruction.h"
#include "lbool.h"
namespace datalog {
@ -35,10 +36,11 @@ namespace datalog {
ast_manager& m;
relation_manager m_rmanager;
expr_ref m_answer;
volatile bool m_cancel;
relation_base * m_last_result_relation;
decl_set m_output_preds;
fact_vector m_table_facts;
execution_context m_ectx;
instruction_block m_code;
void reset_negated_tables();
@ -53,8 +55,8 @@ namespace datalog {
relation_manager & get_rmanager();
const relation_manager & get_rmanager() const;
ast_manager& get_manager() { return m; }
context& get_context() { return m_context; }
ast_manager& get_manager() const { return m; }
context& get_context() const { return m_context; }
relation_base & get_relation(func_decl * pred);
relation_base * try_get_relation(func_decl * pred) const;
expr_ref get_last_answer() { return m_answer; }
@ -70,10 +72,6 @@ namespace datalog {
void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
void cancel() { m_cancel = true; }
void cleanup() { m_cancel = false; }
/**
\brief Restrict the set of used predicates to \c res.
@ -107,6 +105,8 @@ namespace datalog {
void display_output_facts(std::ostream & out) const;
void display_facts(std::ostream & out) const;
void display_profile(std::ostream& out) const;
lbool saturate();
};

1
src/shell/datalog_frontend.cpp
View file

@ -209,7 +209,6 @@ unsigned read_datalog(char const * file) {
rules_code.make_annotations(ex_ctx);
ex_ctx.set_timelimit(timeout);
SASSERT(!ex_ctx.should_terminate());
early_termination = !rules_code.perform(ex_ctx);
if(early_termination) {