Skip to content

Commit 36dedf1

Browse files
ahmed-irfanahmed-irfan
authored
hack: undef status_interrupted to fix windows build (#467)
* hack: undef status_interrupted to fix windows build * follow Mark's suggestion
1 parent 1b9d96e commit 36dedf1

File tree

14 files changed

+90
-80
lines changed

14 files changed

+90
-80
lines changed

‎src/api/yices_api.c

+12-12
Original file line numberDiff line numberDiff line change
@@ -8510,7 +8510,7 @@ EXPORTED int32_t yices_push(context_t *ctx) {
85108510
}
85118511
assert(context_status(ctx) == STATUS_UNSAT);
85128512
// fall through
8513-
case STATUS_INTERRUPTED:
8513+
case YICES_STATUS_INTERRUPTED:
85148514
case STATUS_SEARCHING:
85158515
set_error_code(CTX_INVALID_OPERATION);
85168516
return -1;
@@ -8555,7 +8555,7 @@ EXPORTED int32_t yices_pop(context_t *ctx) {
85558555
switch (context_status(ctx)) {
85568556
case STATUS_UNKNOWN:
85578557
case STATUS_SAT:
8558-
case STATUS_INTERRUPTED:
8558+
case YICES_STATUS_INTERRUPTED:
85598559
context_clear(ctx);
85608560
break;
85618561

@@ -8699,7 +8699,7 @@ int32_t _o_yices_assert_formula(context_t *ctx, term_t t) {
86998699
break;
87008700

87018701
case STATUS_SEARCHING:
8702-
case STATUS_INTERRUPTED:
8702+
case YICES_STATUS_INTERRUPTED:
87038703
set_error_code(CTX_INVALID_OPERATION);
87048704
return -1;
87058705

@@ -8773,7 +8773,7 @@ EXPORTED int32_t yices_assert_formulas(context_t *ctx, uint32_t n, const term_t
87738773
break;
87748774

87758775
case STATUS_SEARCHING:
8776-
case STATUS_INTERRUPTED:
8776+
case YICES_STATUS_INTERRUPTED:
87778777
set_error_code(CTX_INVALID_OPERATION);
87788778
return -1;
87798779

@@ -8828,7 +8828,7 @@ EXPORTED int32_t yices_assert_blocking_clause(context_t *ctx) {
88288828
case STATUS_UNSAT:
88298829
case STATUS_IDLE:
88308830
case STATUS_SEARCHING:
8831-
case STATUS_INTERRUPTED:
8831+
case YICES_STATUS_INTERRUPTED:
88328832
set_error_code(CTX_INVALID_OPERATION);
88338833
return -1;
88348834

@@ -9029,13 +9029,13 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params)
90299029
params = &default_params;
90309030
}
90319031
stat = check_context(ctx, params);
9032-
if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
9032+
if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
90339033
context_cleanup(ctx);
90349034
}
90359035
break;
90369036

90379037
case STATUS_SEARCHING:
9038-
case STATUS_INTERRUPTED:
9038+
case YICES_STATUS_INTERRUPTED:
90399039
set_error_code(CTX_INVALID_OPERATION);
90409040
stat = STATUS_ERROR;
90419041
break;
@@ -9101,7 +9101,7 @@ smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param
91019101
break;
91029102

91039103
case STATUS_SEARCHING:
9104-
case STATUS_INTERRUPTED:
9104+
case YICES_STATUS_INTERRUPTED:
91059105
set_error_code(CTX_INVALID_OPERATION);
91069106
return STATUS_ERROR;
91079107

@@ -9136,7 +9136,7 @@ smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param
91369136

91379137
// call check
91389138
stat = check_context_with_assumptions(ctx, params, n, assumptions.data);
9139-
if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
9139+
if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
91409140
context_cleanup(ctx);
91419141
}
91429142

@@ -9212,7 +9212,7 @@ EXPORTED smt_status_t yices_check_context_with_model(context_t *ctx, const param
92129212
break;
92139213

92149214
case STATUS_SEARCHING:
9215-
case STATUS_INTERRUPTED:
9215+
case YICES_STATUS_INTERRUPTED:
92169216
set_error_code(CTX_INVALID_OPERATION);
92179217
return STATUS_ERROR;
92189218

@@ -9232,7 +9232,7 @@ EXPORTED smt_status_t yices_check_context_with_model(context_t *ctx, const param
92329232

92339233
// call check
92349234
stat = check_context_with_model(ctx, params, mdl, n, t);
9235-
if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
9235+
if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
92369236
context_cleanup(ctx);
92379237
}
92389238

@@ -10316,7 +10316,7 @@ static smt_status_t yices_ef_check_formulas(const term_t f[], uint32_t n, smt_lo
1031610316
break;
1031710317

1031810318
case EF_STATUS_INTERRUPTED:
10319-
stat = STATUS_INTERRUPTED;
10319+
stat = YICES_STATUS_INTERRUPTED;
1032010320
break;
1032110321

1032210322
case EF_STATUS_SUBST_ERROR:

‎src/context/context.h

+4-4
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,7 @@ extern int32_t assert_blocking_clause(context_t *ctx);
206206
* - if parameters is NULL, the default values are used
207207
*
208208
* return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
209-
* STATUS_INTERRUPTED (these codes are defined in smt_core.h)
209+
* YICES_STATUS_INTERRUPTED (these codes are defined in smt_core.h)
210210
*/
211211
extern smt_status_t check_context(context_t *ctx, const param_t *parameters);
212212

@@ -219,7 +219,7 @@ extern smt_status_t check_context(context_t *ctx, const param_t *parameters);
219219
* - each a[i] must be defined in ctx->core
220220
*
221221
* return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
222-
* STATUS_INTERRUPTED
222+
* YICES_STATUS_INTERRUPTED
223223
*
224224
* If status is STATUS_UNSAT then the assumptions are inconsistent
225225
*/
@@ -235,7 +235,7 @@ extern smt_status_t check_context_with_assumptions(context_t *ctx, const param_t
235235
* - t = variables to use from the model (size = n)
236236
*
237237
* return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
238-
* STATUS_INTERRUPTED
238+
* YICES_STATUS_INTERRUPTED
239239
*
240240
* If status is STATUS_UNSAT then the context and model are inconsistent
241241
*/
@@ -434,7 +434,7 @@ extern int32_t context_process_formulas(context_t *ctx, uint32_t n, term_t *f);
434434
* STATUS_UNKNOWN
435435
* STATUS_SAT
436436
* STATUS_UNSAT
437-
* STATUS_INTERRUPTED
437+
* YICES_STATUS_INTERRUPTED
438438
*/
439439
static inline smt_status_t context_status(context_t *ctx) {
440440
if (ctx->arch == CTX_ARCH_MCSAT) {

‎src/context/context_solver.c

+7-7
Original file line numberDiff line numberDiff line change
@@ -149,7 +149,7 @@ static void search(smt_core_t *core, uint32_t conflict_bound, uint32_t *reduce_t
149149
uint32_t r_threshold;
150150
literal_t l;
151151

152-
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
152+
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
153153

154154
max_conflicts = num_conflicts(core) + conflict_bound;
155155
r_threshold = *reduce_threshold;
@@ -203,7 +203,7 @@ static void luby_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *red
203203
uint32_t r_threshold;
204204
literal_t l;
205205

206-
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
206+
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
207207

208208
max_conflicts = num_conflicts(core) + conflict_bound;
209209
r_threshold = *reduce_threshold;
@@ -262,7 +262,7 @@ static void special_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *
262262
uint32_t r_threshold;
263263
literal_t l;
264264

265-
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
265+
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);
266266

267267
max_conflicts = num_conflicts(core) + conflict_bound;
268268
r_threshold = *reduce_threshold;
@@ -666,7 +666,7 @@ smt_status_t precheck_context(context_t *ctx) {
666666
stat = smt_status(core);
667667

668668
assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
669-
stat == STATUS_INTERRUPTED);
669+
stat == YICES_STATUS_INTERRUPTED);
670670

671671
if (stat == STATUS_SEARCHING) {
672672
end_search_unknown(core);
@@ -703,7 +703,7 @@ smt_status_t check_with_delegate(context_t *ctx, const char *sat_solver, uint32_
703703
stat = smt_status(core);
704704

705705
assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
706-
stat == STATUS_INTERRUPTED);
706+
stat == YICES_STATUS_INTERRUPTED);
707707

708708
if (stat == STATUS_SEARCHING) {
709709
if (smt_easy_sat(core)) {
@@ -763,7 +763,7 @@ int32_t bitblast_then_export_to_dimacs(context_t *ctx, const char *filename, smt
763763
stat = smt_status(core);
764764

765765
assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
766-
stat == STATUS_INTERRUPTED);
766+
stat == YICES_STATUS_INTERRUPTED);
767767

768768
if (stat == STATUS_SEARCHING) {
769769
code = 1;
@@ -820,7 +820,7 @@ int32_t process_then_export_to_dimacs(context_t *ctx, const char *filename, smt_
820820
stat = smt_status(core);
821821

822822
assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
823-
stat == STATUS_INTERRUPTED);
823+
stat == YICES_STATUS_INTERRUPTED);
824824

825825
if (stat == STATUS_SEARCHING) {
826826
if (smt_easy_sat(core)) {

‎src/exists_forall/efsolver.c

+5-5
Original file line numberDiff line numberDiff line change
@@ -508,7 +508,7 @@ static context_t *get_forall_context(ef_solver_t *solver) {
508508
* - value[i] = a constant term mapped to evar[i] in the model
509509
* 2) code = STATUS_UNSAT: not satisfiable
510510
*
511-
* 3) other codes report an error of some kind or STATUS_INTERRUPTED
511+
* 3) other codes report an error of some kind or YICES_STATUS_INTERRUPTED
512512
*/
513513
static smt_status_t satisfy_context(ef_solver_t *solver, context_t *ctx, term_t *var, uint32_t n, term_t *value, model_t **model, bool is_exists) {
514514
smt_status_t stat;
@@ -829,7 +829,7 @@ static void ef_sample_constraint(ef_solver_t *solver, uint32_t i) {
829829
// no more samples for this constraints
830830
goto done;
831831

832-
case STATUS_INTERRUPTED:
832+
case YICES_STATUS_INTERRUPTED:
833833
solver->status = EF_STATUS_INTERRUPTED;
834834
goto done;
835835

@@ -1342,7 +1342,7 @@ static smt_status_t ef_solver_test_exists_model(ef_solver_t *solver, term_t doma
13421342
case STATUS_UNSAT:
13431343
break;
13441344

1345-
case STATUS_INTERRUPTED:
1345+
case YICES_STATUS_INTERRUPTED:
13461346
solver->status = EF_STATUS_INTERRUPTED;
13471347
break;
13481348

@@ -1389,7 +1389,7 @@ static void trace_candidate_check(ef_solver_t *solver, uint32_t i, smt_status_t
13891389
trace_printf(solver->trace, 4, "(EF: candidate passed constraint %"PRIu32")\n", i);
13901390
break;
13911391

1392-
case STATUS_INTERRUPTED:
1392+
case YICES_STATUS_INTERRUPTED:
13931393
trace_printf(solver->trace, 4, "(EF: candidate check was interrupted)\n");
13941394
break;
13951395

@@ -1549,7 +1549,7 @@ static void ef_solver_search(ef_solver_t *solver) {
15491549
solver->status = EF_STATUS_UNSAT;
15501550
break;
15511551

1552-
case STATUS_INTERRUPTED:
1552+
case YICES_STATUS_INTERRUPTED:
15531553
trace_puts(solver->trace, 4, "(EF: Interrupted)\n");
15541554
solver->status = EF_STATUS_INTERRUPTED;
15551555
break;

0 commit comments

Comments
 (0)