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

updated unit tests

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2014-09-20 01:05:43 -07:00
parent 2b2ba2d541
commit f94bdf4035
6 changed files with 346 additions and 84 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -415,8 +415,8 @@ void doc_manager::subtract(doc const& A, doc const& B, ptr_vector<doc>& result)
r2 = allocate(B.neg()[i]);
if (set_and(*r, *r2)) {
result.push_back(r.detach());
r = allocate(A);
}
r = allocate(A);
}
}
bool doc_manager::equals(doc const& a, doc const& b) const {

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

@ -22,16 +22,20 @@ Revision History:
#include "hashtable.h"
//#define _DEBUG_MEM 1
#define _DEBUG_MEM 0
static bool s_debug_alloc = false;
void tbv_manager::debug_alloc() {
s_debug_alloc = true;
}
tbv_manager::~tbv_manager() {
#if _DEBUG_MEM
ptr_vector<tbv>::iterator it = allocated_tbvs.begin(), end = allocated_tbvs.end();
for (; it != end; ++it) {
std::cout << "dangling: " << (*it) << "\n";
}
#endif
DEBUG_CODE(
ptr_vector<tbv>::iterator it = allocated_tbvs.begin();
ptr_vector<tbv>::iterator end = allocated_tbvs.end();
for (; it != end; ++it) {
std::cout << "dangling: " << (*it) << "\n";
TRACE("doc", tout << "dangling: " << (*it) << "\n";);
});
}
void tbv_manager::reset() {
@ -39,10 +43,12 @@ void tbv_manager::reset() {
}
tbv* tbv_manager::allocate() {
tbv* r = reinterpret_cast<tbv*>(m.allocate());
#if _DEBUG_MEM
std::cout << allocated_tbvs.size() << " " << r << "\n";
allocated_tbvs.insert(r);
#endif
DEBUG_CODE(
if (s_debug_alloc) {
TRACE("doc", tout << allocated_tbvs.size() << " " << r << "\n";);
}
allocated_tbvs.insert(r);
);
return r;
}
tbv* tbv_manager::allocate1() {
@ -145,14 +151,15 @@ tbv* tbv_manager::allocate(rational const& r) {
return v;
}
void tbv_manager::deallocate(tbv* bv) {
#if _DEBUG_MEM
if (!allocated_tbvs.contains(bv)) {
std::cout << "double deallocate: " << bv << "\n";
UNREACHABLE();
}
std::cout << "deallocate: " << bv << "\n";
allocated_tbvs.erase(bv);
#endif
DEBUG_CODE(
if (!allocated_tbvs.contains(bv)) {
std::cout << "double deallocate: " << bv << "\n";
UNREACHABLE();
}
if (s_debug_alloc) {
TRACE("doc", tout << "deallocate: " << bv << "\n";);
}
allocated_tbvs.erase(bv););
m.deallocate(bv);
}
void tbv_manager::copy(tbv& dst, tbv const& src) const {

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

@ -73,6 +73,8 @@ public:
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;
static void debug_alloc();
};
class tbv: private fixed_bit_vector {
@ -132,6 +134,7 @@ public:
return *this;
}
tbv& operator*() { return *d; }
tbv* operator->() { return d; }
tbv* get() { return d; }
tbv* detach() { tbv* result = d; d = 0; return result; }
};

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

@ -667,6 +667,7 @@ namespace datalog {
TRACE("doc", sub.display(dm, tout << "sub:") << "\n";);
result.subtract(dm, sub);
result.simplify(dm);
sub.reset(dm);
TRACE("doc", result.display(dm, tout << "result:") << "\n";);
}
@ -678,7 +679,11 @@ namespace datalog {
arg = mk_not(m, to_app(g)->get_arg(i));
apply_guard(arg, sub, equalities, discard_cols);
}
TRACE("doc", result.display(dm, tout << "result0:") << "\n";);
result.subtract(dm, sub);
TRACE("doc",
sub.display(dm, tout << "sub:") << "\n";
result.display(dm, tout << "result:") << "\n";);
sub.reset(dm);
}
else if (m.is_true(g)) {
@ -897,7 +902,7 @@ namespace datalog {
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_col_list.set(m_removed_cols[i], true);
}
m_to_delete.resize(m_removed_cols.size(), false);
m_to_delete.resize(t.get_num_bits(), false);
for (unsigned i = 0; i < m_removed_cols.size(); ++i) {
m_to_delete[m_removed_cols[i]] = true;
}

71
src/test/doc.cpp
View file

@ -167,6 +167,16 @@ class test_doc_cls {
return result;
}
expr_ref to_formula(udoc const& ud, doc_manager& m2, bool const* to_delete) {
expr_ref result(m);
expr_ref_vector disjs(m);
for (unsigned i = 0; i < ud.size(); ++i) {
disjs.push_back(to_formula(ud[i], m2, to_delete));
}
result = mk_or(m, disjs.size(), disjs.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",
@ -264,15 +274,20 @@ class test_doc_cls {
}
rw(fml1);
rw(fml2);
check_equiv(fml1, fml2);
}
void check_equiv(expr* fml1, expr* fml2) {
smt_params fp;
smt::kernel solver(m, fp);
TRACE("doc", tout << "manual project:\n" << fml1 << "\nautomatic project: \n" << fml2 << "\n";);
expr_ref fml(m);
fml = m.mk_not(m.mk_eq(fml1, fml2));
solver.assert_expr(fml);
lbool res = solver.check();
SASSERT(res == l_false);
}
public:
test_doc_cls(unsigned num_vars): dm(num_vars), m_vars(m) {
reg_decl_plugins(m);
@ -292,15 +307,61 @@ public:
test_merge(num_clauses);
}
}
void test_subtract() {
doc_ref d1(dm);
doc_ref d2(dm);
doc_ref d3(dm);
udoc ds1, ds2;
d1 = dm.allocateX();
d2 = dm.allocateX();
d3 = dm.allocateX();
dm.set(*d1, 0, BIT_1);
dm.set(*d1, 1, BIT_0);
dm.set(*d2, 0, BIT_0);
dm.set(*d2, 1, BIT_1);
//ds1.push_back(d1.detach());
ds1.push_back(d2.detach());
// ds1 = {10x, 01x}
d1 = dm.allocateX();
tbv_ref t1(dm.tbvm());
tbv_ref t2(dm.tbvm());
t1 = dm.tbvm().allocateX();
t2 = dm.tbvm().allocateX();
t1->set(0, BIT_1);
t1->set(2, BIT_0);
t2->set(0, BIT_0);
t2->set(2, BIT_1);
d1->neg().push_back(t1.detach());
d1->neg().push_back(t2.detach());
ds2.push_back(d1.detach());
ds1.display(dm, std::cout) << "\n";
ds2.display(dm, std::cout) << "\n";
svector<bool> to_delete(m_vars.size(), false);
expr_ref fml1 = to_formula(ds1, dm, to_delete.c_ptr());
expr_ref fml2 = to_formula(ds2, dm, to_delete.c_ptr());
ds1.subtract(dm, ds2);
ds1.display(dm, std::cout) << "\n";
expr_ref fml3 = to_formula(ds1, dm, to_delete.c_ptr());
fml1 = m.mk_and(fml1, m.mk_not(fml2));
check_equiv(fml1, fml3);
ds1.reset(dm);
ds2.reset(dm);
//sub:{xxx \ {1x0, 0x1}}
//result:{100}
}
};
void tst_doc() {
test_doc_cls tp(4);
tp.test_subtract();
tp.test_merge(200,7);
tp.test_project(200,7);
tst_doc1(5);
tst_doc1(10);
tst_doc1(70);
test_doc_cls tp(4);
tp.test_merge(200,7);
tp.test_project(200,7);
}

300
src/test/udoc_relation.cpp
View file

@ -87,6 +87,43 @@ public:
relation_base* t;
udoc_relation* t1, *t2, *t3;
expr_ref fml(m);
// filter_by_negation
/*
The filter_by_negation postcondition:
filter_by_negation(tgt, neg, columns in tgt: c1,...,cN,
corresponding columns in neg: d1,...,dN):
tgt_1:={x: x\in tgt_0 && ! \exists y: ( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) }
*/
{
relation_signature sig4;
sig4.push_back(bv.mk_sort(1));
sig4.push_back(bv.mk_sort(1));
sig4.push_back(bv.mk_sort(1));
t1 = mk_empty(sig4);
t2 = mk_empty(sig4);
unsigned_vector cols1, cols2;
unsigned num_bits = t1->get_dm().num_tbits();
cols1.push_back(0);
cols2.push_back(1);
for (unsigned i = 0; i < 100; ++i) {
set_random(*t1, 2*num_bits/3);
set_random(*t2, 2*num_bits/3);
apply_filter_neg(*t1,*t2, cols1, cols2);
}
cols1.push_back(1);
cols2.push_back(2);
for (unsigned i = 0; i < 100; ++i) {
set_random(*t1, 2*num_bits/3);
set_random(*t2, 2*num_bits/3);
apply_filter_neg(*t1,*t2, cols1, cols2);
}
t1->deallocate();
t2->deallocate();
}
// empty
{
std::cout << "empty\n";
@ -228,6 +265,22 @@ public:
t1->display(std::cout); std::cout << "\n";
t1->deallocate();
}
// tbv_manager::debug_alloc();
{
relation_signature sig3;
sig3.push_back(m.mk_bool_sort());
sig3.push_back(m.mk_bool_sort());
sig3.push_back(m.mk_bool_sort());
var_ref v0(m.mk_var(0, m.mk_bool_sort()),m);
var_ref v1(m.mk_var(1, m.mk_bool_sort()),m);
var_ref v2(m.mk_var(2, m.mk_bool_sort()),m);
app_ref cond1(m);
t1 = mk_full(sig3);
cond1 = m.mk_eq(v0,v1);
apply_filter(*t1, cond1);
t1->deallocate();
}
{
relation_signature sig3;
@ -238,8 +291,8 @@ public:
var_ref v1(m.mk_var(1, m.mk_bool_sort()),m);
var_ref v2(m.mk_var(2, m.mk_bool_sort()),m);
app_ref cond1(m);
cond1 = m.mk_or(m.mk_eq(v0,v1),m.mk_eq(v0,v2));
t1 = mk_full(sig3);
cond1 = m.mk_or(m.mk_eq(v0,v1),m.mk_eq(v0,v2));
apply_filter(*t1, cond1);
t1->deallocate();
}
@ -259,73 +312,138 @@ public:
t1->deallocate();
}
app_ref_vector conds(m);
app_ref cond1(m);
var_ref v0(m.mk_var(0, bv.mk_sort(3)),m);
var_ref v1(m.mk_var(1, bv.mk_sort(6)),m);
var_ref v2(m.mk_var(2, bv.mk_sort(3)),m);
var_ref v3(m.mk_var(3, bv.mk_sort(3)),m);
var_ref v4(m.mk_var(4, bv.mk_sort(3)),m);
conds.push_back(m.mk_true());
conds.push_back(m.mk_false());
conds.push_back(m.mk_eq(v0, v2));
conds.push_back(m.mk_not(m.mk_eq(v0, v2)));
conds.push_back(m.mk_eq(v0, bv.mk_numeral(rational(2), 3)));
cond1 = m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2));
conds.push_back(cond1);
conds.push_back(m.mk_or(cond1,m.mk_eq(v3,v4)));
conds.push_back(m.mk_or(cond1,m.mk_eq(ex(2,1,v3),ex(1,0,v4))));
conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v0,v4)));
conds.push_back(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4)));
conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),ex(1,0,v2)),m.mk_eq(v3,v4)));
conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)),
m.mk_eq(v3,v4)));
conds.push_back(m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)),
m.mk_eq(v3,bv.mk_numeral(rational(3),3))));
conds.push_back(m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(5),3)),
m.mk_eq(v3,bv.mk_numeral(rational(5),3))));
conds.push_back(m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(7),3)),
m.mk_eq(v3,bv.mk_numeral(rational(7),3))));
conds.push_back(m.mk_not(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4))));
// filter_interpreted
{
std::cout << "filter interpreted\n";
t1 = mk_full(sig2);
var_ref v0(m.mk_var(0, bv.mk_sort(3)),m);
var_ref v1(m.mk_var(1, bv.mk_sort(6)),m);
var_ref v2(m.mk_var(2, bv.mk_sort(3)),m);
var_ref v3(m.mk_var(3, bv.mk_sort(3)),m);
var_ref v4(m.mk_var(4, bv.mk_sort(3)),m);
app_ref cond1(m), cond2(m), cond3(m), cond4(m);
app_ref cond5(m), cond6(m), cond7(m), cond8(m);
cond1 = m.mk_true();
cond2 = m.mk_false();
cond3 = m.mk_eq(v0, v2);
cond4 = m.mk_not(m.mk_eq(v0, v2));
cond5 = m.mk_eq(v0, bv.mk_numeral(rational(2), 3));
apply_filter(*t1, cond1);
apply_filter(*t1, cond2);
apply_filter(*t1, cond3);
apply_filter(*t1, cond4);
apply_filter(*t1, cond5);
cond1 = m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2));
apply_filter(*t1, cond1);
cond2 = m.mk_or(cond1,m.mk_eq(v3,v4));
apply_filter(*t1, cond2);
cond2 = m.mk_or(cond1,m.mk_eq(ex(2,1,v3),ex(1,0,v4)));
apply_filter(*t1, cond2);
cond1 = m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v0,v4));
apply_filter(*t1, cond1);
cond1 = m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4));
apply_filter(*t1, cond1);
cond1 = m.mk_or(m.mk_eq(ex(2,1,v0),ex(1,0,v2)),m.mk_eq(v3,v4));
apply_filter(*t1, cond1);
cond1 = m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)),
m.mk_eq(v3,v4));
apply_filter(*t1, cond1);
cond1 = m.mk_or(m.mk_eq(ex(2,1,v0),bv.mk_numeral(rational(3),2)),
m.mk_eq(v3,bv.mk_numeral(rational(3),5)));
apply_filter(*t1, cond1);
cond1 = m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(5),3)),
m.mk_eq(v3,bv.mk_numeral(rational(5),3)));
apply_filter(*t1, cond1);
cond1 = m.mk_or(m.mk_eq(v0,bv.mk_numeral(rational(7),3)),
m.mk_eq(v3,bv.mk_numeral(rational(7),3)));
apply_filter(*t1, cond1);
cond1 = m.mk_not(m.mk_or(m.mk_eq(v0,v2),m.mk_eq(v3,v4)));
apply_filter(*t1, cond1);
for (unsigned i = 0; i < conds.size(); ++i) {
apply_filter(*t1, conds[i].get());
}
t1->deallocate();
}
// filter_by_negation
// filter_interpreted_project
{
unsigned_vector remove;
remove.push_back(0);
remove.push_back(2);
t1 = mk_full(sig2);
for (unsigned i = 0; i < conds.size(); ++i) {
apply_filter_project(*t1, remove, conds[i].get());
}
remove[1] = 1;
for (unsigned i = 0; i < conds.size(); ++i) {
apply_filter_project(*t1, remove, conds[i].get());
}
t1->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());
rel_union union_fn = p.mk_union_fn(r, r, 0);
(*union_fn)(r, *full);
doc_manager& dm = r.get_dm();
SASSERT(r.get_udoc().size() == 1);
doc& d0 = r.get_udoc()[0];
SASSERT(dm.is_full(d0));
for (unsigned i = 0; i < num_vals; ++i) {
unsigned idx = m_rand(num_bits);
unsigned val = m_rand(2);
tbit b = (val == 0)?BIT_0:BIT_1;
dm.set(d0, idx, b);
}
}
void apply_filter_neg(udoc_relation& t1, udoc_relation& t2,
unsigned_vector const& cols1, unsigned_vector const& cols2) {
relation_signature const& sig = t1.get_signature();
scoped_ptr<datalog::relation_intersection_filter_fn> negf;
negf = p.mk_filter_by_negation_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr());
expr_ref fml1(m), fml2(m), fml3(m);
t1.to_formula(fml1);
t2.to_formula(fml2);
(*negf)(t1, t2);
t1.to_formula(fml3);
std::cout << fml1 << "\n";
std::cout << fml2 << "\n";
std::cout << fml3 << "\n";
expr_ref_vector eqs(m);
expr_ref_vector sub(m);
for (unsigned i = 0; i < sig.size(); ++i) {
sub.push_back(m.mk_var(i+sig.size(),sig[i]));
}
var_subst subst(m, false);
subst(fml2, sub.size(), sub.c_ptr(), fml2);
eqs.push_back(fml2);
for (unsigned i = 0; i < cols1.size(); ++i) {
var_ref v1(m), v2(m);
unsigned c1 = cols1[i];
unsigned c2 = cols2[i];
v1 = m.mk_var(c1, sig[c1]);
v2 = m.mk_var(sig.size() + c2, sig[c2]);
eqs.push_back(m.mk_eq(v1,v2));
}
fml2 = mk_and(m, eqs.size(), eqs.c_ptr());
for (unsigned i = 0; i < sub.size(); ++i) {
project_var(sig.size() + i, m.get_sort(sub[i].get()), fml2);
}
fml1 = m.mk_and(fml1, fml2);
expr_ref_vector vars(m);
for (unsigned i = 0; i < sig.size(); ++i) {
std::stringstream strm;
strm << "x" << i;
vars.push_back(m.mk_const(symbol(strm.str().c_str()), sig[i]));
}
subst(fml1, vars.size(), vars.c_ptr(), fml1);
subst(fml3, vars.size(), vars.c_ptr(), fml3);
check_equiv(fml1, fml3);
/*
tgt_1:={ x: x\in tgt_0 && ! \exists y:
( y \in neg & pi_c1(x)= pi_d1(y) & ... & pi_cN(x)= pi_dN(y) ) }
*/
}
expr_ref ex(unsigned hi, unsigned lo, expr* e) {
@ -334,6 +452,74 @@ public:
return result;
}
void apply_filter_project(udoc_relation& t, unsigned_vector const& rm, app* cond) {
scoped_ptr<datalog::relation_transformer_fn> rt;
rt = p.mk_filter_interpreted_and_project_fn(t, cond, rm.size(), rm.c_ptr());
udoc_relation* full = mk_full(t.get_signature());
rel_union union_fn = p.mk_union_fn(t, *full, 0);
(*union_fn)(t, *full, 0);
datalog::relation_base* result = (*rt)(t);
for (unsigned i = 0; i < rm.size(); ++i) {
std::cout << rm[i] << " ";
}
std::cout << mk_pp(cond, m) << "\n";
t.display(std::cout);
result->display(std::cout);
result->deallocate();
full->deallocate();
}
void verify_filter_project(udoc_relation const& r, unsigned_vector const& rm, app* cond) {
expr_ref fml(m), cfml(m);
r.to_formula(fml);
cfml = cond;
relation_signature const& sig = r.get_signature();
expr_ref_vector vars(m);
for (unsigned i = 0, j = 0, k = 0; i < sig.size(); ++i) {
if (j < rm.size() && rm[j] == i) {
project_var(i, sig[i], cfml);
++j;
}
else {
vars.push_back(m.mk_var(k, sig[i]));
++k;
}
}
check_equiv(fml, cfml);
}
void check_equiv(expr* fml1, expr* fml2) {
TRACE("doc", tout << mk_pp(fml1, m) << "\n";
tout << mk_pp(fml2, m) << "\n";);
smt_params fp;
smt::kernel solver(m, fp);
expr_ref tmp(m);
tmp = m.mk_not(m.mk_eq(fml1, fml2));
solver.assert_expr(tmp);
lbool res = solver.check();
SASSERT(res == l_false);
}
void project_var(unsigned i, sort* s, expr_ref& fml) {
var_ref v(m);
v = m.mk_var(i, s);
unsigned num_bits = bv.get_bv_size(s);
unsigned p = 1 << num_bits;
expr_ref_vector disj(m);
expr_ref tmp(m);
for (unsigned i = 0; i < p; ++i) {
expr_safe_replace repl(m);
repl.insert(v, bv.mk_numeral(rational(i), s));
tmp = fml;
repl(tmp);
disj.push_back(tmp);
}
fml = mk_or(m, disj.size(), disj.c_ptr());
}
void apply_filter(udoc_relation& t, app* cond) {
udoc_relation* full = mk_full(t.get_signature());
rel_union union_fn = p.mk_union_fn(t, *full, 0);