FindMUS/lib/Marco.cpp at develop · MiniZinc/FindMUS · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
#include <iostream>
#include <set>
#include <string>

#include "Marco.h"

namespace HierMUS {
using std::set;
using std::string;

Marco::Marco(SubProblem &p, MUSEnumOptions &mo, SubsetMap *m)
    : MusEnumerator(p, mo, m) {
  setFrontier(subsetMap->getLeavesSelector());
}

Marco::~Marco() {}

void Marco::setFrontier(const Selection &f) {
  log("New frontier");
  frontier = f;
}

bool Marco::search() {
  if (mopts.timedOut())
    return false;
  while (true) {
    if (mopts.timedOut())
      return false;
    stats.madeMapCall();
    Selection s = subsetMap->getSelection(frontier);

    if (s.size() == 0)
      break;

    stats.madeSatCheck();
    if (!subProblem.check(s)) {
      stats.foundUnSatSet();
      NodeSet empty_crits;
      if (!shrink(s, empty_crits))
        return false;
      frontier.setMinimal(false);
      subsetMap->blockSupersets(s);
      if (s.isLeaves()) {
        current_mus = s;
        return true;
      }
      if (unsat_callback) {
        unsat_callback(s);
        if (mopts.map_enum_focus_mode) {
          // Pretend that we have exhausted this frontier
          return false;
        }
      }
    } else {
      subsetMap->blockSubsets(s);
      stats.foundSatSet();
      if (stats.shouldRestart())
        return false;
    }
  }
  if (frontier.knownMinimal() && frontier.isLeaves()) {
    current_mus = frontier;
    frontier = {};
    frontier.setMinimal(false);
    return true;
  }

  return false;
}

} // namespace HierMUS