optmizing DL

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

src/muz_qe/dl_rule.cpp

@@ -41,6 +41,7 @@ Revision History:
 #include"quant_hoist.h"
 #include"expr_replacer.h"
 #include"bool_rewriter.h"
+#include"qe_lite.h"
 
 namespace datalog {
 
@@ -613,14 +614,67 @@ namespace datalog {
         return r;
     }
 
+    void rule_manager::reduce_unbound_vars(rule_ref& r) {
+        unsigned ut_len = r->get_uninterpreted_tail_size();
+        unsigned t_len = r->get_tail_size();
+        ptr_vector<sort> vars;
+        uint_set index_set;
+        qe_lite qe(m);
+        expr_ref_vector conjs(m);
+
+        if (ut_len == t_len) {
+            return;
+        }
+
+        get_free_vars(r->get_head(), vars);
+        for (unsigned i = 0; i < ut_len; ++i) {
+            get_free_vars(r->get_tail(i), vars);
+        }
+        for (unsigned i = ut_len; i < t_len; ++i) {
+            conjs.push_back(r->get_tail(i));
+        }
+
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            if (vars[i]) {
+                index_set.insert(i);
+            }
+        }
+        qe(index_set, false, conjs);
+        bool change = conjs.size() != t_len - ut_len;
+        for (unsigned i = 0; !change && i < conjs.size(); ++i) {
+            change = r->get_tail(ut_len+i) != conjs[i].get();
+        }
+        if (change) {
+            app_ref_vector tail(m);
+            svector<bool> tail_neg;
+            for (unsigned i = 0; i < ut_len; ++i) {
+                tail.push_back(r->get_tail(i));
+                tail_neg.push_back(r->is_neg_tail(i));
+            }
+            for (unsigned i = 0; i < conjs.size(); ++i) {
+                tail.push_back(ensure_app(conjs[i].get()));
+            }
+            tail_neg.resize(tail.size(), false);
+            IF_VERBOSE(1, r->display(m_ctx, verbose_stream() << "reducing rule\n"););
+            r = mk(r->get_head(), tail.size(), tail.c_ptr(), tail_neg.c_ptr());
+            IF_VERBOSE(1, r->display(m_ctx, verbose_stream() << "reduced rule\n"););
+            TRACE("dl", r->display(m_ctx, tout << "reduced rule\n"););
+        }
+    }
+
     void rule_manager::fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination) {
 
+        reduce_unbound_vars(r);
+
         if (!m_ctx.fix_unbound_vars()) {
             return;
         }
 
-        if (r->get_uninterpreted_tail_size() == r->get_tail_size()) {
+        unsigned ut_len = r->get_uninterpreted_tail_size();
-            //no interpreted tail to fix
+        unsigned t_len = r->get_tail_size();
+
+        if (ut_len == t_len) {
+            // no interpreted tail to fix
             return;
         }
 
@@ -633,7 +687,7 @@ namespace datalog {
         get_free_vars(r, free_rule_vars);
         vctr.count_vars(m, head);
 
-        unsigned ut_len = r->get_uninterpreted_tail_size();
+
         for (unsigned i = 0; i < ut_len; i++) {
             app * t = r->get_tail(i);
             vctr.count_vars(m, t);
@@ -642,11 +696,9 @@ namespace datalog {
         }
 
         ptr_vector<sort> interp_vars;
-        //var_idx_set interp_vars;
         var_idx_set unbound_vars;
         expr_ref_vector tails_with_unbound(m);
 
-        unsigned t_len = r->get_tail_size();
         for (unsigned i = ut_len; i < t_len; i++) {
             app * t = r->get_tail(i);
             interp_vars.reset();

src/muz_qe/dl_rule.h

@@ -83,6 +83,11 @@ namespace datalog {
 
         unsigned hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
 
+        /**
+           \brief Perform cheap quantifier elimination to reduce the number of variables in the interpreted tail.
+         */
+        void reduce_unbound_vars(rule_ref& r);
+
     public:
 
         ast_manager& get_manager() const { return m; }
@@ -127,6 +132,7 @@ namespace datalog {
         void fix_unbound_vars(rule_ref& r, bool try_quantifier_elimination);
 
 
+
         /**
            \brief apply substitution to variables of rule.
         */

src/muz_qe/pdr_context.cpp

@@ -1825,6 +1825,7 @@ namespace pdr {
             ++m_stats.m_num_nodes;
             m_search.add_leaf(*child); 
             IF_VERBOSE(2, verbose_stream() << "Predecessor: " << mk_pp(o_cube, m) << "\n";);
+            m_stats.m_max_depth = std::max(m_stats.m_max_depth, child->depth());
         }
         check_pre_closed(n);
         TRACE("pdr", m_search.display(tout););

src/muz_qe/pdr_context.h

@@ -175,21 +175,25 @@ namespace pdr {
         expr_ref               m_state;
         model_ref              m_model;
         ptr_vector<model_node> m_children;
-        unsigned               m_level;
+        unsigned               m_level;       
         unsigned               m_orig_level;
+        unsigned               m_depth;
         bool                   m_closed;
     public:
         model_node(model_node* parent, expr_ref& state, pred_transformer& pt, unsigned level):
-            m_parent(parent), m_pt(pt), m_state(state), m_model(0), m_level(level), m_orig_level(level), m_closed(false) {
+            m_parent(parent), m_pt(pt), m_state(state), m_model(0), 
+                m_level(level), m_orig_level(level), m_depth(0), m_closed(false) {
             if (m_parent) {
                 m_parent->m_children.push_back(this);
                 SASSERT(m_parent->m_level == level+1);
                 SASSERT(m_parent->m_level > 0);
+                m_depth = m_parent->m_depth+1;
             }
         }
         void set_model(model_ref& m) { m_model = m; }
         unsigned level() const { return m_level; }
         unsigned orig_level() const { return m_orig_level; }
+        unsigned depth() const { return m_depth; }
         void     increase_level() { ++m_level; }
         expr*    state() const { return m_state; }
         ptr_vector<model_node> const& children() { return m_children; }

src/muz_qe/qe_lite.h

@@ -22,6 +22,7 @@ Revision History:
 #define __QE_LITE_H__
 
 #include "ast.h"
+#include "uint_set.h"
 
 class qe_lite {
     class impl;
@@ -40,6 +41,17 @@ public:
     */
     void operator()(app_ref_vector& vars, expr_ref& fml);
 
+    /**
+       \brief
+       Apply light-weight quantifier elimination to variables present/absent in the index set.
+       If 'index_of_bound' is true, then the index_set is treated as the set of
+       bound variables. if 'index_of_bound' is false, then index_set is treated as the
+       set of variables that are not bound (variables that are not in the index set are bound).
+     */
+    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref& fml);
+
+    void operator()(uint_set const& index_set, bool index_of_bound, expr_ref_vector& conjs);
+
     /**
         \brief full rewriting based light-weight quantifier elimination round.
     */