mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-09 10:30:59 +00:00
Code Activity

Convert cofactor-term-ite tactic to also expose as a simplifier

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:52:01 +00:00
parent e8db5204c0
commit c18db6080a
1 changed files with 49 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

52
src/tactic/core/cofactor_term_ite_tactic.h
View file

@ -29,11 +29,57 @@ It hoists nested if-then-else expressions inside terms into the top level of the
#pragma once #pragma once
#include "util/params.h" #include "util/params.h"
class ast_manager; #include "tactic/tactic.h"
class tactic; #include "tactic/dependent_expr_state_tactic.h"
#include "ast/simplifiers/dependent_expr_state.h"
#include "tactic/core/cofactor_elim_term_ite.h"
class cofactor_term_ite_simplifier : public dependent_expr_simplifier {
params_ref m_params;
cofactor_elim_term_ite m_elim_ite;
public:
cofactor_term_ite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s)
: dependent_expr_simplifier(m, s), m_params(p), m_elim_ite(m, p) {}
char const* name() const override { return "cofactor-term-ite"; }
void updt_params(params_ref const& p) override {
m_params.append(p);
m_elim_ite.updt_params(m_params);
}
void collect_param_descrs(param_descrs& r) override {
m_elim_ite.collect_param_descrs(r);
}
bool supports_proofs() const override { return false; }
void reduce() override {
expr_ref new_fml(m);
for (unsigned idx : indices()) {
auto const& d = m_fmls[idx];
m_elim_ite(d.fml(), new_fml);
if (new_fml != d.fml())
m_fmls.update(idx, dependent_expr(m, new_fml, nullptr, d.dep()));
}
}
};
inline dependent_expr_simplifier* mk_cofactor_term_ite_simplifier(
ast_manager& m, params_ref const& p, dependent_expr_state& s) {
return alloc(cofactor_term_ite_simplifier, m, p, s);
}
inline tactic* mk_cofactor_term_ite2_tactic(ast_manager& m, params_ref const& p = params_ref()) {
return alloc(dependent_expr_state_tactic, m, p, mk_cofactor_term_ite_simplifier);
}
tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref()); tactic * mk_cofactor_term_ite_tactic(ast_manager & m, params_ref const & p = params_ref());
/* /*
ADD_TACTIC("cofactor-term-ite", "eliminate term if-the-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)") ADD_TACTIC("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_tactic(m, p)")
ADD_TACTIC("cofactor-term-ite2", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite2_tactic(m, p)")
ADD_SIMPLIFIER("cofactor-term-ite", "eliminate term if-then-else using cofactors.", "mk_cofactor_term_ite_simplifier(m, p, s)")
*/ */