mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-31 03:32:28 +00:00
Code Activity

propagate value initialization to atoms

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-09-24 11:01:24 +03:00
parent 10dce45d8b
commit 95ab02aa4f
4 changed files with 53 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/nra_solver.cpp
View file

@ -135,7 +135,7 @@ struct solver::imp {
UNREACHABLE();
return l_undef;
}
for (auto const& m : m_nla_core.emons()) {
for (auto const &m : m_nla_core.emons()) {
if (!check_monic(m)) {
IF_VERBOSE(0, verbose_stream() << "monic " << m << " violated\n";
lra.constraints().display(verbose_stream()));

52
src/smt/smt_context.cpp
View file

@ -3768,6 +3768,55 @@ namespace smt {
TRACE(literal_occ, display_literal_num_occs(tout););
}
void context::initialize_values() {
if (m_values.empty())
return;
expr_safe_replace sub(m);
for (auto const &[var, value] : m_values) {
initialize_value(var, value);
sub.insert(var, value);
}
for (unsigned v = 0; v < get_num_bool_vars(); ++v) {
expr_ref var(bool_var2expr(v), m);
if (!var)
continue;
sub(var);
m_rewriter(var);
if (m.is_true(var)) {
m_bdata[v].m_phase_available = true;
m_bdata[v].m_phase = true;
}
else if (m.is_false(var)) {
m_bdata[v].m_phase_available = true;
m_bdata[v].m_phase = false;
}
}
for (clause *cls : m_aux_clauses) {
literal undef_lit = null_literal;
bool is_true = false;
for (auto lit : *cls) {
auto v = lit.var();
if (m_bdata[v].m_phase_available) {
bool phase = m_bdata[v].m_phase;
if (lit.sign() != phase) {
is_true = true;
break;
}
}
else {
undef_lit = lit;
}
}
if (!is_true && undef_lit != null_literal) {
auto v = undef_lit.var();
m_bdata[v].m_phase_available = true;
m_bdata[v].m_phase = !undef_lit.sign();
}
}
}
void context::end_search() {
m_case_split_queue->end_search_eh();
}
@ -3820,8 +3869,7 @@ namespace smt {
TRACE(search, display(tout); display_enodes_lbls(tout););
TRACE(search_detail, m_asserted_formulas.display(tout););
init_search();
for (auto const& [var, value] : m_values)
initialize_value(var, value);
initialize_values();
flet<bool> l(m_searching, true);
TRACE(after_init_search, display(tout););

1
src/smt/smt_context.h
View file

@ -269,6 +269,7 @@ namespace smt {
// ----------------------------------
vector<std::pair<expr_ref, expr_ref>> m_values;
void initialize_value(expr* var, expr* value);
void initialize_values();
// -----------------------------------