Repository navigation
Expand file tree
/
Copy pathminisat.cpp
More file actions
155 lines (134 loc) · 5.38 KB
/
Copy pathminisat.cpp
File metadata and controls
155 lines (134 loc) · 5.38 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
#include "minisat/core/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(lbool(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(lbool(polarity), dvar);
}
return ret;
}
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; }
}