Move ast_counter to location for common utilities. It depends on get_free_vars, so is in rewriter directory

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

src/muz_qe/dl_compiler.cpp

@@ -384,8 +384,8 @@ namespace datalog {
     void compiler::get_local_indexes_for_projection(rule * r, unsigned_vector & res) {
         SASSERT(r->get_positive_tail_size()==2);
         ast_manager & m = m_context.get_manager();
-        var_counter counter;
+        rule_counter counter;
-        counter.count_vars(m, r);
+        counter.count_rule_vars(m, r);
         app * t1 = r->get_tail(0);
         app * t2 = r->get_tail(1);
         counter.count_vars(m, t1, -1);

src/muz_qe/dl_mk_explanations.cpp

@@ -708,8 +708,8 @@ namespace datalog {
     }
 
     rule * mk_explanations::get_e_rule(rule * r) {
-        var_counter ctr;
+        rule_counter ctr;
-        ctr.count_vars(m_manager, r);
+        ctr.count_rule_vars(m_manager, r);
         unsigned max_var;
         unsigned next_var = ctr.get_max_positive(max_var) ? (max_var+1) : 0;
         unsigned head_var = next_var++;

src/muz_qe/dl_mk_interp_tail_simplifier.cpp

@@ -35,7 +35,7 @@ namespace datalog {
     // -----------------------------------
 
     void mk_interp_tail_simplifier::rule_substitution::reset(rule * r) {
-        unsigned var_cnt = m_context.get_rule_manager().get_var_counter().get_max_var(*r)+1;
+        unsigned var_cnt = m_context.get_rule_manager().get_counter().get_max_rule_var(*r)+1;
         m_subst.reset();
         m_subst.reserve(1, var_cnt);
         m_rule = r;
@@ -541,8 +541,8 @@ namespace datalog {
 
         rule_ref pro_var_eq_result(m_context.get_rule_manager());
         if (propagate_variable_equivalences(res, pro_var_eq_result)) {
-            SASSERT(var_counter().get_max_var(*r.get())==0 || 
+            SASSERT(rule_counter().get_max_rule_var(*r.get())==0 || 
-                var_counter().get_max_var(*r.get()) > var_counter().get_max_var(*pro_var_eq_result.get()));
+                    rule_counter().get_max_rule_var(*r.get()) > rule_counter().get_max_rule_var(*pro_var_eq_result.get()));
             r = pro_var_eq_result;
             goto start;
         }

src/muz_qe/dl_mk_karr_invariants.cpp

@@ -145,7 +145,7 @@ namespace datalog {
     }
     
     bool mk_karr_invariants::get_transition_relation(rule const& r, matrix& M) {
-        unsigned num_vars = rm.get_var_counter().get_max_var(r)+1;
+        unsigned num_vars = rm.get_counter().get_max_rule_var(r)+1;
         unsigned arity = r.get_decl()->get_arity();
         unsigned num_columns = arity + num_vars;        
         unsigned utsz = r.get_uninterpreted_tail_size();

src/muz_qe/dl_mk_rule_inliner.cpp

@@ -65,8 +65,8 @@ namespace datalog {
     // -----------------------------------
 
     bool rule_unifier::unify_rules(const rule& tgt, unsigned tgt_idx, const rule& src) {
-        var_counter& vc = m_rm.get_var_counter();
+        rule_counter& vc = m_rm.get_counter();
-        unsigned var_cnt = std::max(vc.get_max_var(tgt), vc.get_max_var(src))+1;
+        unsigned var_cnt = std::max(vc.get_max_rule_var(tgt), vc.get_max_rule_var(src))+1;
         m_subst.reset();
         m_subst.reserve(2, var_cnt);
         
@@ -733,7 +733,7 @@ namespace datalog {
         }
 
         // initialize substitution.
-        var_counter& vc = m_rm.get_var_counter();
+        rule_counter& vc = m_rm.get_counter();
         unsigned max_var = 0;
         for (unsigned i = 0; i < sz; ++i) {
             rule* r = acc[i].get();
@@ -820,7 +820,7 @@ namespace datalog {
                     del_rule(r2, j);
                 }
 
-                max_var = std::max(max_var, vc.get_max_var(*r.get()));
+                max_var = std::max(max_var, vc.get_max_rule_var(*r.get()));
                 m_subst.reserve_vars(max_var+1);
 
             }

src/muz_qe/dl_mk_similarity_compressor.cpp

@@ -372,10 +372,10 @@ namespace datalog {
             new_negs.push_back(r->is_neg_tail(i));
         }
 
-        var_counter var_ctr;
+        rule_counter ctr;
-        var_ctr.count_vars(m_manager, r);
+        ctr.count_rule_vars(m_manager, r);
         unsigned max_var_idx, new_var_idx_base;
-        if(var_ctr.get_max_positive(max_var_idx)) {
+        if(ctr.get_max_positive(max_var_idx)) {
             new_var_idx_base = max_var_idx+1;
         }
         else {

src/muz_qe/dl_mk_simple_joins.cpp

@@ -310,8 +310,8 @@ namespace datalog {
         }
 
         void register_rule(rule * r) {
-            var_counter counter;
+            rule_counter counter;
-            counter.count_vars(m, r, 1);
+            counter.count_rule_vars(m, r, 1);
 
             ptr_vector<app> & rule_content = 
                 m_rules_content.insert_if_not_there2(r, ptr_vector<app>())->get_data().m_value;

src/muz_qe/dl_rule.cpp

@@ -705,7 +705,7 @@ namespace datalog {
         bool_rewriter(m).mk_and(tails_with_unbound.size(), tails_with_unbound.c_ptr(), unbound_tail);
 
         unsigned q_var_cnt = unbound_vars.num_elems();
-        unsigned max_var = m_var_counter.get_max_var(*r);
+        unsigned max_var = m_counter.get_max_rule_var(*r);
 
         expr_ref_vector subst(m);
 

src/muz_qe/dl_rule.h

@@ -45,7 +45,7 @@ namespace datalog {
     {
         ast_manager&        m;
         context&            m_ctx;
-        var_counter         m_var_counter;
+        rule_counter        m_counter;
         obj_map<expr, app*> m_memoize_disj;
         expr_ref_vector     m_refs;
 
@@ -162,7 +162,7 @@ namespace datalog {
 
         static bool is_forall(ast_manager& m, expr* e, quantifier*& q);
 
-        var_counter& get_var_counter() { return m_var_counter; }
+        rule_counter& get_counter() { return m_counter; }
 
     };
 

src/muz_qe/dl_util.cpp

@@ -431,89 +431,8 @@ namespace datalog {
         }
     }
 
-    void counter::update(unsigned el, int delta) {
+    
-        int & counter = get(el);
+    void rule_counter::count_rule_vars(ast_manager & m, const rule * r, int coef) {
-        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(idx_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);
-                }
-            }
-        }
-    }
-
-    void var_counter::count_vars(ast_manager & m, const rule * r, int coef) {
         count_vars(m, r->get_head(), 1);
         unsigned n = r->get_tail_size();
         for (unsigned i = 0; i < n; i++) {
@@ -521,50 +440,7 @@ namespace datalog {
         }
     }
 
-    unsigned var_counter::get_max_var(bool& has_var) {
+    unsigned rule_counter::get_max_rule_var(const rule & r) {
-        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(const rule & r) {
         m_todo.push_back(r.get_head());
         m_scopes.push_back(0);
         unsigned n = r.get_tail_size();
@@ -576,22 +452,6 @@ namespace datalog {
         return get_max_var(has_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;
-    }
-
     void del_rule(horn_subsume_model_converter* mc, rule& r) {
         if (mc) {
             ast_manager& m = mc->get_manager();
@@ -678,10 +538,6 @@ namespace datalog {
     proof_converter* mk_skip_proof_converter() { return alloc(skip_proof_converter); }
 
 
-    unsigned get_max_var(const rule & r, ast_manager & m) {
-        var_counter ctr;
-        return ctr.get_max_var(r);
-    }
 
     void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt) {
         SASSERT(tgt.empty());

src/muz_qe/dl_util.h

@@ -27,6 +27,7 @@ Revision History:
 #include"replace_proof_converter.h"
 #include"substitution.h"
 #include"fixedpoint_params.hpp"
+#include"ast_counter.h"
 
 namespace datalog {
 
@@ -411,80 +412,12 @@ namespace datalog {
     }
 
 
-    class counter {
+
-    protected:
+    class rule_counter : public var_counter {        
-        typedef u_map<int> map_impl;
-        map_impl m_data;
-        const bool m_stay_non_negative;
     public:
-        typedef map_impl::iterator iterator;
+        rule_counter(bool stay_non_negative = true): var_counter(stay_non_negative) {}
-
+        void count_rule_vars(ast_manager & m, const rule * r, int coef = 1);
-        counter(bool stay_non_negative = true) : m_stay_non_negative(stay_non_negative) {}
+        unsigned get_max_rule_var(const rule& r);
-
-        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(idx_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 {
-        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);
-        void count_vars(ast_manager & m, const rule * r, int coef = 1);
-        unsigned get_max_var(const rule& r);
-        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); }
     };
 
     void del_rule(horn_subsume_model_converter* mc, rule& r);
@@ -497,11 +430,6 @@ namespace datalog {
     proof_converter* mk_skip_proof_converter();
 
 
-    /**
-       Return maximal variable number, or zero is there isn't any
-    */
-    // unsigned get_max_var(const rule & r, ast_manager & m);
-
     void reverse_renaming(ast_manager & m, const expr_ref_vector & src, expr_ref_vector & tgt);
 
     /**

src/muz_qe/pdr_context.cpp

@@ -968,11 +968,11 @@ namespace pdr {
         unsigned deltas[2];
         datalog::rule_ref rule(rm), r0(rm);
         model_node* n = m_root;
-        datalog::var_counter& vc = rm.get_var_counter();
+        datalog::rule_counter& vc = rm.get_counter();
         substitution subst(m);
         unifier unif(m);
         rule = n->get_rule();
-        unsigned max_var = vc.get_max_var(*rule);
+        unsigned max_var = vc.get_max_rule_var(*rule);
         predicates.push_back(rule->get_head());
         children.append(n);
         bool first = true;
@@ -983,7 +983,7 @@ namespace pdr {
             children.pop_back();
             n->mk_instantiate(r0, rule, binding);
             
-            max_var = std::max(max_var, vc.get_max_var(*rule));
+            max_var = std::max(max_var, vc.get_max_rule_var(*rule));
             subst.reset();
             subst.reserve(2, max_var+1);
             deltas[0] = 0;

src/muz_qe/pdr_quantifiers.cpp

@@ -612,8 +612,8 @@ namespace pdr {
         datalog::rule_set::iterator it = m_rules.begin(), end = m_rules.end();
         for (; it != end; ++it) {
             datalog::rule* r = *it;
-            datalog::var_counter vc(true);
+            datalog::rule_counter vc(true);
-            unsigned max_var = vc.get_max_var(*r);
+            unsigned max_var = vc.get_max_rule_var(*r);
             app_ref_vector body(m);
             for (unsigned i = 0; i < m_instantiations.size(); ++i) {
                 if (r == m_instantiated_rules[i]) {

src/muz_qe/tab_context.cpp

@@ -317,7 +317,7 @@ namespace tb {
             for (unsigned i = utsz; i < tsz; ++i) {
                 fmls.push_back(r->get_tail(i));
             }
-            m_num_vars = 1 + r.get_manager().get_var_counter().get_max_var(*r);
+            m_num_vars = 1 + r.get_manager().get_counter().get_max_rule_var(*r);
             m_head = r->get_head();
             m_predicates.reset();
             for (unsigned i = 0; i < utsz; ++i) {

src/smt/tactic/ctx_solver_simplify_tactic.cpp

@@ -92,7 +92,34 @@ protected:
         ptr_vector<expr> fmls;
         g.get_formulas(fmls);
         fml = m.mk_and(fmls.size(), fmls.c_ptr());
+        m_solver.push();
         reduce(fml);
+        m_solver.pop(1);
+        SASSERT(m_solver.get_scope_level() == 0);
+        TRACE("ctx_solver_simplify_tactic",
+              for (unsigned i = 0; i < fmls.size(); ++i) {
+                  tout << mk_pp(fmls[i], m) << "\n";
+              }
+              tout << "=>\n";
+              tout << mk_pp(fml, m) << "\n";);
+        DEBUG_CODE(
+        {
+            m_solver.push();
+            expr_ref fml1(m);
+            fml1 = m.mk_and(fmls.size(), fmls.c_ptr());
+            fml1 = m.mk_iff(fml, fml1);
+            fml1 = m.mk_not(fml1);
+            m_solver.assert_expr(fml1);
+            lbool is_sat = m_solver.check();
+            TRACE("ctx_solver_simplify_tactic", tout << "is non-equivalence sat?: " << is_sat << "\n";);
+            if (is_sat != l_false) {
+                TRACE("ctx_solver_simplify_tactic", 
+                      tout << "result is not equivalent to input\n";
+                      tout << mk_pp(fml1, m) << "\n";);
+                UNREACHABLE();
+            }
+            m_solver.pop(1);
+        });
         g.reset();
         g.assert_expr(fml, 0, 0); 
         IF_VERBOSE(TACTIC_VERBOSITY_LVL, verbose_stream() << "(ctx-solver-simplify :num-steps " << m_num_steps << ")\n";);
@@ -106,21 +133,22 @@ protected:
         svector<bool>    is_checked;
         svector<unsigned> parent_ids, self_ids;
         expr_ref_vector fresh_vars(m), trail(m);
-        expr_ref res(m);
+        expr_ref res(m), tmp(m);
         obj_map<expr,std::pair<unsigned, expr*> > cache;
         unsigned id = 1;
-        expr* n = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
         expr* n2, *fml;
         unsigned path_id = 0, self_pos = 0;
         app * a;
         unsigned sz;
         std::pair<unsigned,expr*> path_r;
         ptr_vector<expr> found;
+        expr* n = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
+        trail.push_back(n);        
 
         fml = result.get();
-        m_solver.assert_expr(m.mk_not(m.mk_iff(fml, n)));
+        tmp = m.mk_not(m.mk_iff(fml, n));
+        m_solver.assert_expr(tmp);
 
-        trail.push_back(n);        
         todo.push_back(fml);
         names.push_back(n);
         is_checked.push_back(false);
@@ -144,6 +172,7 @@ protected:
                 goto done;
             }
             if (m.is_bool(e) && !checked && simplify_bool(n, res)) {
+                TRACE("ctx_solver_simplify_tactic", tout << "simplified: " << mk_pp(e, m) << " |-> " << mk_pp(res, m) << "\n";);                
                 goto done;
             }
             if (!is_app(e)) {
@@ -176,7 +205,7 @@ protected:
                                         
                     found.push_back(arg);
                     if (path_r.first == self_pos) {
-                        TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << "\n";);
+                        TRACE("ctx_solver_simplify_tactic", tout << "cached " << mk_pp(arg, m) << " |-> " << mk_pp(path_r.second, m) << "\n";);
                         args.push_back(path_r.second);
                     }
                     else {
@@ -188,11 +217,11 @@ protected:
                 }
                 else if (!n2 && !found.contains(arg)) {                
                     n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
+                    trail.push_back(n2);
                     todo.push_back(arg);
                     parent_ids.push_back(self_pos);
                     self_ids.push_back(0);
                     names.push_back(n2);
-                    trail.push_back(n2);
                     args.push_back(n2);
                     is_checked.push_back(false);
                 }
@@ -205,7 +234,8 @@ protected:
             // child needs to be visited.
             if (n2) {
                 m_solver.push();
-                m_solver.assert_expr(m.mk_eq(res, n));
+                tmp = m.mk_eq(res, n);
+                m_solver.assert_expr(tmp);
                 continue;
             }
         
@@ -229,7 +259,7 @@ protected:
     }
 
     bool simplify_bool(expr* n, expr_ref& res) {
-
+        expr_ref tmp(m);
         m_solver.push();
         m_solver.assert_expr(n);
         lbool is_sat = m_solver.check();
@@ -240,7 +270,8 @@ protected:
         }
 
         m_solver.push();
-        m_solver.assert_expr(m.mk_not(n));
+        tmp = m.mk_not(n);
+        m_solver.assert_expr(tmp);
         is_sat = m_solver.check();
         m_solver.pop(1);
         if (is_sat == l_false) {
@@ -254,7 +285,7 @@ protected:
     expr_ref local_simplify(app* a, expr* n, unsigned& id, unsigned index) {
         SASSERT(index < a->get_num_args());
         SASSERT(m.is_bool(a->get_arg(index)));
-        expr_ref n2(m), result(m);
+        expr_ref n2(m), result(m), tmp(m);
         n2 = m.mk_app(m_fn, m_arith.mk_numeral(rational(id++), true));
         ptr_buffer<expr> args;
         for (unsigned i = 0; i < a->get_num_args(); ++i) {
@@ -267,7 +298,8 @@ protected:
         }
         m_mk_app(a->get_decl(), args.size(), args.c_ptr(), result);
         m_solver.push();
-        m_solver.assert_expr(m.mk_eq(result, n));
+        tmp = m.mk_eq(result, n);
+        m_solver.assert_expr(tmp);
         if (!simplify_bool(n2, result)) {
             result = a;
         }