move quantifier hoist routines to quant_hoist

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

src/ast/rewriter/ast_counter.cpp

@@ -0,0 +1,165 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    ast_counter.cpp
+
+Abstract:
+
+    Routines for counting features of terms, such as free variables.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-18.
+
+Revision History:
+
+--*/
+
+#include "ast_counter.h"
+#include "var_subst.h"
+
+void counter::update(unsigned el, int delta) {
+    int & counter = get(el);
+    SASSERT(!m_stay_non_negative || counter>=0);
+    SASSERT(!m_stay_non_negative || static_cast<int>(counter)>=-delta);
+    counter += delta;
+}
+
+int & counter::get(unsigned el) {
+    return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
+}
+
+counter & counter::count(unsigned sz, const unsigned * els, int delta) {
+    for(unsigned i=0; i<sz; i++) {
+        update(els[i], delta);
+    }
+    return *this;
+}
+
+unsigned counter::get_positive_count() const {
+    unsigned cnt = 0;
+    iterator eit = begin();
+    iterator eend = end();
+    for(; eit!=eend; ++eit) {
+        if( eit->m_value>0 ) { 
+            cnt++;
+        }
+    }
+    return cnt;
+}
+
+void counter::collect_positive(uint_set & acc) const {
+    iterator eit = begin();
+    iterator eend = end();
+    for(; eit!=eend; ++eit) {
+        if(eit->m_value>0) { acc.insert(eit->m_key); }
+    }
+}
+
+bool counter::get_max_positive(unsigned & res) const {
+    bool found = false;
+    iterator eit = begin();
+    iterator eend = end();
+    for(; eit!=eend; ++eit) {
+        if( eit->m_value>0 && (!found || eit->m_key>res) ) { 
+            found = true;
+            res = eit->m_key;
+        }
+    }
+    return found;
+}
+
+unsigned counter::get_max_positive() const {
+    unsigned max_pos;
+    VERIFY(get_max_positive(max_pos));
+    return max_pos;
+}
+
+int counter::get_max_counter_value() const {
+    int res = 0;
+    iterator eit = begin();
+    iterator eend = end();
+    for (; eit!=eend; ++eit) {
+        if( eit->m_value>res ) { 
+            res = eit->m_value;
+        }
+    }
+    return res;
+}
+
+void var_counter::count_vars(ast_manager & m, const app * pred, int coef) {
+    unsigned n = pred->get_num_args();
+    for (unsigned i = 0; i < n; i++) {
+        m_sorts.reset();
+        ::get_free_vars(pred->get_arg(i), m_sorts);
+        for (unsigned j = 0; j < m_sorts.size(); ++j) {
+            if (m_sorts[j]) {
+                update(j, coef);
+            }
+        }
+    }
+}
+
+
+unsigned var_counter::get_max_var(bool& has_var) {
+    has_var = false;
+    unsigned max_var = 0;
+    while (!m_todo.empty()) {
+        expr* e = m_todo.back();
+        unsigned scope = m_scopes.back();
+        m_todo.pop_back();
+        m_scopes.pop_back();
+        if (m_visited.is_marked(e)) {
+            continue;
+        }
+        m_visited.mark(e, true);
+        switch(e->get_kind()) {
+        case AST_QUANTIFIER: {
+            quantifier* q = to_quantifier(e);
+            m_todo.push_back(q->get_expr());
+            m_scopes.push_back(scope + q->get_num_decls());
+            break;                 
+        }
+        case AST_VAR: {
+            if (to_var(e)->get_idx() >= scope + max_var) {
+                has_var = true;
+                max_var = to_var(e)->get_idx() - scope;
+            }
+            break;
+        }
+        case AST_APP: {
+            app* a = to_app(e);
+            for (unsigned i = 0; i < a->get_num_args(); ++i) {
+                m_todo.push_back(a->get_arg(i));
+                m_scopes.push_back(scope);                    
+            }
+            break;
+        }
+        default:
+            UNREACHABLE();
+            break;
+        }
+    }
+    m_visited.reset();
+    return max_var;
+}
+
+
+unsigned var_counter::get_max_var(expr* e) {
+    bool has_var = false;
+    m_todo.push_back(e);
+    m_scopes.push_back(0);
+    return get_max_var(has_var);
+}
+
+unsigned var_counter::get_next_var(expr* e) {
+    bool has_var = false;
+    m_todo.push_back(e);
+    m_scopes.push_back(0);
+    unsigned mv = get_max_var(has_var);
+    if (has_var) mv++;
+    return mv;
+}
+

