From c108b7f99cbd77703df1f3198dba43930cb48e7b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 31 Mar 2020 13:46:02 -0700 Subject: [PATCH] early givup #3604 Signed-off-by: Nikolaj Bjorner --- src/solver/parallel_tactic.cpp | 12 ++++++++---- 1 file changed, 8 insertions(+), 4 deletions(-) diff --git a/src/solver/parallel_tactic.cpp b/src/solver/parallel_tactic.cpp index 891b42809..34d20b843 100644 --- a/src/solver/parallel_tactic.cpp +++ b/src/solver/parallel_tactic.cpp @@ -183,6 +183,7 @@ class parallel_tactic : public tactic { ref m_solver; // solver state unsigned m_depth; // number of nested calls to cubing double m_width; // estimate of fraction of problem handled by state + bool m_giveup; public: solver_state(ast_manager* m, solver* s, params_ref const& p): @@ -192,7 +193,8 @@ class parallel_tactic : public tactic { m_params(p), m_solver(s), m_depth(0), - m_width(1.0) + m_width(1.0), + m_giveup(false) { } @@ -264,7 +266,9 @@ class parallel_tactic : public tactic { bool giveup() { std::string r = get_solver().reason_unknown(); - return r == "(incomplete quantifiers)"; + std::string inc("(incomplete"); + m_giveup |= r.compare(0, inc.size(), inc) == 0; + return m_giveup; } void assert_cube(expr_ref_vector const& cube) { @@ -309,7 +313,7 @@ class parallel_tactic : public tactic { } bool canceled() { - return m().canceled(); + return m_giveup || m().canceled(); } std::ostream& display(std::ostream& out) { @@ -469,7 +473,7 @@ private: case l_false: report_unsat(s); return; } if (canceled(s)) return; - if (s.giveup()) return; + if (s.giveup()) { report_undef(s); return; } if (memory_pressure()) { goto simplify_again;