mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-08 12:11:23 +00:00
Code Activity

add destructive equality resolution to the main simplifier.

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-02-18 17:54:26 -08:00
parent c0f80f92ba
commit cb81473260
2 changed files with 15 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/ast/rewriter/th_rewriter.cpp
View file

@ -31,6 +31,7 @@ Notes:
#include "ast/rewriter/seq_rewriter.h"
#include "ast/rewriter/rewriter_def.h"
#include "ast/rewriter/var_subst.h"
#include "ast/rewriter/der.h"
#include "ast/rewriter/expr_safe_replace.h"
#include "ast/expr_substitution.h"
#include "ast/ast_smt2_pp.h"
@ -54,6 +55,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
recfun_rewriter m_rec_rw;
arith_util m_a_util;
bv_util m_bv_util;
der m_der;
expr_safe_replace m_rep;
expr_ref_vector m_pinned;
// substitution support
@ -819,6 +821,15 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
result_pr = m().mk_transitivity(p1, p2);
}
if (is_quantifier(result)) {
proof_ref p2(m());
expr_ref r(m());
m_der(to_quantifier(result), r, p2);
if (m().proofs_enabled() && result.get() != r.get())
result_pr = m().mk_transitivity(result_pr, p2);
result = r;
}
TRACE("reduce_quantifier", tout << "after elim_unused_vars:\n" << result << " " << result_pr << "\n" ;);
SASSERT(old_q->get_sort() == result->get_sort());
@ -839,6 +850,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
m_rec_rw(m),
m_a_util(m),
m_bv_util(m),
m_der(m),
m_rep(m),
m_pinned(m),
m_used_dependencies(m) {