mirror of
https://github.com/Z3Prover/z3
synced 2026-04-02 09:58:59 +00:00
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>
This commit is contained in:
copilot-swe-agent[bot]
parent
7c440341c7
commit
8904fdaaf8
5 changed files with 76 additions and 119 deletions
|
|
@ -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
|
||||
|
|
|
|||
60
src/ast/simplifiers/nnf_simplifier.h
Normal file
60
src/ast/simplifiers/nnf_simplifier.h
Normal file
|
|
@ -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));
|
||||
}
|
||||
};
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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);
|
||||
}
|
||||
|
|
@ -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)")
|
||||
*/
|
||||
|
||||
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue