From 31677a057014b5f3187d19c705762d51c3194a00 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Aug 2023 20:22:12 -0700 Subject: [PATCH] set synth solver check as last resort Signed-off-by: Nikolaj Bjorner --- src/sat/smt/euf_solver.cpp | 25 ++++++++++++++----------- src/sat/smt/euf_solver.h | 1 + src/sat/smt/synth_solver.cpp | 1 + 3 files changed, 16 insertions(+), 11 deletions(-) diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp index ee6d42a99..020ace414 100644 --- a/src/sat/smt/euf_solver.cpp +++ b/src/sat/smt/euf_solver.cpp @@ -147,7 +147,7 @@ namespace euf { else if (rf.get_family_id() == fid) ext = alloc(recfun::solver, *this); else if (m.mk_family_id("synth") == fid) - ext = alloc(synth::solver, *this); + m_synth_solver = ext = alloc(synth::solver, *this); if (ext) add_solver(ext); @@ -592,6 +592,12 @@ namespace euf { 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()) cont = true; for (unsigned i = 0; i < m_solvers.size(); ++i) { @@ -600,29 +606,26 @@ namespace euf { m_reason_unknown = "canceled"; return sat::check_result::CR_GIVEUP; } - if (e == m_qsolver) + if (e == m_qsolver || e == m_synth_solver) continue; apply_solver(e); if (s().inconsistent()) return sat::check_result::CR_CONTINUE; } - - if (s().inconsistent()) - return sat::check_result::CR_CONTINUE; - if (cont) + if (should_continue()) return sat::check_result::CR_CONTINUE; if (m_qsolver && !m_config.m_arith_ignore_int) apply_solver(m_qsolver); - if (num_nodes < m_egraph.num_nodes()) + if (should_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; 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_DONE; } diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h index a9dc20e0e..50d542aaa 100644 --- a/src/sat/smt/euf_solver.h +++ b/src/sat/smt/euf_solver.h @@ -140,6 +140,7 @@ namespace euf { void* m_on_clause_ctx = nullptr; user_solver::solver* m_user_propagator = nullptr; th_solver* m_qsolver = nullptr; + th_solver* m_synth_solver = nullptr; unsigned m_generation = 0; std::string m_reason_unknown; mutable ptr_vector m_todo; diff --git a/src/sat/smt/synth_solver.cpp b/src/sat/smt/synth_solver.cpp index f9d1cd152..76dd2c5b7 100644 --- a/src/sat/smt/synth_solver.cpp +++ b/src/sat/smt/synth_solver.cpp @@ -246,6 +246,7 @@ namespace synth { replace(result); th_rewriter rw(m); rw(result); + IF_VERBOSE(2, ctx.display(verbose_stream())); IF_VERBOSE(0, verbose_stream() << "simplifying: " << result << "\n"); result = simplify_condition(result.get()); IF_VERBOSE(0, verbose_stream() << result << "\n");