Repository navigation
Expand file tree
/
Copy pathminicard.cpp
More file actions
162 lines (141 loc) · 5.6 KB
/
Copy pathminicard.cpp
File metadata and controls
162 lines (141 loc) · 5.6 KB
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
157
158
159
160
161
162
#include "minicard/minicard/Solver.h"
using namespace Minisat;
inline Lit itoLit(int i) {
bool sign = i < 0;
int var = (sign) ? -i-1 : i-1; // 0-based variable numbering
return (sign) ? ~mkLit(var) : mkLit(var);
}
inline int Littoi(Lit l) {
return (var(l)+1) * (sign(l) ? -1 : 1);
}
extern "C" {
Solver* Solver_new() { return new Solver(); }
void Solver_delete(Solver* s) { delete s; }
int nVars(Solver* s) { return s->nVars(); }
int nClauses(Solver* s) { return s->nClauses(); }
// Controls the level of phase saving (0=none, 1=limited, 2=full).
void setPhaseSaving(Solver* s, int ps) { s->phase_saving = ps; }
// Control whether random polarities are used (overridden if vars are created with a user polarity other than Undef)
void setRndPol(Solver* s, bool val) { s->rnd_pol = val; }
// Control whether variables are intialized with a random initial activity
// (default: False)
void setRndInitAct(Solver* s, bool val) { s->rnd_init_act = val; }
// Initialize the solver's random seed
void setRndSeed(Solver* s, double seed) { assert(seed != 0.0); s->random_seed = seed; }
// polarity: 0=False, 1=True, 2=Undef
int newVar(Solver* s, uint8_t polarity, bool dvar=true) { return s->newVar(polarity, dvar); }
int newVars(Solver* s, int number, uint8_t polarity, bool dvar=true) {
int ret;
for (int i = 0 ; i < number ; i++) {
ret = s->newVar(polarity, dvar);
}
return ret;
}
bool addAtMost(Solver* s, int len, int* lits, int k) {
vec<Lit> atmost;
for (int i = 0 ; i < len ; i++) {
atmost.push( itoLit(lits[i]) );
}
return s->addAtMost(atmost, k);
}
bool addClause(Solver* s, int len, int* lits) {
vec<Lit> clause;
for (int i = 0 ; i < len ; i++) {
clause.push( itoLit(lits[i]) );
}
return s->addClause(clause);
}
bool addUnit(Solver* s, int lit) {
return s->addClause(itoLit(lit));
}
bool solve(Solver* s) { return s->solve(); }
bool solve_assumptions(Solver* s, int len, int* lits) {
vec<Lit> assumptions;
for (int i = 0 ; i < len ; i++) {
assumptions.push( itoLit(lits[i]) );
}
return s->solve(assumptions);
}
bool check_complete(Solver* s, const int len, const int* lits, const bool pos) {
int n = s->nVars();
vec<Lit> assumptions;
bool * specified = new bool[n+1]();
for (int i = 0 ; i < len ; i++) {
assumptions.push( itoLit(lits[i]) );
specified[pos ? lits[i] : -lits[i]] = true;
}
for (int i = 1 ; i < n+1 ; i++) {
if (!specified[i]) {
assumptions.push( itoLit(pos ? -i : i) );
}
}
delete[] specified;
return s->solve(assumptions);
}
bool simplify(Solver* s) { return s->simplify(); }
// This is fairly slow to call from Python.
// It is better to copy the whole model over with fillModel()
// if you will be looking at most or all values, anyway.
int modelValue(Solver* s, int i) { return s->modelValue(i-1) != l_False; }
void fillModel(Solver* s, int* model, int from, int to) {
for (int i = from ; i < to ; i++) {
model[i-from] = s->modelValue(i) != l_False;
}
}
int getModelTrues(Solver* s, int* trues, int from, int to, int offset) {
int count = 0;
for (int i = from ; i < to ; i++) {
if (s->modelValue(i) == l_True) trues[count++] = i - from + offset;
}
return count;
}
// returns the size of the current conflict
int conflictSize(Solver* s) {
return s->conflict.size();
}
// returns a core with 0-based counting
// (i.e., first clause is 0, etc.)
// (subtracts given number of original variables from conflict variables)
int unsatCore(Solver* s, int nv, int* core, int offset) {
for (int i = 0 ; i < s->conflict.size() ; i++) {
core[i] = var(s->conflict[i]) - nv + offset;
}
return s->conflict.size();
}
// fills an array w/ any literals known to be implied by the current formula
// (i.e., all 0-level assignments)
// returns number of elements in the filled array
int getImplies(Solver* s, int* assigns) {
vec<Lit> empty;
vec<Lit> outvec;
s->implies(empty, outvec, true);
int len = outvec.size();
for (int i = 0 ; i < len ; i++) {
assigns[i] = Littoi(outvec[i]);
}
return len;
}
// fills an array w/ any literals known to be implied by the current formula
// and any given assumptions (i.e., all 0-level assignments)
// returns number of elements in the filled array
int getImplies_assumptions(Solver* s, int* assigns, int* assumps, int assumps_size) {
vec<Lit> assumptions;
for (int i = 0 ; i < assumps_size ; i++) {
assumptions.push( itoLit(assumps[i]) );
}
vec<Lit> outvec;
s->implies(assumptions, outvec, true);
int len = outvec.size();
for (int i = 0 ; i < len ; i++) {
assigns[i] = Littoi(outvec[i]);
}
return len;
}
// getter methods for accessing solver statistics
uint64_t get_solves(Solver* s) { return s->solves; }
uint64_t get_starts(Solver* s) { return s->starts; }
uint64_t get_decisions(Solver* s) { return s->decisions; }
uint64_t get_rnd_decisions(Solver* s) { return s->rnd_decisions; }
uint64_t get_propagations(Solver* s) { return s->propagations; }
uint64_t get_conflicts(Solver* s) { return s->conflicts; }
}