From 9845c33236e944c3435b7303267d3acc5fc7b8e9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 15 Nov 2022 09:13:13 -0800 Subject: [PATCH] add shortcuts in rewriter, eliminate redundancies in dependent_expr tactic --- src/ast/rewriter/bool_rewriter.cpp | 12 +++-- src/ast/rewriter/bv_rewriter.cpp | 4 +- src/ast/rewriter/th_rewriter.cpp | 57 +++++++++++++++--------- src/ast/rewriter/th_rewriter.h | 1 + src/tactic/dependent_expr_state_tactic.h | 1 + 5 files changed, 50 insertions(+), 25 deletions(-) diff --git a/src/ast/rewriter/bool_rewriter.cpp b/src/ast/rewriter/bool_rewriter.cpp index 632b6c0f606..1e0b6318aea 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 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 209f7a13b16..c594233102e 100644 --- a/src/ast/rewriter/bv_rewriter.cpp +++ b/src/ast/rewriter/bv_rewriter.cpp @@ -19,6 +19,7 @@ Module Name: #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 9604f6d16a3..4c7d4dc4921 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 { 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 b84164abc61..2c08c247d35 100644 --- a/src/ast/rewriter/th_rewriter.h +++ b/src/ast/rewriter/th_rewriter.h @@ -51,6 +51,7 @@ class th_rewriter { expr_ref mk_app(func_decl* f, unsigned num_args, expr* const* args); expr_ref mk_app(func_decl* f, ptr_vector 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 aaf744d5fbf..d3f77b7732e 100644 --- a/src/tactic/dependent_expr_state_tactic.h +++ b/src/tactic/dependent_expr_state_tactic.h @@ -99,6 +99,7 @@ class dependent_expr_state_tactic : public tactic, public dependent_expr_state { 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());