mirror of
https://github.com/Z3Prover/z3
synced 2025-11-13 01:21:14 +00:00
0a93ff515d
* Introduce X-macro-based trace tag definition - Created trace_tags.def to centralize TRACE tag definitions - Each tag includes a symbolic name and description - Set up enum class TraceTag for type-safe usage in TRACE macros * Add script to generate Markdown documentation from trace_tags.def - Python script parses trace_tags.def and outputs trace_tags.md * Refactor TRACE_NEW to prepend TraceTag and pass enum to is_trace_enabled * trace: improve trace tag handling system with hierarchical tagging - Introduce hierarchical tag-class structure: enabling a tag class activates all child tags - Unify TRACE, STRACE, SCTRACE, and CTRACE under enum TraceTag - Implement initial version of trace_tag.def using X(tag, tag_class, description) (class names and descriptions to be refined in a future update) * trace: replace all string-based TRACE tags with enum TraceTag - Migrated all TRACE, STRACE, SCTRACE, and CTRACE macros to use enum TraceTag values instead of raw string literals * trace : add cstring header * trace : Add Markdown documentation generation from trace_tags.def via mk_api_doc.py * trace : rename macro parameter 'class' to 'tag_class' and remove Unicode comment in trace_tags.h. * trace : Add TODO comment for future implementation of tag_class activation * trace : Disable code related to tag_class until implementation is ready (#7663).
113 lines
3.1 KiB
C++
113 lines
3.1 KiB
C++
/*++
|
|
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);
|
|
}
|