File tree 2 files changed +23
-1
lines changed
2 files changed +23
-1
lines changed Original file line number Diff line number Diff line change 12
12
13
13
// decision procedure wrapper for boolean propositional logics
14
14
15
+ #include < stdint.h>
16
+
15
17
#include < util/message.h>
16
18
#include < util/threeval.h>
17
19
Original file line number Diff line number Diff line change @@ -115,13 +115,17 @@ void satcheck_minisat2_baset<T>::lcnf(const bvt &bv)
115
115
clause_counter++;
116
116
}
117
117
118
+ #ifndef _WIN32
119
+
118
120
static Minisat::Solver *solver_to_interrupt=nullptr ;
119
121
120
122
static void interrupt_solver (int signum)
121
123
{
122
124
solver_to_interrupt->interrupt ();
123
125
}
124
126
127
+ #endif
128
+
125
129
template <typename T>
126
130
propt::resultt satcheck_minisat2_baset<T>::prop_solve()
127
131
{
@@ -161,6 +165,10 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
161
165
Minisat::vec<Minisat::Lit> solver_assumptions;
162
166
convert (assumptions, solver_assumptions);
163
167
168
+ using Minisat::lbool;
169
+
170
+ #ifndef _WIN32
171
+
164
172
void (*old_handler)(int )=SIG_ERR;
165
173
166
174
if (time_limit_seconds!=0 )
@@ -173,7 +181,6 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
173
181
alarm (time_limit_seconds);
174
182
}
175
183
176
- using Minisat::lbool;
177
184
lbool solver_result=solver->solveLimited (solver_assumptions);
178
185
179
186
if (old_handler!=SIG_ERR)
@@ -183,6 +190,19 @@ propt::resultt satcheck_minisat2_baset<T>::prop_solve()
183
190
solver_to_interrupt=solver;
184
191
}
185
192
193
+ #else // _WIN32
194
+
195
+ if (time_limit_seconds!=0 )
196
+ {
197
+ messaget::warning () <<
198
+ " Time limit ignored (not supported on Win32 yet)" << messaget::eom;
199
+ }
200
+
201
+ lbool solver_result=
202
+ solver->solve (solver_assumptions) ? l_True : l_False;
203
+
204
+ #endif
205
+
186
206
if (solver_result==l_True)
187
207
{
188
208
messaget::status () <<
You can’t perform that action at this time.
0 commit comments