mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 17:15:31 +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 05:52:09 -07:00
parent 2a00f2b38c
commit 9a3a1835cc
3 changed files with 78 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

32
src/test/doc.cpp
View file

@ -73,15 +73,41 @@ static void tst_doc1(unsigned n) {
class test_doc_project {
random_gen m_ran;
int m_num_vars;
void test_clauses(unsigned num_vars, unsigned num_clauses) {
unsigned choose_var() {
return m_ran(m_num_vars) + 1;
}
tbit choose_tbit() {
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) {
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;
default: break;
}
}
}
void test_clauses(unsigned num_clauses) {
//
}
public:
void operator()(unsigned num_vars, unsigned min_clauses, unsigned max_clauses) {
test_doc_project(unsigned num_vars): m_num_vars(num_vars) {}
void operator()(unsigned min_clauses, unsigned max_clauses) {
for (unsigned i = min_clauses; i < max_clauses; ++i) {
test_clauses(num_vars, i);
test_clauses(i);
}
}
};