mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

add rewrite glue for instantiating equalities, #7154

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2024-03-07 15:21:26 -08:00
parent a4ecaf1ff5
commit dcaacf5e9b
1 changed files with 10 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/ast/macros/macro_manager.cpp
View file

@ -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);