mirror of
https://github.com/Z3Prover/z3
synced 2026-01-19 00:38:57 +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.2 KiB
C++
113 lines
3.2 KiB
C++
/*++
|
|
Copyright (c) 2014 Microsoft Corporation
|
|
|
|
Module Name:
|
|
|
|
opt_pareto.cpp
|
|
|
|
Abstract:
|
|
|
|
Pareto front utilities
|
|
|
|
Author:
|
|
|
|
Nikolaj Bjorner (nbjorner) 2014-4-24
|
|
|
|
Notes:
|
|
|
|
|
|
--*/
|
|
|
|
#include "opt/opt_pareto.h"
|
|
#include "ast/ast_pp.h"
|
|
#include "ast/ast_util.h"
|
|
#include "model/model_smt2_pp.h"
|
|
|
|
namespace opt {
|
|
|
|
// ---------------------
|
|
// GIA pareto algorithm
|
|
|
|
lbool gia_pareto::operator()() {
|
|
expr_ref fml(m);
|
|
lbool is_sat = m_solver->check_sat(0, nullptr);
|
|
if (is_sat == l_true) {
|
|
{
|
|
m_solver->get_model(m_model);
|
|
solver::scoped_push _s(*m_solver.get());
|
|
while (is_sat == l_true) {
|
|
if (!m.inc()) {
|
|
return l_undef;
|
|
}
|
|
if (!m_model)
|
|
return l_undef;
|
|
m_solver->get_labels(m_labels);
|
|
m_model->set_model_completion(true);
|
|
IF_VERBOSE(1,
|
|
model_ref mdl(m_model);
|
|
cb.fix_model(mdl);
|
|
model_smt2_pp(verbose_stream() << "new model:\n", m, *mdl, 0););
|
|
// TBD: we can also use local search to tune solution coordinate-wise.
|
|
mk_dominates();
|
|
is_sat = m_solver->check_sat(0, nullptr);
|
|
if (is_sat == l_true) m_solver->get_model(m_model);
|
|
}
|
|
}
|
|
if (is_sat == l_undef) {
|
|
return l_undef;
|
|
}
|
|
SASSERT(is_sat == l_false);
|
|
is_sat = l_true;
|
|
mk_not_dominated_by();
|
|
}
|
|
return is_sat;
|
|
}
|
|
|
|
void pareto_base::mk_dominates() {
|
|
unsigned sz = cb.num_objectives();
|
|
expr_ref fml(m);
|
|
expr_ref_vector gt(m), fmls(m);
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
fmls.push_back(cb.mk_ge(i, m_model));
|
|
gt.push_back(cb.mk_gt(i, m_model));
|
|
}
|
|
fmls.push_back(mk_or(gt));
|
|
fml = mk_and(fmls);
|
|
IF_VERBOSE(10, verbose_stream() << "dominates: " << fml << "\n";);
|
|
TRACE(opt, model_smt2_pp(tout << fml << "\n", m, *m_model, 0););
|
|
m_solver->assert_expr(fml);
|
|
}
|
|
|
|
void pareto_base::mk_not_dominated_by() {
|
|
unsigned sz = cb.num_objectives();
|
|
expr_ref fml(m);
|
|
expr_ref_vector le(m);
|
|
for (unsigned i = 0; i < sz; ++i) {
|
|
le.push_back(cb.mk_le(i, m_model));
|
|
}
|
|
fml = m.mk_not(mk_and(le));
|
|
IF_VERBOSE(10, verbose_stream() << "not dominated by: " << fml << "\n";);
|
|
TRACE(opt, tout << fml << "\n";);
|
|
m_solver->assert_expr(fml);
|
|
}
|
|
|
|
// ---------------------------------
|
|
// OIA algorithm (without filtering)
|
|
|
|
lbool oia_pareto::operator()() {
|
|
solver::scoped_push _s(*m_solver.get());
|
|
lbool is_sat = m_solver->check_sat(0, nullptr);
|
|
if (!m.inc()) {
|
|
is_sat = l_undef;
|
|
}
|
|
if (is_sat == l_true) {
|
|
m_solver->get_model(m_model);
|
|
m_solver->get_labels(m_labels);
|
|
m_model->set_model_completion(true);
|
|
mk_not_dominated_by();
|
|
}
|
|
return is_sat;
|
|
}
|
|
|
|
}
|
|
|