src/ast/rewriter/ast_counter.h

@@ -0,0 +1,107 @@
+/*++
+Copyright (c) 2013 Microsoft Corporation
+
+Module Name:
+
+    ast_counter.h
+
+Abstract:
+
+    Routines for counting features of terms, such as free variables.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2013-03-18.
+    Krystof Hoder (t-khoder) 2010-10-10.
+
+Revision History:
+
+    Hoisted from dl_util.h 2013-03-18.
+
+--*/
+
+
+#ifndef _AST_COUNTER_H_
+#define _AST_COUNTER_H_
+
+#include "ast.h"
+#include "map.h"
+#include "uint_set.h"
+
+class counter {
+protected:
+    typedef u_map<int> map_impl;
+    map_impl m_data;
+    const bool m_stay_non_negative;
+public:
+    typedef map_impl::iterator iterator;
+    
+    counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    
+    iterator begin() const { return m_data.begin(); }
+    iterator end() const { return m_data.end(); }    
+    void update(unsigned el, int delta);
+    int & get(unsigned el);
+
+    /**
+       \brief Increase values of elements in \c els by \c delta.
+       
+       The function returns a reference to \c *this to allow for expressions like
+       counter().count(sz, arr).get_positive_count()
+    */
+    counter & count(unsigned sz, const unsigned * els, int delta = 1);
+    counter & count(const unsigned_vector & els, int delta = 1) {
+        return count(els.size(), els.c_ptr(), delta);
+    }
+    
+    void collect_positive(uint_set & acc) const;
+    unsigned get_positive_count() const;
+
+    bool get_max_positive(unsigned & res) const;
+    unsigned get_max_positive() const;
+
+    /**
+       Since the default counter value of a counter is zero, the result is never negative.
+    */
+    int get_max_counter_value() const;
+};
+
+class var_counter : public counter {
+protected:
+    ptr_vector<sort> m_sorts;
+    expr_fast_mark1  m_visited;
+    ptr_vector<expr> m_todo;
+    unsigned_vector  m_scopes;
+    unsigned get_max_var(bool & has_var);    
+public:
+    var_counter(bool stay_non_negative = true): counter(stay_non_negative) {}
+    void count_vars(ast_manager & m, const app * t, int coef = 1);
+    unsigned get_max_var(expr* e);
+    unsigned get_next_var(expr* e);
+};
+
+class ast_counter {
+    typedef obj_map<ast, int> map_impl;
+    map_impl m_data;
+    bool     m_stay_non_negative;
+ public:
+    typedef map_impl::iterator iterator;
+    
+    ast_counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+    
+    iterator begin() const { return m_data.begin(); }
+    iterator end() const { return m_data.end(); }
+    
+    int & get(ast * el) {
+        return m_data.insert_if_not_there2(el, 0)->get_data().m_value;
+    }
+    void update(ast * el, int delta){
+        get(el) += delta;
+        SASSERT(!m_stay_non_negative || get(el) >= 0);
+    }
+    
+    void inc(ast * el) { update(el, 1); }
+    void dec(ast * el) { update(el, -1); }
+};
+
+#endif

src/ast/rewriter/quant_hoist.cpp

@@ -25,7 +25,8 @@ Revision History:
 #include "bool_rewriter.h"
 #include "var_subst.h"
 #include "ast_pp.h"
-
+#include "ast_counter.h"
+#include "expr_safe_replace.h"
 
 //
 // Bring quantifiers of common type into prenex form.
