Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

hack: undef status_interrupted to fix windows build #467

Merged
merged 2 commits into from
Oct 11, 2023
Merged

hack: undef status_interrupted to fix windows build #467

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
8638a19
hack: undef status_interrupted to fix windows build
ahmed-irfan Oct 10, 2023
4bea5b9
follow Mark's suggestion
ahmed-irfan Oct 10, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
24 changes: 12 additions & 12 deletions src/api/yices_api.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8510,7 +8510,7 @@ EXPORTED int32_t yices_push(context_t *ctx) {
}
assert(context_status(ctx) == STATUS_UNSAT);
// fall through
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
case STATUS_SEARCHING:
set_error_code(CTX_INVALID_OPERATION);
return -1;
Expand Down Expand Up @@ -8555,7 +8555,7 @@ EXPORTED int32_t yices_pop(context_t *ctx) {
switch (context_status(ctx)) {
case STATUS_UNKNOWN:
case STATUS_SAT:
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
context_clear(ctx);
break;

Expand Down Expand Up @@ -8699,7 +8699,7 @@ int32_t _o_yices_assert_formula(context_t *ctx, term_t t) {
break;

case STATUS_SEARCHING:
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
set_error_code(CTX_INVALID_OPERATION);
return -1;

Expand Down Expand Up @@ -8773,7 +8773,7 @@ EXPORTED int32_t yices_assert_formulas(context_t *ctx, uint32_t n, const term_t
break;

case STATUS_SEARCHING:
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
set_error_code(CTX_INVALID_OPERATION);
return -1;

Expand Down Expand Up @@ -8828,7 +8828,7 @@ EXPORTED int32_t yices_assert_blocking_clause(context_t *ctx) {
case STATUS_UNSAT:
case STATUS_IDLE:
case STATUS_SEARCHING:
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
set_error_code(CTX_INVALID_OPERATION);
return -1;

Expand Down Expand Up @@ -9029,13 +9029,13 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params)
params = &default_params;
}
stat = check_context(ctx, params);
if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
context_cleanup(ctx);
}
break;

case STATUS_SEARCHING:
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
set_error_code(CTX_INVALID_OPERATION);
stat = STATUS_ERROR;
break;
Expand Down Expand Up @@ -9101,7 +9101,7 @@ smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param
break;

case STATUS_SEARCHING:
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
set_error_code(CTX_INVALID_OPERATION);
return STATUS_ERROR;

Expand Down Expand Up @@ -9136,7 +9136,7 @@ smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param

// call check
stat = check_context_with_assumptions(ctx, params, n, assumptions.data);
if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
context_cleanup(ctx);
}

Expand Down Expand Up @@ -9212,7 +9212,7 @@ EXPORTED smt_status_t yices_check_context_with_model(context_t *ctx, const param
break;

case STATUS_SEARCHING:
case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
set_error_code(CTX_INVALID_OPERATION);
return STATUS_ERROR;

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

// call check
stat = check_context_with_model(ctx, params, mdl, n, t);
if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
context_cleanup(ctx);
}

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

case EF_STATUS_INTERRUPTED:
stat = STATUS_INTERRUPTED;
stat = YICES_STATUS_INTERRUPTED;
break;

case EF_STATUS_SUBST_ERROR:
Expand Down
8 changes: 4 additions & 4 deletions src/context/context.h
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -206,7 +206,7 @@ extern int32_t assert_blocking_clause(context_t *ctx);
* - if parameters is NULL, the default values are used
*
* return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
* STATUS_INTERRUPTED (these codes are defined in smt_core.h)
* YICES_STATUS_INTERRUPTED (these codes are defined in smt_core.h)
*/
extern smt_status_t check_context(context_t *ctx, const param_t *parameters);

Expand All @@ -219,7 +219,7 @@ extern smt_status_t check_context(context_t *ctx, const param_t *parameters);
* - each a[i] must be defined in ctx->core
*
* return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
* STATUS_INTERRUPTED
* YICES_STATUS_INTERRUPTED
*
* If status is STATUS_UNSAT then the assumptions are inconsistent
*/
Expand All @@ -235,7 +235,7 @@ extern smt_status_t check_context_with_assumptions(context_t *ctx, const param_t
* - t = variables to use from the model (size = n)
*
* return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
* STATUS_INTERRUPTED
* YICES_STATUS_INTERRUPTED
*
* If status is STATUS_UNSAT then the context and model are inconsistent
*/
Expand Down Expand Up @@ -434,7 +434,7 @@ extern int32_t context_process_formulas(context_t *ctx, uint32_t n, term_t *f);
* STATUS_UNKNOWN
* STATUS_SAT
* STATUS_UNSAT
* STATUS_INTERRUPTED
* YICES_STATUS_INTERRUPTED
*/
static inline smt_status_t context_status(context_t *ctx) {
if (ctx->arch == CTX_ARCH_MCSAT) {
Expand Down
14 changes: 7 additions & 7 deletions src/context/context_solver.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -149,7 +149,7 @@ static void search(smt_core_t *core, uint32_t conflict_bound, uint32_t *reduce_t
uint32_t r_threshold;
literal_t l;

assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);

max_conflicts = num_conflicts(core) + conflict_bound;
r_threshold = *reduce_threshold;
Expand Down Expand Up @@ -203,7 +203,7 @@ static void luby_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *red
uint32_t r_threshold;
literal_t l;

assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);

max_conflicts = num_conflicts(core) + conflict_bound;
r_threshold = *reduce_threshold;
Expand Down Expand Up @@ -262,7 +262,7 @@ static void special_search(smt_core_t *core, uint32_t conflict_bound, uint32_t *
uint32_t r_threshold;
literal_t l;

assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == STATUS_INTERRUPTED);
assert(smt_status(core) == STATUS_SEARCHING || smt_status(core) == YICES_STATUS_INTERRUPTED);

max_conflicts = num_conflicts(core) + conflict_bound;
r_threshold = *reduce_threshold;
Expand Down Expand Up @@ -666,7 +666,7 @@ smt_status_t precheck_context(context_t *ctx) {
stat = smt_status(core);

assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
stat == STATUS_INTERRUPTED);
stat == YICES_STATUS_INTERRUPTED);

if (stat == STATUS_SEARCHING) {
end_search_unknown(core);
Expand Down Expand Up @@ -703,7 +703,7 @@ smt_status_t check_with_delegate(context_t *ctx, const char *sat_solver, uint32_
stat = smt_status(core);

assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
stat == STATUS_INTERRUPTED);
stat == YICES_STATUS_INTERRUPTED);

if (stat == STATUS_SEARCHING) {
if (smt_easy_sat(core)) {
Expand Down Expand Up @@ -763,7 +763,7 @@ int32_t bitblast_then_export_to_dimacs(context_t *ctx, const char *filename, smt
stat = smt_status(core);

assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
stat == STATUS_INTERRUPTED);
stat == YICES_STATUS_INTERRUPTED);

if (stat == STATUS_SEARCHING) {
code = 1;
Expand Down Expand Up @@ -820,7 +820,7 @@ int32_t process_then_export_to_dimacs(context_t *ctx, const char *filename, smt_
stat = smt_status(core);

assert(stat == STATUS_UNSAT || stat == STATUS_SEARCHING ||
stat == STATUS_INTERRUPTED);
stat == YICES_STATUS_INTERRUPTED);

if (stat == STATUS_SEARCHING) {
if (smt_easy_sat(core)) {
Expand Down
10 changes: 5 additions & 5 deletions src/exists_forall/efsolver.c
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -508,7 +508,7 @@ static context_t *get_forall_context(ef_solver_t *solver) {
* - value[i] = a constant term mapped to evar[i] in the model
* 2) code = STATUS_UNSAT: not satisfiable
*
* 3) other codes report an error of some kind or STATUS_INTERRUPTED
* 3) other codes report an error of some kind or YICES_STATUS_INTERRUPTED
*/
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) {
smt_status_t stat;
Expand Down Expand Up @@ -829,7 +829,7 @@ static void ef_sample_constraint(ef_solver_t *solver, uint32_t i) {
// no more samples for this constraints
goto done;

case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
solver->status = EF_STATUS_INTERRUPTED;
goto done;

Expand Down Expand Up @@ -1342,7 +1342,7 @@ static smt_status_t ef_solver_test_exists_model(ef_solver_t *solver, term_t doma
case STATUS_UNSAT:
break;

case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
solver->status = EF_STATUS_INTERRUPTED;
break;

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

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

Expand Down Expand Up @@ -1549,7 +1549,7 @@ static void ef_solver_search(ef_solver_t *solver) {
solver->status = EF_STATUS_UNSAT;
break;

case STATUS_INTERRUPTED:
case YICES_STATUS_INTERRUPTED:
trace_puts(solver->trace, 4, "(EF: Interrupted)\n");
solver->status = EF_STATUS_INTERRUPTED;
break;
Expand Down
Loading