From 8904fdaaf8c9769c44ae57487d72121a845ef3f5 Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 28 Mar 2026 22:33:38 +0000 Subject: [PATCH] Convert nnf/snf tactics to dependent_expr_state_tactic with nnf_simplifier Agent-Logs-Url: https://github.com/Z3Prover/z3/sessions/799df8c8-e146-4a9b-9e1c-1cacf5ad3126 Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/ast/simplifiers/CMakeLists.txt | 1 + src/ast/simplifiers/nnf_simplifier.h | 60 ++++++++++++++ src/tactic/core/CMakeLists.txt | 1 - src/tactic/core/nnf_tactic.cpp | 113 --------------------------- src/tactic/core/nnf_tactic.h | 20 +++-- 5 files changed, 76 insertions(+), 119 deletions(-) create mode 100644 src/ast/simplifiers/nnf_simplifier.h delete mode 100644 src/tactic/core/nnf_tactic.cpp diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt index d43bbe203..4588302c2 100644 --- a/src/ast/simplifiers/CMakeLists.txt +++ b/src/ast/simplifiers/CMakeLists.txt @@ -38,6 +38,7 @@ z3_add_component(simplifiers blast_term_ite_simplifier.h elim_bounds.h elim_term_ite.h + nnf_simplifier.h pull_nested_quantifiers.h push_ite.h randomizer.h diff --git a/src/ast/simplifiers/nnf_simplifier.h b/src/ast/simplifiers/nnf_simplifier.h new file mode 100644 index 000000000..99f68df45 --- /dev/null +++ b/src/ast/simplifiers/nnf_simplifier.h @@ -0,0 +1,60 @@ +/*++ +Copyright (c) 2024 Microsoft Corporation + +Module Name: + + nnf_simplifier.h + +Abstract: + + NNF simplifier + +Author: + + Nikolaj Bjorner (nbjorner) 2024-01-01 + +--*/ +#pragma once + +#include "ast/simplifiers/dependent_expr_state.h" +#include "ast/normal_forms/nnf.h" +#include "ast/normal_forms/defined_names.h" + +class nnf_simplifier : public dependent_expr_simplifier { + params_ref m_params; + +public: + nnf_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& s) + : dependent_expr_simplifier(m, s), m_params(p) {} + + char const* name() const override { return "nnf"; } + + bool supports_proofs() const override { return true; } + + void updt_params(params_ref const& p) override { m_params.append(p); } + + void collect_param_descrs(param_descrs& r) override { nnf::get_param_descrs(r); } + + void reduce() override { + defined_names dnames(m); + nnf local_nnf(m, dnames, m_params); + + expr_ref_vector defs(m); + proof_ref_vector def_prs(m); + expr_ref new_curr(m); + proof_ref new_pr(m); + + for (unsigned idx : indices()) { + auto const& d = m_fmls[idx]; + local_nnf(d.fml(), defs, def_prs, new_curr, new_pr); + m_fmls.update(idx, dependent_expr(m, new_curr, mp(d.pr(), new_pr), d.dep())); + } + + for (unsigned i = 0; i < defs.size(); ++i) + m_fmls.add(dependent_expr(m, defs.get(i), def_prs.get(i), nullptr)); + + unsigned num_extra_names = dnames.get_num_names(); + for (unsigned i = 0; i < num_extra_names; ++i) + m_fmls.model_trail().hide(dnames.get_name_decl(i)); + } +}; diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt index 8ab41f155..08b46ce4f 100644 --- a/src/tactic/core/CMakeLists.txt +++ b/src/tactic/core/CMakeLists.txt @@ -6,7 +6,6 @@ z3_add_component(core_tactics ctx_simplify_tactic.cpp elim_term_ite_tactic.cpp elim_uncnstr_tactic.cpp - nnf_tactic.cpp occf_tactic.cpp pb_preprocess_tactic.cpp propagate_values_tactic.cpp diff --git a/src/tactic/core/nnf_tactic.cpp b/src/tactic/core/nnf_tactic.cpp deleted file mode 100644 index b7d5a92a4..000000000 --- a/src/tactic/core/nnf_tactic.cpp +++ /dev/null @@ -1,113 +0,0 @@ -/*++ -Copyright (c) 2011 Microsoft Corporation - -Module Name: - - nnf_tactic.cpp - -Abstract: - - NNF tactic - -Author: - - Leonardo de Moura (leonardo) 2011-12-28. - -Revision History: - ---*/ -#include "ast/normal_forms/nnf.h" -#include "tactic/tactical.h" -#include "ast/converters/generic_model_converter.h" - -class nnf_tactic : public tactic { - params_ref m_params; - nnf * m_nnf; - - struct set_nnf { - nnf_tactic & m_owner; - - set_nnf(nnf_tactic & owner, nnf & n): - m_owner(owner) { - m_owner.m_nnf = &n; - } - - ~set_nnf() { - m_owner.m_nnf = nullptr; - } - }; -public: - nnf_tactic(params_ref const & p): - m_params(p), - m_nnf(nullptr) { - TRACE(nnf, tout << "nnf_tactic constructor: " << p << "\n";); - } - - tactic * translate(ast_manager & m) override { - return alloc(nnf_tactic, m_params); - } - - char const* name() const override { return "nnf"; } - - void updt_params(params_ref const & p) override { m_params.append(p); } - - void collect_param_descrs(param_descrs & r) override { nnf::get_param_descrs(r); } - - void operator()(goal_ref const & g, goal_ref_buffer & result) override { - TRACE(nnf, tout << "params: " << m_params << "\n"; g->display(tout);); - tactic_report report("nnf", *g); - bool produce_proofs = g->proofs_enabled(); - - ast_manager & m = g->m(); - defined_names dnames(m); - nnf local_nnf(m, dnames, m_params); - set_nnf setter(*this, local_nnf); - - expr_ref_vector defs(m); - proof_ref_vector def_prs(m); - - expr_ref new_curr(m); - proof_ref new_pr(m); - - unsigned sz = g->size(); - for (unsigned i = 0; !g->inconsistent() && i < sz; ++i) { - expr * curr = g->form(i); - local_nnf(curr, defs, def_prs, new_curr, new_pr); - if (produce_proofs) { - proof * pr = g->pr(i); - new_pr = m.mk_modus_ponens(pr, new_pr); - } - g->update(i, new_curr, new_pr, g->dep(i)); - } - - sz = defs.size(); - for (unsigned i = 0; !g->inconsistent() && i < sz; ++i) { - if (produce_proofs) - g->assert_expr(defs.get(i), def_prs.get(i), nullptr); - else - g->assert_expr(defs.get(i), nullptr, nullptr); - } - g->inc_depth(); - result.push_back(g.get()); - unsigned num_extra_names = dnames.get_num_names(); - if (num_extra_names > 0 && !g->inconsistent()) { - generic_model_converter * fmc = alloc(generic_model_converter, m, "nnf"); - g->add(fmc); - for (unsigned i = 0; i < num_extra_names; ++i) - fmc->hide(dnames.get_name_decl(i)); - } - } - - void cleanup() override {} -}; - -tactic * mk_snf_tactic(ast_manager & m, params_ref const & p) { - return alloc(nnf_tactic, p); -} - -tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p) { - params_ref new_p(p); - new_p.set_sym("mode", symbol("full")); - TRACE(nnf, tout << "mk_nnf: " << new_p << "\n";); - return using_params(mk_snf_tactic(m, p), new_p); -} diff --git a/src/tactic/core/nnf_tactic.h b/src/tactic/core/nnf_tactic.h index 083380be8..cc90a09de 100644 --- a/src/tactic/core/nnf_tactic.h +++ b/src/tactic/core/nnf_tactic.h @@ -57,16 +57,26 @@ Once all negations are pushed inside, the resulting formula is in NNF. --*/ #pragma once -#include "util/params.h" -class ast_manager; -class tactic; +#include "tactic/dependent_expr_state_tactic.h" +#include "ast/simplifiers/nnf_simplifier.h" -tactic * mk_snf_tactic(ast_manager & m, params_ref const & p = params_ref()); -tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref()); +inline tactic * mk_snf_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(nnf_simplifier, m, p, s); + }); +} + +inline tactic * mk_nnf_tactic(ast_manager & m, params_ref const & p = params_ref()) { + params_ref new_p(p); + new_p.set_sym("mode", symbol("full")); + return using_params(mk_snf_tactic(m, new_p), new_p); +} /* ADD_TACTIC("snf", "put goal in skolem normal form.", "mk_snf_tactic(m, p)") ADD_TACTIC("nnf", "put goal in negation normal form.", "mk_nnf_tactic(m, p)") + ADD_SIMPLIFIER("nnf", "put formula in negation normal form.", "alloc(nnf_simplifier, m, p, s)") */