@@ -42,7 +43,7 @@ public:
     
     void operator()(expr* fml, app_ref_vector& vars, bool& is_fa, expr_ref& result) {
         quantifier_type qt = Q_none_pos;
-        pull_quantifiers(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
@@ -52,7 +53,7 @@ public:
     
     void pull_exists(expr* fml, app_ref_vector& vars, expr_ref& result) {
         quantifier_type qt = Q_exists_pos;
-        pull_quantifiers(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
@@ -61,7 +62,7 @@ public:
     void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars) {
         quantifier_type qt = is_forall?Q_forall_pos:Q_exists_pos;
         expr_ref result(m);
-        pull_quantifiers(fml, qt, vars, result);
+        pull_quantifier(fml, qt, vars, result);
         TRACE("qe_verbose", 
               tout << mk_pp(fml, m) << "\n";
               tout << mk_pp(result, m) << "\n";);
@@ -78,7 +79,37 @@ public:
         expr * const * exprs = (expr* const*) (vars.c_ptr() + vars.size()- nd);
         instantiate(m, q, exprs, result);
     }
-    
+
+    unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {
+        unsigned index = var_counter().get_next_var(fml);
+        while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
+            quantifier* q = to_quantifier(fml);
+            index += q->get_num_decls();
+            if (names) {
+                names->append(q->get_num_decls(), q->get_decl_names());
+            }
+            fml = q->get_expr();
+        }
+        if (!has_quantifiers(fml)) {
+            return index;
+        }
+        app_ref_vector vars(m);
+        pull_quantifier(is_forall, fml, vars);
+        if (vars.empty()) {
+            return index;
+        }
+        // replace vars by de-bruijn indices
+        expr_safe_replace rep(m);
+        for (unsigned i = 0; i < vars.size(); ++i) {
+            app* v = vars[i].get();
+            if (names) {
+                names->push_back(v->get_decl()->get_name());
+            }                
+            rep.insert(v, m.mk_var(index++,m.get_sort(v)));
+        }
+        rep(fml);
+        return index;
+    }    
     
 private:
     
@@ -143,7 +174,7 @@ private:
     }
     
     
-    void pull_quantifiers(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
+    void pull_quantifier(expr* fml, quantifier_type& qt, app_ref_vector& vars, expr_ref& result) {
         
         if (!has_quantifiers(fml)) {
             result = fml;
@@ -159,7 +190,7 @@ private:
             if (m.is_and(fml)) {
                 num_args = a->get_num_args();
                 for (unsigned i = 0; i < num_args; ++i) {
-                    pull_quantifiers(a->get_arg(i), qt, vars, tmp);
+                    pull_quantifier(a->get_arg(i), qt, vars, tmp);
                     args.push_back(tmp);
                 }
                 m_rewriter.mk_and(args.size(), args.c_ptr(), result);
@@ -167,25 +198,25 @@ private:
             else if (m.is_or(fml)) {
                 num_args = to_app(fml)->get_num_args();
                 for (unsigned i = 0; i < num_args; ++i) {
-                    pull_quantifiers(to_app(fml)->get_arg(i), qt, vars, tmp);
+                    pull_quantifier(to_app(fml)->get_arg(i), qt, vars, tmp);
                     args.push_back(tmp);
                 }
                 m_rewriter.mk_or(args.size(), args.c_ptr(), result);
             }
             else if (m.is_not(fml)) {
-                pull_quantifiers(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
+                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
                 negate(qt);
                 result = m.mk_not(tmp);
             }
             else if (m.is_implies(fml)) {
-                pull_quantifiers(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
+                pull_quantifier(to_app(fml)->get_arg(0), negate(qt), vars, tmp);
                 negate(qt);
-                pull_quantifiers(to_app(fml)->get_arg(1), qt, vars, result);
+                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, result);
                 result = m.mk_implies(tmp, result);
             }
             else if (m.is_ite(fml)) {
-                pull_quantifiers(to_app(fml)->get_arg(1), qt, vars, tmp);
-                pull_quantifiers(to_app(fml)->get_arg(2), qt, vars, result);
+                pull_quantifier(to_app(fml)->get_arg(1), qt, vars, tmp);
+                pull_quantifier(to_app(fml)->get_arg(2), qt, vars, result);
                 result = m.mk_ite(to_app(fml)->get_arg(0), tmp, result);
             }
             else {
@@ -203,7 +234,7 @@ private:
             }
             set_quantifier_type(qt, q->is_forall());
             extract_quantifier(q, vars, tmp);
-            pull_quantifiers(tmp, qt, vars, result);
+            pull_quantifier(tmp, qt, vars, result);
             break;
         }
         case AST_VAR:
@@ -215,6 +246,8 @@ private:
             break;
         }
     }
+
+
 };   
 
 quantifier_hoister::quantifier_hoister(ast_manager& m) {
@@ -237,3 +270,6 @@ void quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, app_ref_
     m_impl->pull_quantifier(is_forall, fml, vars);
 }
 
+unsigned quantifier_hoister::pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {
+    return m_impl->pull_quantifier(is_forall, fml, names);
+}

src/ast/rewriter/quant_hoist.h

@@ -59,6 +59,14 @@ public:
        The list of variables is empty if there are no top-level universal/existential quantifier.
     */
     void pull_quantifier(bool is_forall, expr_ref& fml, app_ref_vector& vars);
+
+    /**
+       \brief Pull top-most universal (is_forall true) or existential (is_forall=false) quantifier up.
+       Return an expression with de-Bruijn indices and the list of names that were used.
+       Return index of maximal variable.
+    */
+
+    unsigned pull_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names);
 };
 
 #endif

