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

Merge branch 'opt' of https://git01.codeplex.com/z3 into opt

Browse source
This commit is contained in:
Nikolaj Bjorner 2014-10-01 13:49:36 -07:00
commit 985e48c66a
19 changed files with 295 additions and 183 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -307,7 +307,7 @@ namespace datalog {
idx_vector::const_iterator end=m_controls.end();
for(; it != end; ++it) {
reg_idx r = *it;
if (ctx.reg(r) && !ctx.reg(r)->empty()) {
if (ctx.reg(r) && !ctx.reg(r)->fast_empty()) {
return false;
}
}

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

@ -122,7 +122,7 @@ namespace datalog {
relation_map::iterator it = m_relations.begin();
relation_map::iterator end = m_relations.end();
for(; it!=end; ++it) {
if(!it->m_value->empty()) {
if(!it->m_value->fast_empty()) {
res.insert(it->m_key);
}
}

88
src/muz/rel/doc.cpp
View file

@ -83,7 +83,6 @@ void doc_manager::deallocate(doc* src) {
m.deallocate(&src->pos());
src->neg().reset(m);
m_alloc.deallocate(sizeof(doc), src);
// dealloc(src);
}
void doc_manager::copy(doc& dst, doc const& src) {
m.copy(dst.pos(), src.pos());
@ -110,23 +109,21 @@ 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;
dst.neg().intersect(m, dst.pos());
dst.neg().intersect(m, dst.pos());
tbv_ref t(m);
for (unsigned i = 0; i < src.neg().size(); ++i) {
t = m.allocate(src.neg()[i]);
if (m.set_and(*t, dst.pos())) {
if (m.equals(*t, dst.pos())) return false;
dst.neg().insert(m, t.detach());
}
}
SASSERT(well_formed(dst));
return fold_neg(dst);
}
bool doc_manager::set_and(doc& dst, tbv const& src) {
// (A \ B) & C = (A & C) \ B
// (A \ B) & C = (A & C) \ (B & C)
if (!m.set_and(dst.pos(), src)) return false;
dst.neg().intersect(m, src);
return true;
return fold_neg(dst);
}
bool doc_manager::well_formed(doc const& d) const {
@ -141,6 +138,9 @@ bool doc_manager::well_formed(doc const& d) const {
bool doc_manager::fold_neg(doc& dst) {
start_over:
for (unsigned i = 0; i < dst.neg().size(); ++i) {
if (m.contains(dst.neg()[i], dst.pos()))
return false;
unsigned index;
unsigned count = diff_by_012(dst.pos(), dst.neg()[i], index);
if (count != 2) {
@ -280,7 +280,7 @@ bool doc_manager::intersect(doc const& A, doc const& B, doc& result) {
// indices where BIT_0 is set are positive.
//
doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src) {
doc* doc_manager::project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src) {
tbv_manager& dstt = dstm.m;
tbv_ref t(dstt);
t = dstt.project(n, to_delete, src.pos());
@ -391,7 +391,7 @@ doc* doc_manager::project(doc_manager& dstm, unsigned n, bool const* to_delete,
doc_manager::project_action_t
doc_manager::pick_resolvent(
tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx) {
tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx) {
if (neg.empty()) return project_done;
for (unsigned j = 0; j < neg.size(); ++j) {
if (m.equals(pos, *neg[j])) return project_is_empty;
@ -401,7 +401,7 @@ doc_manager::pick_resolvent(
unsigned best_neg = UINT_MAX;
unsigned best_idx = UINT_MAX;
for (unsigned i = 0; i < num_tbits(); ++i) {
if (!to_delete[i]) continue;
if (!to_delete.get(i)) continue;
if (pos[i] != BIT_x) continue;
unsigned num_pos = 0, num_neg = 0;
tbit b1 = (*neg[0])[i];
@ -472,12 +472,12 @@ void doc_manager::subtract(doc const& A, doc const& B, doc_vector& result) {
tbv_ref t(m);
r = allocate(A);
t = m.allocate(B.pos());
if (m.set_and(*t, A.pos()) && r->neg().insert(m, t.detach())) {
if (m.set_and(*t, A.pos())) {
r->neg().insert(m, t.detach());
}
if (fold_neg(*r))
result.push_back(r.detach());
}
else {
result.push_back(allocate(A));
}
for (unsigned i = 0; i < B.neg().size(); ++i) {
r = allocate(A);
if (set_and(*r, B.neg()[i])) {
@ -496,36 +496,19 @@ bool doc_manager::equals(doc const& a, doc const& b) const {
bool doc_manager::is_full(doc const& src) const {
return src.neg().is_empty() && m.equals(src.pos(), *m_full);
}
bool doc_manager::is_empty(doc const& src) {
bool doc_manager::is_empty_complete(ast_manager& m, doc const& src) {
if (src.neg().size() == 0) return false;
if (src.neg().size() == 1) {
return m.equals(src.pos(), src.neg()[0]);
}
return false;
#if 0
// buggy:
tbv_ref pos(m, m.allocate(src.pos()));
for (unsigned i = 0; i < src.neg().size(); ++i) {
bool found = false;
for (unsigned j = 0; !found && j < num_tbits(); ++j) {
tbit b1 = (*pos)[j];
tbit b2 = src.neg()[i][j];
found = (b1 != BIT_x && b2 != BIT_x && b1 != b2);
}
for (unsigned j = 0; !found && j < num_tbits(); ++j) {
tbit b1 = (*pos)[j];
tbit b2 = src.neg()[i][j];
found = (b1 == BIT_x && b2 != BIT_x);
if (found) {
m.set(*pos, j, neg(b2));
}
}
if (!found) {
return false; // TBD make complete SAT check.
}
smt_params fp;
smt::kernel s(m, fp);
expr_ref fml = to_formula(m, src);
s.assert_expr(fml);
lbool res = s.check();
if (res == l_true) {
return false;
}
SASSERT(res == l_false);
return true;
#endif
}
unsigned doc_manager::hash(doc const& src) const {
@ -553,16 +536,15 @@ bool doc_manager::contains(doc const& a, doc const& b) const {
return true;
}
bool doc_manager::contains(
unsigned offset_a, doc const& a,
doc_manager const& dm_b,
unsigned offset_b, doc const& b,
unsigned length) const {
if (!m.contains(offset_a, a.pos(), dm_b.tbvm(), offset_b, b.pos(), length)) return false;
bool doc_manager::contains(doc const& a, unsigned_vector const& colsa,
doc const& b, unsigned_vector const& colsb) const {
if (!m.contains(a.pos(), colsa, b.pos(), colsb))
return false;
for (unsigned i = 0; i < a.neg().size(); ++i) {
bool found = false;
for (unsigned j = 0; !found && j < b.neg().size(); ++j) {
found = dm_b.tbvm().contains(offset_b, b.neg()[j], tbvm(), offset_a, a.neg()[i], length);
found = m.contains(b.neg()[j], colsb, a.neg()[i], colsa);
}
if (!found) return false;
}
@ -583,7 +565,7 @@ std::ostream& doc_manager::display(std::ostream& out, doc const& b, unsigned hi,
}
void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst) {
void doc_manager::verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst) {
expr_ref fml1 = to_formula(m, src);
expr_ref fml2 = dstm.to_formula(m, dst);
project_rename(fml2, to_delete);
@ -620,11 +602,11 @@ expr_ref doc_manager::to_formula(ast_manager& m, doc const& src) {
return result;
}
void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
void doc_manager::project_expand(expr_ref& fml, bit_vector const& to_delete) {
ast_manager& m = fml.get_manager();
expr_ref tmp1(m), tmp2(m);
for (unsigned i = 0; i < num_tbits(); ++i) {
if (to_delete[i]) {
if (to_delete.get(i)) {
expr_safe_replace rep1(m), rep2(m);
rep1.insert(tbvm().mk_var(m, i), m.mk_true());
rep1(fml, tmp1);
@ -640,11 +622,11 @@ void doc_manager::project_expand(expr_ref& fml, bool const* to_delete) {
}
}
void doc_manager::project_rename(expr_ref& fml, bool const* to_delete) {
void doc_manager::project_rename(expr_ref& fml, bit_vector const& to_delete) {
ast_manager& m = fml.get_manager();
expr_safe_replace rep(m);
for (unsigned i = 0, j = 0; i < num_tbits(); ++i) {
if (!to_delete[i]) {
if (!to_delete.get(i)) {
rep.insert(tbvm().mk_var(m, j), tbvm().mk_var(m, i));
++j;
}

35
src/muz/rel/doc.h
View file

@ -48,7 +48,7 @@ class doc_manager {
project_resolve
};
project_action_t pick_resolvent(
tbv const& pos, tbv_vector const& neg, bool const* to_delete, unsigned& idx);
tbv const& pos, tbv_vector const& neg, bit_vector const& to_delete, unsigned& idx);
public:
doc_manager(unsigned num_bits);
~doc_manager();
@ -72,7 +72,7 @@ public:
doc& fill1(doc& src);
doc& fillX(doc& src);
bool is_full(doc const& src) const;
bool is_empty(doc const& src);
bool is_empty_complete(ast_manager& m, doc const& src);
bool set_and(doc& dst, doc const& src);
bool set_and(doc& dst, tbv const& src);
bool fold_neg(doc& dst);
@ -82,23 +82,22 @@ public:
bool equals(doc const& a, doc const& b) const;
unsigned hash(doc const& src) const;
bool contains(doc const& a, doc const& b) const;
bool contains(unsigned offset_a, doc const& a,
doc_manager const& dm_b, unsigned offset_b, doc const& b,
unsigned length) const;
bool contains(doc const& a, unsigned_vector const& colsa,
doc const& b, unsigned_vector const& colsb) const;
std::ostream& display(std::ostream& out, doc const& b) const;
std::ostream& display(std::ostream& out, doc const& b, unsigned hi, unsigned lo) const;
unsigned num_tbits() const { return m.num_tbits(); }
doc* project(doc_manager& dstm, unsigned n, bool const* to_delete, doc const& src);
doc* project(doc_manager& dstm, unsigned n, bit_vector const& to_delete, doc const& src);
bool well_formed(doc const& d) const;
bool merge(doc& d, unsigned lo, unsigned length, subset_ints const& equalities, bit_vector const& discard_cols);
void set(doc& d, unsigned idx, tbit value);
void verify_project(ast_manager& m, doc_manager& dstm, bool const* to_delete, doc const& src, doc const& dst);
void verify_project(ast_manager& m, doc_manager& dstm, bit_vector const& to_delete, doc const& src, doc const& dst);
private:
unsigned diff_by_012(tbv const& pos, tbv const& neg, unsigned& index);
bool merge(doc& d, unsigned idx, subset_ints const& equalities, bit_vector const& discard_cols);
void project_rename(expr_ref& fml, bool const* to_delete);
void project_expand(expr_ref& fml, bool const* to_delete);
void project_rename(expr_ref& fml, bit_vector const& to_delete);
void project_expand(expr_ref& fml, bit_vector const& to_delete);
expr_ref to_formula(ast_manager& m, doc const& src);
void check_equiv(ast_manager& m, expr* fml1, expr* fml2);
};
@ -119,10 +118,17 @@ class union_bvec {
public:
unsigned size() const { return m_elems.size(); }
T& operator[](unsigned idx) const { return *m_elems[idx]; }
bool is_empty() const { return m_elems.empty(); }
bool is_empty() const { return m_elems.empty(); }
bool is_empty_complete(ast_manager& m, doc_manager& dm) const {
for (unsigned i = 0; i < size(); ++i) {
if (!dm.is_empty_complete(m, *m_elems[i]))
return false;
}
return true;
}
bool is_full(M& m) const { return size() == 1 && m.is_full(*m_elems[0]); }
bool contains(M& m, T& t) const {
for (unsigned i = 0; i < m_elems.size(); ++i) {
for (unsigned i = 0; i < size(); ++i) {
if (m.contains(*m_elems[i], t)) return true;
}
return false;
@ -164,11 +170,13 @@ public:
SASSERT(t);
unsigned sz = size(), j = 0;
bool found = false;
for (unsigned i = 0; i < sz; ++i, ++j) {
unsigned i = 0;
for ( ; i < sz; ++i, ++j) {
if (m.contains(*m_elems[i], *t)) {
found = true;
break;
}
if (!found && m.contains(*t, *m_elems[i])) {
if (m.contains(*t, *m_elems[i])) {
m.deallocate(m_elems[i]);
--j;
}
@ -178,6 +186,7 @@ public:
}
if (j != sz) m_elems.resize(j);
if (found) {
SASSERT(j == i);
m.deallocate(t);
}
else {

4
src/muz/rel/rel_context.cpp
View file

@ -375,7 +375,7 @@ namespace datalog {
for (; it != end; ++it) {
func_decl* pred = *it;
relation_base & rel = get_relation(pred);
if (!rel.empty()) {
if (!rel.fast_empty()) {
non_empty = true;
break;
}
@ -449,7 +449,7 @@ namespace datalog {
bool rel_context::is_empty_relation(func_decl* pred) const {
relation_base* rb = try_get_relation(pred);
return !rb || rb->empty();
return !rb || rb->fast_empty();
}
relation_manager & rel_context::get_rmanager() { return m_rmanager; }

22
src/muz/rel/tbv.cpp
View file

@ -99,11 +99,11 @@ tbv* tbv_manager::allocate(tbv const& bv, unsigned const* permutation) {
}
return r;
}
tbv* tbv_manager::project(unsigned n, bool const* to_delete, tbv const& src) {
tbv* tbv_manager::project(unsigned n, bit_vector const& to_delete, tbv const& src) {
tbv* r = allocate();
unsigned i, j;
for (i = 0, j = 0; i < n; ++i) {
if (!to_delete[i]) {
if (!to_delete.get(i)) {
set(*r, j, src[i]);
++j;
}
@ -245,18 +245,12 @@ bool tbv_manager::contains(tbv const& a, tbv const& b) const {
return m.contains(a, b);
}
bool tbv_manager::contains(unsigned offset_a, tbv const& a,
tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
unsigned length) const {
if (this == &dm_b && length == num_tbits()) {
SASSERT(offset_a == 0);
SASSERT(offset_b == 0);
return m.contains(a, b);
}
for (unsigned i = 0; i < length; ++i) {
tbit bit_a = a[offset_a + i];
bool tbv_manager::contains(tbv const& a, unsigned_vector const& colsa,
tbv const& b, unsigned_vector const& colsb) const {
for (unsigned i = 0; i < colsa.size(); ++i) {
tbit bit_a = a[colsa[i]];
if (bit_a == BIT_x) continue;
if (bit_a != b[offset_b + i]) return false;
if (bit_a != b[colsb[i]]) return false;
}
return true;
}
@ -268,7 +262,7 @@ bool tbv_manager::intersect(tbv const& a, tbv const& b, tbv& result) {
std::ostream& tbv_manager::display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const {
SASSERT(lo <= hi && hi < num_tbits());
for (unsigned i = lo; i <= hi; ++i) {
for (unsigned i = hi+1; i-- > lo; ) {
switch (b.get(i)) {
case BIT_0:
out << '0';

7
src/muz/rel/tbv.h
View file

@ -70,13 +70,12 @@ public:
bool equals(tbv const& a, tbv const& b) const;
unsigned hash(tbv const& src) const;
bool contains(tbv const& a, tbv const& b) const;
bool contains(unsigned offset_a, tbv const& a,
tbv_manager const& dm_b, unsigned offset_b, tbv const& b,
unsigned length) const;
bool contains(tbv const& a, unsigned_vector const& colsa,
tbv const& b, unsigned_vector const& colsb) const;
bool intersect(tbv const& a, tbv const& b, tbv& result);
std::ostream& display(std::ostream& out, tbv const& b) const;
std::ostream& display(std::ostream& out, tbv const& b, unsigned hi, unsigned lo) const;
tbv* project(unsigned n, bool const* to_delete, tbv const& src);
tbv* project(unsigned n, bit_vector const& to_delete, tbv const& src);
bool is_well_formed(tbv const& b) const; // - does not contain BIT_z;
void set(tbv& dst, uint64 n, unsigned hi, unsigned lo);
void set(tbv& dst, rational const& r, unsigned hi, unsigned lo);

69
src/muz/rel/udoc_relation.cpp
View file

@ -21,10 +21,6 @@ Revision History:
Notes:
Current pending items:
- Fix the incomplete non-emptiness check in doc.cpp
It can fall back to a sat_solver call in the worst case.
The sat_solver.h interface gives a way to add clauses to a sat solver
and check for satisfiability. It can be used from scratch each time.
- Profile and fix bottlnecks:
- Potential bottleneck in projection exercised in some benchmarks.
Projection is asymptotically very expensive. We are here interested in
@ -58,9 +54,6 @@ Notes:
return tgt \ join_project(tgt, neg, c1, .., cN, d1, .. , dN)
We have most of the facilities required for a join project operation.
For example, the filter_project function uses both equalities and deleted columns.
- Lipstick service:
- filter_proj_fn uses both a bit_vector and a svector<bool> for representing removed bits.
This is due to underlying routines using different types for the same purpose.
--*/
#include "udoc_relation.h"
#include "dl_relation_manager.h"
@ -127,12 +120,7 @@ namespace datalog {
m_elems.push_back(fact2doc(f));
}
bool udoc_relation::empty() const {
if (m_elems.is_empty()) return true;
// TBD: make this a complete check
for (unsigned i = 0; i < m_elems.size(); ++i) {
if (!dm.is_empty(m_elems[i])) return false;
}
return true;
return m_elems.is_empty_complete(get_plugin().m, dm);
}
bool udoc_relation::contains_fact(const relation_fact & f) const {
doc_ref d(dm, fact2doc(f));
@ -482,7 +470,7 @@ namespace datalog {
}
class udoc_plugin::project_fn : public convenient_relation_project_fn {
svector<bool> m_to_delete;
bit_vector m_to_delete;
public:
project_fn(udoc_relation const & t, unsigned removed_col_cnt, const unsigned * removed_cols)
: convenient_relation_project_fn(t.get_signature(), removed_col_cnt, removed_cols) {
@ -490,7 +478,7 @@ namespace datalog {
unsigned n = t.get_dm().num_tbits();
m_to_delete.resize(n, false);
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_to_delete[m_removed_cols[i]] = true;
m_to_delete.set(m_removed_cols[i], true);
}
}
@ -505,7 +493,7 @@ namespace datalog {
udoc const& ud1 = t.get_udoc();
udoc& ud2 = r->get_udoc();
for (unsigned i = 0; i < ud1.size(); ++i) {
d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), ud1[i]);
d2 = dm1.project(dm2, m_to_delete.size(), m_to_delete, ud1[i]);
ud2.push_back(d2.detach());
}
TRACE("doc", tout << "final size: " << r->get_size_estimate_rows() << '\n';);
@ -1076,14 +1064,16 @@ namespace datalog {
// 4. Unit/stress test cases are needed.
//
class udoc_plugin::negation_filter_fn : public relation_intersection_filter_fn {
const unsigned_vector m_t_cols;
const unsigned_vector m_neg_cols;
unsigned_vector m_t_cols;
unsigned_vector m_neg_cols;
public:
negation_filter_fn(const udoc_relation & r, const udoc_relation & neg, unsigned joined_col_cnt,
const unsigned *t_cols, const unsigned *neg_cols)
: m_t_cols(joined_col_cnt, t_cols), m_neg_cols(joined_col_cnt, neg_cols) {
SASSERT(joined_col_cnt > 0);
r.expand_column_vector(m_t_cols);
neg.expand_column_vector(m_neg_cols);
}
virtual void operator()(relation_base& tb, const relation_base& negb) {
@ -1098,30 +1088,16 @@ namespace datalog {
udoc result;
for (unsigned i = 0; i < dst.size(); ++i) {
bool subsumed = false;
for (unsigned j = 0; j < neg.size(); ++j) {
for (unsigned c = 0; c < m_t_cols.size(); ++c) {
unsigned t_col = m_t_cols[c];
unsigned n_col = m_neg_cols[c];
unsigned num_bits = t.column_num_bits(t_col);
SASSERT(num_bits == n.column_num_bits(n_col));
unsigned t_idx = t.column_idx(t_col);
unsigned n_idx = n.column_idx(n_col);
bool cont = dmn.contains(n_idx, neg[j], dmt, t_idx, dst[i], num_bits);
IF_VERBOSE(
3,
dmt.display(verbose_stream() << "dst:", dst[i], t_idx+num_bits-1,t_idx) << "\n";
dmn.display(verbose_stream() << "neg:", neg[j], n_idx+num_bits-1,n_idx) << "\n";
verbose_stream() << "contains: " << (cont?"true":"false") << "\n";);
if (!cont) {
goto next_neg_disj;
}
if (dmn.contains(neg[j], m_neg_cols, dst[i], m_t_cols)) {
dmt.deallocate(&dst[i]);
subsumed = true;
break;
}
dmt.deallocate(&dst[i]);
goto next_disj;
next_neg_disj:;
}
result.push_back(&dst[i]);
next_disj:;
if (!subsumed)
result.push_back(&dst[i]);
}
std::swap(dst, result);
if (dst.is_empty()) {
@ -1207,8 +1183,7 @@ namespace datalog {
expr_ref m_reduced_condition;
udoc m_udoc;
udoc m_udoc2;
bit_vector m_col_list; // map: col idx -> bool (whether the column is to be removed)
svector<bool> m_to_delete; // same
bit_vector m_to_delete; // map: col idx -> bool (whether the column is to be removed)
subset_ints m_equalities;
unsigned_vector m_roots;
@ -1222,19 +1197,17 @@ namespace datalog {
m_equalities(union_ctx) {
unsigned num_bits = t.get_num_bits();
t.expand_column_vector(m_removed_cols);
m_col_list.resize(num_bits, false);
m_to_delete.resize(num_bits, false);
for (unsigned i = 0; i < num_bits; ++i) {
m_equalities.mk_var();
}
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_col_list.set(m_removed_cols[i], true);
m_to_delete[m_removed_cols[i]] = true;
m_to_delete.set(m_removed_cols[i], true);
}
expr_ref guard(m), non_eq_cond(condition, m);
t.extract_equalities(condition, non_eq_cond, m_equalities, m_roots);
t.extract_guard(non_eq_cond, guard, m_reduced_condition);
t.compile_guard(guard, m_udoc, m_col_list);
t.compile_guard(guard, m_udoc, m_to_delete);
}
virtual ~filter_proj_fn() {
@ -1247,13 +1220,13 @@ namespace datalog {
ast_manager& m = m_reduced_condition.get_manager();
m_udoc2.copy(dm, u1);
m_udoc2.intersect(dm, m_udoc);
t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_col_list);
m_udoc2.merge(dm, m_roots, m_equalities, m_col_list);
t.apply_guard(m_reduced_condition, m_udoc2, m_equalities, m_to_delete);
m_udoc2.merge(dm, m_roots, m_equalities, m_to_delete);
SASSERT(m_udoc2.well_formed(dm));
udoc_relation* r = get(t.get_plugin().mk_empty(get_result_signature()));
doc_manager& dm2 = r->get_dm();
for (unsigned i = 0; i < m_udoc2.size(); ++i) {
doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete.c_ptr(), m_udoc2[i]);
doc* d = dm.project(dm2, m_to_delete.size(), m_to_delete, m_udoc2[i]);
r->get_udoc().insert(dm2, d);
SASSERT(r->get_udoc().well_formed(dm2));
}

118
src/sat/sat_bceq.cpp
View file

@ -64,6 +64,11 @@ namespace sat {
m_bin_clauses.push_back(cls);
register_clause(cls);
}
TRACE("sat",
for (unsigned i = 0; i < m_clauses.size(); ++i) {
clause const* cls = m_clauses[i];
if (cls) tout << *cls << "\n";
});
}
void bceq::pure_decompose() {
@ -109,7 +114,7 @@ namespace sat {
m_L_blits.resize(sz1+delta1, lit);
m_R_blits.resize(sz2+delta2, ~lit);
}
std::cout << lit << " " << "pos: " << delta1 << " " << "neg: " << delta2 << "\n";
TRACE("bceq", tout << lit << " " << "pos: " << delta1 << " " << "neg: " << delta2 << "\n";);
}
void bceq::pure_decompose(clause_use_list& uses, svector<clause*>& clauses) {
@ -134,24 +139,88 @@ namespace sat {
for (unsigned i = 0; i < m_L.size(); ++i) {
ul.insert(*m_L[i]);
}
#define MOVE_R_TO_L \
// cheap pass: add clauses from R in order
// such that they are blocked with respect to
// predecessors.
m_removed.reset();
for (unsigned i = 0; i < m_R.size(); ++i) {
literal lit = find_blocked(*m_R[i]);
if (lit != null_literal) {
m_L.push_back(m_R[i]);
m_L_blits.push_back(lit);
ul.insert(*m_R[i]);
m_L.push_back(m_R[i]);
m_L_blits.push_back(lit);
ul.insert(*m_R[i]);
m_R[i] = m_R.back();
m_R_blits[i] = m_R_blits.back();
m_R.pop_back();
m_R_blits.pop_back();
--i;
}
}
// expensive pass: add clauses from R as long
// as BCE produces the empty set of clauses.
for (unsigned i = 0; i < m_R.size(); ++i) {
if (bce(*m_R[i])) {
m_R[i] = m_R.back();
m_R_blits[i] = m_R_blits.back();
m_R.pop_back();
m_R_blits.pop_back();
--i;
}
}
}
m_use_list = save;
}
bool bceq::bce(clause& cls) {
svector<bool> live_clauses;
use_list ul;
use_list* save = m_use_list;
m_use_list = &ul;
ul.init(m_solver.num_vars());
for (unsigned i = 0; i < m_L.size(); ++i) {
ul.insert(*m_L[i]);
}
ul.insert(cls);
svector<clause*> clauses(m_L), new_clauses;
literal_vector blits(m_L_blits), new_blits;
clauses.push_back(&cls);
blits.push_back(null_literal);
bool removed = false;
m_removed.reset();
do {
removed = false;
for (unsigned i = 0; i < clauses.size(); ++i) {
clause& cls = *clauses[i];
literal lit = find_blocked(cls);
if (lit != null_literal) {
m_removed.setx(cls.id(), true, false);
new_clauses.push_back(&cls);
new_blits.push_back(lit);
removed = true;
clauses[i] = clauses.back();
blits[i] = blits.back();
clauses.pop_back();
blits.pop_back();
--i;
}
}
}
while (removed);
if (clauses.empty()) {
m_L.reset();
m_L_blits.reset();
new_clauses.reverse();
new_blits.reverse();
m_L.append(new_clauses);
m_L_blits.append(new_blits);
}
std::cout << "Number left after BCE: " << clauses.size() << "\n";
return clauses.empty();
}
literal bceq::find_blocked(clause const& cls) {
std::cout << "find blocker for: " << cls << "\n";
TRACE("bceq", tout << cls << "\n";);
unsigned sz = cls.size();
for (unsigned i = 0; i < sz; ++i) {
@ -161,7 +230,7 @@ namespace sat {
for (unsigned i = 0; i < sz; ++i) {
literal lit = cls[i];
if (is_blocked(lit)) {
std::cout << "is blocked " << lit << " : " << cls << "\n";
TRACE("bceq", tout << "is blocked " << lit << " : " << cls << "\n";);
result = lit;
break;
}
@ -178,12 +247,12 @@ namespace sat {
while (!it.at_end()) {
clause const& cls = it.curr();
unsigned sz = cls.size();
bool is_axiom = false;
bool is_axiom = m_removed.get(cls.id(), false);
for (unsigned i = 0; !is_axiom && i < sz; ++i) {
is_axiom = m_marked[cls[i].index()] && cls[i] != ~lit;
}
std::cout << "resolvent " << lit << " : " << cls << " " << (is_axiom?"axiom":"non-axiom") << "\n";
TRACE("bceq", tout << "resolvent " << lit << " : " << cls << " " << (is_axiom?"axiom":"non-axiom") << "\n";);
if (!is_axiom) {
return false;
}
@ -231,8 +300,6 @@ namespace sat {
clause const& cls = *m_rstack[i];
literal block_lit = m_bstack[i];
uint64 b = eval_clause(cls);
// std::cout << "Eval: " << block_lit << " " << std::hex << " ";
// std::cout << m_rbits[block_lit.var()] << " " << b << std::dec << "\n";
// v = 0, b = 0 -> v := 1
// v = 0, b = 1 -> v := 0
// v = 1, b = 0 -> v := 0
@ -278,7 +345,7 @@ namespace sat {
table.insert(val, i);
}
}
union_find.display(std::cout);
TRACE("sat", union_find.display(tout););
//
// Preliminary version:
@ -305,7 +372,7 @@ namespace sat {
}
void bceq::check_equality(unsigned v1, unsigned v2) {
std::cout << "check: " << v1 << " = " << v2 << "\n";
TRACE("sat", tout << "check: " << v1 << " = " << v2 << "\n";);
uint64 val1 = m_rbits[v1];
uint64 val2 = m_rbits[v2];
literal l1 = literal(v1, false);
@ -315,7 +382,7 @@ namespace sat {
l2.neg();
}
if (is_equiv(l1, l2)) {
std::cout << "Already equivalent: " << l1 << " " << l2 << "\n";
TRACE("sat", tout << "Already equivalent: " << l1 << " " << l2 << "\n";);
return;
}
@ -329,10 +396,10 @@ namespace sat {
is_sat = m_s->check(2, lits);
}
if (is_sat == l_false) {
std::cout << "Found equivalent: " << l1 << " " << l2 << "\n";
TRACE("sat", tout << "Found equivalent: " << l1 << " " << l2 << "\n";);
}
else {
std::cout << "Not equivalent\n";
TRACE("sat", tout << "Not equivalent: " << l1 << " " << l2 << "\n";);
}
}
@ -344,7 +411,7 @@ namespace sat {
found = w.is_binary_clause() && w.get_literal() == ~l2;
}
if (!found) return false;
found = true;
found = false;
watch_list const& w2 = m_solver.get_wlist(~l1);
for (unsigned i = 0; !found && i < w2.size(); ++i) {
watched const& w = w2[i];
@ -361,6 +428,8 @@ namespace sat {
void bceq::operator()() {
if (!m_solver.m_config.m_bcd) return;
flet<bool> _disable_bcd(m_solver.m_config.m_bcd, false);
use_list ul;
solver s(m_solver.m_params, 0);
m_use_list = &ul;
@ -369,7 +438,20 @@ namespace sat {
init();
pure_decompose();
post_decompose();
std::cout << m_L.size() << " vs " << m_R.size() << "\n";
std::cout << "Decomposed set " << m_L.size() << "\n";
TRACE("sat",
tout << "Decomposed set " << m_L.size() << "\n";
for (unsigned i = 0; i < m_L.size(); ++i) {
clause const* cls = m_L[i];
if (cls) tout << *cls << "\n";
}
tout << "remainder " << m_R.size() << "\n";
for (unsigned i = 0; i < m_R.size(); ++i) {
clause const* cls = m_R[i];
if (cls) tout << *cls << "\n";
}
);
sat_sweep();
extract_partition();
cleanup();

2
src/sat/sat_bceq.h
View file

@ -45,6 +45,7 @@ namespace sat {
svector<clause*> m_rstack; // stack of blocked clauses
literal_vector m_bstack; // stack of blocking literals
svector<bool> m_marked;
svector<bool> m_removed; // set of clauses removed (not considered in clause set during BCE)
union_find_default_ctx m_union_find_ctx;
void init();
@ -55,6 +56,7 @@ namespace sat {
void pure_decompose(clause_use_list& uses, svector<clause*>& clauses);
void post_decompose();
literal find_blocked(clause const& cls);
bool bce(clause& cls);
bool is_blocked(literal lit) const;
void init_rbits();
void init_reconstruction_stack();

1
src/sat/sat_config.cpp
View file

@ -107,6 +107,7 @@ namespace sat {
m_minimize_core = p.minimize_core();
m_minimize_core_partial = p.minimize_core_partial();
m_optimize_model = p.optimize_model();
m_bcd = p.bcd();
m_dyn_sub_res = p.dyn_sub_res();
}

1
src/sat/sat_config.h
View file

@ -71,6 +71,7 @@ namespace sat {
bool m_minimize_core;
bool m_minimize_core_partial;
bool m_optimize_model;
bool m_bcd;
symbol m_always_true;

1
src/sat/sat_params.pyg
View file

@ -21,4 +21,5 @@ def_module_params('sat',
('minimize_core', BOOL, False, 'minimize computed core'),
('minimize_core_partial', BOOL, False, 'apply partial (cheap) core minimization'),
('optimize_model', BOOL, False, 'enable optimization of soft constraints'),
('bcd', BOOL, False, 'enable blocked clause decomposition for equality extraction'),
('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks')))

2
src/sat/sat_simplifier.cpp
View file

@ -157,7 +157,7 @@ namespace sat {
if (!learned && (m_elim_blocked_clauses || m_elim_blocked_clauses_at == m_num_calls))
elim_blocked_clauses();
#if 0
#if 1
// experiment is disabled.
if (!learned) { // && m_equality_inference
bceq bc(s);

2
src/sat/sat_solver.cpp
View file

@ -20,6 +20,7 @@ Revision History:
#include"sat_integrity_checker.h"
#include"luby.h"
#include"trace.h"
#include"sat_bceq.h"
// define to update glue during propagation
#define UPDATE_GLUE
@ -959,6 +960,7 @@ namespace sat {
m_stopwatch.start();
m_core.reset();
TRACE("sat", display(tout););
}
/**

51
src/test/doc.cpp
View file

@ -73,23 +73,24 @@ static void tst_doc1(unsigned n) {
m.display(std::cout, *d1) << "\n";
svector<bool> to_delete(n, false);
to_delete[1] = true;
to_delete[3] = true;
bit_vector to_delete;
to_delete.resize(n, false);
to_delete.set(1);
to_delete.set(3);
doc_manager m1(n-2);
doc_ref d1_1(m1, m.project(m1, n, to_delete.c_ptr(), *d1));
doc_ref d1_1(m1, m.project(m1, n, to_delete, *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));
m.set(*d1,2,BIT_x);
m.set(*d1,4,BIT_x);
d1_1 = m.project(m1, n, to_delete.c_ptr(), *d1);
d1_1 = m.project(m1, n, to_delete, *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);
d1_1 = m.project(m1, n, to_delete, *d1);
m.display(std::cout, *d1) << " -> ";
m1.display(std::cout, *d1_1) << "\n";
}
@ -216,11 +217,11 @@ class test_doc_cls {
return result;
}
void project(doc const& d, doc_manager& m2, bool const* to_delete, doc_ref& result) {
void project(doc const& d, doc_manager& m2, const bit_vector& 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 << (to_delete.get(i)?"0":"1");
}
tout << " ";
dm.display(tout, d) << " -> ";
@ -234,28 +235,29 @@ class test_doc_cls {
d = mk_rand_doc(3);
expr_ref fml1(m), fml2(m), fml3(m), tmp1(m), tmp2(m), fml(m);
fml1 = to_formula(*d, dm);
svector<bool> to_delete(m_vars.size(), false);
bit_vector to_delete;
to_delete.reserve(m_vars.size(), false);
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;
to_delete.set(i, m_ran(2) == 0);
if (!to_delete.get(i)) ++num_bits;
}
doc_manager m2(num_bits);
doc_ref result(m2);
project(*d, m2, to_delete.c_ptr(), result);
project(*d, m2, to_delete, result);
TRACE("doc",
dm.display(tout, *d) << "\n";
m2.display(tout, *result) << "\n";);
fml2 = to_formula(*result, m2);
project_expand(fml1, to_delete.c_ptr());
project_rename(fml2, to_delete.c_ptr());
project_expand(fml1, to_delete);
project_rename(fml2, to_delete);
check_equiv(fml1, fml2);
}
void project_expand(expr_ref& fml, bool const* to_delete) {
void project_expand(expr_ref& fml, bit_vector const& to_delete) {
expr_ref tmp1(m), tmp2(m);
for (unsigned i = 0; i < m_vars.size(); ++i) {
if (to_delete[i]) {
if (to_delete.get(i)) {
expr_safe_replace rep1(m), rep2(m);
rep1.insert(m_vars[i].get(), m.mk_true());
rep1(fml, tmp1);
@ -271,10 +273,10 @@ class test_doc_cls {
}
}
void project_rename(expr_ref& fml, bool const* to_delete) {
void project_rename(expr_ref& fml, bit_vector const& to_delete) {
expr_safe_replace rep(m);
for (unsigned i = 0, j = 0; i < m_vars.size(); ++i) {
if (!to_delete[i]) {
if (!to_delete.get(i)) {
rep.insert(m_vars[j].get(), m_vars[i].get());
++j;
}
@ -293,7 +295,7 @@ class test_doc_cls {
d->neg().push_back(t);
}
fml1 = mk_and(m, fmls.size(), fmls.c_ptr());
svector<bool> to_merge(N, false), to_delete(N, false);
svector<bool> to_merge(N, false);
bit_vector discard_cols;
discard_cols.resize(N, false);
unsigned num_bits = 1;
@ -371,17 +373,18 @@ public:
dm.tbvm().set(*t, 0, BIT_0);
d->neg().push_back(t.detach());
unsigned num_bits = dm.num_tbits();
svector<bool> to_delete(num_bits, false);
bit_vector to_delete;
to_delete.reserve(num_bits, false);
fml1 = to_formula(*d, dm);
to_delete[0] = true;
to_delete.set(0, true);
doc_manager m2(num_bits-1);
doc_ref result(m2);
project(*d, m2, to_delete.c_ptr(), result);
project(*d, m2, to_delete, result);
dm.display(std::cout, *d) << "\n";
m2.display(std::cout, *result) << "\n";
fml2 = to_formula(*result, m2);
project_rename(fml2, to_delete.c_ptr());
project_expand(fml1, to_delete.c_ptr());
project_rename(fml2, to_delete);
project_expand(fml1, to_delete);
std::cout << fml1 << " " << fml2 << "\n";
check_equiv(fml1, fml2);
}

9
src/test/tbv.cpp
View file

@ -25,13 +25,14 @@ static void tst1(unsigned num_bits) {
SASSERT(m.equals(*b0, *bN));
VERIFY(!m.intersect(*b0,*b1,*bN));
m.fill1(*b1);
svector<bool> to_delete(num_bits, false);
bit_vector to_delete;
to_delete.reserve(num_bits, false);
tbv_manager m2(num_bits-2);
to_delete[1] = true;
to_delete[3] = true;
to_delete.set(1);
to_delete.set(3);
m.set(*b1, 2, BIT_0);
m.set(*b1, 4, BIT_x);
tbv_ref b2(m2, m2.project(num_bits, to_delete.c_ptr(), *b1));
tbv_ref b2(m2, m2.project(num_bits, to_delete, *b1));
m.display(std::cout, *b1) << " -> ";
m2.display(std::cout, *b2) << "\n";
m.deallocate(b0);

50
src/test/udoc_relation.cpp
View file

@ -148,6 +148,7 @@ public:
test_rename();
test_filter_neg();
test_filter_neg2();
// empty
@ -551,6 +552,55 @@ public:
t2->deallocate();
}
void test_filter_neg2() {
// filter_by_negation
relation_signature sig4;
sig4.push_back(bv.mk_sort(1));
sig4.push_back(bv.mk_sort(1));
sig4.push_back(bv.mk_sort(1));
unsigned_vector cols, allcols;
cols.push_back(0);
cols.push_back(2);
allcols.push_back(0);
allcols.push_back(1);
allcols.push_back(2);
/// xxx \ 1x0
udoc_relation* t1 = mk_full(sig4);
{
udoc_relation* neg = mk_full(sig4);
doc& n = neg->get_udoc()[0];
neg->get_dm().set(n, 0, BIT_1);
neg->get_dm().set(n, 2, BIT_0);
apply_filter_neg(*t1, *neg, allcols, allcols);
neg->deallocate();
}
/// xxx \ (1x1 u 0x0)
udoc_relation* t2 = mk_full(sig4);
{
udoc_relation* neg = mk_full(sig4);
doc& n = neg->get_udoc()[0];
neg->get_dm().set(n, 0, BIT_0);
neg->get_dm().set(n, 2, BIT_0);
apply_filter_neg(*t2, *neg, allcols, allcols);
neg->deallocate();
}
{
udoc_relation* neg = mk_full(sig4);
doc& n = neg->get_udoc()[0];
neg->get_dm().set(n, 0, BIT_1);
neg->get_dm().set(n, 2, BIT_1);
apply_filter_neg(*t2, *neg, allcols, allcols);
neg->deallocate();
}
apply_filter_neg(*t2, *t1, cols, cols);
t1->deallocate();
t2->deallocate();
}
void set_random(udoc_relation& r, unsigned num_vals) {
unsigned num_bits = r.get_dm().num_tbits();
udoc_relation* full = mk_full(r.get_signature());

12
src/util/union_find.h
View file

@ -132,6 +132,18 @@ public:
CASSERT("union_find", check_invariant());
}
// dissolve equivalence class of v
// this method cannot be used with backtracking.
void dissolve(unsigned v) {
do {
w = next(v);
m_size[v] = 1;
m_find[v] = v;
m_next[v] = v;
}
while (w != v);
}
void display(std::ostream & out) const {
unsigned num = get_num_vars();
for (unsigned v = 0; v < num; v++) {