mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-04 10:20:23 +00:00
Code Activity

set synth solver check as last resort

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2023-08-12 20:22:12 -07:00
parent 93833d1045
commit 31677a0570
3 changed files with 16 additions and 11 deletions
Download patch file Download diff file Expand all files Collapse all files

25
src/sat/smt/euf_solver.cpp
View file

@ -147,7 +147,7 @@ namespace euf {
else if (rf.get_family_id() == fid) else if (rf.get_family_id() == fid)
ext = alloc(recfun::solver, *this); ext = alloc(recfun::solver, *this);
else if (m.mk_family_id("synth") == fid) else if (m.mk_family_id("synth") == fid)
ext = alloc(synth::solver, *this); m_synth_solver = ext = alloc(synth::solver, *this);
if (ext) if (ext)
add_solver(ext); add_solver(ext);
@ -592,6 +592,12 @@ namespace euf {
default: break; default: break;
} }
}; };
auto should_continue = [&]() {
return num_nodes < m_egraph.num_nodes() || cont || s().inconsistent();
};
auto should_giveup = [&]() {
return give_up || (m_qsolver && m_config.m_arith_ignore_int);
};
if (merge_shared_bools()) if (merge_shared_bools())
cont = true; cont = true;
for (unsigned i = 0; i < m_solvers.size(); ++i) { for (unsigned i = 0; i < m_solvers.size(); ++i) {
@ -600,28 +606,25 @@ namespace euf {
m_reason_unknown = "canceled"; m_reason_unknown = "canceled";
return sat::check_result::CR_GIVEUP; return sat::check_result::CR_GIVEUP;
} }
if (e == m_qsolver) if (e == m_qsolver || e == m_synth_solver)
continue; continue;
apply_solver(e); apply_solver(e);
if (s().inconsistent()) if (s().inconsistent())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
} }
if (should_continue())
if (s().inconsistent())
return sat::check_result::CR_CONTINUE;
if (cont)
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
if (m_qsolver && !m_config.m_arith_ignore_int) if (m_qsolver && !m_config.m_arith_ignore_int)
apply_solver(m_qsolver); apply_solver(m_qsolver);
if (num_nodes < m_egraph.num_nodes()) if (should_continue())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
if (cont) if (m_synth_solver)
apply_solver(m_synth_solver);
if (should_continue())
return sat::check_result::CR_CONTINUE; return sat::check_result::CR_CONTINUE;
TRACE("after_search", s().display(tout);); TRACE("after_search", s().display(tout););
if (give_up) if (should_giveup())
return sat::check_result::CR_GIVEUP;
if (m_qsolver && m_config.m_arith_ignore_int)
return sat::check_result::CR_GIVEUP; return sat::check_result::CR_GIVEUP;
return sat::check_result::CR_DONE; return sat::check_result::CR_DONE;
} }

1
src/sat/smt/euf_solver.h
View file

@ -140,6 +140,7 @@ namespace euf {
void* m_on_clause_ctx = nullptr; void* m_on_clause_ctx = nullptr;
user_solver::solver* m_user_propagator = nullptr; user_solver::solver* m_user_propagator = nullptr;
th_solver* m_qsolver = nullptr; th_solver* m_qsolver = nullptr;
th_solver* m_synth_solver = nullptr;
unsigned m_generation = 0; unsigned m_generation = 0;
std::string m_reason_unknown; std::string m_reason_unknown;
mutable ptr_vector<expr> m_todo; mutable ptr_vector<expr> m_todo;

1
src/sat/smt/synth_solver.cpp
View file

@ -246,6 +246,7 @@ namespace synth {
replace(result); replace(result);
th_rewriter rw(m); th_rewriter rw(m);
rw(result); rw(result);
IF_VERBOSE(2, ctx.display(verbose_stream()));
IF_VERBOSE(0, verbose_stream() << "simplifying: " << result << "\n"); IF_VERBOSE(0, verbose_stream() << "simplifying: " << result << "\n");
result = simplify_condition(result.get()); result = simplify_condition(result.get());
IF_VERBOSE(0, verbose_stream() << result << "\n"); IF_VERBOSE(0, verbose_stream() << result << "\n");