rustsat-cadical 0.7.5

Interface to the SAT solver CaDiCaL for the RustSAT library.
Documentation 
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
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146

#include "internal.hpp"

namespace CaDiCaL {

Limit::Limit () { memset (this, 0, sizeof *this); }

/*------------------------------------------------------------------------*/

double Internal::scale (double v) const {
  const double ratio = clause_variable_ratio ();
  const double factor = (ratio <= 2) ? 1.0 : log (ratio) / log (2);
  double res = factor * v;
  if (res < 1)
    res = 1;
  return res;
}

/*------------------------------------------------------------------------*/

Last::Last () { memset (this, 0, sizeof *this); }

/*------------------------------------------------------------------------*/

Inc::Inc () {
  memset (this, 0, sizeof *this);
  ticks = decisions = conflicts = -1; // unlimited
}

void Internal::limit_terminate (int l) {
  if (l <= 0 && !lim.terminate.forced) {
    LOG ("keeping unbounded terminate limit");
  } else if (l <= 0) {
    LOG ("reset terminate limit to be unbounded");
    lim.terminate.forced = 0;
  } else {
    lim.terminate.forced = l;
    LOG ("new terminate limit of %d calls", l);
  }
}

void Internal::limit_conflicts (int l) {
  if (l < 0 && inc.conflicts < 0) {
    LOG ("keeping unbounded conflict limit");
  } else if (l < 0) {
    LOG ("reset conflict limit to be unbounded");
    inc.conflicts = -1;
  } else {
    inc.conflicts = l;
    LOG ("new conflict limit of %d conflicts", l);
  }
}

void Internal::limit_decisions (int l) {
  if (l < 0 && inc.decisions < 0) {
    LOG ("keeping unbounded decision limit");
  } else if (l < 0) {
    LOG ("reset decision limit to be unbounded");
    inc.decisions = -1;
  } else {
    inc.decisions = l;
    LOG ("new decision limit of %d decisions", l);
  }
}

void Internal::limit_ticks (int64_t l) {
  if (l < 0 && inc.ticks < 0) {
    LOG ("keeping unbounded ticks limit");
  } else if (l < 0) {
    LOG ("reset ticks limit to be unbounded");
    inc.ticks = -1;
  } else {
    inc.ticks = l;
    LOG ("new ticks limit of %" PRId64 " ticks", l);
  }
}

void Internal::limit_preprocessing (int l) {
  if (l < 0) {
    LOG ("ignoring invalid preprocessing limit %d", l);
  } else if (!l) {
    LOG ("reset preprocessing limit to no preprocessing");
    inc.preprocessing = 0;
  } else {
    inc.preprocessing = l;
    LOG ("new preprocessing limit of %d preprocessing rounds", l);
  }
}

void Internal::limit_local_search (int l) {
  if (l < 0) {
    LOG ("ignoring invalid local search limit %d", l);
  } else if (!l) {
    LOG ("reset local search limit to no local search");
    inc.localsearch = 0;
  } else {
    inc.localsearch = l;
    LOG ("new local search limit of %d local search rounds", l);
  }
}

bool Internal::is_valid_limit (const char *name) {
  if (!strcmp (name, "terminate"))
    return true;
  if (!strcmp (name, "conflicts"))
    return true;
  if (!strcmp (name, "decisions"))
    return true;
  if (!strcmp (name, "preprocessing"))
    return true;
  if (!strcmp (name, "localsearch"))
    return true;
  if (!strcmp (name, "ticks"))
    return true;
  return false;
}

bool Internal::limit (const char *name, int l) {
  bool res = true;
  if (!strcmp (name, "terminate"))
    limit_terminate (l);
  else if (!strcmp (name, "conflicts"))
    limit_conflicts (l);
  else if (!strcmp (name, "decisions"))
    limit_decisions (l);
  else if (!strcmp (name, "preprocessing"))
    limit_preprocessing (l);
  else if (!strcmp (name, "localsearch"))
    limit_local_search (l);
  else if (!strcmp (name, "ticks"))
    limit_ticks (l);
  else
    res = false;
  return res;
}

void Internal::reset_limits () {
  LOG ("reset limits");
  limit_terminate (0);
  limit_conflicts (-1);
  limit_decisions (-1);
  limit_preprocessing (0);
  limit_local_search (0);
  limit_ticks (-1);
}

} // namespace CaDiCaL