[datalog] merge changes from the hassel branch

Signed-off-by: Nuno Lopes <t-nclaud@microsoft.com>

src/muz_qe/dl_check_table.h

@@ -89,15 +89,6 @@ namespace datalog {
 
     class check_table : public table_base {
         friend class check_table_plugin;
-        friend class check_table_plugin::join_fn;
-        friend class check_table_plugin::union_fn;
-        friend class check_table_plugin::transformer_fn;
-        friend class check_table_plugin::rename_fn;
-        friend class check_table_plugin::project_fn;
-        friend class check_table_plugin::filter_equal_fn;
-        friend class check_table_plugin::filter_identical_fn;
-        friend class check_table_plugin::filter_interpreted_fn;
-        friend class check_table_plugin::filter_by_negation_fn;
 
         table_base* m_checker;
         table_base* m_tocheck;

src/muz_qe/dl_compiler.cpp

@@ -421,6 +421,7 @@ namespace datalog {
     void compiler::compile_rule_evaluation_run(rule * r, reg_idx head_reg, const reg_idx * tail_regs, 
             reg_idx delta_reg, bool use_widening, instruction_block & acc) {
         
+        ast_manager & m = m_context.get_manager();
         m_instruction_observer.start_rule(r);
 
         const app * h = r->get_head();
@@ -433,7 +434,7 @@ namespace datalog {
         SASSERT(pt_len<=2); //we require rules to be processed by the mk_simple_joins rule transformer plugin
 
         reg_idx single_res;
-        ptr_vector<expr> single_res_expr;
+        expr_ref_vector single_res_expr(m);
 
         //used to save on filter_identical instructions where the check is already done 
         //by the join operation
@@ -536,7 +537,7 @@ namespace datalog {
             unsigned srlen=single_res_expr.size();
             SASSERT((single_res==execution_context::void_register) ? (srlen==0) : (srlen==m_reg_signatures[single_res].size()));
             for(unsigned i=0; i<srlen; i++) {
-                expr * exp = single_res_expr[i];
+                expr * exp = single_res_expr[i].get();
                 if(is_app(exp)) {
                     SASSERT(m_context.get_decl_util().is_numeral_ext(exp));
                     relation_element value = to_app(exp);
@@ -622,9 +623,8 @@ namespace datalog {
         unsigned ft_len=r->get_tail_size(); //full tail
         for(unsigned tail_index=ut_len; tail_index<ft_len; tail_index++) {
             app * t = r->get_tail(tail_index);
-            var_idx_set t_vars;
+            ptr_vector<sort> t_vars;
-            ast_manager & m = m_context.get_manager();
+            ::get_free_vars(t, t_vars);
-            collect_vars(m, t, t_vars);
             
             if(t_vars.empty()) {
                 expr_ref simplified(m);
@@ -639,40 +639,23 @@ namespace datalog {
             }
 
             //determine binding size
-            unsigned max_var=0;
+            while (!t_vars.back()) {
-            var_idx_set::iterator vit = t_vars.begin();
+                t_vars.pop_back();
-            var_idx_set::iterator vend = t_vars.end();
-            for(; vit!=vend; ++vit) {
-                unsigned v = *vit;
-                if(v>max_var) { max_var = v; }
             }
+            unsigned max_var = t_vars.size();
 
             //create binding
             expr_ref_vector binding(m);
             binding.resize(max_var+1);
-            vit = t_vars.begin();
+            
-            for(; vit!=vend; ++vit) {
+            for(unsigned v = 0; v < t_vars.size(); ++v) {
-                unsigned v = *vit;
+                if (!t_vars[v]) {
+                    continue;
+                }
                 int2ints::entry * e = var_indexes.find_core(v);
                 if(!e) {
                     //we have an unbound variable, so we add an unbound column for it
-                    relation_sort unbound_sort = 0;
+                    relation_sort unbound_sort = t_vars[v];
-
-                    for(unsigned hindex = 0; hindex<head_len; hindex++) {
-                        expr * harg = h->get_arg(hindex);
-                        if(!is_var(harg) || to_var(harg)->get_idx()!=v) {
-                            continue;
-                        }
-                        unbound_sort = to_var(harg)->get_sort();
-                    }
-                    if(!unbound_sort) {
-                        // the variable in the interpreted tail is neither bound in the 
-                        // uninterpreted tail nor present in the head
-                        std::stringstream sstm;
-                        sstm << "rule with unbound variable #" << v << " in interpreted tail: ";                       
-                        r->display(m_context, sstm);
-                        throw default_exception(sstm.str());
-                    }
 
                     reg_idx new_reg;
                     TRACE("dl", tout << mk_pp(head_pred, m_context.get_manager()) << "\n";);
@@ -759,7 +742,7 @@ namespace datalog {
         m_instruction_observer.finish_rule();
     }
 
-    void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr, 
+    void compiler::add_unbound_columns_for_negation(rule* r, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr, 
                                                     bool & dealloc, instruction_block & acc) {
         uint_set pos_vars;
         u_map<expr*> neg_vars;
@@ -782,7 +765,7 @@ namespace datalog {
         }
         // populate positive variables:
         for (unsigned i = 0; i < single_res_expr.size(); ++i) {
-            expr* e = single_res_expr[i];
+            expr* e = single_res_expr[i].get();
             if (is_var(e)) {
                 pos_vars.insert(to_var(e)->get_idx());
             }

src/muz_qe/dl_compiler.h

@@ -177,7 +177,7 @@ namespace datalog {
         void make_full_relation(func_decl* pred, const relation_signature & sig, reg_idx & result, 
             instruction_block & acc);
 
-        void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, ptr_vector<expr>& single_res_expr,
+        void add_unbound_columns_for_negation(rule* compiled_rule, func_decl* pred, reg_idx& single_res, expr_ref_vector& single_res_expr,
                                               bool & dealloc, instruction_block& acc);
         
         void make_duplicate_column(reg_idx src, unsigned col, reg_idx & result, instruction_block & acc);

src/muz_qe/dl_context.cpp

@@ -823,7 +823,14 @@ namespace datalog {
         if (similarity_compressor()) {
             m_transf.register_plugin(alloc(mk_similarity_compressor, *this)); 
         }
-        m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
+        m_transf.register_plugin(alloc(mk_partial_equivalence_transformer, *this));
+        m_transf.register_plugin(alloc(mk_rule_inliner, *this));
+        m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this));
+
+        if (get_params().bit_blast()) {
+            m_transf.register_plugin(alloc(mk_bit_blast, *this, 22000));
+            m_transf.register_plugin(alloc(mk_interp_tail_simplifier, *this, 21000));
+        }
 
         transform_rules(m_transf);
     }

src/muz_qe/dl_relation_manager.cpp

@@ -740,7 +740,6 @@ namespace datalog {
     relation_transformer_fn * relation_manager::mk_select_equal_and_project_fn(const relation_base & t, 
             const relation_element & value, unsigned col) { 
         relation_transformer_fn * res = t.get_plugin().mk_select_equal_and_project_fn(t, value, col);
-        TRACE("dl", tout << t.get_plugin().get_name() << " " << value << " " << col << "\n";);
         if(!res) {
             relation_mutator_fn * selector = mk_filter_equal_fn(t, value, col);
             if(selector) {

src/muz_qe/dl_util.h

@@ -207,7 +207,9 @@ namespace datalog {
         static unsigned expr_cont_get_size(app * a) { return a->get_num_args(); }
         static expr * expr_cont_get(app * a, unsigned i) { return a->get_arg(i); }
         static unsigned expr_cont_get_size(const ptr_vector<expr> & v) { return v.size(); }
+        static unsigned expr_cont_get_size(const expr_ref_vector & v) { return v.size(); }
         static expr * expr_cont_get(const ptr_vector<expr> & v, unsigned i) { return v[i]; }
+        static expr * expr_cont_get(const expr_ref_vector & v, unsigned i) { return v[i]; }
     public:
         variable_intersection(ast_manager & m) : m_consts(m) {}