mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-19 20:33:38 +00:00
Code Activity

factor out relation context for datalog

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2012-12-03 15:05:43 -08:00
parent 8425685ea3
commit 67183ea08a
24 changed files with 799 additions and 569 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_datalog.cpp
View file

@ -48,7 +48,7 @@ namespace api {
if (!m.has_plugin(name)) { if (!m.has_plugin(name)) {
m.register_plugin(name, alloc(datalog::dl_decl_plugin)); m.register_plugin(name, alloc(datalog::dl_decl_plugin));
} }
datalog::relation_manager& r = m_context.get_rmanager(); datalog::relation_manager& r = m_context.get_rel_context().get_rmanager();
r.register_plugin(alloc(datalog::external_relation_plugin, *this, r)); r.register_plugin(alloc(datalog::external_relation_plugin, *this, r));
} }
@ -295,7 +295,7 @@ extern "C" {
{ {
scoped_timer timer(timeout, &eh); scoped_timer timer(timeout, &eh);
try { try {
r = to_fixedpoint_ref(d)->ctx().dl_query(num_relations, to_func_decls(relations)); r = to_fixedpoint_ref(d)->ctx().rel_query(num_relations, to_func_decls(relations));
} }
catch (z3_exception& ex) { catch (z3_exception& ex) {
mk_c(c)->handle_exception(ex); mk_c(c)->handle_exception(ex);

3
src/muz_qe/datalog_parser.cpp
View file

@ -1326,9 +1326,6 @@ private:
throw default_exception("tuple file %s for undeclared predicate %s", throw default_exception("tuple file %s for undeclared predicate %s",
m_current_file.c_str(), predicate_name.bare_str()); m_current_file.c_str(), predicate_name.bare_str());
} }
if(!m_context.can_add_table_fact(pred)) {
NOT_IMPLEMENTED_YET();
}
unsigned pred_arity = pred->get_arity(); unsigned pred_arity = pred->get_arity();
sort * const * arg_sorts = pred->get_domain(); sort * const * arg_sorts = pred->get_domain();

1
src/muz_qe/dl_bmc_engine.cpp
View file

@ -57,7 +57,6 @@ namespace datalog {
m_ctx.ensure_opened(); m_ctx.ensure_opened();
m_rules.reset(); m_rules.reset();
m_ctx.get_rmanager().reset_relations();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
datalog::rule_set old_rules(m_ctx.get_rules()); datalog::rule_set old_rules(m_ctx.get_rules());
datalog::rule_ref_vector query_rules(rule_manager); datalog::rule_ref_vector query_rules(rule_manager);

8
src/muz_qe/dl_compiler.cpp
View file

@ -42,7 +42,7 @@ namespace datalog {
return; return;
} }
relation_signature sig; relation_signature sig;
m_context.get_rmanager().from_predicate(pred, sig); m_context.get_rel_context().get_rmanager().from_predicate(pred, sig);
reg_idx reg = get_fresh_register(sig); reg_idx reg = get_fresh_register(sig);
e->get_data().m_value=reg; e->get_data().m_value=reg;
@ -563,7 +563,7 @@ namespace datalog {
} }
SASSERT(is_app(e)); SASSERT(is_app(e));
relation_sort arg_sort; relation_sort arg_sort;
m_context.get_rmanager().from_predicate(neg_pred, i, arg_sort); m_context.get_rel_context().get_rmanager().from_predicate(neg_pred, i, arg_sort);
reg_idx new_reg; reg_idx new_reg;
make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, acc); make_add_constant_column(head_pred, filtered_res, arg_sort, to_app(e), new_reg, acc);
@ -1096,7 +1096,7 @@ namespace datalog {
func_decl_set::iterator fdit = preds.begin(); func_decl_set::iterator fdit = preds.begin();
func_decl_set::iterator fdend = preds.end(); func_decl_set::iterator fdend = preds.end();
for(; fdit!=fdend; ++fdit) { for(; fdit!=fdend; ++fdit) {
if(!m_context.get_rmanager().is_saturated(*fdit)) { if(!m_context.get_rel_context().get_rmanager().is_saturated(*fdit)) {
return false; return false;
} }
} }
@ -1181,7 +1181,7 @@ namespace datalog {
acc.set_observer(0); acc.set_observer(0);
TRACE("dl", execution_code.display(m_context, tout);); TRACE("dl", execution_code.display(m_context.get_rel_context(), tout););
} }

478
src/muz_qe/dl_context.cpp
View file

@ -24,18 +24,12 @@ Revision History:
#include"arith_decl_plugin.h" #include"arith_decl_plugin.h"
#include"bv_decl_plugin.h" #include"bv_decl_plugin.h"
#include"dl_table.h" #include"dl_table.h"
#include"dl_sparse_table.h"
#include"dl_table_relation.h" #include"dl_table_relation.h"
#include"dl_bound_relation.h"
#include"dl_interval_relation.h"
#include"dl_finite_product_relation.h"
#include"dl_product_relation.h"
#include"dl_rule_transformer.h" #include"dl_rule_transformer.h"
#include"dl_mk_coi_filter.h" #include"dl_mk_coi_filter.h"
#include"dl_mk_explanations.h" #include"dl_mk_explanations.h"
#include"dl_mk_filter_rules.h" #include"dl_mk_filter_rules.h"
#include"dl_mk_interp_tail_simplifier.h" #include"dl_mk_interp_tail_simplifier.h"
#include"dl_mk_magic_sets.h"
#include"dl_mk_rule_inliner.h" #include"dl_mk_rule_inliner.h"
#include"dl_mk_simple_joins.h" #include"dl_mk_simple_joins.h"
#include"dl_mk_similarity_compressor.h" #include"dl_mk_similarity_compressor.h"
@ -44,9 +38,6 @@ Revision History:
#include"dl_compiler.h" #include"dl_compiler.h"
#include"dl_instruction.h" #include"dl_instruction.h"
#include"dl_context.h" #include"dl_context.h"
#ifndef _EXTERNAL_RELEASE
#include"dl_skip_table.h"
#endif
#include"for_each_expr.h" #include"for_each_expr.h"
#include"ast_smt_pp.h" #include"ast_smt_pp.h"
#include"ast_smt2_pp.h" #include"ast_smt2_pp.h"
@ -189,7 +180,6 @@ namespace datalog {
virtual ~restore_rules() {} virtual ~restore_rules() {}
virtual void undo(context& ctx) { virtual void undo(context& ctx) {
ctx.reset_tables();
ctx.replace_rules(*m_old_rules); ctx.replace_rules(*m_old_rules);
reset(); reset();
} }
@ -209,7 +199,6 @@ namespace datalog {
m_trail.push_scope(); m_trail.push_scope();
m_trail.push(restore_rules(m_rule_set)); m_trail.push(restore_rules(m_rule_set));
m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background)); m_trail.push(restore_vec_size_trail<context,expr_ref_vector>(m_background));
m_trail.push(restore_vec_size_trail<context,fact_vector>(m_table_facts));
} }
void context::pop() { void context::pop() {
@ -233,7 +222,6 @@ namespace datalog {
m_decl_util(m), m_decl_util(m),
m_rewriter(m), m_rewriter(m),
m_var_subst(m), m_var_subst(m),
m_rmanager(*this),
m_rule_manager(*this), m_rule_manager(*this),
m_trail(*this), m_trail(*this),
m_pinned(m), m_pinned(m),
@ -243,25 +231,11 @@ namespace datalog {
m_background(m), m_background(m),
m_closed(false), m_closed(false),
m_saturation_was_run(false), m_saturation_was_run(false),
m_last_result_relation(0),
m_last_answer(m), m_last_answer(m),
m_engine(LAST_ENGINE), m_engine(LAST_ENGINE),
m_cancel(false) { m_cancel(false) {
//register plugins for builtin tables //register plugins for builtin tables
get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
#ifndef _EXTERNAL_RELEASE
get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
#endif
//register plugins for builtin relations
get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
} }
context::~context() { context::~context() {
@ -272,14 +246,12 @@ namespace datalog {
m_trail.reset(); m_trail.reset();
m_rule_set.reset(); m_rule_set.reset();
m_argument_var_names.reset(); m_argument_var_names.reset();
m_output_preds.reset();
m_preds.reset(); m_preds.reset();
m_preds_by_name.reset(); m_preds_by_name.reset();
reset_dealloc_values(m_sorts); reset_dealloc_values(m_sorts);
if (m_last_result_relation) { m_pdr = 0;
m_last_result_relation->deallocate(); m_bmc = 0;
m_last_result_relation = 0; m_rel = 0;
}
} }
bool context::is_fact(app * head) const { bool context::is_fact(app * head) const {
@ -455,59 +427,13 @@ namespace datalog {
return e->get_data().m_value[arg_index]; return e->get_data().m_value[arg_index];
} }
relation_plugin & context::get_ordinary_relation_plugin(symbol relation_name) {
relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
if (!plugin) {
std::stringstream sstm;
sstm << "relation plugin " << relation_name << " does not exist";
throw default_exception(sstm.str());
}
if (plugin->is_product_relation()) {
throw default_exception("cannot request product relation directly");
}
if (plugin->is_sieve_relation()) {
throw default_exception("cannot request sieve relation directly");
}
if (plugin->is_finite_product_relation()) {
throw default_exception("cannot request finite product relation directly");
}
return *plugin;
}
void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names) { symbol const * relation_names) {
relation_manager & rmgr = get_rmanager(); if (relation_name_cnt > 0) {
ensure_rel();
family_id target_kind = null_family_id; m_rel->set_predicate_representation(pred, relation_name_cnt, relation_names);
switch (relation_name_cnt) {
case 0:
return;
case 1:
target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
break;
default: {
svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
family_id rel_kind; // the aggregate kind of non-table plugins
for (unsigned i = 0; i < relation_name_cnt; i++) {
relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
rel_kinds.push_back(p.get_kind());
} }
if (rel_kinds.size() == 1) {
rel_kind = rel_kinds[0];
}
else {
relation_signature rel_sig;
//rmgr.from_predicate(pred, rel_sig);
product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
}
target_kind = rel_kind;
break;
}
}
SASSERT(target_kind != null_family_id);
get_rmanager().set_predicate_kind(pred, target_kind);
} }
func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix, func_decl * context::mk_fresh_head_predicate(symbol const & prefix, symbol const & suffix,
@ -517,19 +443,25 @@ namespace datalog {
register_predicate(new_pred); register_predicate(new_pred);
if (orig_pred) { if (m_rel.get()) {
family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred); m_rel->inherit_predicate_kind(new_pred, orig_pred);
if (target_kind != null_family_id) {
get_rmanager().set_predicate_kind(new_pred, target_kind);
}
} }
return new_pred; return new_pred;
} }
void context::set_output_predicate(func_decl * pred) { void context::set_output_predicate(func_decl * pred) {
if (!m_output_preds.contains(pred)) { ensure_rel();
m_output_preds.insert(pred); m_rel->set_output_predicate(pred);
} }
bool context::is_output_predicate(func_decl * pred) {
ensure_rel();
return m_rel->is_output_predicate(pred);
}
const decl_set & context::get_output_predicates() {
ensure_rel();
return m_rel->get_output_predicates();
} }
void context::add_rule(expr* rl, symbol const& name) { void context::add_rule(expr* rl, symbol const& name) {
@ -562,7 +494,6 @@ namespace datalog {
throw default_exception(strm.str()); throw default_exception(strm.str());
} }
rule_ref r(rules[0].get(), rm); rule_ref r(rules[0].get(), rm);
get_rmanager().reset_saturated_marks();
rule_ref_vector const& rls = m_rule_set.get_rules(); rule_ref_vector const& rls = m_rule_set.get_rules();
rule* old_rule = 0; rule* old_rule = 0;
for (unsigned i = 0; i < rls.size(); ++i) { for (unsigned i = 0; i < rls.size(); ++i) {
@ -795,7 +726,6 @@ namespace datalog {
} }
void context::add_rule(rule_ref& r) { void context::add_rule(rule_ref& r) {
get_rmanager().reset_saturated_marks();
m_rule_set.add_rule(r); m_rule_set.add_rule(r);
} }
@ -809,12 +739,10 @@ namespace datalog {
void context::add_fact(func_decl * pred, const relation_fact & fact) { void context::add_fact(func_decl * pred, const relation_fact & fact) {
if (get_engine() == DATALOG_ENGINE) { if (get_engine() == DATALOG_ENGINE) {
get_rmanager().reset_saturated_marks(); ensure_rel();
get_relation(pred).add_fact(fact); m_rel->add_fact(pred, fact);
m_table_facts.push_back(std::make_pair(pred, fact));
} }
else { else {
ast_manager& m = get_manager();
expr_ref rule(m.mk_app(pred, fact.size(), (expr*const*)fact.c_ptr()), m); expr_ref rule(m.mk_app(pred, fact.size(), (expr*const*)fact.c_ptr()), m);
add_rule(rule, symbol::null); add_rule(rule, symbol::null);
} }
@ -832,26 +760,18 @@ namespace datalog {
add_fact(head->get_decl(), fact); add_fact(head->get_decl(), fact);
} }
bool context::can_add_table_fact(func_decl * pred) {
return get_relation(pred).from_table();
}
void context::add_table_fact(func_decl * pred, const table_fact & fact) { void context::add_table_fact(func_decl * pred, const table_fact & fact) {
relation_base & rel0 = get_relation(pred); if (get_engine() == DATALOG_ENGINE) {
if (get_engine() != DATALOG_ENGINE || ensure_rel();
!can_add_table_fact(pred) || m_rel->add_fact(pred, fact);
!rel0.from_table()) { }
else {
relation_fact rfact(m); relation_fact rfact(m);
for (unsigned i = 0; i < fact.size(); ++i) { for (unsigned i = 0; i < fact.size(); ++i) {
rfact.push_back(m_decl_util.mk_numeral(fact[i], pred->get_domain()[i])); rfact.push_back(m_decl_util.mk_numeral(fact[i], pred->get_domain()[i]));
} }
add_fact(pred, rfact); add_fact(pred, rfact);
} }
else {
get_rmanager().reset_saturated_marks();
table_relation & rel = static_cast<table_relation &>(rel0);
rel.add_table_fact(fact);
}
} }
void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) { void context::add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]) {
@ -968,117 +888,14 @@ namespace datalog {
if (m_pdr.get()) m_pdr->updt_params(); if (m_pdr.get()) m_pdr->updt_params();
} }
void context::collect_predicates(decl_set & res) { void context::collect_predicates(decl_set& res) {
unsigned rule_cnt = m_rule_set.get_num_rules(); ensure_rel();
for (unsigned rindex=0; rindex<rule_cnt; rindex++) { m_rel->collect_predicates(res);
rule * r = m_rule_set.get_rule(rindex);
res.insert(r->get_head()->get_decl());
unsigned tail_len = r->get_uninterpreted_tail_size();
for (unsigned tindex=0; tindex<tail_len; tindex++) {
res.insert(r->get_tail(tindex)->get_decl());
}
}
decl_set::iterator oit = m_output_preds.begin();
decl_set::iterator oend = m_output_preds.end();
for (; oit!=oend; ++oit) {
res.insert(*oit);
}
get_rmanager().collect_predicates(res);
} }
void context::restrict_predicates( const decl_set & res ) { void context::restrict_predicates(decl_set const& res) {
set_intersection(m_output_preds, res); ensure_rel();
get_rmanager().restrict_predicates(res); m_rel->restrict_predicates(res);
}
lbool context::dl_saturate() {
if (!m_closed) {
close();
}
bool time_limit = soft_timeout()!=0;
unsigned remaining_time_limit = soft_timeout();
unsigned restart_time = initial_restart_timeout();
rule_set original_rules(get_rules());
decl_set original_predicates;
collect_predicates(original_predicates);
instruction_block rules_code;
instruction_block termination_code;
execution_context ex_ctx(*this);
lbool result;
TRACE("dl", display(tout););
while (true) {
model_converter_ref mc; // Ignored in Datalog mode
proof_converter_ref pc; // Ignored in Datalog mode
transform_rules(mc, pc);
compiler::compile(*this, get_rules(), rules_code, termination_code);
TRACE("dl", rules_code.display(*this, tout); );
bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
if (time_limit || restart_time!=0) {
unsigned timeout = time_limit ? (restart_time!=0) ?
std::min(remaining_time_limit, restart_time)
: remaining_time_limit : restart_time;
ex_ctx.set_timelimit(timeout);
}
bool early_termination = !rules_code.perform(ex_ctx);
ex_ctx.reset_timelimit();
VERIFY( termination_code.perform(ex_ctx) );
rules_code.process_all_costs();
IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream()););
if (!early_termination) {
m_last_status = OK;
result = l_true;
break;
}
if (memory::above_high_watermark()) {
m_last_status = MEMOUT;
result = l_undef;
break;
}
if (timeout_after_this_round || m_cancel) {
m_last_status = TIMEOUT;
result = l_undef;
break;
}
SASSERT(restart_time!=0);
if (time_limit) {
SASSERT(remaining_time_limit>restart_time);
remaining_time_limit-=restart_time;
}
uint64 new_restart_time = static_cast<uint64>(restart_time)*initial_restart_timeout();
if (new_restart_time>UINT_MAX) {
restart_time=UINT_MAX;
}
else {
restart_time=static_cast<unsigned>(new_restart_time);
}
rules_code.reset();
termination_code.reset();
ex_ctx.reset();
reopen();
restrict_predicates(original_predicates);
replace_rules(original_rules);
close();
}
reopen();
restrict_predicates(original_predicates);
replace_rules(original_rules);
close();
TRACE("dl", ex_ctx.report_big_relations(100, tout););
return result;
} }
expr_ref context::get_background_assertion() { expr_ref context::get_background_assertion() {
@ -1101,6 +918,7 @@ namespace datalog {
m_cancel = true; m_cancel = true;
if (m_pdr.get()) m_pdr->cancel(); if (m_pdr.get()) m_pdr->cancel();
if (m_bmc.get()) m_bmc->cancel(); if (m_bmc.get()) m_bmc->cancel();
if (m_rel.get()) m_rel->cancel();
} }
void context::cleanup() { void context::cleanup() {
@ -1180,7 +998,7 @@ namespace datalog {
switch(get_engine()) { switch(get_engine()) {
case DATALOG_ENGINE: case DATALOG_ENGINE:
return dl_query(query); return rel_query(query);
case PDR_ENGINE: case PDR_ENGINE:
case QPDR_ENGINE: case QPDR_ENGINE:
return pdr_query(query); return pdr_query(query);
@ -1189,18 +1007,14 @@ namespace datalog {
return bmc_query(query); return bmc_query(query);
default: default:
UNREACHABLE(); UNREACHABLE();
return dl_query(query); return rel_query(query);
} }
} }
void context::new_query() { void context::new_query() {
flush_add_rules(); flush_add_rules();
if (m_last_result_relation) {
m_last_result_relation->deallocate();
m_last_result_relation = 0;
}
m_last_status = OK; m_last_status = OK;
m_last_answer = get_manager().mk_true(); m_last_answer = 0;
} }
model_ref context::get_model() { model_ref context::get_model() {
@ -1233,7 +1047,6 @@ namespace datalog {
lbool context::pdr_query(expr* query) { lbool context::pdr_query(expr* query) {
ensure_pdr(); ensure_pdr();
m_last_answer = 0;
return m_pdr->query(query); return m_pdr->query(query);
} }
@ -1245,218 +1058,25 @@ namespace datalog {
lbool context::bmc_query(expr* query) { lbool context::bmc_query(expr* query) {
ensure_bmc(); ensure_bmc();
m_last_answer = 0;
return m_bmc->query(query); return m_bmc->query(query);
} }
#define BEGIN_QUERY() \ void context::ensure_rel() {
rule_set original_rules(get_rules()); \ if (!m_rel.get()) {
decl_set original_preds; \ m_rel = alloc(rel_context, *this);
collect_predicates(original_preds); \
bool was_closed = m_closed; \
if (m_closed) { \
reopen(); \
} \
#define END_QUERY() \
reopen(); \
replace_rules(original_rules); \
restrict_predicates(original_preds); \
\
if (was_closed) { \
close(); \
} \
lbool context::dl_query(unsigned num_rels, func_decl * const* rels) {
BEGIN_QUERY();
for (unsigned i = 0; i < num_rels; ++i) {
set_output_predicate(rels[i]);
}
close();
reset_negated_tables();
lbool res = dl_saturate();
switch(res) {
case l_true: {
expr_ref_vector ans(m);
expr_ref e(m);
bool some_non_empty = num_rels == 0;
for (unsigned i = 0; i < num_rels; ++i) {
relation_base& rel = get_relation(rels[i]);
if (!rel.empty()) {
some_non_empty = true;
}
rel.to_formula(e);
ans.push_back(e);
}
SASSERT(!m_last_result_relation);
if (some_non_empty) {
m_last_answer = m.mk_and(ans.size(), ans.c_ptr());
}
else {
m_last_answer = m.mk_false();
res = l_false;
}
break;
}
case l_false:
m_last_answer = m.mk_false();
break;
case l_undef:
break;
}
END_QUERY();
return res;
}
lbool context::dl_query(expr* query) {
BEGIN_QUERY();
rule_manager& rm = get_rule_manager();
rule_ref qrule(rm);
rule_ref_vector qrules(rm);
func_decl_ref query_pred(get_manager());
try {
rm.mk_query(query, query_pred, qrules, qrule);
}
catch(default_exception& exn) {
close();
m_last_status = INPUT_ERROR;
throw exn;
}
try {
add_rules(qrules);
}
catch (default_exception& exn) {
close();
m_last_status = INPUT_ERROR;
throw exn;
}
set_output_predicate(qrule->get_head()->get_decl());
close();
reset_negated_tables();
if (generate_explanations()) {
model_converter_ref mc; // ignored in Datalog mode
proof_converter_ref pc; // ignored in Datalog mode
rule_transformer transformer(*this);
//expl_plugin is deallocated when transformer goes out of scope
mk_explanations * expl_plugin =
alloc(mk_explanations, *this, explanations_on_relation_level());
transformer.register_plugin(expl_plugin);
transform_rules(transformer, mc, pc);
//we will retrieve the predicate with explanations instead of the original query predicate
query_pred = expl_plugin->get_e_decl(query_pred);
const rule_vector & query_rules = get_rules().get_predicate_rules(query_pred);
SASSERT(query_rules.size()==1);
qrule = query_rules.back();
}
if (magic_sets_for_queries()) {
model_converter_ref mc; // Ignored in Datalog mode
proof_converter_ref pc; // Ignored in Datalog mode
rule_transformer transformer(*this);
transformer.register_plugin(alloc(mk_magic_sets, *this, qrule.get()));
transform_rules(transformer, mc, pc);
}
lbool res = dl_saturate();
if (res != l_undef) {
m_last_result_relation = get_relation(query_pred).clone();
if (m_last_result_relation->empty()) {
res = l_false;
m_last_answer = m.mk_false();
}
else {
m_last_result_relation->to_formula(m_last_answer);
} }
} }
END_QUERY(); lbool context::rel_query(unsigned num_rels, func_decl * const* rels) {
return res; ensure_rel();
return m_rel->query(num_rels, rels);
} }
void context::reset_tables() { lbool context::rel_query(expr* query) {
get_rmanager().reset_saturated_marks(); ensure_rel();
rule_set::decl2rules::iterator it = m_rule_set.begin_grouped_rules(); return m_rel->query(query);
rule_set::decl2rules::iterator end = m_rule_set.end_grouped_rules();
for (; it != end; ++it) {
func_decl* p = it->m_key;
relation_base & rel = get_relation(p);
rel.reset();
}
for (unsigned i = 0; i < m_table_facts.size(); ++i) {
func_decl* pred = m_table_facts[i].first;
relation_fact const& fact = m_table_facts[i].second;
get_relation(pred).add_fact(fact);
}
} }
void context::reset_negated_tables() {
rule_set::pred_set_vector const & pred_sets = m_rule_set.get_strats();
bool non_empty = false;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
non_empty = true;
break;
}
}
}
if (!non_empty) {
return;
}
// collect predicates that depend on negation.
func_decl_set depends_on_negation;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
bool change = true;
while (change) {
change = false;
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
if (depends_on_negation.contains(pred)) {
continue;
}
rule_vector const& rules = m_rule_set.get_predicate_rules(pred);
bool inserted = false;
for (unsigned j = 0; !inserted && j < rules.size(); ++j) {
rule* r = rules[j];
unsigned psz = r->get_positive_tail_size();
unsigned tsz = r->get_uninterpreted_tail_size();
if (psz < tsz) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
for (unsigned k = 0; !inserted && k < tsz; ++k) {
func_decl* tail_decl = r->get_tail(k)->get_decl();
if (depends_on_negation.contains(tail_decl)) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
}
}
}
}
}
func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";);
rel.reset();
}
}
}
expr* context::get_answer_as_formula() { expr* context::get_answer_as_formula() {
if (m_last_answer) { if (m_last_answer) {
@ -1473,6 +1093,10 @@ namespace datalog {
ensure_bmc(); ensure_bmc();
m_last_answer = m_bmc->get_answer(); m_last_answer = m_bmc->get_answer();
return m_last_answer.get(); return m_last_answer.get();
case DATALOG_ENGINE:
ensure_rel();
m_last_answer = m_rel->get_last_answer();
return m_last_answer.get();
default: default:
UNREACHABLE(); UNREACHABLE();
} }
@ -1533,8 +1157,8 @@ namespace datalog {
execution_result context::get_status() { return m_last_status; } execution_result context::get_status() { return m_last_status; }
bool context::result_contains_fact(relation_fact const& f) { bool context::result_contains_fact(relation_fact const& f) {
SASSERT(m_last_result_relation); ensure_rel();
return m_last_result_relation->contains_fact(f); return m_rel->result_contains_fact(f);
} }
// TBD: algebraic data-types declarations will not be printed. // TBD: algebraic data-types declarations will not be printed.

66
src/muz_qe/dl_context.h
View file

@ -35,11 +35,11 @@ Revision History:
#include"dl_rule_set.h" #include"dl_rule_set.h"
#include"pdr_dl_interface.h" #include"pdr_dl_interface.h"
#include"dl_bmc_engine.h" #include"dl_bmc_engine.h"
#include"rel_context.h"
#include"lbool.h" #include"lbool.h"
#include"statistics.h" #include"statistics.h"
#include"params.h" #include"params.h"
#include"trail.h" #include"trail.h"
#include"dl_external_relation.h"
#include"model_converter.h" #include"model_converter.h"
#include"proof_converter.h" #include"proof_converter.h"
#include"model2expr.h" #include"model2expr.h"
@ -75,7 +75,6 @@ namespace datalog {
typedef map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> sym2decl; typedef map<symbol, func_decl*, symbol_hash_proc, symbol_eq_proc> sym2decl;
typedef obj_map<const func_decl, svector<symbol> > pred2syms; typedef obj_map<const func_decl, svector<symbol> > pred2syms;
typedef obj_map<const sort, sort_domain*> sort_domain_map; typedef obj_map<const sort, sort_domain*> sort_domain_map;
typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
ast_manager & m; ast_manager & m;
smt_params & m_fparams; smt_params & m_fparams;
@ -84,7 +83,6 @@ namespace datalog {
dl_decl_util m_decl_util; dl_decl_util m_decl_util;
th_rewriter m_rewriter; th_rewriter m_rewriter;
var_subst m_var_subst; var_subst m_var_subst;
relation_manager m_rmanager;
rule_manager m_rule_manager; rule_manager m_rule_manager;
trail_stack<context> m_trail; trail_stack<context> m_trail;
@ -94,7 +92,6 @@ namespace datalog {
func_decl_set m_preds; func_decl_set m_preds;
sym2decl m_preds_by_name; sym2decl m_preds_by_name;
pred2syms m_argument_var_names; pred2syms m_argument_var_names;
decl_set m_output_preds;
rule_set m_rule_set; rule_set m_rule_set;
expr_ref_vector m_rule_fmls; expr_ref_vector m_rule_fmls;
svector<symbol> m_rule_names; svector<symbol> m_rule_names;
@ -102,23 +99,20 @@ namespace datalog {
scoped_ptr<pdr::dl_interface> m_pdr; scoped_ptr<pdr::dl_interface> m_pdr;
scoped_ptr<bmc> m_bmc; scoped_ptr<bmc> m_bmc;
scoped_ptr<rel_context> m_rel;
bool m_closed; bool m_closed;
bool m_saturation_was_run; bool m_saturation_was_run;
execution_result m_last_status; execution_result m_last_status;
relation_base * m_last_result_relation;
expr_ref m_last_answer; expr_ref m_last_answer;
DL_ENGINE m_engine; DL_ENGINE m_engine;
volatile bool m_cancel; volatile bool m_cancel;
fact_vector m_table_facts;
bool is_fact(app * head) const; bool is_fact(app * head) const;
bool has_sort_domain(relation_sort s) const; bool has_sort_domain(relation_sort s) const;
sort_domain & get_sort_domain(relation_sort s); sort_domain & get_sort_domain(relation_sort s);
const sort_domain & get_sort_domain(relation_sort s) const; const sort_domain & get_sort_domain(relation_sort s) const;
relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
class engine_type_proc; class engine_type_proc;
@ -130,25 +124,12 @@ namespace datalog {
void push(); void push();
void pop(); void pop();
relation_base & get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); }
relation_base * try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); }
bool saturation_was_run() const { return m_saturation_was_run; } bool saturation_was_run() const { return m_saturation_was_run; }
void notify_saturation_was_run() { m_saturation_was_run = true; } void notify_saturation_was_run() { m_saturation_was_run = true; }
/**
\brief Store the relation \c rel under the predicate \c pred. The \c context object
takes over the ownership of the relation object.
*/
void store_relation(func_decl * pred, relation_base * rel) {
get_rmanager().store_relation(pred, rel);
}
void configure_engine(); void configure_engine();
ast_manager & get_manager() const { return m; } ast_manager & get_manager() const { return m; }
relation_manager & get_rmanager() { return m_rmanager; }
const relation_manager & get_rmanager() const { return m_rmanager; }
rule_manager & get_rule_manager() { return m_rule_manager; } rule_manager & get_rule_manager() { return m_rule_manager; }
smt_params & get_fparams() const { return m_fparams; } smt_params & get_fparams() const { return m_fparams; }
fixedpoint_params const& get_params() const { return m_params; } fixedpoint_params const& get_params() const { return m_params; }
@ -247,8 +228,8 @@ namespace datalog {
symbol const * relation_names); symbol const * relation_names);
void set_output_predicate(func_decl * pred); void set_output_predicate(func_decl * pred);
bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); } bool is_output_predicate(func_decl * pred);
const decl_set & get_output_predicates() const { return m_output_preds; } const decl_set & get_output_predicates();
rule_set const & get_rules() { flush_add_rules(); return m_rule_set; } rule_set const & get_rules() { flush_add_rules(); return m_rule_set; }
@ -314,7 +295,6 @@ namespace datalog {
and there is no transformation of relation values before they are put into the and there is no transformation of relation values before they are put into the
table. table.
*/ */
bool can_add_table_fact(func_decl * pred);
void add_table_fact(func_decl * pred, const table_fact & fact); void add_table_fact(func_decl * pred, const table_fact & fact);
void add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]); void add_table_fact(func_decl * pred, unsigned num_args, unsigned args[]);
@ -323,6 +303,7 @@ namespace datalog {
*/ */
void close(); void close();
void ensure_closed(); void ensure_closed();
bool is_closed() { return m_closed; }
/** /**
\brief Undo the effect of the \c close operation. \brief Undo the effect of the \c close operation.
@ -351,13 +332,10 @@ namespace datalog {
void display_rules(std::ostream & out) const { void display_rules(std::ostream & out) const {
m_rule_set.display(out); m_rule_set.display(out);
} }
void display_facts(std::ostream & out) const {
m_rmanager.display(out);
}
void display(std::ostream & out) const { void display(std::ostream & out) const {
display_rules(out); display_rules(out);
display_facts(out); if (m_rel) m_rel->display_facts(out);
} }
void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out); void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out);
@ -407,23 +385,16 @@ namespace datalog {
/** /**
Query multiple output relations. Query multiple output relations.
*/ */
lbool dl_query(unsigned num_rels, func_decl * const* rels); lbool rel_query(unsigned num_rels, func_decl * const* rels);
/**
Reset tables that are under negation.
*/
void reset_negated_tables();
/**
Just reset all tables.
*/
void reset_tables();
/** /**
\brief retrieve last proof status. \brief retrieve last proof status.
*/ */
execution_result get_status(); execution_result get_status();
void set_status(execution_result r) { m_last_status = r; }
/** /**
\brief retrieve formula corresponding to query that returns l_true. \brief retrieve formula corresponding to query that returns l_true.
The formula describes one or more instances of the existential variables The formula describes one or more instances of the existential variables
@ -446,29 +417,36 @@ namespace datalog {
*/ */
bool result_contains_fact(relation_fact const& f); bool result_contains_fact(relation_fact const& f);
#if 0
/** /**
\brief display facts generated for query. \brief display facts generated for query.
*/ */
void display_output_facts(std::ostream & out) const { void display_output_facts(std::ostream & out) const {
m_rmanager.display_output_tables(out); get_rel_context().get_rmanager().display_output_tables(out);
} }
#endif
/** rel_context& get_rel_context() { ensure_rel(); return *m_rel; }
\brief expose datalog saturation for test.
*/
lbool dl_saturate();
private: private:
/**
Just reset all tables.
*/
void reset_tables();
void flush_add_rules(); void flush_add_rules();
void ensure_pdr(); void ensure_pdr();
void ensure_bmc(); void ensure_bmc();
void ensure_rel();
void new_query(); void new_query();
lbool dl_query(expr* query); lbool rel_query(expr* query);
lbool pdr_query(expr* query); lbool pdr_query(expr* query);

2
src/muz_qe/dl_costs.cpp
View file

@ -115,7 +115,7 @@ namespace datalog {
} }
void accounted_object::output_profile(context & ctx, std::ostream & out) const { void accounted_object::output_profile(std::ostream & out) const {
costs c; costs c;
get_total_cost(c); get_total_cost(c);
c.output(out); c.output(out);

2
src/muz_qe/dl_costs.h
View file

@ -79,7 +79,7 @@ namespace datalog {
void process_costs(); void process_costs();
bool passes_output_thresholds(context & ctx) const; bool passes_output_thresholds(context & ctx) const;
void output_profile(context & ctx, std::ostream & out) const; void output_profile(std::ostream & out) const;
private: private:
//private and undefined copy constructor and operator= to avoid the default ones //private and undefined copy constructor and operator= to avoid the default ones

74
src/muz_qe/dl_instruction.cpp
View file

@ -33,11 +33,11 @@ namespace datalog {
// //
// ----------------------------------- // -----------------------------------
execution_context::execution_context(context & datalog_context) execution_context::execution_context(context & context)
: m_datalog_context(datalog_context), : m_context(context),
m_stopwatch(0), m_stopwatch(0),
m_timelimit_ms(0), m_timelimit_ms(0),
m_eager_emptiness_checking(datalog_context.eager_emptiness_checking()) {} m_eager_emptiness_checking(context.eager_emptiness_checking()) {}
execution_context::~execution_context() { execution_context::~execution_context() {
reset(); reset();
@ -135,12 +135,12 @@ namespace datalog {
process_costs(); process_costs();
} }
void instruction::display_indented(context & ctx, std::ostream & out, std::string indentation) const { void instruction::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const {
out << indentation; out << indentation;
display_head_impl(ctx, out); display_head_impl(ctx, out);
if (ctx.output_profile()) { if (ctx.output_profile()) {
out << " {"; out << " {";
output_profile(ctx, out); output_profile(out);
out << '}'; out << '}';
} }
out << "\n"; out << "\n";
@ -157,10 +157,10 @@ namespace datalog {
virtual bool perform(execution_context & ctx) { virtual bool perform(execution_context & ctx) {
if (m_store) { if (m_store) {
if (ctx.reg(m_reg)) { if (ctx.reg(m_reg)) {
ctx.get_datalog_context().store_relation(m_pred, ctx.release_reg(m_reg)); ctx.get_rel_context().store_relation(m_pred, ctx.release_reg(m_reg));
} }
else { else {
context & dctx = ctx.get_datalog_context(); rel_context & dctx = ctx.get_rel_context();
relation_base * empty_rel; relation_base * empty_rel;
//the object referenced by sig is valid only until we call dctx.store_relation() //the object referenced by sig is valid only until we call dctx.store_relation()
const relation_signature & sig = dctx.get_relation(m_pred).get_signature(); const relation_signature & sig = dctx.get_relation(m_pred).get_signature();
@ -169,7 +169,7 @@ namespace datalog {
} }
} }
else { else {
relation_base& rel = ctx.get_datalog_context().get_relation(m_pred); relation_base& rel = ctx.get_rel_context().get_relation(m_pred);
if ((!ctx.eager_emptiness_checking() || !rel.empty())) { if ((!ctx.eager_emptiness_checking() || !rel.empty())) {
ctx.set_reg(m_reg, rel.clone()); ctx.set_reg(m_reg, rel.clone());
} }
@ -182,7 +182,7 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) { virtual void make_annotations(execution_context & ctx) {
ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str()); ctx.set_register_annotation(m_reg, m_pred->get_name().bare_str());
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
const char * rel_name = m_pred->get_name().bare_str(); const char * rel_name = m_pred->get_name().bare_str();
if (m_store) { if (m_store) {
out << "store " << m_reg << " into " << rel_name; out << "store " << m_reg << " into " << rel_name;
@ -213,7 +213,7 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) { virtual void make_annotations(execution_context & ctx) {
ctx.set_register_annotation(m_reg, "alloc"); ctx.set_register_annotation(m_reg, "alloc");
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "dealloc " << m_reg; out << "dealloc " << m_reg;
} }
}; };
@ -248,7 +248,7 @@ namespace datalog {
ctx.set_register_annotation(m_src, str); ctx.set_register_annotation(m_src, str);
} }
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt; out << (m_clone ? "clone " : "move ") << m_src << " into " << m_tgt;
} }
}; };
@ -304,11 +304,11 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) { virtual void make_annotations(execution_context & ctx) {
m_body->make_annotations(ctx); m_body->make_annotations(ctx);
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "while"; out << "while";
print_container(m_controls, out); print_container(m_controls, out);
} }
virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const { virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {
m_body->display_indented(ctx, out, indentation+" "); m_body->display_indented(ctx, out, indentation+" ");
} }
}; };
@ -349,9 +349,9 @@ namespace datalog {
} }
TRACE("dl", TRACE("dl",
r1.get_signature().output(ctx.get_datalog_context().get_manager(), tout); r1.get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<r1.get_size_estimate_rows()<<" x "; tout<<":"<<r1.get_size_estimate_rows()<<" x ";
r2.get_signature().output(ctx.get_datalog_context().get_manager(), tout); r2.get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";); tout<<":"<<r2.get_size_estimate_rows()<<" ->\n";);
try { try {
@ -371,7 +371,7 @@ namespace datalog {
} }
TRACE("dl", TRACE("dl",
ctx.reg(m_res)->get_signature().output(ctx.get_datalog_context().get_manager(), tout); ctx.reg(m_res)->get_signature().output(ctx.get_rel_context().get_manager(), tout);
tout<<":"<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";); tout<<":"<<ctx.reg(m_res)->get_size_estimate_rows()<<"\n";);
if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) { if (ctx.eager_emptiness_checking() && ctx.reg(m_res)->empty()) {
@ -385,7 +385,7 @@ namespace datalog {
ctx.get_register_annotation(m_rel1, a1); ctx.get_register_annotation(m_rel1, a1);
ctx.set_register_annotation(m_res, "join " + a1 + " " + a2); ctx.set_register_annotation(m_res, "join " + a1 + " " + a2);
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "join " << m_rel1; out << "join " << m_rel1;
print_container(m_cols1, out); print_container(m_cols1, out);
out << " and " << m_rel2; out << " and " << m_rel2;
@ -431,10 +431,10 @@ namespace datalog {
} }
virtual void make_annotations(execution_context & ctx) { virtual void make_annotations(execution_context & ctx) {
std::stringstream a; std::stringstream a;
a << "filter_equal " << m_col << " val: " << ctx.get_datalog_context().get_rmanager().to_nice_string(m_value); 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()); ctx.set_register_annotation(m_reg, a.str());
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_equal " << m_reg << " col: " << m_col << " val: " out << "filter_equal " << m_reg << " col: " << m_col << " val: "
<< ctx.get_rmanager().to_nice_string(m_value); << ctx.get_rmanager().to_nice_string(m_value);
} }
@ -476,7 +476,7 @@ namespace datalog {
} }
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_identical " << m_reg << " "; out << "filter_identical " << m_reg << " ";
print_container(m_cols, out); print_container(m_cols, out);
} }
@ -519,7 +519,7 @@ namespace datalog {
} }
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_interpreted " << m_reg << " using " out << "filter_interpreted " << m_reg << " using "
<< mk_pp(m_cond, m_cond.get_manager()); << mk_pp(m_cond, m_cond.get_manager());
} }
@ -624,7 +624,7 @@ namespace datalog {
ctx.set_register_annotation(m_delta, "delta of "+str); ctx.set_register_annotation(m_delta, "delta of "+str);
} }
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt; out << (m_widen ? "widen " : "union ") << m_src << " into " << m_tgt;
if (m_delta!=execution_context::void_register) { if (m_delta!=execution_context::void_register) {
out << " with delta " << m_delta; out << " with delta " << m_delta;
@ -678,7 +678,7 @@ namespace datalog {
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt; out << (m_projection ? "project " : "rename ") << m_src << " into " << m_tgt;
out << (m_projection ? " deleting columns " : " with cycle "); out << (m_projection ? " deleting columns " : " with cycle ");
print_container(m_cols, out); print_container(m_cols, out);
@ -739,7 +739,7 @@ namespace datalog {
} }
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "join_project " << m_rel1; out << "join_project " << m_rel1;
print_container(m_cols1, out); print_container(m_cols1, out);
out << " and " << m_rel2; out << " and " << m_rel2;
@ -800,7 +800,7 @@ namespace datalog {
} }
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col out << "select_equal_and_project " << m_src <<" into " << m_result << " col: " << m_col
<< " val: " << ctx.get_rmanager().to_nice_string(m_value); << " val: " << ctx.get_rmanager().to_nice_string(m_value);
} }
@ -809,7 +809,7 @@ namespace datalog {
std::string s1 = "src"; std::string s1 = "src";
ctx.get_register_annotation(m_src, s1); ctx.get_register_annotation(m_src, s1);
s << "select equal project col " << m_col << " val: " s << "select equal project col " << m_col << " val: "
<< ctx.get_datalog_context().get_rmanager().to_nice_string(m_value) << " " << s1; << ctx.get_rel_context().get_rmanager().to_nice_string(m_value) << " " << s1;
ctx.set_register_annotation(m_result, s.str()); ctx.set_register_annotation(m_result, s.str());
} }
}; };
@ -854,7 +854,7 @@ namespace datalog {
} }
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "filter_by_negation on " << m_tgt; out << "filter_by_negation on " << m_tgt;
print_container(m_cols1, out); print_container(m_cols1, out);
out << " with " << m_neg_rel; out << " with " << m_neg_rel;
@ -887,12 +887,12 @@ namespace datalog {
} }
virtual bool perform(execution_context & ctx) { virtual bool perform(execution_context & ctx) {
ctx.make_empty(m_tgt); ctx.make_empty(m_tgt);
relation_base * rel = ctx.get_datalog_context().get_rmanager().mk_empty_relation(m_sig, m_pred); relation_base * rel = ctx.get_rel_context().get_rmanager().mk_empty_relation(m_sig, m_pred);
rel->add_fact(m_fact); rel->add_fact(m_fact);
ctx.set_reg(m_tgt, rel); ctx.set_reg(m_tgt, rel);
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "mk_unary_singleton into " << m_tgt << " sort:" 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]) << " val:"
<< ctx.get_rmanager().to_nice_string(m_sig[0], m_fact[0]); << ctx.get_rmanager().to_nice_string(m_sig[0], m_fact[0]);
@ -919,10 +919,10 @@ namespace datalog {
instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {} instr_mk_total(const relation_signature & sig, func_decl* p, reg_idx tgt) : m_sig(sig), m_pred(p), m_tgt(tgt) {}
virtual bool perform(execution_context & ctx) { virtual bool perform(execution_context & ctx) {
ctx.make_empty(m_tgt); ctx.make_empty(m_tgt);
ctx.set_reg(m_tgt, ctx.get_datalog_context().get_rmanager().mk_full_relation(m_sig, m_pred)); ctx.set_reg(m_tgt, ctx.get_rel_context().get_rmanager().mk_full_relation(m_sig, m_pred));
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "mk_total into " << m_tgt << " sort:" out << "mk_total into " << m_tgt << " sort:"
<< ctx.get_rmanager().to_nice_string(m_sig); << ctx.get_rmanager().to_nice_string(m_sig);
} }
@ -944,10 +944,10 @@ namespace datalog {
instr_mark_saturated(ast_manager & m, func_decl * pred) instr_mark_saturated(ast_manager & m, func_decl * pred)
: m_pred(pred, m) {} : m_pred(pred, m) {}
virtual bool perform(execution_context & ctx) { virtual bool perform(execution_context & ctx) {
ctx.get_datalog_context().get_rmanager().mark_saturated(m_pred); ctx.get_rel_context().get_rmanager().mark_saturated(m_pred);
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "mark_saturated " << m_pred->get_name().bare_str(); out << "mark_saturated " << m_pred->get_name().bare_str();
} }
virtual void make_annotations(execution_context & ctx) { virtual void make_annotations(execution_context & ctx) {
@ -970,7 +970,7 @@ namespace datalog {
} }
return true; return true;
} }
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "instr_assert_signature of " << m_tgt << " signature:"; out << "instr_assert_signature of " << m_tgt << " signature:";
print_container(m_sig, out); print_container(m_sig, out);
} }
@ -1019,7 +1019,7 @@ namespace datalog {
TRACE("dl", TRACE("dl",
tout <<"% "; tout <<"% ";
instr->display_head_impl(ctx.get_datalog_context(), tout); instr->display_head_impl(ctx.get_rel_context(), tout);
tout <<"\n";); tout <<"\n";);
success = !ctx.should_terminate() && instr->perform(ctx); success = !ctx.should_terminate() && instr->perform(ctx);
} }
@ -1042,12 +1042,12 @@ namespace datalog {
} }
} }
void instruction_block::display_indented(context & ctx, std::ostream & out, std::string indentation) const { void instruction_block::display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const {
instr_seq_type::const_iterator it = m_data.begin(); instr_seq_type::const_iterator it = m_data.begin();
instr_seq_type::const_iterator end = m_data.end(); instr_seq_type::const_iterator end = m_data.end();
for(; it!=end; ++it) { for(; it!=end; ++it) {
instruction * i = (*it); instruction * i = (*it);
if (i->passes_output_thresholds(ctx) || i->being_recorded()) { if (i->passes_output_thresholds(ctx.get_context()) || i->being_recorded()) {
i->display_indented(ctx, out, indentation); i->display_indented(ctx, out, indentation);
} }
} }

18
src/muz_qe/dl_instruction.h
View file

@ -58,7 +58,7 @@ namespace datalog {
private: private:
typedef u_map<std::string> reg_annotations; typedef u_map<std::string> reg_annotations;
context & m_datalog_context; context & m_context;
reg_vector m_registers; reg_vector m_registers;
reg_annotations m_reg_annotation; reg_annotations m_reg_annotation;
@ -73,12 +73,12 @@ namespace datalog {
*/ */
bool m_eager_emptiness_checking; bool m_eager_emptiness_checking;
public: public:
execution_context(context & datalog_context); execution_context(context & context);
~execution_context(); ~execution_context();
void reset(); void reset();
context & get_datalog_context() { return m_datalog_context; }; rel_context & get_rel_context() { return m_context.get_rel_context(); };
void set_timelimit(unsigned time_in_ms); void set_timelimit(unsigned time_in_ms);
void reset_timelimit(); void reset_timelimit();
@ -208,7 +208,7 @@ namespace datalog {
The newline character at the end should not be printed. The newline character at the end should not be printed.
*/ */
virtual void display_head_impl(context & ctx, std::ostream & out) const { virtual void display_head_impl(rel_context & ctx, std::ostream & out) const {
out << "<instruction>"; out << "<instruction>";
} }
/** /**
@ -216,7 +216,7 @@ namespace datalog {
Each line must be prepended by \c indentation and ended by a newline character. Each line must be prepended by \c indentation and ended by a newline character.
*/ */
virtual void display_body_impl(context & ctx, std::ostream & out, std::string indentation) const {} virtual void display_body_impl(rel_context & ctx, std::ostream & out, std::string indentation) const {}
public: public:
typedef execution_context::reg_type reg_type; typedef execution_context::reg_type reg_type;
typedef execution_context::reg_idx reg_idx; typedef execution_context::reg_idx reg_idx;
@ -227,10 +227,10 @@ namespace datalog {
virtual void make_annotations(execution_context & ctx) = 0; virtual void make_annotations(execution_context & ctx) = 0;
void display(context & ctx, std::ostream & out) const { void display(rel_context & ctx, std::ostream & out) const {
display_indented(ctx, out, ""); display_indented(ctx, out, "");
} }
void display_indented(context & ctx, std::ostream & out, std::string indentation) const; void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt); static instruction * mk_load(ast_manager & m, func_decl * pred, reg_idx tgt);
/** /**
@ -329,10 +329,10 @@ namespace datalog {
void make_annotations(execution_context & ctx); void make_annotations(execution_context & ctx);
void display(context & ctx, std::ostream & out) const { void display(rel_context & ctx, std::ostream & out) const {
display_indented(ctx, out, ""); display_indented(ctx, out, "");
} }
void display_indented(context & ctx, std::ostream & out, std::string indentation) const; void display_indented(rel_context & ctx, std::ostream & out, std::string indentation) const;
}; };

6
src/muz_qe/dl_mk_explanations.cpp
View file

@ -607,7 +607,7 @@ namespace datalog {
m_e_sort = m_decl_util.mk_rule_sort(); m_e_sort = m_decl_util.mk_rule_sort();
m_pinned.push_back(m_e_sort); m_pinned.push_back(m_e_sort);
relation_manager & rmgr = ctx.get_rmanager(); relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
symbol er_symbol = explanation_relation_plugin::get_name(relation_level); symbol er_symbol = explanation_relation_plugin::get_name(relation_level);
m_er_plugin = static_cast<explanation_relation_plugin *>(rmgr.get_relation_plugin(er_symbol)); m_er_plugin = static_cast<explanation_relation_plugin *>(rmgr.get_relation_plugin(er_symbol));
if(!m_er_plugin) { if(!m_er_plugin) {
@ -640,7 +640,7 @@ namespace datalog {
void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) { void mk_explanations::assign_rel_level_kind(func_decl * e_decl, func_decl * orig) {
SASSERT(m_relation_level); SASSERT(m_relation_level);
relation_manager & rmgr = m_context.get_rmanager(); relation_manager & rmgr = m_context.get_rel_context().get_rmanager();
unsigned sz = e_decl->get_arity(); unsigned sz = e_decl->get_arity();
relation_signature sig; relation_signature sig;
rmgr.from_predicate(e_decl, sig); rmgr.from_predicate(e_decl, sig);
@ -884,7 +884,7 @@ namespace datalog {
m_context.collect_predicates(m_original_preds); m_context.collect_predicates(m_original_preds);
rule_set * res = alloc(rule_set, m_context); rule_set * res = alloc(rule_set, m_context);
transform_facts(m_context.get_rmanager()); transform_facts(m_context.get_rel_context().get_rmanager());
transform_rules(source, *res); transform_rules(source, *res);
return res; return res;
} }

2
src/muz_qe/dl_mk_magic_sets.cpp
View file

@ -365,7 +365,7 @@ namespace datalog {
rule * r = *it; rule * r = *it;
transform_rule(task.m_adornment, r); transform_rule(task.m_adornment, r);
} }
if(!m_context.get_relation(task.m_pred).empty()) { if(!m_context.get_rel_context().get_relation(task.m_pred).empty()) {
//we need a rule to copy facts that are already in a relation into the adorned //we need a rule to copy facts that are already in a relation into the adorned
//relation (since out intentional predicates can have facts, not only rules) //relation (since out intentional predicates can have facts, not only rules)
create_transfer_rule(task); create_transfer_rule(task);

2
src/muz_qe/dl_mk_partial_equiv.cpp
View file

@ -97,7 +97,7 @@ namespace datalog {
return 0; return 0;
} }
relation_manager & rm = m_context.get_rmanager(); relation_manager & rm = m_context.get_rel_context().get_rmanager();
rule_set::decl2rules::iterator it = source.begin_grouped_rules(); rule_set::decl2rules::iterator it = source.begin_grouped_rules();
rule_set::decl2rules::iterator end = source.end_grouped_rules(); rule_set::decl2rules::iterator end = source.end_grouped_rules();

2
src/muz_qe/dl_mk_rule_inliner.cpp
View file

@ -205,7 +205,7 @@ namespace datalog {
void mk_rule_inliner::count_pred_occurrences(rule_set const & orig) void mk_rule_inliner::count_pred_occurrences(rule_set const & orig)
{ {
m_context.get_rmanager().collect_non_empty_predicates(m_preds_with_facts); m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_preds_with_facts);
rule_set::iterator rend = orig.end(); rule_set::iterator rend = orig.end();
for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) { for (rule_set::iterator rit = orig.begin(); rit!=rend; ++rit) {

2
src/muz_qe/dl_mk_similarity_compressor.cpp
View file

@ -361,7 +361,7 @@ namespace datalog {
collect_orphan_consts(*it, const_infos, val_fact); collect_orphan_consts(*it, const_infos, val_fact);
m_context.add_fact(aux_pred, val_fact); m_context.add_fact(aux_pred, val_fact);
} }
m_context.get_rmanager().mark_saturated(aux_pred); m_context.get_rel_context().get_rmanager().mark_saturated(aux_pred);
app * new_head = r->get_head(); app * new_head = r->get_head();
ptr_vector<app> new_tail; ptr_vector<app> new_tail;

9
src/muz_qe/dl_mk_simple_joins.cpp
View file

@ -569,10 +569,11 @@ namespace datalog {
cost estimate_size(app * t) const { cost estimate_size(app * t) const {
func_decl * pred = t->get_decl(); func_decl * pred = t->get_decl();
unsigned n=pred->get_arity(); unsigned n=pred->get_arity();
if( (m_context.saturation_was_run() && m_context.get_rmanager().try_get_relation(pred)) relation_manager& rm = m_context.get_rel_context().get_rmanager();
|| m_context.get_rmanager().is_saturated(pred)) { if( (m_context.saturation_was_run() && rm.try_get_relation(pred))
SASSERT(m_context.get_rmanager().try_get_relation(pred)); //if it is saturated, it should exist || rm.is_saturated(pred)) {
unsigned rel_size_int = m_context.get_relation(pred).get_size_estimate_rows(); SASSERT(rm.try_get_relation(pred)); //if it is saturated, it should exist
unsigned rel_size_int = m_context.get_rel_context().get_relation(pred).get_size_estimate_rows();
if(rel_size_int!=0) { if(rel_size_int!=0) {
cost rel_size = static_cast<cost>(rel_size_int); cost rel_size = static_cast<cost>(rel_size_int);
cost curr_size = rel_size; cost curr_size = rel_size;

2
src/muz_qe/dl_mk_subsumption_checker.cpp
View file

@ -250,7 +250,7 @@ namespace datalog {
} }
void mk_subsumption_checker::scan_for_relations_total_due_to_facts() { void mk_subsumption_checker::scan_for_relations_total_due_to_facts() {
relation_manager& rm = m_context.get_rmanager(); relation_manager& rm = m_context.get_rel_context().get_rmanager();
decl_set candidate_preds; decl_set candidate_preds;
m_context.collect_predicates(candidate_preds); m_context.collect_predicates(candidate_preds);

2
src/muz_qe/dl_mk_unbound_compressor.cpp
View file

@ -337,7 +337,7 @@ namespace datalog {
// TODO mc, pc // TODO mc, pc
m_modified = false; m_modified = false;
m_context.get_rmanager().collect_non_empty_predicates(m_non_empty_rels); m_context.get_rel_context().get_rmanager().collect_non_empty_predicates(m_non_empty_rels);
unsigned init_rule_cnt = source.get_num_rules(); unsigned init_rule_cnt = source.get_num_rules();
SASSERT(m_rules.empty()); SASSERT(m_rules.empty());

2
src/muz_qe/dl_rule.cpp
View file

@ -1014,7 +1014,7 @@ namespace datalog {
out << '.'; out << '.';
if (ctx.output_profile()) { if (ctx.output_profile()) {
out << " {"; out << " {";
output_profile(ctx, out); output_profile(out);
out << '}'; out << '}';
} }
out << '\n'; out << '\n';

34
src/muz_qe/fixedpoint_params.pyg
View file

@ -30,25 +30,25 @@ def_module_params('fixedpoint',
('print_with_fixedpoint_extensions', BOOL, True, "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"), ('print_with_fixedpoint_extensions', BOOL, True, "use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules"),
('print_low_level_smt2', BOOL, False, "use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"), ('print_low_level_smt2', BOOL, False, "use (faster) low-level SMT2 printer (the printer is scalable but the result may not be as readable)"),
('print_with_variable_declarations', BOOL, True, "use variable declarations when displaying rules (instead of attempting to use original names)"), ('print_with_variable_declarations', BOOL, True, "use variable declarations when displaying rules (instead of attempting to use original names)"),
('bfs_model_search', BOOL, True, "PDR: (default true) use BFS strategy for expanding model search"), ('bfs_model_search', BOOL, True, "PDR: use BFS strategy for expanding model search"),
('use_farkas', BOOL, True, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)"), ('use_farkas', BOOL, True, "PDR: use lemma generator based on Farkas (for linear real arithmetic)"),
('generate_proof_trace', BOOL, False, "PDR: (default false) trace for 'sat' answer as proof object"), ('generate_proof_trace', BOOL, False, "PDR: trace for 'sat' answer as proof object"),
('flexible_trace', BOOL, False, "PDR: (default false) allow PDR generate long counter-examples " ('flexible_trace', BOOL, False, "PDR: allow PDR generate long counter-examples "
"by extending candidate trace within search area"), "by extending candidate trace within search area"),
('unfold_rules', UINT, 0, "PDR: (default 0) unfold rules statically using iterative squarring"), ('unfold_rules', UINT, 0, "PDR: unfold rules statically using iterative squarring"),
('use_model_generalizer', BOOL, False, "PDR: (default false) use model for backwards propagation (instead of symbolic simulation)"), ('use_model_generalizer', BOOL, False, "PDR: use model for backwards propagation (instead of symbolic simulation)"),
('validate_result', BOOL, False, "PDR (default false) validate result (by proof checking or model checking)"), ('validate_result', BOOL, False, "PDR validate result (by proof checking or model checking)"),
('simplify_formulas_pre', BOOL, False, "PDR: (default false) simplify derived formulas before inductive propagation"), ('simplify_formulas_pre', BOOL, False, "PDR: simplify derived formulas before inductive propagation"),
('simplify_formulas_post', BOOL, False, "PDR: (default false) simplify derived formulas after inductive propagation"), ('simplify_formulas_post', BOOL, False, "PDR: simplify derived formulas after inductive propagation"),
('slice', BOOL, True, "PDR: (default true) simplify clause set using slicing"), ('slice', BOOL, True, "PDR: simplify clause set using slicing"),
('coalesce_rules', BOOL, False, "BMC: (default false) coalesce rules"), ('coalesce_rules', BOOL, False, "BMC: coalesce rules"),
('use_multicore_generalizer', BOOL, False, "PDR: (default false) extract multiple cores for blocking states"), ('use_multicore_generalizer', BOOL, False, "PDR: extract multiple cores for blocking states"),
('use_inductive_generalizer', BOOL, True, "PDR: (default true) generalize lemmas using induction strengthening"), ('use_inductive_generalizer', BOOL, True, "PDR: generalize lemmas using induction strengthening"),
('cache_mode', UINT, 0, "PDR: use no (0 - default) symbolic (1) or explicit cache (2) for model search"), ('cache_mode', UINT, 0, "PDR: use no (0), symbolic (1) or explicit cache (2) for model search"),
('inductive_reachability_check', BOOL, False, "PDR: (default false) assume negation of the cube on the previous level when " ('inductive_reachability_check', BOOL, False, "PDR: assume negation of the cube on the previous level when "
"checking for reachability (not only during cube weakening)"), "checking for reachability (not only during cube weakening)"),
('max_num_contexts', UINT, 500, "PDR: (default 500) maximal number of contexts to create"), ('max_num_contexts', UINT, 500, "PDR: maximal number of contexts to create"),
('try_minimize_core', BOOL, False, "PDR: (default false) try to reduce core size (before inductive minimization)"), ('try_minimize_core', BOOL, False, "PDR: try to reduce core size (before inductive minimization)"),
('profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"), ('profile_timeout_milliseconds', UINT, 0, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list"),
('dbg_fpr_nonempty_relation_signature', BOOL, False, ('dbg_fpr_nonempty_relation_signature', BOOL, False,
"if true, finite_product_relation will attempt to avoid creating inner relation with empty signature " "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "

1
src/muz_qe/pdr_dl_interface.cpp
View file

@ -83,7 +83,6 @@ lbool dl_interface::query(expr * query) {
m_pdr_rules.reset(); m_pdr_rules.reset();
m_refs.reset(); m_refs.reset();
m_pred2slice.reset(); m_pred2slice.reset();
m_ctx.get_rmanager().reset_relations();
ast_manager& m = m_ctx.get_manager(); ast_manager& m = m_ctx.get_manager();
datalog::rule_manager& rule_manager = m_ctx.get_rule_manager(); datalog::rule_manager& rule_manager = m_ctx.get_rule_manager();
datalog::rule_set old_rules(m_ctx.get_rules()); datalog::rule_set old_rules(m_ctx.get_rules());

517
src/muz_qe/rel_context.cpp Normal file
View file

@ -0,0 +1,517 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
rel_context.cpp
Abstract:
context for relational datalog engine.
Author:
Nikolaj Bjorner (nbjorner) 2012-12-3.
Revision History:
Extracted from dl_context
--*/
#include"rel_context.h"
#include"dl_context.h"
#include"dl_compiler.h"
#include"dl_instruction.h"
#include"dl_mk_explanations.h"
#include"dl_mk_magic_sets.h"
#include"dl_product_relation.h"
#include"dl_bound_relation.h"
#include"dl_interval_relation.h"
#include"dl_finite_product_relation.h"
#include"dl_sparse_table.h"
#include"dl_table.h"
#include"dl_table_relation.h"
#ifndef _EXTERNAL_RELEASE
#include"dl_skip_table.h"
#endif
namespace datalog {
rel_context::rel_context(context& ctx)
: m_context(ctx),
m(ctx.get_manager()),
m_rmanager(ctx),
m_answer(m),
m_cancel(false),
m_last_result_relation(0) {
get_rmanager().register_plugin(alloc(sparse_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(hashtable_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(bitvector_table_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(equivalence_table_plugin, get_rmanager()));
#ifndef _EXTERNAL_RELEASE
get_rmanager().register_plugin(alloc(skip_table_plugin, get_rmanager()));
#endif
//register plugins for builtin relations
get_rmanager().register_plugin(alloc(bound_relation_plugin, get_rmanager()));
get_rmanager().register_plugin(alloc(interval_relation_plugin, get_rmanager()));
}
rel_context::~rel_context() {
if (m_last_result_relation) {
m_last_result_relation->deallocate();
m_last_result_relation = 0;
}
}
void rel_context::collect_predicates(decl_set & res) {
unsigned rule_cnt = m_context.get_rules().get_num_rules();
for (unsigned rindex=0; rindex<rule_cnt; rindex++) {
rule * r = m_context.get_rules().get_rule(rindex);
res.insert(r->get_head()->get_decl());
unsigned tail_len = r->get_uninterpreted_tail_size();
for (unsigned tindex=0; tindex<tail_len; tindex++) {
res.insert(r->get_tail(tindex)->get_decl());
}
}
decl_set::iterator oit = m_output_preds.begin();
decl_set::iterator oend = m_output_preds.end();
for (; oit!=oend; ++oit) {
res.insert(*oit);
}
get_rmanager().collect_predicates(res);
}
lbool rel_context::saturate() {
m_context.ensure_closed();
bool time_limit = m_context.soft_timeout()!=0;
unsigned remaining_time_limit = m_context.soft_timeout();
unsigned restart_time = m_context.initial_restart_timeout();
rule_set original_rules(m_context.get_rules());
decl_set original_predicates;
m_context.collect_predicates(original_predicates);
instruction_block rules_code;
instruction_block termination_code;
execution_context ex_ctx(m_context);
lbool result;
TRACE("dl", m_context.display(tout););
while (true) {
model_converter_ref mc; // Ignored in Datalog mode
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);
TRACE("dl", rules_code.display(*this, tout); );
bool timeout_after_this_round = time_limit && (restart_time==0 || remaining_time_limit<=restart_time);
if (time_limit || restart_time!=0) {
unsigned timeout = time_limit ? (restart_time!=0) ?
std::min(remaining_time_limit, restart_time)
: remaining_time_limit : restart_time;
ex_ctx.set_timelimit(timeout);
}
bool early_termination = !rules_code.perform(ex_ctx);
ex_ctx.reset_timelimit();
VERIFY( termination_code.perform(ex_ctx) );
rules_code.process_all_costs();
IF_VERBOSE(10, ex_ctx.report_big_relations(1000, verbose_stream()););
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) {
m_context.set_status(TIMEOUT);
result = l_undef;
break;
}
SASSERT(restart_time != 0);
if (time_limit) {
SASSERT(remaining_time_limit>restart_time);
remaining_time_limit -= restart_time;
}
uint64 new_restart_time = static_cast<uint64>(restart_time)*m_context.initial_restart_timeout();
if (new_restart_time > UINT_MAX) {
restart_time = UINT_MAX;
}
else {
restart_time = static_cast<unsigned>(new_restart_time);
}
rules_code.reset();
termination_code.reset();
ex_ctx.reset();
m_context.reopen();
restrict_predicates(original_predicates);
m_context.replace_rules(original_rules);
m_context.close();
}
m_context.reopen();
restrict_predicates(original_predicates);
m_context.replace_rules(original_rules);
m_context.close();
TRACE("dl", ex_ctx.report_big_relations(100, tout););
m_cancel = false;
return result;
}
#define BEGIN_QUERY() \
rule_set original_rules(m_context.get_rules()); \
decl_set original_preds; \
m_context.collect_predicates(original_preds); \
bool was_closed = m_context.is_closed(); \
if (was_closed) { \
m_context.reopen(); \
} \
#define END_QUERY() \
m_context.reopen(); \
m_context.replace_rules(original_rules); \
restrict_predicates(original_preds); \
\
if (was_closed) { \
m_context.close(); \
} \
lbool rel_context::query(unsigned num_rels, func_decl * const* rels) {
get_rmanager().reset_saturated_marks();
BEGIN_QUERY();
for (unsigned i = 0; i < num_rels; ++i) {
set_output_predicate(rels[i]);
}
m_context.close();
reset_negated_tables();
lbool res = saturate();
switch(res) {
case l_true: {
expr_ref_vector ans(m);
expr_ref e(m);
bool some_non_empty = num_rels == 0;
for (unsigned i = 0; i < num_rels; ++i) {
relation_base& rel = get_relation(rels[i]);
if (!rel.empty()) {
some_non_empty = true;
}
rel.to_formula(e);
ans.push_back(e);
}
SASSERT(!m_last_result_relation);
if (some_non_empty) {
m_answer = m.mk_and(ans.size(), ans.c_ptr());
}
else {
m_answer = m.mk_false();
res = l_false;
}
break;
}
case l_false:
m_answer = m.mk_false();
break;
case l_undef:
break;
}
END_QUERY();
return res;
}
lbool rel_context::query(expr* query) {
get_rmanager().reset_saturated_marks();
BEGIN_QUERY();
rule_manager& rm = m_context.get_rule_manager();
rule_ref qrule(rm);
rule_ref_vector qrules(rm);
func_decl_ref query_pred(m);
try {
rm.mk_query(query, query_pred, qrules, qrule);
}
catch(default_exception& exn) {
m_context.close();
m_context.set_status(INPUT_ERROR);
throw exn;
}
try {
m_context.add_rules(qrules);
}
catch (default_exception& exn) {
m_context.close();
m_context.set_status(INPUT_ERROR);
throw exn;
}
set_output_predicate(qrule->get_head()->get_decl());
m_context.close();
reset_negated_tables();
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);
//expl_plugin is deallocated when transformer goes out of scope
mk_explanations * expl_plugin =
alloc(mk_explanations, m_context, m_context.explanations_on_relation_level());
transformer.register_plugin(expl_plugin);
m_context.transform_rules(transformer, mc, pc);
//we will retrieve the predicate with explanations instead of the original query predicate
query_pred = expl_plugin->get_e_decl(query_pred);
const rule_vector & query_rules = m_context.get_rules().get_predicate_rules(query_pred);
SASSERT(query_rules.size()==1);
qrule = query_rules.back();
}
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);
transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get()));
m_context.transform_rules(transformer, mc, pc);
}
lbool res = saturate();
if (res != l_undef) {
m_last_result_relation = get_relation(query_pred).clone();
if (m_last_result_relation->empty()) {
res = l_false;
m_answer = m.mk_false();
}
else {
m_last_result_relation->to_formula(m_answer);
}
}
END_QUERY();
return res;
}
void rel_context::reset_negated_tables() {
rule_set::pred_set_vector const & pred_sets = m_context.get_rules().get_strats();
bool non_empty = false;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
non_empty = true;
break;
}
}
}
if (!non_empty) {
return;
}
// collect predicates that depend on negation.
func_decl_set depends_on_negation;
for (unsigned i = 1; i < pred_sets.size(); ++i) {
bool change = true;
while (change) {
change = false;
func_decl_set::iterator it = pred_sets[i]->begin(), end = pred_sets[i]->end();
for (; it != end; ++it) {
func_decl* pred = *it;
if (depends_on_negation.contains(pred)) {
continue;
}
rule_vector const& rules = m_context.get_rules().get_predicate_rules(pred);
bool inserted = false;
for (unsigned j = 0; !inserted && j < rules.size(); ++j) {
rule* r = rules[j];
unsigned psz = r->get_positive_tail_size();
unsigned tsz = r->get_uninterpreted_tail_size();
if (psz < tsz) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
for (unsigned k = 0; !inserted && k < tsz; ++k) {
func_decl* tail_decl = r->get_tail(k)->get_decl();
if (depends_on_negation.contains(tail_decl)) {
depends_on_negation.insert(pred);
change = true;
inserted = true;
}
}
}
}
}
}
func_decl_set::iterator it = depends_on_negation.begin(), end = depends_on_negation.end();
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
TRACE("dl", tout << "Resetting: " << mk_ismt2_pp(pred, m) << "\n";);
rel.reset();
}
}
}
void rel_context::set_output_predicate(func_decl * pred) {
if (!m_output_preds.contains(pred)) {
m_output_preds.insert(pred);
}
}
void rel_context::restrict_predicates( const decl_set & res ) {
set_intersection(m_output_preds, res);
get_rmanager().restrict_predicates(res);
}
relation_base & rel_context::get_relation(func_decl * pred) { return get_rmanager().get_relation(pred); }
relation_base * rel_context::try_get_relation(func_decl * pred) const { return get_rmanager().try_get_relation(pred); }
relation_manager & rel_context::get_rmanager() { return m_rmanager; }
const relation_manager & rel_context::get_rmanager() const { return m_rmanager; }
bool rel_context::output_profile() const { return m_context.output_profile(); }
void rel_context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names) {
relation_manager & rmgr = get_rmanager();
family_id target_kind = null_family_id;
switch (relation_name_cnt) {
case 0:
return;
case 1:
target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
break;
default: {
svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
family_id rel_kind; // the aggregate kind of non-table plugins
for (unsigned i = 0; i < relation_name_cnt; i++) {
relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
rel_kinds.push_back(p.get_kind());
}
if (rel_kinds.size() == 1) {
rel_kind = rel_kinds[0];
}
else {
relation_signature rel_sig;
//rmgr.from_predicate(pred, rel_sig);
product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
}
target_kind = rel_kind;
break;
}
}
SASSERT(target_kind != null_family_id);
get_rmanager().set_predicate_kind(pred, target_kind);
}
relation_plugin & rel_context::get_ordinary_relation_plugin(symbol relation_name) {
relation_plugin * plugin = get_rmanager().get_relation_plugin(relation_name);
if (!plugin) {
std::stringstream sstm;
sstm << "relation plugin " << relation_name << " does not exist";
throw default_exception(sstm.str());
}
if (plugin->is_product_relation()) {
throw default_exception("cannot request product relation directly");
}
if (plugin->is_sieve_relation()) {
throw default_exception("cannot request sieve relation directly");
}
if (plugin->is_finite_product_relation()) {
throw default_exception("cannot request finite product relation directly");
}
return *plugin;
}
bool rel_context::result_contains_fact(relation_fact const& f) {
SASSERT(m_last_result_relation);
return m_last_result_relation->contains_fact(f);
}
void rel_context::reset_tables() {
get_rmanager().reset_saturated_marks();
rule_set::decl2rules::iterator it = m_context.get_rules().begin_grouped_rules();
rule_set::decl2rules::iterator end = m_context.get_rules().end_grouped_rules();
for (; it != end; ++it) {
func_decl* p = it->m_key;
relation_base & rel = get_relation(p);
rel.reset();
}
for (unsigned i = 0; i < m_table_facts.size(); ++i) {
func_decl* pred = m_table_facts[i].first;
relation_fact const& fact = m_table_facts[i].second;
get_relation(pred).add_fact(fact);
}
}
void rel_context::add_fact(func_decl* pred, relation_fact const& fact) {
get_rmanager().reset_saturated_marks();
get_relation(pred).add_fact(fact);
m_table_facts.push_back(std::make_pair(pred, fact));
}
void rel_context::add_fact(func_decl* pred, table_fact const& fact) {
get_rmanager().reset_saturated_marks();
relation_base & rel0 = get_relation(pred);
if (rel0.from_table()) {
table_relation & rel = static_cast<table_relation &>(rel0);
rel.add_table_fact(fact);
// TODO: table facts?
}
else {
relation_fact rfact(m);
for (unsigned i = 0; i < fact.size(); ++i) {
rfact.push_back(m_context.get_decl_util().mk_numeral(fact[i], pred->get_domain()[i]));
}
add_fact(pred, rfact);
}
}
void rel_context::store_relation(func_decl * pred, relation_base * rel) {
get_rmanager().store_relation(pred, rel);
}
void rel_context::inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred) {
if (orig_pred) {
family_id target_kind = get_rmanager().get_requested_predicate_kind(orig_pred);
if (target_kind != null_family_id) {
get_rmanager().set_predicate_kind(new_pred, target_kind);
}
}
}
void rel_context::display_output_facts(std::ostream & out) const {
get_rmanager().display_output_tables(out);
}
void rel_context::display_facts(std::ostream& out) const {
get_rmanager().display(out);
}
};

