add shortcuts in rewriter, eliminate redundancies in dependent_expr tactic

src/ast/rewriter/bool_rewriter.cpp

@@ -686,6 +686,10 @@ br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result)
 
 
 app* bool_rewriter::mk_eq(expr* lhs, expr* rhs) {
+    if (m().are_distinct(lhs, rhs))
+        return m().mk_false();
+    if (lhs == rhs)
+        return m().mk_true();
     // degrades simplification 
     // if (lhs->get_id() > rhs->get_id()) std::swap(lhs, rhs);
     return m().mk_eq(lhs, rhs);
@@ -785,7 +789,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
 
     if (num_args == 2) {
         expr_ref tmp(m());
-        result = m().mk_not(mk_eq(args[0], args[1]));
+        result = mk_not(mk_eq(args[0], args[1]));
         return BR_REWRITE2; // mk_eq may be dispatched to other rewriters.
     }
 
@@ -827,7 +831,7 @@ br_status bool_rewriter::mk_distinct_core(unsigned num_args, expr * const * args
         ptr_buffer<expr> new_diseqs;
         for (unsigned i = 0; i < num_args; i++) {
             for (unsigned j = i + 1; j < num_args; j++)
-                new_diseqs.push_back(m().mk_not(mk_eq(args[i], args[j])));
+                new_diseqs.push_back(mk_not(mk_eq(args[i], args[j])));
         }
         result = m().mk_and(new_diseqs);
         return BR_REWRITE3;
@@ -937,13 +941,13 @@ br_status bool_rewriter::mk_ite_core(expr * c, expr * t, expr * e, expr_ref & re
     if (m().is_not(t, t1) && m().is_eq(t1, t1, t2) && e == t1) {
         expr_ref a(m());
         mk_and(c, t2, a);
-        result = m().mk_not(m().mk_eq(t1, a));
+        result = mk_not(mk_eq(t1, a));
         return BR_REWRITE3;
     }
     if (m().is_not(t, t1) && m().is_eq(t1, t2, t1) && e == t1) {
         expr_ref a(m());
         mk_and(c, t2, a);
-        result = m().mk_eq(t1, a);
+        result = mk_eq(t1, a);
         return BR_REWRITE3;
     }
 #endif

src/ast/rewriter/bv_rewriter.cpp

@@ -19,6 +19,7 @@ Notes:
 #include "params/bv_rewriter_params.hpp"
 #include "ast/rewriter/bv_rewriter.h"
 #include "ast/rewriter/poly_rewriter_def.h"
+#include "ast/rewriter/bool_rewriter.h"
 #include "ast/ast_smt2_pp.h"
 #include "ast/ast_lt.h"
 
@@ -2386,7 +2387,8 @@ br_status bv_rewriter::mk_bit2bool(expr * lhs, expr * rhs, expr_ref & result) {
 
     expr* a = nullptr, *b = nullptr, *c = nullptr;
     if (m().is_ite(lhs, a, b, c)) {
-        result = m().mk_ite(a, m().mk_eq(b, rhs), m().mk_eq(c, rhs));
+        bool_rewriter rw(m());
+        result = rw.mk_ite(a, rw.mk_eq(b, rhs), rw.mk_eq(c, rhs));
         return BR_REWRITE2;
     }
     

src/ast/rewriter/th_rewriter.cpp

@@ -183,22 +183,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             if (k == OP_EQ) {
                 // theory dispatch for =
                 SASSERT(num == 2);
-                family_id s_fid = args[0]->get_sort()->get_family_id();
+                st = reduce_eq(args[0], args[1], result);
-                if (s_fid == m_a_rw.get_fid())
-                    st = m_a_rw.mk_eq_core(args[0], args[1], result);
-                else if (s_fid == m_bv_rw.get_fid())
-                    st = m_bv_rw.mk_eq_core(args[0], args[1], result);
-                else if (s_fid == m_dt_rw.get_fid())
-                    st = m_dt_rw.mk_eq_core(args[0], args[1], result);
-                else if (s_fid == m_f_rw.get_fid())
-                    st = m_f_rw.mk_eq_core(args[0], args[1], result);
-                else if (s_fid == m_ar_rw.get_fid())
-                    st = m_ar_rw.mk_eq_core(args[0], args[1], result);
-                else if (s_fid == m_seq_rw.get_fid())
-                    st = m_seq_rw.mk_eq_core(args[0], args[1], result);
-                if (st != BR_FAILED)
-                    return st;
-                st = apply_tamagotchi(args[0], args[1], result);
                 if (st != BR_FAILED)
                     return st;
             }
@@ -695,9 +680,35 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args) {
         expr_ref result(m());
         proof_ref pr(m());
-        if (BR_FAILED == reduce_app(f, num_args, args, result, pr)) {
+        if (BR_FAILED == reduce_app(f, num_args, args, result, pr)) 
             result = m().mk_app(f, num_args, args);
+        return result;
     }
+
+    br_status reduce_eq(expr* a, expr* b, expr_ref& result) {
+        family_id s_fid = a->get_sort()->get_family_id();
+        br_status st = BR_FAILED;
+        if (s_fid == m_a_rw.get_fid())
+            st = m_a_rw.mk_eq_core(a, b, result);
+        else if (s_fid == m_bv_rw.get_fid())
+            st = m_bv_rw.mk_eq_core(a, b, result);
+        else if (s_fid == m_dt_rw.get_fid())
+            st = m_dt_rw.mk_eq_core(a, b, result);
+        else if (s_fid == m_f_rw.get_fid())
+            st = m_f_rw.mk_eq_core(a, b, result);
+        else if (s_fid == m_ar_rw.get_fid())
+            st = m_ar_rw.mk_eq_core(a, b, result);
+        else if (s_fid == m_seq_rw.get_fid())
+            st = m_seq_rw.mk_eq_core(a, b, result);
+        if (st != BR_FAILED)
+            return st;
+        return apply_tamagotchi(a, b, result);        
+    }
+
+    expr_ref mk_eq(expr* a, expr* b) {
+        expr_ref result(m());
+        if (BR_FAILED == reduce_eq(a, b, result)) 
+            result = m().mk_eq(a, b);
         return result;
     }
 
@@ -897,6 +908,10 @@ struct th_rewriter::imp : public rewriter_tpl<th_rewriter_cfg> {
         return m_cfg.mk_app(f, sz, args);
     }
 
+    expr_ref mk_eq(expr* a, expr* b) {
+        return m_cfg.mk_eq(a, b);
+    }
+
     void set_solver(expr_solver* solver) {
         m_cfg.m_seq_rw.set_solver(solver);
     }
@@ -928,7 +943,6 @@ void th_rewriter::set_flat_and_or(bool f) {
     m_imp->cfg().m_b_rw.set_flat_and_or(f);
 }
 
-
 th_rewriter::~th_rewriter() {
     dealloc(m_imp);
 }
@@ -941,7 +955,6 @@ unsigned th_rewriter::get_num_steps() const {
     return m_imp->get_num_steps();
 }
 
-
 void th_rewriter::cleanup() {
     ast_manager & m = m_imp->m();
     m_imp->~imp();
@@ -991,6 +1004,10 @@ expr_ref th_rewriter::mk_app(func_decl* f, unsigned num_args, expr* const* args)
     return m_imp->mk_app(f, num_args, args);
 }
 
+expr_ref th_rewriter::mk_eq(expr* a, expr* b) {
+    return m_imp->mk_eq(a, b);
+}
+
 void th_rewriter::set_solver(expr_solver* solver) {
     m_imp->set_solver(solver);
 }

src/ast/rewriter/th_rewriter.h

@@ -51,6 +51,7 @@ public:
 
     expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args);
     expr_ref mk_app(func_decl* f, ptr_vector<expr> const& args) { return mk_app(f, args.size(), args.data()); }
+    expr_ref mk_eq(expr* a, expr* b);
 
     bool reduce_quantifier(quantifier * old_q, 
                            expr * new_body, 

src/tactic/dependent_expr_state_tactic.h

@@ -99,6 +99,7 @@ public:
         if (!in->proofs_enabled())
             m_simp->reduce();
         m_goal->elim_true();
+        m_goal->elim_redundancies();
         m_goal->inc_depth();
         if (in->models_enabled())
             in->add(m_model_trail->get_model_converter().get());