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

fix build

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-05 19:24:05 -08:00
parent a5efe9c29d
commit 5bb5a50490
1 changed files with 4 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/muz/dataflow/dataflow.h
View file

@ -184,21 +184,22 @@ namespace datalog {
typename fact_db::entry* entry; typename fact_db::entry* entry;
if (m_facts.insert_if_not_there_core(kv.m_key, entry)) { if (m_facts.insert_if_not_there_core(kv.m_key, entry)) {
entry->get_data().m_value = kv.m_value; entry->get_data().m_value = kv.m_value;
} else { }
else {
entry->get_data().m_value.join(m_context, kv.m_value); entry->get_data().m_value.join(m_context, kv.m_value);
} }
} }
} }
void intersect(const dataflow_engine<Fact>& oth) { void intersect(const dataflow_engine<Fact>& oth) {
vector<func_decl*> to_delete; ptr_vector<func_decl> to_delete;
for (auto const& kv : m_facts) { for (auto const& kv : m_facts) {
if (typename fact_db::entry *entry = oth.m_facts.find_core(kv.m_key)) { if (typename fact_db::entry *entry = oth.m_facts.find_core(kv.m_key)) {
kv.m_value.intersect(m_context, entry->get_data().m_value); kv.m_value.intersect(m_context, entry->get_data().m_value);
} }
else { else {
to_delete.push_back(kvm_key); to_delete.push_back(kv.m_key);
} }
} }
for (func_decl* f : to_delete) { for (func_decl* f : to_delete) {