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

Remove old der_tactic implementation; rename mk_der2_tactic to mk_der_tactic

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-22 00:40:49 +00:00
parent c78b3d872d
commit 7c4a3b2c1b
2 changed files with 3 additions and 79 deletions
Download patch file Download diff file Expand all files Collapse all files

72
src/tactic/core/der_tactic.cpp
View file

@ -14,74 +14,4 @@ Author:
Leonardo de Moura (leonardo) 2012-10-20
--*/
#include "ast/rewriter/der.h"
#include "tactic/tactical.h"
class der_tactic : public tactic {
struct imp {
ast_manager & m_manager;
der_rewriter m_r;
imp(ast_manager & m):
m_manager(m),
m_r(m) {
}
ast_manager & m() const { return m_manager; }
void reset() {
m_r.reset();
}
void operator()(goal & g) {
tactic_report report("der", g);
expr_ref new_curr(m());
proof_ref new_pr(m());
unsigned idx = 0;
for (auto [curr, dep, pr] : g) {
if (g.inconsistent())
break;
m_r(curr, new_curr, new_pr);
new_pr = m().mk_modus_ponens(pr, new_pr);
g.update(idx++, new_curr, new_pr, dep);
}
g.elim_redundancies();
}
};
imp * m_imp;
public:
der_tactic(ast_manager & m) {
m_imp = alloc(imp, m);
}
tactic * translate(ast_manager & m) override {
return alloc(der_tactic, m);
}
~der_tactic() override {
dealloc(m_imp);
}
char const* name() const override { return "der"; }
void operator()(goal_ref const & in,
goal_ref_buffer & result) override {
(*m_imp)(*(in.get()));
in->inc_depth();
result.push_back(in.get());
}
void cleanup() override {
ast_manager & m = m_imp->m();
imp * d = alloc(imp, m);
std::swap(d, m_imp);
dealloc(d);
}
};
tactic * mk_der_tactic(ast_manager & m) {
return alloc(der_tactic, m);
}
#include "tactic/core/der_tactic.h"

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

@ -52,12 +52,7 @@ equality resolution rule takes the form:
#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()) {
inline tactic * mk_der_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);
@ -65,8 +60,7 @@ inline tactic * mk_der2_tactic(ast_manager & m, params_ref const & p = params_re
}
/*
ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m)")
ADD_TACTIC("der2", "destructive equality resolution.", "mk_der2_tactic(m, p)")
ADD_TACTIC("der", "destructive equality resolution.", "mk_der_tactic(m, p)")
ADD_SIMPLIFIER("der", "destructive equality resolution.", "alloc(der_simplifier, m, p, s)")
*/