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

early givup #3604

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-31 13:46:02 -07:00
parent 98b43322b1
commit c108b7f99c
1 changed files with 8 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/solver/parallel_tactic.cpp
View file

@ -183,6 +183,7 @@ class parallel_tactic : public tactic {
ref<solver> m_solver; // solver state ref<solver> m_solver; // solver state
unsigned m_depth; // number of nested calls to cubing unsigned m_depth; // number of nested calls to cubing
double m_width; // estimate of fraction of problem handled by state double m_width; // estimate of fraction of problem handled by state
bool m_giveup;
public: public:
solver_state(ast_manager* m, solver* s, params_ref const& p): solver_state(ast_manager* m, solver* s, params_ref const& p):
@ -192,7 +193,8 @@ class parallel_tactic : public tactic {
m_params(p), m_params(p),
m_solver(s), m_solver(s),
m_depth(0), 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() { bool giveup() {
std::string r = get_solver().reason_unknown(); 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) { void assert_cube(expr_ref_vector const& cube) {
@ -309,7 +313,7 @@ class parallel_tactic : public tactic {
} }
bool canceled() { bool canceled() {
return m().canceled(); return m_giveup || m().canceled();
} }
std::ostream& display(std::ostream& out) { std::ostream& display(std::ostream& out) {
@ -469,7 +473,7 @@ private:
case l_false: report_unsat(s); return; case l_false: report_unsat(s); return;
} }
if (canceled(s)) return; if (canceled(s)) return;
if (s.giveup()) return; if (s.giveup()) { report_undef(s); return; }
if (memory_pressure()) { if (memory_pressure()) {
goto simplify_again; goto simplify_again;