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
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
|
/* Boolector: Satisfiablity Modulo Theories (SMT) solver. *
* Copyright (C) 2011-2012 Armin Biere.
*
* All rights reserved.
*
* This file is part of Boolector.
* See COPYING for more information on using this software.
*/
#ifdef BTOR_USE_MINISAT
#ifndef __STDC_LIMIT_MACROS
#define __STDC_LIMIT_MACROS
#endif
#ifndef __STDC_FORMAT_MACROS
#define __STDC_FORMAT_MACROS
#endif
#include "../minisat/minisat/simp/SimpSolver.h"
extern "C" {
#include "btorminisat.h"
#include "btorsat.h"
#include <cassert>
#include <cstring>
#include <cstdio>
using namespace Minisat;
class BtorMiniSAT : public SimpSolver {
vec<Lit> assumptions, clause;
int szfmap;
signed char * fmap;
bool nomodel;
Lit import (int lit) {
assert (0 < abs (lit) && abs (lit) <= nVars ());
return mkLit (Var (abs (lit) - 1), (lit < 0));
}
void reset () { if (fmap) delete [] fmap, fmap = 0, szfmap = 0; }
void ana () {
fmap = new signed char [szfmap = nVars ()];
memset (fmap, 0, szfmap);
for (int i = 0; i < conflict.size (); i++) {
int tmp = var (conflict[i]);
assert (0 <= tmp && tmp < szfmap);
fmap[tmp] = 1;
}
}
public:
BtorMiniSAT () : szfmap (0), fmap (0), nomodel (true) { }
~BtorMiniSAT () { reset (); }
int inc () {
nomodel = true;
int res = newVar ();
assert (0 <= res && res == nVars () - 1);
return res + 1;
}
void assume (int lit) { nomodel = true; assumptions.push (import (lit)); }
void add (int lit) {
nomodel = true;
if (lit) clause.push (import (lit));
else addClause (clause), clause.clear ();
}
unsigned long long calls;
int sat (bool simp) {
calls++;
reset ();
bool res = solve (assumptions, simp);
assumptions.clear ();
nomodel = !res;
return res ? 10 : 20;
}
int failed (int lit) {
if (!fmap) ana ();
int tmp = var (import (lit));
assert (0 <= tmp && tmp < nVars ());
return fmap [ tmp ];
}
int fixed (int lit) {
Var v = var (import (lit));
int idx = v, res;
assert (0 <= idx && idx < nVars ());
lbool val = assigns[idx];
if (val == l_Undef || level (v)) res = 0;
else res = (val == l_True) ? 1 : -1;
if (lit < 0) res = -res;
return res;
}
int deref (int lit) {
if (nomodel) return fixed (lit);
lbool res = modelValue (import (lit));
return (res == l_True) ? 1 : -1;
}
};
void * btor_minisat_init (BtorSATMgr *) { return new BtorMiniSAT (); }
const char * btor_minisat_version (void) { return "unknown"; }
void btor_minisat_add (BtorSATMgr * smgr, int lit) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
solver->add (lit);
}
int btor_minisat_sat (BtorSATMgr * smgr, int limit) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
(void) limit;
return solver->sat (!smgr->inc_required);
}
int btor_minisat_deref (BtorSATMgr * smgr, int lit) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
return solver->deref (lit);
}
int btor_minisat_repr (BtorSATMgr * smgr, int lit) {
(void) smgr;
return lit;
}
void btor_minisat_reset (BtorSATMgr * smgr) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
delete solver;
}
int btor_minisat_inc_max_var (BtorSATMgr * smgr) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
return solver->inc ();
}
int btor_minisat_variables (BtorSATMgr * smgr) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
return solver->nVars ();
}
void btor_minisat_assume (BtorSATMgr * smgr, int lit) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
solver->assume (lit);
}
int btor_minisat_fixed (BtorSATMgr * smgr, int lit) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
return solver->fixed (lit);
}
int btor_minisat_failed (BtorSATMgr * smgr, int lit) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
return solver->failed (lit);
}
void btor_minisat_set_output (BtorSATMgr *, FILE *) { }
void btor_minisat_set_prefix (BtorSATMgr *, const char *) { }
void btor_minisat_enable_verbosity (BtorSATMgr * smgr) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
solver->verbosity = 1;
}
void btor_minisat_stats (BtorSATMgr * smgr) {
BtorMiniSAT * solver = (BtorMiniSAT*) BTOR_GET_SOLVER_SAT (smgr);
printf (
"[minisat] calls %llu\n"
"[minisat] restarts %llu\n"
"[minisat] conflicts %llu\n"
"[minisat] decisions %llu\n"
"[minisat] propagations %llu\n",
(unsigned long long) solver->calls,
(unsigned long long) solver->starts,
(unsigned long long) solver->conflicts,
(unsigned long long) solver->decisions,
(unsigned long long) solver->propagations);
fflush (stdout);
}
int btor_minisat_changed (BtorSATMgr *) { return 1; }
int btor_minisat_inconsistent (BtorSATMgr *) { return 0; }
};
#endif
|
