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

stash

Browse source
This commit is contained in:
Nikolaj Bjorner 2013-04-09 10:16:37 -07:00
parent 75ad174567
commit 6a36116b5c
7 changed files with 34 additions and 18 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/muz_qe/dl_compiler.cpp
View file

@ -61,13 +61,14 @@ namespace datalog {
void compiler::make_join_project(reg_idx t1, reg_idx t2, const variable_intersection & vars,
const unsigned_vector & removed_cols, reg_idx & result, instruction_block & acc) {
relation_signature aux_sig;
relation_signature::from_join(m_reg_signatures[t1], m_reg_signatures[t2], vars.size(),
vars.get_cols1(), vars.get_cols2(), aux_sig);
relation_signature sig1 = m_reg_signatures[t1];
relation_signature sig2 = m_reg_signatures[t2];
relation_signature::from_join(sig1, sig2, vars.size(), vars.get_cols1(), vars.get_cols2(), aux_sig);
relation_signature res_sig;
relation_signature::from_project(aux_sig, removed_cols.size(), removed_cols.c_ptr(),
res_sig);
result = get_fresh_register(res_sig);
acc.push_back(instruction::mk_join_project(t1, t2, vars.size(), vars.get_cols1(),
vars.get_cols2(), removed_cols.size(), removed_cols.c_ptr(), result));
}

3
src/muz_qe/dl_instruction.cpp
View file

@ -723,7 +723,8 @@ namespace datalog {
instr_join_project(reg_idx rel1, reg_idx rel2, unsigned joined_col_cnt, const unsigned * cols1,
const unsigned * cols2, unsigned removed_col_cnt, const unsigned * removed_cols, reg_idx result)
: m_rel1(rel1), m_rel2(rel2), m_cols1(joined_col_cnt, cols1),
m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols), m_res(result) {}
m_cols2(joined_col_cnt, cols2), m_removed_cols(removed_col_cnt, removed_cols), m_res(result) {
}
virtual bool perform(execution_context & ctx) {
ctx.make_empty(m_res);
if (!ctx.reg(m_rel1) || !ctx.reg(m_rel2)) {

1
src/muz_qe/dl_mk_magic_sets.cpp
View file

@ -318,7 +318,6 @@ namespace datalog {
}
rule_set * mk_magic_sets::operator()(rule_set const & source) {
SASSERT(!m_context.get_model_converter());
unsigned init_rule_cnt = source.get_num_rules();
{
func_decl_set intentional;

5
src/muz_qe/dl_sparse_table.cpp
View file

@ -500,6 +500,11 @@ namespace datalog {
char * reserve = m_data.get_reserve_ptr();
unsigned col_cnt = m_column_layout.size();
for(unsigned i=0; i<col_cnt; i++) {
if (f[i] >= get_signature()[i]) {
std::cout << "***************************\n";
std::cout << f[i] << " " << get_signature()[i] << "\n";
} //the value fits into the table signature
SASSERT(f[i]<get_signature()[i]); //the value fits into the table signature
m_column_layout.set(reserve, i, f[i]);
}

6
src/muz_qe/dl_util.h
View file

@ -316,6 +316,12 @@ namespace datalog {
}
container[i-ofs] = container[i];
}
if (r_i != removed_col_cnt) {
for (unsigned i = 0; i < removed_col_cnt; ++i) {
std::cout << removed_cols[i] << " ";
}
std::cout << " container size: " << n << "\n";
}
SASSERT(r_i==removed_col_cnt);
container.resize(n-removed_col_cnt);
}

17
src/muz_qe/rel_context.cpp
View file

@ -87,30 +87,29 @@ namespace datalog {
lbool rel_context::saturate() {
m_context.ensure_closed();
m_context.ensure_closed();
bool time_limit = m_context.soft_timeout()!=0;
unsigned remaining_time_limit = m_context.soft_timeout();
unsigned restart_time = m_context.initial_restart_timeout();
unsigned restart_time = m_context.initial_restart_timeout();
rule_set original_rules(m_context.get_rules());
decl_set original_predicates;
m_context.collect_predicates(original_predicates);
m_code.reset();
m_context.collect_predicates(original_predicates);
instruction_block termination_code;
m_ectx.reset();
lbool result;
TRACE("dl", m_context.display(tout););
while (true) {
m_code.reset();
m_ectx.reset();
termination_code.reset();
m_context.transform_rules();
if (m_context.canceled()) {
result = l_undef;
break;
}
TRACE("dl", m_context.display(tout););
compiler::compile(m_context, m_context.get_rules(), m_code, termination_code);
TRACE("dl", m_code.display(*this, tout); );

13
src/test/dl_query.cpp
View file

@ -48,6 +48,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
bool use_magic_sets) {
dl_decl_util decl_util(m);
random_gen ran(0);
context ctx_q(m, fparams);
params.set_bool("magic_sets_for_queries", use_magic_sets);
@ -86,7 +87,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
warning_msg("cannot get sort size");
return;
}
uint64 num = rand()%sort_sz;
uint64 num = ran()%sort_sz;
app * el_b = decl_util.mk_numeral(num, sig_b[col]);
f_b.push_back(el_b);
app * el_q = decl_util.mk_numeral(num, sig_q[col]);
@ -112,7 +113,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
table_base::iterator fit = table_b.begin();
table_base::iterator fend = table_b.end();
for(; fit!=fend; ++fit) {
if(rand()%std::max(1u,table_sz/test_count)!=0) {
if(ran()%std::max(1u,table_sz/test_count)!=0) {
continue;
}
fit->get_fact(tf);
@ -127,6 +128,7 @@ void dl_query_test(ast_manager & m, smt_params & fparams, params_ref& params,
void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
params.set_bool("magic_sets_for_queries", true);
ast_manager m;
random_gen ran(0);
reg_decl_plugins(m);
arith_util arith(m);
const char * problem_dir = "C:\\tvm\\src\\z3_2\\debug\\test\\w0.datalog";
@ -151,8 +153,8 @@ void dl_query_test_wpa(smt_params & fparams, params_ref& params) {
TRUSTME( ctx.try_get_sort_constant_count(var_sort, var_sz) );
for(unsigned attempt=0; attempt<attempts; attempt++) {
unsigned el1 = rand()%var_sz;
unsigned el2 = rand()%var_sz;
unsigned el1 = ran()%var_sz;
unsigned el2 = ran()%var_sz;
expr_ref_vector q_args(m);
q_args.push_back(dl_util.mk_numeral(el1, var_sort));
@ -218,6 +220,9 @@ void tst_dl_query() {
for(unsigned use_magic_sets=0; use_magic_sets<=1; use_magic_sets++) {
stopwatch watch;
if (!(use_restarts == 1 && use_similar == 0 && use_magic_sets == 1)) {
continue;
}
watch.start();
std::cerr << "------- " << (use_restarts ? "With" : "Without") << " restarts -------\n";
std::cerr << "------- " << (use_similar ? "With" : "Without") << " similar compressor -------\n";