add default simplifications as tactic

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

src/muz_qe/hilbert_basis.cpp

@@ -23,8 +23,6 @@ Revision History:
 #include "heap_trie.h"
 #include "stopwatch.h"
 
-template<typename Value>
-class rational_map : public map<rational, Value, rational::hash_proc, rational::eq_proc> {};
 
 typedef int_hashtable<int_hash, default_eq<int> > int_table;
 
@@ -264,7 +262,10 @@ class hilbert_basis::index {
         void reset() { memset(this, 0, sizeof(*this)); }
     };        
 
-    typedef rational_map<value_index*> value_map;
+    template<typename Value>
+    class numeral_map : public map<numeral, Value, numeral::hash_proc, numeral::eq_proc> {};
+
+    typedef numeral_map<value_index*> value_map;
     hilbert_basis&   hb;
     value_map        m_neg;
     value_index      m_pos;

src/muz_qe/horn_tactic.cpp

@@ -21,15 +21,18 @@ Revision History:
 #include"proof_converter.h"
 #include"horn_tactic.h"
 #include"dl_context.h"
+#include"expr_replacer.h"
 
 class horn_tactic : public tactic {
     struct imp {
         ast_manager&             m;
+        bool                     m_is_simplify;
         datalog::context         m_ctx;
         smt_params               m_fparams;
 
-        imp(ast_manager & m, params_ref const & p):
+        imp(bool is_simplify, ast_manager & m, params_ref const & p):
             m(m),
+            m_is_simplify(is_simplify),
             m_ctx(m, m_fparams) {
             updt_params(p);
         }
@@ -180,6 +183,9 @@ class horn_tactic : public tactic {
             expr_ref_vector queries(m);
             std::stringstream msg;
 
+            m_ctx.reset();
+            m_ctx.ensure_opened();
+
             for (unsigned i = 0; i < sz; i++) {
                 f = g->form(i);
                 formula_kind k = get_formula_kind(f);
@@ -196,7 +202,7 @@ class horn_tactic : public tactic {
                 }
             }
 
-            if (queries.size() != 1) {
+            if (queries.size() != 1 || m_is_simplify) {
                 q = m.mk_fresh_const("query", m.mk_bool_sort());
                 register_predicate(q);
                 for (unsigned i = 0; i < queries.size(); ++i) {
@@ -208,8 +214,26 @@ class horn_tactic : public tactic {
             }
             SASSERT(queries.size() == 1);
             q = queries[0].get();
+            if (m_is_simplify) {
+                simplify(q, g, result, mc, pc);
+            }
+            else {
+                verify(q, g, result, mc, pc);
+            }
+        }
+
+        void verify(expr* q, 
+                    goal_ref const& g,
+                    goal_ref_buffer & result, 
+                    model_converter_ref & mc, 
+                    proof_converter_ref & pc) {
+
             lbool is_reachable = m_ctx.query(q);
             g->inc_depth();
+
+            bool produce_models = g->models_enabled();
+            bool produce_proofs = g->proofs_enabled();
+
             result.push_back(g.get());
             switch (is_reachable) {
             case l_true: {
@@ -237,19 +261,60 @@ class horn_tactic : public tactic {
             TRACE("horn", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
+
+        void simplify(expr* q, 
+                    goal_ref const& g,
+                    goal_ref_buffer & result, 
+                    model_converter_ref & mc, 
+                    proof_converter_ref & pc) {
+
+            expr_ref fml(m);            
+            bool produce_models = g->models_enabled();
+            bool produce_proofs = g->proofs_enabled();
+
+            if (produce_models) {
+                mc = datalog::mk_skip_model_converter();
+            }
+            if (produce_proofs) {
+                pc = datalog::mk_skip_proof_converter();
+            }
+
+            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);
+
+            expr_substitution sub(m);
+            sub.insert(q, m.mk_false());
+            scoped_ptr<expr_replacer> rep = mk_default_expr_replacer(m);
+            g->inc_depth();
+            g->reset();
+            result.push_back(g.get());
+            datalog::rule_set const& rules = m_ctx.get_rules();
+            datalog::rule_set::iterator it = rules.begin(), end = rules.end();
+            for (; it != end; ++it) {
+                datalog::rule* r = *it;
+                r->to_formula(fml);
+                (*rep)(fml);
+                g->assert_expr(fml);
+            }
+        }
+        
     };
-    
+
+    bool       m_is_simplify;
     params_ref m_params;
     statistics m_stats;
     imp *      m_imp;
 public:
-    horn_tactic(ast_manager & m, params_ref const & p):
+    horn_tactic(bool is_simplify, ast_manager & m, params_ref const & p):
+        m_is_simplify(is_simplify),
         m_params(p) {
-        m_imp = alloc(imp, m, p);
+        m_imp = alloc(imp, is_simplify, m, p);
     }
 
     virtual tactic * translate(ast_manager & m) {
-        return alloc(horn_tactic, m, m_params);
+        return alloc(horn_tactic, m_is_simplify, m, m_params);
     }
         
     virtual ~horn_tactic() {
@@ -293,7 +358,7 @@ public:
             m_imp = 0;
         }
         dealloc(d);
-        d = alloc(imp, m, m_params);
+        d = alloc(imp, m_is_simplify, m, m_params);
         #pragma omp critical (tactic_cancel)
         {
             m_imp = d;
@@ -308,6 +373,10 @@ protected:
 };
 
 tactic * mk_horn_tactic(ast_manager & m, params_ref const & p) {
-    return clean(alloc(horn_tactic, m, p));
+    return clean(alloc(horn_tactic, false, m, p));
+}
+
+tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p) {
+    return clean(alloc(horn_tactic, true, m, p));
 }
 

src/muz_qe/horn_tactic.h

@@ -27,4 +27,9 @@ tactic * mk_horn_tactic(ast_manager & m, params_ref const & p = params_ref());
 /*
   ADD_TACTIC("horn", "apply tactic for horn clauses.", "mk_horn_tactic(m, p)")
 */
+
+tactic * mk_horn_simplify_tactic(ast_manager & m, params_ref const & p = params_ref());
+/*
+  ADD_TACTIC("horn-simplify", "simplify horn clauses.", "mk_horn_simplify_tactic(m, p)")
+*/
 #endif