diff --git a/configure.ac b/configure.ac index b66ebacd7..15b4a97b6 100644 --- a/configure.ac +++ b/configure.ac @@ -870,10 +870,6 @@ fi AC_SUBST(THREAD_SAFE) if test "x$thread_safe" = xyes ; then THREAD_SAFE=1 - # iam: the aim is to eventually eliminate this restriction, but not before the 2.6.2 release. - if test $use_mcsat = yes ; then - AC_MSG_ERROR([Building with both --enable-mcsat and --enable-thread-safety is currently not supported.]) - fi fi dnl diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 6442da188..47f1dd452 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -8669,10 +8669,10 @@ static inline bool yices_assert_formula_checks(term_t t) { MT_PROTECT(bool, __yices_globals.lock, _o_yices_assert_formula_checks(t)); } -EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { +int32_t _o_yices_assert_formula(context_t *ctx, term_t t) { int32_t code; - if (! yices_assert_formula_checks(t)) { + if (! _o_yices_assert_formula_checks(t)) { return -1; } @@ -8711,7 +8711,7 @@ EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { assert(context_status(ctx) == STATUS_IDLE); - code = assert_formula(ctx, t); + code = _o_assert_formula(ctx, t); if (code < 0) { // error during internalization convert_internalization_error(code); @@ -8722,6 +8722,10 @@ EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { return 0; } +EXPORTED int32_t yices_assert_formula(context_t *ctx, term_t t) { + MT_PROTECT(int32_t, __yices_globals.lock, + _o_yices_assert_formula(ctx, t)); +} @@ -9054,23 +9058,19 @@ static bool _o_unsat_core_check_assumptions(uint32_t n, const term_t a[]) { return check_good_terms(__yices_globals.manager, n, a) && check_boolean_args(__yices_globals.manager, n, a); } -static bool unsat_core_check_assumptions(uint32_t n, const term_t a[]) { - MT_PROTECT(bool, __yices_globals.lock, _o_unsat_core_check_assumptions(n, a)); -} - /* * Check context with assumptions * - n = number of assumptions * - a[0] ... a[n-1] = n assumptions. All of them must be Boolean terms. */ -EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t a[]) { +smt_status_t _o_yices_check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const term_t a[]) { param_t default_params; ivector_t assumptions; smt_status_t stat; uint32_t i; literal_t l; - if (!unsat_core_check_assumptions(n, a)) { + if (!_o_unsat_core_check_assumptions(n, a)) { return STATUS_ERROR; // Bad assumptions } @@ -9113,8 +9113,6 @@ EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const assert(context_status(ctx) == STATUS_IDLE); - yices_obtain_mutex(); - // convert the assumptions to n literals init_ivector(&assumptions, n); for (i=0; i void bv_subexplainer_construct(bv_subexplainer_t* exp, const char* name, plugin_context_t* ctx, watch_list_manager_t* wlm, bv_evaluator_t* eval) { @@ -169,10 +170,10 @@ void bv_explainer_normalize_conflict(bv_explainer_t* exp, ivector_t* conflict_ou } void bv_explainer_check_conflict(bv_explainer_t* exp, const ivector_t* conflict) { - context_t* ctx = yices_new_context(NULL); + context_t* ctx = _o_yices_new_context(NULL); uint32_t i; for (i = 0; i < conflict->size; ++ i) { - yices_assert_formula(ctx, conflict->data[i]); + _o_yices_assert_formula(ctx, conflict->data[i]); } smt_status_t result = yices_check_context(ctx, NULL); (void) result; diff --git a/src/mcsat/bv/bv_utils.h b/src/mcsat/bv/bv_utils.h index 121fb4912..39aae56e2 100644 --- a/src/mcsat/bv/bv_utils.h +++ b/src/mcsat/bv/bv_utils.h @@ -35,6 +35,7 @@ #include "mcsat/tracing.h" #include "mcsat/value.h" #include "yices.h" +#include "api/yices_api_lock_free.h" /** Types of bitvector terms */ typedef enum { @@ -467,8 +468,8 @@ static inline bool check_rewrite(plugin_context_t* ctx, term_t old, term_t t){ if (t == old) return true; term_manager_t* tm = ctx->tm; - context_t* yctx = yices_new_context(NULL); - yices_assert_formula(yctx, mk_neq(tm, old, t)); + context_t* yctx = _o_yices_new_context(NULL); + _o_yices_assert_formula(yctx, mk_neq(tm, old, t)); smt_status_t output = yices_check_context(yctx, NULL); bool result = (output == STATUS_UNSAT); if (!result && ctx_trace_enabled(ctx, "mcsat::bv::arith::ctz")) { @@ -479,7 +480,7 @@ bool check_rewrite(plugin_context_t* ctx, term_t old, term_t t){ ctx_trace_term(ctx, t); assert(false); } - yices_free_context(yctx); + _o_yices_free_context(yctx); return result; } diff --git a/src/mcsat/bv/explain/eq_ext_con.c b/src/mcsat/bv/explain/eq_ext_con.c index f61b1a486..d49821673 100644 --- a/src/mcsat/bv/explain/eq_ext_con.c +++ b/src/mcsat/bv/explain/eq_ext_con.c @@ -33,6 +33,7 @@ #include "mcsat/eq/equality_graph.h" #include "yices.h" +#include "api/yices_api_lock_free.h" #include "eq_ext_con.h" @@ -1543,7 +1544,7 @@ term_t explain_propagation(bv_subexplainer_t* this, const ivector_t* reasons_in, if (ok) { // Concat the terms if (to_concat.size > 1) { - result_subst = yices_bvconcat(to_concat.size, to_concat.data); + result_subst = _o_yices_bvconcat(to_concat.size, to_concat.data); } else { result_subst = to_concat.data[0]; } diff --git a/src/mcsat/bv/explain/full_bv_sat.c b/src/mcsat/bv/explain/full_bv_sat.c index 3dccadfee..7d255fb29 100644 --- a/src/mcsat/bv/explain/full_bv_sat.c +++ b/src/mcsat/bv/explain/full_bv_sat.c @@ -142,8 +142,8 @@ void bb_sat_solver_add_variable(bb_sat_solver_t* solver, variable_t var, bool wi term_t var_fresh; term_kind_t kind = term_kind(solver->yices_ctx->terms, var_term); if (kind != UNINTERPRETED_TERM) { - type_t var_type = yices_type_of_term(var_term); - var_fresh = yices_new_uninterpreted_term(var_type); + type_t var_type = _o_yices_type_of_term(var_term); + var_fresh = _o_yices_new_uninterpreted_term(var_type); } else { var_fresh = var_term; } @@ -163,7 +163,7 @@ void bb_sat_solver_assert_term(bb_sat_solver_t* solver, variable_t assertion_ter fprintf(out, " previously \n"); ctx_trace_term(solver->ctx, assertion_term); } - yices_assert_formula(solver->yices_ctx, assertion_term); + _o_yices_assert_formula(solver->yices_ctx, assertion_term); } /** @@ -276,7 +276,7 @@ void bb_sat_solver_solve_and_get_core(bb_sat_solver_t* solver, term_vector_t* co } // Check the assumptions (should be unsat) - smt_status_t status = yices_check_context_with_assumptions(solver->yices_ctx, NULL, assumptions.size, assumptions.data); + smt_status_t status = _o_yices_check_context_with_assumptions(solver->yices_ctx, NULL, assumptions.size, assumptions.data); (void) status; assert(status == STATUS_UNSAT); diff --git a/src/mcsat/conflict.c b/src/mcsat/conflict.c index 648f169a6..d097a97d4 100644 --- a/src/mcsat/conflict.c +++ b/src/mcsat/conflict.c @@ -29,19 +29,20 @@ #include "mcsat/tracing.h" #include "yices.h" +#include "api/yices_api_lock_free.h" #include #define CONFLICT_DEFAULT_ELEMENT_SIZE 100 void conflict_check(conflict_t* conflict) { ctx_config_t* config = yices_new_config(); - context_t* ctx = yices_new_context(config); + context_t* ctx = _o_yices_new_context(config); uint32_t i; const ivector_t* literals = &conflict->disjuncts.element_list; for (i = 0; i < literals->size; ++i) { term_t literal = literals->data[i]; literal = opposite_term(literal); - int32_t ret = yices_assert_formula(ctx, literal); + int32_t ret = _o_yices_assert_formula(ctx, literal); if (ret != 0) { // unsupported by regular yices fprintf(stderr, "skipping conflict (ret)\n"); @@ -52,7 +53,7 @@ void conflict_check(conflict_t* conflict) { smt_status_t result = yices_check_context(ctx, NULL); (void) result; assert(result == STATUS_UNSAT); - yices_free_context(ctx); + _o_yices_free_context(ctx); yices_free_config(config); } diff --git a/src/mcsat/preprocessor.c b/src/mcsat/preprocessor.c index 3ccebcc4a..07171b1fe 100644 --- a/src/mcsat/preprocessor.c +++ b/src/mcsat/preprocessor.c @@ -34,6 +34,7 @@ #include "context/context_types.h" #include "yices.h" +#include "api/yices_api_lock_free.h" void preprocessor_construct(preprocessor_t* pre, term_table_t* terms, jmp_buf* handler, const mcsat_options_t* options) { pre->terms = terms; @@ -459,8 +460,8 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is size = 0; } } - current_pre = yices_bvconcat(n_vars, vars); - term_t eq = yices_eq(current, current_pre); + current_pre = _o_yices_bvconcat(n_vars, vars); + term_t eq = _o_yices_eq(current, current_pre); preprocessor_mark_eq(pre, eq, current); } } @@ -598,7 +599,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is } else { type_t arg_pre_type = term_type(pre->terms, arg_pre); term_t arg_pre_is_positive = mk_arith_term_geq0(&pre->tm, arg_pre); - term_t arg_negative = yices_neg(arg_pre); + term_t arg_negative = _o_yices_neg(arg_pre); current_pre = mk_ite(&pre->tm, arg_pre_is_positive, arg_pre, arg_negative, arg_pre_type); } break; @@ -718,7 +719,7 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out, bool is trace_term_ln(pre->tracer, terms, arg_pre); } // For simplification purposes use API - current_pre = yices_bitextract(arg_pre, index); + current_pre = _o_yices_bitextract(arg_pre, index); assert(current_pre != NULL_TERM); } } diff --git a/src/mt/yices_locks_posix.c b/src/mt/yices_locks_posix.c index cf63e99d4..827e7f584 100644 --- a/src/mt/yices_locks_posix.c +++ b/src/mt/yices_locks_posix.c @@ -20,30 +20,38 @@ #include #include #include +#include #include "yices_locks.h" -//I see NDEBUG and DEBUG in the code; which is it? -#ifdef DEBUG -static pthread_mutexattr_t mta; -static pthread_mutexattr_t* mattr = &mta; -#else -static pthread_mutexattr_t* mattr = NULL; -#endif +static void print_error(const char *caller, const char *syscall, int errnum) { + char buffer[64]; + strerror_r(errnum, buffer, sizeof(buffer)); + fprintf(stderr, "%s failed: %s returned %d: %s\n", caller, syscall, + errnum, buffer); +} int32_t create_yices_lock(yices_lock_t* lock){ int32_t retcode; -#ifdef DEBUG - retcode = pthread_mutexattr_settype(&mta, PTHREAD_MUTEX_ERRORCHECK); - if(retcode){ - fprintf(stderr, "create_yices_lock failed: pthread_mutexattr_settype returned %d\n", retcode); - } +#ifndef NDEBUG + pthread_mutexattr_t mta; + pthread_mutexattr_t *mattr = &mta; +#else + pthread_mutexattr_t *mattr = NULL; +#endif + +#ifndef NDEBUG + retcode = pthread_mutexattr_init(mattr); + if(retcode) + print_error("create_yices_lock", "pthread_mutexattr_init", retcode); + retcode = pthread_mutexattr_settype(mattr, PTHREAD_MUTEX_ERRORCHECK); + if(retcode) + print_error("create_yices_lock", "pthread_mutextattr_settype", retcode); #endif retcode = pthread_mutex_init(lock, mattr); - if(retcode){ - fprintf(stderr, "create_yices_lock failed: pthread_mutex_init returned %d\n", retcode); - } + if(retcode) + print_error("create_yices_lock", "pthread_mutex_init", retcode); assert(retcode == 0); return retcode; } @@ -54,7 +62,7 @@ int32_t try_yices_lock(yices_lock_t* lock){ if(retcode == EBUSY){ return 1; } else { - fprintf(stderr, "try_yices_lock failed: pthread_mutex_trylock returned %d\n", retcode); + print_error("try_yices_lock", "pthread_mutex_trylock", retcode); } return -1; } @@ -65,7 +73,7 @@ int32_t try_yices_lock(yices_lock_t* lock){ int32_t get_yices_lock(yices_lock_t* lock){ int32_t retcode = pthread_mutex_lock(lock); if(retcode){ - fprintf(stderr, "get_yices_lock failed: pthread_mutex_lock returned %d\n", retcode); + print_error("get_yices_lock", "pthread_mutex_lock", retcode); } assert(retcode == 0); return retcode; @@ -74,7 +82,7 @@ int32_t get_yices_lock(yices_lock_t* lock){ int32_t release_yices_lock(yices_lock_t* lock){ int32_t retcode = pthread_mutex_unlock(lock); if(retcode){ - fprintf(stderr, "release_yices_lock failed: pthread_mutex_unlock returned %d\n", retcode); + print_error("release_yices_lock", "pthread_mutex_unlock", retcode); } assert(retcode == 0); return retcode; @@ -83,7 +91,7 @@ int32_t release_yices_lock(yices_lock_t* lock){ void destroy_yices_lock(yices_lock_t* lock){ int32_t retcode = pthread_mutex_destroy(lock); if(retcode){ - fprintf(stderr, "destroy_yices_lock failed: pthread_mutex_destroy returned %d\n", retcode); + print_error("destroy_yices_lock", "pthread_mutex_destroy", retcode); } assert(retcode == 0); }