From 51785b09abffbacbfd9c599fc7648936291b055e Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 9 Mar 2026 20:21:20 -0700 Subject: [PATCH 1/3] Draft: integrate supplementary MCSAT satellite in CDCL(T) --- src/Makefile | 1 + src/api/search_parameters.c | 47 +- src/api/search_parameters.h | 18 + src/api/yices_api.c | 1 + src/context/context.c | 528 ++++++++++ src/context/context_simplifier.c | 40 +- src/context/context_solver.c | 187 +++- src/context/context_types.h | 5 +- src/context/context_utils.h | 9 +- src/context/shared_terms.c | 21 +- src/frontend/common/parameters.c | 39 + src/frontend/common/parameters.h | 7 + src/frontend/smt2/smt2_commands.c | 59 +- src/frontend/smt2/smt2_commands.h | 7 + src/frontend/yices/yices_help.c | 14 +- src/frontend/yices/yices_reval.c | 13 +- src/frontend/yices_smt2.c | 20 +- src/mcsat/solver.c | 19 +- src/solvers/egraph/egraph.c | 68 ++ src/solvers/egraph/egraph.h | 16 + src/solvers/egraph/egraph_base_types.h | 15 +- src/solvers/egraph/egraph_printer.c | 5 +- src/solvers/egraph/egraph_types.h | 2 + src/solvers/mcsat_satellite.c | 1132 ++++++++++++++++++++++ src/solvers/mcsat_satellite.h | 85 ++ src/terms/term_explorer.c | 16 +- tests/regress/both/README.md | 16 + tests/regress/both/smoke_sat.smt2 | 4 + tests/regress/both/smoke_sat.smt2.gold | 1 + tests/regress/both/smoke_unsat.smt2 | 5 + tests/regress/both/smoke_unsat.smt2.gold | 1 + tests/regress/check.sh | 2 +- tests/regress/run_test.sh | 130 ++- 33 files changed, 2442 insertions(+), 91 deletions(-) create mode 100644 src/solvers/mcsat_satellite.c create mode 100644 src/solvers/mcsat_satellite.h create mode 100644 tests/regress/both/README.md create mode 100644 tests/regress/both/smoke_sat.smt2 create mode 100644 tests/regress/both/smoke_sat.smt2.gold create mode 100644 tests/regress/both/smoke_unsat.smt2 create mode 100644 tests/regress/both/smoke_unsat.smt2.gold diff --git a/src/Makefile b/src/Makefile index b3a79be6e..b646acc6f 100644 --- a/src/Makefile +++ b/src/Makefile @@ -198,6 +198,7 @@ core_src_c := \ solvers/egraph/egraph_explanations.c \ solvers/egraph/egraph_utils.c \ solvers/egraph/theory_explanations.c \ + solvers/mcsat_satellite.c \ solvers/floyd_warshall/dl_vartable.c \ solvers/floyd_warshall/idl_floyd_warshall.c \ solvers/floyd_warshall/rdl_floyd_warshall.c \ diff --git a/src/api/search_parameters.c b/src/api/search_parameters.c index a798e352d..105c9e704 100644 --- a/src/api/search_parameters.c +++ b/src/api/search_parameters.c @@ -101,6 +101,7 @@ #define DEFAULT_USE_BOOL_DYN_ACK false #define DEFAULT_USE_OPTIMISTIC_FCHECK true #define DEFAULT_AUX_EQ_RATIO 0.3 +#define DEFAULT_MCSAT_SUPPLEMENT_CHECK MCSAT_SUPPLEMENT_CHECK_BOTH /* @@ -165,6 +166,7 @@ static const param_t default_settings = { DEFAULT_MAX_UPDATE_CONFLICTS, DEFAULT_MAX_EXTENSIONALITY, + DEFAULT_MCSAT_SUPPLEMENT_CHECK, }; @@ -221,9 +223,10 @@ typedef enum param_key { // array solver PARAM_MAX_UPDATE_CONFLICTS, PARAM_MAX_EXTENSIONALITY, + PARAM_MCSAT_SUPPLEMENT_CHECK, } param_key_t; -#define NUM_PARAM_KEYS (PARAM_MAX_EXTENSIONALITY+1) +#define NUM_PARAM_KEYS (PARAM_MCSAT_SUPPLEMENT_CHECK+1) // parameter names in lexicographic ordering static const char *const param_key_names[NUM_PARAM_KEYS] = { @@ -249,6 +252,7 @@ static const char *const param_key_names[NUM_PARAM_KEYS] = { "max-extensionality", "max-interface-eqs", "max-update-conflicts", + "mcsat-supplement-check", "optimistic-final-check", "prop-threshold", "r-factor", @@ -286,6 +290,7 @@ static const int32_t param_code[NUM_PARAM_KEYS] = { PARAM_MAX_EXTENSIONALITY, PARAM_MAX_INTERFACE_EQS, PARAM_MAX_UPDATE_CONFLICTS, + PARAM_MCSAT_SUPPLEMENT_CHECK, PARAM_OPTIMISTIC_FCHECK, PARAM_PROP_THRESHOLD, PARAM_R_FACTOR, @@ -322,6 +327,19 @@ static const int32_t branching_code[NUM_BRANCHING_MODES] = { BRANCHING_THEORY, }; +/* + * Supplementary MCSAT checking modes (in lexicographic order) + */ +static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + "both", + "final-only", +}; + +static const int32_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + MCSAT_SUPPLEMENT_CHECK_BOTH, + MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY, +}; + @@ -380,6 +398,29 @@ static int32_t set_branching_param(const char *value, branch_t *v) { return k; } +/* + * Parse value as supplementary MCSAT check mode. Store the result in *v. + * - return 0 if this works + * - return -2 otherwise + */ +static int32_t set_mcsat_supplement_check_param(const char *value, mcsat_supplement_check_t *v) { + int32_t k; + + k = parse_as_keyword(value, mcsat_supplement_check_modes, mcsat_supplement_check_code, + NUM_MCSAT_SUPPLEMENT_CHECK_MODES); + assert(k >= 0 || k == -1); + + if (k >= 0) { + assert(MCSAT_SUPPLEMENT_CHECK_BOTH <= k && k <= MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY); + *v = (mcsat_supplement_check_t) k; + k = 0; + } else { + k = -2; + } + + return k; +} + /* * Parse val as a signed 32bit integer. Check whether @@ -685,6 +726,10 @@ int32_t params_set_field(param_t *parameters, const char *key, const char *value } break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + r = set_mcsat_supplement_check_param(value, ¶meters->mcsat_supplement_check); + break; + default: assert(k == -1); r = -1; diff --git a/src/api/search_parameters.h b/src/api/search_parameters.h index ddcb4b158..57ff401b5 100644 --- a/src/api/search_parameters.h +++ b/src/api/search_parameters.h @@ -45,6 +45,17 @@ typedef enum { #define NUM_BRANCHING_MODES 6 +/* + * Supplementary MCSAT check mode (for CDCL(T) mode) + */ +typedef enum { + MCSAT_SUPPLEMENT_CHECK_BOTH, + MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY, +} mcsat_supplement_check_t; + +// keep in sync with mcsat_supplement_check_modes in search_parameters.c +#define NUM_MCSAT_SUPPLEMENT_CHECK_MODES 2 + struct param_s { /* @@ -170,6 +181,13 @@ struct param_s { uint32_t max_update_conflicts; uint32_t max_extensionality; + /* + * Supplementary MCSAT checks in CDCL(T) + * - BOTH: run in propagate and final_check + * - FINAL_ONLY: run in final_check only + */ + mcsat_supplement_check_t mcsat_supplement_check; + }; diff --git a/src/api/yices_api.c b/src/api/yices_api.c index 6eedb9aba..1b28e2598 100644 --- a/src/api/yices_api.c +++ b/src/api/yices_api.c @@ -8693,6 +8693,7 @@ static const error_code_t intern_code2error[NUM_INTERNALIZATION_ERRORS] = { CTX_BV_SOLVER_EXCEPTION, MCSAT_ERROR_UNSUPPORTED_THEORY, CTX_HIGH_ORDER_FUN_NOT_SUPPORTED, + MCSAT_ERROR_UNSUPPORTED_THEORY, }; static inline void convert_internalization_error(int32_t code) { diff --git a/src/context/context.c b/src/context/context.c index 27ee78d96..17339ea70 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -22,6 +22,7 @@ #include +#include "api/context_config.h" #include "context/context.h" #include "context/context_simplifier.h" #include "context/context_utils.h" @@ -31,10 +32,13 @@ #include "solvers/floyd_warshall/idl_floyd_warshall.h" #include "solvers/floyd_warshall/rdl_floyd_warshall.h" #include "solvers/funs/fun_solver.h" +#include "solvers/mcsat_satellite.h" #include "solvers/quant/quant_solver.h" #include "solvers/simplex/simplex.h" #include "terms/poly_buffer_terms.h" +#include "terms/term_explorer.h" #include "terms/term_utils.h" +#include "utils/int_hash_map.h" #include "utils/memalloc.h" #include "mcsat/solver.h" @@ -73,6 +77,424 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t); static thvar_t internalize_to_arith(context_t *ctx, term_t t); static thvar_t internalize_to_bv(context_t *ctx, term_t t); +static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx); +static bool context_atom_requires_mcsat(context_t *ctx, term_t atom); +static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom); +static int32_t context_enable_mcsat_supplement(context_t *ctx); +static void context_disable_mcsat_supplement(context_t *ctx); +static bool context_assertions_need_mcsat_supplement(context_t *ctx, uint32_t n, const term_t *a); +static int32_t context_seed_mcsat_satellite(context_t *ctx); + + +/* + * Supplementary MCSAT support (CDCL(T) mode) + */ +static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx) { + if (ctx->egraph == NULL) { + return NULL; + } + return (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; +} + +static inline bool divisor_requires_mcsat(term_table_t *terms, term_t t) { + t = unsigned_term(t); + if (term_kind(terms, t) != ARITH_CONSTANT) { + return true; + } + return q_is_zero(rational_term_desc(terms, t)); +} + +/* + * Detect whether t contains arithmetic or finite-field subterms. + * This is used to route all relevant arithmetic/FF atoms to the supplementary + * MCSAT context once supplementation is active. + */ +static bool term_contains_arith_or_ff(context_t *ctx, term_t t, int_hmap_t *cache) { + term_table_t *terms; + int_hmap_pair_t *p; + type_t tau; + type_kind_t tkind; + bool found; + uint32_t i, nchildren; + + if (t < 0) { + return false; + } + + t = unsigned_term(t); + p = int_hmap_find(cache, t); + if (p != NULL) { + return p->val != 0; + } + + terms = ctx->terms; + tau = term_type(terms, t); + tkind = type_kind(terms->types, tau); + + /* + * Variables of arithmetic/finite-field type may not satisfy + * is_arithmetic_term/is_finitefield_term, so include type-based detection. + */ + found = is_arithmetic_term(terms, t) || is_finitefield_term(terms, t) || + tkind == INT_TYPE || tkind == REAL_TYPE || is_ff_type(terms->types, tau); + + if (!found) { + if (term_is_projection(terms, t)) { + found = term_contains_arith_or_ff(ctx, proj_term_arg(terms, t), cache); + + } else if (term_is_sum(terms, t)) { + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + term_t child; + mpq_t q; + mpq_init(q); + sum_term_component(terms, t, i, q, &child); + found = term_contains_arith_or_ff(ctx, child, cache); + mpq_clear(q); + } + + } else if (term_is_bvsum(terms, t)) { + int32_t *aux; + uint32_t nbits; + term_t child; + + nbits = term_bitsize(terms, t); + aux = (int32_t *) safe_malloc(nbits * sizeof(int32_t)); + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + bvsum_term_component(terms, t, i, aux, &child); + found = term_contains_arith_or_ff(ctx, child, cache); + } + safe_free(aux); + + } else if (term_is_product(terms, t)) { + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + term_t child; + uint32_t exp; + product_term_component(terms, t, i, &child, &exp); + found = term_contains_arith_or_ff(ctx, child, cache); + } + + } else if (term_is_composite(terms, t)) { + nchildren = term_num_children(terms, t); + for (i = 0; i < nchildren && !found; i++) { + found = term_contains_arith_or_ff(ctx, term_child(terms, t, i), cache); + } + } + } + + p = int_hmap_get(cache, t); + p->val = found ? 1 : 0; + return found; +} + +static bool term_requires_mcsat_supplement(context_t *ctx, term_t t, int_hmap_t *cache) { + term_table_t *terms; + int_hmap_pair_t *p; + bool trigger; + uint32_t i, nchildren; + + if (t < 0) { + return false; + } + + t = unsigned_term(t); + p = int_hmap_find(cache, t); + if (p != NULL) { + return p->val != 0; + } + + terms = ctx->terms; + trigger = false; + + // finite-field usage + if (is_finitefield_term(terms, t)) { + trigger = true; + } + + if (!trigger) { + switch (term_kind(terms, t)) { + case ARITH_ROOT_ATOM: + case ARITH_FF_CONSTANT: + case ARITH_FF_POLY: + case ARITH_FF_EQ_ATOM: + case ARITH_FF_BINEQ_ATOM: + trigger = true; + break; + + case ARITH_RDIV: + trigger = divisor_requires_mcsat(terms, arith_rdiv_term_desc(terms, t)->arg[1]); + break; + + case ARITH_IDIV: + trigger = divisor_requires_mcsat(terms, arith_idiv_term_desc(terms, t)->arg[1]); + break; + + case ARITH_MOD: + trigger = divisor_requires_mcsat(terms, arith_mod_term_desc(terms, t)->arg[1]); + break; + + case ARITH_DIVIDES_ATOM: + trigger = divisor_requires_mcsat(terms, arith_divides_atom_desc(terms, t)->arg[0]); + break; + + default: + break; + } + } + + // arithmetic nonlinearity (including deep products in arithmetic predicates) + if (!trigger && is_arithmetic_term(terms, t) && term_degree(terms, t) > 1) { + trigger = true; + } + + if (!trigger) { + if (term_is_projection(terms, t)) { + trigger = term_requires_mcsat_supplement(ctx, proj_term_arg(terms, t), cache); + + } else if (term_is_sum(terms, t)) { + nchildren = term_num_children(terms, t); + for (i=0; ival = trigger ? 1 : 0; + return trigger; +} + +static bool context_assertions_need_mcsat_supplement(context_t *ctx, uint32_t n, const term_t *a) { + int_hmap_t cache; + uint32_t i; + bool trigger; + + init_int_hmap(&cache, 0); + trigger = false; + for (i=0; imcsat_supplement_active) { + return CTX_NO_ERROR; + } + if (ctx->arch == CTX_ARCH_MCSAT || ctx->egraph == NULL) { + return CONTEXT_UNSUPPORTED_THEORY; + } + + sat = new_mcsat_satellite(ctx); + egraph_attach_mcsat_solver(ctx->egraph, sat, + mcsat_satellite_ctrl_interface(sat), + mcsat_satellite_smt_interface(sat), + mcsat_satellite_egraph_interface(sat)); + ctx->mcsat_supplement_active = true; + + code = context_seed_mcsat_satellite(ctx); + if (code < 0) { + context_disable_mcsat_supplement(ctx); + return code; + } + + return CTX_NO_ERROR; +} + +static void context_disable_mcsat_supplement(context_t *ctx) { + mcsat_satellite_t *sat; + + if (!ctx->mcsat_supplement_active || ctx->egraph == NULL) { + return; + } + + sat = context_mcsat_satellite(ctx); + egraph_detach_mcsat_solver(ctx->egraph); + delete_mcsat_satellite(sat); + ctx->mcsat_supplement_active = false; +} + +/* + * Import already-internalized arithmetic/FF atoms when supplementary MCSAT + * is activated after earlier assertions. + */ +static int32_t context_seed_mcsat_satellite(context_t *ctx) { + mcsat_satellite_t *sat; + term_table_t *terms; + uint32_t i, n; + uint32_t seeded = 0; + bool trace_seed; + + sat = context_mcsat_satellite(ctx); + if (sat == NULL) { + return CTX_NO_ERROR; + } + + terms = ctx->terms; + trace_seed = tracing_tag(ctx->trace, "mcsat::supplement::seed"); + n = intern_tbl_num_terms(&ctx->intern); + for (i = 1; i < n; i++) { + term_t t; + int32_t code; + literal_t l; + + if (!good_term_idx(terms, i)) { + continue; + } + + t = pos_term(i); + if (!is_boolean_term(terms, t) || + !intern_tbl_is_root(&ctx->intern, t) || + !intern_tbl_root_is_mapped(&ctx->intern, t)) { + continue; + } + + if (!context_atom_requires_mcsat(ctx, t)) { + continue; + } + + code = intern_tbl_map_of_root(&ctx->intern, t); + if (code_is_var(code)) { + l = code2literal(code); + } else { + occ_t u = code2occ(code); + if (u == true_occ) { + l = true_literal; + } else if (u == false_occ) { + l = false_literal; + } else if (ctx->egraph != NULL) { + l = egraph_occ2literal(ctx->egraph, u); + } else { + continue; + } + } + + code = mcsat_satellite_register_atom(sat, t, l, NULL); + if (code < 0) { + return code; + } + seeded ++; + if (trace_seed) { + trace_printf(ctx->trace, 1, "mcsat supplement seed: lit=%"PRId32" atom=", l); + trace_pp_term(ctx->trace, 1, terms, t); + } + } + + if (trace_seed) { + trace_printf(ctx->trace, 1, "mcsat supplement seeded %"PRIu32" atoms\n", seeded); + } + + return CTX_NO_ERROR; +} + +static bool mcsat_satellite_candidate_atom(term_table_t *terms, term_t atom) { + switch (term_kind(terms, atom)) { + case EQ_TERM: + case DISTINCT_TERM: + case ARITH_ROOT_ATOM: + case ARITH_FF_EQ_ATOM: + case ARITH_FF_BINEQ_ATOM: + case ARITH_IS_INT_ATOM: + case ARITH_EQ_ATOM: + case ARITH_GE_ATOM: + case ARITH_BINEQ_ATOM: + case ARITH_DIVIDES_ATOM: + return true; + + default: + return false; + } +} + +static bool context_atom_requires_mcsat(context_t *ctx, term_t atom) { + int_hmap_t cache; + bool trigger, all_arith_mode; + + atom = unsigned_term(atom); + if (!ctx->mcsat_supplement_active || !is_boolean_term(ctx->terms, atom)) { + return false; + } + if (!mcsat_satellite_candidate_atom(ctx->terms, atom)) { + return false; + } + + init_int_hmap(&cache, 0); + /* + * In supplementary mode, route every arithmetic/FF atom to MCSAT so that + * MCSAT sees the complete arithmetic conjunction (not just unsupported atoms). + */ + all_arith_mode = true; + if (all_arith_mode) { + trigger = term_contains_arith_or_ff(ctx, atom, &cache); + } else { + trigger = term_requires_mcsat_supplement(ctx, atom, &cache); + } + delete_int_hmap(&cache); + + return trigger; +} + +static literal_t map_mcsat_atom_to_literal(context_t *ctx, term_t atom) { + mcsat_satellite_t *sat; + literal_t l; + void *obj; + int32_t code; + + sat = context_mcsat_satellite(ctx); + assert(sat != NULL); + + l = pos_lit(create_boolean_variable(ctx->core)); + obj = NULL; + code = mcsat_satellite_register_atom(sat, atom, l, &obj); + if (code < 0) { + longjmp(ctx->env, code); + } + + attach_atom_to_bvar(ctx->core, var_of(l), tagged_mcsat_atom(obj)); + return l; +} + /**************************************** @@ -1848,6 +2270,13 @@ static thvar_t map_bvpoly_buffer_to_bv(context_t *ctx, bvpoly_buffer_t *b) { free_bvpoly(q); } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_register_arith_term(sat, x, r); + } + } + return x; } @@ -2930,6 +3359,14 @@ static thvar_t internalize_to_arith(context_t *ctx, term_t t) { } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat; + sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_register_arith_term(sat, x, unsigned_term(r)); + } + } + return x; abort: @@ -3185,6 +3622,12 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t) { /* * Recursively compute r's internalization */ + if (context_atom_requires_mcsat(ctx, r)) { + l = map_mcsat_atom_to_literal(ctx, r); + intern_tbl_map_root(&ctx->intern, r, literal2code(l)); + goto done; + } + terms = ctx->terms; switch (term_kind(terms, r)) { case CONSTANT_TERM: @@ -3237,6 +3680,15 @@ static literal_t internalize_to_literal(context_t *ctx, term_t t) { l = map_arith_divides_to_literal(ctx, arith_divides_atom_desc(terms, r)); break; + case ARITH_ROOT_ATOM: + longjmp(ctx->env, FORMULA_NOT_LINEAR); + break; + + case ARITH_FF_EQ_ATOM: + case ARITH_FF_BINEQ_ATOM: + longjmp(ctx->env, CONTEXT_UNSUPPORTED_THEORY); + break; + case APP_TERM: l = map_apply_to_literal(ctx, app_term_desc(terms, r)); break; @@ -4688,6 +5140,7 @@ static void assert_toplevel_bvsge(context_t *ctx, composite_term_t *sge, bool tt static void assert_toplevel_formula(context_t *ctx, term_t t) { term_table_t *terms; int32_t code; + literal_t l; bool tt; assert(is_boolean_term(ctx->terms, t) && @@ -4704,6 +5157,14 @@ static void assert_toplevel_formula(context_t *ctx, term_t t) { * tt false: assert (not t) */ terms = ctx->terms; + if (context_atom_requires_mcsat(ctx, t)) { + l = map_mcsat_atom_to_literal(ctx, t); + code = literal2code(l); + intern_tbl_remap_root(&ctx->intern, t, code); + assert_internalization_code(ctx, code, tt); + return; + } + switch (term_kind(terms, t)) { case CONSTANT_TERM: case UNINTERPRETED_TERM: @@ -4808,6 +5269,7 @@ static void assert_toplevel_formula(context_t *ctx, term_t t) { static void assert_term(context_t *ctx, term_t t, bool tt) { term_table_t *terms; int32_t code; + literal_t l; assert(is_boolean_term(ctx->terms, t)); @@ -4829,6 +5291,14 @@ static void assert_term(context_t *ctx, term_t t, bool tt) { assert_internalization_code(ctx, code, tt); } else { + if (context_atom_requires_mcsat(ctx, t)) { + l = map_mcsat_atom_to_literal(ctx, t); + code = literal2code(l); + intern_tbl_map_root(&ctx->intern, t, code); + assert_internalization_code(ctx, code, tt); + return; + } + // store the mapping t --> tt intern_tbl_map_root(&ctx->intern, t, bool2code(tt)); @@ -5499,6 +5969,7 @@ static void init_solvers(context_t *ctx) { ctx->bv_solver = NULL; ctx->fun_solver = NULL; ctx->quant_solver = NULL; + ctx->mcsat_supplement_active = false; // Create egraph first, then satellite solvers if (solvers & EGRPH) { @@ -5745,6 +6216,10 @@ void delete_context(context_t *ctx) { ctx->mcsat = NULL; } + if (ctx->mcsat_supplement_active) { + context_disable_mcsat_supplement(ctx); + } + if (ctx->egraph != NULL) { delete_egraph(ctx->egraph); safe_free(ctx->egraph); @@ -5835,6 +6310,10 @@ void reset_context(context_t *ctx) { reset_smt_core(ctx->core); // this propagates reset to all solvers + if (ctx->mcsat_supplement_active) { + context_disable_mcsat_supplement(ctx); + } + if (ctx->mcsat != NULL) { mcsat_reset(ctx->mcsat); } @@ -5892,6 +6371,12 @@ void context_set_trace(context_t *ctx, tracer_t *trace) { if (ctx->mcsat != NULL) { mcsat_set_tracer(ctx->mcsat, trace); } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_set_trace(sat, trace); + } + } } @@ -5997,6 +6482,25 @@ static int32_t context_process_assertions(context_t *ctx, uint32_t n, const term ivector_reset(&ctx->aux_eqs); ivector_reset(&ctx->aux_atoms); + if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx)) { + if (context_assertions_need_mcsat_supplement(ctx, n, a)) { + code = context_enable_mcsat_supplement(ctx); + if (code < 0) { + return code; + } + } + } + + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + code = mcsat_satellite_assert_formulas(sat, n, a); + if (code < 0) { + return code; + } + } + } + code = setjmp(ctx->env); if (code == 0) { @@ -6336,6 +6840,15 @@ int32_t context_internalize(context_t *ctx, term_t t) { ivector_reset(&ctx->subst_eqs); ivector_reset(&ctx->aux_eqs); + if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx) && !ctx->mcsat_supplement_active) { + if (context_assertions_need_mcsat_supplement(ctx, 1, &t)) { + code = context_enable_mcsat_supplement(ctx); + if (code < 0) { + return code; + } + } + } + code = setjmp(ctx->env); if (code == 0) { // we must call internalization start first @@ -6416,6 +6929,15 @@ int32_t context_process_formulas(context_t *ctx, uint32_t n, term_t *f) { ivector_reset(&ctx->aux_eqs); ivector_reset(&ctx->aux_atoms); + if (ctx->arch != CTX_ARCH_MCSAT && context_has_egraph(ctx)) { + if (context_assertions_need_mcsat_supplement(ctx, n, f)) { + code = context_enable_mcsat_supplement(ctx); + if (code < 0) { + return code; + } + } + } + code = setjmp(ctx->env); if (code == 0) { // flatten @@ -6717,4 +7239,10 @@ void context_gc_mark(context_t *ctx) { if (ctx->mcsat != NULL) { mcsat_gc_mark(ctx->mcsat); } + if (ctx->mcsat_supplement_active) { + mcsat_satellite_t *sat = context_mcsat_satellite(ctx); + if (sat != NULL) { + mcsat_satellite_gc_mark(sat); + } + } } diff --git a/src/context/context_simplifier.c b/src/context/context_simplifier.c index 836587e8b..824ca8706 100644 --- a/src/context/context_simplifier.c +++ b/src/context/context_simplifier.c @@ -1161,6 +1161,15 @@ static void try_substitution(context_t *ctx, term_t t1, term_t t2, term_t e) { assert(is_pos_term(t1) && is_pos_term(t2) && term_is_true(ctx, e)); + /* + * In supplementary-MCSAT mode, keep equalities explicit so they can be + * routed to the MCSAT satellite as tracked atoms/constraints. + */ + if (ctx->mcsat_supplement_active) { + ivector_push(&ctx->top_eqs, e); + return; + } + if (context_var_elim_enabled(ctx)) { intern = &ctx->intern; @@ -1200,6 +1209,14 @@ static void try_bool_substitution(context_t *ctx, term_t t1, term_t t2, term_t e assert(term_is_true(ctx, e)); + /* + * In supplementary-MCSAT mode, keep boolean equalities explicit. + */ + if (ctx->mcsat_supplement_active) { + ivector_push(&ctx->top_formulas, e); + return; + } + if (context_var_elim_enabled(ctx)) { intern = &ctx->intern; @@ -2245,8 +2262,14 @@ void flatten_assertion(context_t *ctx, term_t f) { break; case ARITH_ROOT_ATOM: - exception = FORMULA_NOT_LINEAR; - goto abort; + if (context_mcsat_supplement_active(ctx)) { + intern_tbl_map_root(intern, r, bool2code(tt)); + ivector_push(&ctx->top_atoms, signed_term(r, tt)); + } else { + exception = FORMULA_NOT_LINEAR; + goto abort; + } + break; case ARITH_IS_INT_ATOM: intern_tbl_map_root(intern, r, bool2code(tt)); @@ -2324,10 +2347,19 @@ void flatten_assertion(context_t *ctx, term_t f) { flatten_bit_select(ctx, r, tt); break; - case ARITH_FF_POLY: - case ARITH_FF_CONSTANT: case ARITH_FF_EQ_ATOM: case ARITH_FF_BINEQ_ATOM: + if (context_mcsat_supplement_active(ctx)) { + intern_tbl_map_root(intern, r, bool2code(tt)); + ivector_push(&ctx->top_atoms, signed_term(r, tt)); + } else { + exception = CONTEXT_UNSUPPORTED_THEORY; + goto abort; + } + break; + + case ARITH_FF_POLY: + case ARITH_FF_CONSTANT: exception = CONTEXT_UNSUPPORTED_THEORY; goto abort; } diff --git a/src/context/context_solver.c b/src/context/context_solver.c index beb420ff3..78d49ed69 100644 --- a/src/context/context_solver.c +++ b/src/context/context_solver.c @@ -35,6 +35,7 @@ #include "mcsat/solver.h" #include "solvers/bv/dimacs_printer.h" #include "solvers/cdcl/delegate.h" +#include "solvers/mcsat_satellite.h" #include "solvers/funs/fun_solver.h" #include "solvers/simplex/simplex.h" #include "terms/term_explorer.h" @@ -525,6 +526,10 @@ static void context_set_search_parameters(context_t *ctx, const param_t *params) egraph_set_max_interface_eqs(egraph, params->max_interface_eqs); } + if (ctx->mcsat_supplement_active && egraph != NULL && egraph->th[ETYPE_MCSAT] != NULL) { + mcsat_satellite_set_search_parameters((mcsat_satellite_t *) egraph->th[ETYPE_MCSAT], params); + } + /* * Set simplex parameters */ @@ -555,8 +560,22 @@ static void context_set_search_parameters(context_t *ctx, const param_t *params) } static smt_status_t _o_call_mcsat_solver(context_t *ctx, const param_t *params) { + smt_status_t stat; + mcsat_solve(ctx->mcsat, params, NULL, 0, NULL); - return mcsat_status(ctx->mcsat); + stat = mcsat_status(ctx->mcsat); + + /* + * For plain UNSAT results (without explicit model assumptions), keep the + * interpolant API usable by providing the canonical false interpolant. + */ + if (stat == YICES_STATUS_UNSAT && + context_supports_model_interpolation(ctx) && + mcsat_get_unsat_model_interpolant(ctx->mcsat) == NULL_TERM) { + mcsat_set_unsat_result(ctx->mcsat, false_term); + } + + return stat; } static smt_status_t call_mcsat_solver(context_t *ctx, const param_t *params) { @@ -571,6 +590,7 @@ static smt_status_t call_mcsat_solver(context_t *ctx, const param_t *params) { smt_status_t check_context(context_t *ctx, const param_t *params) { smt_core_t *core; smt_status_t stat; + mcsat_satellite_t *sat; if (params == NULL) { params = get_default_params(); @@ -589,6 +609,19 @@ smt_status_t check_context(context_t *ctx, const param_t *params) { stat = smt_status(core); } + sat = NULL; + if (ctx->mcsat_supplement_active && + ctx->egraph != NULL && + ctx->egraph->th[ETYPE_MCSAT] != NULL) { + sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; + } + if (stat == YICES_STATUS_UNSAT && + sat != NULL && + context_supports_model_interpolation(ctx) && + mcsat_satellite_get_unsat_model_interpolant(sat) == NULL_TERM) { + mcsat_satellite_set_unsat_model_interpolant(sat, false_term); + } + return stat; } @@ -600,6 +633,7 @@ smt_status_t check_context(context_t *ctx, const param_t *params) { smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *params, uint32_t n, const literal_t *a) { smt_core_t *core; smt_status_t stat; + mcsat_satellite_t *sat; assert(ctx->mcsat == NULL); @@ -615,6 +649,19 @@ smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *param stat = smt_status(core); } + sat = NULL; + if (ctx->mcsat_supplement_active && + ctx->egraph != NULL && + ctx->egraph->th[ETYPE_MCSAT] != NULL) { + sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; + } + if (stat == YICES_STATUS_UNSAT && + sat != NULL && + context_supports_model_interpolation(ctx) && + mcsat_satellite_get_unsat_model_interpolant(sat) == NULL_TERM) { + mcsat_satellite_set_unsat_model_interpolant(sat, false_term); + } + return stat; } @@ -813,6 +860,75 @@ static smt_status_t check_context_with_term_assumptions_mcsat(context_t *ctx, co MT_PROTECT(smt_status_t, __yices_globals.lock, _o_check_context_with_term_assumptions_mcsat(ctx, params, n, a, error)); } +/* + * Supplemental-MCSAT variant for term assumptions in CDCL(T) mode. + * We encode assumptions via fresh labels b_i with implications (b_i => a_i), + * then solve under assumptions b_i = true. + * + * Labels are kept in the context (no push/pop) so the regular context status + * and multicheck protocol remain unchanged. + */ +static smt_status_t _o_check_context_with_term_assumptions_supplement(context_t *ctx, const param_t *params, uint32_t n, const term_t *a, int32_t *error) { + smt_status_t stat; + ivector_t assumptions; + term_t interpolant; + uint32_t i; + literal_t l; + mcsat_satellite_t *sat; + + init_ivector(&assumptions, n); + + stat = YICES_STATUS_IDLE; + interpolant = NULL_TERM; + sat = NULL; + + if (ctx->mcsat_supplement_active && + ctx->egraph != NULL && + ctx->egraph->th[ETYPE_MCSAT] != NULL) { + sat = (mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]; + } + + for (i=0; imcsat == NULL) { - smt_status_t stat; - ivector_t assumptions; - uint32_t i; - literal_t l; - - init_ivector(&assumptions, n); - for (i=0; imcsat_supplement_active) { + return check_context_with_term_assumptions_supplement(ctx, params, n, a, error); + } else { + smt_status_t stat; + ivector_t assumptions; + uint32_t i; + literal_t l; + + init_ivector(&assumptions, n); + for (i=0; icore) == YICES_STATUS_SAT || smt_status(ctx->core) == YICES_STATUS_UNKNOWN || mcsat_status(ctx->mcsat) == YICES_STATUS_SAT); + assert(smt_status(ctx->core) == YICES_STATUS_SAT || + smt_status(ctx->core) == YICES_STATUS_UNKNOWN || + (context_has_mcsat(ctx) && mcsat_status(ctx->mcsat) == YICES_STATUS_SAT)); /* * First build assignments in the satellite solvers @@ -1352,6 +1474,14 @@ void build_model(model_t *model, context_t *ctx) { } } } + + /* + * Supplemental MCSAT values are an overlay: apply them after the regular + * CDCL(T) model is fully built so nonlinear/FF values are not overwritten. + */ + if (ctx->mcsat_supplement_active && context_has_egraph(ctx) && ctx->egraph->th[ETYPE_MCSAT] != NULL) { + mcsat_satellite_build_model((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT], model); + } } @@ -1482,6 +1612,19 @@ void context_build_unsat_core(context_t *ctx, ivector_t *v) { * MODEL INTERPOLANT */ term_t context_get_unsat_model_interpolant(context_t *ctx) { - assert(ctx->mcsat != NULL); - return mcsat_get_unsat_model_interpolant(ctx->mcsat); + if (ctx->mcsat != NULL) { + return mcsat_get_unsat_model_interpolant(ctx->mcsat); + } + + if (ctx->mcsat_supplement_active && ctx->egraph != NULL && ctx->egraph->th[ETYPE_MCSAT] != NULL) { + return mcsat_satellite_get_unsat_model_interpolant((mcsat_satellite_t *) ctx->egraph->th[ETYPE_MCSAT]); + } + + if (context_supports_model_interpolation(ctx) && + ctx->core != NULL && + smt_status(ctx->core) == YICES_STATUS_UNSAT) { + return false_term; + } + + return NULL_TERM; } diff --git a/src/context/context_types.h b/src/context/context_types.h index 9a7b39911..f7298ff94 100644 --- a/src/context/context_types.h +++ b/src/context/context_types.h @@ -736,6 +736,9 @@ struct context_s { // flag for enabling adding quant instances bool en_quant; + + // true when supplementary mcsat satellite is active in cdcl(t) mode + bool mcsat_supplement_active; }; @@ -796,7 +799,7 @@ enum { /* * NUM_INTERNALIZATION_ERRORS: must be (1 + number of negative codes) */ -#define NUM_INTERNALIZATION_ERRORS 24 +#define NUM_INTERNALIZATION_ERRORS 25 diff --git a/src/context/context_utils.h b/src/context/context_utils.h index 488a22fc7..e72bd9e2a 100644 --- a/src/context/context_utils.h +++ b/src/context/context_utils.h @@ -657,7 +657,11 @@ static inline bool context_has_quant_solver(context_t *ctx) { } static inline bool context_has_mcsat(context_t *ctx) { - return ctx->mcsat != NULL; + return ctx->arch == CTX_ARCH_MCSAT; +} + +static inline bool context_mcsat_supplement_active(context_t *ctx) { + return ctx->mcsat_supplement_active; } @@ -686,7 +690,7 @@ static inline bool context_supports_cleaninterrupt(context_t *ctx) { } static inline bool context_supports_model_interpolation(context_t* ctx) { - return (ctx->mcsat != NULL && ctx->mcsat_options.model_interpolation); + return (context_has_mcsat(ctx) && ctx->mcsat_options.model_interpolation); } /* @@ -706,4 +710,3 @@ static inline bool context_quant_enabled(context_t *ctx) { #endif /* __CONTEXT_UTILS_H */ - diff --git a/src/context/shared_terms.c b/src/context/shared_terms.c index b69b35545..069999ecf 100644 --- a/src/context/shared_terms.c +++ b/src/context/shared_terms.c @@ -135,6 +135,12 @@ static void sharing_map_visit_poly(sharing_map_t *map, polynomial_t *c, int32_t } } +static void sharing_map_visit_root_atom(sharing_map_t *map, root_atom_t *c, int32_t p) { + assert(c == root_atom_for_idx(map->terms, p)); + sharing_map_process_occurrence(map, index_of(c->x), p); + sharing_map_process_occurrence(map, index_of(c->p), p); +} + static void sharing_map_visit_bvpoly64(sharing_map_t *map, bvpoly64_t *c, int32_t p) { uint32_t i, n; @@ -176,6 +182,7 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { switch (kind_for_idx(map->terms, i)) { case CONSTANT_TERM: case ARITH_CONSTANT: + case ARITH_FF_CONSTANT: case BV64_CONSTANT: case BV_CONSTANT: case VARIABLE: @@ -189,10 +196,11 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { case ARITH_FLOOR: case ARITH_CEIL: case ARITH_ABS: + case ARITH_FF_EQ_ATOM: sharing_map_process_occurrence(map, index_of(integer_value_for_idx(map->terms, i)), i); break; case ARITH_ROOT_ATOM: - assert(false); + sharing_map_visit_root_atom(map, root_atom_for_idx(map->terms, i), i); break; case ITE_TERM: @@ -211,6 +219,7 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { case ARITH_IDIV: case ARITH_MOD: case ARITH_DIVIDES_ATOM: + case ARITH_FF_BINEQ_ATOM: case BV_ARRAY: case BV_DIV: case BV_REM: @@ -236,6 +245,7 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { break; case ARITH_POLY: + case ARITH_FF_POLY: sharing_map_visit_poly(map, polynomial_for_idx(map->terms, i), i); break; @@ -247,14 +257,6 @@ static void sharing_map_visit_subterms(sharing_map_t *map, int32_t i) { sharing_map_visit_bvpoly(map, bvpoly_for_idx(map->terms, i), i); break; - case ARITH_FF_CONSTANT: - case ARITH_FF_POLY: - case ARITH_FF_EQ_ATOM: - case ARITH_FF_BINEQ_ATOM: - // FF arithmetic is not supported in the non-mcsat solver yet - assert(false); - break; - case UNUSED_TERM: case RESERVED_TERM: assert(false); @@ -350,4 +352,3 @@ term_t unique_parent(sharing_map_t *map, term_t t) { return parent; } - diff --git a/src/frontend/common/parameters.c b/src/frontend/common/parameters.c index 318d0398e..b72774aa4 100644 --- a/src/frontend/common/parameters.c +++ b/src/frontend/common/parameters.c @@ -91,6 +91,7 @@ static const char * const param_names[NUM_PARAMETERS] = { "mcsat-partial-restart", "mcsat-rand-dec-freq", "mcsat-rand-dec-seed", + "mcsat-supplement-check", "mcsat-var-order", "optimistic-fcheck", "prop-threshold", @@ -167,6 +168,7 @@ static const yices_param_t param_code[NUM_PARAMETERS] = { PARAM_MCSAT_PARTIAL_RESTART, PARAM_MCSAT_RAND_DEC_FREQ, PARAM_MCSAT_RAND_DEC_SEED, + PARAM_MCSAT_SUPPLEMENT_CHECK, PARAM_MCSAT_VAR_ORDER, PARAM_OPTIMISTIC_FCHECK, PARAM_PROP_THRESHOLD, @@ -207,6 +209,21 @@ static const branch_t branching_code[NUM_BRANCHING_MODES] = { BRANCHING_THEORY, }; +/* + * Supplementary MCSAT check modes + */ +#define NUM_MCSAT_SUPPLEMENT_CHECK_MODES 2 + +static const char * const mcsat_supplement_check_modes[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + "both", + "final-only", +}; + +static const mcsat_supplement_check_t mcsat_supplement_check_code[NUM_MCSAT_SUPPLEMENT_CHECK_MODES] = { + MCSAT_SUPPLEMENT_CHECK_BOTH, + MCSAT_SUPPLEMENT_CHECK_FINAL_ONLY, +}; + /* @@ -454,6 +471,28 @@ bool param_val_to_branching(const char *name, const param_val_t *v, branch_t *va return false; } +/* + * Supplementary MCSAT check mode + * - allowed modes are "both" and "final-only" + */ +bool param_val_to_mcsat_supplement_check(const char *name, const param_val_t *v, + mcsat_supplement_check_t *value, char **reason) { + int32_t i; + + if (v->tag == PARAM_VAL_SYMBOL) { + i = binary_search_string(v->val.symbol, mcsat_supplement_check_modes, + NUM_MCSAT_SUPPLEMENT_CHECK_MODES); + if (i >= 0) { + assert(i < NUM_MCSAT_SUPPLEMENT_CHECK_MODES); + *value = mcsat_supplement_check_code[i]; + return true; + } + } + *reason = "must be one of 'both' 'final-only'"; + + return false; +} + /* diff --git a/src/frontend/common/parameters.h b/src/frontend/common/parameters.h index 97a11d19a..7e68c4936 100644 --- a/src/frontend/common/parameters.h +++ b/src/frontend/common/parameters.h @@ -125,6 +125,7 @@ typedef enum yices_param { PARAM_MCSAT_BV_VAR_SIZE, PARAM_MCSAT_VAR_ORDER, PARAM_MCSAT_PARTIAL_RESTART, + PARAM_MCSAT_SUPPLEMENT_CHECK, // error PARAM_UNKNOWN } yices_param_t; @@ -209,6 +210,12 @@ extern bool param_val_to_terms(const char *name, const param_val_t *v, ivector_t */ extern bool param_val_to_branching(const char *name, const param_val_t *v, branch_t *value, char **reason); +/* + * Supplementary MCSAT check mode + * - allowed modes are "both" and "final-only" + */ +extern bool param_val_to_mcsat_supplement_check(const char *name, const param_val_t *v, mcsat_supplement_check_t *value, char **reason); + /* * EF generalization mode * - allowed modes are 'none' 'substitution' 'projection' 'auto' diff --git a/src/frontend/smt2/smt2_commands.c b/src/frontend/smt2/smt2_commands.c index d8472510a..b07ceb8c6 100644 --- a/src/frontend/smt2/smt2_commands.c +++ b/src/frontend/smt2/smt2_commands.c @@ -634,6 +634,8 @@ static smt_status_t check_with_model(context_t *ctx, const param_t *params, uint model_t mdl; evaluator_t mdl_evaluator; + assert(ctx->mcsat != NULL); + // Init model and evaluation init_model(&mdl, ctx->terms, true); init_evaluator(&mdl_evaluator, &mdl); @@ -2250,6 +2252,23 @@ static void set_verbosity(smt2_globals_t *g, const char *name, aval_t value) { q_clear(&aux); } +/* + * Effective architecture for SMT2 logic: + * - defaults to arch_for_logic(logic) + * - if force_dpllt is enabled, replace MCSAT architecture with CDCL(T). + */ +static inline context_arch_t smt2_arch_for_logic(const smt2_globals_t *g, smt_logic_t logic) { + context_arch_t arch; + + assert(logic != SMT_UNKNOWN); + arch = (context_arch_t) arch_for_logic(logic); + if (g->force_dpllt && arch == CTX_ARCH_MCSAT) { + arch = CTX_ARCH_EGFUNSPLXBV; + } + + return arch; +} + /* * Options: produce-unsat-cores and produce-unsat-assumptions. @@ -2265,7 +2284,7 @@ static void set_unsat_core_option(smt2_globals_t *g, const char *name, aval_t va } else { g->produce_unsat_cores = flag; // Set model_interpolation if context is MCSAT or will use MCSAT architecture - if (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)) { + if (g->mcsat || (g->logic_code != SMT_UNKNOWN && smt2_arch_for_logic(g, g->logic_code) == CTX_ARCH_MCSAT)) { g->mcsat_options.model_interpolation = true; } report_success(); @@ -2284,7 +2303,7 @@ static void set_unsat_assumption_option(smt2_globals_t *g, const char *name, ava } else { g->produce_unsat_assumptions = flag; // Set model_interpolation if context is MCSAT or will use MCSAT architecture - if (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)) { + if (g->mcsat || (g->logic_code != SMT_UNKNOWN && smt2_arch_for_logic(g, g->logic_code) == CTX_ARCH_MCSAT)) { g->mcsat_options.model_interpolation = true; } report_success(); @@ -2581,7 +2600,7 @@ static void init_smt2_context(smt2_globals_t *g) { if (g->timeout > 0) { mode = CTX_MODE_INTERACTIVE; } - arch = arch_for_logic(logic); + arch = smt2_arch_for_logic(g, logic); iflag = iflag_for_logic(logic); qflag = qflag_for_logic(logic); @@ -4645,6 +4664,7 @@ static void init_smt2_globals(smt2_globals_t *g) { g->pushes_after_unsat = 0; g->logic_name = NULL; g->mcsat = false; + g->force_dpllt = false; init_ivector(&g->var_order, 0); init_mcsat_options(&g->mcsat_options); g->efmode = false; @@ -5042,7 +5062,8 @@ void smt2_get_unsat_assumptions(void) { /* Check whether MCSAT solver is going to be used. */ static bool mcsat_enabled(smt2_globals_t *g) { - return g->mcsat || arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT; + return !g->force_dpllt && + (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)); } /* @@ -5443,6 +5464,11 @@ static bool yices_get_option(smt2_globals_t *g, yices_param_t p) { print_int32_value(g->parameters.random_seed); break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + print_string_value(g->parameters.mcsat_supplement_check == MCSAT_SUPPLEMENT_CHECK_BOTH ? + "both" : "final-only"); + break; + case PARAM_MCSAT_VAR_ORDER: print_terms_value(g, &g->var_order); break; @@ -6241,6 +6267,12 @@ static void yices_set_option(smt2_globals_t *g, const char *param, const param_v } break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + if (param_val_to_mcsat_supplement_check(param, val, &g->parameters.mcsat_supplement_check, &reason)) { + // parameter is consumed during check-sat + } + break; + case PARAM_MCSAT_VAR_ORDER: if (param_val_to_terms(param, val, &terms, &reason)) { context = g->ctx; @@ -6462,7 +6494,7 @@ void smt2_set_logic(const char *name) { arch = ef_arch_for_logic(code); } else if (logic_is_supported(code)) { __smt2_globals.efmode = false; - arch = arch_for_logic(code); + arch = smt2_arch_for_logic(&__smt2_globals, code); } else { print_error("logic %s is not supported", name); return; @@ -6479,7 +6511,7 @@ void smt2_set_logic(const char *name) { } // if mcsat was requested, check whether the logic is supported by the MCSAT solver - if (__smt2_globals.mcsat && !logic_is_supported_by_mcsat(code)) { + if (__smt2_globals.mcsat && !__smt2_globals.force_dpllt && !logic_is_supported_by_mcsat(code)) { print_error("logic %s is not supported by the mcsat solver", name); return; } @@ -6492,7 +6524,7 @@ void smt2_set_logic(const char *name) { // in efmode : can't use the mcsat solver and must not be incremental if (__smt2_globals.efmode) { - if (__smt2_globals.mcsat) { + if (__smt2_globals.mcsat && !__smt2_globals.force_dpllt) { print_error("the mcsat solver does not support quantifiers"); return; } @@ -6507,8 +6539,8 @@ void smt2_set_logic(const char *name) { } // Set model_interpolation if unsat cores are enabled and architecture is MCSAT - if ((__smt2_globals.produce_unsat_cores || __smt2_globals.produce_unsat_assumptions) && - (arch == CTX_ARCH_MCSAT || __smt2_globals.mcsat)) { + if ((__smt2_globals.produce_unsat_cores || __smt2_globals.produce_unsat_assumptions) && + (arch == CTX_ARCH_MCSAT || (__smt2_globals.mcsat && !__smt2_globals.force_dpllt))) { __smt2_globals.mcsat_options.model_interpolation = true; } @@ -7272,5 +7304,14 @@ void smt2_add_pattern(int32_t op, term_t t, term_t *p, uint32_t n) { * Enables the mcsat solver. */ void smt2_enable_mcsat(void) { + assert(!__smt2_globals.force_dpllt); __smt2_globals.mcsat = true; } + +/* + * Force CDCL(T) architecture in SMT2 mode. + */ +void smt2_force_dpllt(void) { + assert(!__smt2_globals.mcsat); + __smt2_globals.force_dpllt = true; +} diff --git a/src/frontend/smt2/smt2_commands.h b/src/frontend/smt2/smt2_commands.h index 9fea4ee96..29fbe07d7 100644 --- a/src/frontend/smt2/smt2_commands.h +++ b/src/frontend/smt2/smt2_commands.h @@ -354,6 +354,7 @@ typedef struct smt2_globals_s { // mcsat bool mcsat; // set to true to use the mcsat solver + bool force_dpllt; // force cdcl(t) architecture mcsat_options_t mcsat_options; // options for the mcsat solver ivector_t var_order; // order in which mcsat needs to assign variables @@ -490,6 +491,12 @@ extern void init_mt2(bool benchmark, uint32_t timeout, uint32_t nthreads, bool p */ extern void smt2_enable_mcsat(void); +/* + * Force CDCL(T) architecture in SMT2 frontend + * - must not be called before init_smt2 + */ +extern void smt2_force_dpllt(void); + /* * Force verbosity level to k * - this has the same effect as (set-option :verbosity k) diff --git a/src/frontend/yices/yices_help.c b/src/frontend/yices/yices_help.c index 51bc606f8..305ac155a 100644 --- a/src/frontend/yices/yices_help.c +++ b/src/frontend/yices/yices_help.c @@ -1622,11 +1622,20 @@ static const help_record_t help_data[] = { "whose values matter for satisfying the assertions.\n", NULL, }, - // END MARKER: index 162 + // mcsat-supplement-check: index 163 + { HPARAM, + "(set-param mcsat-supplement-check [mode])", + "Control supplementary MCSAT checks in CDCL(T) mode", + "Allowed modes are:\n" + " both --> check in propagate and final-check\n" + " final-only --> check only in final-check.\n", + NULL, }, + + // END MARKER: index 164 { HMISC, NULL, NULL, NULL, NULL }, }; -#define END_HELP_DATA 163 +#define END_HELP_DATA 164 @@ -2087,6 +2096,7 @@ static const help_index_t help_index[] = { { "max-extensionality", NULL, 139, help_basic }, { "max-interface-eqs", NULL, 130, help_basic }, { "max-update-conflicts", NULL, 138, help_basic }, + { "mcsat-supplement-check", NULL, 163, help_basic }, { "mk-bv", NULL, 58, help_basic }, { "mk-tuple", NULL, 36, help_basic }, { "mod", NULL, 156, help_basic }, diff --git a/src/frontend/yices/yices_reval.c b/src/frontend/yices/yices_reval.c index 4212ad262..cb94a6378 100644 --- a/src/frontend/yices/yices_reval.c +++ b/src/frontend/yices/yices_reval.c @@ -1396,6 +1396,12 @@ static void show_param(yices_param_t p, uint32_t n) { show_pos32_param(param2string[p], parameters.max_extensionality, n); break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + show_string_param(param2string[p], + parameters.mcsat_supplement_check == MCSAT_SUPPLEMENT_CHECK_BOTH ? + "both" : "final-only", n); + break; + case PARAM_EF_FLATTEN_IFF: show_bool_param(param2string[p], ef_client_globals.ef_parameters.flatten_iff, n); break; @@ -1887,6 +1893,12 @@ static void yices_setparam_cmd(const char *param, const param_val_t *val) { } break; + case PARAM_MCSAT_SUPPLEMENT_CHECK: + if (param_val_to_mcsat_supplement_check(param, val, ¶meters.mcsat_supplement_check, &reason)) { + print_ok(); + } + break; + case PARAM_EF_FLATTEN_IFF: if (param_val_to_bool(param, val, &tt, &reason)) { ef_client_globals.ef_parameters.flatten_iff = tt; @@ -4114,4 +4126,3 @@ int yices_main(int argc, char *argv[]) { return exit_code; } - diff --git a/src/frontend/yices_smt2.c b/src/frontend/yices_smt2.c index ff964361b..681646bfe 100644 --- a/src/frontend/yices_smt2.c +++ b/src/frontend/yices_smt2.c @@ -108,6 +108,7 @@ static char *dimacsfile; // mcsat options static bool mcsat; +static bool force_dpllt; static double mcsat_rand_dec_freq; static int32_t mcsat_rand_dec_seed; static bool mcsat_na_mgcd; @@ -165,6 +166,7 @@ typedef enum optid { delegate_opt, // use an external sat solver dimacs_opt, // bitblast then export to DIMACS mcsat_opt, // enable mcsat + dpllt_opt, // force CDCL(T) mcsat_rand_dec_freq_opt, // random decision frequency when making a decision in mcsat mcsat_rand_dec_seed_opt, // seed for random decisions mcsat_na_mgcd_opt, // use the mgcd instead psc in projection @@ -217,6 +219,7 @@ static option_desc_t options[NUM_OPTIONS] = { { "delegate", '\0', MANDATORY_STRING, delegate_opt }, { "dimacs", '\0', MANDATORY_STRING, dimacs_opt }, { "mcsat", '\0', FLAG_OPTION, mcsat_opt }, + { "dpllt", '\0', FLAG_OPTION, dpllt_opt }, { "mcsat-rand-dec-freq", '\0', MANDATORY_FLOAT, mcsat_rand_dec_freq_opt }, { "mcsat-rand-dec-seed", '\0', MANDATORY_INT, mcsat_rand_dec_seed_opt }, { "mcsat-na-mgcd", '\0', FLAG_OPTION, mcsat_na_mgcd_opt }, @@ -284,7 +287,9 @@ static void print_help(const char *progname) { " --bvconst-in-decimal Display bit-vector constants as decimal numbers (default = false)\n" " --delegate= Use an external SAT solver (can be cadical, cryptominisat, kissat, or y2sat)\n" " --dimacs= Bitblast and export to a file (in DIMACS format)\n" - " --mcsat Use the MCSat solver\n" + " --mcsat Force MCSAT as top-level architecture\n" + " --dpllt Force CDCL(T) as top-level architecture\n" + " (mutually exclusive with --mcsat)\n" " --mcsat-help Show the MCSat options\n" " --ef-help Show the EF options\n" " --nthreads= Specify the number of threads (default = 0 = main thread only)\n" @@ -400,6 +405,7 @@ static void parse_command_line(int argc, char *argv[]) { dimacsfile = NULL; mcsat = false; + force_dpllt = false; mcsat_rand_dec_freq = -1; mcsat_rand_dec_seed = -1; mcsat_na_mgcd = false; @@ -560,6 +566,10 @@ static void parse_command_line(int argc, char *argv[]) { mcsat = true; break; + case dpllt_opt: + force_dpllt = true; + break; + case mcsat_rand_dec_freq_opt: if (! yices_has_mcsat()) goto no_mcsat; if (! validate_double_option(&parser, &elem, 0.0, false, 1.0, false)) goto bad_usage; @@ -724,6 +734,12 @@ static void parse_command_line(int argc, char *argv[]) { } done: + if (force_dpllt && mcsat) { + fprintf(stderr, "%s: options --dpllt and --mcsat are mutually exclusive\n", parser.command_name); + code = YICES_EXIT_USAGE; + goto exit; + } + if (incremental && delegate != NULL) { fprintf(stderr, "%s: delegate %s does not support incremental mode\n", parser.command_name, delegate); code = YICES_EXIT_USAGE; @@ -1153,6 +1169,7 @@ int main(int argc, char *argv[]) { yices_init(); init_mt2(!incremental, timeout, nthreads, interactive); + if (force_dpllt) smt2_force_dpllt(); if (smt2_model_format) smt2_force_smt2_model_format(); if (bvdecimal) smt2_force_bvdecimal_format(); if (dimacsfile != NULL && delegate == NULL) smt2_export_to_dimacs(dimacsfile); @@ -1220,4 +1237,3 @@ int main(int argc, char *argv[]) { return YICES_EXIT_SUCCESS; } - diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index df614679e..6e54a3b6b 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -3086,10 +3086,21 @@ void mcsat_build_model(mcsat_solver_t* mcsat, model_t* model) { mcsat_trace_printf(mcsat->ctx->trace, "\n"); } - // Add to model - model_map_term(model, x_term, x_value); - } - } + // Add to model + { + int_hmap_pair_t *entry = int_hmap_get(&model->map, x_term); + if (entry->val < 0) { + model_map_term(model, x_term, x_value); + } else { + /* + * Supplemental use may overlay values onto a model that already + * contains assignments from other CDCL(T) satellites. + */ + entry->val = x_value; + } + } + } + } // Let the plugins run add to the model (e.g. UF, division, ...) for (i = 0; i < mcsat->plugins_count; ++ i) { diff --git a/src/solvers/egraph/egraph.c b/src/solvers/egraph/egraph.c index e8b6a1b6c..c7be4ca5d 100644 --- a/src/solvers/egraph/egraph.c +++ b/src/solvers/egraph/egraph.c @@ -6107,6 +6107,18 @@ static fcheck_code_t baseline_final_check(egraph_t *egraph) { } } + if (egraph->ctrl[ETYPE_MCSAT] != NULL) { + // supplementary mcsat solver + c = egraph->ctrl[ETYPE_MCSAT]->final_check(egraph->th[ETYPE_MCSAT]); + if (c != FCHECK_SAT) { +#if TRACE_FCHECK + printf("---> exit at supplementary mcsat final check\n"); + fflush(stdout); +#endif + return c; + } + } + // i = number of interface equalities generated // max_eq = bound on number of interface equalities @@ -6218,6 +6230,17 @@ static fcheck_code_t experimental_final_check(egraph_t *egraph) { } } + if (egraph->ctrl[ETYPE_MCSAT] != NULL) { + c = egraph->ctrl[ETYPE_MCSAT]->final_check(egraph->th[ETYPE_MCSAT]); + if (c != FCHECK_SAT) { +#if TRACE_FCHECK + printf("---> exit at supplementary mcsat final check\n"); + fflush(stdout); +#endif + return c; + } + } + /* * Try egraph reconciliation @@ -6449,6 +6472,11 @@ bool egraph_assert_atom(egraph_t *egraph, void *atom, literal_t l) { case BV_ATM_TAG: resu = egraph->bv_smt->assert_atom(egraph->th[ETYPE_BV], untag_atom(atom), l); break; + + case MCSAT_ATM_TAG: + assert(egraph->mcsat_smt != NULL); + resu = egraph->mcsat_smt->assert_atom(egraph->th[ETYPE_MCSAT], untag_atom(atom), l); + break; } return resu; @@ -6711,6 +6739,11 @@ void egraph_expand_explanation(egraph_t *egraph, literal_t l, void *expl, ivecto case BV_ATM_TAG: egraph->bv_smt->expand_explanation(egraph->th[ETYPE_BV], l, expl, v); break; + + case MCSAT_ATM_TAG: + assert(egraph->mcsat_smt != NULL); + egraph->mcsat_smt->expand_explanation(egraph->th[ETYPE_MCSAT], l, expl, v); + break; } } @@ -6770,6 +6803,10 @@ static literal_t egraph_select_polarity(egraph_t *egraph, void *atom, literal_t case BV_ATM_TAG: return egraph->bv_smt->select_polarity(egraph->th[ETYPE_BV], untag_atom(atom), l); + case MCSAT_ATM_TAG: + assert(egraph->mcsat_smt != NULL); + return egraph->mcsat_smt->select_polarity(egraph->th[ETYPE_MCSAT], untag_atom(atom), l); + case EGRAPH_ATM_TAG: default: // FOR EQUALITY ATOMS: defer to the satellite solver if any @@ -6907,6 +6944,7 @@ void init_egraph(egraph_t *egraph, type_table_t *ttbl) { } egraph->arith_smt = NULL; egraph->bv_smt = NULL; + egraph->mcsat_smt = NULL; egraph->arith_eg = NULL; egraph->bv_eg = NULL; egraph->fun_eg = NULL; @@ -6958,6 +6996,36 @@ void egraph_attach_bvsolver(egraph_t *egraph, void *solver, th_ctrl_interface_t } +/* + * Attach supplementary mcsat solver + */ +void egraph_attach_mcsat_solver(egraph_t *egraph, void *solver, th_ctrl_interface_t *ctrl, + th_smt_interface_t *smt, th_egraph_interface_t *eg) { + etype_t id; + + assert(egraph->ctrl[ETYPE_MCSAT] == NULL && egraph->mcsat_smt == NULL); + + id = ETYPE_MCSAT; + egraph->th[id] = solver; + egraph->ctrl[id] = ctrl; + egraph->eg[id] = eg; + egraph->mcsat_smt = smt; +} + +/* + * Detach supplementary mcsat solver + */ +void egraph_detach_mcsat_solver(egraph_t *egraph) { + etype_t id; + + id = ETYPE_MCSAT; + egraph->th[id] = NULL; + egraph->ctrl[id] = NULL; + egraph->eg[id] = NULL; + egraph->mcsat_smt = NULL; +} + + /* * Attach a function subsolver * - solver = pointer to the subsolver object diff --git a/src/solvers/egraph/egraph.h b/src/solvers/egraph/egraph.h index 44566d963..ff14b9946 100644 --- a/src/solvers/egraph/egraph.h +++ b/src/solvers/egraph/egraph.h @@ -71,6 +71,22 @@ extern void egraph_attach_bvsolver(egraph_t *egraph, th_egraph_interface_t *eg, bv_egraph_interface_t *bv_eg); +/* + * Attach a supplementary MCSAT satellite + * - solver = pointer to the satellite object + * - ctrl, smt, eg = interface descriptors + */ +extern void egraph_attach_mcsat_solver(egraph_t *egraph, + void *solver, + th_ctrl_interface_t *ctrl, + th_smt_interface_t *smt, + th_egraph_interface_t *eg); + +/* + * Detach the supplementary MCSAT satellite + */ +extern void egraph_detach_mcsat_solver(egraph_t *egraph); + /* * Attach a function/array subsolver * - solver = pointer to the subsolver object diff --git a/src/solvers/egraph/egraph_base_types.h b/src/solvers/egraph/egraph_base_types.h index 4fb4b58c9..fec5b5470 100644 --- a/src/solvers/egraph/egraph_base_types.h +++ b/src/solvers/egraph/egraph_base_types.h @@ -422,16 +422,17 @@ typedef enum etype_s { ETYPE_BV, // 2 ETYPE_QUANT, // 3 ETYPE_FUNCTION, // 4 + ETYPE_MCSAT, // 5 // etypes internal to the egraph - ETYPE_BOOL, // 5 - ETYPE_TUPLE, // 6 - ETYPE_NONE, // 7 + ETYPE_BOOL, // 6 + ETYPE_TUPLE, // 7 + ETYPE_NONE, // 8 } etype_t; #define NUM_ETYPES (ETYPE_NONE + 1) -#define NUM_SATELLITES (ETYPE_FUNCTION + 1) +#define NUM_SATELLITES (ETYPE_MCSAT + 1) /* * tau is an arithmetic type if tau == 0 or 1 @@ -466,6 +467,7 @@ typedef enum atm_tag { EGRAPH_ATM_TAG = 0, ARITH_ATM_TAG = 1, BV_ATM_TAG = 2, + MCSAT_ATM_TAG = 3, } atm_tag_t; #define ATM_TAG_MASK ((size_t) 0x3) @@ -502,6 +504,11 @@ static inline void *tagged_bv_atom(void *atm) { return (void *)(((size_t) atm) | BV_ATM_TAG); } +static inline void *tagged_mcsat_atom(void *atm) { + assert((((size_t) atm) & ATM_TAG_MASK) == 0); + return (void *)(((size_t) atm) | MCSAT_ATM_TAG); +} + diff --git a/src/solvers/egraph/egraph_printer.c b/src/solvers/egraph/egraph_printer.c index a9ad7b531..e74fae8f1 100644 --- a/src/solvers/egraph/egraph_printer.c +++ b/src/solvers/egraph/egraph_printer.c @@ -48,11 +48,11 @@ static char **name = NULL; static const char * const etype2string[] = { - "int ", "real", "bv ", "quant ", "fun ", "bool", "tupl", "none", "", + "int ", "real", "bv ", "quant ", "fun ", "mcsat", "bool", "tupl", "none", "", }; static const char * const etype2theory[] = { - "arith", "arith", "bv", "quant", "fun", "bool", "tuple", "none", "", + "arith", "arith", "bv", "quant", "fun", "mcsat", "bool", "tuple", "none", "", }; static const char * const cmpkind2string[] = { @@ -904,4 +904,3 @@ void print_egraph_congruence_roots(FILE *f, egraph_t *egraph) { delete_pvector(&v); } - diff --git a/src/solvers/egraph/egraph_types.h b/src/solvers/egraph/egraph_types.h index 31b754c7a..4015b65a0 100644 --- a/src/solvers/egraph/egraph_types.h +++ b/src/solvers/egraph/egraph_types.h @@ -1466,6 +1466,7 @@ struct egraph_s { * Theory specific descriptors * - arith_smt: core interface for arith solver * - bv_smt: core interface for bitvector solver + * - mcsat_smt: core interface for supplementary mcsat solver * - arith_eg: egraph interface for arith solver * - bv_eg: egraph interface for the bitvector solver * - fun_eg: egraph interface for the array/function solver @@ -1477,6 +1478,7 @@ struct egraph_s { th_smt_interface_t *arith_smt; th_smt_interface_t *bv_smt; + th_smt_interface_t *mcsat_smt; arith_egraph_interface_t *arith_eg; bv_egraph_interface_t *bv_eg; diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c new file mode 100644 index 000000000..fae2a6af0 --- /dev/null +++ b/src/solvers/mcsat_satellite.c @@ -0,0 +1,1132 @@ +/* + * This file is part of the Yices SMT Solver. + * Copyright (C) 2017 SRI International. + * + * Yices is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Yices is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Yices. If not, see . + */ + +#include +#include "context/context.h" +#include "model/models.h" +#include "solvers/egraph/composites.h" +#include "solvers/egraph/egraph.h" +#include "solvers/mcsat_satellite.h" +#include "terms/term_explorer.h" +#include "terms/term_manager.h" +#include "terms/term_substitution.h" +#include "utils/int_hash_sets.h" +#include "utils/memalloc.h" +#include "utils/pair_hash_map2.h" + + +typedef struct mcsat_atom_object_s { + uint32_t id; +} mcsat_atom_object_t; + +typedef struct mcsat_atom_entry_s { + term_t atom; + literal_t lit; + term_t pos_label; + term_t neg_label; + mcsat_atom_object_t *obj; + bool active; +} mcsat_atom_entry_t; + +typedef struct mcsat_eq_entry_s { + term_t label; + literal_t source_lit; +} mcsat_eq_entry_t; + +struct mcsat_satellite_s { + context_t *ctx; + smt_core_t *core; + egraph_t *egraph; + + context_t mctx; + term_manager_t tm; + + param_t params; + bool check_in_propagate; + + int32_t internal_error; + + bool cache_valid; + uint64_t cache_signature; + + mcsat_atom_entry_t *atoms; + uint32_t num_atoms; + uint32_t atom_size; + uint32_t push_depth; + ivector_t atom_push_mark; + + int_hmap_t arith_var_to_term; + + mcsat_eq_entry_t *eq; + uint32_t num_eq; + uint32_t eq_size; + uint32_t dlevel; + pmap2_t eq_active; + ivector_t eq_level_mark; + + ivector_t assumptions; + ivector_t assumption_lits; + int_hmap_t label_to_lit; + ivector_t conflict; +}; + + +/* + * Atom/generic vector growth. + */ +static void mcsat_satellite_extend_atoms(mcsat_satellite_t *sat) { + uint32_t n; + assert(sat->num_atoms == sat->atom_size); + n = sat->atom_size + 1; + n += n >> 1; + sat->atoms = (mcsat_atom_entry_t *) safe_realloc(sat->atoms, n * sizeof(mcsat_atom_entry_t)); + sat->atom_size = n; +} + +static void mcsat_satellite_extend_eq(mcsat_satellite_t *sat) { + uint32_t n; + assert(sat->num_eq == sat->eq_size); + n = sat->eq_size + 1; + n += n >> 1; + sat->eq = (mcsat_eq_entry_t *) safe_realloc(sat->eq, n * sizeof(mcsat_eq_entry_t)); + sat->eq_size = n; +} + +/* + * Hash helper for assignment signatures. + */ +static inline uint64_t sig_mix(uint64_t h, uint32_t x) { + h ^= x; + h *= UINT64_C(1099511628211); + return h; +} + +static uint64_t mcsat_satellite_signature(const mcsat_satellite_t *sat) { + uint64_t h; + uint32_t i, n; + + h = UINT64_C(1469598103934665603); + n = sat->assumptions.size; + for (i = 0; i < n; i++) { + h = sig_mix(h, (uint32_t) sat->assumptions.data[i]); + } + return sig_mix(h, n); +} + +/* + * Ensure mctx is ready for assertion. + */ +static void mcsat_satellite_prepare_assertion_state(mcsat_satellite_t *sat) { + smt_status_t status; + status = mcsat_status(sat->mctx.mcsat); + if (status != YICES_STATUS_IDLE) { + mcsat_clear(sat->mctx.mcsat); + } +} + +/* + * Assert a formula in the internal MCSAT context. + */ +static int32_t mcsat_satellite_assert_formula(mcsat_satellite_t *sat, term_t f) { + int32_t code; + + mcsat_satellite_prepare_assertion_state(sat); + code = mcsat_assert_formulas(sat->mctx.mcsat, 1, &f); + if (code < 0) { + sat->internal_error = code; + } + return code; +} + +/* + * Track one assumption. + */ +static inline void mcsat_satellite_add_assumption(mcsat_satellite_t *sat, term_t label, literal_t lit) { + int_hmap_pair_t *p; + + ivector_push(&sat->assumptions, label); + ivector_push(&sat->assumption_lits, lit); + if (lit != null_literal) { + p = int_hmap_get(&sat->label_to_lit, label); + p->val = lit; + } +} + +/* + * Build assumption lists from current assignment + active eq/diseq labels. + */ +static void mcsat_satellite_build_assumptions(mcsat_satellite_t *sat, bool complete_with_phase) { + bval_t v; + uint32_t i; + + ivector_reset(&sat->assumptions); + ivector_reset(&sat->assumption_lits); + int_hmap_reset(&sat->label_to_lit); + + for (i = 0; i < sat->num_atoms; i++) { + if (!sat->atoms[i].active) { + continue; + } + + v = literal_value(sat->core, sat->atoms[i].lit); + if (v == VAL_TRUE || (complete_with_phase && v == VAL_UNDEF_TRUE)) { + mcsat_satellite_add_assumption(sat, sat->atoms[i].pos_label, sat->atoms[i].lit); + } else if (v == VAL_FALSE || (complete_with_phase && v == VAL_UNDEF_FALSE)) { + mcsat_satellite_add_assumption(sat, sat->atoms[i].neg_label, not(sat->atoms[i].lit)); + } + } + + for (i = 0; i < sat->num_eq; i++) { + mcsat_satellite_add_assumption(sat, sat->eq[i].label, sat->eq[i].source_lit); + } + +} + +/* + * Explore a term and collect all Boolean atoms in atoms. + */ +static void collect_boolean_atoms(mcsat_satellite_t *sat, term_t t, int_hset_t *atoms, int_hset_t *visited) { + term_table_t *terms; + uint32_t i, nchildren; + + if (t < 0) { + t = not(t); + } + if (int_hset_member(visited, t)) { + return; + } + int_hset_add(visited, t); + + terms = sat->mctx.terms; + if (term_type(terms, t) == bool_type(terms->types)) { + int_hset_add(atoms, t); + } + + if (term_is_projection(terms, t)) { + collect_boolean_atoms(sat, proj_term_arg(terms, t), atoms, visited); + + } else if (term_is_sum(terms, t)) { + nchildren = term_num_children(terms, t); + for (i=0; iconflict); + init_int_hset(&labels, 0); + init_int_hset(&visited, 0); + init_int_hset(&seen_lits, 0); + + interpolant = mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); + if (interpolant != NULL_TERM) { + collect_boolean_atoms(sat, interpolant, &labels, &visited); + p = int_hmap_first_record(&sat->label_to_lit); + while (p != NULL) { + if (int_hset_member(&labels, p->key) && p->val != null_literal && + !int_hset_member(&seen_lits, p->val)) { + int_hset_add(&seen_lits, p->val); + ivector_push(&sat->conflict, not(p->val)); + } + p = int_hmap_next_record(&sat->label_to_lit, p); + } + } + + if (sat->conflict.size == 0) { + for (i = 0; i < sat->assumption_lits.size; i++) { + l = sat->assumption_lits.data[i]; + if (l != null_literal && !int_hset_member(&seen_lits, l)) { + int_hset_add(&seen_lits, l); + ivector_push(&sat->conflict, not(l)); + } + } + } + + ivector_push(&sat->conflict, null_literal); + record_theory_conflict(sat->core, sat->conflict.data); + + delete_int_hset(&seen_lits); + delete_int_hset(&visited); + delete_int_hset(&labels); +} + +/* + * Run one consistency check in the internal MCSAT context. + */ +static smt_status_t mcsat_satellite_check(mcsat_satellite_t *sat, bool force, bool emit_conflict) { + model_t mdl; + smt_status_t status; + uint64_t sig; + uint32_t i; + value_t vtrue; + + if (sat->internal_error < 0) { + if (emit_conflict) { + literal_t c[1]; + c[0] = null_literal; + record_theory_conflict(sat->core, c); + } + return YICES_STATUS_UNSAT; + } + + mcsat_satellite_build_assumptions(sat, false); + sig = mcsat_satellite_signature(sat); + if (!force && sat->cache_valid && sat->cache_signature == sig) { + return YICES_STATUS_SAT; + } + + init_model(&mdl, sat->mctx.terms, true); + vtrue = vtbl_mk_bool(&mdl.vtbl, true); + for (i=0; iassumptions.size; i++) { + if (model_find_term_value(&mdl, sat->assumptions.data[i]) == null_value) { + model_map_term(&mdl, sat->assumptions.data[i], vtrue); + } + } + + mcsat_clear(sat->mctx.mcsat); + mcsat_solve(sat->mctx.mcsat, &sat->params, &mdl, sat->assumptions.size, (const term_t *) sat->assumptions.data); + status = mcsat_status(sat->mctx.mcsat); + + delete_model(&mdl); + + sat->cache_valid = false; + if (status == YICES_STATUS_SAT) { + sat->cache_valid = true; + sat->cache_signature = sig; + } else if (status == YICES_STATUS_UNSAT && emit_conflict) { + mcsat_satellite_record_conflict(sat); + } + + return status; +} + +/* + * Open one decision level in the eq/diseq activation map. + */ +static void mcsat_satellite_open_level(mcsat_satellite_t *sat) { + pmap2_push(&sat->eq_active); + sat->dlevel ++; + if (sat->eq_level_mark.size <= sat->dlevel) { + ivector_push(&sat->eq_level_mark, sat->num_eq); + } else { + sat->eq_level_mark.data[sat->dlevel] = sat->num_eq; + } + sat->cache_valid = false; +} + +/* + * Backtrack eq/diseq activation to target. + */ +static void mcsat_satellite_backtrack_to(mcsat_satellite_t *sat, uint32_t target) { + while (sat->dlevel > target) { + sat->num_eq = sat->eq_level_mark.data[sat->dlevel]; + pmap2_pop(&sat->eq_active); + sat->dlevel --; + } + sat->cache_valid = false; +} + +/* + * Align the internal MCSAT scope stack with the outer context base level. + * This is needed when the satellite is attached after one or more pushes. + */ +static void mcsat_satellite_sync_base_level(mcsat_satellite_t *sat, uint32_t base_level) { + uint32_t i; + + for (i = 0; i < base_level; i++) { + context_push(&sat->mctx); + ivector_push(&sat->atom_push_mark, sat->num_atoms); + sat->push_depth ++; + mcsat_satellite_open_level(sat); + } +} + +/* + * Derive a source literal from a disequality hint if possible. + */ +static literal_t source_lit_from_hint(mcsat_satellite_t *sat, composite_t *hint) { + literal_t l; + + if (hint == NULL || sat->egraph == NULL) { + return null_literal; + } + + l = egraph_occ2literal(sat->egraph, pos_occ(hint->id)); + if (l == null_literal || l == false_literal) { + return null_literal; + } + + if (composite_kind(hint) == COMPOSITE_EQ) { + return not(l); + } + + return l; +} + +/* + * Add one eq/diseq notification as a labeled internal assumption. + */ +static void mcsat_satellite_add_eq_notification(mcsat_satellite_t *sat, term_t t1, term_t t2, bool eq, literal_t src) { + int32_t k0, k1; + pmap2_rec_t *r; + term_t atom; + term_t label; + term_t implication; + + if (t1 > t2) { + term_t aux = t1; + t1 = t2; + t2 = aux; + } + + k0 = eq ? (int32_t) t1 : -((int32_t) t1) - 1; + k1 = (int32_t) t2; + + r = pmap2_get(&sat->eq_active, k0, k1); + if (r->val >= 0) { + return; + } + + if (sat->num_eq == sat->eq_size) { + mcsat_satellite_extend_eq(sat); + } + + label = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); + atom = eq ? mk_eq(&sat->tm, t1, t2) : mk_neq(&sat->tm, t1, t2); + implication = mk_implies(&sat->tm, label, atom); + if (mcsat_satellite_assert_formula(sat, implication) < 0) { + return; + } + + sat->eq[sat->num_eq].label = label; + sat->eq[sat->num_eq].source_lit = src; + sat->num_eq ++; + + r->val = 1; + sat->cache_valid = false; +} + +/* + * Control-interface callbacks. + */ +static void mcsat_satellite_start_internalization(void *solver) { + mcsat_satellite_t *sat = solver; + sat->cache_valid = false; +} + +static void mcsat_satellite_start_search(void *solver) { + mcsat_satellite_t *sat = solver; + sat->cache_valid = false; + if (mcsat_status(sat->mctx.mcsat) != YICES_STATUS_IDLE) { + mcsat_clear(sat->mctx.mcsat); + } +} + +static bool mcsat_satellite_propagate(void *solver) { + mcsat_satellite_t *sat = solver; + smt_status_t status; + + if (!sat->check_in_propagate) { + return true; + } + + status = mcsat_satellite_check(sat, false, true); + return status != YICES_STATUS_UNSAT; +} + +static fcheck_code_t mcsat_satellite_final_check(void *solver) { + mcsat_satellite_t *sat = solver; + smt_status_t status; + + status = mcsat_satellite_check(sat, false, true); + switch (status) { + case YICES_STATUS_UNSAT: + return FCHECK_CONTINUE; + case YICES_STATUS_UNKNOWN: + return FCHECK_UNKNOWN; + default: + return FCHECK_SAT; + } +} + +static void mcsat_satellite_increase_decision_level(void *solver) { + mcsat_satellite_open_level(solver); +} + +static void mcsat_satellite_backtrack(void *solver, uint32_t back_level) { + mcsat_satellite_backtrack_to(solver, back_level); +} + +static void mcsat_satellite_push(void *solver) { + mcsat_satellite_t *sat = solver; + context_push(&sat->mctx); + ivector_push(&sat->atom_push_mark, sat->num_atoms); + sat->push_depth ++; + mcsat_satellite_open_level(sat); +} + +static void mcsat_satellite_pop(void *solver) { + mcsat_satellite_t *sat = solver; + uint32_t i; + int32_t mark; + + assert(sat->push_depth > 0); + assert(sat->atom_push_mark.size > 0); + + context_pop(&sat->mctx); + assert(sat->dlevel > 0); + + mark = ivector_pop2(&sat->atom_push_mark); + for (i=mark; inum_atoms; i++) { + sat->atoms[i].active = false; + } + sat->push_depth --; + mcsat_satellite_backtrack_to(sat, sat->dlevel - 1); +} + +static void mcsat_satellite_reset(void *solver) { + mcsat_satellite_t *sat = solver; + uint32_t i; + + reset_context(&sat->mctx); + + for (i=0; inum_atoms; i++) { + if (sat->atoms[i].obj != NULL) { + safe_free(sat->atoms[i].obj); + sat->atoms[i].obj = NULL; + } + } + + sat->num_atoms = 0; + sat->num_eq = 0; + sat->push_depth = 0; + sat->dlevel = 0; + sat->cache_valid = false; + sat->internal_error = 0; + + ivector_reset(&sat->atom_push_mark); + reset_pmap2(&sat->eq_active); + ivector_reset(&sat->eq_level_mark); + ivector_push(&sat->eq_level_mark, 0); + + int_hmap_reset(&sat->arith_var_to_term); + int_hmap_reset(&sat->label_to_lit); + ivector_reset(&sat->assumptions); + ivector_reset(&sat->assumption_lits); + ivector_reset(&sat->conflict); +} + +static void mcsat_satellite_clear(void *solver) { + mcsat_satellite_t *sat = solver; + context_clear(&sat->mctx); + sat->cache_valid = false; +} + +/* + * SMT interface callbacks. + */ +static bool mcsat_satellite_assert_atom(void *solver, void *atom, literal_t l) { + (void) solver; + (void) atom; + (void) l; + return true; +} + +static void mcsat_satellite_expand_explanation(void *solver, literal_t l, void *expl, ivector_t *v) { + (void) solver; + (void) l; + (void) expl; + (void) v; +} + +static literal_t mcsat_satellite_select_polarity(void *solver, void *atom, literal_t l) { + (void) solver; + (void) atom; + return l; +} + +/* + * Egraph interface callbacks. + */ +static void mcsat_satellite_assert_equality(void *solver, thvar_t x1, thvar_t x2, int32_t id) { + mcsat_satellite_t *sat = solver; + int_hmap_pair_t *p1, *p2; + (void) id; + + p1 = int_hmap_find(&sat->arith_var_to_term, x1); + p2 = int_hmap_find(&sat->arith_var_to_term, x2); + if (p1 != NULL && p2 != NULL) { + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, true, null_literal); + } +} + +static void mcsat_satellite_assert_disequality(void *solver, thvar_t x1, thvar_t x2, composite_t *hint) { + mcsat_satellite_t *sat = solver; + int_hmap_pair_t *p1, *p2; + literal_t src; + + p1 = int_hmap_find(&sat->arith_var_to_term, x1); + p2 = int_hmap_find(&sat->arith_var_to_term, x2); + if (p1 != NULL && p2 != NULL) { + src = source_lit_from_hint(sat, hint); + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, false, src); + } +} + +static bool mcsat_satellite_assert_distinct(void *solver, uint32_t n, thvar_t *a, composite_t *hint) { + mcsat_satellite_t *sat = solver; + int_hmap_pair_t *p1, *p2; + literal_t src; + uint32_t i, j; + + src = source_lit_from_hint(sat, hint); + for (i=0; iarith_var_to_term, a[i]); + if (p1 == NULL) continue; + for (j=i+1; jarith_var_to_term, a[j]); + if (p2 != NULL) { + mcsat_satellite_add_eq_notification(sat, p1->val, p2->val, false, src); + } + } + } + return true; +} + +static bool mcsat_satellite_check_diseq(void *solver, thvar_t x1, thvar_t x2) { + (void) solver; + (void) x1; + (void) x2; + return false; +} + +static bool mcsat_satellite_is_constant(void *solver, thvar_t x) { + (void) solver; + (void) x; + return false; +} + +static void mcsat_satellite_expand_th_expl(void *solver, thvar_t x1, thvar_t x2, void *expl, th_explanation_t *result) { + (void) solver; + (void) x1; + (void) x2; + (void) expl; + (void) result; +} + +static uint32_t mcsat_satellite_reconcile_model(void *solver, uint32_t max_eq) { + (void) solver; + (void) max_eq; + return 0; +} + +static void mcsat_satellite_prepare_model(void *solver) { + (void) solver; +} + +static bool mcsat_satellite_equal_in_model(void *solver, thvar_t x1, thvar_t x2) { + (void) solver; + (void) x1; + (void) x2; + return false; +} + +static void mcsat_satellite_gen_interface_lemma(void *solver, literal_t l, thvar_t x1, thvar_t x2, bool equiv) { + (void) solver; + (void) l; + (void) x1; + (void) x2; + (void) equiv; +} + +static void mcsat_satellite_release_model(void *solver) { + (void) solver; +} + +static ipart_t *mcsat_satellite_build_partition(void *solver) { + (void) solver; + return NULL; +} + +static void mcsat_satellite_release_partition(void *solver, ipart_t *partition) { + (void) solver; + (void) partition; +} + +static void mcsat_satellite_attach_eterm(void *solver, thvar_t x, eterm_t t) { + (void) solver; + (void) x; + (void) t; +} + +static eterm_t mcsat_satellite_eterm_of_var(void *solver, thvar_t x) { + (void) solver; + (void) x; + return null_eterm; +} + +static literal_t mcsat_satellite_select_eq_polarity(void *solver, thvar_t x, thvar_t y, literal_t l) { + (void) solver; + (void) x; + (void) y; + return l; +} + +/* + * Static interface records. + */ +static th_ctrl_interface_t mcsat_satellite_ctrl = { + (start_intern_fun_t) mcsat_satellite_start_internalization, + (start_fun_t) mcsat_satellite_start_search, + (propagate_fun_t) mcsat_satellite_propagate, + (final_check_fun_t) mcsat_satellite_final_check, + (increase_level_fun_t) mcsat_satellite_increase_decision_level, + (backtrack_fun_t) mcsat_satellite_backtrack, + (push_fun_t) mcsat_satellite_push, + (pop_fun_t) mcsat_satellite_pop, + (reset_fun_t) mcsat_satellite_reset, + (clear_fun_t) mcsat_satellite_clear, +}; + +static th_smt_interface_t mcsat_satellite_smt = { + (assert_fun_t) mcsat_satellite_assert_atom, + (expand_expl_fun_t) mcsat_satellite_expand_explanation, + (select_pol_fun_t) mcsat_satellite_select_polarity, + NULL, + NULL, +}; + +static th_egraph_interface_t mcsat_satellite_eg = { + (assert_eq_fun_t) mcsat_satellite_assert_equality, + (assert_diseq_fun_t) mcsat_satellite_assert_disequality, + (assert_distinct_fun_t) mcsat_satellite_assert_distinct, + (check_diseq_fun_t) mcsat_satellite_check_diseq, + (is_constant_fun_t) mcsat_satellite_is_constant, + (expand_eq_exp_fun_t) mcsat_satellite_expand_th_expl, + (reconcile_model_fun_t) mcsat_satellite_reconcile_model, + (prepare_model_fun_t) mcsat_satellite_prepare_model, + (equal_in_model_fun_t) mcsat_satellite_equal_in_model, + (gen_inter_lemma_fun_t) mcsat_satellite_gen_interface_lemma, + (release_model_fun_t) mcsat_satellite_release_model, + (build_partition_fun_t) mcsat_satellite_build_partition, + (free_partition_fun_t) mcsat_satellite_release_partition, + (attach_to_var_fun_t) mcsat_satellite_attach_eterm, + (get_eterm_fun_t) mcsat_satellite_eterm_of_var, + (select_eq_polarity_fun_t) mcsat_satellite_select_eq_polarity, +}; + + +/* + * Constructor/destructor. + */ +mcsat_satellite_t *new_mcsat_satellite(context_t *ctx) { + mcsat_satellite_t *sat; + + sat = (mcsat_satellite_t *) safe_malloc(sizeof(mcsat_satellite_t)); + + sat->ctx = ctx; + sat->core = ctx->core; + sat->egraph = ctx->egraph; + + init_context(&sat->mctx, ctx->terms, ctx->logic, CTX_MODE_PUSHPOP, CTX_ARCH_MCSAT, false); + sat->mctx.mcsat_options = ctx->mcsat_options; + sat->mctx.mcsat_options.model_interpolation = true; + ivector_copy(&sat->mctx.mcsat_var_order, ctx->mcsat_var_order.data, ctx->mcsat_var_order.size); + ivector_copy(&sat->mctx.mcsat_initial_var_order, ctx->mcsat_initial_var_order.data, ctx->mcsat_initial_var_order.size); + + init_term_manager(&sat->tm, sat->mctx.terms); + + init_params_to_defaults(&sat->params); + sat->check_in_propagate = true; + + sat->internal_error = 0; + + sat->cache_valid = false; + sat->cache_signature = 0; + + sat->atoms = NULL; + sat->num_atoms = 0; + sat->atom_size = 0; + sat->push_depth = 0; + init_ivector(&sat->atom_push_mark, 0); + + init_int_hmap(&sat->arith_var_to_term, 0); + + sat->eq = NULL; + sat->num_eq = 0; + sat->eq_size = 0; + sat->dlevel = 0; + init_pmap2(&sat->eq_active); + init_ivector(&sat->eq_level_mark, 8); + ivector_push(&sat->eq_level_mark, 0); + + init_ivector(&sat->assumptions, 0); + init_ivector(&sat->assumption_lits, 0); + init_int_hmap(&sat->label_to_lit, 0); + init_ivector(&sat->conflict, 0); + + if (ctx->trace != NULL) { + mcsat_satellite_set_trace(sat, ctx->trace); + } + + mcsat_satellite_sync_base_level(sat, ctx->base_level); + + return sat; +} + +void delete_mcsat_satellite(mcsat_satellite_t *sat) { + uint32_t i; + + if (sat == NULL) { + return; + } + + for (i = 0; i < sat->num_atoms; i++) { + if (sat->atoms[i].obj != NULL) { + safe_free(sat->atoms[i].obj); + sat->atoms[i].obj = NULL; + } + } + safe_free(sat->atoms); + sat->atoms = NULL; + + safe_free(sat->eq); + sat->eq = NULL; + + delete_ivector(&sat->conflict); + delete_int_hmap(&sat->label_to_lit); + delete_ivector(&sat->assumption_lits); + delete_ivector(&sat->assumptions); + + delete_ivector(&sat->eq_level_mark); + delete_pmap2(&sat->eq_active); + + delete_int_hmap(&sat->arith_var_to_term); + delete_ivector(&sat->atom_push_mark); + + delete_term_manager(&sat->tm); + delete_context(&sat->mctx); + safe_free(sat); +} + + +/* + * Public interface getters. + */ +th_ctrl_interface_t *mcsat_satellite_ctrl_interface(mcsat_satellite_t *sat) { + (void) sat; + return &mcsat_satellite_ctrl; +} + +th_smt_interface_t *mcsat_satellite_smt_interface(mcsat_satellite_t *sat) { + (void) sat; + return &mcsat_satellite_smt; +} + +th_egraph_interface_t *mcsat_satellite_egraph_interface(mcsat_satellite_t *sat) { + (void) sat; + return &mcsat_satellite_eg; +} + +int32_t mcsat_satellite_assert_formulas(mcsat_satellite_t *sat, uint32_t n, const term_t *a) { + uint32_t i; + int32_t code; + + for (i = 0; i < n; i++) { + code = mcsat_satellite_assert_formula(sat, a[i]); + if (code < 0) { + return code; + } + } + + return CTX_NO_ERROR; +} + +/* + * Register one tracked unsupported atom. + */ +int32_t mcsat_satellite_register_atom(mcsat_satellite_t *sat, term_t atom, literal_t l, void **obj) { + mcsat_atom_entry_t *entry; + term_t plabel, nlabel; + term_t implication; + int32_t code; + mcsat_atom_object_t *atom_obj; + uint32_t i; + + assert(l >= 0); + + // Already tracked: keep the existing object/literal association. + for (i = 0; i < sat->num_atoms; i++) { + entry = sat->atoms + i; + if (entry->atom == atom && entry->lit == l) { + if (obj != NULL) { + *obj = entry->obj; + } + return CTX_NO_ERROR; + } + } + + if (sat->num_atoms == sat->atom_size) { + mcsat_satellite_extend_atoms(sat); + } + + plabel = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); + nlabel = mk_uterm(&sat->tm, bool_type(sat->mctx.types)); + + implication = mk_implies(&sat->tm, plabel, atom); + code = mcsat_satellite_assert_formula(sat, implication); + if (code < 0) { + return code; + } + + implication = mk_implies(&sat->tm, nlabel, not(atom)); + code = mcsat_satellite_assert_formula(sat, implication); + if (code < 0) { + return code; + } + + atom_obj = NULL; + if (obj != NULL) { + atom_obj = safe_malloc(sizeof(mcsat_atom_object_t)); + atom_obj->id = sat->num_atoms; + *obj = atom_obj; + } + + entry = sat->atoms + sat->num_atoms; + entry->atom = atom; + entry->lit = l; + entry->pos_label = plabel; + entry->neg_label = nlabel; + entry->obj = atom_obj; + entry->active = true; + sat->num_atoms ++; + + sat->cache_valid = false; + return CTX_NO_ERROR; +} + +/* + * Register thvar -> term for arithmetic terms. + */ +void mcsat_satellite_register_arith_term(mcsat_satellite_t *sat, thvar_t x, term_t t) { + int_hmap_pair_t *p; + p = int_hmap_get(&sat->arith_var_to_term, x); + p->val = t; +} + +/* + * Parameters/tracing/model/GC support. + */ +void mcsat_satellite_set_search_parameters(mcsat_satellite_t *sat, const param_t *params) { + sat->params = *params; + sat->check_in_propagate = (params->mcsat_supplement_check == MCSAT_SUPPLEMENT_CHECK_BOTH); + sat->cache_valid = false; +} + +void mcsat_satellite_set_trace(mcsat_satellite_t *sat, tracer_t *trace) { + mcsat_set_tracer(sat->mctx.mcsat, trace); +} + +term_t mcsat_satellite_get_unsat_model_interpolant(mcsat_satellite_t *sat) { + return mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); +} + +void mcsat_satellite_set_unsat_model_interpolant(mcsat_satellite_t *sat, term_t t) { + mcsat_set_unsat_result(sat->mctx.mcsat, t); +} + +term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, const param_t *params, uint32_t n, const term_t *a) { + ivector_t labels; + ivector_t assumptions; + term_manager_t tm; + model_t mdl; + value_t vtrue; + term_t result; + smt_status_t status; + uint32_t i; + bool pushed; + + if (sat->internal_error < 0) { + return NULL_TERM; + } + + init_ivector(&labels, n); + init_ivector(&assumptions, n); + init_term_manager(&tm, sat->mctx.terms); + init_model(&mdl, sat->mctx.terms, true); + + pushed = false; + result = NULL_TERM; + + if (context_supports_pushpop(&sat->mctx)) { + context_push(&sat->mctx); + pushed = true; + } + + vtrue = vtbl_mk_bool(&mdl.vtbl, true); + + for (i = 0; i < n; i++) { + term_t b, implication; + int32_t code; + + b = new_uninterpreted_term(sat->mctx.terms, bool_id); + implication = mk_implies(&tm, b, a[i]); + code = mcsat_satellite_assert_formula(sat, implication); + if (code < 0) { + goto done; + } + + ivector_push(&labels, b); + ivector_push(&assumptions, b); + model_map_term(&mdl, b, vtrue); + } + + mcsat_clear(sat->mctx.mcsat); + mcsat_solve(sat->mctx.mcsat, params != NULL ? params : &sat->params, &mdl, + assumptions.size, (const term_t *) assumptions.data); + status = mcsat_status(sat->mctx.mcsat); + + if (status == YICES_STATUS_UNSAT) { + term_t raw = mcsat_get_unsat_model_interpolant(sat->mctx.mcsat); + if (raw == NULL_TERM) { + raw = false_term; + } + if (labels.size > 0) { + term_subst_t subst; + init_term_subst(&subst, &tm, labels.size, labels.data, a); + result = apply_term_subst(&subst, raw); + delete_term_subst(&subst); + } else { + result = raw; + } + } + +done: + delete_model(&mdl); + delete_term_manager(&tm); + delete_ivector(&assumptions); + delete_ivector(&labels); + + if (pushed) { + mcsat_cleanup_assumptions(sat->mctx.mcsat); + context_pop(&sat->mctx); + } + + if (result != NULL_TERM) { + mcsat_set_unsat_result(sat->mctx.mcsat, result); + } + + return result; +} + +void mcsat_satellite_build_model(mcsat_satellite_t *sat, model_t *model) { + model_t mdl; + smt_status_t status; + uint32_t i; + value_t vtrue; + + if (sat->internal_error < 0) { + return; + } + + /* + * For model construction, complete unassigned tracked literals with their + * current polarity hint so MCSAT can compute a concrete witness model. + */ + mcsat_satellite_build_assumptions(sat, true); + + init_model(&mdl, sat->mctx.terms, true); + vtrue = vtbl_mk_bool(&mdl.vtbl, true); + for (i = 0; i < sat->assumptions.size; i++) { + if (model_find_term_value(&mdl, sat->assumptions.data[i]) == null_value) { + model_map_term(&mdl, sat->assumptions.data[i], vtrue); + } + } + + mcsat_clear(sat->mctx.mcsat); + mcsat_solve(sat->mctx.mcsat, &sat->params, &mdl, sat->assumptions.size, (const term_t *) sat->assumptions.data); + status = mcsat_status(sat->mctx.mcsat); + + delete_model(&mdl); + + if (status == YICES_STATUS_SAT) { + mcsat_build_model(sat->mctx.mcsat, model); + } +} + +void mcsat_satellite_gc_mark(mcsat_satellite_t *sat) { + uint32_t i; + + for (i=0; inum_atoms; i++) { + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->atoms[i].atom)); + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->atoms[i].pos_label)); + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->atoms[i].neg_label)); + } + + for (i=0; inum_eq; i++) { + term_table_set_gc_mark(sat->mctx.terms, index_of(sat->eq[i].label)); + } + + mcsat_gc_mark(sat->mctx.mcsat); +} diff --git a/src/solvers/mcsat_satellite.h b/src/solvers/mcsat_satellite.h new file mode 100644 index 000000000..172f1d3cd --- /dev/null +++ b/src/solvers/mcsat_satellite.h @@ -0,0 +1,85 @@ +/* + * This file is part of the Yices SMT Solver. + * Copyright (C) 2017 SRI International. + * + * Yices is free software: you can redistribute it and/or modify + * it under the terms of the GNU General Public License as published by + * the Free Software Foundation, either version 3 of the License, or + * (at your option) any later version. + * + * Yices is distributed in the hope that it will be useful, + * but WITHOUT ANY WARRANTY; without even the implied warranty of + * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the + * GNU General Public License for more details. + * + * You should have received a copy of the GNU General Public License + * along with Yices. If not, see . + */ + +#ifndef __MCSAT_SATELLITE_H +#define __MCSAT_SATELLITE_H + +#include +#include + +#include "context/context_types.h" +#include "solvers/egraph/egraph_types.h" + +typedef struct mcsat_satellite_s mcsat_satellite_t; + +extern mcsat_satellite_t *new_mcsat_satellite(context_t *ctx); +extern void delete_mcsat_satellite(mcsat_satellite_t *sat); + +extern th_ctrl_interface_t *mcsat_satellite_ctrl_interface(mcsat_satellite_t *sat); +extern th_smt_interface_t *mcsat_satellite_smt_interface(mcsat_satellite_t *sat); +extern th_egraph_interface_t *mcsat_satellite_egraph_interface(mcsat_satellite_t *sat); + +extern int32_t mcsat_satellite_assert_formulas(mcsat_satellite_t *sat, uint32_t n, const term_t *a); + +/* + * Register a Boolean atom term tracked by the supplementary MCSAT satellite. + * - atom must be a Boolean term. + * - l must be a positive core literal. + * - *obj is set to a satellite-owned atom object for egraph tagging/dispatch. + * Return code: + * - CTX_NO_ERROR on success + * - a negative internalization code on error. + */ +/* + * Register one tracked atom/literal pair. + * - if obj is non-NULL, create an opaque atom object for egraph tagging. + * - if obj is NULL, register as observation-only (no egraph atom tag). + */ +extern int32_t mcsat_satellite_register_atom(mcsat_satellite_t *sat, term_t atom, literal_t l, void **obj); + +/* + * Record a mapping from an arithmetic theory variable to the source term. + * This is used to materialize eq/diseq notifications into MCSAT assumptions. + */ +extern void mcsat_satellite_register_arith_term(mcsat_satellite_t *sat, thvar_t x, term_t t); + +/* + * Copy search parameters relevant to supplementary checking. + */ +extern void mcsat_satellite_set_search_parameters(mcsat_satellite_t *sat, const param_t *params); + +/* + * Return the most recent UNSAT model interpolant from the satellite solver. + * Returns NULL_TERM if unavailable. + */ +extern term_t mcsat_satellite_get_unsat_model_interpolant(mcsat_satellite_t *sat); +extern void mcsat_satellite_set_unsat_model_interpolant(mcsat_satellite_t *sat, term_t t); +extern term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, const param_t *params, uint32_t n, const term_t *a); + +/* + * Overlay model values from the supplementary MCSAT context. + */ +extern void mcsat_satellite_build_model(mcsat_satellite_t *sat, model_t *model); + +/* + * Trace + GC support. + */ +extern void mcsat_satellite_set_trace(mcsat_satellite_t *sat, tracer_t *trace); +extern void mcsat_satellite_gc_mark(mcsat_satellite_t *sat); + +#endif /* __MCSAT_SATELLITE_H */ diff --git a/src/terms/term_explorer.c b/src/terms/term_explorer.c index b2d93487c..63f3191d1 100644 --- a/src/terms/term_explorer.c +++ b/src/terms/term_explorer.c @@ -449,6 +449,15 @@ term_t term_child(term_table_t *table, term_t t, uint32_t i) { } break; + case ARITH_FF_EQ_ATOM: + assert(i < 2); + if (i == 0) { + result = arith_ff_eq_arg(table, t); + } else { + result = ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t))); + } + break; + case ARITH_IS_INT_ATOM: case ARITH_FLOOR: case ARITH_CEIL: @@ -500,6 +509,12 @@ void get_term_children(term_table_t *table, term_t t, ivector_t *v) { ivector_push(v, zero_term); break; + case ARITH_FF_EQ_ATOM: + // t == 0 over finite fields: expose both sides uniformly + ivector_push(v, arith_ff_eq_arg(table, t)); + ivector_push(v, ff_zero_term(table, term_type(table, arith_ff_eq_arg(table, t)))); + break; + case ARITH_IS_INT_ATOM: case ARITH_FLOOR: case ARITH_CEIL: @@ -684,4 +699,3 @@ int32_t generic_const_value(term_table_t *table, term_t t) { assert(is_pos_term(t) && t != true_term); return constant_term_index(table, t); } - diff --git a/tests/regress/both/README.md b/tests/regress/both/README.md new file mode 100644 index 000000000..bd3f87b36 --- /dev/null +++ b/tests/regress/both/README.md @@ -0,0 +1,16 @@ +# Shared Regression Tests (`regress/both`) + +Tests in this directory are expected to pass in both solver modes: + +- `--mcsat` +- `--dpllt` + +The regression harness runs each SMT2 test in this directory twice, once per +mode. Do not put `--mcsat` or `--dpllt` in `.options` files here; the harness +injects these flags automatically. + +Keep MCSAT-only tests (for example, `check-sat-assuming-model` and +`get-unsat-model-interpolant`) in `tests/regress/mcsat`. + +Keep core-shape-sensitive tests where outputs differ across solvers outside this +directory. diff --git a/tests/regress/both/smoke_sat.smt2 b/tests/regress/both/smoke_sat.smt2 new file mode 100644 index 000000000..85d6f47e7 --- /dev/null +++ b/tests/regress/both/smoke_sat.smt2 @@ -0,0 +1,4 @@ +(set-logic QF_LIA) +(declare-const x Int) +(assert (> x 0)) +(check-sat) diff --git a/tests/regress/both/smoke_sat.smt2.gold b/tests/regress/both/smoke_sat.smt2.gold new file mode 100644 index 000000000..6b8a2c3d2 --- /dev/null +++ b/tests/regress/both/smoke_sat.smt2.gold @@ -0,0 +1 @@ +sat diff --git a/tests/regress/both/smoke_unsat.smt2 b/tests/regress/both/smoke_unsat.smt2 new file mode 100644 index 000000000..725d76139 --- /dev/null +++ b/tests/regress/both/smoke_unsat.smt2 @@ -0,0 +1,5 @@ +(set-logic QF_LIA) +(declare-const x Int) +(assert (> x 0)) +(assert (< x 0)) +(check-sat) diff --git a/tests/regress/both/smoke_unsat.smt2.gold b/tests/regress/both/smoke_unsat.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/both/smoke_unsat.smt2.gold @@ -0,0 +1 @@ +unsat diff --git a/tests/regress/check.sh b/tests/regress/check.sh index b5d9e471a..67d93edfd 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -117,7 +117,7 @@ fi ./"$bin_dir"/yices_smt2 --mcsat >& /dev/null < /dev/null if [ $? -ne 0 ] then - MCSAT_FILTER="-v mcsat" + MCSAT_FILTER="-v -E /(mcsat|both)/" else MCSAT_FILTER="." fi diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index 2ddbcefc7..655430188 100755 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -110,6 +110,8 @@ fi # outfile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; } timefile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; } +outfile2= +timefile2= if [[ -z "$TIME_LIMIT" ]]; then @@ -160,38 +162,120 @@ if [ -d "$out_dir" ] ; then log_file="$out_dir/_$(echo "${test_file//_/__}" | tr '/' '_')" fi -# Run the binary -( - ulimit -S -t $TIME_LIMIT &> /dev/null - ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null - (time "./$bin_dir/$binary" $options "./$test_file" >& "$outfile" ) >& "$timefile" -) -status=$? -runtime=$(cat "$timefile") +run_solver_once() { + local run_options=$1 + local run_outfile=$2 + local run_timefile=$3 -# Do the diff -DIFF=$(diff -w "$outfile" "$gold") + ( + ulimit -S -t $TIME_LIMIT &> /dev/null + ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null + (time "./$bin_dir/$binary" $run_options "./$test_file" >& "$run_outfile") >& "$run_timefile" + ) +} -if [ $? -eq 0 ] && [ $status -eq 0 ] -then - echo -e "$green PASS [${runtime} s] $black $test_string" +strip_solver_mode_flags() { + local input=$1 + local output= + local tok + + for tok in $input; do + case "$tok" in + --mcsat|--dpllt) + ;; + *) + output="$output $tok" + ;; + esac + done + + echo "$output" +} + +if [ "$binary" = yices_smt2 ] && [[ "$test_file" == *"/both/"* ]]; then + options=$(strip_solver_mode_flags "$options") + test_string="$test_file [ $options --mcsat ] [ $options --dpllt ]" + + outfile2=$($mktemp_cmd) || { echo "Can't create temp file" ; rm -f "$timefile" "$outfile" ; exit 3 ; } + timefile2=$($mktemp_cmd) || { echo "Can't create temp file" ; rm -f "$timefile" "$outfile" "$outfile2" ; exit 3 ; } + + run_solver_once "$options --mcsat" "$outfile" "$timefile" + status_mcsat=$? + runtime_mcsat=$(cat "$timefile") + diff_mcsat=$(diff -w "$outfile" "$gold") + diff_status_mcsat=$? + + run_solver_once "$options --dpllt" "$outfile2" "$timefile2" + status_dpllt=$? + runtime_dpllt=$(cat "$timefile2") + diff_dpllt=$(diff -w "$outfile2" "$gold") + diff_status_dpllt=$? + + if [ $status_mcsat -eq 0 ] && [ $diff_status_mcsat -eq 0 ] && [ $status_dpllt -eq 0 ] && [ $diff_status_dpllt -eq 0 ]; then + echo -e "$green PASS [mcsat ${runtime_mcsat} s, dpllt ${runtime_dpllt} s] $black $test_string" if [ -n "$log_file" ] ; then - log_file="$log_file.pass" - echo "$test_string" > "$log_file" - echo "$runtime" >> "$log_file" + log_file="$log_file.pass" + echo "$test_string" > "$log_file" + echo "mcsat: $runtime_mcsat" >> "$log_file" + echo "dpllt: $runtime_dpllt" >> "$log_file" fi code=0 -else + else + DIFF= + if [ $status_mcsat -ne 0 ] || [ $diff_status_mcsat -ne 0 ]; then + DIFF+="--- mcsat (--mcsat) ---"$'\n' + if [ $status_mcsat -ne 0 ]; then + DIFF+="exit status: $status_mcsat"$'\n' + fi + DIFF+="$diff_mcsat"$'\n' + fi + if [ $status_dpllt -ne 0 ] || [ $diff_status_dpllt -ne 0 ]; then + DIFF+="--- dpllt (--dpllt) ---"$'\n' + if [ $status_dpllt -ne 0 ]; then + DIFF+="exit status: $status_dpllt"$'\n' + fi + DIFF+="$diff_dpllt"$'\n' + fi + echo -e "$red FAIL $black $test_string" if [ -n "$log_file" ] ; then - log_file="$log_file.error" - echo "$test_string" > "$log_file" - echo "$runtime" >> "$log_file" - echo "$DIFF" >> "$log_file" + log_file="$log_file.error" + echo "$test_string" > "$log_file" + echo "mcsat: $runtime_mcsat" >> "$log_file" + echo "dpllt: $runtime_dpllt" >> "$log_file" + echo "$DIFF" >> "$log_file" fi code=1 + fi +else + # Run the binary once + run_solver_once "$options" "$outfile" "$timefile" + status=$? + runtime=$(cat "$timefile") + + # Do the diff + DIFF=$(diff -w "$outfile" "$gold") + + if [ $? -eq 0 ] && [ $status -eq 0 ] + then + echo -e "$green PASS [${runtime} s] $black $test_string" + if [ -n "$log_file" ] ; then + log_file="$log_file.pass" + echo "$test_string" > "$log_file" + echo "$runtime" >> "$log_file" + fi + code=0 + else + echo -e "$red FAIL $black $test_string" + if [ -n "$log_file" ] ; then + log_file="$log_file.error" + echo "$test_string" > "$log_file" + echo "$runtime" >> "$log_file" + echo "$DIFF" >> "$log_file" + fi + code=1 + fi fi -rm "$timefile" -rm "$outfile" +rm -f "$timefile" "$outfile" "$timefile2" "$outfile2" exit $code From b268ef575dc84511755a1d61b274fc0a90c7e7a8 Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 9 Mar 2026 21:24:21 -0700 Subject: [PATCH 2/3] Fix supplemental trigger to preserve div-by-zero errors --- src/context/context.c | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/context/context.c b/src/context/context.c index 17339ea70..b626d50f5 100644 --- a/src/context/context.c +++ b/src/context/context.c @@ -98,10 +98,7 @@ static inline mcsat_satellite_t *context_mcsat_satellite(context_t *ctx) { static inline bool divisor_requires_mcsat(term_table_t *terms, term_t t) { t = unsigned_term(t); - if (term_kind(terms, t) != ARITH_CONSTANT) { - return true; - } - return q_is_zero(rational_term_desc(terms, t)); + return term_kind(terms, t) != ARITH_CONSTANT; } /* From ccde68223bf6e8c968e12493e6c7bb1000e174ad Mon Sep 17 00:00:00 2001 From: Stephane Graham-Lengrand Date: Mon, 9 Mar 2026 22:41:53 -0700 Subject: [PATCH 3/3] Add broad CDCL(T)+supplementary-MCSAT API coverage --- src/solvers/mcsat_satellite.c | 8 + tests/api/test_cdclt_mcsat_supplement.c | 383 ++++++++++++++++++++++++ 2 files changed, 391 insertions(+) create mode 100644 tests/api/test_cdclt_mcsat_supplement.c diff --git a/src/solvers/mcsat_satellite.c b/src/solvers/mcsat_satellite.c index fae2a6af0..84a478502 100644 --- a/src/solvers/mcsat_satellite.c +++ b/src/solvers/mcsat_satellite.c @@ -1019,6 +1019,14 @@ term_t mcsat_satellite_compute_unsat_model_interpolant(mcsat_satellite_t *sat, c pushed = false; result = NULL_TERM; + /* + * Internal push requires an idle MCSAT state in debug builds. + * This path may be called after a previous UNSAT check. + */ + if (mcsat_status(sat->mctx.mcsat) != YICES_STATUS_IDLE) { + mcsat_clear(sat->mctx.mcsat); + } + if (context_supports_pushpop(&sat->mctx)) { context_push(&sat->mctx); pushed = true; diff --git a/tests/api/test_cdclt_mcsat_supplement.c b/tests/api/test_cdclt_mcsat_supplement.c new file mode 100644 index 000000000..22f1f49b4 --- /dev/null +++ b/tests/api/test_cdclt_mcsat_supplement.c @@ -0,0 +1,383 @@ +/* + * API coverage for CDCL(T) with supplementary MCSAT. + * + * This test intentionally forces top-level solver-type=dpllt and exercises: + * - nonlinear arithmetic handled via supplementary MCSAT + * - finite-field constraints handled via supplementary MCSAT + * - assumptions + unsat-core extraction on unsupported atoms + * - push/pop lifecycle on supplemental formulas + * - supplementary check-mode parameter (both/final-only) + * - division-by-zero behavior remains a front-end error path + */ + +#ifdef NDEBUG +#undef NDEBUG +#endif + +#include +#include +#include +#include +#include +#include + +#include + +static void fail(const char *msg) { + fprintf(stderr, "FAIL: %s\n", msg); + yices_print_error(stderr); + exit(2); +} + +static void check(bool cond, const char *msg) { + if (!cond) { + fail(msg); + } +} + +static void check_code(int32_t code, const char *msg) { + if (code < 0) { + fail(msg); + } +} + +static void check_status(smt_status_t actual, smt_status_t expected, const char *msg) { + if (actual != expected) { + fail(msg); + } +} + +static bool has_term(const term_vector_t *v, term_t t) { + uint32_t i; + + for (i = 0; i < v->size; i++) { + if (v->data[i] == t) { + return true; + } + } + return false; +} + +static context_t *make_cdclt_context(const char *logic_name) { + ctx_config_t *cfg; + context_t *ctx; + int32_t code; + + cfg = yices_new_config(); + if (cfg == NULL) { + fail("yices_new_config failed"); + } + + if (logic_name != NULL) { + code = yices_default_config_for_logic(cfg, logic_name); + if (code < 0) { + yices_free_config(cfg); + fail("yices_default_config_for_logic failed"); + } + } + + code = yices_set_config(cfg, "solver-type", "dpllt"); + if (code < 0) { + yices_free_config(cfg); + fail("setting solver-type=dpllt failed"); + } + + code = yices_set_config(cfg, "mode", "push-pop"); + if (code < 0) { + yices_free_config(cfg); + fail("setting mode=push-pop failed"); + } + + ctx = yices_new_context(cfg); + yices_free_config(cfg); + if (ctx == NULL) { + fail("yices_new_context failed"); + } + + return ctx; +} + +static term_t ff_const_si(long val, long mod) { + mpz_t zval, zmod; + term_t t; + + mpz_init_set_si(zval, val); + mpz_init_set_si(zmod, mod); + t = yices_ff_const(zval, zmod); + mpz_clear(zmod); + mpz_clear(zval); + return t; +} + +static void test_nla_sat_unsat_and_model(void) { + context_t *ctx; + term_t x, xx, eq4, eq2, eq3; + smt_status_t stat; + model_t *mdl; + int64_t v; + + ctx = make_cdclt_context("QF_UFLIA"); + + x = yices_new_uninterpreted_term(yices_int_type()); + xx = yices_mul(x, x); + eq4 = yices_arith_eq_atom(xx, yices_int32(4)); + check(eq4 != NULL_TERM, "building nonlinear equation failed"); + + check_code(yices_assert_formula(ctx, eq4), "assert x*x=4 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT for x*x=4"); + + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "yices_get_model failed on SAT nonlinear context"); + check(yices_formula_true_in_model(mdl, eq4) == 1, "model must satisfy x*x=4"); + check_code(yices_get_int64_value(mdl, xx, &v), "reading value of x*x failed"); + check(v == 4, "expected model value x*x = 4"); + yices_free_model(mdl); + + yices_reset_context(ctx); + eq2 = yices_arith_eq_atom(xx, yices_int32(2)); + eq3 = yices_arith_eq_atom(xx, yices_int32(3)); + check_code(yices_assert_formula(ctx, eq2), "assert x*x=2 failed"); + check_code(yices_assert_formula(ctx, eq3), "assert x*x=3 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for x*x=2 and x*x=3"); + + yices_free_context(ctx); +} + +static void test_nla_hidden_product_and_push_pop(void) { + context_t *ctx; + term_t x, y, xy, ge5, xle1, yle1, xge0, yge0, eq2, eq1, xeq1; + smt_status_t stat; + + ctx = make_cdclt_context("QF_UFLIA"); + x = yices_new_uninterpreted_term(yices_int_type()); + y = yices_new_uninterpreted_term(yices_int_type()); + xy = yices_mul(x, y); + + ge5 = yices_arith_geq_atom(xy, yices_int32(5)); + xle1 = yices_arith_leq_atom(x, yices_int32(1)); + yle1 = yices_arith_leq_atom(y, yices_int32(1)); + xge0 = yices_arith_geq_atom(x, yices_int32(0)); + yge0 = yices_arith_geq_atom(y, yices_int32(0)); + + check_code(yices_assert_formula(ctx, ge5), "assert x*y>=5 failed"); + check_code(yices_assert_formula(ctx, xle1), "assert x<=1 failed"); + check_code(yices_assert_formula(ctx, yle1), "assert y<=1 failed"); + check_code(yices_assert_formula(ctx, xge0), "assert x>=0 failed"); + check_code(yices_assert_formula(ctx, yge0), "assert y>=0 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for hidden-product constraints"); + + yices_reset_context(ctx); + + check_code(yices_push(ctx), "push failed"); + eq2 = yices_arith_eq_atom(yices_mul(x, x), yices_int32(2)); + check_code(yices_assert_formula(ctx, eq2), "assert x*x=2 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for integer x*x=2"); + check_code(yices_pop(ctx), "pop failed"); + + check_code(yices_push(ctx), "second push failed"); + eq1 = yices_arith_eq_atom(yices_mul(x, x), yices_int32(1)); + xeq1 = yices_arith_eq_atom(x, yices_int32(1)); + check_code(yices_assert_formula(ctx, eq1), "assert x*x=1 failed"); + check_code(yices_assert_formula(ctx, xeq1), "assert x=1 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT for x*x=1 and x=1"); + check_code(yices_pop(ctx), "second pop failed"); + + yices_free_context(ctx); +} + +static void test_nonconstant_divisor_and_param_modes(void) { + context_t *ctx; + param_t *params; + term_t x, y; + term_t yeq2, xeq6, div_eq3, div_eq4; + smt_status_t stat; + model_t *mdl; + + ctx = make_cdclt_context("QF_UFLRA"); + x = yices_new_uninterpreted_term(yices_real_type()); + y = yices_new_uninterpreted_term(yices_real_type()); + + yeq2 = yices_arith_eq_atom(y, yices_rational32(2, 1)); + xeq6 = yices_arith_eq_atom(x, yices_rational32(6, 1)); + div_eq3 = yices_arith_eq_atom(yices_division(x, y), yices_rational32(3, 1)); + div_eq4 = yices_arith_eq_atom(yices_division(x, y), yices_rational32(4, 1)); + + params = yices_new_param_record(); + check(params != NULL, "yices_new_param_record failed"); + yices_default_params_for_context(ctx, params); + + check_code(yices_set_param(params, "mcsat-supplement-check", "final-only"), + "set_param(final-only) failed"); + check_code(yices_assert_formula(ctx, yeq2), "assert y=2 failed"); + check_code(yices_assert_formula(ctx, xeq6), "assert x=6 failed"); + check_code(yices_assert_formula(ctx, div_eq3), "assert x/y=3 failed"); + stat = yices_check_context(ctx, params); + check_status(stat, YICES_STATUS_SAT, "expected SAT for x=6,y=2,x/y=3"); + + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "get_model failed for nonconstant-divisor SAT"); + check(yices_formula_true_in_model(mdl, div_eq3) == 1, "model must satisfy x/y=3"); + yices_free_model(mdl); + + yices_reset_context(ctx); + + check_code(yices_set_param(params, "mcsat-supplement-check", "both"), + "set_param(both) failed"); + check_code(yices_assert_formula(ctx, yeq2), "reassert y=2 failed"); + check_code(yices_assert_formula(ctx, xeq6), "reassert x=6 failed"); + check_code(yices_assert_formula(ctx, div_eq4), "assert x/y=4 failed"); + stat = yices_check_context(ctx, params); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for x=6,y=2,x/y=4"); + + yices_free_param_record(params); + yices_free_context(ctx); +} + +static void test_ff_sat_unsat_model_and_assumption_core(void) { + context_t *ctx; + mpz_t p, val, mod, tmp; + type_t tau; + term_t a, c1, c3, sat_eq, ff_eq, ff_neq; + term_t pa, qa, imp1, imp2; + term_t assumptions[2]; + term_vector_t core; + smt_status_t stat; + model_t *mdl; + + mpz_init_set_si(p, 7); + mpz_init(val); + mpz_init(mod); + mpz_init(tmp); + + ctx = make_cdclt_context(NULL); + tau = yices_ff_type(p); + check(tau != NULL_TYPE, "creating FF type failed"); + a = yices_new_uninterpreted_term(tau); + check(a != NULL_TERM, "creating FF variable failed"); + + c1 = ff_const_si(1, 7); + c3 = ff_const_si(3, 7); + sat_eq = yices_ff_eq_atom(yices_ff_add(a, c1), c3); + check(sat_eq != NULL_TERM, "building FF SAT constraint failed"); + + check_code(yices_assert_formula(ctx, sat_eq), "assert FF SAT constraint failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_SAT, "expected SAT for a+1=3 in F7"); + + mdl = yices_get_model(ctx, 1); + check(mdl != NULL, "get_model failed for FF SAT"); + check_code(yices_get_ff_value(mdl, a, val, mod), "get_ff_value failed"); + check(mpz_cmp_si(mod, 7) == 0, "expected FF modulus 7"); + mpz_mod(tmp, val, mod); + check(mpz_cmp_si(tmp, 2) == 0, "expected a = 2 mod 7"); + check(yices_formula_true_in_model(mdl, sat_eq) == 1, "model must satisfy a+1=3"); + yices_free_model(mdl); + + yices_reset_context(ctx); + + ff_eq = yices_ff_eq_atom(a, c1); + ff_neq = yices_ff_neq_atom(a, c1); + check_code(yices_assert_formula(ctx, ff_eq), "assert a=1 failed"); + check_code(yices_assert_formula(ctx, ff_neq), "assert a!=1 failed"); + stat = yices_check_context(ctx, NULL); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT for a=1 and a!=1"); + + yices_reset_context(ctx); + + pa = yices_new_uninterpreted_term(yices_bool_type()); + qa = yices_new_uninterpreted_term(yices_bool_type()); + imp1 = yices_implies(pa, yices_ff_eq_atom(a, c1)); + imp2 = yices_implies(qa, yices_ff_neq_atom(a, c1)); + check_code(yices_assert_formula(ctx, imp1), "assert implication pa=>a=1 failed"); + check_code(yices_assert_formula(ctx, imp2), "assert implication qa=>a!=1 failed"); + + assumptions[0] = pa; + assumptions[1] = qa; + stat = yices_check_context_with_assumptions(ctx, NULL, 2, assumptions); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT with FF assumptions pa,qa"); + + yices_init_term_vector(&core); + check_code(yices_get_unsat_core(ctx, &core), "yices_get_unsat_core failed for FF assumptions"); + check(core.size == 2, "expected two assumptions in FF unsat core"); + check(has_term(&core, pa) && has_term(&core, qa), "FF unsat core missing assumptions"); + yices_delete_term_vector(&core); + + yices_free_context(ctx); + mpz_clear(tmp); + mpz_clear(mod); + mpz_clear(val); + mpz_clear(p); +} + +static void test_nla_assumption_core(void) { + context_t *ctx; + term_t x, p, q; + term_t imp1, imp2; + term_t assumptions[2]; + term_vector_t core; + smt_status_t stat; + + ctx = make_cdclt_context("QF_UFLRA"); + x = yices_new_uninterpreted_term(yices_real_type()); + p = yices_new_uninterpreted_term(yices_bool_type()); + q = yices_new_uninterpreted_term(yices_bool_type()); + + imp1 = yices_implies(p, yices_arith_eq_atom(yices_mul(x, x), yices_rational32(2, 1))); + imp2 = yices_implies(q, yices_arith_eq_atom(yices_mul(x, x), yices_rational32(3, 1))); + check_code(yices_assert_formula(ctx, imp1), "assert p=>x*x=2 failed"); + check_code(yices_assert_formula(ctx, imp2), "assert q=>x*x=3 failed"); + + assumptions[0] = p; + assumptions[1] = q; + stat = yices_check_context_with_assumptions(ctx, NULL, 2, assumptions); + check_status(stat, YICES_STATUS_UNSAT, "expected UNSAT with NLA assumptions p,q"); + + yices_init_term_vector(&core); + check_code(yices_get_unsat_core(ctx, &core), "yices_get_unsat_core failed for NLA assumptions"); + check(core.size == 2, "expected two assumptions in NLA unsat core"); + check(has_term(&core, p) && has_term(&core, q), "NLA unsat core missing assumptions"); + yices_delete_term_vector(&core); + + yices_free_context(ctx); +} + +static void test_division_by_zero_remains_error(void) { + context_t *ctx; + term_t r, z, div, f; + int32_t code; + + ctx = make_cdclt_context("QF_ALIRA"); + r = yices_new_uninterpreted_term(yices_real_type()); + z = yices_rational32(0, 1); + div = yices_division(r, z); + f = yices_arith_eq_atom(div, z); + + code = yices_assert_formula(ctx, f); + check(code < 0, "asserting division-by-zero formula should fail"); + check(yices_error_code() == DIVISION_BY_ZERO, "expected DIVISION_BY_ZERO"); + + yices_free_context(ctx); +} + +int main(void) { + if (!yices_has_mcsat()) { + return 1; // skipped + } + + yices_init(); + + test_nla_sat_unsat_and_model(); + test_nla_hidden_product_and_push_pop(); + test_nonconstant_divisor_and_param_modes(); + test_ff_sat_unsat_model_and_assumption_core(); + test_nla_assumption_core(); + test_division_by_zero_remains_error(); + + yices_exit(); + return 0; +}