mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 05:18:44 +00:00
debug projection
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner
commit
0d5b1637ba
|
|
@ -22,7 +22,7 @@ Revision History:
|
|||
|
||||
#include "doc.h"
|
||||
|
||||
doc_manager::doc_manager(unsigned n): m(n) {
|
||||
doc_manager::doc_manager(unsigned n): m(n), m_alloc("doc") {
|
||||
m_full = m.allocateX();
|
||||
}
|
||||
|
||||
|
|
@ -30,39 +30,43 @@ doc_manager::~doc_manager() {
|
|||
m.deallocate(m_full);
|
||||
}
|
||||
|
||||
void doc_manager::reset() {
|
||||
// m.reset(); - not until docs are in small object allocator.
|
||||
}
|
||||
doc* doc_manager::allocate() {
|
||||
return alloc(doc, m.allocate());
|
||||
return allocate(m.allocate());
|
||||
}
|
||||
doc* doc_manager::allocate1() {
|
||||
return alloc(doc, m.allocate1());
|
||||
return allocate(m.allocate1());
|
||||
}
|
||||
doc* doc_manager::allocate0() {
|
||||
return alloc(doc, m.allocate0());
|
||||
return allocate(m.allocate0());
|
||||
}
|
||||
doc* doc_manager::allocateX() {
|
||||
return alloc(doc, m.allocateX());
|
||||
return allocate(m.allocateX());
|
||||
}
|
||||
doc* doc_manager::allocate(doc const& src) {
|
||||
doc* r = alloc(doc, m.allocate(src.pos()));
|
||||
doc* r = allocate(m.allocate(src.pos()));
|
||||
for (unsigned i = 0; i < src.neg().size(); ++i) {
|
||||
r->neg().push_back(m.allocate(src.neg()[i]));
|
||||
}
|
||||
return r;
|
||||
}
|
||||
doc* doc_manager::allocate(tbv* t) {
|
||||
void* mm = m_alloc.allocate(sizeof(doc));
|
||||
return new (mm) doc(t);
|
||||
}
|
||||
doc* doc_manager::allocate(tbv const& src) {
|
||||
return allocate(m.allocate(src));
|
||||
}
|
||||
doc* doc_manager::allocate(uint64 n) {
|
||||
return alloc(doc, m.allocate(n));
|
||||
return allocate(m.allocate(n));
|
||||
}
|
||||
doc* doc_manager::allocate(rational const& r) {
|
||||
return alloc(doc, m.allocate(r));
|
||||
return allocate(m.allocate(r));
|
||||
}
|
||||
doc* doc_manager::allocate(uint64 n, unsigned hi, unsigned lo) {
|
||||
return alloc(doc, m.allocate(n, hi, lo));
|
||||
return allocate(m.allocate(n, hi, lo));
|
||||
}
|
||||
doc* doc_manager::allocate(doc const& src, unsigned const* permutation) {
|
||||
doc* r = alloc(doc, m.allocate(src.pos(), permutation));
|
||||
doc* r = allocate(m.allocate(src.pos(), permutation));
|
||||
for (unsigned i = 0; i < src.neg().size(); ++i) {
|
||||
r->neg().push_back(m.allocate(src.neg()[i], permutation));
|
||||
}
|
||||
|
|
@ -72,7 +76,8 @@ void doc_manager::deallocate(doc* src) {
|
|||
if (!src) return;
|
||||
m.deallocate(&src->pos());
|
||||
src->neg().reset(m);
|
||||
dealloc(src);
|
||||
m_alloc.deallocate(sizeof(doc), src);
|
||||
// dealloc(src);
|
||||
}
|
||||
void doc_manager::copy(doc& dst, doc const& src) {
|
||||
m.copy(dst.pos(), src.pos());
|
||||
|
|
@ -105,11 +110,31 @@ doc& doc_manager::fillX(doc& src) {
|
|||
bool doc_manager::set_and(doc& dst, doc const& src) {
|
||||
// (A \ B) & (C \ D) = (A & C) \ (B u D)
|
||||
if (!m.set_and(dst.pos(), src.pos())) return false;
|
||||
for (unsigned i = 0; i < dst.neg().size(); ++i) {
|
||||
if (!m.set_and(dst.neg()[i], dst.pos())) {
|
||||
dst.neg().erase(m, i);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
tbv_ref t(m);
|
||||
for (unsigned i = 0; i < src.neg().size(); ++i) {
|
||||
dst.neg().insert(m, m.allocate(src.neg()[i]));
|
||||
t = m.allocate(src.neg()[i]);
|
||||
if (m.set_and(*t, dst.pos())) {
|
||||
dst.neg().insert(m, t.detach());
|
||||
}
|
||||
}
|
||||
return (src.neg().is_empty() || fold_neg(dst));
|
||||
}
|
||||
|
||||
bool doc_manager::well_formed(doc const& d) const {
|
||||
if (!m.is_well_formed(d.pos())) return false;
|
||||
for (unsigned i = 0; i < d.neg().size(); ++i) {
|
||||
if (!m.is_well_formed(d.neg()[i])) return false;
|
||||
if (!m.contains(d.pos(), d.neg()[i])) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
bool doc_manager::fold_neg(doc& dst) {
|
||||
start_over:
|
||||
for (unsigned i = 0; i < dst.neg().size(); ++i) {
|
||||
|
|
@ -153,143 +178,239 @@ unsigned doc_manager::diff_by_012(tbv const& pos, tbv const& neg, unsigned& inde
|
|||
}
|
||||
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;
|
||||
|
||||
void doc_manager::set(doc& d, unsigned idx, tbit value) {
|
||||
d.pos().set(idx, value);
|
||||
for (unsigned i = 0; i < d.neg().size(); ++i) {
|
||||
d.neg()[i].set(idx, value);
|
||||
}
|
||||
NOT_IMPLEMENTED_YET();
|
||||
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])) {
|
||||
|
||||
}
|
||||
}
|
||||
|
||||
//
|
||||
// merge range from [lo:lo+length-1] with each index in equivalence class.
|
||||
// under assumption of equalities and columns that are discarded.
|
||||
//
|
||||
bool doc_manager::merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols) {
|
||||
for (unsigned i = 0; i < length; ++i) {
|
||||
unsigned idx = lo + i;
|
||||
if (!merge(d, lo + i, equalities, discard_cols)) return false;
|
||||
}
|
||||
#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;
|
||||
return true;
|
||||
}
|
||||
bool doc_manager::merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols) {
|
||||
unsigned root = equalities.find(idx);
|
||||
idx = root;
|
||||
unsigned num_x = 0;
|
||||
unsigned root1;
|
||||
tbit value = BIT_x;
|
||||
do {
|
||||
switch (d[idx]) {
|
||||
case BIT_0:
|
||||
if (value == BIT_1) return false;
|
||||
value = BIT_0;
|
||||
break;
|
||||
case BIT_1:
|
||||
if (value == BIT_0) return false;
|
||||
value = BIT_1;
|
||||
break;
|
||||
case BIT_x:
|
||||
if (!discard_cols.get(idx)) {
|
||||
++num_x;
|
||||
root1 = idx;
|
||||
}
|
||||
break;
|
||||
default:
|
||||
break;
|
||||
}
|
||||
|
||||
newneg.reset();
|
||||
I->project(delcols, new_size, newneg);
|
||||
result.m_neg.add_fact(newneg);
|
||||
skip_row: ;
|
||||
idx = equalities.next(idx);
|
||||
}
|
||||
while (idx != root);
|
||||
|
||||
if (num_x == 0) {
|
||||
// nothing to do.
|
||||
}
|
||||
else if (value != BIT_x) {
|
||||
do {
|
||||
if (d[idx] == BIT_x) {
|
||||
set(d, idx, value);
|
||||
}
|
||||
idx = equalities.next(idx);
|
||||
}
|
||||
while (idx != root);
|
||||
}
|
||||
else {
|
||||
do {
|
||||
if (!discard_cols.get(idx) && idx != root1) {
|
||||
tbv* t = tbvm().allocate(d.pos());
|
||||
t->set(idx, BIT_0);
|
||||
t->set(root1, BIT_1);
|
||||
d.neg().insert(tbvm(), t);
|
||||
t = tbvm().allocate(d.pos());
|
||||
t->set(idx, BIT_1);
|
||||
t->set(root1, BIT_0);
|
||||
d.neg().insert(tbvm(), t);
|
||||
}
|
||||
idx = equalities.next(idx);
|
||||
}
|
||||
while (idx != root);
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
//
|
||||
// 1. If n = 0,1: can project directly.
|
||||
// 2. If tbv_i uses X in all positions with vars or constant where tbv is constant: can project directly.
|
||||
// 3. Perform resolution on remaining tbv_i
|
||||
//
|
||||
// tbv & ~tbv1 & ~tbv2 & .. & ~tbv_n
|
||||
// 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.
|
||||
//
|
||||
|
||||
doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
|
||||
tbv_manager& dstt = dstm.m;
|
||||
doc* r = dstm.allocate(dstt.project(n, to_delete, src.pos()));
|
||||
|
||||
if (src.neg().is_empty()) {
|
||||
return r;
|
||||
}
|
||||
if (src.neg().size() == 1) {
|
||||
r->neg().push_back(dstt.project(n, to_delete, src.neg()[0]));
|
||||
return r;
|
||||
}
|
||||
|
||||
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));
|
||||
//
|
||||
// All negations can be projected if they are sign compatible.
|
||||
//
|
||||
tbv_ref bits(tbvm(), tbvm().allocateX());
|
||||
for (unsigned i = 0; i < src.neg().size(); ++i) {
|
||||
tbvm().set_and(*bits, src.neg()[i]);
|
||||
}
|
||||
bool can_project_const = true;
|
||||
for (unsigned i = 0; can_project_const && i < n; ++i) {
|
||||
can_project_const = !to_delete[i] || (*bits)[i] == BIT_x;
|
||||
}
|
||||
if (can_project_const) {
|
||||
for (unsigned i = 0; i < src.neg().size(); ++i) {
|
||||
r->neg().push_back(dstt.project(n, to_delete, src.neg()[i]));
|
||||
}
|
||||
return r;
|
||||
}
|
||||
|
||||
//
|
||||
// A negation can be projected directly if it does not constrain
|
||||
// deleted variables.
|
||||
//
|
||||
ptr_vector<tbv> todo;
|
||||
for (unsigned i = 0; i < src.neg().size(); ++i) {
|
||||
if (can_project_neg(src.pos(), n, to_delete, src.neg()[i])) {
|
||||
r->neg().push_back(dstt.project(n, to_delete, src.neg()[i]));
|
||||
}
|
||||
else {
|
||||
todo.push_back(tbvm().allocate(src.neg()[i]));
|
||||
}
|
||||
}
|
||||
if (todo.empty()) {
|
||||
return r;
|
||||
}
|
||||
ptr_vector<tbv> pos, neg, new_todo;
|
||||
tbv_ref t1(tbvm()), t2(tbvm());
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
if (to_delete[i] && (*bits)[i] != BIT_x) {
|
||||
TRACE("doc", tout << "delete " << i << " ";
|
||||
for (unsigned j = 0; j < todo.size(); ++j) {
|
||||
tbvm().display(tout, *todo[j]) << " ";
|
||||
}
|
||||
tout << "\n";);
|
||||
new_todo.reset();
|
||||
pos.reset();
|
||||
neg.reset();
|
||||
for (unsigned j = 0; j < todo.size(); ++j) {
|
||||
tbv& t = *todo[j];
|
||||
switch(t[i]) {
|
||||
case BIT_x: new_todo.push_back(&t); break;
|
||||
case BIT_0: neg.push_back(&t); break;
|
||||
case BIT_1: pos.push_back(&t); break;
|
||||
default: UNREACHABLE(); break;
|
||||
}
|
||||
}
|
||||
|
||||
newneg.reset();
|
||||
(*I)->project(delcols, new_size, newneg);
|
||||
result.m_neg.add_fact(newneg);
|
||||
skip_bv: ;
|
||||
if (pos.empty() || neg.empty()) {
|
||||
std::swap(new_todo, todo);
|
||||
continue;
|
||||
}
|
||||
TRACE("doc",
|
||||
tout << "pos: ";
|
||||
for (unsigned i = 0; i < pos.size(); ++i) {
|
||||
tbvm().display(tout, *pos[i]) << " ";
|
||||
}
|
||||
tout << "\nneg: ";
|
||||
for (unsigned i = 0; i < neg.size(); ++i) {
|
||||
tbvm().display(tout, *neg[i]) << " ";
|
||||
}
|
||||
tout << "\n";
|
||||
);
|
||||
|
||||
for (unsigned j = 0; j < pos.size(); ++j) {
|
||||
for (unsigned k = 0; k < neg.size(); ++k) {
|
||||
t1 = tbvm().allocate(*pos[j]);
|
||||
(*t1).set(i, BIT_x);
|
||||
if (tbvm().set_and(*t1, *neg[k])) {
|
||||
(*t1).set(i, BIT_x);
|
||||
new_todo.push_back(t1.detach());
|
||||
}
|
||||
}
|
||||
}
|
||||
for (unsigned i = 0; i < pos.size(); ++i) {
|
||||
tbvm().deallocate(pos[i]);
|
||||
}
|
||||
for (unsigned i = 0; i < neg.size(); ++i) {
|
||||
tbvm().deallocate(neg[i]);
|
||||
}
|
||||
std::swap(todo, new_todo);
|
||||
}
|
||||
}
|
||||
|
||||
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;
|
||||
for (unsigned i = 0; i < todo.size(); ++i) {
|
||||
r->neg().push_back(dstt.project(n, to_delete, *todo[i]));
|
||||
tbvm().deallocate(todo[i]);
|
||||
}
|
||||
|
||||
#endif
|
||||
return 0;
|
||||
return r;
|
||||
}
|
||||
|
||||
bool doc_manager::can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg) {
|
||||
for (unsigned i = 0; i < n; ++i) {
|
||||
if (to_delete[i] && BIT_x != neg[i] && BIT_x == pos[i]) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
||||
|
||||
void doc_manager::complement(doc const& src, ptr_vector<doc>& result) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
result.reset();
|
||||
if (is_full(src)) {
|
||||
return;
|
||||
}
|
||||
doc* r = allocateX();
|
||||
r->neg().push_back(m.allocate(src.pos()));
|
||||
result.push_back(r);
|
||||
for (unsigned i = 0; i < src.neg().size(); ++i) {
|
||||
result.push_back(allocate(src.neg()[i]));
|
||||
}
|
||||
}
|
||||
void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
doc_ref r(*this), r2(*this);
|
||||
r = allocate(A);
|
||||
if (r->neg().insert(m, m.allocate(B.pos()))) {
|
||||
result.push_back(r.detach());
|
||||
r = allocate(A);
|
||||
}
|
||||
for (unsigned i = 0; i < B.neg().size(); ++i) {
|
||||
r2 = allocate(B.neg()[i]);
|
||||
if (set_and(*r, *r2)) {
|
||||
result.push_back(r.detach());
|
||||
r = allocate(A);
|
||||
}
|
||||
}
|
||||
}
|
||||
bool doc_manager::equals(doc const& a, doc const& b) const {
|
||||
if (!m.equals(a.pos(), b.pos())) return false;
|
||||
|
|
|
|||
|
|
@ -29,20 +29,23 @@ Revision History:
|
|||
|
||||
class doc;
|
||||
template<typename M, typename T> class union_bvec;
|
||||
typedef union_find<> subset_ints;
|
||||
|
||||
class doc_manager {
|
||||
tbv_manager m;
|
||||
tbv* m_full;
|
||||
small_object_allocator m_alloc;
|
||||
public:
|
||||
doc_manager(unsigned num_bits);
|
||||
~doc_manager();
|
||||
tbv_manager& tbvm() { return m; }
|
||||
void reset();
|
||||
doc* allocate();
|
||||
doc* allocate1();
|
||||
doc* allocate0();
|
||||
doc* allocateX();
|
||||
doc* allocate(doc const& src);
|
||||
doc* allocate(tbv const& src);
|
||||
doc* allocate(tbv * src);
|
||||
doc* allocate(uint64 n);
|
||||
doc* allocate(rational const& r);
|
||||
doc* allocate(uint64 n, unsigned hi, unsigned lo);
|
||||
|
|
@ -64,12 +67,16 @@ 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);
|
||||
doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src);
|
||||
bool well_formed(doc const& d) const;
|
||||
bool merge(doc& d, unsigned lo, unsigned length, subset_ints& equalities, bit_vector const& discard_cols);
|
||||
void set(doc& d, unsigned idx, tbit value);
|
||||
private:
|
||||
unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
|
||||
bool merge(doc& d, unsigned idx, subset_ints& equalities, bit_vector const& discard_cols);
|
||||
bool can_project_neg(tbv const& pos, unsigned n, bool const* to_delete, tbv const& neg);
|
||||
};
|
||||
|
||||
typedef union_find<> subset_ints;
|
||||
|
||||
// union of tbv*, union of doc*
|
||||
template<typename M, typename T>
|
||||
|
|
@ -210,98 +217,31 @@ public:
|
|||
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) {
|
||||
unsigned k = 0;
|
||||
for (unsigned j = 0; j < size(); ++j, ++k) {
|
||||
NOT_IMPLEMENTED_YET();
|
||||
|
||||
#if 0
|
||||
T *eqBV = BV ? const_cast<T*>(BV) : &*I;
|
||||
bool discard_col = discard_cols.get(idx1+i) || (!BV && discard_cols.get(idx2+i));
|
||||
|
||||
switch (fix_single_bit(*I, idx1+i, eqBV, idx2+i, equalities, discard_col)) {
|
||||
case 1:
|
||||
// remove row
|
||||
I = m_bitvectors.erase(I);
|
||||
break;
|
||||
|
||||
case 2: {
|
||||
// don't care column equality. try subtraction first.
|
||||
union_ternary_bitvector diff(I->size()), result(I->size());
|
||||
T BV(I->size(), true);
|
||||
BV.set(idx1+i, BIT_0);
|
||||
BV.set(idx2+i, BIT_1);
|
||||
diff.add_new_fact(BV);
|
||||
|
||||
BV.set(idx1+i, BIT_1);
|
||||
BV.set(idx2+i, BIT_0);
|
||||
diff.add_new_fact(BV);
|
||||
|
||||
I->subtract(diff, result);
|
||||
*I = *result.begin();
|
||||
++I;
|
||||
break;
|
||||
}
|
||||
|
||||
default:
|
||||
if (I->is_empty()) {
|
||||
I = m_bitvectors.erase(I);
|
||||
} else {
|
||||
// bits fixed
|
||||
++I;
|
||||
}
|
||||
}
|
||||
#endif
|
||||
void merge(M& m, unsigned lo, unsigned length, subset_ints & equalities, bit_vector const& discard_cols) {
|
||||
for (unsigned i = 0; i < size(); ++i) {
|
||||
if (!m.merge(*m_elems[i], lo, length, equalities, discard_cols)) {
|
||||
erase(m, i);
|
||||
--i;
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
void merge(M& m, unsigned lo1, unsigned lo2, unsigned length, bit_vector const& discard_cols) {
|
||||
union_find_default_ctx union_ctx;
|
||||
subset_ints equalities(union_ctx);
|
||||
for (unsigned i = 0; i < discard_cols.size(); ++i) {
|
||||
equalities.mk_var();
|
||||
}
|
||||
for (unsigned j = 0; j < length; ++j) {
|
||||
equalities.merge(lo1 + j, lo2 + j);
|
||||
}
|
||||
merge(m, lo1, length, equalities, discard_cols);
|
||||
}
|
||||
|
||||
|
||||
private:
|
||||
|
||||
fix_bit_result_t fix_single_bit(tbv& bv, unsigned idx, unsigned value, const subset_ints& equalities) {
|
||||
unsigned root = equalities.find(idx);
|
||||
idx = root;
|
||||
do {
|
||||
unsigned bitval = bv.get(idx);
|
||||
if (bitval == tbv::BIT_x) {
|
||||
bv.set(idx, value);
|
||||
}
|
||||
else if (bitval != value) {
|
||||
return e_row_removed;
|
||||
}
|
||||
idx = equalities.next(idx);
|
||||
}
|
||||
while (idx != root);
|
||||
return e_fixed;
|
||||
}
|
||||
|
||||
fix_bit_result_t fix_single_bit(tbv & BV1, unsigned idx1, tbv & BV2, unsigned idx2,
|
||||
subset_ints& equalities, bool discard_col) {
|
||||
unsigned A = BV1.get(idx1);
|
||||
unsigned B = BV2.get(idx2);
|
||||
|
||||
if (A == tbv::BIT_x) {
|
||||
if (B == tbv::BIT_x) {
|
||||
// Both are don't cares.
|
||||
if (!discard_col)
|
||||
return e_duplicate_row;
|
||||
equalities.merge(idx1, idx2);
|
||||
return e_fixed;
|
||||
} else {
|
||||
// only A is don't care.
|
||||
return fix_single_bit(BV1, idx1, B, equalities);
|
||||
}
|
||||
} else if (B == tbv::BIT_x) {
|
||||
// Only B is don't care.
|
||||
return fix_single_bit(BV2, idx2, A, equalities);
|
||||
} else if (A == B) {
|
||||
return e_fixed;
|
||||
} else {
|
||||
return e_row_removed;
|
||||
}
|
||||
}
|
||||
|
||||
};
|
||||
|
||||
|
|
@ -335,7 +275,7 @@ public:
|
|||
utbv& neg() { return m_neg; }
|
||||
tbv const& pos() const { return *m_pos; }
|
||||
utbv const& neg() const { return m_neg; }
|
||||
|
||||
tbit operator[](unsigned idx) const { return pos()[idx]; }
|
||||
};
|
||||
|
||||
typedef union_bvec<doc_manager, doc> udoc;
|
||||
|
|
@ -356,6 +296,7 @@ public:
|
|||
}
|
||||
doc& operator*() { return *d; }
|
||||
doc* operator->() { return d; }
|
||||
doc* detach() { doc* r = d; d = 0; return r; }
|
||||
};
|
||||
|
||||
#endif /* _DOC_H_ */
|
||||
|
|
|
|||
|
|
@ -19,12 +19,26 @@ Revision History:
|
|||
--*/
|
||||
|
||||
#include "tbv.h"
|
||||
#include "hashtable.h"
|
||||
|
||||
|
||||
tbv_manager::~tbv_manager() {
|
||||
#if 0
|
||||
ptr_vector<tbv>::iterator it = allocated_tbvs.begin(), end = allocated_tbvs.end();
|
||||
for (; it != end; ++it) {
|
||||
std::cout << "dangling: " << (*it) << "\n";
|
||||
}
|
||||
#endif
|
||||
}
|
||||
|
||||
void tbv_manager::reset() {
|
||||
m.reset();
|
||||
}
|
||||
tbv* tbv_manager::allocate() {
|
||||
return reinterpret_cast<tbv*>(m.allocate());
|
||||
tbv* r = reinterpret_cast<tbv*>(m.allocate());
|
||||
//std::cout << allocated_tbvs.size() << " " << r << "\n";
|
||||
//allocated_tbvs.insert(r);
|
||||
return r;
|
||||
}
|
||||
tbv* tbv_manager::allocate1() {
|
||||
tbv* v = allocate();
|
||||
|
|
@ -42,7 +56,9 @@ tbv* tbv_manager::allocateX() {
|
|||
return v;
|
||||
}
|
||||
tbv* tbv_manager::allocate(tbv const& bv) {
|
||||
return reinterpret_cast<tbv*>(m.allocate(bv));
|
||||
tbv* r = allocate();
|
||||
copy(*r, bv);
|
||||
return r;
|
||||
}
|
||||
tbv* tbv_manager::allocate(uint64 val) {
|
||||
tbv* v = allocate0();
|
||||
|
|
@ -124,6 +140,13 @@ tbv* tbv_manager::allocate(rational const& r) {
|
|||
return v;
|
||||
}
|
||||
void tbv_manager::deallocate(tbv* bv) {
|
||||
#if 0
|
||||
if (!allocated_tbvs.contains(bv)) {
|
||||
std::cout << "double deallocate: " << bv << "\n";
|
||||
UNREACHABLE();
|
||||
}
|
||||
allocated_tbvs.erase(bv);
|
||||
#endif
|
||||
m.deallocate(bv);
|
||||
}
|
||||
void tbv_manager::copy(tbv& dst, tbv const& src) const {
|
||||
|
|
@ -150,8 +173,12 @@ tbv& tbv_manager::set_or(tbv& dst, tbv const& src) const {
|
|||
}
|
||||
bool tbv_manager::set_and(tbv& dst, tbv const& src) const {
|
||||
m.set_and(dst, src);
|
||||
return is_well_formed(dst);
|
||||
}
|
||||
|
||||
bool tbv_manager::is_well_formed(tbv const& dst) const {
|
||||
for (unsigned i = 0; i < num_tbits(); ++i) {
|
||||
if (dst.get(i) == BIT_z) return false;
|
||||
if (dst[i] == BIT_z) return false;
|
||||
}
|
||||
return true;
|
||||
}
|
||||
|
|
|
|||
|
|
@ -40,8 +40,10 @@ inline tbit neg(tbit t) {
|
|||
class tbv_manager {
|
||||
friend class tbv;
|
||||
fixed_bit_vector_manager m;
|
||||
// ptr_vector<tbv> allocated_tbvs;
|
||||
public:
|
||||
tbv_manager(unsigned n): m(2*n) {}
|
||||
~tbv_manager();
|
||||
void reset();
|
||||
tbv* allocate();
|
||||
tbv* allocate1();
|
||||
|
|
@ -70,6 +72,7 @@ public:
|
|||
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);
|
||||
bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
|
||||
};
|
||||
|
||||
class tbv: private fixed_bit_vector {
|
||||
|
|
@ -130,6 +133,7 @@ public:
|
|||
}
|
||||
tbv& operator*() { return *d; }
|
||||
tbv* get() { return d; }
|
||||
tbv* detach() { tbv* result = d; d = 0; return result; }
|
||||
};
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -461,14 +461,18 @@ namespace datalog {
|
|||
for (unsigned i = 0, e = m_empty_bv.size(); i < e; ++i) {
|
||||
m_equalities.mk_var();
|
||||
}
|
||||
for (unsigned i = 1; i < col_cnt; ++i) {
|
||||
for (unsigned j = 0; j < m_size; ++j) {
|
||||
m_equalities.merge(m_cols[0]+j ,m_cols[i]+j);
|
||||
}
|
||||
}
|
||||
}
|
||||
|
||||
virtual void operator()(relation_base & _r) {
|
||||
udoc_relation& r = get(_r);
|
||||
udoc& d = r.get_udoc();
|
||||
for (unsigned i = 1; i < m_cols.size(); ++i) {
|
||||
d.fix_eq_bits(m_cols[0], 0, m_cols[i], m_size, m_equalities, m_empty_bv);
|
||||
}
|
||||
doc_manager& dm = r.get_dm();
|
||||
d.merge(dm, m_cols[0], m_size, m_equalities, m_empty_bv);
|
||||
TRACE("dl", tout << "final size: " << r.get_size_estimate_rows() << '\n';);
|
||||
}
|
||||
};
|
||||
|
|
@ -624,10 +628,10 @@ namespace datalog {
|
|||
SASSERT(m.is_bool(g));
|
||||
unsigned v = to_var(g)->get_idx();
|
||||
unsigned idx = column_idx(v);
|
||||
doc_manager& dm1 = get_plugin().dm(1);
|
||||
tbv_ref bit1(dm1.tbvm());
|
||||
bit1 = dm1.tbvm().allocate1();
|
||||
result.fix_eq_bits(idx, bit1.get(), 0, 1, equalities, discard_cols);
|
||||
doc_ref d(dm);
|
||||
d = dm.allocateX();
|
||||
dm.set(*d, idx, BIT_1);
|
||||
result.intersect(dm, *d);
|
||||
}
|
||||
else if (m.is_eq(g, e1, e2) && bv.is_bv(e1)) {
|
||||
unsigned hi, lo;
|
||||
|
|
@ -650,7 +654,7 @@ namespace datalog {
|
|||
unsigned idx1 = column_idx(v1->get_idx());
|
||||
unsigned idx2 = column_idx(v2->get_idx());
|
||||
unsigned length = column_num_bits(v1->get_idx());
|
||||
result.fix_eq_bits(idx1, 0, idx2, length, equalities, discard_cols);
|
||||
result.merge(dm, idx1, idx2, length, discard_cols);
|
||||
}
|
||||
else {
|
||||
goto failure_case;
|
||||
|
|
|
|||
136
src/test/doc.cpp
136
src/test/doc.cpp
|
|
@ -9,14 +9,13 @@
|
|||
#include "model_smt2_pp.h"
|
||||
#include "smt_params.h"
|
||||
#include "ast_util.h"
|
||||
#include "expr_safe_replace.h"
|
||||
#include "th_rewriter.h"
|
||||
|
||||
|
||||
static void tst_doc1(unsigned n) {
|
||||
doc_manager m(n);
|
||||
|
||||
m.allocate();
|
||||
m.reset();
|
||||
|
||||
doc_ref d(m, m.allocate());
|
||||
doc_ref d1(m, m.allocate1());
|
||||
doc_ref d0(m, m.allocate0());
|
||||
|
|
@ -74,17 +73,25 @@ static void tst_doc1(unsigned n) {
|
|||
m.display(std::cout, *d1) << "\n";
|
||||
|
||||
|
||||
#if 0
|
||||
svector<bool> to_delete(n, false);
|
||||
to_delete[1] = true;
|
||||
to_delete[3] = true;
|
||||
doc_manager m1(n-2);
|
||||
doc_ref d1_1(m1, m1.project(n, to_delete.c_ptr(), *d0));
|
||||
doc_ref d1_1(m1, m.project(m1, n, to_delete.c_ptr(), *d1));
|
||||
doc_ref d1_2(m1, m1.allocate1());
|
||||
m.display(std::cout, *d1) << " -> ";
|
||||
m1.display(std::cout, *d1_1) << "\n";
|
||||
SASSERT(m1.equals(*d1_1,*d1_2));
|
||||
#endif
|
||||
m.set(*d1,2,BIT_x);
|
||||
m.set(*d1,4,BIT_x);
|
||||
d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
|
||||
m.display(std::cout, *d1) << " -> ";
|
||||
m1.display(std::cout, *d1_1) << "\n";
|
||||
d1->neg().push_back(m.tbvm().allocate1());
|
||||
SASSERT(m.well_formed(*d1));
|
||||
d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
|
||||
m.display(std::cout, *d1) << " -> ";
|
||||
m1.display(std::cout, *d1_1) << "\n";
|
||||
}
|
||||
|
||||
|
||||
|
|
@ -106,48 +113,113 @@ class test_doc_project {
|
|||
default : return BIT_x;
|
||||
}
|
||||
}
|
||||
void mk_clause(expr_ref& result, tbv& t) {
|
||||
expr_ref_vector clause(m);
|
||||
expr_ref mk_conj(tbv& t) {
|
||||
expr_ref result(m);
|
||||
expr_ref_vector conjs(m);
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
tbit b = choose_tbit();
|
||||
t.set(i, b);
|
||||
switch (b) {
|
||||
case BIT_0: clause.push_back(m.mk_not(m_vars[i].get())); break;
|
||||
case BIT_1: clause.push_back(m_vars[i].get()); break;
|
||||
case BIT_1: conjs.push_back(m_vars[i].get()); break;
|
||||
case BIT_0: conjs.push_back(m.mk_not(m_vars[i].get())); break;
|
||||
default: break;
|
||||
}
|
||||
}
|
||||
result = mk_or(m, clause.size(), clause.c_ptr());
|
||||
result = mk_and(m, conjs.size(), conjs.c_ptr());
|
||||
return result;
|
||||
}
|
||||
|
||||
expr_ref to_formula(tbv const& t, doc_manager& m2, bool const* to_delete) {
|
||||
expr_ref result(m);
|
||||
expr_ref_vector conjs(m);
|
||||
unsigned n = m2.num_tbits();
|
||||
tbv_manager& tm = m2.tbvm();
|
||||
for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
|
||||
if (!to_delete[i]) {
|
||||
switch (t[j]) {
|
||||
case BIT_x:
|
||||
break;
|
||||
case BIT_1:
|
||||
conjs.push_back(m_vars[i].get());
|
||||
break;
|
||||
case BIT_0:
|
||||
conjs.push_back(m.mk_not(m_vars[i].get()));
|
||||
break;
|
||||
default:
|
||||
UNREACHABLE();
|
||||
break;
|
||||
}
|
||||
++j;
|
||||
}
|
||||
}
|
||||
result = mk_and(m, conjs.size(), conjs.c_ptr());
|
||||
return result;
|
||||
}
|
||||
|
||||
expr_ref to_formula(doc const& d, doc_manager& m2, bool const* to_delete) {
|
||||
expr_ref result(m);
|
||||
expr_ref_vector conjs(m);
|
||||
conjs.push_back(to_formula(d.pos(), m2, to_delete));
|
||||
for (unsigned i = 0; i < d.neg().size(); ++i) {
|
||||
conjs.push_back(m.mk_not(to_formula(d.neg()[i], m2, to_delete)));
|
||||
}
|
||||
result = mk_and(m, conjs.size(), conjs.c_ptr());
|
||||
return result;
|
||||
}
|
||||
|
||||
void project(doc const& d, doc_manager& m2, bool const* to_delete, doc_ref& result) {
|
||||
result = dm.project(m2, m_vars.size(), to_delete, d);
|
||||
TRACE("doc",
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
tout << (to_delete[i]?"0":"1");
|
||||
}
|
||||
tout << " ";
|
||||
dm.display(tout, d) << " -> ";
|
||||
m2.display(tout, *result) << "\n";
|
||||
);
|
||||
}
|
||||
|
||||
void test_clauses(unsigned num_clauses) {
|
||||
doc_ref d(dm, dm.allocateX());
|
||||
expr_ref_vector fmls(m);
|
||||
expr_ref fml(m);
|
||||
th_rewriter rw(m);
|
||||
expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m);
|
||||
for (unsigned i = 0; i < num_clauses; ++i) {
|
||||
expr_ref clause(m);
|
||||
tbv* t = dm.tbvm().allocate();
|
||||
mk_clause(clause, *t);
|
||||
fmls.push_back(m.mk_not(mk_conj(*t)));
|
||||
d->neg().push_back(t);
|
||||
fmls.push_back(clause);
|
||||
}
|
||||
fml = mk_and(m, fmls.size(), fmls.c_ptr());
|
||||
dm.display(std::cout, *d) << "\n";
|
||||
std::cout << fml << "\n";
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
//test_project(i, fml, *d);
|
||||
}
|
||||
}
|
||||
|
||||
void test_project(unsigned i, expr* fml, doc& d) {
|
||||
fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
|
||||
svector<bool> to_delete(m_vars.size(), false);
|
||||
to_delete[i] = true;
|
||||
doc_manager dm1(m_vars.size()-1);
|
||||
doc_ref d1(dm1, dm1.project(m_vars.size(), to_delete.c_ptr(), d));
|
||||
expr_ref fml1(m);
|
||||
// fml1 = m.mk_exists();
|
||||
// extrac formula fml2 from d1,
|
||||
// check that fml1 is equivalent to fml2
|
||||
unsigned num_bits = 1;
|
||||
for (unsigned i = 1; i < to_delete.size(); ++i) {
|
||||
to_delete[i] = (m_ran(2) == 0);
|
||||
if (!to_delete[i]) ++num_bits;
|
||||
}
|
||||
doc_manager m2(num_bits);
|
||||
doc_ref result(m2);
|
||||
project(*d, m2, to_delete.c_ptr(), result);
|
||||
fml2 = to_formula(*result, m2, to_delete.c_ptr());
|
||||
rw(fml2);
|
||||
|
||||
for (unsigned i = 0; i < m_vars.size(); ++i) {
|
||||
if (to_delete[i]) {
|
||||
expr_safe_replace rep1(m), rep2(m);
|
||||
rep1.insert(m_vars[i].get(), m.mk_true());
|
||||
rep1(fml1, tmp1);
|
||||
rep2.insert(m_vars[i].get(), m.mk_false());
|
||||
rep2(fml1, tmp2);
|
||||
fml1 = m.mk_or(tmp1, tmp2);
|
||||
}
|
||||
}
|
||||
rw(fml1);
|
||||
smt_params fp;
|
||||
smt::kernel solver(m, fp);
|
||||
TRACE("doc", tout << "manual project:\n" << fml1 << "\nautomatic project: \n" << fml2 << "\n";);
|
||||
fml = m.mk_not(m.mk_eq(fml1, fml2));
|
||||
solver.assert_expr(fml);
|
||||
lbool res = solver.check();
|
||||
SASSERT(res == l_false);
|
||||
}
|
||||
|
||||
public:
|
||||
|
|
@ -171,5 +243,5 @@ void tst_doc() {
|
|||
tst_doc1(70);
|
||||
|
||||
test_doc_project tp(4);
|
||||
tp(5,7);
|
||||
tp(200,7);
|
||||
}
|
||||
|
|
|
|||
|
|
@ -24,6 +24,16 @@ static void tst1(unsigned num_bits) {
|
|||
VERIFY(m.intersect(*bX,*b0,*bN));
|
||||
SASSERT(m.equals(*b0, *bN));
|
||||
VERIFY(!m.intersect(*b0,*b1,*bN));
|
||||
m.fill1(*b1);
|
||||
svector<bool> to_delete(num_bits, false);
|
||||
tbv_manager m2(num_bits-2);
|
||||
to_delete[1] = true;
|
||||
to_delete[3] = true;
|
||||
(*b1).set(2, BIT_0);
|
||||
(*b1).set(4, BIT_x);
|
||||
tbv_ref b2(m2, m2.project(num_bits, to_delete.c_ptr(), *b1));
|
||||
m.display(std::cout, *b1) << " -> ";
|
||||
m2.display(std::cout, *b2) << "\n";
|
||||
m.deallocate(b0);
|
||||
m.deallocate(b1);
|
||||
m.deallocate(bX);
|
||||
|
|
|
|||
Loading…
Reference in a new issue