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

fix #4870

Browse source
This commit is contained in:
Nikolaj Bjorner 2020-12-07 17:52:56 -08:00
parent 9f6a0a868a
commit 430b4ea252
1 changed files with 31 additions and 24 deletions
Download patch file Download diff file Expand all files Collapse all files

37
src/muz/rel/dl_mk_simple_joins.cpp
View file

@ -20,10 +20,10 @@ Revision History:
#include<utility> #include<utility>
#include<sstream> #include<sstream>
#include<limits> #include<limits>
#include "muz/rel/dl_mk_simple_joins.h"
#include "muz/rel/dl_relation_manager.h"
#include "ast/ast_pp.h" #include "ast/ast_pp.h"
#include "util/trace.h" #include "util/trace.h"
#include "muz/rel/dl_mk_simple_joins.h"
#include "muz/rel/dl_relation_manager.h"
namespace datalog { namespace datalog {
@ -47,14 +47,14 @@ namespace datalog {
being notified about it, it will surely see the decrease from length 3 to 2 which being notified about it, it will surely see the decrease from length 3 to 2 which
the threshold for rule being counted in this counter. the threshold for rule being counted in this counter.
*/ */
unsigned m_consumers; unsigned m_consumers { 0 };
bool m_stratified; bool m_stratified { true };
unsigned m_src_stratum; unsigned m_src_stratum { 0 };
public: public:
var_idx_set m_all_nonlocal_vars; var_idx_set m_all_nonlocal_vars;
rule_vector m_rules; rule_vector m_rules;
pair_info() : m_consumers(0), m_stratified(true), m_src_stratum(0) {} pair_info() {}
bool can_be_joined() const { bool can_be_joined() const {
return m_consumers > 0; return m_consumers > 0;
@ -246,7 +246,7 @@ namespace datalog {
m_pinned.push_back(t1n); m_pinned.push_back(t1n);
m_pinned.push_back(t2n); m_pinned.push_back(t2n);
TRACE("dl", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << " |-> " << t1n_ref << " " << t2n_ref << "\n";); TRACE("dl_verbose", tout << mk_pp(t1, m) << " " << mk_pp(t2, m) << " |-> " << t1n_ref << " " << t2n_ref << "\n";);
return app_pair(t1n, t2n); return app_pair(t1n, t2n);
} }
@ -555,6 +555,18 @@ namespace datalog {
TRACE("dl", tout << mk_pp(rt2, m) << " " << mk_pp(rt1, m) << " -> " << new_transf << "\n";); TRACE("dl", tout << mk_pp(rt2, m) << " " << mk_pp(rt1, m) << " -> " << new_transf << "\n";);
} }
app * new_lit = to_app(new_transf); app * new_lit = to_app(new_transf);
if (added_tails.contains(new_lit)) {
if (i1 < rule_content.size())
rule_content[i1] = rule_content.back();
rule_content.pop_back();
if (i2 < rule_content.size())
rule_content[i2] = rule_content.back();
rule_content.pop_back();
len -= 2;
removed_tails.push_back(rt1);
removed_tails.push_back(rt2);
}
else {
m_pinned.push_back(new_lit); m_pinned.push_back(new_lit);
rule_content[i1] = new_lit; rule_content[i1] = new_lit;
rule_content[i2] = rule_content.back(); rule_content[i2] = rule_content.back();
@ -563,6 +575,7 @@ namespace datalog {
removed_tails.push_back(rt1); removed_tails.push_back(rt1);
removed_tails.push_back(rt2); removed_tails.push_back(rt2);
added_tails.push_back(new_lit); added_tails.push_back(new_lit);
}
// this exits the inner loop, the outer one continues in case there will // this exits the inner loop, the outer one continues in case there will
// be other matches // be other matches
break; break;
@ -657,10 +670,8 @@ namespace datalog {
bool pick_best_pair(app_pair & p) { bool pick_best_pair(app_pair & p) {
app_pair best;
bool found = false; bool found = false;
cost best_cost; cost best_cost;
for (auto const& kv : m_costs) { for (auto const& kv : m_costs) {
app_pair key = kv.m_key; app_pair key = kv.m_key;
pair_info & inf = *kv.m_value; pair_info & inf = *kv.m_value;
@ -671,14 +682,10 @@ namespace datalog {
if (!found || c < best_cost) { if (!found || c < best_cost) {
found = true; found = true;
best_cost = c; best_cost = c;
best = key; p = key;
} }
} }
if (!found) { return found;
return false;
}
p = best;
return true;
} }