115
src/muz_qe/rel_context.h Normal file
View file

@ -0,0 +1,115 @@
/*++
Copyright (c) 2012 Microsoft Corporation
Module Name:
rel_context.h
Abstract:
context for relational datalog engine.
Author:
Nikolaj Bjorner (nbjorner) 2012-12-3.
Revision History:
Extracted from dl_context
--*/
#ifndef _REL_CONTEXT_H_
#define _REL_CONTEXT_H_
#include "ast.h"
#include "dl_relation_manager.h"
#include "lbool.h"
namespace datalog {
class context;
class rel_context {
typedef vector<std::pair<func_decl*,relation_fact> > fact_vector;
context& m_context;
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;
void reset_negated_tables();
lbool saturate();
relation_plugin & get_ordinary_relation_plugin(symbol relation_name);
void reset_tables();
public:
rel_context(context& ctx);
~rel_context();
relation_manager & get_rmanager();
const relation_manager & get_rmanager() const;
ast_manager& get_manager() { return m; }
context& get_context() { 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; }
bool output_profile() const;
lbool query(expr* q);
lbool query(unsigned num_rels, func_decl * const* rels);
void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt,
symbol const * relation_names);
void inherit_predicate_kind(func_decl* new_pred, func_decl* orig_pred);
void cancel() { m_cancel = true; }
/**
\brief Restrict the set of used predicates to \c res.
The function deallocates unsused relations, it does not deal with rules.
*/
void restrict_predicates(const decl_set & res);
void collect_predicates(decl_set & res);
void set_output_predicate(func_decl * 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; }
/**
\brief query result if it contains fact.
*/
bool result_contains_fact(relation_fact const& f);
void add_fact(func_decl* pred, relation_fact const& fact);
void add_fact(func_decl* pred, table_fact const& fact);
/**
\brief Store the relation \c rel under the predicate \c pred. The \c context object
takes over the ownership of the relation object.
*/
void store_relation(func_decl * pred, relation_base * rel);
void display_output_facts(std::ostream & out) const;
void display_facts(std::ostream & out) const;
};
};
#endif /* _REL_CONTEXT_H_ */

