mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

doc

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-18 03:53:14 -07:00
parent 4c3605421c
commit 4eadaabe64
5 changed files with 229 additions and 19 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

174
src/muz/ddnf/doc.cpp
View file

@ -66,6 +66,180 @@ doc& doc_manager::fillX(doc& src) const {
bool doc_manager::set_and(doc& dst, doc const& src) const {
return false;
}
bool doc_manager::fold_neg(doc& dst) {
start_over:
for (unsigned i = 0; i < dst.neg().size(); ++i) {
unsigned index;
unsigned count = diff_by_012(dst.pos(), dst.neg()[i], index);
if (count != 2) {
if (count == 0) {
return false;
}
else if (count == 3) {
dst.neg().erase(tbvm(), i);
--i;
}
else { // count == 1:
dst.pos().set(index, neg(dst.neg()[i][index]));
dst.neg().erase(tbvm(), i);
goto start_over;
}
}
}
return true;
}
unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& index) {
unsigned n = num_tbits();
unsigned count = 0;
for (unsigned i = 0; i < n; ++i) {
tbit b1 = pos[i];
tbit b2 = neg[i];
SASSERT(b1 != BIT_z && b2 != BIT_z);
if (b1 != b2) {
if (count == 1) return 2;
if (b1 == BIT_x) {
index = i;
count = 1;
}
else if (b2 != BIT_x) {
return 3;
}
}
}
return count;
}
doc* doc_manager::project(unsigned n, bool const* to_delete, doc const& src) {
tbv* p = tbvm().project(n, to_delete, src.pos());
if (src.neg().is_empty()) {
// build doc from p.
return 0;
}
ptr_vector<tbv> todo;
#if 0
// tbv & ~tbv1 & ~tbv2 & ..
// Semantics of ~tbv1 is that it is a clause of literals.
// indices where BIT_1 is set are negative.
// indices where BIT_0 is set are positive.
// The first loop is supposed to project tbv_i directly
// when some safety condition is met.
// The second loop handles the remaining tbv_i that
// don't meet the safety condition.
for (unsigned i = 0; i < src.neg().size(); ++i) {
if (can_project_neg(n, to_delete, src.neg()[i])) {
}
}
#endif
#if 0
// REVIEW: what is the spec for this code?
ternary_diff_bitvector TBV(*this);
if (!TBV.fold_neg())
return false;
std::set<ternary_bitvector*> todo;
cpy_bits_t cpy_bits;
ternary_bitvector newneg;
for (union_ternary_bitvector<ternary_bitvector>::iterator I = TBV.m_neg.begin(),
E = TBV.m_neg.end(); I != E; ++I) {
// check if subtract TBV should be skiped
for (unsigned i = 0; i < delcols.size()-1; ++i) {
unsigned idx = delcols[i];
if (I->get(idx) != TBV.m_pos.get(idx)) { // xx \ 1x
if (analyze_copy_bit(TBV.m_pos, *I, delcols, cpy_bits))
todo.insert(&*I);
goto skip_row;
}
}
newneg.reset();
I->project(delcols, new_size, newneg);
result.m_neg.add_fact(newneg);
skip_row: ;
}
if (!todo.empty()) {
for (std::set<ternary_bitvector*>::iterator I = todo.begin(),
E = todo.end(); I != E; ++I) {
for (unsigned i = 0; i < delcols.size()-1; ++i) {
unsigned idx = delcols[i];
if ((*I)->get(idx) != TBV.m_pos.get(idx)) {
cpy_bits_t::iterator II = cpy_bits.find(idx);
if (II == cpy_bits.end())
goto skip_bv;
unsigned idx_keep = II->second.first;
unsigned cpy_val = II->second.second;
if (!((*I)->get(idx) & cpy_val) || (*I)->get(idx_keep) != BIT_x)
goto skip_bv;
(*I)->set(idx_keep, (*I)->get(idx));
}
}
newneg.reset();
(*I)->project(delcols, new_size, newneg);
result.m_neg.add_fact(newneg);
skip_bv: ;
}
}
return !result.is_empty();
// idx_del -> <idx_keep, val>
// val -> BIT_*
typedef std::map<unsigned, std::pair<unsigned, unsigned char> > cpy_bits_t;
static bool analyze_copy_bit(const ternary_bitvector& pos, const ternary_bitvector& neg,
const unsigned_vector& delcols, cpy_bits_t& cpy_bits) {
unsigned *del = delcols.c_ptr();
bool got_del_col = false, got_keep_col = false;
unsigned del_col = 0, keep_col = 0;
for (unsigned i = 0; i < pos.size(); ++i) {
if (pos.get(i) != neg.get(i)) {
if (*del == i) {
if (got_del_col)
return true;
del_col = i;
got_del_col = true;
} else {
if (got_keep_col)
return true;
keep_col = i;
got_keep_col = true;
}
}
if (i == *del)
++del;
}
if (!got_del_col || !got_keep_col)
return true;
if (neg.get(keep_col) == neg.get(del_col))
return false;
unsigned char val = neg.get(del_col);
cpy_bits_t::iterator I = cpy_bits.find(del_col);
if (I == cpy_bits.end())
cpy_bits[del_col] = std::make_pair(keep_col, val);
else {
// FIXME: eq classes with size > 1 not supported for now
SASSERT(I->second.first == keep_col);
I->second.second |= val;
}
return false;
}
#endif
return 0;
}
void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
}
void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {

17
src/muz/ddnf/doc.h
View file

@ -34,7 +34,7 @@ class doc_manager {
tbv_manager m;
public:
doc_manager(unsigned n): m(n) {}
tbv_manager& tbv() { return m; }
tbv_manager& tbvm() { return m; }
void reset();
doc* allocate();
doc* allocate1();
@ -53,6 +53,7 @@ public:
doc& fillX(doc& src) const;
bool is_full(doc const& src) const;
bool set_and(doc& dst, doc const& src) const;
bool fold_neg(doc& dst);
bool intersect(doc const& A, doc const& B, doc& result) const;
void complement(doc const& src, ptr_vector<doc>& result);
void subtract(doc const& A, doc const& B, ptr_vector<doc>& result);
@ -61,6 +62,9 @@ public:
bool contains(doc const& a, doc const& b) const;
std::ostream& display(std::ostream& out, doc const& b) const;
unsigned num_tbits() const { return m.num_tbits(); }
doc* project(unsigned n, bool const* to_delete, doc const& src);
private:
unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
};
typedef union_find<> subset_ints;
@ -99,6 +103,11 @@ public:
void push_back(T* t) {
m_elems.push_back(t);
}
void erase(M& m, unsigned idx) {
T* t = m_elems[idx];
m_elems.erase(t);
m.deallocate(t);
}
void reset(M& m) {
for (unsigned i = 0; i < m_elems.size(); ++i) {
m.deallocate(m_elems[i]);
@ -193,6 +202,12 @@ public:
negated.reset(m);
}
}
void copy(M& m, union_bvec const& other) {
reset(m);
for (unsigned i = 0; i < other.size(); ++i) {
push_back(m.allocate(other[i]));
}
}
void fix_eq_bits(unsigned idx1, tbv* BV, unsigned idx2, unsigned length,
subset_ints& equalities, const bit_vector& discard_cols) {
for (unsigned i = 0; i < length; ++i) {

17
src/muz/ddnf/tbv.cpp
View file

@ -66,10 +66,23 @@ tbv* tbv_manager::allocate(uint64 val, unsigned hi, unsigned lo) {
tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
tbv* r = allocate();
for (unsigned i = 0; i < num_tbits(); ++i) {
r->set(permutation[i], bv.get(i));
r->set(permutation[i], bv[i]);
}
return r;
}
tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
tbv* r = allocate();
unsigned i, j;
for (i = 0, j = 0; i < n; ++i) {
if (!to_delete[i]) {
r->set(j, src[i]);
++j;
}
}
SASSERT(num_tbits() == j);
return r;
}
void tbv::set(uint64 val, unsigned hi, unsigned lo) {
for (unsigned i = 0; i < hi - lo + 1; ++i) {
set(lo + i, (val & (1ULL << i))?BIT_1:BIT_0);
@ -90,7 +103,7 @@ void tbv::set(rational const& r, unsigned hi, unsigned lo) {
void tbv::set(tbv const& other, unsigned hi, unsigned lo) {
for (unsigned i = 0; i < hi - lo + 1; ++i) {
set(lo + i, other.get(i));
set(lo + i, other[i]);
}
}

20
src/muz/ddnf/tbv.h
View file

@ -26,10 +26,16 @@ Revision History:
class tbv;
#define BIT_0 0x1
#define BIT_1 0x2
#define BIT_x 0x3
#define BIT_z 0x0
enum tbit {
BIT_z = 0x0,
BIT_0 = 0x1,
BIT_1 = 0x2,
BIT_x = 0x3
};
inline tbit neg(tbit t) {
return (tbit)(t ^ 0x3);
}
class tbv_manager {
friend class tbv;
@ -63,6 +69,7 @@ public:
bool contains(tbv const& a, tbv const& b) const;
bool intersect(tbv const& a, tbv const& b, tbv& result);
std::ostream& display(std::ostream& out, tbv const& b) const;
tbv* project(unsigned n, bool const* to_delete, tbv const& src);
};
class tbv: private fixed_bit_vector {
@ -91,13 +98,14 @@ public:
void set(rational const& r, unsigned hi, unsigned lo);
void set(tbv const& other, unsigned hi, unsigned lo);
unsigned operator[](unsigned idx) const { return get(idx); }
void set(unsigned index, unsigned value) {
tbit operator[](unsigned idx) const { return (tbit)get(idx); }
void set(unsigned index, tbit value) {
SASSERT(value <= 3);
fixed_bit_vector::set(2*index, (value & 2) != 0);
fixed_bit_vector::set(2*index+1, (value & 1) != 0);
}
private:
unsigned get(unsigned index) const {

20
src/muz/ddnf/udoc_relation.cpp
View file

@ -271,8 +271,8 @@ namespace datalog {
for (unsigned i = 0; i < m_cols1.size(); ++i) {
unsigned idx1 = m_cols1[i];
unsigned idx2 = mid + m_cols2[i];
unsigned v1 = pos[idx1];
unsigned v2 = pos[idx2];
tbit v1 = pos[idx1];
tbit v2 = pos[idx2];
if (v1 == BIT_x) {
if (v2 != BIT_x)
@ -294,12 +294,12 @@ namespace datalog {
if (v1 == BIT_x && v2 == BIT_x) {
// add to subtracted TBVs: 1xx0 and 0xx1
tbv* r = dm.tbv().allocate(pos);
tbv* r = dm.tbvm().allocate(pos);
r->set(idx1, BIT_0);
r->set(idx2, BIT_1);
neg.push_back(r);
r = dm.tbv().allocate(pos);
r = dm.tbvm().allocate(pos);
r->set(idx1, BIT_1);
r->set(idx2, BIT_0);
neg.push_back(r);
@ -308,13 +308,13 @@ namespace datalog {
// handle subtracted TBVs: 1010 -> 1010xxx
for (unsigned i = 0; i < d1.neg().size(); ++i) {
tbv* t = dm.tbv().allocate();
tbv* t = dm.tbvm().allocate();
t->set(d1.neg()[i], mid-1, 0);
t->set(d2.pos(), hi - 1, mid);
neg.push_back(t);
}
for (unsigned i = 0; i < d2.neg().size(); ++i) {
tbv* t = dm.tbv().allocate();
tbv* t = dm.tbvm().allocate();
t->set(d1.pos(), mid-1, 0);
t->set(d2.neg()[i], hi - 1, mid);
neg.push_back(t);
@ -625,8 +625,8 @@ namespace datalog {
unsigned v = to_var(g)->get_idx();
unsigned idx = column_idx(v);
doc_manager& dm1 = get_plugin().dm(1);
tbv_ref bit1(dm1.tbv());
bit1 = dm1.tbv().allocate1();
tbv_ref bit1(dm1.tbvm());
bit1 = dm1.tbvm().allocate1();
result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols);
}
else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
@ -792,9 +792,9 @@ namespace datalog {
virtual relation_base* operator()(const relation_base & tb) {
udoc_relation const & t = get(tb);
udoc const& u1 = t.get_udoc();
doc_manager& dm = t.get_dm();
udoc u2;
// copy u1 -> u2;
NOT_IMPLEMENTED_YET();
u2.copy(dm, u1);
u2.intersect(dm, m_udoc);
if (m_condition && !u2.is_empty()) {
t.apply_guard(m_condition, u2, m_col_list);