From dcaacf5e9bc8876c88746fbd2bdd99be875a2703 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 7 Mar 2024 15:21:26 -0800 Subject: [PATCH] add rewrite glue for instantiating equalities, #7154 Signed-off-by: Nikolaj Bjorner --- src/ast/macros/macro_manager.cpp | 13 ++++++++++--- 1 file changed, 10 insertions(+), 3 deletions(-) diff --git a/src/ast/macros/macro_manager.cpp b/src/ast/macros/macro_manager.cpp index bbe7f245c..b7c94b1b5 100644 --- a/src/ast/macros/macro_manager.cpp +++ b/src/ast/macros/macro_manager.cpp @@ -319,14 +319,21 @@ struct macro_manager::macro_expander_cfg : public default_rewriter_cfg { if (m.proofs_enabled()) { expr_ref instance = s(q->get_expr(), num, subst_args.data()); expr* eq, * lhs, * rhs; + + expr* q_inst = m.mk_or(m.mk_not(q), instance); + proof * qi_pr = m.mk_quant_inst(q_inst, num, subst_args.data()); if (m.is_not(instance, eq) && m.is_eq(eq, lhs, rhs)) { + expr_ref instance2(m); if (revert) - instance = m.mk_eq(m.mk_not(lhs), rhs); + instance2 = m.mk_eq(m.mk_not(lhs), rhs); else - instance = m.mk_eq(lhs, m.mk_not(rhs)); + instance2 = m.mk_eq(lhs, m.mk_not(rhs)); + expr* q_inst2 = m.mk_or(m.mk_not(q), instance2); + proof* eq_pr = m.mk_rewrite(q_inst, q_inst2); + qi_pr = m.mk_modus_ponens(qi_pr, eq_pr); + instance = instance2; } SASSERT(m.is_eq(instance)); - proof * qi_pr = m.mk_quant_inst(m.mk_or(m.mk_not(q), instance), num, subst_args.data()); proof * q_pr = mm.m_decl2macro_pr.find(d); proof * prs[2] = { qi_pr, q_pr }; p = m.mk_unit_resolution(2, prs);