rustsat-cadical 0.7.4

Interface to the SAT solver CaDiCaL for the RustSAT library.
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
147
148
149
150
151
152
153
154
155
156

// CaDiCaL C API Extension (Christoph Jabs)
// To be included at the bottom of `ccadical.cpp`

extern "C" {

int ccadical_add_mem(CCaDiCaL *wrapper, int lit) {
  try {
    ((Wrapper *)wrapper)->solver->add(lit);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int ccadical_assume_mem(CCaDiCaL *wrapper, int lit) {
  try {
    ((Wrapper *)wrapper)->solver->assume(lit);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int ccadical_constrain_mem(CCaDiCaL *wrapper, int lit) {
  try {
    ((Wrapper *)wrapper)->solver->constrain(lit);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int ccadical_solve_mem(CCaDiCaL *wrapper) {
  try {
    return ((Wrapper *)wrapper)->solver->solve();
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int ccadical_configure(CCaDiCaL *ptr, const char *name) {
  return ((Wrapper *)ptr)->solver->configure(name);
}

void ccadical_phase(CCaDiCaL *ptr, int lit) {
  ((Wrapper *)ptr)->solver->phase(lit);
}

void ccadical_unphase(CCaDiCaL *ptr, int lit) {
  ((Wrapper *)ptr)->solver->unphase(lit);
}

int ccadical_vars(CCaDiCaL *ptr) { return ((Wrapper *)ptr)->solver->vars(); }

int ccadical_set_option_ret(CCaDiCaL *wrapper, const char *name, int val) {
  return ((Wrapper *)wrapper)->solver->set(name, val);
}

int ccadical_limit_ret(CCaDiCaL *wrapper, const char *name, int val) {
  return ((Wrapper *)wrapper)->solver->limit(name, val);
}

int64_t ccadical_redundant(CCaDiCaL *wrapper) {
  return ((Wrapper *)wrapper)->solver->redundant();
}

int ccadical_simplify_rounds(CCaDiCaL *wrapper, int rounds) {
  return ((Wrapper *)wrapper)->solver->simplify(rounds);
}

int ccadical_reserve(CCaDiCaL *wrapper, int min_max_var) {
  try {
    ((Wrapper *)wrapper)->solver->reserve(min_max_var);
    return 0;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

int64_t ccadical_propagations(CCaDiCaL *wrapper) {
  return ((Wrapper *)wrapper)->solver->propagations();
}

int64_t ccadical_decisions(CCaDiCaL *wrapper) {
  return ((Wrapper *)wrapper)->solver->decisions();
}

int64_t ccadical_conflicts(CCaDiCaL *wrapper) {
  return ((Wrapper *)wrapper)->solver->conflicts();
}

#ifdef FLIP
int ccadical_flip(CCaDiCaL *wrapper, int lit) {
  return ((Wrapper *)wrapper)->solver->flip(lit);
}

int ccadical_flippable(CCaDiCaL *wrapper, int lit) {
  return ((Wrapper *)wrapper)->solver->flippable(lit);
}
#endif

#ifdef PYSAT_PROPCHECK
int ccadical_propcheck(CCaDiCaL *wrapper, const int *assumps,
                       size_t assumps_len, int psaving,
                       void (*prop_cb)(void *, int), void *cb_data) {
  try {
    if (((Wrapper *)wrapper)
            ->solver->prop_check(assumps, assumps_len, psaving, prop_cb,
                                 cb_data)) {
      return 10;
    }
    return 20;
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}
#endif

#ifdef PROPAGATE
int ccadical_propagate(CCaDiCaL *wrapper) {
  try {
    return ((Wrapper *)wrapper)->solver->propagate();
  } catch (std::bad_alloc &) {
    return OUT_OF_MEM;
  }
}

void ccadical_get_entrailed_literals(CCaDiCaL *wrapper,
                                     void (*entrailed_cb)(void *, int),
                                     void *cb_data) {
  std::vector<int> entrailed{};
  ((Wrapper *)wrapper)->solver->get_entrailed_literals(entrailed);
  for (int lit : entrailed) {
    entrailed_cb(cb_data, lit);
  }
}
#endif

#ifndef NTRACING
int ccadical_trace_api_calls(CCaDiCaL *wrapper, const char *path) {
  FILE *trace_file = fopen(path, "w");
  if (!trace_file)
    return 1;
  ((Wrapper *)wrapper)->solver->trace_api_calls(trace_file);
  return 0;
}
#endif

int ccadical_trace_proof_path(CCaDiCaL *wrapper, const char *path) {
  return ((Wrapper *)wrapper)->solver->trace_proof(path);
}
}

#ifdef TRACER
#include "ctracer.cpp"
#endif