mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +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 06:39:59 -07:00
parent 9116d38628
commit 53ac452253
1 changed files with 54 additions and 19 deletions
Download patch file Download diff file Expand all files Collapse all files

73
src/test/doc.cpp
View file

@ -1,4 +1,15 @@
#include "doc.h"
#include "trace.h"
#include "vector.h"
#include "ast.h"
#include "ast_pp.h"
#include "reg_decl_plugins.h"
#include "sorting_network.h"
#include "smt_kernel.h"
#include "model_smt2_pp.h"
#include "smt_params.h"
#include "ast_util.h"
static void tst_doc1(unsigned n) {
doc_manager m(n);
@ -18,9 +29,11 @@ static void tst_doc1(unsigned n) {
m.display(std::cout, *dX) << "\n";
m.display(std::cout, *d10) << "\n";
m.display(std::cout, *d20) << "\n";
unsigned hi = 3, lo = 1;
SASSERT(hi <= n);
doc_ref d111X(m, m.allocate(0xFF, hi, lo));
if (n < 64) {
unsigned hi = 3, lo = 1;
SASSERT(hi <= n);
doc_ref d111X(m, m.allocate(0xFF, hi, lo));
}
m.copy(*d, *d10);
SASSERT(m.equals(*d, *d10));
m.reset(*d);
@ -61,6 +74,7 @@ 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;
@ -70,7 +84,7 @@ static void tst_doc1(unsigned n) {
m.display(std::cout, *d1) << " -> ";
m1.display(std::cout, *d1_1) << "\n";
SASSERT(m1.equals(*d1_1,*d1_2));
#endif
}
@ -80,42 +94,60 @@ static void tst_doc1(unsigned n) {
// check that result is the same as QE over those clauses.
class test_doc_project {
random_gen m_ran;
int m_num_vars;
random_gen m_ran;
ast_manager m;
doc_manager dm;
expr_ref_vector m_vars;
unsigned choose_var() {
return m_ran(m_num_vars) + 1;
}
tbit choose_tbit() {
switch(m_ran(3)) {
switch (m_ran(3)) {
case 0: return BIT_0;
case 1: return BIT_1;
default : return BIT_x;
}
}
void mk_clause(svector<int>& clause, tbv& t) {
for (int i = 0; i < m_num_vars; ++i) {
void mk_clause(expr_ref& result, tbv& t) {
expr_ref_vector clause(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(-i-1); break;
case BIT_1: clause.push_back(i+1); break;
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;
default: break;
}
}
result = mk_or(m, clause.size(), clause.c_ptr());
}
void test_clauses(unsigned num_clauses) {
doc_ref d(dm, dm.allocateX());
expr_ref_vector fmls(m);
expr_ref fml(m);
for (unsigned i = 0; i < num_clauses; ++i) {
expr_ref clause(m);
tbv* t = dm.tbvm().allocate();
mk_clause(clause, *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";
//
}
public:
test_doc_project(unsigned num_vars): m_num_vars(num_vars) {}
test_doc_project(unsigned num_vars): dm(num_vars), m_vars(m) {
reg_decl_plugins(m);
for (unsigned i = 0; i < num_vars; ++i) {
m_vars.push_back(m.mk_fresh_const("b", m.mk_bool_sort()));
}
}
void operator()(unsigned min_clauses, unsigned max_clauses) {
for (unsigned i = min_clauses; i < max_clauses; ++i) {
test_clauses(i);
void operator()(unsigned num_rounds, unsigned num_clauses) {
for (unsigned i = 0; i < num_rounds; ++i) {
test_clauses(num_clauses);
}
}
};
@ -124,4 +156,7 @@ void tst_doc() {
tst_doc1(5);
tst_doc1(10);
tst_doc1(70);
test_doc_project tp(4);
tp(5,7);
}