12
src/shell/datalog_frontend.cpp
View file

@ -86,7 +86,7 @@ static void display_statistics(
out << "--------------\n"; out << "--------------\n";
out << "instructions \n"; out << "instructions \n";
code.display(ctx, out); code.display(ctx.get_rel_context(), out);
out << "--------------\n"; out << "--------------\n";
out << "big relations \n"; out << "big relations \n";
@ -94,7 +94,7 @@ static void display_statistics(
} }
out << "--------------\n"; out << "--------------\n";
out << "relation sizes\n"; out << "relation sizes\n";
ctx.get_rmanager().display_relation_sizes(out); ctx.get_rel_context().get_rmanager().display_relation_sizes(out);
if (verbose) { if (verbose) {
out << "--------------\n"; out << "--------------\n";
@ -139,7 +139,7 @@ unsigned read_datalog(char const * file) {
params.set_bool("default_table_checked", dl_params.m_default_table_checked); params.set_bool("default_table_checked", dl_params.m_default_table_checked);
datalog::context ctx(m, s_params, params); datalog::context ctx(m, s_params, params);
datalog::relation_manager & rmgr = ctx.get_rmanager(); datalog::relation_manager & rmgr = ctx.get_rel_context().get_rmanager();
datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable")); datalog::relation_plugin & inner_plg = *rmgr.get_relation_plugin(symbol("tr_hashtable"));
SASSERT(&inner_plg); SASSERT(&inner_plg);
rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr)); rmgr.register_plugin(alloc(datalog::finite_product_relation_plugin, inner_plg, rmgr));
@ -206,7 +206,7 @@ unsigned read_datalog(char const * file) {
datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code); datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);
TRACE("dl_compiler", rules_code.display(ctx, tout);); TRACE("dl_compiler", rules_code.display(ctx.get_rel_context(), tout););
rules_code.make_annotations(ex_ctx); rules_code.make_annotations(ex_ctx);
@ -248,10 +248,10 @@ unsigned read_datalog(char const * file) {
TRACE("dl_compiler", ctx.display(tout); TRACE("dl_compiler", ctx.display(tout);
rules_code.display(ctx, tout);); rules_code.display(ctx.get_rel_context(), tout););
if (ctx.get_params().output_tuples()) { if (ctx.get_params().output_tuples()) {
ctx.display_output_facts(std::cout); ctx.get_rel_context().display_output_facts(std::cout);
} }
display_statistics( display_statistics(