diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp
index 632b6c0f6..1e0b6318a 100644
--- a/src/ast/rewriter/bool_rewriter.cpp
+++ b/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
diff --git a/src/ast/rewriter/bv_rewriter.cpp b/src/ast/rewriter/bv_rewriter.cpp
index 209f7a13b..c59423310 100644
--- a/src/ast/rewriter/bv_rewriter.cpp
+++ b/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;
}
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index 9604f6d16..4c7d4dc49 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/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();
- 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);
+ st = reduce_eq(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);
}
diff --git a/src/ast/rewriter/th_rewriter.h b/src/ast/rewriter/th_rewriter.h
index b84164abc..2c08c247d 100644
--- a/src/ast/rewriter/th_rewriter.h
+++ b/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,
diff --git a/src/tactic/dependent_expr_state_tactic.h b/src/tactic/dependent_expr_state_tactic.h
index aaf744d5f..d3f77b773 100644
--- a/src/tactic/dependent_expr_state_tactic.h
+++ b/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());