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

fix #3777

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-05 15:08:28 -07:00
parent 406c0792f1
commit b79b8c9bc4
3 changed files with 22 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

24
src/muz/base/dl_rule_transformer.cpp
View file

@ -36,21 +36,15 @@ namespace datalog {
} }
void rule_transformer::reset() { void rule_transformer::reset() {
plugin_vector::iterator it = m_plugins.begin(); for (auto* p : m_plugins)
plugin_vector::iterator end = m_plugins.end(); dealloc(p);
for(; it!=end; ++it) {
dealloc(*it);
}
m_plugins.reset(); m_plugins.reset();
m_dirty = false; m_dirty = false;
} }
void rule_transformer::cancel() { void rule_transformer::cancel() {
plugin_vector::iterator it = m_plugins.begin(); for (auto* p : m_plugins)
plugin_vector::iterator end = m_plugins.end(); p->cancel();
for(; it!=end; ++it) {
(*it)->cancel();
}
} }
struct rule_transformer::plugin_comparator { struct rule_transformer::plugin_comparator {
@ -81,7 +75,7 @@ namespace datalog {
tout<<"init:\n"; tout<<"init:\n";
rules.display(tout); rules.display(tout);
); );
rule_set* new_rules = alloc(rule_set, rules); scoped_ptr<rule_set> new_rules = alloc(rule_set, rules);
plugin_vector::iterator it = m_plugins.begin(); plugin_vector::iterator it = m_plugins.begin();
plugin_vector::iterator end = m_plugins.end(); plugin_vector::iterator end = m_plugins.end();
for(; it!=end && !m_context.canceled(); ++it) { for(; it!=end && !m_context.canceled(); ++it) {
@ -91,7 +85,7 @@ namespace datalog {
IF_VERBOSE(1, verbose_stream() << "(transform " << typeid(p).name() << "...";); IF_VERBOSE(1, verbose_stream() << "(transform " << typeid(p).name() << "...";);
stopwatch sw; stopwatch sw;
sw.start(); sw.start();
rule_set * new_rules1 = p(*new_rules); scoped_ptr<rule_set> new_rules1 = p(*new_rules);
sw.stop(); sw.stop();
double sec = sw.get_seconds(); double sec = sw.get_seconds();
if (sec < 0.001) sec = 0.0; if (sec < 0.001) sec = 0.0;
@ -104,13 +98,12 @@ namespace datalog {
!new_rules1->close()) { !new_rules1->close()) {
warning_msg("a rule transformation skipped " warning_msg("a rule transformation skipped "
"because it destratified negation"); "because it destratified negation");
dealloc(new_rules1); new_rules1 = nullptr;
IF_VERBOSE(1, verbose_stream() << "no-op " << sec << "s)\n";); IF_VERBOSE(1, verbose_stream() << "no-op " << sec << "s)\n";);
continue; continue;
} }
modified = true; modified = true;
dealloc(new_rules); new_rules = new_rules1.detach();
new_rules = new_rules1;
new_rules->ensure_closed(); new_rules->ensure_closed();
IF_VERBOSE(1, verbose_stream() << new_rules->get_num_rules() << " rules " << sec << "s)\n";); IF_VERBOSE(1, verbose_stream() << new_rules->get_num_rules() << " rules " << sec << "s)\n";);
@ -122,7 +115,6 @@ namespace datalog {
if (modified) { if (modified) {
rules.replace_rules(*new_rules); rules.replace_rules(*new_rules);
} }
dealloc(new_rules);
return modified; return modified;
} }

16
src/muz/rel/dl_mk_explanations.cpp
View file

@ -628,6 +628,9 @@ namespace datalog {
); );
} }
mk_explanations::~mk_explanations() {
}
func_decl * mk_explanations::get_union_decl(context & ctx) { func_decl * mk_explanations::get_union_decl(context & ctx) {
ast_manager & m = ctx.get_manager(); ast_manager & m = ctx.get_manager();
sort_ref s(ctx.get_decl_util().mk_rule_sort(), m); sort_ref s(ctx.get_decl_util().mk_rule_sort(), m);
@ -669,7 +672,7 @@ namespace datalog {
func_decl * mk_explanations::get_e_decl(func_decl * orig_decl) { func_decl * mk_explanations::get_e_decl(func_decl * orig_decl) {
decl_map::obj_map_entry * e = m_e_decl_map.insert_if_not_there2(orig_decl, 0); decl_map::obj_map_entry * e = m_e_decl_map.insert_if_not_there2(orig_decl, 0);
if (e->get_data().m_value==0) { if (e->get_data().m_value == nullptr) {
relation_signature e_domain; relation_signature e_domain;
e_domain.append(orig_decl->get_arity(), orig_decl->get_domain()); e_domain.append(orig_decl->get_arity(), orig_decl->get_domain());
e_domain.push_back(m_e_sort); e_domain.push_back(m_e_sort);
@ -790,8 +793,11 @@ namespace datalog {
product_relation & prod_rel = static_cast<product_relation &>(e_rel); product_relation & prod_rel = static_cast<product_relation &>(e_rel);
SASSERT(prod_rel.size()==2); SASSERT(prod_rel.size()==2);
SASSERT(prod_rel[0].get_plugin().is_sieve_relation());
SASSERT(prod_rel[1].get_plugin().is_sieve_relation()); if (!prod_rel[0].get_plugin().is_sieve_relation())
throw default_exception("explanations are not supported for this query");
if (!prod_rel[1].get_plugin().is_sieve_relation())
throw default_exception("explanations are not supported for this query");
sieve_relation * srels[] = { sieve_relation * srels[] = {
static_cast<sieve_relation *>(&prod_rel[0]), static_cast<sieve_relation *>(&prod_rel[0]),
static_cast<sieve_relation *>(&prod_rel[1]) }; static_cast<sieve_relation *>(&prod_rel[1]) };
@ -876,10 +882,10 @@ namespace datalog {
if (!m_context.generate_explanations()) { if (!m_context.generate_explanations()) {
return nullptr; return nullptr;
} }
rule_set * res = alloc(rule_set, m_context); scoped_ptr<rule_set> res = alloc(rule_set, m_context);
transform_facts(m_context.get_rel_context()->get_rmanager(), source, *res); transform_facts(m_context.get_rel_context()->get_rmanager(), source, *res);
transform_rules(source, *res); transform_rules(source, *res);
return res; return res.detach();
} }
}; };

2
src/muz/rel/dl_mk_explanations.h
View file

@ -66,6 +66,8 @@ namespace datalog {
*/ */
mk_explanations(context & ctx); mk_explanations(context & ctx);
~mk_explanations() override;
/** /**
\brief Return explanation predicate that corresponds to \c orig_decl. \brief Return explanation predicate that corresponds to \c orig_decl.
*/ */