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

product set local changes

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-08-29 08:36:47 -07:00
parent 965c9397b5
commit 0c6ce3a338
2 changed files with 20 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -24,19 +24,38 @@ Revision History:
namespace datalog { namespace datalog {
static unsigned s_ps_num_bits = 0;
static unsigned s_num_ps = 0;
product_set::product_set( product_set::product_set(
product_set_plugin& p, relation_signature const& s, product_set_plugin& p, relation_signature const& s,
initial_t init, T const& t): initial_t init, T const& t):
vector_relation(p, s, false, t), m_refs(0) { vector_relation(p, s, false, t), m_refs(0) {
unsigned delta = 0;
for (unsigned i = 0; i < s.size(); ++i) { for (unsigned i = 0; i < s.size(); ++i) {
unsigned sz = p.set_size(s[i]); unsigned sz = p.set_size(s[i]);
(*this)[i].resize(sz); (*this)[i].resize(sz);
if (init == FULL_t) { if (init == FULL_t) {
(*this)[i].neg(); (*this)[i].neg();
} }
delta += sz;
}
s_ps_num_bits += delta;
s_num_ps ++;
if ((s_num_ps % 1000) == 0) {
std::cout << s_num_ps << " " << s_ps_num_bits << " " << delta << "\n";
} }
} }
product_set::~product_set() {
relation_signature const& s = get_signature();
product_set_plugin& p = dynamic_cast<product_set_plugin&>(get_plugin());
for (unsigned i = 0; i < s.size(); ++i) {
unsigned sz = p.set_size(s[i]);
s_ps_num_bits -= sz;
}
--s_num_ps;
}
unsigned product_set::get_hash() const { unsigned product_set::get_hash() const {
unsigned hash = 0; unsigned hash = 0;

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

@ -46,7 +46,7 @@ namespace datalog {
}; };
product_set(product_set_plugin& p, relation_signature const& s, initial_t init, T const& t = T()); product_set(product_set_plugin& p, relation_signature const& s, initial_t init, T const& t = T());
virtual ~product_set() {} virtual ~product_set();
unsigned get_hash() const; unsigned get_hash() const;
bool operator==(product_set const& p) const; bool operator==(product_set const& p) const;
bool contains(product_set const& p) const; bool contains(product_set const& p) const;