mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

expanding product_set

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-27 14:32:31 -07:00
parent 9e7cef7d6b
commit 965c9397b5
3 changed files with 46 additions and 23 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -89,8 +89,7 @@ namespace datalog {
void relation_base::reset() {
ast_manager & m = get_plugin().get_ast_manager();
app_ref bottom_ref(m.mk_false(), m);
scoped_ptr<relation_mutator_fn> reset_fn =
get_manager().mk_filter_interpreted_fn(static_cast<relation_base &>(*this), bottom_ref);
scoped_ptr<relation_mutator_fn> reset_fn = get_manager().mk_filter_interpreted_fn(*this, bottom_ref);
if(!reset_fn) {
NOT_IMPLEMENTED_YET();
}

63
src/muz/rel/product_set.cpp
View file

@ -52,27 +52,40 @@ namespace datalog {
}
return true;
}
bool product_set::contains(product_set const& p) const {
for (unsigned i = 0; i < get_signature().size(); ++i) {
if ((*this)[i].contains(p[i])) return false;
}
return true;
}
void product_set::reset() {
for (unsigned i = 0; i < get_signature().size(); ++i) {
(*this)[i].fill0();
}
}
void product_set::add_fact(const relation_fact & f) {
UNREACHABLE();
}
bool product_set::contains_fact(const relation_fact & f) const {
UNREACHABLE();
return false;
}
relation_base * product_set::clone() const {
UNREACHABLE();
return 0;
product_set* result = alloc(product_set, dynamic_cast<product_set_plugin&>(get_plugin()), get_signature(), EMPTY_t);
result->copy(*this);
return result;
}
relation_base * product_set::complement(func_decl*) const {
UNREACHABLE();
return 0;
product_set* result = alloc(product_set, dynamic_cast<product_set_plugin&>(get_plugin()), get_signature(), EMPTY_t);
result->copy(*this);
result->complement();
return result;
}
void product_set::complement() {
for (unsigned i = 0; i < get_signature().size(); ++i) {
(*this)[i].neg();
}
}
void product_set::to_formula(expr_ref& fml) const {
ast_manager& m = fml.get_manager();
@ -133,10 +146,7 @@ namespace datalog {
}
product_set_relation::~product_set_relation() {
product_sets::iterator it = m_elems.begin(), end = m_elems.end();
for (; it != end; ++it) {
(*it)->dec_ref();
}
reset();
}
class product_set_plugin::filter_interpreted_fn : public relation_mutator_fn {
@ -150,7 +160,8 @@ namespace datalog {
virtual void operator()(relation_base & _r) {
ast_manager& m = m_condition.get_manager();
if (m.is_false(m_condition)) {
_r.reset();
product_set_relation & r = get(_r);
r.reset();
return;
}
if (m.is_true(m_condition)) {
@ -172,7 +183,6 @@ namespace datalog {
for (unsigned i = 0; i < f.size(); ++i) {
VERIFY(bv.is_numeral(f[i], v, bv_size));
SASSERT(v.is_unsigned());
(*s)[i] = bit_vector(get_plugin().set_size(m.get_sort(f[i])));
(*s)[i].set(v.get_unsigned(), true);
}
// s->display(std::cout << "fact");
@ -194,12 +204,19 @@ namespace datalog {
product_set_relation* r = alloc(product_set_relation, get_plugin(), get_signature());
product_sets::iterator it = m_elems.begin(), end = m_elems.end();
for (; it != end; ++it) {
// TBD: have to copy because other operations are destructive.
(*it)->inc_ref();
r->m_elems.insert(*it);
product_set* ps = dynamic_cast<product_set*>((*it)->clone());
ps->inc_ref();
r->m_elems.insert(ps);
}
return r;
}
void product_set_relation::reset() {
product_sets::iterator it = m_elems.begin(), end = m_elems.end();
for (; it != end; ++it) {
(*it)->dec_ref();
}
m_elems.reset();
}
product_set_relation * product_set_relation::complement(func_decl*) const {
std::cout << "complement\n";
NOT_IMPLEMENTED_YET();
@ -264,9 +281,11 @@ namespace datalog {
product_set* product_set_plugin::insert(product_set* s, product_set_relation* r) {
if (s->empty()) {
s->reset();
s->complement();
}
else if (r->m_elems.contains(s)) {
s->reset();
s->complement();
}
else {
s->inc_ref();
@ -309,6 +328,7 @@ namespace datalog {
}
}
dealloc(s);
std::cout << "join " << result->m_elems.size() << "\n";
return result;
}
};
@ -397,6 +417,7 @@ namespace datalog {
product_set_relation const& src = get(_src);
product_set_relation* d = get(_delta);
r.get_plugin().mk_union(r, src, d);
std::cout << "union: " << r.m_elems.size() << "\n";
}
};
void product_set_plugin::mk_union(
@ -540,8 +561,7 @@ namespace datalog {
}
};
product_set_plugin::decomp_t product_set_plugin::decompose(
expr* condition, expr_ref_vector& args, unsigned& col) {
product_set_plugin::decomp_t product_set_plugin::decompose(expr* condition, expr_ref_vector& args, unsigned& col) {
args.reset();
expr* e1, *e2;
app* value;
@ -575,6 +595,7 @@ namespace datalog {
return AND_d;
}
if (is_setof(condition, args, col)) {
SASSERT(!args.empty());
return SET_d;
}
if (m.is_or(condition)) {
@ -636,7 +657,6 @@ namespace datalog {
unsigned col;
ptr_vector<relation_mutator_fn> mutators;
expr_ref_vector args(m);
std::cout << mk_pp(condition, m) << "\n";
bit_vector mask;
switch (decompose(condition, args, col)) {
case NE_d:
@ -713,6 +733,9 @@ namespace datalog {
values.push_back(value);
}
}
else {
return false;
}
}
return true;
}
@ -722,9 +745,7 @@ namespace datalog {
rational val;
unsigned bv_size;
if (!m.is_eq(e, e1, e2)) return false;
if (!is_var(e1)) {
std::swap(e1, e2);
}
if (!is_var(e1)) std::swap(e1, e2);
if (!is_var(e1)) return false;
if (!bv.is_numeral(e2, val, bv_size)) return false;
if (!val.is_unsigned()) return false;

3
src/muz/rel/product_set.h
View file

@ -71,9 +71,11 @@ namespace datalog {
virtual bool contains_fact(const relation_fact & f) const;
virtual relation_base * clone() const;
virtual relation_base * complement(func_decl*) const;
virtual void reset();
virtual void to_formula(expr_ref& fml) const;
bool mk_intersect(unsigned idx, T const& t);
void complement();
private:
virtual void display_index(unsigned i, const T&, std::ostream& out) const;
@ -132,6 +134,7 @@ namespace datalog {
public:
product_set_relation(product_set_plugin& p, relation_signature const& s);
virtual ~product_set_relation();
virtual void reset();
virtual void add_fact(const relation_fact & f);
virtual bool contains_fact(const relation_fact & f) const;
virtual product_set_relation * clone() const;