src/muz_qe/dl_rule.cpp

@@ -107,41 +107,6 @@ namespace datalog {
         mk_rule_core(fml1, rules, name);
     }
 
-    // 
-    // Hoist quantifier from rule (universal) or query (existential)
-    // 
-    unsigned rule_manager::hoist_quantifier(bool is_forall, expr_ref& fml, svector<symbol>* names) {   
-
-        unsigned index = var_counter().get_next_var(fml);
-        while (is_quantifier(fml) && (is_forall == to_quantifier(fml)->is_forall())) {
-            quantifier* q = to_quantifier(fml);
-            index += q->get_num_decls();
-            if (names) {
-                names->append(q->get_num_decls(), q->get_decl_names());
-            }
-            fml = q->get_expr();
-        }
-        if (!has_quantifiers(fml)) {
-            return index;
-        }
-        app_ref_vector vars(m);
-        quantifier_hoister qh(m);
-        qh.pull_quantifier(is_forall, fml, vars);
-        if (vars.empty()) {
-            return index;
-        }
-        // replace vars by de-bruijn indices
-        expr_safe_replace rep(m);
-        for (unsigned i = 0; i < vars.size(); ++i) {
-            app* v = vars[i].get();
-            if (names) {
-                names->push_back(v->get_decl()->get_name());
-            }                
-            rep.insert(v, m.mk_var(index++,m.get_sort(v)));
-        }
-        rep(fml);
-        return index;
-    }
 
     void rule_manager::mk_rule_core(expr* _fml, rule_ref_vector& rules, symbol const& name) {
         app_ref_vector body(m);
@@ -149,7 +114,8 @@ namespace datalog {
         expr_ref e(m), fml(_fml, m);
         svector<bool> is_negated;
         TRACE("dl_rule", tout << mk_pp(fml, m) << "\n";);
-        unsigned index = hoist_quantifier(true, fml, 0); 
+        quantifier_hoister qh(m);
+        unsigned index = qh.pull_quantifier(true, fml, 0); 
         check_app(fml);
         head = to_app(fml);
         
@@ -225,7 +191,8 @@ namespace datalog {
         // Add implicit variables.
         // Remove existential prefix.
         bind_variables(query, false, q);
-        hoist_quantifier(false, q, &names);
+        quantifier_hoister qh(m);
+        qh.pull_quantifier(false, q, &names);
         // retrieve free variables.
         get_free_vars(q, vars);
         if (vars.contains(static_cast<sort*>(0))) {
@@ -1115,3 +1082,4 @@ namespace datalog {
 
 
 };
+

src/muz_qe/dl_rule.h

@@ -81,8 +81,6 @@ namespace datalog {
 
         void mk_rule_core(expr* fml, rule_ref_vector& rules, symbol const& name);
 
-        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.
          */