* invoked from DepthSpec.cpp. * returning true means that we do eager backtracking. */
| 212 | * returning true means that we do eager backtracking. |
| 213 | */ |
| 214 | bool |
| 215 | DFSRndNumGenerator::eager_backtracking(int depth_needed) |
| 216 | { |
| 217 | if (current_pos_ <= 0) { |
| 218 | // all_done_ = true; |
| 219 | // Error::set_error(BACKTRACKING_ERROR); |
| 220 | // return true; |
| 221 | return false; |
| 222 | } |
| 223 | |
| 224 | int max_depth = CGOptions::max_exhaustive_depth(); |
| 225 | int remain_depth = max_depth - current_pos_; |
| 226 | if (remain_depth >= depth_needed) |
| 227 | return false; |
| 228 | |
| 229 | if (current_pos_ > decision_depth_) { |
| 230 | Error::set_error(BACKTRACKING_ERROR); |
| 231 | return true; |
| 232 | } |
| 233 | |
| 234 | // reset decision depth |
| 235 | decision_depth_ = current_pos_; |
| 236 | for (int i = current_pos_ + 1; i < max_depth; ++i) |
| 237 | states_[i]->set_init(false); |
| 238 | |
| 239 | Error::set_error(BACKTRACKING_ERROR); |
| 240 | return true; |
| 241 | } |
| 242 | |
| 243 | int |
| 244 | DFSRndNumGenerator::revisit_node(DFSRndNumGenerator::SearchState *state, int local_current_pos, |