mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-24 09:11:17 +00:00
Code Activity

Convert der tactic to simplifier: add der_simplifier.h and update der_tactic.h

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-21 23:49:05 +00:00
parent 30784ecaa9
commit c78b3d872d
2 changed files with 54 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

42
src/ast/simplifiers/der_simplifier.h Normal file
View file

@ -0,0 +1,42 @@
/*++
Copyright (c) 2022 Microsoft Corporation
Module Name:
der_simplifier.h
Abstract:
Dependent expression simplifier for destructive equality resolution (DER).
Author:
Nikolaj Bjorner (nbjorner) 2022-11-24
--*/
#pragma once
#include "ast/simplifiers/dependent_expr_state.h"
#include "ast/rewriter/der.h"
class der_simplifier : public dependent_expr_simplifier {
der_rewriter m_r;
public:
der_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& fmls)
: dependent_expr_simplifier(m, fmls), m_r(m) {}
char const* name() const override { return "der"; }
void reduce() override {
expr_ref new_curr(m);
proof_ref new_pr(m);
for (unsigned idx : indices()) {
auto d = m_fmls[idx];
m_r(d.fml(), new_curr, new_pr);
m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep()));
}
}
bool supports_proofs() const override { return true; }
};

12
src/tactic/core/der_tactic.h
View file

@ -49,12 +49,24 @@ equality resolution rule takes the form:
--*/
#pragma once
#include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/der_simplifier.h"
class ast_manager;
class tactic;
tactic * mk_der_tactic(ast_manager & m);
inline tactic * mk_der2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p,
[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* {
return alloc(der_simplifier, m, p, s);
});
}
/*
ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m)")
ADD_TACTIC("der2", "destructive equality resolution.", "mk_der2_tactic(m, p)")
ADD_SIMPLIFIER("der", "destructive equality resolution.", "alloc(der_simplifier, m, p, s)")
*/