From c0d41ebed447598f15c62c582adc8c74f5b39943 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 2 Mar 2026 13:48:49 -0800 Subject: [PATCH 1/9] api: select QF_BV SAT delegate via search params --- src/api/search_parameters.c | 50 ++++++++++ src/api/search_parameters.h | 14 +++ src/api/yices_api.c | 52 +++++++++- src/include/yices.h | 6 +- tests/api/context_delegate.c | 179 +++++++++++++++++++++++++++++++++++ 5 files changed, 298 insertions(+), 3 deletions(-) create mode 100644 tests/api/context_delegate.c diff --git a/src/api/search_parameters.c b/src/api/search_parameters.c index a798e352d..d2209f22d 100644 --- a/src/api/search_parameters.c +++ b/src/api/search_parameters.c @@ -84,6 +84,7 @@ * Default branching = the smt_core default */ #define DEFAULT_BRANCHING BRANCHING_DEFAULT +#define DEFAULT_SAT_DELEGATE SAT_DELEGATE_NONE /* * The default EGRAPH parameters are defined in egraph_types.h @@ -144,6 +145,7 @@ static const param_t default_settings = { DEFAULT_CLAUSE_DECAY, DEFAULT_CACHE_TCLAUSES, DEFAULT_TCLAUSE_SIZE, + DEFAULT_SAT_DELEGATE, DEFAULT_USE_DYN_ACK, DEFAULT_USE_BOOL_DYN_ACK, @@ -187,6 +189,7 @@ typedef enum param_key { PARAM_D_THRESHOLD, PARAM_C_FACTOR, PARAM_D_FACTOR, + PARAM_DELEGATE, // clause deletion heuristic PARAM_R_THRESHOLD, PARAM_R_FRACTION, @@ -237,6 +240,7 @@ static const char *const param_key_names[NUM_PARAM_KEYS] = { "clause-decay", "d-factor", "d-threshold", + "delegate", "dyn-ack", "dyn-ack-threshold", "dyn-bool-ack", @@ -274,6 +278,7 @@ static const int32_t param_code[NUM_PARAM_KEYS] = { PARAM_CLAUSE_DECAY, PARAM_D_FACTOR, PARAM_D_THRESHOLD, + PARAM_DELEGATE, PARAM_DYN_ACK, PARAM_DYN_ACK_THRESHOLD, PARAM_DYN_BOOL_ACK, @@ -322,6 +327,25 @@ static const int32_t branching_code[NUM_BRANCHING_MODES] = { BRANCHING_THEORY, }; +/* + * Names of delegate solvers (in lexicographic order) + */ +static const char * const sat_delegate_modes[NUM_SAT_DELEGATES] = { + "cadical", + "cryptominisat", + "kissat", + "none", + "y2sat", +}; + +static const int32_t sat_delegate_code[NUM_SAT_DELEGATES] = { + SAT_DELEGATE_CADICAL, + SAT_DELEGATE_CRYPTOMINISAT, + SAT_DELEGATE_KISSAT, + SAT_DELEGATE_NONE, + SAT_DELEGATE_Y2SAT, +}; + @@ -380,6 +404,28 @@ static int32_t set_branching_param(const char *value, branch_t *v) { return k; } +/* + * Parse value as a SAT delegate mode. Store the result in *v + * - return 0 if this works + * - return -2 otherwise + */ +static int32_t set_sat_delegate_param(const char *value, sat_delegate_t *v) { + int32_t k; + + k = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES); + assert(k >= 0 || k == -1); + + if (k >= 0) { + assert(SAT_DELEGATE_NONE <= k && k <= SAT_DELEGATE_KISSAT); + *v = (sat_delegate_t) k; + k = 0; + } else { + k = -2; + } + + return k; +} + /* * Parse val as a signed 32bit integer. Check whether @@ -523,6 +569,10 @@ int32_t params_set_field(param_t *parameters, const char *key, const char *value r = set_double_param(value, ¶meters->d_factor, 1.0, DBL_MAX); break; + case PARAM_DELEGATE: + r = set_sat_delegate_param(value, ¶meters->delegate); + break; + case PARAM_R_THRESHOLD: r = set_int32_param(value, &z, 1, INT32_MAX); if (r == 0) { diff --git a/src/api/search_parameters.h b/src/api/search_parameters.h index ddcb4b158..2d7bd2646 100644 --- a/src/api/search_parameters.h +++ b/src/api/search_parameters.h @@ -45,6 +45,19 @@ typedef enum { #define NUM_BRANCHING_MODES 6 +/* + * Optional SAT delegate for QF_BV one-shot solving. + */ +typedef enum { + SAT_DELEGATE_NONE, + SAT_DELEGATE_Y2SAT, + SAT_DELEGATE_CADICAL, + SAT_DELEGATE_CRYPTOMINISAT, + SAT_DELEGATE_KISSAT, +} sat_delegate_t; + +#define NUM_SAT_DELEGATES 5 + struct param_s { /* @@ -103,6 +116,7 @@ struct param_s { float clause_decay; // decay factor for learned-clause activity bool cache_tclauses; uint32_t tclause_size; + sat_delegate_t delegate; /* * EGRAPH PARAMETERS diff --git a/src/api/yices_api.c b/src/api/yices_api.c index adf5114e6..e8ed7424a 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -9050,6 +9050,43 @@ EXPORTED void yices_default_params_for_context(const context_t *ctx, param_t *pa yices_set_default_params(params, ctx->logic, ctx->arch, ctx->mode); } +/* + * Check whether the given delegate is supported and set the error + * report if not. + */ +static bool check_delegate(const char *delegate); + +/* + * Delegate name from search-parameter record. + * - return NULL if the default internal SAT solver should be used + */ +static const char *params_delegate_name(const param_t *params) { + const char *s; + + s = NULL; + switch (params->delegate) { + case SAT_DELEGATE_NONE: + break; + case SAT_DELEGATE_Y2SAT: + s = "y2sat"; + break; + case SAT_DELEGATE_CADICAL: + s = "cadical"; + break; + case SAT_DELEGATE_CRYPTOMINISAT: + s = "cryptominisat"; + break; + case SAT_DELEGATE_KISSAT: + s = "kissat"; + break; + default: + assert(false); + break; + } + + return s; +} + /* @@ -9084,6 +9121,7 @@ EXPORTED void yices_default_params_for_context(const context_t *ctx, param_t *pa */ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) { param_t default_params; + const char *delegate; smt_status_t stat; stat = context_status(ctx); @@ -9107,7 +9145,19 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) yices_default_params_for_context(ctx, &default_params); params = &default_params; } - stat = check_context(ctx, params); + delegate = params_delegate_name(params); + if (delegate == NULL) { + stat = check_context(ctx, params); + } else { + if (!check_delegate(delegate)) { + return YICES_STATUS_ERROR; + } + if (ctx->logic != QF_BV || context_get_mode(ctx) != CTX_MODE_ONECHECK) { + set_error_code(CTX_OPERATION_NOT_SUPPORTED); + return YICES_STATUS_ERROR; + } + stat = check_with_delegate(ctx, delegate, 0); + } if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) { context_cleanup(ctx); } diff --git a/src/include/yices.h b/src/include/yices.h index 107e32dfa..727a74bbf 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -3254,8 +3254,6 @@ __YICES_DLLSPEC__ extern int32_t yices_assert_formulas(context_t *ctx, uint32_t */ __YICES_DLLSPEC__ extern smt_status_t yices_check_context(context_t *ctx, const param_t *params); - - /* * Check satisfiability under assumptions. * @@ -3527,6 +3525,10 @@ __YICES_DLLSPEC__ extern void yices_default_params_for_context(const context_t * * The parameters are explained in doc/YICES-LANGUAGE * (and at http://yices.csl.sri.com/doc/parameters.html) * + * For QF_BV one-shot contexts, parameter name "delegate" can be set to + * "none", "y2sat", "cadical", "cryptominisat", or "kissat" to select + * the SAT backend used by yices_check_context. + * * Return -1 if there's an error, 0 otherwise. * * Error codes: diff --git a/tests/api/context_delegate.c b/tests/api/context_delegate.c new file mode 100644 index 000000000..7dd31fcbe --- /dev/null +++ b/tests/api/context_delegate.c @@ -0,0 +1,179 @@ +#ifdef NDEBUG +#undef NDEBUG +#endif + +#include + +#include + +static context_t *new_qfbv_one_shot_context(void) { + ctx_config_t *config; + context_t *ctx; + + config = yices_new_config(); + assert(config != NULL); + + assert(yices_default_config_for_logic(config, "QF_BV") == 0); + assert(yices_set_config(config, "mode", "one-shot") == 0); + + ctx = yices_new_context(config); + assert(ctx != NULL); + + yices_free_config(config); + return ctx; +} + +static context_t *new_qflia_one_shot_context(void) { + ctx_config_t *config; + context_t *ctx; + + config = yices_new_config(); + assert(config != NULL); + + assert(yices_default_config_for_logic(config, "QF_LIA") == 0); + assert(yices_set_config(config, "mode", "one-shot") == 0); + + ctx = yices_new_context(config); + assert(ctx != NULL); + + yices_free_config(config); + return ctx; +} + +static context_t *new_qfbv_pushpop_context(void) { + ctx_config_t *config; + context_t *ctx; + + config = yices_new_config(); + assert(config != NULL); + + assert(yices_default_config_for_logic(config, "QF_BV") == 0); + assert(yices_set_config(config, "mode", "push-pop") == 0); + + ctx = yices_new_context(config); + assert(ctx != NULL); + + yices_free_config(config); + return ctx; +} + +static param_t *new_delegate_params(const char *delegate) { + param_t *params; + + params = yices_new_param_record(); + assert(params != NULL); + assert(yices_set_param(params, "delegate", delegate) == 0); + + return params; +} + +static void check_sat_case(const char *delegate) { + type_t bv8; + term_t x, f; + context_t *ctx; + param_t *params; + smt_status_t stat; + model_t *mdl; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + f = yices_bveq_atom(yices_bvadd(x, yices_bvconst_uint32(8, 1)), yices_bvconst_uint32(8, 2)); + + ctx = new_qfbv_one_shot_context(); + assert(yices_assert_formula(ctx, f) == 0); + + params = new_delegate_params(delegate); + stat = yices_check_context(ctx, params); + assert(stat == YICES_STATUS_SAT); + assert(yices_error_code() == YICES_NO_ERROR); + + mdl = yices_get_model(ctx, 1); + assert(mdl != NULL); + yices_free_model(mdl); + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_unsat_case(const char *delegate) { + type_t bv8; + term_t x, f0, f1; + context_t *ctx; + param_t *params; + smt_status_t stat; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + + f0 = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + f1 = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + + ctx = new_qfbv_one_shot_context(); + assert(yices_assert_formula(ctx, f0) == 0); + assert(yices_assert_formula(ctx, f1) == 0); + + params = new_delegate_params(delegate); + stat = yices_check_context(ctx, params); + assert(stat == YICES_STATUS_UNSAT); + assert(yices_error_code() == YICES_NO_ERROR); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +int main(void) { + const char *delegates[] = { "y2sat", "cadical", "cryptominisat", "kissat" }; + context_t *ctx; + param_t *params; + smt_status_t stat; + uint32_t i; + + yices_init(); + + assert(yices_has_delegate("y2sat")); + + for (i=0; i Date: Mon, 2 Mar 2026 15:17:32 -0800 Subject: [PATCH 2/9] tests(api): expand delegate context coverage --- tests/api/context_delegate.c | 276 ++++++++++++++++++++++++++++++++--- 1 file changed, 254 insertions(+), 22 deletions(-) diff --git a/tests/api/context_delegate.c b/tests/api/context_delegate.c index 7dd31fcbe..ff5aaf32c 100644 --- a/tests/api/context_delegate.c +++ b/tests/api/context_delegate.c @@ -6,6 +6,23 @@ #include +static void expect_status(context_t *ctx, const param_t *params, smt_status_t expected) { + smt_status_t stat; + + stat = yices_check_context(ctx, params); + assert(stat == expected); + assert(yices_error_code() == YICES_NO_ERROR); +} + +static void assert_formula_true_in_context_model(context_t *ctx, term_t f) { + model_t *mdl; + + mdl = yices_get_model(ctx, 1); + assert(mdl != NULL); + assert(yices_formula_true_in_model(mdl, f) == 1); + yices_free_model(mdl); +} + static context_t *new_qfbv_one_shot_context(void) { ctx_config_t *config; context_t *ctx; @@ -72,8 +89,6 @@ static void check_sat_case(const char *delegate) { term_t x, f; context_t *ctx; param_t *params; - smt_status_t stat; - model_t *mdl; bv8 = yices_bv_type(8); x = yices_new_uninterpreted_term(bv8); @@ -83,13 +98,8 @@ static void check_sat_case(const char *delegate) { assert(yices_assert_formula(ctx, f) == 0); params = new_delegate_params(delegate); - stat = yices_check_context(ctx, params); - assert(stat == YICES_STATUS_SAT); - assert(yices_error_code() == YICES_NO_ERROR); - - mdl = yices_get_model(ctx, 1); - assert(mdl != NULL); - yices_free_model(mdl); + expect_status(ctx, params, YICES_STATUS_SAT); + assert_formula_true_in_context_model(ctx, f); yices_free_param_record(params); yices_free_context(ctx); } @@ -99,7 +109,6 @@ static void check_unsat_case(const char *delegate) { term_t x, f0, f1; context_t *ctx; param_t *params; - smt_status_t stat; bv8 = yices_bv_type(8); x = yices_new_uninterpreted_term(bv8); @@ -112,9 +121,233 @@ static void check_unsat_case(const char *delegate) { assert(yices_assert_formula(ctx, f1) == 0); params = new_delegate_params(delegate); - stat = yices_check_context(ctx, params); - assert(stat == YICES_STATUS_UNSAT); - assert(yices_error_code() == YICES_NO_ERROR); + expect_status(ctx, params, YICES_STATUS_UNSAT); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_pushpop_incremental_case(const char *delegate) { + type_t bv8; + term_t x, f0, f1; + context_t *ctx; + param_t *params; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + + f0 = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + f1 = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + + ctx = new_qfbv_pushpop_context(); + params = new_delegate_params(delegate); + + assert(yices_assert_formula(ctx, f0) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, f1) == 0); + expect_status(ctx, params, YICES_STATUS_UNSAT); + + assert(yices_pop(ctx) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + + assert(yices_assert_formula(ctx, f1) == 0); + expect_status(ctx, params, YICES_STATUS_UNSAT); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_sat_model_value_case(const char *delegate) { + type_t bv8; + term_t x, f0, f1; + context_t *ctx; + param_t *params; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + f0 = yices_bveq_atom(yices_bvadd(x, yices_bvconst_uint32(8, 1)), yices_bvconst_uint32(8, 2)); + f1 = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + + ctx = new_qfbv_one_shot_context(); + assert(yices_assert_formula(ctx, f0) == 0); + + params = new_delegate_params(delegate); + expect_status(ctx, params, YICES_STATUS_SAT); + assert_formula_true_in_context_model(ctx, f0); + assert_formula_true_in_context_model(ctx, f1); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_bitwise_sat_case(const char *delegate) { + type_t bv8; + term_t x, y, f0, f1; + context_t *ctx; + param_t *params; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + y = yices_new_uninterpreted_term(bv8); + + f0 = yices_bveq_atom(yices_bvand2(x, y), yices_bvconst_uint32(8, 0x0f)); + f1 = yices_bveq_atom(yices_bvor2(x, y), yices_bvconst_uint32(8, 0xff)); + + ctx = new_qfbv_one_shot_context(); + assert(yices_assert_formula(ctx, f0) == 0); + assert(yices_assert_formula(ctx, f1) == 0); + + params = new_delegate_params(delegate); + expect_status(ctx, params, YICES_STATUS_SAT); + assert_formula_true_in_context_model(ctx, f0); + assert_formula_true_in_context_model(ctx, f1); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_bitwise_unsat_not_case(const char *delegate) { + type_t bv8; + term_t x, f; + context_t *ctx; + param_t *params; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + f = yices_bveq_atom(x, yices_bvnot(x)); + + ctx = new_qfbv_one_shot_context(); + assert(yices_assert_formula(ctx, f) == 0); + + params = new_delegate_params(delegate); + expect_status(ctx, params, YICES_STATUS_UNSAT); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_concat_extract_sat_case(const char *delegate) { + type_t bv4; + term_t hi, lo, z, f0, f1, f2, f3, f4; + context_t *ctx; + param_t *params; + + bv4 = yices_bv_type(4); + hi = yices_new_uninterpreted_term(bv4); + lo = yices_new_uninterpreted_term(bv4); + z = yices_bvconcat2(hi, lo); + + f0 = yices_bveq_atom(hi, yices_bvconst_uint32(4, 0x0a)); + f1 = yices_bveq_atom(lo, yices_bvconst_uint32(4, 0x05)); + f2 = yices_bveq_atom(yices_bvextract(z, 4, 7), hi); + f3 = yices_bveq_atom(yices_bvextract(z, 0, 3), lo); + f4 = yices_bveq_atom(z, yices_bvconst_uint32(8, 0xa5)); + + ctx = new_qfbv_one_shot_context(); + assert(yices_assert_formula(ctx, f0) == 0); + assert(yices_assert_formula(ctx, f1) == 0); + assert(yices_assert_formula(ctx, f2) == 0); + assert(yices_assert_formula(ctx, f3) == 0); + assert(yices_assert_formula(ctx, f4) == 0); + + params = new_delegate_params(delegate); + expect_status(ctx, params, YICES_STATUS_SAT); + assert_formula_true_in_context_model(ctx, f4); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_add_self_unsat_case(const char *delegate) { + type_t bv8; + term_t x, f; + context_t *ctx; + param_t *params; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + f = yices_bveq_atom(yices_bvadd(x, yices_bvconst_uint32(8, 1)), x); + + ctx = new_qfbv_one_shot_context(); + assert(yices_assert_formula(ctx, f) == 0); + + params = new_delegate_params(delegate); + expect_status(ctx, params, YICES_STATUS_UNSAT); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_nested_pushpop_case(const char *delegate) { + type_t bv8; + term_t x, y, xeq0, xeq1, yeq1; + context_t *ctx; + param_t *params; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + y = yices_new_uninterpreted_term(bv8); + xeq0 = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + xeq1 = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + yeq1 = yices_bveq_atom(y, yices_bvconst_uint32(8, 1)); + + ctx = new_qfbv_pushpop_context(); + params = new_delegate_params(delegate); + + assert(yices_assert_formula(ctx, xeq0) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, yeq1) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, xeq1) == 0); + expect_status(ctx, params, YICES_STATUS_UNSAT); + + assert(yices_pop(ctx) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + + assert(yices_pop(ctx) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void check_branching_pushpop_case(const char *delegate) { + type_t bv8; + term_t x, xeq0, xeq1, xneq0; + context_t *ctx; + param_t *params; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + xeq0 = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + xeq1 = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + xneq0 = yices_not(xeq0); + + ctx = new_qfbv_pushpop_context(); + params = new_delegate_params(delegate); + + assert(yices_assert_formula(ctx, xneq0) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, xeq0) == 0); + expect_status(ctx, params, YICES_STATUS_UNSAT); + assert(yices_pop(ctx) == 0); + + expect_status(ctx, params, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, xeq1) == 0); + expect_status(ctx, params, YICES_STATUS_SAT); + assert(yices_pop(ctx) == 0); + + expect_status(ctx, params, YICES_STATUS_SAT); yices_free_param_record(params); yices_free_context(ctx); @@ -135,6 +368,14 @@ int main(void) { if (yices_has_delegate(delegates[i])) { check_sat_case(delegates[i]); check_unsat_case(delegates[i]); + check_pushpop_incremental_case(delegates[i]); + check_sat_model_value_case(delegates[i]); + check_bitwise_sat_case(delegates[i]); + check_bitwise_unsat_not_case(delegates[i]); + check_concat_extract_sat_case(delegates[i]); + check_add_self_unsat_case(delegates[i]); + check_nested_pushpop_case(delegates[i]); + check_branching_pushpop_case(delegates[i]); } } @@ -156,15 +397,6 @@ int main(void) { yices_free_context(ctx); } - // Wrong mode: push-pop - ctx = new_qfbv_pushpop_context(); - params = new_delegate_params("y2sat"); - stat = yices_check_context(ctx, params); - assert(stat == YICES_STATUS_ERROR); - assert(yices_error_code() == CTX_OPERATION_NOT_SUPPORTED); - yices_free_param_record(params); - yices_free_context(ctx); - // Wrong logic: not QF_BV ctx = new_qflia_one_shot_context(); params = new_delegate_params("y2sat"); From 0dcae76b7990fbda077424b55b828baccb411af4 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 2 Mar 2026 15:25:40 -0800 Subject: [PATCH 3/9] delegate(level2): enable incremental QF_BV delegates and delegate-only regressions --- Makefile.build | 18 ++- src/api/search_parameters.h | 2 +- src/api/yices_api.c | 2 +- src/frontend/smt2/smt2_commands.c | 9 ++ src/frontend/yices_smt2.c | 7 - src/include/yices.h | 6 +- src/solvers/cdcl/delegate.c | 13 +- .../bv/delegate_incremental_y2sat.smt2 | 11 ++ .../bv/delegate_incremental_y2sat.smt2.gold | 4 + .../delegate_incremental_y2sat.smt2.options | 1 + tests/regress/check.sh | 148 ++++++++++++++++-- 11 files changed, 183 insertions(+), 38 deletions(-) create mode 100644 tests/regress/bv/delegate_incremental_y2sat.smt2 create mode 100644 tests/regress/bv/delegate_incremental_y2sat.smt2.gold create mode 100644 tests/regress/bv/delegate_incremental_y2sat.smt2.options diff --git a/Makefile.build b/Makefile.build index 987fff948..1398c4eeb 100644 --- a/Makefile.build +++ b/Makefile.build @@ -305,6 +305,8 @@ static-check-api: static_build_subdirs version check: regress mcsat-check: mcsat-regress static-check: static-regress +delegate-check: delegate-regress +static-delegate-check: static-delegate-regress regress: build_subdirs version @ echo "=== Building binaries ===" @@ -312,6 +314,12 @@ regress: build_subdirs version @ echo "=== Running regressions ===" +@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin +delegate-regress: build_subdirs version + @ echo "=== Building binaries ===" + @ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin + @ echo "=== Running delegate-only regressions ===" + +@ REGRESS_DELEGATE_MODE=only $(regressdir)/check.sh $(regressdir) $(build_dir)/bin + mcsat-regress: build_subdirs version @ echo "=== Building binaries ===" @@ -326,6 +334,12 @@ static-regress: static_build_subdirs version @ echo "=== Running regressions ===" +@ $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin +static-delegate-regress: static_build_subdirs version + @ echo "=== Building binaries ===" + @ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin + @ echo "=== Running delegate-only regressions ===" + +@ REGRESS_DELEGATE_MODE=only $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin + static-mcsat-regress: static_build_subdirs version @ echo "=== Building binaries ===" @@ -335,7 +349,9 @@ static-mcsat-regress: static_build_subdirs version .PHONY: all obj static-obj lib static-lib bin static-bin test static-test \ - regress static-regress check static-check check-api static-check-api + regress delegate-regress static-regress static-delegate-regress \ + check delegate-check static-check static-delegate-check \ + check-api static-check-api # diff --git a/src/api/search_parameters.h b/src/api/search_parameters.h index 2d7bd2646..24e4340fa 100644 --- a/src/api/search_parameters.h +++ b/src/api/search_parameters.h @@ -46,7 +46,7 @@ typedef enum { #define NUM_BRANCHING_MODES 6 /* - * Optional SAT delegate for QF_BV one-shot solving. + * Optional SAT delegate for QF_BV solving. */ typedef enum { SAT_DELEGATE_NONE, diff --git a/src/api/yices_api.c b/src/api/yices_api.c index e8ed7424a..066db6e2c 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -9152,7 +9152,7 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) if (!check_delegate(delegate)) { return YICES_STATUS_ERROR; } - if (ctx->logic != QF_BV || context_get_mode(ctx) != CTX_MODE_ONECHECK) { + if (ctx->logic != QF_BV) { set_error_code(CTX_OPERATION_NOT_SUPPORTED); return YICES_STATUS_ERROR; } diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index d8472510a..bc26f2405 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -2635,8 +2635,17 @@ static void init_smt2_context(smt2_globals_t *g) { * this must be called after the assertions */ static void init_search_parameters(smt2_globals_t *g) { + int32_t code; + assert(g->ctx != NULL); yices_default_params_for_context(g->ctx, &g->parameters); + if (g->delegate != NULL) { + code = params_set_field(&g->parameters, "delegate", g->delegate); + assert(code == 0); + if (code < 0) { + g->parameters.delegate = SAT_DELEGATE_NONE; + } + } } diff --git a/src/frontend/yices_smt2.c b/src/frontend/yices_smt2.c index ff964361b..ee2a61f71 100644 --- a/src/frontend/yices_smt2.c +++ b/src/frontend/yices_smt2.c @@ -724,12 +724,6 @@ static void parse_command_line(int argc, char *argv[]) { } done: - if (incremental && delegate != NULL) { - fprintf(stderr, "%s: delegate %s does not support incremental mode\n", parser.command_name, delegate); - code = YICES_EXIT_USAGE; - goto exit; - } - if (incremental && dimacsfile != NULL) { fprintf(stderr, "%s: export to DIMACS is not supported in incremental mode\n", parser.command_name); code = YICES_EXIT_USAGE; @@ -1220,4 +1214,3 @@ int main(int argc, char *argv[]) { return YICES_EXIT_SUCCESS; } - diff --git a/src/include/yices.h b/src/include/yices.h index 727a74bbf..52b580c58 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -3525,9 +3525,9 @@ __YICES_DLLSPEC__ extern void yices_default_params_for_context(const context_t * * The parameters are explained in doc/YICES-LANGUAGE * (and at http://yices.csl.sri.com/doc/parameters.html) * - * For QF_BV one-shot contexts, parameter name "delegate" can be set to - * "none", "y2sat", "cadical", "cryptominisat", or "kissat" to select - * the SAT backend used by yices_check_context. + * For QF_BV contexts, parameter name "delegate" can be set to "none", + * "y2sat", "cadical", "cryptominisat", or "kissat" to select the SAT + * backend used by yices_check_context. * * Return -1 if there's an error, 0 otherwise. * diff --git a/src/solvers/cdcl/delegate.c b/src/solvers/cdcl/delegate.c index 73d0aca66..2b6a5e632 100644 --- a/src/solvers/cdcl/delegate.c +++ b/src/solvers/cdcl/delegate.c @@ -271,17 +271,10 @@ static void cadical_delete(void *solver) { static void cadical_as_delegate(delegate_t *d, uint32_t nvars) { d->solver = ccadical_init(); - ccadical_set_option(d->solver, "quiet", 1); // no output from cadical by default init_ivector(&d->buffer, 0); // not used - // fine tuning - ccadical_set_option(d->solver, "walk", 0); - ccadical_set_option(d->solver, "lucky", 0); - ccadical_set_option(d->solver, "chrono", 0); - ccadical_set_option(d->solver, "elimands", 0); - // ccadical_set_option(d->solver, "elimequivs", 0); - ccadical_set_option(d->solver, "elimites", 0); - ccadical_set_option(d->solver, "elimxors", 0); - // end of fine tuning + if (nvars > 0) { + ccadical_declare_more_variables(d->solver, (int32_t) nvars); + } d->add_empty_clause = cadical_add_empty_clause; d->add_unit_clause = cadical_add_unit_clause; d->add_binary_clause = cadical_add_binary_clause; diff --git a/tests/regress/bv/delegate_incremental_y2sat.smt2 b/tests/regress/bv/delegate_incremental_y2sat.smt2 new file mode 100644 index 000000000..b53a241c3 --- /dev/null +++ b/tests/regress/bv/delegate_incremental_y2sat.smt2 @@ -0,0 +1,11 @@ +(set-logic QF_BV) +(declare-fun x () (_ BitVec 8)) +(assert (= x (_ bv0 8))) +(check-sat) +(push 1) +(assert (= x (_ bv1 8))) +(check-sat) +(pop 1) +(check-sat) +(assert (= x (_ bv1 8))) +(check-sat) diff --git a/tests/regress/bv/delegate_incremental_y2sat.smt2.gold b/tests/regress/bv/delegate_incremental_y2sat.smt2.gold new file mode 100644 index 000000000..a3500f934 --- /dev/null +++ b/tests/regress/bv/delegate_incremental_y2sat.smt2.gold @@ -0,0 +1,4 @@ +sat +unsat +sat +unsat diff --git a/tests/regress/bv/delegate_incremental_y2sat.smt2.options b/tests/regress/bv/delegate_incremental_y2sat.smt2.options new file mode 100644 index 000000000..4f0d920d7 --- /dev/null +++ b/tests/regress/bv/delegate_incremental_y2sat.smt2.options @@ -0,0 +1 @@ +--incremental --delegate=y2sat diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 0849f6ea7..2cb14538a 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -43,6 +43,91 @@ cleanup() { [[ -n "$logdir" ]] && rm -rf "$logdir" } +run_test_batch() { + local test_set="$1" + local local_smt2_options="$2" + local run_label="$3" + local run_logdir="$logdir/$run_label" + + if [ -z "$test_set" ] ; then + return + fi + + mkdir -p "$run_logdir" || { echo "Can't create temp folder $run_logdir" ; exit 1 ; } + + case "$parallel_tool" in + more) + parallel -i $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$local_smt2_options" {} "$bin_dir" "$run_logdir" -- $test_set + ;; + gnu) + parallel -q $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$local_smt2_options" {} "$bin_dir" "$run_logdir" ::: $test_set + ;; + *) + for file in $test_set; do + bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$local_smt2_options" "$file" "$bin_dir" "$run_logdir" + done + ;; + esac +} + +is_qf_bv_delegate_candidate() { + local file="$1" + local opt_file="$file.options" + local gold_file="$file.gold" + + case "$file" in + *.smt2) + ;; + *) + return 1 + ;; + esac + + case "$file" in + */mcsat/*) + return 1 + ;; + esac + + if ! grep -Eq '^[[:space:]]*\(set-logic[[:space:]]+QF_BV\)' "$file" ; then + return 1 + fi + + # Delegate regressions should compare SAT status only. + # Exclude tests that query models/values/cores/assumptions. + if grep -Eq '\(get-model\)|\(get-value\)|\(get-unsat-core\)|\(get-unsat-assumptions\)|\(get-assignment\)' "$file"; then + return 1 + fi + + if grep -Eq '\(echo[[:space:]]' "$file"; then + return 1 + fi + + # Restrict to tests whose expected output consists only of sat/unsat/unknown lines. + if [ ! -e "$gold_file" ]; then + return 1 + fi + if grep -Eqv '^[[:space:]]*$|^[[:space:]]*(sat|unsat|unknown)[[:space:]]*$' "$gold_file"; then + return 1 + fi + + if [ -e "$opt_file" ]; then + if grep -Eq '(^|[[:space:]])--delegate(=|[[:space:]])' "$opt_file"; then + return 1 + fi + if grep -Eq '(^|[[:space:]])--mcsat([[:space:]]|$)' "$opt_file"; then + return 1 + fi + fi + + return 0 +} + +supports_delegate() { + local delegate="$1" + ./"$bin_dir"/yices_smt2 --delegate="$delegate" < /dev/null > /dev/null 2>&1 +} + smt2_options= j_option= @@ -70,6 +155,19 @@ bin_dir=$2 shift 2 all_tests="$@" +if [[ -z "$REGRESS_DELEGATE_MODE" ]]; then + REGRESS_DELEGATE_MODE="auto" +fi + +case "$REGRESS_DELEGATE_MODE" in + auto|only|off) + ;; + *) + echo "Invalid REGRESS_DELEGATE_MODE='$REGRESS_DELEGATE_MODE' (expected auto|only|off)" + exit 2 + ;; +esac + # # System-dependent configuration # @@ -166,19 +264,39 @@ fi j_param="-j$job_count" if [[ $job_count == 0 ]]; then j_param=""; fi -case "$parallel_tool" in - more) - parallel -i $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests - ;; - gnu) - parallel -q $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: $all_tests - ;; - *) - for file in $all_tests; do - bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir" - done - ;; -esac +# +# Baseline regression pass +# +if [[ "$REGRESS_DELEGATE_MODE" != "only" ]]; then + run_test_batch "$all_tests" "$smt2_options" "baseline" +fi + +# +# Delegate passes on QF_BV tests: +# run one extra pass for each installed external delegate. +# +delegate_tests= +if [[ "$REGRESS_DELEGATE_MODE" != "off" ]] && ! echo " $smt2_options " | grep -Eq '(^|[[:space:]])--delegate(=|[[:space:]])'; then + for file in $all_tests; do + if is_qf_bv_delegate_candidate "$file"; then + delegate_tests="$delegate_tests $file" + fi + done +fi + +if [ -n "$delegate_tests" ]; then + delegates= + for d in cadical cryptominisat kissat; do + if supports_delegate "$d"; then + delegates="$delegates $d" + fi + done + + for d in $delegates; do + echo "=== Running QF_BV delegate regressions ($d) ===" + run_test_batch "$delegate_tests" "$smt2_options --delegate=$d" "delegate_$d" + done +fi # give back tokens while [[ $job_count -gt 1 ]]; do @@ -196,10 +314,10 @@ echo "Fail: $fail" if [ "$fail" -eq 0 ] ; then code=0 else - for f in "$logdir"/*.error ; do + while IFS= read -r f; do cat "$f" echo - done + done < <(find "$logdir" -type f -name "*.error" | sort) code=1 fi From 0dfdda09fef8fcb3638ccfa69b310008f00feac1 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 2 Mar 2026 17:02:43 -0800 Subject: [PATCH 4/9] delegate(level2): persist incremental SAT delegates in context Add config/context-level SAT delegate selection for QF_BV, including\npersistent delegate runtime state across check-sat calls. Implement\nincremental delegate integration for CaDiCaL and CryptoMiniSat with\ncheck-sat-assuming support and unsat-core mapping from failed assumptions.\n\nKeep non-incremental delegates (y2sat, kissat) valid selections but return\nCTX_OPERATION_NOT_SUPPORTED for check-sat-assuming.\n\nAdd selector-frame mode wiring (ignored for non-incremental delegates),\ncontext mutation tracking/cleanup, and API+regression tests for delegate\ncontexts/assumptions. --- src/api/context_config.c | 43 +++- src/api/context_config.h | 2 + src/api/yices_api.c | 51 ++++- src/context/context.c | 16 ++ src/context/context.h | 16 ++ src/context/context_solver.c | 381 ++++++++++++++++++++++++++++++++++- src/context/context_types.h | 6 + src/solvers/cdcl/delegate.c | 181 +++++++++++++++-- src/solvers/cdcl/delegate.h | 45 +++++ tests/api/context_delegate.c | 79 ++++++++ 10 files changed, 793 insertions(+), 27 deletions(-) diff --git a/src/api/context_config.c b/src/api/context_config.c index dcf88892b..a81c59399 100644 --- a/src/api/context_config.c +++ b/src/api/context_config.c @@ -90,9 +90,11 @@ typedef enum ctx_config_key { CTX_CONFIG_KEY_BV_SOLVER, CTX_CONFIG_KEY_ARITH_SOLVER, CTX_CONFIG_KEY_MODEL_INTERPOLATION, + CTX_CONFIG_KEY_SAT_DELEGATE, + CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES, } ctx_config_key_t; -#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_MODEL_INTERPOLATION+1) +#define NUM_CONFIG_KEYS (CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES+1) static const char *const config_key_names[NUM_CONFIG_KEYS] = { @@ -102,6 +104,8 @@ static const char *const config_key_names[NUM_CONFIG_KEYS] = { "bv-solver", "mode", "model-interpolation", + "sat-delegate", + "sat-delegate-selector-frames", "solver-type", "trace", "uf-solver", @@ -114,11 +118,32 @@ static const int32_t config_key[NUM_CONFIG_KEYS] = { CTX_CONFIG_KEY_BV_SOLVER, CTX_CONFIG_KEY_MODE, CTX_CONFIG_KEY_MODEL_INTERPOLATION, + CTX_CONFIG_KEY_SAT_DELEGATE, + CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES, CTX_CONFIG_KEY_SOLVER_TYPE, CTX_CONFIG_KEY_TRACE_TAGS, CTX_CONFIG_KEY_UF_SOLVER, }; +/* + * Names of delegate solvers (in lexicographic order) + */ +static const char * const sat_delegate_modes[NUM_SAT_DELEGATES] = { + "cadical", + "cryptominisat", + "kissat", + "none", + "y2sat", +}; + +static const int32_t sat_delegate_code[NUM_SAT_DELEGATES] = { + SAT_DELEGATE_CADICAL, + SAT_DELEGATE_CRYPTOMINISAT, + SAT_DELEGATE_KISSAT, + SAT_DELEGATE_NONE, + SAT_DELEGATE_Y2SAT, +}; + @@ -261,6 +286,8 @@ static const ctx_config_t default_config = { CTX_CONFIG_DEFAULT, // arith ARITH_LIRA, // fragment false, // model interpolation + SAT_DELEGATE_NONE, // sat delegate + false, // sat delegate selector frames NULL, // trace tags }; @@ -421,6 +448,20 @@ int32_t config_set_field(ctx_config_t *config, const char *key, const char *valu r = -2; } break; + case CTX_CONFIG_KEY_SAT_DELEGATE: + v = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES); + if (v < 0) { + r = -2; + } else { + config->sat_delegate = (sat_delegate_t) v; + } + break; + case CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES: + v = parse_as_boolean(value, &config->sat_delegate_selector_frames); + if (v < 0) { + r = -2; + } + break; default: assert(k == -1); r = -1; diff --git a/src/api/context_config.h b/src/api/context_config.h index bbf718e38..86c58e0b8 100644 --- a/src/api/context_config.h +++ b/src/api/context_config.h @@ -106,6 +106,8 @@ struct ctx_config_s { solver_code_t arith_config; arith_fragment_t arith_fragment; bool model_interpolation; + sat_delegate_t sat_delegate; + bool sat_delegate_selector_frames; char* trace_tags; }; diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 066db6e2c..b240edb9f 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -8498,6 +8498,9 @@ context_t *_o_yices_new_context(const ctx_config_t *config) { // Additional setup for MCSAT options in the config if (config != NULL) { + ctx->sat_delegate = config->sat_delegate; + ctx->sat_delegate_selector_frames = config->sat_delegate_selector_frames; + // If trace tags are passed in, set them if (config->trace_tags != NULL) { // Make new tracer @@ -9057,14 +9060,14 @@ EXPORTED void yices_default_params_for_context(const context_t *ctx, param_t *pa static bool check_delegate(const char *delegate); /* - * Delegate name from search-parameter record. - * - return NULL if the default internal SAT solver should be used + * Delegate name from SAT delegate mode. + * - return NULL if the default internal SAT solver should be used. */ -static const char *params_delegate_name(const param_t *params) { +static const char *delegate_name(sat_delegate_t mode) { const char *s; s = NULL; - switch (params->delegate) { + switch (mode) { case SAT_DELEGATE_NONE: break; case SAT_DELEGATE_Y2SAT: @@ -9087,6 +9090,34 @@ static const char *params_delegate_name(const param_t *params) { return s; } +/* + * Delegate selected for this check. + * - if params specifies a delegate (!= none), that delegate is selected. + * - otherwise the delegate from context config is selected. + * - *one_shot is set to true iff params override the context delegate. + */ +static sat_delegate_t effective_delegate_mode(const context_t *ctx, const param_t *params, bool *one_shot) { + sat_delegate_t req, cfg; + + req = SAT_DELEGATE_NONE; + if (params != NULL) { + req = params->delegate; + } + cfg = ctx->sat_delegate; + + if (req != SAT_DELEGATE_NONE) { + if (one_shot != NULL) { + *one_shot = (req != cfg || cfg == SAT_DELEGATE_NONE); + } + return req; + } + + if (one_shot != NULL) { + *one_shot = false; + } + return cfg; +} + /* @@ -9121,6 +9152,8 @@ static const char *params_delegate_name(const param_t *params) { */ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) { param_t default_params; + sat_delegate_t delegate_mode; + bool one_shot_delegate; const char *delegate; smt_status_t stat; @@ -9145,7 +9178,8 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) yices_default_params_for_context(ctx, &default_params); params = &default_params; } - delegate = params_delegate_name(params); + delegate_mode = effective_delegate_mode(ctx, params, &one_shot_delegate); + delegate = delegate_name(delegate_mode); if (delegate == NULL) { stat = check_context(ctx, params); } else { @@ -9156,7 +9190,12 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) set_error_code(CTX_OPERATION_NOT_SUPPORTED); return YICES_STATUS_ERROR; } - stat = check_with_delegate(ctx, delegate, 0); + if (!one_shot_delegate && incremental_delegate(delegate)) { + stat = check_with_incremental_delegate(ctx, delegate, 0, ctx->sat_delegate_selector_frames, + 0, NULL, NULL); + } else { + stat = check_with_delegate(ctx, delegate, 0); + } } if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) { context_cleanup(ctx); diff --git a/src/context/context.c b/src/context/context.c index 27ee78d96..661868017 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -5627,6 +5627,8 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, ctx->mode = mode; ctx->arch = arch; ctx->logic = logic; + ctx->sat_delegate = SAT_DELEGATE_NONE; + ctx->sat_delegate_selector_frames = false; ctx->theories = arch2theories[arch]; ctx->options = mode2options[mode]; if (qflag) { @@ -5636,6 +5638,7 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, } ctx->base_level = 0; + ctx->mutation_count = 1; /* * The core is always needed: allocate it here. It's not initialized yet. @@ -5699,6 +5702,7 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, ctx->divmod_table = NULL; ctx->explorer = NULL; ctx->unsat_core_cache = NULL; + ctx->delegate_state = NULL; ctx->dl_profile = NULL; ctx->arith_buffer = NULL; @@ -5733,6 +5737,8 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, * Delete ctx */ void delete_context(context_t *ctx) { + context_delegate_state_cleanup(ctx); + if (ctx->core != NULL) { delete_smt_core(ctx->core); safe_free(ctx->core); @@ -5831,7 +5837,9 @@ void context_invalidate_unsat_core_cache(context_t *ctx) { */ void reset_context(context_t *ctx) { ctx->base_level = 0; + ctx->mutation_count ++; context_invalidate_unsat_core_cache(ctx); + context_delegate_state_cleanup(ctx); reset_smt_core(ctx->core); // this propagates reset to all solvers @@ -5911,6 +5919,7 @@ void context_push(context_t *ctx) { context_divmod_table_push(ctx); ctx->base_level ++; + ctx->mutation_count ++; } void context_pop(context_t *ctx) { @@ -5926,6 +5935,7 @@ void context_pop(context_t *ctx) { context_divmod_table_pop(ctx); ctx->base_level --; + ctx->mutation_count ++; } @@ -6249,6 +6259,10 @@ int32_t _o_assert_formulas(context_t *ctx, uint32_t n, const term_t *f) { } } + if (code == CTX_NO_ERROR || code == TRIVIALLY_UNSAT) { + ctx->mutation_count ++; + } + return code; } @@ -6656,6 +6670,8 @@ int32_t assert_blocking_clause(context_t *ctx) { ctx->core->status = YICES_STATUS_UNSAT; } + ctx->mutation_count ++; + assert(n == 0 || smt_status(ctx->core) == YICES_STATUS_IDLE); return code; diff --git a/src/context/context.h b/src/context/context.h index dba7485d7..1a88e0cb1 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -64,6 +64,11 @@ extern void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic, */ extern void delete_context(context_t *ctx); +/* + * Release delegate runtime state (if any). + */ +extern void context_delegate_state_cleanup(context_t *ctx); + /* * Reset: remove all assertions @@ -396,6 +401,17 @@ extern smt_status_t precheck_context(context_t *ctx); */ extern smt_status_t check_with_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity); +/* + * Incremental delegate solve for QF_BV contexts. + * - sat_solver must be an incremental delegate (cadical/cryptominisat). + * - selector_frames controls pop handling strategy (ignored by non-incremental delegates). + * - assumptions can be NULL if n == 0. + * - if failed != NULL and result is UNSAT under assumptions, failed literals are appended to *failed. + */ +extern smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity, + bool selector_frames, uint32_t n, const literal_t *assumptions, + ivector_t *failed); + /* * Bit-blast then export to DIMACS diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 11d957289..2691cb74b 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -617,6 +617,267 @@ smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *param return stat; } +typedef struct delegate_state_s { + delegate_t delegate; + sat_delegate_t mode; + bool live; + bool selector_frames; + uint64_t synced_mutation; + uint32_t delegate_nvars; + bvar_t next_selector_var; + literal_t active_selector; + ivector_t assumptions; + ivector_t failed; +} delegate_state_t; + +static const char *delegate_name(sat_delegate_t mode) { + switch (mode) { + case SAT_DELEGATE_Y2SAT: + return "y2sat"; + case SAT_DELEGATE_CADICAL: + return "cadical"; + case SAT_DELEGATE_CRYPTOMINISAT: + return "cryptominisat"; + case SAT_DELEGATE_KISSAT: + return "kissat"; + case SAT_DELEGATE_NONE: + default: + return NULL; + } +} + +static sat_delegate_t effective_delegate_mode(const context_t *ctx, const param_t *params, bool *one_shot) { + sat_delegate_t req, cfg; + + req = SAT_DELEGATE_NONE; + if (params != NULL) { + req = params->delegate; + } + cfg = ctx->sat_delegate; + + if (req != SAT_DELEGATE_NONE) { + if (one_shot != NULL) { + *one_shot = (req != cfg || cfg == SAT_DELEGATE_NONE); + } + return req; + } + + if (one_shot != NULL) { + *one_shot = false; + } + return cfg; +} + +void context_delegate_state_cleanup(context_t *ctx) { + delegate_state_t *st; + + st = (delegate_state_t *) ctx->delegate_state; + if (st == NULL) { + return; + } + + if (st->live) { + delete_delegate(&st->delegate); + st->live = false; + } + delete_ivector(&st->assumptions); + delete_ivector(&st->failed); + safe_free(st); + ctx->delegate_state = NULL; +} + +static delegate_state_t *context_get_delegate_state(context_t *ctx) { + delegate_state_t *st; + + st = (delegate_state_t *) ctx->delegate_state; + if (st == NULL) { + st = (delegate_state_t *) safe_malloc(sizeof(delegate_state_t)); + st->mode = SAT_DELEGATE_NONE; + st->live = false; + st->selector_frames = false; + st->synced_mutation = 0; + st->delegate_nvars = 0; + st->next_selector_var = 0; + st->active_selector = true_literal; + init_ivector(&st->assumptions, 0); + init_ivector(&st->failed, 0); + ctx->delegate_state = st; + } + return st; +} + +static void context_import_delegate_model(smt_core_t *core, delegate_t *d) { + bvar_t x; + + for (x=0; xhas_assumptions = false; + core->num_assumptions = 0; + core->assumption_index = 0; + core->assumptions = NULL; + core->bad_assumption = null_literal; + return; + } + + core->has_assumptions = true; + core->num_assumptions = n; + core->assumption_index = n; + core->assumptions = assumptions; + core->bad_assumption = null_literal; + + if (stat == YICES_STATUS_UNSAT && failed != NULL && failed->size > 0) { + core->bad_assumption = failed->data[0]; + } +} + +static bool context_prepare_incremental_delegate(context_t *ctx, delegate_state_t *st, const char *sat_solver, + uint32_t verbosity, bool selector_frames) { + sat_delegate_t mode; + smt_core_t *core; + uint32_t nvars; + literal_t guard; + uint32_t nnew; + + core = ctx->core; + nvars = num_vars(core); + mode = effective_delegate_mode(ctx, NULL, NULL); + (void) mode; + + if (st->live && + (st->mode != ctx->sat_delegate || + st->selector_frames != selector_frames)) { + delete_delegate(&st->delegate); + st->live = false; + } + + if (!st->live) { + if (!init_delegate(&st->delegate, sat_solver, nvars)) { + return false; + } + delegate_set_verbosity(&st->delegate, verbosity); + st->mode = ctx->sat_delegate; + st->selector_frames = selector_frames; + st->synced_mutation = 0; + st->delegate_nvars = nvars; + st->next_selector_var = nvars; + st->active_selector = true_literal; + st->live = true; + } + + if (st->selector_frames && st->delegate_nvars < nvars) { + nnew = nvars - st->delegate_nvars; + delegate_add_vars(&st->delegate, nnew); + st->delegate_nvars = nvars; + } + + if (st->synced_mutation != ctx->mutation_count) { + if (st->selector_frames) { + if (st->next_selector_var >= st->delegate_nvars) { + nnew = st->next_selector_var - st->delegate_nvars + 1; + delegate_add_vars(&st->delegate, nnew); + st->delegate_nvars += nnew; + } + guard = neg_lit(st->next_selector_var); + add_problem_clauses_to_delegate(&st->delegate, core, guard); + st->active_selector = pos_lit(st->next_selector_var); + st->next_selector_var ++; + } else { + delete_delegate(&st->delegate); + st->live = false; + if (!init_delegate(&st->delegate, sat_solver, nvars)) { + return false; + } + delegate_set_verbosity(&st->delegate, verbosity); + add_problem_clauses_to_delegate(&st->delegate, core, true_literal); + st->mode = ctx->sat_delegate; + st->delegate_nvars = nvars; + st->next_selector_var = nvars; + st->active_selector = true_literal; + st->live = true; + } + st->synced_mutation = ctx->mutation_count; + } + + return true; +} + +smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity, + bool selector_frames, uint32_t n, const literal_t *assumptions, + ivector_t *failed) { + smt_status_t stat; + smt_core_t *core; + delegate_state_t *st; + uint32_t i; + + core = ctx->core; + stat = smt_status(core); + if (stat != YICES_STATUS_IDLE) { + return stat; + } + + start_search(core, 0, NULL); + smt_process(core); + stat = smt_status(core); + + assert(stat == YICES_STATUS_UNSAT || stat == YICES_STATUS_SEARCHING || + stat == YICES_STATUS_INTERRUPTED); + + if (stat != YICES_STATUS_SEARCHING) { + return stat; + } + + if (n == 0 && smt_easy_sat(core)) { + stat = YICES_STATUS_SAT; + set_smt_status(core, stat); + return stat; + } + + st = context_get_delegate_state(ctx); + if (!context_prepare_incremental_delegate(ctx, st, sat_solver, verbosity, selector_frames)) { + return YICES_STATUS_UNKNOWN; + } + + ivector_reset(&st->assumptions); + if (st->selector_frames && st->active_selector != true_literal) { + ivector_push(&st->assumptions, st->active_selector); + } + for (i=0; iassumptions, assumptions[i]); + } + + if (st->assumptions.size == 0) { + stat = st->delegate.check(st->delegate.solver); + } else if (delegate_supports_assumptions(&st->delegate)) { + stat = delegate_check_with_assumptions(&st->delegate, st->assumptions.size, + (literal_t *) st->assumptions.data, &st->failed); + if (stat == YICES_STATUS_UNSAT && failed != NULL) { + ivector_reset(failed); + for (i=0; ifailed.size; i++) { + literal_t l = st->failed.data[i]; + if (l != st->active_selector) { + ivector_push(failed, l); + } + } + } + } else { + stat = YICES_STATUS_UNKNOWN; + } + + set_smt_status(core, stat); + set_delegate_assumption_state(core, n, assumptions, stat, &st->failed); + if (stat == YICES_STATUS_SAT) { + context_import_delegate_model(core, &st->delegate); + } + + return stat; +} + /* * Explore term t and collect all Boolean atoms into atoms. */ @@ -715,6 +976,31 @@ static void cache_unsat_core(context_t *ctx, const ivector_t *core) { ivector_copy(ctx->unsat_core_cache, core->data, core->size); } +static void cache_failed_assumptions_core(context_t *ctx, uint32_t n, const term_t *a, + const ivector_t *assumption_literals, + const ivector_t *failed_literals) { + ivector_t core_terms; + int_hset_t failed; + uint32_t i; + + init_ivector(&core_terms, 0); + init_int_hset(&failed, 0); + for (i=0; isize; i++) { + int_hset_add(&failed, failed_literals->data[i]); + } + for (i=0; idata[i])) { + ivector_push(&core_terms, a[i]); + } + } + cache_unsat_core(ctx, &core_terms); + delete_int_hset(&failed); + delete_ivector(&core_terms); +} + +static smt_status_t check_with_delegate_assumptions(context_t *ctx, const char *sat_solver, uint32_t verbosity, + uint32_t n, const literal_t *assumptions, ivector_t *failed); + /* * Check under assumptions given as terms. * - if MCSAT is enabled, this uses temporary labels + model interpolation. @@ -735,7 +1021,12 @@ smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t * context_invalidate_unsat_core_cache(ctx); if (ctx->mcsat == NULL) { + sat_delegate_t mode; + bool one_shot; + const char *delegate; + bool unknown; literal_t l; + ivector_t failed; init_ivector(&assumptions, n); for (i=0; ilogic != QF_BV) { + if (error != NULL) { + *error = CTX_OPERATION_NOT_SUPPORTED; + } + delete_ivector(&assumptions); + return YICES_STATUS_ERROR; + } + + if (!supported_delegate(delegate, &unknown)) { + if (error != NULL) { + *error = unknown ? CTX_UNKNOWN_DELEGATE : CTX_DELEGATE_NOT_AVAILABLE; + } + delete_ivector(&assumptions); + return YICES_STATUS_ERROR; + } + + if (!incremental_delegate(delegate)) { + if (error != NULL) { + *error = CTX_OPERATION_NOT_SUPPORTED; + } + delete_ivector(&assumptions); + return YICES_STATUS_ERROR; + } + + init_ivector(&failed, 0); + if (one_shot) { + stat = check_with_delegate_assumptions(ctx, delegate, 0, n, assumptions.data, &failed); + } else { + stat = check_with_incremental_delegate(ctx, delegate, 0, + ctx->sat_delegate_selector_frames, + n, assumptions.data, &failed); + } + if (stat == YICES_STATUS_UNSAT) { + cache_failed_assumptions_core(ctx, n, a, &assumptions, &failed); + } + delete_ivector(&failed); delete_ivector(&assumptions); return stat; } @@ -971,6 +1305,51 @@ smt_status_t check_with_delegate(context_t *ctx, const char *sat_solver, uint32_ return stat; } +/* + * One-shot check with delegate and assumptions. + * - assumptions are literals in core encoding. + * - if failed != NULL and result is UNSAT, failed assumptions are appended to *failed. + */ +static smt_status_t check_with_delegate_assumptions(context_t *ctx, const char *sat_solver, uint32_t verbosity, + uint32_t n, const literal_t *assumptions, ivector_t *failed) { + smt_status_t stat; + smt_core_t *core; + delegate_t delegate; + + core = ctx->core; + + stat = smt_status(core); + if (stat != YICES_STATUS_IDLE) { + return stat; + } + + start_search(core, 0, NULL); + smt_process(core); + stat = smt_status(core); + + assert(stat == YICES_STATUS_UNSAT || stat == YICES_STATUS_SEARCHING || + stat == YICES_STATUS_INTERRUPTED); + + if (stat != YICES_STATUS_SEARCHING) { + return stat; + } + + if (!init_delegate(&delegate, sat_solver, num_vars(core))) { + return YICES_STATUS_UNKNOWN; + } + delegate_set_verbosity(&delegate, verbosity); + + stat = solve_with_delegate_assumptions(&delegate, core, n, assumptions, failed); + set_smt_status(core, stat); + set_delegate_assumption_state(core, n, assumptions, stat, failed); + if (stat == YICES_STATUS_SAT) { + context_import_delegate_model(core, &delegate); + } + + delete_delegate(&delegate); + return stat; +} + /* * Bit-blast then export to DIMACS diff --git a/src/context/context_types.h b/src/context/context_types.h index 9a7b39911..8d4de1d99 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -28,6 +28,7 @@ #include #include "api/smt_logic_codes.h" +#include "api/search_parameters.h" #include "context/assumption_stack.h" #include "context/common_conjuncts.h" #include "context/divmod_table.h" @@ -636,6 +637,8 @@ struct context_s { context_mode_t mode; context_arch_t arch; smt_logic_t logic; + sat_delegate_t sat_delegate; + bool sat_delegate_selector_frames; // theories flag uint32_t theories; @@ -645,6 +648,7 @@ struct context_s { // base_level == number of calls to push uint32_t base_level; + uint64_t mutation_count; // core and theory solvers smt_core_t *core; @@ -694,6 +698,8 @@ struct context_s { assumption_stack_t assumptions; // cached unsat core (NULL if cache is invalid) ivector_t *unsat_core_cache; + // delegate runtime state (allocated lazily) + void *delegate_state; // optional components: allocated if needed pseudo_subst_t *subst; diff --git a/src/solvers/cdcl/delegate.c b/src/solvers/cdcl/delegate.c index 2b6a5e632..2a37a5a7c 100644 --- a/src/solvers/cdcl/delegate.c +++ b/src/solvers/cdcl/delegate.c @@ -19,6 +19,7 @@ #include #include #include +#include #ifdef HAVE_CADICAL #include "ccadical.h" @@ -100,6 +101,10 @@ static void ysat_set_verbosity(void *solver, uint32_t level) { nsat_set_verbosity(solver, level); } +static void ysat_add_vars(void *solver, uint32_t n) { + nsat_solver_add_vars(solver, n); +} + static void ysat_delete(void *solver) { delete_nsat_solver(solver); safe_free(solver); @@ -141,9 +146,12 @@ static void ysat_as_delegate(delegate_t *d, uint32_t nvars) { d->add_ternary_clause = ysat_add_ternary_clause; d->add_clause = ysat_add_clause; d->check = ysat_check; + d->check_assuming = NULL; + d->collect_failed_assumptions = NULL; d->get_value = ysat_get_value; d->set_verbosity = ysat_set_verbosity; d->delete = ysat_delete; + d->add_vars = ysat_add_vars; // experimental // d->keep_var = ysat_keep_var; @@ -224,6 +232,25 @@ static smt_status_t cadical_check(void *solver) { } } +static smt_status_t cadical_check_assuming(void *solver, uint32_t n, const literal_t *a) { + uint32_t i; + + for (i=0; i 0) { + ccadical_declare_more_variables(solver, (int32_t) n); + } +} + static void cadical_as_delegate(delegate_t *d, uint32_t nvars) { d->solver = ccadical_init(); init_ivector(&d->buffer, 0); // not used - if (nvars > 0) { - ccadical_declare_more_variables(d->solver, (int32_t) nvars); - } + cadical_add_vars(d->solver, nvars); d->add_empty_clause = cadical_add_empty_clause; d->add_unit_clause = cadical_add_unit_clause; d->add_binary_clause = cadical_add_binary_clause; d->add_ternary_clause = cadical_add_ternary_clause; d->add_clause = cadical_add_clause; d->check = cadical_check; + d->check_assuming = cadical_check_assuming; + d->collect_failed_assumptions = cadical_collect_failed_assumptions; d->get_value = cadical_get_value; d->set_verbosity = cadical_set_verbosity; d->delete = cadical_delete; + d->add_vars = cadical_add_vars; d->keep_var = NULL; d->var_def2 = NULL; d->var_def3 = NULL; @@ -343,6 +377,44 @@ static smt_status_t cryptominisat_check(void *solver) { } } +static smt_status_t cryptominisat_check_assuming(void *solver, uint32_t n, const literal_t *a) { + switch (cmsat_solve_with_assumptions(solver, (uint32_t *) a, n)) { + case CMSAT_SAT: return YICES_STATUS_SAT; + case CMSAT_UNSAT: return YICES_STATUS_UNSAT; + default: return YICES_STATUS_UNKNOWN; + } +} + +static void cryptominisat_collect_failed_assumptions(void *solver, uint32_t n, const literal_t *a, ivector_t *out) { + cmsat_lit_vector_t conflict; + uint32_t i, j; + literal_t lit, neg_lit, c; + + conflict.lit = NULL; + conflict.nlits = 0; + cmsat_get_conflict(solver, &conflict); + + /* + * CryptoMiniSat may return assumptions in negated form. + * Normalize to Yices assumption literals so callers can map back cleanly. + */ + for (i=0; i 0) { + cmsat_new_vars(solver, n); + } +} + static void cryptominisat_as_delegate(delegate_t *d, uint32_t nvars) { d->solver = cmsat_new_solver(); - cmsat_new_vars(d->solver, nvars); + cryptominisat_add_vars(d->solver, nvars); init_ivector(&d->buffer, 0); // not used d->add_empty_clause = cryptominisat_add_empty_clause; d->add_unit_clause = cryptominisat_add_unit_clause; @@ -378,9 +456,12 @@ static void cryptominisat_as_delegate(delegate_t *d, uint32_t nvars) { d->add_ternary_clause = cryptominisat_add_ternary_clause; d->add_clause = cryptominisat_add_clause; d->check = cryptominisat_check; + d->check_assuming = cryptominisat_check_assuming; + d->collect_failed_assumptions = cryptominisat_collect_failed_assumptions; d->get_value = cryptominisat_get_value; d->set_verbosity = cryptominisat_set_verbosity; d->delete = cryptominisat_delete; + d->add_vars = cryptominisat_add_vars; d->keep_var = NULL; d->var_def2 = NULL; d->var_def3 = NULL; @@ -483,9 +564,12 @@ static void kissat_as_delegate(delegate_t *d, uint32_t nvars) { d->add_ternary_clause = kissat_add_ternary_clause; d->add_clause = kissat_add_clause; d->check = kissat_check; + d->check_assuming = NULL; + d->collect_failed_assumptions = NULL; d->get_value = kissat_get_value; d->set_verbosity = kissat_set_verbosity; d->delete = kissat_delete; + d->add_vars = NULL; d->keep_var = NULL; d->var_def2 = NULL; d->var_def3 = NULL; @@ -575,6 +659,10 @@ bool supported_delegate(const char *solver_name, bool *unknown) { return false; } +bool incremental_delegate(const char *solver_name) { + return strcmp("cadical", solver_name) == 0 || strcmp("cryptominisat", solver_name) == 0; +} + /* * Delete the solver and free memory @@ -601,23 +689,29 @@ void delete_delegate(delegate_t *d) { /* * Transfer unit clauses from core to delegate */ -static void copy_unit_clauses(delegate_t *d, smt_core_t *core) { +static void copy_unit_clauses(delegate_t *d, smt_core_t *core, literal_t g) { prop_stack_t *stack; uint32_t i, n; - d->add_unit_clause(d->solver, true_literal); // CHECK THIS + if (g == true_literal) { + d->add_unit_clause(d->solver, true_literal); // CHECK THIS + } n = core->nb_unit_clauses; stack = &core->stack; for (i=0; iadd_unit_clause(d->solver, stack->lit[i]); + if (g == true_literal) { + d->add_unit_clause(d->solver, stack->lit[i]); + } else { + d->add_binary_clause(d->solver, g, stack->lit[i]); + } } } /* * Transfer binary clauses */ -static void copy_binary_clauses(delegate_t *d, smt_core_t *core) { +static void copy_binary_clauses(delegate_t *d, smt_core_t *core, literal_t g) { int32_t n; literal_t l1, l2; literal_t *bin; @@ -630,7 +724,11 @@ static void copy_binary_clauses(delegate_t *d, smt_core_t *core) { l2 = *bin ++; if (l2 < 0) break; if (l1 <= l2) { - d->add_binary_clause(d->solver, l1, l2); + if (g == true_literal) { + d->add_binary_clause(d->solver, l1, l2); + } else { + d->add_ternary_clause(d->solver, g, l1, l2); + } } } } @@ -642,11 +740,14 @@ static void copy_binary_clauses(delegate_t *d, smt_core_t *core) { * - we make an intermediate copy in d->vector in case the * SAT solver modifies the input array */ -static void copy_clause(delegate_t *d, const clause_t *c) { +static void copy_clause(delegate_t *d, const clause_t *c, literal_t g) { uint32_t i; literal_t l; ivector_reset(&d->buffer); + if (g != true_literal) { + ivector_push(&d->buffer, g); + } i = 0; l = c->cl[0]; while (l >= 0) { @@ -660,13 +761,13 @@ static void copy_clause(delegate_t *d, const clause_t *c) { /* * Copy the clauses from a vector */ -static void copy_clause_vector(delegate_t *d, clause_t **vector) { +static void copy_clause_vector(delegate_t *d, clause_t **vector, literal_t g) { uint32_t i, n; if (vector != NULL) { n = get_cv_size(vector); for (i=0; iinconsistent) { - d->add_empty_clause(d->solver); + if (g == true_literal) { + d->add_empty_clause(d->solver); + } else { + d->add_unit_clause(d->solver, g); + } } - copy_unit_clauses(d, core); - copy_binary_clauses(d, core); - copy_clause_vector(d, core->problem_clauses); + copy_unit_clauses(d, core, g); + copy_binary_clauses(d, core, g); + copy_clause_vector(d, core->problem_clauses, g); } @@ -810,7 +915,7 @@ static void export_gate_definitions(delegate_t *d, smt_core_t *core) { * Copy all clauses of core to a delegate d then call the delegate's solver */ smt_status_t solve_with_delegate(delegate_t *d, smt_core_t *core) { - copy_problem_clauses(d, core); + add_problem_clauses_to_delegate(d, core, true_literal); if (d->keep_var != NULL) { mark_atom_variables(d, core); } @@ -827,7 +932,7 @@ smt_status_t solve_with_delegate(delegate_t *d, smt_core_t *core) { smt_status_t preprocess_with_delegate(delegate_t *d, smt_core_t *core) { if (d->preprocess == NULL) return YICES_STATUS_UNKNOWN; // not supported - copy_problem_clauses(d, core); + add_problem_clauses_to_delegate(d, core, true_literal); if (d->keep_var != NULL) { mark_atom_variables(d, core); } @@ -861,3 +966,41 @@ bval_t delegate_get_value(delegate_t *d, bvar_t x) { void delegate_set_verbosity(delegate_t *d, uint32_t level) { d->set_verbosity(d->solver, level); } + +void delegate_add_vars(delegate_t *d, uint32_t n) { + if (d->add_vars != NULL && n > 0) { + d->add_vars(d->solver, n); + } +} + +bool delegate_supports_assumptions(const delegate_t *d) { + return d->check_assuming != NULL; +} + +smt_status_t delegate_check_with_assumptions(delegate_t *d, uint32_t n, const literal_t *a, ivector_t *failed) { + smt_status_t stat; + + if (d->check_assuming == NULL) { + return YICES_STATUS_UNKNOWN; + } + + stat = d->check_assuming(d->solver, n, a); + if (stat == YICES_STATUS_UNSAT && failed != NULL && d->collect_failed_assumptions != NULL) { + ivector_reset(failed); + d->collect_failed_assumptions(d->solver, n, a, failed); + } + + return stat; +} + +smt_status_t solve_with_delegate_assumptions(delegate_t *d, smt_core_t *core, uint32_t n, const literal_t *a, + ivector_t *failed) { + add_problem_clauses_to_delegate(d, core, true_literal); + if (d->keep_var != NULL) { + mark_atom_variables(d, core); + } + if (d->var_def2 != NULL && d->var_def3 != NULL) { + export_gate_definitions(d, core); + } + return delegate_check_with_assumptions(d, n, a, failed); +} diff --git a/src/solvers/cdcl/delegate.h b/src/solvers/cdcl/delegate.h index 4437190c0..19e1d97c7 100644 --- a/src/solvers/cdcl/delegate.h +++ b/src/solvers/cdcl/delegate.h @@ -65,9 +65,12 @@ typedef void (*add_binary_clause_fun_t)(void *solver, literal_t l1, literal_t l2 typedef void (*add_ternary_clause_fun_t)(void *solver, literal_t l1, literal_t l2, literal_t l3); typedef void (*add_clause_fun_t)(void *solver, uint32_t n, literal_t *a); typedef smt_status_t (*check_sat_fun_t)(void *solver); +typedef smt_status_t (*check_sat_assuming_fun_t)(void *solver, uint32_t n, const literal_t *a); typedef bval_t (*get_value_fun_t)(void *solver, bvar_t x); typedef void (*set_verbosity_fun_t)(void *solver, uint32_t level); typedef void (*delete_fun_t)(void *solver); +typedef void (*add_vars_fun_t)(void *solver, uint32_t n); +typedef void (*collect_failed_assumptions_fun_t)(void *solver, uint32_t n, const literal_t *a, ivector_t *out); typedef void (*keep_var_fun_t)(void *solver, bvar_t x); typedef void (*var_def2_fun_t)(void *solver, bvar_t x, uint32_t b, literal_t l1, literal_t l2); @@ -85,9 +88,12 @@ typedef struct delegate_s { add_ternary_clause_fun_t add_ternary_clause; add_clause_fun_t add_clause; check_sat_fun_t check; + check_sat_assuming_fun_t check_assuming; + collect_failed_assumptions_fun_t collect_failed_assumptions; get_value_fun_t get_value; set_verbosity_fun_t set_verbosity; delete_fun_t delete; + add_vars_fun_t add_vars; keep_var_fun_t keep_var; var_def2_fun_t var_def2; var_def3_fun_t var_def3; @@ -118,6 +124,13 @@ extern bool init_delegate(delegate_t *delegate, const char *solver_name, uint32_ */ extern bool supported_delegate(const char *solver_name, bool *unknown); +/* + * Classify solver capabilities. + * - returns true iff solver_name is supported as an incremental delegate + * (currently: cadical, cryptominisat). + */ +extern bool incremental_delegate(const char *solver_name); + /* * Delete the solver and free memory @@ -132,6 +145,21 @@ extern void delete_delegate(delegate_t *delegate); */ extern smt_status_t solve_with_delegate(delegate_t *delegate, smt_core_t *core); +/* + * Same as solve_with_delegate, but solve under assumptions a[0 ... n-1]. + * - if assumptions are not supported by delegate, return YICES_STATUS_UNKNOWN. + * - if failed != NULL and the result is UNSAT, failed assumptions are appended to *failed. + */ +extern smt_status_t solve_with_delegate_assumptions(delegate_t *delegate, smt_core_t *core, + uint32_t n, const literal_t *a, ivector_t *failed); + +/* + * Add all problem clauses in core to delegate, optionally guarded by literal g. + * - if g == true_literal, clauses are copied as-is. + * - otherwise each copied clause C is replaced by (g \/ C). + */ +extern void add_problem_clauses_to_delegate(delegate_t *delegate, smt_core_t *core, literal_t g); + /* * Export the clauses from the core to the delegate * then appply delegate's CNF-level preprocessing @@ -158,6 +186,23 @@ extern bval_t delegate_get_value(delegate_t *delegate, bvar_t x); */ extern void delegate_set_verbosity(delegate_t *delegate, uint32_t level); +/* + * Add n fresh variables to delegate (if supported). + */ +extern void delegate_add_vars(delegate_t *delegate, uint32_t n); + +/* + * Check whether delegate supports assumptions. + */ +extern bool delegate_supports_assumptions(const delegate_t *delegate); + +/* + * Solve with assumptions using an already-populated delegate. + * - if failed != NULL and the result is UNSAT, failed assumptions are appended to *failed. + */ +extern smt_status_t delegate_check_with_assumptions(delegate_t *delegate, uint32_t n, const literal_t *a, + ivector_t *failed); + diff --git a/tests/api/context_delegate.c b/tests/api/context_delegate.c index ff5aaf32c..168c1930f 100644 --- a/tests/api/context_delegate.c +++ b/tests/api/context_delegate.c @@ -3,6 +3,8 @@ #endif #include +#include +#include #include @@ -74,6 +76,27 @@ static context_t *new_qfbv_pushpop_context(void) { return ctx; } +static context_t *new_qfbv_pushpop_context_with_delegate(const char *delegate, const char *selector_frames) { + ctx_config_t *config; + context_t *ctx; + + config = yices_new_config(); + assert(config != NULL); + + assert(yices_default_config_for_logic(config, "QF_BV") == 0); + assert(yices_set_config(config, "mode", "push-pop") == 0); + assert(yices_set_config(config, "sat-delegate", delegate) == 0); + if (selector_frames != NULL) { + assert(yices_set_config(config, "sat-delegate-selector-frames", selector_frames) == 0); + } + + ctx = yices_new_context(config); + assert(ctx != NULL); + + yices_free_config(config); + return ctx; +} + static param_t *new_delegate_params(const char *delegate) { param_t *params; @@ -353,6 +376,60 @@ static void check_branching_pushpop_case(const char *delegate) { yices_free_context(ctx); } +static bool is_incremental_delegate_name(const char *delegate) { + return strcmp(delegate, "cadical") == 0 || strcmp(delegate, "cryptominisat") == 0; +} + +static void check_config_delegate_case(const char *delegate) { + type_t bv8; + term_t x, f; + context_t *ctx; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + f = yices_bveq_atom(yices_bvadd(x, yices_bvconst_uint32(8, 1)), yices_bvconst_uint32(8, 2)); + + ctx = new_qfbv_pushpop_context_with_delegate(delegate, "true"); + assert(yices_assert_formula(ctx, f) == 0); + + expect_status(ctx, NULL, YICES_STATUS_SAT); + assert_formula_true_in_context_model(ctx, f); + + yices_free_context(ctx); +} + +static void check_assumptions_delegate_case(const char *delegate) { + type_t bv8; + term_t x, f, a; + context_t *ctx; + smt_status_t stat; + term_vector_t core; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + f = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + a = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + + ctx = new_qfbv_pushpop_context_with_delegate(delegate, "true"); + assert(yices_assert_formula(ctx, f) == 0); + + stat = yices_check_context_with_assumptions(ctx, NULL, 1, &a); + if (is_incremental_delegate_name(delegate)) { + assert(stat == YICES_STATUS_UNSAT); + yices_init_term_vector(&core); + assert(yices_get_unsat_core(ctx, &core) == 0); + assert(core.size == 1); + assert(core.data[0] == a); + yices_delete_term_vector(&core); + } else { + assert(stat == YICES_STATUS_ERROR); + assert(yices_error_code() == CTX_OPERATION_NOT_SUPPORTED); + yices_clear_error(); + } + + yices_free_context(ctx); +} + int main(void) { const char *delegates[] = { "y2sat", "cadical", "cryptominisat", "kissat" }; context_t *ctx; @@ -376,6 +453,8 @@ int main(void) { check_add_self_unsat_case(delegates[i]); check_nested_pushpop_case(delegates[i]); check_branching_pushpop_case(delegates[i]); + check_config_delegate_case(delegates[i]); + check_assumptions_delegate_case(delegates[i]); } } From 183dc4fe26b0c68ae2adcfce14ed645a6f83bc2f Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Fri, 8 May 2026 09:10:44 -0700 Subject: [PATCH 5/9] Fix delegate selector-frame assumptions --- src/context/context_solver.c | 22 ++++++++-- src/solvers/cdcl/delegate.c | 15 +++++++ tests/api/context_delegate.c | 80 ++++++++++++++++++++++++++++++++++++ 3 files changed, 113 insertions(+), 4 deletions(-) diff --git a/src/context/context_solver.c b/src/context/context_solver.c index b927384fe..361b92c55 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -779,6 +779,9 @@ static bool context_prepare_incremental_delegate(context_t *ctx, delegate_state_ if (st->synced_mutation != ctx->mutation_count) { if (st->selector_frames) { + if (st->next_selector_var < st->delegate_nvars) { + st->next_selector_var = st->delegate_nvars; + } if (st->next_selector_var >= st->delegate_nvars) { nnew = st->next_selector_var - st->delegate_nvars + 1; delegate_add_vars(&st->delegate, nnew); @@ -814,6 +817,7 @@ smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_sol smt_status_t stat; smt_core_t *core; delegate_state_t *st; + ivector_t visible_failed; uint32_t i; core = ctx->core; @@ -844,7 +848,9 @@ smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_sol return YICES_STATUS_UNKNOWN; } + init_ivector(&visible_failed, 0); ivector_reset(&st->assumptions); + ivector_reset(&st->failed); if (st->selector_frames && st->active_selector != true_literal) { ivector_push(&st->assumptions, st->active_selector); } @@ -857,25 +863,29 @@ smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_sol } else if (delegate_supports_assumptions(&st->delegate)) { stat = delegate_check_with_assumptions(&st->delegate, st->assumptions.size, (literal_t *) st->assumptions.data, &st->failed); - if (stat == YICES_STATUS_UNSAT && failed != NULL) { - ivector_reset(failed); + if (stat == YICES_STATUS_UNSAT) { for (i=0; ifailed.size; i++) { literal_t l = st->failed.data[i]; if (l != st->active_selector) { - ivector_push(failed, l); + ivector_push(&visible_failed, l); } } + if (failed != NULL) { + ivector_reset(failed); + ivector_add(failed, visible_failed.data, visible_failed.size); + } } } else { stat = YICES_STATUS_UNKNOWN; } set_smt_status(core, stat); - set_delegate_assumption_state(core, n, assumptions, stat, &st->failed); + set_delegate_assumption_state(core, n, assumptions, stat, &visible_failed); if (stat == YICES_STATUS_SAT) { context_import_delegate_model(core, &st->delegate); } + delete_ivector(&visible_failed); return stat; } @@ -1112,6 +1122,10 @@ smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t * *error = CTX_NO_ERROR; } + /* + * Clear any prior term-assumption core before all paths below. Delegate + * checks cache a new core only on UNSAT. + */ context_invalidate_unsat_core_cache(ctx); if (ctx->mcsat == NULL) { diff --git a/src/solvers/cdcl/delegate.c b/src/solvers/cdcl/delegate.c index 2a37a5a7c..38fdac451 100644 --- a/src/solvers/cdcl/delegate.c +++ b/src/solvers/cdcl/delegate.c @@ -304,7 +304,18 @@ static void cadical_add_vars(void *solver, uint32_t n) { static void cadical_as_delegate(delegate_t *d, uint32_t nvars) { d->solver = ccadical_init(); + ccadical_set_option(d->solver, "quiet", 1); // no output from cadical by default init_ivector(&d->buffer, 0); // not used + + // fine tuning + ccadical_set_option(d->solver, "walk", 0); + ccadical_set_option(d->solver, "lucky", 0); + ccadical_set_option(d->solver, "chrono", 0); + ccadical_set_option(d->solver, "elimands", 0); + ccadical_set_option(d->solver, "elimites", 0); + ccadical_set_option(d->solver, "elimxors", 0); + // end of fine tuning + cadical_add_vars(d->solver, nvars); d->add_empty_clause = cadical_add_empty_clause; d->add_unit_clause = cadical_add_unit_clause; @@ -411,6 +422,10 @@ static void cryptominisat_collect_failed_assumptions(void *solver, uint32_t n, c } if (conflict.lit != NULL) { + /* + * The supported CryptoMiniSat C API allocates this vector with malloc + * and does not provide a vector-specific deallocator. + */ free(conflict.lit); } } diff --git a/tests/api/context_delegate.c b/tests/api/context_delegate.c index 168c1930f..db02ffe48 100644 --- a/tests/api/context_delegate.c +++ b/tests/api/context_delegate.c @@ -430,6 +430,84 @@ static void check_assumptions_delegate_case(const char *delegate) { yices_free_context(ctx); } +static void check_selector_frames_growing_vars_case(const char *delegate) { + type_t bv8; + term_t x, y, z, xeq0, yneq0, zneq0; + context_t *ctx; + + if (!is_incremental_delegate_name(delegate)) { + return; + } + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + y = yices_new_uninterpreted_term(bv8); + z = yices_new_uninterpreted_term(bv8); + xeq0 = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + yneq0 = yices_not(yices_bveq_atom(y, yices_bvconst_uint32(8, 0))); + zneq0 = yices_not(yices_bveq_atom(z, yices_bvconst_uint32(8, 0))); + + ctx = new_qfbv_pushpop_context_with_delegate(delegate, "true"); + + assert(yices_assert_formula(ctx, xeq0) == 0); + expect_status(ctx, NULL, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, yneq0) == 0); + expect_status(ctx, NULL, YICES_STATUS_SAT); + assert_formula_true_in_context_model(ctx, yneq0); + assert(yices_pop(ctx) == 0); + + expect_status(ctx, NULL, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, zneq0) == 0); + expect_status(ctx, NULL, YICES_STATUS_SAT); + assert_formula_true_in_context_model(ctx, zneq0); + assert(yices_pop(ctx) == 0); + + yices_free_context(ctx); +} + +static void check_selector_frames_assumptions_case(const char *delegate) { + type_t bv8; + term_t x, y, xeq0, xeq1, yeq1; + context_t *ctx; + smt_status_t stat; + term_vector_t core; + + if (!is_incremental_delegate_name(delegate)) { + return; + } + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + y = yices_new_uninterpreted_term(bv8); + xeq0 = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + xeq1 = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + yeq1 = yices_bveq_atom(y, yices_bvconst_uint32(8, 1)); + + ctx = new_qfbv_pushpop_context_with_delegate(delegate, "true"); + + assert(yices_assert_formula(ctx, xeq0) == 0); + expect_status(ctx, NULL, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, yeq1) == 0); + expect_status(ctx, NULL, YICES_STATUS_SAT); + + stat = yices_check_context_with_assumptions(ctx, NULL, 1, &xeq1); + assert(stat == YICES_STATUS_UNSAT); + + yices_init_term_vector(&core); + assert(yices_get_unsat_core(ctx, &core) == 0); + assert(core.size == 1); + assert(core.data[0] == xeq1); + yices_delete_term_vector(&core); + + yices_free_context(ctx); +} + int main(void) { const char *delegates[] = { "y2sat", "cadical", "cryptominisat", "kissat" }; context_t *ctx; @@ -455,6 +533,8 @@ int main(void) { check_branching_pushpop_case(delegates[i]); check_config_delegate_case(delegates[i]); check_assumptions_delegate_case(delegates[i]); + check_selector_frames_growing_vars_case(delegates[i]); + check_selector_frames_assumptions_case(delegates[i]); } } From bf025a4532e75505a767483f6090e5b79cda374a Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Fri, 8 May 2026 09:40:11 -0700 Subject: [PATCH 6/9] Document incremental delegate behavior --- doc/manual/manual.tex | 27 +++++++++++++++++++-------- src/include/yices.h | 18 ++++++++++++++++++ 2 files changed, 37 insertions(+), 8 deletions(-) diff --git a/doc/manual/manual.tex b/doc/manual/manual.tex index b280f9d20..b2cafb822 100644 --- a/doc/manual/manual.tex +++ b/doc/manual/manual.tex @@ -1459,12 +1459,14 @@ \section{Third-Party SAT Solvers} In Yices 2.6.2, we have added support for using third-party Boolean satisfiability solvers. Such solvers are optional but can provide significant performance improvements on bit-vector problems. Use of -these SAT solvers is enabled by a command-line option and is currently -restricted to non-incremental QF\_BV problems. If an external solver -is selected, Yices will perform ``bit blasting,'' that is, convert the -problem to an equisatisfiable SAT problem in conjunctive normal form -(CNF) and use the third-party solver to check satisfiability of this -CNF formula. +these SAT solvers is enabled by a command-line option for QF\_BV +problems. If an external solver is selected, Yices will perform ``bit +blasting,'' that is, convert the problem to an equisatisfiable SAT +problem in conjunctive normal form (CNF) and use the selected solver to +check satisfiability of this CNF formula. CaDiCaL and CryptoMiniSat can +be used incrementally. Non-incremental delegates such as \texttt{y2sat} +and Kissat are rebuilt from the current bit-blasted problem on each +incremental check. @@ -3772,7 +3774,13 @@ \subsubsection*{Selecting a Back-end SAT Solver} problems by preprocessing and simplification, without producing a CNF formula. In such cases, the \texttt{delegate} option is irrelevant. -\paragraph{Limitation:} Currently, use of the delegates is restricted to non-incremental problems. +\paragraph{Incremental use:} Delegates can be used with +\texttt{--incremental} on QF\_BV problems. CaDiCaL and CryptoMiniSat +support incremental delegate checks. Non-incremental delegates such as +\texttt{y2sat} and Kissat are rebuilt from the current bit-blasted +problem on each \texttt{check-sat}. The selector-frame configuration +used by the API for incremental delegates has no effect for +non-incremental delegates. \subsubsection*{Exporting to Dimacs} @@ -3864,7 +3872,10 @@ \subsubsection*{All Command-line Options} \item[--delegate=] Select an external SAT solver for bit-vector problems, - The \texttt{} can be either \texttt{cadical}, or \texttt{cryptominisat}, or \texttt{y2sat}. + The \texttt{} can be either \texttt{cadical}, + \texttt{cryptominisat}, \texttt{kissat}, or \texttt{y2sat}. In + incremental mode, \texttt{y2sat} and Kissat are rebuilt from the + current bit-blasted problem on each \texttt{check-sat}. \item[--dimacs=] Bitblast then export the CNF to a file (in DIMACS format). diff --git a/src/include/yices.h b/src/include/yices.h index a1106edf5..82b17a098 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -2959,7 +2959,23 @@ __YICES_DLLSPEC__ extern void yices_free_config(ctx_config_t *config); * ---------------------------------------------------------------------------------------- * "model-interpolation" | "false" | don't enable model interpolation (default) * | "true" | enable model interpolation + * ---------------------------------------------------------------------------------------- + * "sat-delegate" | "none" | use the default SAT solver (default) + * | "y2sat" | use y2sat for QF_BV contexts + * | "cadical" | use CaDiCaL for QF_BV contexts + * | "cryptominisat"| use CryptoMiniSat for QF_BV contexts + * | "kissat" | use Kissat for QF_BV contexts + * ---------------------------------------------------------------------------------------- + * "sat-delegate-selector-frames" | "false" | rebuild delegate clauses after each + * | | context mutation (default) + * | "true" | keep an incremental delegate live + * | | using selector-guarded frames * + * The SAT delegate options have an effect only for QF_BV contexts. + * CaDiCaL and CryptoMiniSat support incremental delegate checks. Non-incremental + * delegates such as y2sat and Kissat are rebuilt from the current bit-blasted + * problem on each incremental check. "sat-delegate-selector-frames" is ignored + * for non-incremental delegates. * * The function returns -1 if there's an error, 0 otherwise. * @@ -3593,6 +3609,8 @@ __YICES_DLLSPEC__ extern void yices_default_params_for_context(const context_t * * For QF_BV contexts, parameter name "delegate" can be set to "none", * "y2sat", "cadical", "cryptominisat", or "kissat" to select the SAT * backend used by yices_check_context. + * In incremental contexts, non-incremental delegates such as y2sat and Kissat + * are rebuilt from the current bit-blasted problem on each check. * * Return -1 if there's an error, 0 otherwise. * From 08b5377f67e21ec5cf1274efcf8c046aec4f21c8 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Fri, 8 May 2026 09:47:37 -0700 Subject: [PATCH 7/9] Clean up delegate dispatch helpers --- src/api/context_config.c | 28 +-------- src/api/search_parameters.c | 67 +++++++++++++++++----- src/api/search_parameters.h | 7 +++ src/api/yices_api.c | 70 ++--------------------- src/context/context.h | 6 +- src/context/context_solver.c | 106 +++++++---------------------------- tests/api/context_delegate.c | 25 +++++++++ 7 files changed, 114 insertions(+), 195 deletions(-) diff --git a/src/api/context_config.c b/src/api/context_config.c index a81c59399..9638f583c 100644 --- a/src/api/context_config.c +++ b/src/api/context_config.c @@ -24,6 +24,7 @@ #include #include "api/context_config.h" +#include "api/search_parameters.h" #include "utils/memalloc.h" #include "utils/string_utils.h" @@ -125,28 +126,6 @@ static const int32_t config_key[NUM_CONFIG_KEYS] = { CTX_CONFIG_KEY_UF_SOLVER, }; -/* - * Names of delegate solvers (in lexicographic order) - */ -static const char * const sat_delegate_modes[NUM_SAT_DELEGATES] = { - "cadical", - "cryptominisat", - "kissat", - "none", - "y2sat", -}; - -static const int32_t sat_delegate_code[NUM_SAT_DELEGATES] = { - SAT_DELEGATE_CADICAL, - SAT_DELEGATE_CRYPTOMINISAT, - SAT_DELEGATE_KISSAT, - SAT_DELEGATE_NONE, - SAT_DELEGATE_Y2SAT, -}; - - - - /* * CONTEXT SETTING FOR A GIVEN LOGIC CODE */ @@ -449,11 +428,8 @@ int32_t config_set_field(ctx_config_t *config, const char *key, const char *valu } break; case CTX_CONFIG_KEY_SAT_DELEGATE: - v = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES); - if (v < 0) { + if (parse_sat_delegate(value, &config->sat_delegate) < 0) { r = -2; - } else { - config->sat_delegate = (sat_delegate_t) v; } break; case CTX_CONFIG_KEY_SAT_DELEGATE_SELECTOR_FRAMES: diff --git a/src/api/search_parameters.c b/src/api/search_parameters.c index d2209f22d..af9d4c8b4 100644 --- a/src/api/search_parameters.c +++ b/src/api/search_parameters.c @@ -346,6 +346,58 @@ static const int32_t sat_delegate_code[NUM_SAT_DELEGATES] = { SAT_DELEGATE_Y2SAT, }; +const char *sat_delegate_name(sat_delegate_t mode) { + switch (mode) { + case SAT_DELEGATE_Y2SAT: + return "y2sat"; + case SAT_DELEGATE_CADICAL: + return "cadical"; + case SAT_DELEGATE_CRYPTOMINISAT: + return "cryptominisat"; + case SAT_DELEGATE_KISSAT: + return "kissat"; + case SAT_DELEGATE_NONE: + default: + return NULL; + } +} + +int32_t parse_sat_delegate(const char *value, sat_delegate_t *v) { + int32_t k; + + k = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES); + assert(k >= 0 || k == -1); + + if (k >= 0) { + assert(SAT_DELEGATE_NONE <= k && k <= SAT_DELEGATE_KISSAT); + *v = (sat_delegate_t) k; + return 0; + } + + return -2; +} + +sat_delegate_t effective_sat_delegate_mode(sat_delegate_t config_delegate, const param_t *params, bool *one_shot) { + sat_delegate_t req; + + req = SAT_DELEGATE_NONE; + if (params != NULL) { + req = params->delegate; + } + + if (req != SAT_DELEGATE_NONE) { + if (one_shot != NULL) { + *one_shot = (req != config_delegate || config_delegate == SAT_DELEGATE_NONE); + } + return req; + } + + if (one_shot != NULL) { + *one_shot = false; + } + return config_delegate; +} + @@ -410,20 +462,7 @@ static int32_t set_branching_param(const char *value, branch_t *v) { * - return -2 otherwise */ static int32_t set_sat_delegate_param(const char *value, sat_delegate_t *v) { - int32_t k; - - k = parse_as_keyword(value, sat_delegate_modes, sat_delegate_code, NUM_SAT_DELEGATES); - assert(k >= 0 || k == -1); - - if (k >= 0) { - assert(SAT_DELEGATE_NONE <= k && k <= SAT_DELEGATE_KISSAT); - *v = (sat_delegate_t) k; - k = 0; - } else { - k = -2; - } - - return k; + return parse_sat_delegate(value, v); } diff --git a/src/api/search_parameters.h b/src/api/search_parameters.h index 24e4340fa..0f1df81e5 100644 --- a/src/api/search_parameters.h +++ b/src/api/search_parameters.h @@ -58,6 +58,13 @@ typedef enum { #define NUM_SAT_DELEGATES 5 +/* + * SAT delegate helpers. + */ +extern const char *sat_delegate_name(sat_delegate_t mode); +extern int32_t parse_sat_delegate(const char *value, sat_delegate_t *v); +extern sat_delegate_t effective_sat_delegate_mode(sat_delegate_t config_delegate, const param_t *params, bool *one_shot); + struct param_s { /* diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 39f4ab36c..caf677b22 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -9395,67 +9395,6 @@ EXPORTED void yices_default_params_for_context(const context_t *ctx, param_t *pa */ static bool check_delegate(const char *delegate); -/* - * Delegate name from SAT delegate mode. - * - return NULL if the default internal SAT solver should be used. - */ -static const char *delegate_name(sat_delegate_t mode) { - const char *s; - - s = NULL; - switch (mode) { - case SAT_DELEGATE_NONE: - break; - case SAT_DELEGATE_Y2SAT: - s = "y2sat"; - break; - case SAT_DELEGATE_CADICAL: - s = "cadical"; - break; - case SAT_DELEGATE_CRYPTOMINISAT: - s = "cryptominisat"; - break; - case SAT_DELEGATE_KISSAT: - s = "kissat"; - break; - default: - assert(false); - break; - } - - return s; -} - -/* - * Delegate selected for this check. - * - if params specifies a delegate (!= none), that delegate is selected. - * - otherwise the delegate from context config is selected. - * - *one_shot is set to true iff params override the context delegate. - */ -static sat_delegate_t effective_delegate_mode(const context_t *ctx, const param_t *params, bool *one_shot) { - sat_delegate_t req, cfg; - - req = SAT_DELEGATE_NONE; - if (params != NULL) { - req = params->delegate; - } - cfg = ctx->sat_delegate; - - if (req != SAT_DELEGATE_NONE) { - if (one_shot != NULL) { - *one_shot = (req != cfg || cfg == SAT_DELEGATE_NONE); - } - return req; - } - - if (one_shot != NULL) { - *one_shot = false; - } - return cfg; -} - - - /* * Check satisfiability: check whether the assertions stored in ctx * are satisfiable. @@ -9514,8 +9453,8 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) yices_default_params_for_context(ctx, &default_params); params = &default_params; } - delegate_mode = effective_delegate_mode(ctx, params, &one_shot_delegate); - delegate = delegate_name(delegate_mode); + delegate_mode = effective_sat_delegate_mode(ctx->sat_delegate, params, &one_shot_delegate); + delegate = sat_delegate_name(delegate_mode); if (delegate == NULL) { stat = check_context(ctx, params); } else { @@ -9526,9 +9465,8 @@ EXPORTED smt_status_t yices_check_context(context_t *ctx, const param_t *params) set_error_code(CTX_OPERATION_NOT_SUPPORTED); return YICES_STATUS_ERROR; } - if (!one_shot_delegate && incremental_delegate(delegate)) { - stat = check_with_incremental_delegate(ctx, delegate, 0, ctx->sat_delegate_selector_frames, - 0, NULL, NULL); + if (!one_shot_delegate && ctx->sat_delegate_selector_frames && incremental_delegate(delegate)) { + stat = check_with_incremental_delegate(ctx, delegate, 0, 0, NULL, NULL); } else { stat = check_with_delegate(ctx, delegate, 0); } diff --git a/src/context/context.h b/src/context/context.h index 5fc993a8b..0ffa0ba3e 100644 --- a/src/context/context.h +++ b/src/context/context.h @@ -401,15 +401,13 @@ extern smt_status_t precheck_context(context_t *ctx); extern smt_status_t check_with_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity); /* - * Incremental delegate solve for QF_BV contexts. + * Incremental selector-frame delegate solve for QF_BV contexts. * - sat_solver must be an incremental delegate (cadical/cryptominisat). - * - selector_frames controls pop handling strategy (ignored by non-incremental delegates). * - assumptions can be NULL if n == 0. * - if failed != NULL and result is UNSAT under assumptions, failed literals are appended to *failed. */ extern smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity, - bool selector_frames, uint32_t n, const literal_t *assumptions, - ivector_t *failed); + uint32_t n, const literal_t *assumptions, ivector_t *failed); /* diff --git a/src/context/context_solver.c b/src/context/context_solver.c index 361b92c55..fa3604978 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -622,7 +622,6 @@ typedef struct delegate_state_s { delegate_t delegate; sat_delegate_t mode; bool live; - bool selector_frames; uint64_t synced_mutation; uint32_t delegate_nvars; bvar_t next_selector_var; @@ -631,44 +630,6 @@ typedef struct delegate_state_s { ivector_t failed; } delegate_state_t; -static const char *delegate_name(sat_delegate_t mode) { - switch (mode) { - case SAT_DELEGATE_Y2SAT: - return "y2sat"; - case SAT_DELEGATE_CADICAL: - return "cadical"; - case SAT_DELEGATE_CRYPTOMINISAT: - return "cryptominisat"; - case SAT_DELEGATE_KISSAT: - return "kissat"; - case SAT_DELEGATE_NONE: - default: - return NULL; - } -} - -static sat_delegate_t effective_delegate_mode(const context_t *ctx, const param_t *params, bool *one_shot) { - sat_delegate_t req, cfg; - - req = SAT_DELEGATE_NONE; - if (params != NULL) { - req = params->delegate; - } - cfg = ctx->sat_delegate; - - if (req != SAT_DELEGATE_NONE) { - if (one_shot != NULL) { - *one_shot = (req != cfg || cfg == SAT_DELEGATE_NONE); - } - return req; - } - - if (one_shot != NULL) { - *one_shot = false; - } - return cfg; -} - void context_delegate_state_cleanup(context_t *ctx) { delegate_state_t *st; @@ -695,7 +656,6 @@ static delegate_state_t *context_get_delegate_state(context_t *ctx) { st = (delegate_state_t *) safe_malloc(sizeof(delegate_state_t)); st->mode = SAT_DELEGATE_NONE; st->live = false; - st->selector_frames = false; st->synced_mutation = 0; st->delegate_nvars = 0; st->next_selector_var = 0; @@ -738,8 +698,7 @@ static void set_delegate_assumption_state(smt_core_t *core, uint32_t n, const li } static bool context_prepare_incremental_delegate(context_t *ctx, delegate_state_t *st, const char *sat_solver, - uint32_t verbosity, bool selector_frames) { - sat_delegate_t mode; + uint32_t verbosity) { smt_core_t *core; uint32_t nvars; literal_t guard; @@ -747,12 +706,8 @@ static bool context_prepare_incremental_delegate(context_t *ctx, delegate_state_ core = ctx->core; nvars = num_vars(core); - mode = effective_delegate_mode(ctx, NULL, NULL); - (void) mode; - if (st->live && - (st->mode != ctx->sat_delegate || - st->selector_frames != selector_frames)) { + if (st->live && st->mode != ctx->sat_delegate) { delete_delegate(&st->delegate); st->live = false; } @@ -763,7 +718,6 @@ static bool context_prepare_incremental_delegate(context_t *ctx, delegate_state_ } delegate_set_verbosity(&st->delegate, verbosity); st->mode = ctx->sat_delegate; - st->selector_frames = selector_frames; st->synced_mutation = 0; st->delegate_nvars = nvars; st->next_selector_var = nvars; @@ -771,40 +725,25 @@ static bool context_prepare_incremental_delegate(context_t *ctx, delegate_state_ st->live = true; } - if (st->selector_frames && st->delegate_nvars < nvars) { + if (st->delegate_nvars < nvars) { nnew = nvars - st->delegate_nvars; delegate_add_vars(&st->delegate, nnew); st->delegate_nvars = nvars; } if (st->synced_mutation != ctx->mutation_count) { - if (st->selector_frames) { - if (st->next_selector_var < st->delegate_nvars) { - st->next_selector_var = st->delegate_nvars; - } - if (st->next_selector_var >= st->delegate_nvars) { - nnew = st->next_selector_var - st->delegate_nvars + 1; - delegate_add_vars(&st->delegate, nnew); - st->delegate_nvars += nnew; - } - guard = neg_lit(st->next_selector_var); - add_problem_clauses_to_delegate(&st->delegate, core, guard); - st->active_selector = pos_lit(st->next_selector_var); - st->next_selector_var ++; - } else { - delete_delegate(&st->delegate); - st->live = false; - if (!init_delegate(&st->delegate, sat_solver, nvars)) { - return false; - } - delegate_set_verbosity(&st->delegate, verbosity); - add_problem_clauses_to_delegate(&st->delegate, core, true_literal); - st->mode = ctx->sat_delegate; - st->delegate_nvars = nvars; - st->next_selector_var = nvars; - st->active_selector = true_literal; - st->live = true; + if (st->next_selector_var < st->delegate_nvars) { + st->next_selector_var = st->delegate_nvars; + } + if (st->next_selector_var >= st->delegate_nvars) { + nnew = st->next_selector_var - st->delegate_nvars + 1; + delegate_add_vars(&st->delegate, nnew); + st->delegate_nvars += nnew; } + guard = neg_lit(st->next_selector_var); + add_problem_clauses_to_delegate(&st->delegate, core, guard); + st->active_selector = pos_lit(st->next_selector_var); + st->next_selector_var ++; st->synced_mutation = ctx->mutation_count; } @@ -812,8 +751,7 @@ static bool context_prepare_incremental_delegate(context_t *ctx, delegate_state_ } smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_solver, uint32_t verbosity, - bool selector_frames, uint32_t n, const literal_t *assumptions, - ivector_t *failed) { + uint32_t n, const literal_t *assumptions, ivector_t *failed) { smt_status_t stat; smt_core_t *core; delegate_state_t *st; @@ -844,14 +782,14 @@ smt_status_t check_with_incremental_delegate(context_t *ctx, const char *sat_sol } st = context_get_delegate_state(ctx); - if (!context_prepare_incremental_delegate(ctx, st, sat_solver, verbosity, selector_frames)) { + if (!context_prepare_incremental_delegate(ctx, st, sat_solver, verbosity)) { return YICES_STATUS_UNKNOWN; } init_ivector(&visible_failed, 0); ivector_reset(&st->assumptions); ivector_reset(&st->failed); - if (st->selector_frames && st->active_selector != true_literal) { + if (st->active_selector != true_literal) { ivector_push(&st->assumptions, st->active_selector); } for (i=0; isat_delegate, params, &one_shot); + delegate = sat_delegate_name(mode); if (delegate == NULL) { stat = check_context_with_assumptions(ctx, params, n, assumptions.data); delete_ivector(&assumptions); @@ -1185,12 +1123,10 @@ smt_status_t check_context_with_term_assumptions(context_t *ctx, const param_t * } init_ivector(&failed, 0); - if (one_shot) { + if (one_shot || !ctx->sat_delegate_selector_frames) { stat = check_with_delegate_assumptions(ctx, delegate, 0, n, assumptions.data, &failed); } else { - stat = check_with_incremental_delegate(ctx, delegate, 0, - ctx->sat_delegate_selector_frames, - n, assumptions.data, &failed); + stat = check_with_incremental_delegate(ctx, delegate, 0, n, assumptions.data, &failed); } if (stat == YICES_STATUS_UNSAT) { cache_failed_assumptions_core(ctx, n, a, &assumptions, &failed); diff --git a/tests/api/context_delegate.c b/tests/api/context_delegate.c index db02ffe48..0548f48d1 100644 --- a/tests/api/context_delegate.c +++ b/tests/api/context_delegate.c @@ -398,6 +398,30 @@ static void check_config_delegate_case(const char *delegate) { yices_free_context(ctx); } +static void check_config_delegate_rebuild_case(const char *delegate) { + type_t bv8; + term_t x, xeq0, xeq1; + context_t *ctx; + + bv8 = yices_bv_type(8); + x = yices_new_uninterpreted_term(bv8); + xeq0 = yices_bveq_atom(x, yices_bvconst_uint32(8, 0)); + xeq1 = yices_bveq_atom(x, yices_bvconst_uint32(8, 1)); + + ctx = new_qfbv_pushpop_context_with_delegate(delegate, "false"); + assert(yices_assert_formula(ctx, xeq0) == 0); + expect_status(ctx, NULL, YICES_STATUS_SAT); + + assert(yices_push(ctx) == 0); + assert(yices_assert_formula(ctx, xeq1) == 0); + expect_status(ctx, NULL, YICES_STATUS_UNSAT); + + assert(yices_pop(ctx) == 0); + expect_status(ctx, NULL, YICES_STATUS_SAT); + + yices_free_context(ctx); +} + static void check_assumptions_delegate_case(const char *delegate) { type_t bv8; term_t x, f, a; @@ -532,6 +556,7 @@ int main(void) { check_nested_pushpop_case(delegates[i]); check_branching_pushpop_case(delegates[i]); check_config_delegate_case(delegates[i]); + check_config_delegate_rebuild_case(delegates[i]); check_assumptions_delegate_case(delegates[i]); check_selector_frames_growing_vars_case(delegates[i]); check_selector_frames_assumptions_case(delegates[i]); From 34ef66ab43d99d14c818db8dd452fde677c59584 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Fri, 8 May 2026 10:36:16 -0700 Subject: [PATCH 8/9] Document context-level SAT delegate API Expand the Third-Party SAT Solvers section of the user manual, the sphinx Contexts and Heuristic Parameters pages, the formula-operations Delegates note, and the comment blocks in yices.h around yices_set_config and yices_set_param so the three documentation surfaces describe the same picture: - sat-delegate context configuration parameter (y2sat / cadical / cryptominisat / kissat) with the capability matrix. - sat-delegate-selector-frames configuration parameter, including the rebuild-on-mutation default and the keep-live behaviour for CaDiCaL / CryptoMiniSat. - delegate per-check search parameter, including the one-shot override semantics relative to the configured context delegate. - Cross-references between formula-operations (one-shot yices_check_formula(s)) and the context-level documentation. --- doc/manual/manual.tex | 77 ++++++++++++++++++++---- doc/sphinx/source/context-operations.rst | 72 ++++++++++++++++++++++ doc/sphinx/source/formula-operations.rst | 13 +++- doc/sphinx/source/parameters.rst | 35 +++++++++++ src/include/yices.h | 43 ++++++++++--- 5 files changed, 218 insertions(+), 22 deletions(-) diff --git a/doc/manual/manual.tex b/doc/manual/manual.tex index b2cafb822..937444777 100644 --- a/doc/manual/manual.tex +++ b/doc/manual/manual.tex @@ -1455,18 +1455,71 @@ \section{MCSAT} non-linear arithmetic are presented in a preprint~\cite{jovanovic2021interpolation}. \section{Third-Party SAT Solvers} +\label{delegates} + +Yices supports using third-party Boolean satisfiability solvers as the +back-end CNF engine for QF\_BV problems. Such solvers, called +\emph{delegates}, are optional but can provide significant performance +improvements. When a delegate is selected, Yices performs ``bit +blasting'' as usual --- converting the problem to an equisatisfiable +SAT problem in conjunctive normal form (CNF) --- and then hands the +resulting CNF to the selected delegate instead of the internal Yices +CDCL SAT solver. Bit-blasting itself is unchanged. + +Yices recognizes four delegate names. \texttt{y2sat} is an internal +SAT solver always available in any Yices build. CaDiCaL, +CryptoMiniSat, and Kissat are external solvers; support for each must +be enabled at compilation time as explained in +Chapter~\ref{compilation}. The capability matrix is summarized below. +\begin{center} +\begin{tabular}{|l|c|c|c|c|} +\hline +Delegate & Always available & Incremental push/pop & + \texttt{check-sat-assuming} & Unsat core from assumptions \\ +\hline +\texttt{y2sat} & yes & rebuild on each check & rebuild on each check & no \\ +\texttt{cadical} & no & yes (selector frames) & yes & yes \\ +\texttt{cryptominisat}& no & yes (selector frames) & yes & yes \\ +\texttt{kissat} & no & rebuild on each check & rebuild on each check & no \\ +\hline +\end{tabular} +\end{center} + +A delegate can be selected in three ways: +\begin{itemize} +\item from the SMT-LIB~2 frontend, by passing + \texttt{--delegate=} to \texttt{yices-smt2} + (Section~\ref{smt2-tool}); +\item from the API, by setting the \texttt{sat-delegate} parameter on + the context configuration with \texttt{yices\_set\_config} before + the context is created; +\item from the API on a per-check basis, by setting the + \texttt{delegate} field of a search-parameter record with + \texttt{yices\_set\_param}, and passing that record to + \texttt{yices\_check\_context} (or one of its variants). +\end{itemize} +The one-shot helpers \texttt{yices\_check\_formula} and +\texttt{yices\_check\_formulas} also accept a delegate name as their +last argument; they bit-blast the input formulas into a fresh CNF and +hand it to the chosen delegate. + +For incremental QF\_BV contexts (\texttt{push-pop} or +\texttt{multi-checks} mode), CaDiCaL and CryptoMiniSat support a +\emph{selector-frames} strategy that keeps the delegate live across +\texttt{check-sat} calls and uses fresh selector literals to retract +clauses on \texttt{pop}. This strategy preserves learned clauses +between checks and is selected by setting the +\texttt{sat-delegate-selector-frames} configuration parameter to +\texttt{"true"} on the context. The default is \texttt{"false"}, in +which case the delegate is rebuilt from the current bit-blasted +problem at every mutation. The non-incremental delegates +\texttt{y2sat} and Kissat are always rebuilt on each check; the +\texttt{sat-delegate-selector-frames} option has no effect for them. -In Yices 2.6.2, we have added support for using third-party Boolean -satisfiability solvers. Such solvers are optional but can provide -significant performance improvements on bit-vector problems. Use of -these SAT solvers is enabled by a command-line option for QF\_BV -problems. If an external solver is selected, Yices will perform ``bit -blasting,'' that is, convert the problem to an equisatisfiable SAT -problem in conjunctive normal form (CNF) and use the selected solver to -check satisfiability of this CNF formula. CaDiCaL and CryptoMiniSat can -be used incrementally. Non-incremental delegates such as \texttt{y2sat} -and Kissat are rebuilt from the current bit-blasted problem on each -incremental check. +The full list of API names recognized by these mechanisms, together +with their possible values and error codes, is documented in the +\texttt{yices.h} header and on the Yices website (see +Section~\ref{full-api}). @@ -3654,6 +3707,7 @@ \section{SMT-LIB 2.x} \subsection{Tool Invocation} +\label{smt2-tool} To run \texttt{yices-smt2} on an input file, type \begin{small} @@ -4652,6 +4706,7 @@ \subsection*{Building and Querying a Model} \section{Full API} +\label{full-api} The main header file \texttt{yices.h} includes documentation about all API functions. We provide more documentation on the Yices website: diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst index 6300ea824..a963ea77f 100644 --- a/doc/sphinx/source/context-operations.rst +++ b/doc/sphinx/source/context-operations.rst @@ -226,6 +226,53 @@ specialized for difference logic and support only mode one-shot. The default mode is push-pop. +.. _sat_delegate_config: + +**SAT Delegate (QF_BV only)** + +For QF_BV contexts, Yices can be configured to use a third-party +Boolean SAT solver --- called a *delegate* --- as the back-end CNF +engine. When a delegate is selected, Yices bit-blasts the assertions +to CNF as usual and hands the resulting clause set to the chosen +delegate instead of the internal Yices CDCL SAT solver. + +Yices recognizes four delegate names. ``y2sat`` is an internal SAT +solver always available in any Yices build. ``cadical``, +``cryptominisat``, and ``kissat`` are external solvers; their +inclusion in a particular Yices build is optional and can be checked +at runtime with :c:func:`yices_has_delegate`. The capabilities of each +delegate are summarized in the following table. + + +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+ + | Delegate | Always available | Incremental push/pop | ``check_with_assumptions``| Unsat core from assumptions | + +===================+===================+=========================+===========================+==================================+ + | ``y2sat`` | yes | rebuild on each check | rebuild on each check | no | + +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+ + | ``cadical`` | optional | yes (selector frames) | yes | yes | + +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+ + | ``cryptominisat`` | optional | yes (selector frames) | yes | yes | + +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+ + | ``kissat`` | optional | rebuild on each check | rebuild on each check | no | + +-------------------+-------------------+-------------------------+---------------------------+----------------------------------+ + +For incremental QF_BV contexts (``push-pop`` or ``multi-checks`` +mode), CaDiCaL and CryptoMiniSat support a *selector-frames* strategy +that keeps the delegate live across :c:func:`yices_check_context` +calls and uses fresh selector literals to retract clauses on +``yices_pop``. This strategy preserves the delegate's learned clauses +between checks. It is opt-in via the +``sat-delegate-selector-frames`` configuration parameter described +below. When the option is ``"false"`` (the default) or the delegate +is non-incremental, Yices rebuilds the delegate from the current +bit-blasted problem at every mutation. + +The delegate can also be selected, or one-shot overridden, on a +per-check basis through the ``delegate`` field of a search-parameter +record (see :ref:`heuristic_parameters`). + +The SAT delegate options are ignored for any logic other than QF_BV. + + Configuration Descriptor ........................ @@ -288,6 +335,31 @@ arithmetic fragment and the operating mode: +--------------------+-----------------------------------------------------+ +Two more parameters control the SAT back-end for QF_BV contexts. +They are ignored for any other logic. See +:ref:`sat_delegate_config` above for the meaning of each value. + + +--------------------------------+---------------------+----------------------------------------------+ + | Name | Value | Meaning | + +================================+=====================+==============================================+ + | sat-delegate | ``"none"`` | use the internal Yices SAT solver (default) | + | +---------------------+----------------------------------------------+ + | | ``"y2sat"`` | use y2sat as the SAT back-end | + | +---------------------+----------------------------------------------+ + | | ``"cadical"`` | use CaDiCaL as the SAT back-end | + | +---------------------+----------------------------------------------+ + | | ``"cryptominisat"`` | use CryptoMiniSat as the SAT back-end | + | +---------------------+----------------------------------------------+ + | | ``"kissat"`` | use Kissat as the SAT back-end | + +--------------------------------+---------------------+----------------------------------------------+ + | sat-delegate-selector-frames | ``"false"`` | rebuild the delegate on each context | + | | | mutation (default) | + | +---------------------+----------------------------------------------+ + | | ``"true"`` | keep an incremental delegate live across | + | | | checks using selector-guarded frames | + +--------------------------------+---------------------+----------------------------------------------+ + + A configuration descriptor also stores a logic flag, which can either be *unknown* (i.e., no logic specified), or the name of an SMT-LIB diff --git a/doc/sphinx/source/formula-operations.rst b/doc/sphinx/source/formula-operations.rst index d8e443185..a7ba2d25a 100644 --- a/doc/sphinx/source/formula-operations.rst +++ b/doc/sphinx/source/formula-operations.rst @@ -69,21 +69,28 @@ third-party Boolean satisfiability solvers for bit-vector problems. A delegate is a SAT solver to use as backend when checking satisfiability of a bit-vector formula. The *delegate* parameter is ignored and has no effect unless the *logic* is "QF_BV". - In the latter case, three different delegates can be used: + In the latter case, four different delegates can be used: - "cadical": the CaDiCaL solver (https://github.com/arminbiere/cadical) - - "cryptominisat: the CryptoMiniSat solver (https://github.com/msoos/cryptominisat) + - "cryptominisat": the CryptoMiniSat solver (https://github.com/msoos/cryptominisat) + + - "kissat": the Kissat solver (https://github.com/arminbiere/kissat) - "y2sat": an experimental SAT solver included in Yices - These three delegates are known to Yices but support for CaDiCaL and CryptoMiniSat is optional. + These four delegates are known to Yices but support for CaDiCaL, CryptoMiniSat, and Kissat is optional. They may or may not be available depending on how the Yices library was configured and compiled. The "y2sat" delegate is always available. If *delegate* is NULL, the default SAT solver internal to Yices is used (which can be much slower than state-of-the-art solvers such as CaDiCaL). + The same delegates can also be used through the regular context API + --- including with push/pop and ``check-sat-assuming`` --- by setting + the ``sat-delegate`` configuration parameter on a QF_BV context. See + :ref:`sat_delegate_config`. + **Examples** diff --git a/doc/sphinx/source/parameters.rst b/doc/sphinx/source/parameters.rst index f0ad3c71e..c797732d2 100644 --- a/doc/sphinx/source/parameters.rst +++ b/doc/sphinx/source/parameters.rst @@ -472,3 +472,38 @@ Flattening *(<=> p q)* rewrites the term to *(and (=> p q) (=> q p))* Flattening *(ite c p q)* rewrites the term to *(and (=> c p) (=> (not c) q)* + + +SAT Delegate Selection (QF_BV) +------------------------------ + +For QF_BV contexts, the back-end SAT solver --- called a *delegate* +--- can be selected on a per-check basis through the following +parameter. + + +------------+-----------------+---------------------------------------------+ + | Parameter | Value | Meaning | + | Name | | | + +============+=================+=============================================+ + | delegate | none | use the SAT back-end configured on the | + | | | context (default) | + | +-----------------+---------------------------------------------+ + | | y2sat | use y2sat for this check | + | +-----------------+---------------------------------------------+ + | | cadical | use CaDiCaL for this check | + | +-----------------+---------------------------------------------+ + | | cryptominisat | use CryptoMiniSat for this check | + | +-----------------+---------------------------------------------+ + | | kissat | use Kissat for this check | + +------------+-----------------+---------------------------------------------+ + +If a delegate is set in the parameter record and it differs from the +delegate configured on the context (see :ref:`sat_delegate_config`), +the parameter takes effect for that single call only and the persistent +delegate state of the context is left untouched. If the parameter is +``"none"``, the context's configured delegate is used. + +A delegate name in this parameter has no effect for any logic other +than QF_BV. Whether a particular delegate is available in the current +Yices build can be checked with :c:func:`yices_has_delegate`. + diff --git a/src/include/yices.h b/src/include/yices.h index 82b17a098..afcdd603f 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -2971,11 +2971,28 @@ __YICES_DLLSPEC__ extern void yices_free_config(ctx_config_t *config); * | "true" | keep an incremental delegate live * | | using selector-guarded frames * - * The SAT delegate options have an effect only for QF_BV contexts. - * CaDiCaL and CryptoMiniSat support incremental delegate checks. Non-incremental - * delegates such as y2sat and Kissat are rebuilt from the current bit-blasted - * problem on each incremental check. "sat-delegate-selector-frames" is ignored - * for non-incremental delegates. + * The SAT delegate options have an effect only for QF_BV contexts. When a + * delegate is selected, Yices bit-blasts the bit-vector assertions to CNF as + * usual and hands the resulting clause set to the chosen delegate instead of + * the internal Yices CDCL SAT solver. + * + * Delegate capability matrix: + * y2sat : always available; rebuilt on each incremental check + * cadical : optional (build flag); incremental, supports check-with- + * assumptions and unsat-core extraction from assumptions + * cryptominisat : optional (build flag); incremental, supports check-with- + * assumptions and unsat-core extraction from assumptions + * kissat : optional (build flag); rebuilt on each incremental check + * + * "sat-delegate-selector-frames" controls how push/pop is realised against an + * incremental delegate: "false" rebuilds the delegate from the current bit- + * blasted problem on every mutation (simpler, loses the delegate's learned + * clauses), "true" keeps the delegate live across checks with selector-guarded + * frames (preserves learned clauses). The option is ignored for non-incremental + * delegates. + * + * yices_has_delegate() reports whether a particular delegate name is included + * in the current Yices build. * * The function returns -1 if there's an error, 0 otherwise. * @@ -3608,9 +3625,19 @@ __YICES_DLLSPEC__ extern void yices_default_params_for_context(const context_t * * * For QF_BV contexts, parameter name "delegate" can be set to "none", * "y2sat", "cadical", "cryptominisat", or "kissat" to select the SAT - * backend used by yices_check_context. - * In incremental contexts, non-incremental delegates such as y2sat and Kissat - * are rebuilt from the current bit-blasted problem on each check. + * backend used by yices_check_context (and its variants). + * + * If "delegate" differs from the SAT delegate configured on the context (see + * "sat-delegate" in yices_set_config), it takes effect for that single call + * only; the persistent delegate state of the context is left untouched. If + * "delegate" is "none" (the default), the context's configured delegate is + * used. + * + * In incremental contexts, non-incremental delegates (y2sat and Kissat) are + * rebuilt from the current bit-blasted problem on each check. CaDiCaL and + * CryptoMiniSat support incremental delegate checks (see "sat-delegate- + * selector-frames" in yices_set_config). The "delegate" parameter is ignored + * for any logic other than QF_BV. * * Return -1 if there's an error, 0 otherwise. * From 29fc55e08551141ea6d56c13f6b54a6b2304c05f Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Fri, 8 May 2026 10:59:47 -0700 Subject: [PATCH 9/9] Address review: kissat in API docs, default regress mode = off Two low-severity follow-ups from review. 1. yices_check_formula / yices_check_formulas (src/include/yices.h): the public API comment listed valid delegates as "cadical", "cryptominisat", "y2sat" only. The implementation and the rest of the documentation already accept "kissat"; add it to the public header in three places: the valid-delegate list, the build-time note, and the CTX_UNKNOWN_DELEGATE / CTX_DELEGATE_NOT_AVAILABLE error descriptions. 2. tests/regress/check.sh: change the default of REGRESS_DELEGATE_MODE from "auto" to "off". The previous default silently fanned every "make check" / "make regress" out into one extra pass per installed delegate on QF_BV tests, which inflated CI runtime on machines with CaDiCaL / CryptoMiniSat / Kissat installed. The opt-in "make delegate-regress" / "make static-delegate-regress" targets already set REGRESS_DELEGATE_MODE=only explicitly, so they keep working unchanged. Users wanting the combined coverage in a single pass can set REGRESS_DELEGATE_MODE=auto by hand. Documented the three modes inline in check.sh so the default choice has a discoverable rationale. --- src/include/yices.h | 15 ++++++++------- tests/regress/check.sh | 11 ++++++++++- 2 files changed, 18 insertions(+), 8 deletions(-) diff --git a/src/include/yices.h b/src/include/yices.h index 636c9575d..9c111c5e3 100644 --- a/src/include/yices.h +++ b/src/include/yices.h @@ -3998,12 +3998,13 @@ __YICES_DLLSPEC__ extern void yices_model_collect_defined_terms(model_t *mdl, te * The delegate is an optional argument used only when logic is "QF_BV". * If is ignored otherwise. It must either be NULL or be the name of an * external SAT solver to use after bit-blasting. Valid delegates - * are "cadical", "cryptominisat", and "y2sat". + * are "cadical", "cryptominisat", "kissat", and "y2sat". * If delegate is NULL, the default SAT solver is used. * - * Support for "cadical" and "cryptominisat" must be enabled at compilation - * time. The "y2sat" solver is always available. The function will return YICES_STATUS_ERROR - * and store an error code if the requested delegate is not available. + * Support for "cadical", "cryptominisat", and "kissat" must be enabled + * at compilation time. The "y2sat" solver is always available. The + * function will return YICES_STATUS_ERROR and store an error code if + * the requested delegate is not available. * * Error codes: * @@ -4022,11 +4023,11 @@ __YICES_DLLSPEC__ extern void yices_model_collect_defined_terms(model_t *mdl, te * if the logic is known but not supported by Yices * code = CTX_LOGIC_NOT_SUPPORTED * - * if delegate is not one of "cadical", "cryptominisat", "y2sat" + * if delegate is not one of "cadical", "cryptominisat", "kissat", "y2sat" * code = CTX_UNKNOWN_DELEGATE * - * if delegate is "cadical" or "cryptominisat" but support for these SAT solvers - * was not implemented at compile time, + * if delegate is "cadical", "cryptominisat", or "kissat" but support + * for that SAT solver was not implemented at compile time, * code = CTX_DELEGATE_NOT_AVAILABLE * * other error codes are possible if the formula is not in the specified logic (cf. yices_assert_formula) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 2e2e5c8e0..410848762 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -155,8 +155,17 @@ bin_dir=$2 shift 2 all_tests="$@" +# REGRESS_DELEGATE_MODE selects whether the regression run also fans out +# into one extra pass per installed external SAT delegate (CaDiCaL, +# CryptoMiniSat, Kissat) on QF_BV tests: +# +# off : baseline pass only. This is the default so that "make check" +# and "make regress" keep their pre-delegate runtime. +# auto : baseline pass + one pass per installed delegate (opt-in). +# only : delegate passes only, no baseline. Used by the +# delegate-regress / static-delegate-regress make targets. if [[ -z "$REGRESS_DELEGATE_MODE" ]]; then - REGRESS_DELEGATE_MODE="auto" + REGRESS_DELEGATE_MODE="off" fi case "$REGRESS_DELEGATE_MODE" in