From 6a36116b5cd537e159a0fcc8f8e12d78d6f3cf0c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 9 Apr 2013 10:16:37 -0700
Subject: [PATCH] stash

---
 src/muz_qe/dl_compiler.cpp      |  7 ++++---
 src/muz_qe/dl_instruction.cpp   |  3 ++-
 src/muz_qe/dl_mk_magic_sets.cpp |  1 -
 src/muz_qe/dl_sparse_table.cpp  |  5 +++++
 src/muz_qe/dl_util.h            |  6 ++++++
 src/muz_qe/rel_context.cpp      | 17 ++++++++---------
 src/test/dl_query.cpp           | 13 +++++++++----
 7 files changed, 34 insertions(+), 18 deletions(-)

diff --git a/src/muz_qe/dl_compiler.cpp b/src/muz_qe/dl_compiler.cpp
index c898f7964..1bc39d213 100644
--- a/src/muz_qe/dl_compiler.cpp
+++ b/src/muz_qe/dl_compiler.cpp
@@ -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));
     }
diff --git a/src/muz_qe/dl_instruction.cpp b/src/muz_qe/dl_instruction.cpp
index 401a42e98..547752563 100644
--- a/src/muz_qe/dl_instruction.cpp
+++ b/src/muz_qe/dl_instruction.cpp
@@ -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)) {
diff --git a/src/muz_qe/dl_mk_magic_sets.cpp b/src/muz_qe/dl_mk_magic_sets.cpp
index 6885edc4e..e69be05da 100644
--- a/src/muz_qe/dl_mk_magic_sets.cpp
+++ b/src/muz_qe/dl_mk_magic_sets.cpp
@@ -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;
diff --git a/src/muz_qe/dl_sparse_table.cpp b/src/muz_qe/dl_sparse_table.cpp
index 1449b7d3d..dde09428f 100644
--- a/src/muz_qe/dl_sparse_table.cpp
+++ b/src/muz_qe/dl_sparse_table.cpp
@@ -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]);
         }
diff --git a/src/muz_qe/dl_util.h b/src/muz_qe/dl_util.h
index b313f0ae3..c3644cd74 100644
--- a/src/muz_qe/dl_util.h
+++ b/src/muz_qe/dl_util.h
@@ -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);
     }
diff --git a/src/muz_qe/rel_context.cpp b/src/muz_qe/rel_context.cpp
index 58263b9d0..da53d3983 100644
--- a/src/muz_qe/rel_context.cpp
+++ b/src/muz_qe/rel_context.cpp
@@ -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); );
diff --git a/src/test/dl_query.cpp b/src/test/dl_query.cpp
index 4dc770056..8e2e5402a 100644
--- a/src/test/dl_query.cpp
+++ b/src/test/dl_query.cpp
@@ -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";