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

fix #3814

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-07 10:40:36 -07:00
parent cb136418d5
commit 8dac9b7b94
6 changed files with 14 additions and 17 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/muz/base/dl_rule_set.h
View file

@ -254,6 +254,7 @@ namespace datalog {
void set_output_predicate(func_decl * pred) { m_refs.push_back(pred); m_output_preds.insert(pred); }
bool is_output_predicate(func_decl * pred) const { return m_output_preds.contains(pred); }
void inherit_output_predicate(rule_set const& src, func_decl* pred) { if (src.is_output_predicate(pred) && !is_output_predicate(pred)) set_output_predicate(pred); }
const func_decl_set & get_output_predicates() const { return m_output_preds; }
func_decl* get_output_predicate() const { SASSERT(m_output_preds.size() == 1); return *m_output_preds.begin(); }

2
src/muz/rel/dl_base.cpp
View file

@ -377,8 +377,6 @@ namespace datalog {
if (sig.first_functional() == 0) {
if (empty()) {
if (fact.empty())
throw default_exception("empty relations cannot be complemented");
res->add_fact(fact);
}
return res;

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

@ -1231,7 +1231,7 @@ namespace datalog {
bool populated() const { return !m_current.empty(); }
void ensure_populated() const {
if(!populated()) {
if (!populated()) {
get_fact(m_current);
}
}

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

@ -229,7 +229,7 @@ namespace datalog {
};
bitvector_table::bitvector_table(bitvector_table_plugin & plugin, const table_signature & sig)
: table_base(plugin, sig) {
: table_base(plugin, sig){
SASSERT(plugin.can_handle_signature(sig));
m_num_cols = sig.size();
@ -237,7 +237,7 @@ namespace datalog {
for (unsigned i = 0; i < m_num_cols; ++i) {
unsigned s = static_cast<unsigned>(sig[i]);
if (s != sig[i] || !is_power_of_two(s)) {
throw default_exception("bit-vector table is specialized to small domains that are powers of two");
throw default_exception("bit-vector table is specialized to small domains that are powers of two");
}
m_shift.push_back(shift);
m_mask.push_back(s - 1);
@ -253,8 +253,8 @@ namespace datalog {
if (shift >= 32) {
throw default_exception("bit-vector table is specialized to small domains that are powers of two");
}
m_bv.reserve(1 << shift);
}
m_bv.reserve(1 << shift);
}
unsigned bitvector_table::fact2offset(const table_element* f) const {
@ -274,19 +274,15 @@ namespace datalog {
}
void bitvector_table::add_fact(const table_fact & f) {
if (m_num_cols > 0) {
m_bv.set(fact2offset(f.c_ptr()));
}
m_bv.set(fact2offset(f.c_ptr()));
}
void bitvector_table::remove_fact(const table_element* fact) {
if (m_num_cols > 0) {
m_bv.unset(fact2offset(fact));
}
m_bv.unset(fact2offset(fact));
}
bool bitvector_table::contains_fact(const table_fact & f) const {
return !f.empty() && m_bv.get(fact2offset(f.c_ptr()));
return m_bv.get(fact2offset(f.c_ptr()));
}
table_base::iterator bitvector_table::begin() const {

4
src/muz/rel/dl_table.h
View file

@ -127,8 +127,8 @@ namespace datalog {
friend class bitvector_table_plugin;
class bv_iterator;
bit_vector m_bv;
unsigned m_num_cols;
bit_vector m_bv;
unsigned m_num_cols;
unsigned_vector m_shift;
unsigned_vector m_mask;

6
src/muz/transforms/dl_mk_bit_blast.cpp
View file

@ -292,14 +292,16 @@ namespace datalog {
rm.mk_rule(fml, pr, *result, r->name());
}
else {
result->add_rule(r);
result->add_rule(r);
result->inherit_output_predicate(source, r->get_decl());
}
}
// copy output predicates without any rule (bit-blasting not really needed)
const func_decl_set& decls = source.get_output_predicates();
for (func_decl* p : decls)
result->set_output_predicate(p);
if (!source.contains(p))
result->set_output_predicate(p);
if (m_context.get_model_converter()) {
generic_model_converter* fmc = alloc(generic_model_converter, m, "dl_mk_bit_blast");