working on separating horn simplificaiton

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

src/ast/rewriter/quant_hoist.cpp

@@ -25,7 +25,7 @@ Revision History:
 #include "bool_rewriter.h"
 #include "var_subst.h"
 #include "ast_pp.h"
-
+#include "ast_counter.h"
 
 //
 // Bring quantifiers of common type into prenex form.
@@ -215,6 +215,37 @@ private:
             break;
         }
     }
+
+    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;
+    }
 };   
 
 quantifier_hoister::quantifier_hoister(ast_manager& m) {
@@ -237,3 +268,7 @@ 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_bmc_engine.cpp

@@ -1413,20 +1413,22 @@ namespace datalog {
         datalog::rule_set        old_rules(m_ctx.get_rules());
         datalog::rule_ref_vector query_rules(rule_manager);
         datalog::rule_ref        query_rule(rule_manager);
+        model_converter_ref mc = datalog::mk_skip_model_converter();
+        m_pc = datalog::mk_skip_proof_converter();
+        m_ctx.set_model_converter(mc);
+        m_ctx.set_proof_converter(m_pc);
         rule_manager.mk_query(query, m_query_pred, query_rules, query_rule);
         m_ctx.add_rules(query_rules);
         expr_ref bg_assertion = m_ctx.get_background_assertion();        
 
-        model_converter_ref mc = datalog::mk_skip_model_converter();
-        m_pc = datalog::mk_skip_proof_converter();
         m_ctx.set_output_predicate(m_query_pred);
-        m_ctx.apply_default_transformation(mc, m_pc);
+        m_ctx.apply_default_transformation();
         
         if (m_ctx.get_params().slice()) {
             datalog::rule_transformer transformer(m_ctx);
             datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
             transformer.register_plugin(slice);
-            m_ctx.transform_rules(transformer, mc, m_pc);        
+            m_ctx.transform_rules(transformer);
             m_query_pred = slice->get_predicate(m_query_pred.get());
             m_ctx.set_output_predicate(m_query_pred);
         }

src/muz_qe/dl_context.cpp

@@ -474,6 +474,8 @@ namespace datalog {
     void context::flush_add_rules() {
         datalog::rule_manager& rm = get_rule_manager();
         datalog::rule_ref_vector rules(rm);
+        rm.set_model_converter(m_mc);
+        rm.set_proof_converter(m_pc);
         for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
             rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]);
         }
@@ -826,7 +828,7 @@ namespace datalog {
         m_closed = false;
     }
 
-    void context::transform_rules(model_converter_ref& mc, proof_converter_ref& pc) {
+    void context::transform_rules() {
         m_transf.reset();
         m_transf.register_plugin(alloc(mk_filter_rules,*this));
         m_transf.register_plugin(alloc(mk_simple_joins,*this));
@@ -841,13 +843,13 @@ namespace datalog {
         }
         m_transf.register_plugin(alloc(datalog::mk_partial_equivalence_transformer, *this));
 
-        transform_rules(m_transf, mc, pc);
+        transform_rules(m_transf);
     }
     
-    void context::transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc) {
+    void context::transform_rules(rule_transformer& transf) {
         SASSERT(m_closed); //we must finish adding rules before we start transforming them
         TRACE("dl", display_rules(tout););
-        if (transf(m_rule_set, mc, pc)) {
+        if (transf(m_rule_set, m_mc, m_pc)) {
             //we have already ensured the negation is stratified and transformations
             //should not break the stratification
             m_rule_set.ensure_closed();
@@ -862,7 +864,7 @@ namespace datalog {
         m_rule_set.add_rules(rs);
     }
 
-    void context::apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc) {
+    void context::apply_default_transformation() {
         ensure_closed();
         m_transf.reset();
         m_transf.register_plugin(alloc(datalog::mk_coi_filter, *this));
@@ -890,7 +892,7 @@ namespace datalog {
         m_transf.register_plugin(alloc(datalog::mk_bit_blast, *this, 35000));
         m_transf.register_plugin(alloc(datalog::mk_array_blast, *this, 36000));
         m_transf.register_plugin(alloc(datalog::mk_karr_invariants, *this, 36010));
-        transform_rules(m_transf, mc, pc);
+        transform_rules(m_transf);
     }
 
     void context::collect_params(param_descrs& p) {

src/muz_qe/dl_context.h

@@ -85,6 +85,8 @@ namespace datalog {
         var_subst          m_var_subst;
         rule_manager       m_rule_manager;
         rule_transformer   m_transf;
+        model_converter_ref m_mc;
+        proof_converter_ref m_pc;
 
         trail_stack<context> m_trail;
         ast_ref_vector     m_pinned;
@@ -110,6 +112,8 @@ namespace datalog {
         DL_ENGINE          m_engine;
         volatile bool      m_cancel;
 
+
+
         bool is_fact(app * head) const;
         bool has_sort_domain(relation_sort s) const;
         sort_domain & get_sort_domain(relation_sort s);
@@ -313,11 +317,15 @@ namespace datalog {
         void reopen();
         void ensure_opened();
 
-        void transform_rules(model_converter_ref& mc, proof_converter_ref& pc);
+        void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
-        void transform_rules(rule_transformer& transf, model_converter_ref& mc, proof_converter_ref& pc);
+        void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
+
+        void transform_rules();
+        void transform_rules(rule_transformer::plugin* plugin);
+        void transform_rules(rule_transformer& transf);
         void replace_rules(rule_set & rs);
 
-        void apply_default_transformation(model_converter_ref& mc, proof_converter_ref& pc);
+        void apply_default_transformation();
 
         void collect_params(param_descrs& r);
         

src/muz_qe/dl_rule.cpp

@@ -56,16 +56,16 @@ namespace datalog {
 
     void rule_manager::inc_ref(rule * r) {
         if (r) {
-            SASSERT(r->m_ref_cnt!=UINT_MAX);
+            SASSERT(r->m_ref_cnt != UINT_MAX);
             r->m_ref_cnt++;
         }
     }
 
     void rule_manager::dec_ref(rule * r) {
         if (r) {
-            SASSERT(r->m_ref_cnt>0);
+            SASSERT(r->m_ref_cnt > 0);
             r->m_ref_cnt--;
-            if (r->m_ref_cnt==0) {
+            if (r->m_ref_cnt == 0) {
                 r->deallocate(m);
             }
         }
@@ -103,8 +103,13 @@ namespace datalog {
         m_memoize_disj.reset();
         m_refs.reset();
         bind_variables(fml, true, fml1);
-        remove_labels(fml1);
+        unsigned num_rules = rules.size();
         mk_rule_core(fml1, rules, name);
+        if (m_pc) {
+            // big-step proof
+            // m.mk_cnf_star(fml1, conj, 0, 0);
+            // 
+        }
     }
 
     // 

src/muz_qe/dl_rule.h

@@ -24,6 +24,9 @@ Revision History:
 #include"dl_costs.h"
 #include"dl_util.h"
 #include"used_vars.h"
+#include"proof_converter.h"
+#include"model_converter.h"
+#include"ast_counter.h"
 
 namespace datalog {
 
@@ -48,12 +51,17 @@ namespace datalog {
         var_counter         m_var_counter;
         obj_map<expr, app*> m_memoize_disj;
         expr_ref_vector     m_refs;
+        model_converter_ref m_mc;
+        proof_converter_ref m_pc;
 
         // only the context can create a rule_manager
         friend class context;
 
         explicit rule_manager(context& ctx);
 
+        void set_model_converter(model_converter_ref& mc) { m_mc = mc; }
+        void set_proof_converter(proof_converter_ref& pc) { m_pc = pc; }
+
         /**
            \brief Move functions from predicate tails into the interpreted tail by introducing new variables.
         */

src/muz_qe/dl_util.cpp

@@ -431,166 +431,6 @@ namespace datalog {
         }
     }
 
-    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(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++) {
-            count_vars(m, r->get_tail(i), 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(const rule & r) {
-        m_todo.push_back(r.get_head());
-        m_scopes.push_back(0);
-        unsigned n = r.get_tail_size();
-        bool has_var = false;
-        for (unsigned i = 0; i < n; i++) {
-            m_todo.push_back(r.get_tail(i));
-            m_scopes.push_back(0);
-        }
-        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) {
@@ -614,6 +454,7 @@ namespace datalog {
         }
     }
 
+
     void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 
                       expr_ref_vector const& s1, expr_ref_vector const& s2, rule const& res) {
         if (!pc) return;

src/muz_qe/dl_util.h

@@ -411,82 +411,6 @@ namespace datalog {
     }
 
 
-    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(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);
 
     void resolve_rule(replace_proof_converter* pc, rule const& r1, rule const& r2, unsigned idx, 

src/muz_qe/horn_tactic.cpp

@@ -284,13 +284,15 @@ class horn_tactic : public tactic {
             func_decl* query_pred = to_app(q)->get_decl();
             m_ctx.set_output_predicate(query_pred);
             m_ctx.get_rules(); // flush adding rules.
-            m_ctx.apply_default_transformation(mc, pc);
+            m_ctx.set_model_converter(mc);
+            m_ctx.set_proof_converter(pc);
+            m_ctx.apply_default_transformation();
             
             if (m_ctx.get_params().slice()) {
                 datalog::rule_transformer transformer(m_ctx);
                 datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
                 transformer.register_plugin(slice);
-                m_ctx.transform_rules(transformer, mc, pc);
+                m_ctx.transform_rules(transformer);
             }
 
             expr_substitution sub(m);

src/muz_qe/pdr_dl_interface.cpp

@@ -89,6 +89,13 @@ lbool dl_interface::query(expr * query) {
     func_decl_ref            query_pred(m);
     datalog::rule_ref_vector query_rules(rule_manager);
     datalog::rule_ref        query_rule(rule_manager);
+    model_converter_ref mc = datalog::mk_skip_model_converter();
+    proof_converter_ref pc;
+    if (m_ctx.get_params().generate_proof_trace()) {
+        pc = datalog::mk_skip_proof_converter();
+    }
+    m_ctx.set_model_converter(mc);
+    m_ctx.set_proof_converter(pc);
     rule_manager.mk_query(query, query_pred, query_rules, query_rule);
     m_ctx.add_rules(query_rules);
     expr_ref bg_assertion = m_ctx.get_background_assertion();
@@ -105,19 +112,15 @@ lbool dl_interface::query(expr * query) {
           m_ctx.display_rules(tout);
           );
 
-    model_converter_ref mc = datalog::mk_skip_model_converter();
-    proof_converter_ref pc;
-    if (m_ctx.get_params().generate_proof_trace()) {
-        pc = datalog::mk_skip_proof_converter();
-    }
     m_ctx.set_output_predicate(query_pred);
-    m_ctx.apply_default_transformation(mc, pc);
+
+    m_ctx.apply_default_transformation();
 
     if (m_ctx.get_params().slice()) {
         datalog::rule_transformer transformer(m_ctx);
         datalog::mk_slice* slice = alloc(datalog::mk_slice, m_ctx);
         transformer.register_plugin(slice);
-        m_ctx.transform_rules(transformer, mc, pc);        
+        m_ctx.transform_rules(transformer);
         query_pred = slice->get_predicate(query_pred.get());
         m_ctx.set_output_predicate(query_pred);
         
@@ -134,22 +137,25 @@ lbool dl_interface::query(expr * query) {
 
     if (m_ctx.get_params().unfold_rules() > 0) {
         unsigned num_unfolds = m_ctx.get_params().unfold_rules();
-        datalog::rule_transformer transformer1(m_ctx), transformer2(m_ctx);
+        datalog::rule_transformer transf1(m_ctx), transf2(m_ctx);        
+        transf1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
+        transf2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
         if (m_ctx.get_params().coalesce_rules()) {
-            transformer1.register_plugin(alloc(datalog::mk_coalesce, m_ctx));
+            m_ctx.transform_rules(transf1);
-            m_ctx.transform_rules(transformer1, mc, pc);
         }
-        transformer2.register_plugin(alloc(datalog::mk_unfold, m_ctx));
         while (num_unfolds > 0) {
-            m_ctx.transform_rules(transformer2, mc, pc);        
+            m_ctx.transform_rules(transf2);
             --num_unfolds;
         }
     }
     // remove universal quantifiers from body.
+
+
+
     datalog::mk_extract_quantifiers* extract_quantifiers = alloc(datalog::mk_extract_quantifiers, m_ctx);
     datalog::rule_transformer extract_q_tr(m_ctx);
     extract_q_tr.register_plugin(extract_quantifiers);
-    m_ctx.transform_rules(extract_q_tr, mc, pc);
+    m_ctx.transform_rules(extract_q_tr);
     
 
     IF_VERBOSE(2, m_ctx.display_rules(verbose_stream()););

src/muz_qe/rel_context.cpp

@@ -106,9 +106,7 @@ namespace datalog {
         TRACE("dl", m_context.display(tout););
 
         while (true) {
-            model_converter_ref mc; // Ignored in Datalog mode
+            m_context.transform_rules();
-            proof_converter_ref pc; // Ignored in Datalog mode
-            m_context.transform_rules(mc, pc);
             compiler::compile(m_context, m_context.get_rules(), rules_code, termination_code);
 
             TRACE("dl", rules_code.display(*this, tout); );
@@ -266,14 +264,12 @@ namespace datalog {
         reset_negated_tables();
         
         if (m_context.generate_explanations()) {
-            model_converter_ref mc; // ignored in Datalog mode
-            proof_converter_ref pc; // ignored in Datalog mode
             rule_transformer transformer(m_context);
             //expl_plugin is deallocated when transformer goes out of scope
             mk_explanations * expl_plugin = 
                 alloc(mk_explanations, m_context, m_context.explanations_on_relation_level());
             transformer.register_plugin(expl_plugin);
-            m_context.transform_rules(transformer, mc, pc);
+            m_context.transform_rules(transformer);
 
             //we will retrieve the predicate with explanations instead of the original query predicate
             query_pred = expl_plugin->get_e_decl(query_pred);
@@ -283,11 +279,9 @@ namespace datalog {
         }
 
         if (m_context.magic_sets_for_queries()) {
-            model_converter_ref mc; // Ignored in Datalog mode
-            proof_converter_ref pc; // Ignored in Datalog mode
             rule_transformer transformer(m_context);
             transformer.register_plugin(alloc(mk_magic_sets, m_context, qrule.get()));
-            m_context.transform_rules(transformer, mc, pc);
+            m_context.transform_rules(transformer);
         }
 
         lbool res = saturate();

src/shell/datalog_frontend.cpp

@@ -200,9 +200,7 @@ unsigned read_datalog(char const * file) {
             timeout = UINT_MAX;
         }
         do {
-            model_converter_ref mc; // ignored
+            ctx.transform_rules();
-            proof_converter_ref pc; // ignored
-            ctx.transform_rules(mc, pc);
             
             datalog::compiler::compile(ctx, ctx.get_rules(), rules_code, termination_code);
             

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;
         }