add transformation to reduce overhead of negation for predicates with free variables

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

src/muz/base/dl_context.cpp

@@ -232,6 +232,7 @@ namespace datalog {
 
     context::~context() {
         reset();
+        dealloc(m_params);        
     }
 
     void context::reset() {

src/muz/rel/rel_context.cpp

@@ -46,6 +46,7 @@ Revision History:
 #include"dl_mk_rule_inliner.h"
 #include"dl_mk_interp_tail_simplifier.h"
 #include"dl_mk_bit_blast.h"
+#include"dl_mk_separate_negated_tails.h"
 #include"fixedpoint_params.hpp"
 
 
@@ -281,6 +282,7 @@ namespace datalog {
         transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context));
         transf.register_plugin(alloc(mk_rule_inliner, m_context));
         transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context));
+        transf.register_plugin(alloc(mk_separate_negated_tails, m_context));
 
         if (m_context.get_params().bit_blast()) {
             transf.register_plugin(alloc(mk_bit_blast, m_context, 22000));

src/muz/transforms/dl_mk_separate_negated_tails.cpp

@@ -0,0 +1,119 @@
+
+#include "dl_mk_separate_negated_tails.h"
+#include "dl_context.h"
+
+namespace datalog {
+
+    mk_separate_negated_tails::mk_separate_negated_tails(context& ctx, unsigned priority):
+        plugin(priority),
+        m(ctx.get_manager()),
+        rm(ctx.get_rule_manager()),
+        m_ctx(ctx)
+    {}
+
+    bool mk_separate_negated_tails::has_private_vars(rule const& r, unsigned j) {
+        get_private_vars(r, j);
+        return !m_vars.empty();
+    }
+
+    void mk_separate_negated_tails::get_private_vars(rule const& r, unsigned j) {
+        m_vars.reset();
+        m_fv.reset();
+        get_free_vars(r.get_head(), m_fv);
+        for (unsigned i = 0; i < r.get_tail_size(); ++i) {
+            if (i != j) {
+                get_free_vars(r.get_tail(i), m_fv);
+            }
+        }
+        
+        app* p = r.get_tail(j);
+        for (unsigned i = 0; i < p->get_num_args(); ++i) {
+            expr* v = p->get_arg(i);
+            if (is_var(v)) {
+                unsigned idx = to_var(v)->get_idx();
+                if (idx >= m_fv.size() || !m_fv[idx]) {
+                    m_vars.push_back(v);
+                }
+            }
+        }
+    }
+
+    void mk_separate_negated_tails::abstract_predicate(app* p, app_ref& q, rule_set& rules) {
+        expr_ref_vector args(m);
+        sort_ref_vector sorts(m);
+        func_decl_ref fn(m);
+        for (unsigned i = 0; i < p->get_num_args(); ++i) {
+            expr* arg = p->get_arg(i);
+            if (!m_vars.contains(arg)) {
+                args.push_back(arg);
+                sorts.push_back(m.get_sort(arg));
+            }
+        }
+        fn = m.mk_fresh_func_decl(p->get_decl()->get_name(), symbol("N"), sorts.size(), sorts.c_ptr(), m.mk_bool_sort());
+        m_ctx.register_predicate(fn, false);
+        q = m.mk_app(fn, args.size(), args.c_ptr());
+        bool is_neg = true;
+        rules.add_rule(rm.mk(q, 1, & p, &is_neg));
+    }
+
+    void mk_separate_negated_tails::create_rule(rule const&r, rule_set& rules) {
+        unsigned utsz = r.get_uninterpreted_tail_size();
+        unsigned ptsz = r.get_positive_tail_size();
+        unsigned tsz  = r.get_tail_size();
+        app_ref_vector tail(m);
+        app_ref p(m);
+        svector<bool> neg;
+        for (unsigned i = 0; i < ptsz; ++i) {
+            tail.push_back(r.get_tail(i));
+            neg.push_back(false);
+        }
+        for (unsigned i = ptsz; i < utsz; ++i) {
+            get_private_vars(r, i);
+            if (!m_vars.empty()) {
+                abstract_predicate(r.get_tail(i), p, rules);
+                tail.push_back(p);
+                neg.push_back(false);
+            }
+            else {
+                neg.push_back(true);
+                tail.push_back(r.get_tail(i));
+            }
+        }
+        for (unsigned i = utsz; i < tsz; ++i) {
+            tail.push_back(r.get_tail(i));
+            neg.push_back(false);
+        }
+        rules.add_rule(rm.mk(r.get_head(), tail.size(), tail.c_ptr(), neg.c_ptr(), r.name()));
+    }
+    
+    rule_set * mk_separate_negated_tails::operator()(rule_set const& src) {
+        scoped_ptr<rule_set> result = alloc(rule_set, m_ctx);
+        bool has_new_rule = false;
+        unsigned sz = src.get_num_rules();
+        for (unsigned i = 0; i < sz; ++i) {            
+            bool change = false;
+            rule & r = *src.get_rule(i);
+            unsigned utsz = r.get_uninterpreted_tail_size();
+            unsigned ptsz = r.get_positive_tail_size();
+            for (unsigned j = ptsz; j < utsz; ++j) {
+                SASSERT(r.is_neg_tail(j));
+                if (has_private_vars(r, j)) {
+                    create_rule(r, *result);
+                    has_new_rule = true;
+                    change = true;
+                    break;
+                }
+            }
+            if (!change) {
+                result->add_rule(&r);
+            }
+        }
+        if (!has_new_rule) {
+            return 0;
+        }
+        else {
+            result->inherit_predicates(src);
+            return result.detach();
+        }
+    }
+}

src/muz/transforms/dl_mk_separate_negated_tails.h

@@ -0,0 +1,61 @@
+/*++
+Copyright (c) 2006 Microsoft Corporation
+
+Module Name:
+
+    mk_separate_negated_tails.h
+
+Abstract:
+
+    Rule transformer which creates new rules for predicates
+    in negated tails that use free variables not used
+    elsewhere. These free variables incur an overhead
+    on the instructions compiled using dl_compiler.
+
+    Consider the following transformations:
+
+       P(x)    :- Exists y, z, u . Q(x,y), !R(y,z), !T(z,u).
+    => 
+       P(x)    :- Exists y, z . Q(x,y), !R(y,z), Exists u . ! T(z,u).
+    => 
+       P(x)    :- Exists y, z . Q(x,y), !R(y,z), TN(z).
+       TN(z)   :- !T(z,u).
+
+
+
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-09-09
+
+Revision History:
+
+--*/
+
+#ifndef _DL_MK_SEPARAT_NEGATED_TAILS_H_
+#define _DL_MK_SEPARAT_NEGATED_TAILS_H_
+
+#include "dl_rule_transformer.h"
+#include "dl_context.h"
+
+namespace datalog {
+
+    class mk_separate_negated_tails : public rule_transformer::plugin {
+        ast_manager & m;
+        rule_manager& rm;
+        context &     m_ctx;
+        ptr_vector<expr> m_vars;
+        ptr_vector<sort> m_fv;
+        
+        bool has_private_vars(rule const& r, unsigned j);
+        void get_private_vars(rule const& r, unsigned j);
+        void abstract_predicate(app* p, app_ref& q, rule_set& rules);
+        void create_rule(rule const&r, rule_set& rules);
+
+    public:
+        mk_separate_negated_tails(context& ctx, unsigned priority = 21000);
+        rule_set * operator()(rule_set const & source);
+    };
+}
+
+#endif

src/muz/transforms/dl_mk_subsumption_checker.h

@@ -84,7 +84,7 @@ namespace datalog {
             reset_dealloc_values(m_ground_unconditional_rule_heads);
         }
 
-        rule_set * operator()(rule_set const & source);
+        virtual rule_set * operator()(rule_set const & source);
     };
 
 };