From 93d223da9f23d8177880957d572622efc49f02bc Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 13 Feb 2024 11:53:11 -0800 Subject: [PATCH 01/23] Fixed typos --- src/mcsat/plugin.h | 3 +-- src/mcsat/solver.c | 14 +++++++------- 2 files changed, 8 insertions(+), 9 deletions(-) diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h index a75c506f9..2fdd56267 100644 --- a/src/mcsat/plugin.h +++ b/src/mcsat/plugin.h @@ -334,10 +334,9 @@ void plugin_construct(plugin_t* plugin) { plugin->pop = NULL; plugin->build_model = NULL; plugin->gc_mark = NULL; - plugin->gc_mark_and_clear = NULL; + plugin->gc_mark_and_clear = NULL; plugin->gc_sweep = NULL; plugin->set_exception_handler = NULL; } - #endif /* PLUGIN_H_ */ diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 0a344fa84..fe31359a3 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -563,7 +563,7 @@ void trail_token_definition_lemma(trail_token_t* token, term_t lemma, term_t t) ivector_push(&tk->ctx->mcsat->plugin_definition_vars, t); } -/** Concstruct the trail token */ +/** Construct the trail token */ static inline void trail_token_construct(plugin_trail_token_t* token, mcsat_plugin_context_t* ctx, variable_t x) { token->token_interface.add = trail_token_add; @@ -1159,7 +1159,7 @@ void mcsat_get_kind_owners(mcsat_solver_t* mcsat, term_t t, int_mset_t* owners) } -static void mcsat_process_registeration_queue(mcsat_solver_t* mcsat) { +static void mcsat_process_registration_queue(mcsat_solver_t* mcsat) { term_t t; uint32_t i, plugin_i; plugin_t* plugin; @@ -1488,7 +1488,7 @@ void mcsat_assert_formula(mcsat_solver_t* mcsat, term_t f) { // Add the terms f_pos = unsigned_term(f); f_pos_var = variable_db_get_variable(mcsat->var_db, f_pos); - mcsat_process_registeration_queue(mcsat); + mcsat_process_registration_queue(mcsat); // Remember the assertion ivector_push(&mcsat->assertion_vars, f_pos_var); @@ -1644,7 +1644,7 @@ void mcsat_add_lemma(mcsat_solver_t* mcsat, ivector_t* lemma, term_t decision_bo } // Process any newly registered variables - mcsat_process_registeration_queue(mcsat); + mcsat_process_registration_queue(mcsat); // Check if the literal has value (only negative allowed) if (trail_has_value(mcsat->trail, disjunct_pos_var)) { @@ -2551,7 +2551,7 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi assert(x_value >= 0); trail_add_propagation(mcsat->trail, x_var, &value, plugin_i, mcsat->trail->decision_level); mcsat_value_destruct(&value); - mcsat_process_registeration_queue(mcsat); + mcsat_process_registration_queue(mcsat); } mcsat_pop(mcsat); @@ -2584,7 +2584,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin // Make sure the variable is registered (maybe it doesn't appear in assertions) variable_t x_var = variable_db_get_variable(mcsat->var_db, unsigned_term(x)); ivector_push(&mcsat->assumption_vars, x_var); - mcsat_process_registeration_queue(mcsat); + mcsat_process_registration_queue(mcsat); } } @@ -2714,7 +2714,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin } // Make sure any additional terms are registered - mcsat_process_registeration_queue(mcsat); + mcsat_process_registration_queue(mcsat); solve_done: From b9ee6e110c5d00358d636f97e5f0007991717927 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 13 Feb 2024 18:18:22 -0800 Subject: [PATCH 02/23] rename int_queue_t size with capacity --- src/exists_forall/ef_values.c | 2 +- src/utils/int_queues.c | 24 ++++++++++++------------ src/utils/int_queues.h | 10 +++++----- 3 files changed, 18 insertions(+), 18 deletions(-) diff --git a/src/exists_forall/ef_values.c b/src/exists_forall/ef_values.c index 2bfc5f9bf..88368621f 100755 --- a/src/exists_forall/ef_values.c +++ b/src/exists_forall/ef_values.c @@ -557,7 +557,7 @@ void postprocess_ef_table(ef_table_t *vtable, bool check) { } } } - m = queue.size; + m = queue.capacity; j = 0; while(!int_queue_is_empty(&queue)) { tvalue = int_queue_pop(&queue); diff --git a/src/utils/int_queues.c b/src/utils/int_queues.c index 600f09ec2..88fc8fc87 100644 --- a/src/utils/int_queues.c +++ b/src/utils/int_queues.c @@ -27,17 +27,17 @@ /* - * Initialize a queue of size n + * Initialize a queue of capacity n */ void init_int_queue(int_queue_t *q, uint32_t n) { if (n == 0) { - n = DEFAULT_INT_QUEUE_INITIAL_SIZE; - } else if (n > MAX_INT_QUEUE_SIZE) { + n = DEFAULT_INT_QUEUE_INITIAL_CAPACITY; + } else if (n > MAX_INT_QUEUE_CAPACITY) { out_of_memory(); } q->data = (int32_t *) safe_malloc(n * sizeof(int32_t)); - q->size = n; + q->capacity = n; q->head = 0; q->tail = 0; } @@ -59,15 +59,15 @@ void delete_int_queue(int_queue_t *q) { static void resize_queue(int_queue_t *q) { uint32_t n; - n = q->size + 1; + n = q->capacity + 1; n += n >> 1; - if (n > MAX_INT_QUEUE_SIZE) { + if (n > MAX_INT_QUEUE_CAPACITY) { out_of_memory(); } q->data = (int32_t *) safe_realloc(q->data, n * sizeof(int32_t)); - q->size = n; + q->capacity = n; } @@ -83,7 +83,7 @@ void int_queue_push(int_queue_t *q, int32_t x) { i ++; q->tail = i; - if (i == q->size) { + if (i == q->capacity) { if (q->head == 0) { /* * full queue, stored in data[0...size-1], @@ -99,9 +99,9 @@ void int_queue_push(int_queue_t *q, int32_t x) { * increase the size and shift data[head .. size - 1] to the end * of the new data array. */ - n = q->size; + n = q->capacity; resize_queue(q); - j = q->size; + j = q->capacity; do { n --; j --; @@ -136,7 +136,7 @@ int32_t int_queue_pop(int_queue_t *q) { h = q->head; x = q->data[h]; h ++; - if (h >= q->size) h = 0; + if (h >= q->capacity) h = 0; q->head = h; return x; @@ -162,7 +162,7 @@ int32_t int_queue_last(int_queue_t *q) { assert(q->head != q->tail); i = q->tail; if (i == 0) { - i = q->size; + i = q->capacity; } assert(i > 0); return q->data[i-1]; diff --git a/src/utils/int_queues.h b/src/utils/int_queues.h index 9d916c72f..df8e7a6bb 100644 --- a/src/utils/int_queues.h +++ b/src/utils/int_queues.h @@ -30,17 +30,17 @@ /* * Components: * - data = integer array to store the elements - * - size = size of that array + * - capacity = size of that array * - head, tail = indices between 0 and size - 1. * The queue is managed as a circular array: * - if head = tail, the queue is empty * - if head < tail, the queue content is data[head ... tail-1] * - if head > tail, the queue content is - * data[head...size-1] + data[0 ... tail-1] + * data[head...capacity-1] + data[0 ... tail-1] */ typedef struct int_queue_s { int32_t *data; - uint32_t size; + uint32_t capacity; uint32_t head; uint32_t tail; } int_queue_t; @@ -49,13 +49,13 @@ typedef struct int_queue_s { /* * Maximal size: make sure n * sizeof(int32_t) does not overflow */ -#define MAX_INT_QUEUE_SIZE (UINT32_MAX/sizeof(int32_t)) +#define MAX_INT_QUEUE_CAPACITY (UINT32_MAX/sizeof(int32_t)) /* * Default size */ -#define DEFAULT_INT_QUEUE_INITIAL_SIZE 16 +#define DEFAULT_INT_QUEUE_INITIAL_CAPACITY 16 /* From 472deca3b5ff5a17588b885d10e38784d28d33ea Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 13 Feb 2024 18:33:27 -0800 Subject: [PATCH 03/23] enhanced int_queue --- src/utils/int_queues.c | 63 +++++++++++++++++++++++++++++------------- src/utils/int_queues.h | 55 ++++++++++++++++++++++-------------- 2 files changed, 78 insertions(+), 40 deletions(-) diff --git a/src/utils/int_queues.c b/src/utils/int_queues.c index 88fc8fc87..0a3ddca05 100644 --- a/src/utils/int_queues.c +++ b/src/utils/int_queues.c @@ -26,7 +26,7 @@ #include "utils/memalloc.h" -/* +/** * Initialize a queue of capacity n */ void init_int_queue(int_queue_t *q, uint32_t n) { @@ -43,7 +43,7 @@ void init_int_queue(int_queue_t *q, uint32_t n) { } -/* +/** * Delete: free data array */ void delete_int_queue(int_queue_t *q) { @@ -51,12 +51,12 @@ void delete_int_queue(int_queue_t *q) { q->data = NULL; } - -/* +/** * Resize the queue. make data array 50% larger. * content of data array is unchanged */ -static void resize_queue(int_queue_t *q) { +static +void resize_queue(int_queue_t *q) { uint32_t n; n = q->capacity + 1; @@ -70,9 +70,7 @@ static void resize_queue(int_queue_t *q) { q->capacity = n; } - - -/* +/** * Push element x at the end of the queue */ void int_queue_push(int_queue_t *q, int32_t x) { @@ -111,8 +109,7 @@ void int_queue_push(int_queue_t *q, int32_t x) { } } - -/* +/** * Push a[0 ... n-1] in the queue (in this order) */ void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n) { @@ -123,8 +120,7 @@ void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n) { } } - -/* +/** * Return first element and remove it */ int32_t int_queue_pop(int_queue_t *q) { @@ -142,21 +138,18 @@ int32_t int_queue_pop(int_queue_t *q) { return x; } - - -/* +/** * Get the first element (don't remove it). */ -int32_t int_queue_first(int_queue_t *q) { +int32_t int_queue_first(const int_queue_t *q) { assert(q->head != q->tail); return q->data[q->head]; } - -/* +/** * Get the last element (don't remove it) */ -int32_t int_queue_last(int_queue_t *q) { +int32_t int_queue_last(const int_queue_t *q) { uint32_t i; assert(q->head != q->tail); @@ -167,3 +160,35 @@ int32_t int_queue_last(int_queue_t *q) { assert(i > 0); return q->data[i-1]; } + +/** + * Get element at position i + */ +int32_t int_queue_at(const int_queue_t *q, uint32_t i) { + assert(q->head != q->tail); + + if (q->head < q->tail) { + assert(q->head + i < q->tail); + return q->data[q->head + i]; + } else if (q->head > q->tail) { + uint32_t size_first = q->capacity - q->head; + assert(i < size_first || i - size_first < q->tail); + return i < size_first + ? q->data[q->head + i] + : q->data[i - size_first]; + } + + assert(false); + return 0; +} + +/** + * Get size of queue + */ +uint32_t int_queue_size(const int_queue_t *q) { + if (q->head <= q->tail) { + return q->tail - q->head; + } else { + return (q->capacity - q->head) + q->tail; + } +} diff --git a/src/utils/int_queues.h b/src/utils/int_queues.h index df8e7a6bb..91a25203b 100644 --- a/src/utils/int_queues.h +++ b/src/utils/int_queues.h @@ -27,7 +27,7 @@ #include -/* +/** * Components: * - data = integer array to store the elements * - capacity = size of that array @@ -46,78 +46,91 @@ typedef struct int_queue_s { } int_queue_t; -/* +/** * Maximal size: make sure n * sizeof(int32_t) does not overflow */ #define MAX_INT_QUEUE_CAPACITY (UINT32_MAX/sizeof(int32_t)) -/* +/** * Default size */ #define DEFAULT_INT_QUEUE_INITIAL_CAPACITY 16 -/* +/** * Initialize a queue of size n. * If n = 0 then DEFAULT_QUEUE_INITIAL_SIZE is used. */ -extern void init_int_queue(int_queue_t *q, uint32_t n); +void init_int_queue(int_queue_t *q, uint32_t n); -/* +/** * Delete q */ -extern void delete_int_queue(int_queue_t *q); +void delete_int_queue(int_queue_t *q); -/* +/** * Push element x in the queue (at the end) */ -extern void int_queue_push(int_queue_t *q, int32_t x); +void int_queue_push(int_queue_t *q, int32_t x); -/* +/** * Push a[0 ... n-1] in the queue (in this order) */ -extern void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n); +void int_queue_push_array(int_queue_t *q, int32_t *a, uint32_t n); -/* +/** * Check whether the queue is empty */ static inline bool int_queue_is_empty(int_queue_t *q) { return q->head == q->tail; } -/* + +/** + * Gets the size of the queue. + */ +uint32_t int_queue_size(const int_queue_t *q); + + +/** * Return the first element and remove it from q. * - q must be non-empty. */ -extern int32_t int_queue_pop(int_queue_t *q); +int32_t int_queue_pop(int_queue_t *q); -/* +/** * Get the first element of q but don't remove it. * - q must be non-empty */ -extern int32_t int_queue_first(int_queue_t *q); +int32_t int_queue_first(const int_queue_t *q); -/* +/** * Get the last element of q (don't remove it) * - q must be non-empty */ -extern int32_t int_queue_last(int_queue_t *q); +int32_t int_queue_last(const int_queue_t *q); -/* +/** + * Gets the element at position i + */ +int32_t int_queue_at(const int_queue_t *q, uint32_t i); + + +/** * Empty the queue */ -static inline void int_queue_reset(int_queue_t *q) { +static inline +void int_queue_reset(int_queue_t *q) { q->head = 0; q->tail = 0; } - #endif /* __INT_QUEUES_H */ From ef12e8059061704abc4c76b0b6dbb1cb513adf9a Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 13 Feb 2024 18:46:48 -0800 Subject: [PATCH 04/23] added queue for next decision --- src/mcsat/nra/nra_plugin.c | 2 +- src/mcsat/plugin.h | 2 +- src/mcsat/solver.c | 36 ++++++++++++++++++++---------------- 3 files changed, 22 insertions(+), 18 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 801ca0e25..2f3962d21 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -692,7 +692,7 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) // If we are at bound variable, set it as main decision if (t == nra->global_bound_term) { - nra->ctx->request_top_decision(nra->ctx, t_var); + nra->ctx->hint_next_decision(nra->ctx, t_var); if (nra->ctx->options->nra_bound_min >= 0) { rational_t q; q_init(&q); diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h index 2fdd56267..395875706 100644 --- a/src/mcsat/plugin.h +++ b/src/mcsat/plugin.h @@ -111,7 +111,7 @@ struct plugin_context_s { int (*cmp_variables) (plugin_context_t* self, variable_t x, variable_t y); /** Request a variable to be a top decision variable */ - void (*request_top_decision) (plugin_context_t* self, variable_t x); + void (*hint_next_decision) (plugin_context_t* self, variable_t x); }; diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index fe31359a3..944a89bc3 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -230,7 +230,7 @@ struct mcsat_solver_s { uint32_t plugins_count; /** Variable to decide on first */ - variable_t top_decision_var; + int_queue_t top_decision_var_queue; /** The queue for variable decisions */ var_queue_t var_queue; @@ -628,9 +628,8 @@ void mcsat_plugin_context_gc(plugin_context_t* self) { } static inline -void mcsat_set_top_decision(mcsat_solver_t* mcsat, variable_t x) { - assert(mcsat->top_decision_var == variable_null); - mcsat->top_decision_var = x; +void mcsat_add_decision_hint(mcsat_solver_t* mcsat, variable_t x) { + int_queue_push(&mcsat->top_decision_var_queue, x); } static inline @@ -682,11 +681,11 @@ int mcsat_plugin_context_cmp_variables(plugin_context_t* self, variable_t x, var } static -void mcsat_plugin_context_request_top_decision(plugin_context_t* self, variable_t x) { +void mcsat_plugin_context_hint_next_decision(plugin_context_t* self, variable_t x) { mcsat_plugin_context_t* mctx; mctx = (mcsat_plugin_context_t*) self; - mcsat_set_top_decision(mctx->mcsat, x); - } + mcsat_add_decision_hint(mctx->mcsat, x); +} static void mcsat_plugin_context_decision_calls(plugin_context_t* self, type_kind_t type) { @@ -717,7 +716,7 @@ void mcsat_plugin_context_construct(mcsat_plugin_context_t* ctx, mcsat_solver_t* ctx->ctx.bump_variable = mcsat_plugin_context_bump_variable; ctx->ctx.bump_variable_n = mcsat_plugin_context_bump_variable_n; ctx->ctx.cmp_variables = mcsat_plugin_context_cmp_variables; - ctx->ctx.request_top_decision = mcsat_plugin_context_request_top_decision; + ctx->ctx.hint_next_decision = mcsat_plugin_context_hint_next_decision; ctx->mcsat = mcsat; ctx->plugin_name = plugin_name; } @@ -860,7 +859,7 @@ void mcsat_construct(mcsat_solver_t* mcsat, const context_t* ctx) { preprocessor_construct(&mcsat->preprocessor, mcsat->terms, mcsat->exception, &mcsat->ctx->mcsat_options); // The variable queue - mcsat->top_decision_var = variable_null; + init_int_queue(&mcsat->top_decision_var_queue, 0); var_queue_construct(&mcsat->var_queue); mcsat->pending_requests_all.restart = false; @@ -919,6 +918,7 @@ void mcsat_destruct(mcsat_solver_t* mcsat) { variable_db_destruct(mcsat->var_db); safe_free(mcsat->var_db); preprocessor_destruct(&mcsat->preprocessor); + delete_int_queue(&mcsat->top_decision_var_queue); var_queue_destruct(&mcsat->var_queue); delete_ivector(&mcsat->plugin_lemmas); delete_ivector(&mcsat->plugin_definition_lemmas); @@ -1251,9 +1251,9 @@ void mcsat_gc(mcsat_solver_t* mcsat, bool mark_and_gc_internal) { } } - // Mark the top decision variable if any - if (mcsat->top_decision_var != variable_null) { - gc_info_mark(&gc_vars, mcsat->top_decision_var); + // Mark the decision hints if there are any + for (i = 0; i < int_queue_size(&mcsat->top_decision_var_queue); ++ i) { + gc_info_mark(&gc_vars, int_queue_at(&mcsat->top_decision_var_queue, i)); } // Mark the trail variables as needed @@ -2320,7 +2320,6 @@ static bool mcsat_decide(mcsat_solver_t* mcsat) { uint32_t i; - variable_t var; plugin_t* plugin; plugin_trail_token_t decision_token; @@ -2329,12 +2328,17 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { assert(!mcsat->trail->inconsistent); + variable_t var = variable_null; bool force_decision = false; while (true) { - // Use the variable a plugin requested - var = mcsat->top_decision_var; - if (var != variable_null && trail_has_value(mcsat->trail, var)) { + // Use the variables a plugin requested + while (!int_queue_is_empty(&mcsat->top_decision_var_queue)) { + var = int_queue_pop(&mcsat->top_decision_var_queue); + assert(var != variable_null); + if (!trail_has_value(mcsat->trail, var)) { + break; + } var = variable_null; } From d786129efc4f5c661977c97435350b801ff4cb8a Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 15 Feb 2024 16:32:09 -0800 Subject: [PATCH 05/23] Clear hint queue on conflict --- src/mcsat/solver.c | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 944a89bc3..5f0d05574 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -1247,7 +1247,7 @@ void mcsat_gc(mcsat_solver_t* mcsat, bool mark_and_gc_internal) { gc_info_mark(&gc_vars, var); if (trace_enabled(mcsat->ctx->trace, "mcsat::gc")) { mcsat_trace_printf(mcsat->ctx->trace, "mcsat_gc(): marking "); - trace_term_ln(mcsat->ctx->trace, mcsat->terms, variable_db_get_term(mcsat->var_db, var)); + trace_term_ln(mcsat->ctx->trace, mcsat->terms, variable_db_get_term(mcsat->var_db, var)); } } @@ -2707,6 +2707,9 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin break; } + // remove all the hints + int_queue_reset(&mcsat->top_decision_var_queue); + // update the variable selection heuristic var_queue_decay_activities(&mcsat->var_queue); } From 5de62d2ec436f9305cf0ca7eeb0cf9df95512c49 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 17:04:31 -0800 Subject: [PATCH 06/23] Added two queues (top and hint) --- src/mcsat/nra/nra_plugin.c | 2 +- src/mcsat/plugin.h | 3 ++ src/mcsat/solver.c | 56 ++++++++++++++++++++++++++++++-------- 3 files changed, 49 insertions(+), 12 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 2f3962d21..801ca0e25 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -692,7 +692,7 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop) // If we are at bound variable, set it as main decision if (t == nra->global_bound_term) { - nra->ctx->hint_next_decision(nra->ctx, t_var); + nra->ctx->request_top_decision(nra->ctx, t_var); if (nra->ctx->options->nra_bound_min >= 0) { rational_t q; q_init(&q); diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h index 395875706..685dbedce 100644 --- a/src/mcsat/plugin.h +++ b/src/mcsat/plugin.h @@ -111,6 +111,9 @@ struct plugin_context_s { int (*cmp_variables) (plugin_context_t* self, variable_t x, variable_t y); /** Request a variable to be a top decision variable */ + void (*request_top_decision) (plugin_context_t* self, variable_t x); + + /** Request a variable to be a next decision variable */ void (*hint_next_decision) (plugin_context_t* self, variable_t x); }; diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 5f0d05574..f6ee8503c 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -230,7 +230,10 @@ struct mcsat_solver_s { uint32_t plugins_count; /** Variable to decide on first */ - int_queue_t top_decision_var_queue; + ivector_t top_decision_vars; + + /** Variables hinted by the plugins to decide next */ + int_queue_t hinted_decision_vars; /** The queue for variable decisions */ var_queue_t var_queue; @@ -627,9 +630,16 @@ void mcsat_plugin_context_gc(plugin_context_t* self) { mcsat_request_gc(mctx->mcsat); } +static inline +void mcsat_add_top_decision(mcsat_solver_t* mcsat, variable_t x) { + // TODO check that the hint is coming from the proper solver + ivector_push(&mcsat->top_decision_vars, x); +} + static inline void mcsat_add_decision_hint(mcsat_solver_t* mcsat, variable_t x) { - int_queue_push(&mcsat->top_decision_var_queue, x); + // TODO check that the hint is coming from the proper solver + int_queue_push(&mcsat->hinted_decision_vars, x); } static inline @@ -680,6 +690,13 @@ int mcsat_plugin_context_cmp_variables(plugin_context_t* self, variable_t x, var return var_queue_cmp_variables(&mctx->mcsat->var_queue, x, y); } +static +void mcsat_plugin_context_request_top_decision(plugin_context_t* self, variable_t x) { + mcsat_plugin_context_t* mctx; + mctx = (mcsat_plugin_context_t*) self; + mcsat_add_top_decision(mctx->mcsat, x); +} + static void mcsat_plugin_context_hint_next_decision(plugin_context_t* self, variable_t x) { mcsat_plugin_context_t* mctx; @@ -716,6 +733,7 @@ void mcsat_plugin_context_construct(mcsat_plugin_context_t* ctx, mcsat_solver_t* ctx->ctx.bump_variable = mcsat_plugin_context_bump_variable; ctx->ctx.bump_variable_n = mcsat_plugin_context_bump_variable_n; ctx->ctx.cmp_variables = mcsat_plugin_context_cmp_variables; + ctx->ctx.request_top_decision = mcsat_plugin_context_request_top_decision; ctx->ctx.hint_next_decision = mcsat_plugin_context_hint_next_decision; ctx->mcsat = mcsat; ctx->plugin_name = plugin_name; @@ -859,7 +877,8 @@ void mcsat_construct(mcsat_solver_t* mcsat, const context_t* ctx) { preprocessor_construct(&mcsat->preprocessor, mcsat->terms, mcsat->exception, &mcsat->ctx->mcsat_options); // The variable queue - init_int_queue(&mcsat->top_decision_var_queue, 0); + init_ivector(&mcsat->top_decision_vars, 0); + init_int_queue(&mcsat->hinted_decision_vars, 0); var_queue_construct(&mcsat->var_queue); mcsat->pending_requests_all.restart = false; @@ -918,7 +937,8 @@ void mcsat_destruct(mcsat_solver_t* mcsat) { variable_db_destruct(mcsat->var_db); safe_free(mcsat->var_db); preprocessor_destruct(&mcsat->preprocessor); - delete_int_queue(&mcsat->top_decision_var_queue); + delete_ivector(&mcsat->top_decision_vars); + delete_int_queue(&mcsat->hinted_decision_vars); var_queue_destruct(&mcsat->var_queue); delete_ivector(&mcsat->plugin_lemmas); delete_ivector(&mcsat->plugin_definition_lemmas); @@ -1252,8 +1272,11 @@ void mcsat_gc(mcsat_solver_t* mcsat, bool mark_and_gc_internal) { } // Mark the decision hints if there are any - for (i = 0; i < int_queue_size(&mcsat->top_decision_var_queue); ++ i) { - gc_info_mark(&gc_vars, int_queue_at(&mcsat->top_decision_var_queue, i)); + for (i = 0; i < int_queue_size(&mcsat->hinted_decision_vars); ++ i) { + gc_info_mark(&gc_vars, int_queue_at(&mcsat->hinted_decision_vars, i)); + } + for (i = 0; i < mcsat->top_decision_vars.size; ++i) { + gc_info_mark(&gc_vars, mcsat->top_decision_vars.data[i]); } // Mark the trail variables as needed @@ -2332,9 +2355,9 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { bool force_decision = false; while (true) { - // Use the variables a plugin requested - while (!int_queue_is_empty(&mcsat->top_decision_var_queue)) { - var = int_queue_pop(&mcsat->top_decision_var_queue); + // Us the top variables first + for (i = 0; i < mcsat->top_decision_vars.size; ++i) { + var = mcsat->top_decision_vars.data[i]; assert(var != variable_null); if (!trail_has_value(mcsat->trail, var)) { break; @@ -2342,11 +2365,22 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { var = variable_null; } + // then try the variables a plugin requested + if (var == variable_null) { + while (!int_queue_is_empty(&mcsat->hinted_decision_vars)) { + var = int_queue_pop(&mcsat->hinted_decision_vars); + assert(var != variable_null); + if (!trail_has_value(mcsat->trail, var)) { + break; + } + var = variable_null; + } + } + // If there is an order that was passed in, try that if (var == variable_null) { const ivector_t* order = &mcsat->ctx->mcsat_var_order; if (order->size > 0) { - uint32_t i; if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { FILE* out = trace_out(mcsat->ctx->trace); fprintf(out, "mcsat_decide(): var_order is "); @@ -2708,7 +2742,7 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin } // remove all the hints - int_queue_reset(&mcsat->top_decision_var_queue); + int_queue_reset(&mcsat->hinted_decision_vars); // update the variable selection heuristic var_queue_decay_activities(&mcsat->var_queue); } From 83bfa01a6578ce21e503350d27ef1d2ed5c8cdbf Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 17:10:42 -0800 Subject: [PATCH 07/23] fixed bug --- src/mcsat/solver.c | 7 +++---- 1 file changed, 3 insertions(+), 4 deletions(-) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index f6ee8503c..96bf4faa5 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -632,13 +632,11 @@ void mcsat_plugin_context_gc(plugin_context_t* self) { static inline void mcsat_add_top_decision(mcsat_solver_t* mcsat, variable_t x) { - // TODO check that the hint is coming from the proper solver ivector_push(&mcsat->top_decision_vars, x); } static inline void mcsat_add_decision_hint(mcsat_solver_t* mcsat, variable_t x) { - // TODO check that the hint is coming from the proper solver int_queue_push(&mcsat->hinted_decision_vars, x); } @@ -2268,7 +2266,7 @@ bool mcsat_decide_assumption(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_ass break; } - // The variable (should exists already) + // The variable (should exist already) var_term = assumptions[mcsat->assumption_i]; var = variable_db_get_variable_if_exists(mcsat->var_db, var_term); assert(var != variable_null); @@ -2343,6 +2341,7 @@ static bool mcsat_decide(mcsat_solver_t* mcsat) { uint32_t i; + variable_t var; plugin_t* plugin; plugin_trail_token_t decision_token; @@ -2351,9 +2350,9 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { assert(!mcsat->trail->inconsistent); - variable_t var = variable_null; bool force_decision = false; while (true) { + var = variable_null; // Us the top variables first for (i = 0; i < mcsat->top_decision_vars.size; ++i) { From 6262396aa18ad376920ee943de13e3b47d1b95e6 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Fri, 16 Feb 2024 18:10:54 -0800 Subject: [PATCH 08/23] added solver hints in NRA --- src/mcsat/nra/nra_plugin.c | 33 +++++++++++++++++++-------------- 1 file changed, 19 insertions(+), 14 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 801ca0e25..692c472a6 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -860,20 +860,25 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, } lp_value_destruct(&v); } - // If the value is implied at zero level, propagate it - if (!nra->ctx->options->model_interpolation && !x_in_conflict && !trail_has_value(nra->ctx->trail, x) && trail_is_at_base_level(nra->ctx->trail)) { - const lp_feasibility_set_t* feasible = feasible_set_db_get(nra->feasible_set_db, x); - if (lp_feasibility_set_is_point(feasible)) { - lp_value_t x_value; - lp_value_construct_none(&x_value); - lp_feasibility_set_pick_value(feasible, &x_value); - if (lp_value_is_rational(&x_value)) { - mcsat_value_t value; - mcsat_value_construct_lp_value(&value, &x_value); - prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); - mcsat_value_destruct(&value); + // TODO check if we are allowed to give hints with model_interpolation? (see issue 274) + if (!x_in_conflict && !trail_has_value(nra->ctx->trail, x) && !nra->ctx->options->model_interpolation) { + const lp_feasibility_set_t *feasible_set = feasible_set_db_get(nra->feasible_set_db, x); + if (lp_feasibility_set_is_point(feasible_set)) { + if (trail_is_at_base_level(nra->ctx->trail)) { + lp_value_t x_value; + lp_value_construct_none(&x_value); + lp_feasibility_set_pick_value(feasible_set, &x_value); + if (lp_value_is_rational(&x_value)) { + mcsat_value_t value; + mcsat_value_construct_lp_value(&value, &x_value); + prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); + mcsat_value_destruct(&value); + } + lp_value_destruct(&x_value); + } else { + // TODO add statistics + nra->ctx->hint_next_decision(nra->ctx, x); } - lp_value_destruct(&x_value); } } } @@ -1069,7 +1074,7 @@ void nra_plugin_propagate(plugin_t* plugin, trail_token_t* prop) { } // Propagate - while(trail_is_consistent(trail) && nra->trail_i < trail_size(trail)) { + while (trail_is_consistent(trail) && nra->trail_i < trail_size(trail)) { // Current trail element var = trail_at(trail, nra->trail_i); nra->trail_i ++; From 36df7346b400e501c48915b339e66718a0ccec8f Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Mon, 19 Feb 2024 11:55:03 -0800 Subject: [PATCH 09/23] model_interpolation questions --- src/mcsat/nra/nra_plugin.c | 27 +++++++++++++++------------ 1 file changed, 15 insertions(+), 12 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 692c472a6..556ca802c 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -860,21 +860,24 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, } lp_value_destruct(&v); } - // TODO check if we are allowed to give hints with model_interpolation? (see issue 274) - if (!x_in_conflict && !trail_has_value(nra->ctx->trail, x) && !nra->ctx->options->model_interpolation) { + if (!x_in_conflict && !trail_has_value(nra->ctx->trail, x)) { const lp_feasibility_set_t *feasible_set = feasible_set_db_get(nra->feasible_set_db, x); if (lp_feasibility_set_is_point(feasible_set)) { - if (trail_is_at_base_level(nra->ctx->trail)) { - lp_value_t x_value; - lp_value_construct_none(&x_value); - lp_feasibility_set_pick_value(feasible_set, &x_value); - if (lp_value_is_rational(&x_value)) { - mcsat_value_t value; - mcsat_value_construct_lp_value(&value, &x_value); - prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); - mcsat_value_destruct(&value); + if (trail_is_at_base_level(nra->ctx->trail) && !nra->ctx->options->model_interpolation) { + if (!nra->ctx->options->model_interpolation) { + lp_value_t x_value; + lp_value_construct_none(&x_value); + lp_feasibility_set_pick_value(feasible_set, &x_value); + if (lp_value_is_rational(&x_value)) { + mcsat_value_t value; + mcsat_value_construct_lp_value(&value, &x_value); + prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); + mcsat_value_destruct(&value); + } + lp_value_destruct(&x_value); + } else { + //nra->ctx->request_top_decision(nra->ctx, x); } - lp_value_destruct(&x_value); } else { // TODO add statistics nra->ctx->hint_next_decision(nra->ctx, x); From 8c32738a968654b20b6dd8defc7d05e7dc75a389 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 21 Feb 2024 17:08:16 -0800 Subject: [PATCH 10/23] model_interpolation does not perform request_top_decision --- src/mcsat/nra/nra_plugin.c | 22 +++++++++------------- 1 file changed, 9 insertions(+), 13 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 556ca802c..86e189186 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -864,20 +864,16 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, const lp_feasibility_set_t *feasible_set = feasible_set_db_get(nra->feasible_set_db, x); if (lp_feasibility_set_is_point(feasible_set)) { if (trail_is_at_base_level(nra->ctx->trail) && !nra->ctx->options->model_interpolation) { - if (!nra->ctx->options->model_interpolation) { - lp_value_t x_value; - lp_value_construct_none(&x_value); - lp_feasibility_set_pick_value(feasible_set, &x_value); - if (lp_value_is_rational(&x_value)) { - mcsat_value_t value; - mcsat_value_construct_lp_value(&value, &x_value); - prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); - mcsat_value_destruct(&value); - } - lp_value_destruct(&x_value); - } else { - //nra->ctx->request_top_decision(nra->ctx, x); + lp_value_t x_value; + lp_value_construct_none(&x_value); + lp_feasibility_set_pick_value(feasible_set, &x_value); + if (lp_value_is_rational(&x_value)) { + mcsat_value_t value; + mcsat_value_construct_lp_value(&value, &x_value); + prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); + mcsat_value_destruct(&value); } + lp_value_destruct(&x_value); } else { // TODO add statistics nra->ctx->hint_next_decision(nra->ctx, x); From da32bd46fda28a15bf949b2e3eb7180a5f5d217a Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 22 Feb 2024 14:03:51 -0800 Subject: [PATCH 11/23] Remove shortcut variables from the queue --- src/mcsat/solver.c | 32 +++++++++++++++++++------------- src/mcsat/variable_queue.c | 19 ++++++++++++++----- src/mcsat/variable_queue.h | 3 +++ 3 files changed, 36 insertions(+), 18 deletions(-) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 96bf4faa5..4f18beaea 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2410,25 +2410,31 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { if (trail_has_value(mcsat->trail, var)) { var = variable_null; } else { + // TODO: what if var gets skipped and is tried to be reintroduced? // fprintf(stderr, "random\n"); } } } - // Use the queue - while (!var_queue_is_empty(&mcsat->var_queue) && var == variable_null) { - // Get the next variable from the queue - var = var_queue_pop(&mcsat->var_queue); - // If already assigned go on - if (trail_has_value(mcsat->trail, var)) { - if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { - FILE* out = trace_out(mcsat->ctx->trace); - fprintf(out, "mcsat_decide(): skipping "); - variable_db_print_variable(mcsat->var_db, var, out); - fprintf(out, "\n"); + if (var != variable_null) { + // variable was selected w/o consulting the queue, keep the queue up to date + var_queue_remove(&mcsat->var_queue, var); + } else { + // Use the queue + while (!var_queue_is_empty(&mcsat->var_queue) && var == variable_null) { + // Get the next variable from the queue + var = var_queue_pop(&mcsat->var_queue); + // If already assigned go on + if (trail_has_value(mcsat->trail, var)) { + if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { + FILE *out = trace_out(mcsat->ctx->trace); + fprintf(out, "mcsat_decide(): skipping "); + variable_db_print_variable(mcsat->var_db, var, out); + fprintf(out, "\n"); + } + var = variable_null; + continue; } - var = variable_null; - continue; } } diff --git a/src/mcsat/variable_queue.c b/src/mcsat/variable_queue.c index d56b64926..17c042e90 100644 --- a/src/mcsat/variable_queue.c +++ b/src/mcsat/variable_queue.c @@ -114,13 +114,13 @@ void var_queue_update_up(var_queue_t *queue, variable_t x, uint32_t i) { } static -void var_queue_update_down(var_queue_t *queue) { +void var_queue_update_down(var_queue_t *queue, uint32_t i) { double *act; int32_t *index; variable_t *h; variable_t x, y, z; double ax, ay, az; - uint32_t i, j, last; + uint32_t j, last; last = queue->heap_last; queue->heap_last = last - 1; @@ -128,6 +128,7 @@ void var_queue_update_down(var_queue_t *queue) { assert(queue->heap_last == 0); return; } + assert(i <= last); h = queue->heap; index = queue->heap_index; @@ -137,8 +138,7 @@ void var_queue_update_down(var_queue_t *queue) { h[last] = -2; // set end marker: act[-2] is negative az = act[z]; // activity of the last element - i = 1; // root - j = 2; // left child of i + j = i << 1; // left child of i while (j < last) { /* * find child of i with highest activity. @@ -204,11 +204,20 @@ variable_t var_queue_pop(var_queue_t *queue) { queue->heap_index[top] = -1; // repair the heap - var_queue_update_down(queue); + var_queue_update_down(queue, 1); return top; } +void var_queue_remove(var_queue_t *queue, variable_t var) { + if (queue->heap_index[var] >= 0) { + uint32_t idx = queue->heap_index[var]; + assert(idx <= queue->heap_last); + var_queue_update_down(queue, idx); + queue->heap_index[var] = -1; + } +} + /** Get random element (the heap must not be empty) */ variable_t var_queue_random(var_queue_t *queue, double* seed) { assert(queue->heap_last > 0); diff --git a/src/mcsat/variable_queue.h b/src/mcsat/variable_queue.h index 484a1ac18..f1d73a97b 100644 --- a/src/mcsat/variable_queue.h +++ b/src/mcsat/variable_queue.h @@ -84,6 +84,9 @@ bool var_queue_is_empty(var_queue_t *queue); /** Get and remove top element (the heap must not be empty) */ variable_t var_queue_pop(var_queue_t *queue); +/** Removes one variable from the heap (var must be on the heap) */ +void var_queue_remove(var_queue_t *queue, variable_t var); + /** Get and remove random element (the heap must not be empty) */ variable_t var_queue_random(var_queue_t *queue, double *seed); From aec6c21e43f5c7cc5914bd8a5663e69fc511adfe Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 22 Feb 2024 15:49:18 -0800 Subject: [PATCH 12/23] regression prints execution time --- tests/regress/check.sh | 6 ++++++ tests/regress/run_test.sh | 2 ++ 2 files changed, 8 insertions(+) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 0849f6ea7..5ac115389 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -192,6 +192,12 @@ fail=$(find "$logdir" -type f -name "*.error" | wc -l) echo "Pass: $pass" echo "Fail: $fail" +if [[ $pass -gt 0 ]]; then + echo "Runtime: $(find "$logdir" -type f -exec sed -n '2p' {} \; | paste -sd+ - | bc) s" + if [[ $fail -gt 0 ]]; then + echo "Runtime (passed): $(find "$logdir" -type f -name "*.pass" -exec sed -n '2p' {} \; | paste -sd+ - | bc) s" + fi +fi if [ "$fail" -eq 0 ] ; then code=0 diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index 2ef34be9d..b3a9f8c94 100755 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -178,6 +178,7 @@ then if [ -n "$log_file" ] ; then log_file="$log_file.pass" echo "$test_string" > "$log_file" + echo "$runtime" >> "$log_file" fi code=0 else @@ -185,6 +186,7 @@ else 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 From c0b00365ed7f6da3bc540b00aa873d6e30f957a5 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 22 Feb 2024 15:50:05 -0800 Subject: [PATCH 13/23] nra_plugin.c hint only on real solution --- src/mcsat/nra/nra_plugin.c | 18 +++++++++--------- 1 file changed, 9 insertions(+), 9 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 86e189186..ad290f7d7 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -863,21 +863,21 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, if (!x_in_conflict && !trail_has_value(nra->ctx->trail, x)) { const lp_feasibility_set_t *feasible_set = feasible_set_db_get(nra->feasible_set_db, x); if (lp_feasibility_set_is_point(feasible_set)) { - if (trail_is_at_base_level(nra->ctx->trail) && !nra->ctx->options->model_interpolation) { - lp_value_t x_value; - lp_value_construct_none(&x_value); - lp_feasibility_set_pick_value(feasible_set, &x_value); - if (lp_value_is_rational(&x_value)) { + lp_value_t x_value; + lp_value_construct_none(&x_value); + lp_feasibility_set_pick_value(feasible_set, &x_value); + if (lp_value_is_rational(&x_value)) { + if (trail_is_at_base_level(nra->ctx->trail) && !nra->ctx->options->model_interpolation) { mcsat_value_t value; mcsat_value_construct_lp_value(&value, &x_value); prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); mcsat_value_destruct(&value); + } else { + // TODO add statistics + nra->ctx->hint_next_decision(nra->ctx, x); } - lp_value_destruct(&x_value); - } else { - // TODO add statistics - nra->ctx->hint_next_decision(nra->ctx, x); } + lp_value_destruct(&x_value); } } } From c4297592d09e296f48e76f14161e7b65ba332d2c Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 22 Feb 2024 15:53:42 -0800 Subject: [PATCH 14/23] variable selection forces decision on hint --- src/mcsat/solver.c | 33 +++++++++++++++------------------ 1 file changed, 15 insertions(+), 18 deletions(-) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 4f18beaea..ba3eea907 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2359,6 +2359,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { var = mcsat->top_decision_vars.data[i]; assert(var != variable_null); if (!trail_has_value(mcsat->trail, var)) { + force_decision = true; break; } var = variable_null; @@ -2370,6 +2371,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { var = int_queue_pop(&mcsat->hinted_decision_vars); assert(var != variable_null); if (!trail_has_value(mcsat->trail, var)) { + force_decision = true; break; } var = variable_null; @@ -2416,25 +2418,20 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { } } - if (var != variable_null) { - // variable was selected w/o consulting the queue, keep the queue up to date - var_queue_remove(&mcsat->var_queue, var); - } else { - // Use the queue - while (!var_queue_is_empty(&mcsat->var_queue) && var == variable_null) { - // Get the next variable from the queue - var = var_queue_pop(&mcsat->var_queue); - // If already assigned go on - if (trail_has_value(mcsat->trail, var)) { - if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { - FILE *out = trace_out(mcsat->ctx->trace); - fprintf(out, "mcsat_decide(): skipping "); - variable_db_print_variable(mcsat->var_db, var, out); - fprintf(out, "\n"); - } - var = variable_null; - continue; + // Use the queue + while (!var_queue_is_empty(&mcsat->var_queue) && var == variable_null) { + // Get the next variable from the queue + var = var_queue_pop(&mcsat->var_queue); + // If already assigned go on + if (trail_has_value(mcsat->trail, var)) { + if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { + FILE *out = trace_out(mcsat->ctx->trace); + fprintf(out, "mcsat_decide(): skipping "); + variable_db_print_variable(mcsat->var_db, var, out); + fprintf(out, "\n"); } + var = variable_null; + continue; } } From 7fcca51ebf77e734a96f2f6c6d9069d7221da6a4 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 22 Feb 2024 15:54:04 -0800 Subject: [PATCH 15/23] fix random decision --- src/mcsat/solver.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index ba3eea907..e2fb8e11e 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2404,7 +2404,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { } // Random decision: - if (var == variable_null) { + if (var == variable_null && mcsat->heuristic_params.random_decision_freq > 0.0) { double* seed = &mcsat->heuristic_params.random_decision_seed; double freq = mcsat->heuristic_params.random_decision_freq; if (drand(seed) < freq && !var_queue_is_empty(&mcsat->var_queue)) { @@ -2412,8 +2412,8 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { if (trail_has_value(mcsat->trail, var)) { var = variable_null; } else { - // TODO: what if var gets skipped and is tried to be reintroduced? // fprintf(stderr, "random\n"); + var_queue_remove(&mcsat->var_queue, var); } } } From 20deb566ce006d11f14ff08cdb694cb58aadf83c Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 22 Feb 2024 17:03:29 -0800 Subject: [PATCH 16/23] trace printing --- src/mcsat/nra/nra_plugin.c | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index ad290f7d7..308671689 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -874,6 +874,9 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, mcsat_value_destruct(&value); } else { // TODO add statistics + if (ctx_trace_enabled(nra->ctx, "nra::propagate")) { + ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", x); + } nra->ctx->hint_next_decision(nra->ctx, x); } } From f4f6e5857b055ccb01f1a4e67622a91028a418e7 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Thu, 22 Feb 2024 17:04:01 -0800 Subject: [PATCH 17/23] changed the gold of a model interpolant --- tests/regress/mcsat/uf/assumptions/issue274.smt2.gold | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold b/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold index ea078ecf1..34805e86a 100644 --- a/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold +++ b/tests/regress/mcsat/uf/assumptions/issue274.smt2.gold @@ -1,2 +1,2 @@ unsat -(or (= r1 0) (>= (* -1 r1) 0) (>= (+ -6873817 (* -35151836873817 r1) (* -10000000 (^ r1 2))) 0) (>= (+ -35151836873817 (* -20000000 r1)) 0)) +(or (= r1 0) (>= (* -1 r1) 0) ) From fdced2cb93ce8a5f818425e54e0528de64c36396 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Mon, 26 Feb 2024 10:32:24 -0800 Subject: [PATCH 18/23] added option for test issue204.smt2 --- tests/regress/mcsat/nra/issue204.smt2.options | 1 + 1 file changed, 1 insertion(+) create mode 100644 tests/regress/mcsat/nra/issue204.smt2.options diff --git a/tests/regress/mcsat/nra/issue204.smt2.options b/tests/regress/mcsat/nra/issue204.smt2.options new file mode 100644 index 000000000..55e9392b3 --- /dev/null +++ b/tests/regress/mcsat/nra/issue204.smt2.options @@ -0,0 +1 @@ +--mcsat --mcsat-nra-bound \ No newline at end of file From 67348606db537f337757a3f3a100abf91e1c83d3 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 5 Mar 2024 20:07:38 -0800 Subject: [PATCH 19/23] Removed ToDo --- src/mcsat/nra/nra_plugin.c | 1 - 1 file changed, 1 deletion(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 308671689..422c3a3f3 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -873,7 +873,6 @@ void nra_plugin_process_unit_constraint(nra_plugin_t* nra, trail_token_t* prop, prop->add_at_level(prop, x, &value, nra->ctx->trail->decision_level_base); mcsat_value_destruct(&value); } else { - // TODO add statistics if (ctx_trace_enabled(nra->ctx, "nra::propagate")) { ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", x); } From bd2daab658c1c3ac86cfb724245b7ab3c86890d2 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Tue, 5 Mar 2024 20:46:15 -0800 Subject: [PATCH 20/23] avoid dupplication in top_decision_queue --- src/mcsat/solver.c | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index e2fb8e11e..69195671b 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -632,6 +632,11 @@ void mcsat_plugin_context_gc(plugin_context_t* self) { static inline void mcsat_add_top_decision(mcsat_solver_t* mcsat, variable_t x) { + for (int i = 0; i < mcsat->top_decision_vars.size; ++i) { + if (mcsat->top_decision_vars.data[i] == x) { + return; + } + } ivector_push(&mcsat->top_decision_vars, x); } From f19e9271e383ad605fcf2c7d3142db73d2f41bb9 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Mon, 11 Mar 2024 10:45:54 -0700 Subject: [PATCH 21/23] Revert "regression prints execution time" This reverts commit aec6c21e43f5c7cc5914bd8a5663e69fc511adfe. --- tests/regress/check.sh | 6 ------ tests/regress/run_test.sh | 2 -- 2 files changed, 8 deletions(-) diff --git a/tests/regress/check.sh b/tests/regress/check.sh index 5ac115389..0849f6ea7 100755 --- a/tests/regress/check.sh +++ b/tests/regress/check.sh @@ -192,12 +192,6 @@ fail=$(find "$logdir" -type f -name "*.error" | wc -l) echo "Pass: $pass" echo "Fail: $fail" -if [[ $pass -gt 0 ]]; then - echo "Runtime: $(find "$logdir" -type f -exec sed -n '2p' {} \; | paste -sd+ - | bc) s" - if [[ $fail -gt 0 ]]; then - echo "Runtime (passed): $(find "$logdir" -type f -name "*.pass" -exec sed -n '2p' {} \; | paste -sd+ - | bc) s" - fi -fi if [ "$fail" -eq 0 ] ; then code=0 diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh index b3a9f8c94..2ef34be9d 100755 --- a/tests/regress/run_test.sh +++ b/tests/regress/run_test.sh @@ -178,7 +178,6 @@ then if [ -n "$log_file" ] ; then log_file="$log_file.pass" echo "$test_string" > "$log_file" - echo "$runtime" >> "$log_file" fi code=0 else @@ -186,7 +185,6 @@ else 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 From 88e15a3f5bf13c6a9f55365165c9453941299026 Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 13 Mar 2024 11:25:29 -0700 Subject: [PATCH 22/23] Update mcsat_decision (fixed aux decision problems) and moved hinted queue reset to pop. --- src/mcsat/solver.c | 143 ++++++++++++++++++++++++++------------------- 1 file changed, 84 insertions(+), 59 deletions(-) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 69195671b..c4243e69d 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -1017,6 +1017,9 @@ void mcsat_pop_internal(mcsat_solver_t* mcsat) { var_queue_insert(&mcsat->var_queue, unassigned->data[i]); } ivector_reset(unassigned); + + // remove all the hints + int_queue_reset(&mcsat->hinted_decision_vars); } static @@ -2339,32 +2342,88 @@ bool mcsat_decide_assumption(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_ass } /** - * Decides a variable using one of the plugins. Returns true if a variable - * has been decided, or a conflict detected. + * Finds the correct plugin for var and asks it to make a decision. + * Returns true if a decision was made on var. */ static -bool mcsat_decide(mcsat_solver_t* mcsat) { +bool mcsat_decide_var(mcsat_solver_t* mcsat, variable_t var, bool force_decision) { + // must be a valid variable that is not yet decided upon + assert(var != variable_null); + assert(!trail_has_value(mcsat->trail, var)); uint32_t i; - variable_t var; plugin_t* plugin; plugin_trail_token_t decision_token; + bool made_decision = false; + + // Get the owner that will decide that value of the variable + i = mcsat->decision_makers[variable_db_get_type_kind(mcsat->var_db, var)]; + assert(i != MCSAT_MAX_PLUGINS); + // Construct the token + trail_token_construct(&decision_token, mcsat->plugins[i].plugin_ctx, var); + // Decide + if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { + mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): with %s\n", mcsat->plugins[i].plugin_name); + mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): variable "); + variable_db_print_variable(mcsat->var_db, var, trace_out(mcsat->ctx->trace)); + mcsat_trace_printf(mcsat->ctx->trace, "\n"); + } + plugin = mcsat->plugins[i].plugin; + + // Ask the owner to decide + mcsat_push_internal(mcsat); + assert(plugin->decide); + plugin->decide(plugin, var, (trail_token_t*) &decision_token, force_decision); - ivector_t skipped_variables; // Variables we took from the queue but plugin didn't decide - init_ivector(&skipped_variables, 0); + if (decision_token.used == 0) { + // If not decided, remember and go on + made_decision = false; + mcsat_pop_internal(mcsat); + } else { + made_decision = true; + // Decided, we can continue with the search + (*mcsat->solver_stats.decisions)++; + // Plugins are not allowed to cheat and decide on another variable + assert(trail_has_value(mcsat->trail, var)); + if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { + FILE* out = trace_out(mcsat->ctx->trace); + fprintf(out, "mcsat_decide(): value = "); + mcsat_value_print(trail_get_value(mcsat->trail, var), out); + fprintf(out, "\n"); + } + } + + // a forced decision implies a made decision + assert(!force_decision || made_decision); + return made_decision; +} + +/** + * Decides a variable using one of the plugins. Returns true if a variable + * has been decided, or a conflict detected. + */ +static +bool mcsat_decide(mcsat_solver_t* mcsat) { assert(!mcsat->trail->inconsistent); + ivector_t skipped_variables; // Variables we took from the queue but plugin didn't decide + init_ivector(&skipped_variables, 0); + + variable_t var; + bool aux_choice; // indicates that var was not taken from the queue bool force_decision = false; + double rand_freq = mcsat->heuristic_params.random_decision_freq; + while (true) { var = variable_null; + aux_choice = true; // Us the top variables first - for (i = 0; i < mcsat->top_decision_vars.size; ++i) { + for (uint32_t i = 0; i < mcsat->top_decision_vars.size; ++i) { var = mcsat->top_decision_vars.data[i]; assert(var != variable_null); if (!trail_has_value(mcsat->trail, var)) { - force_decision = true; break; } var = variable_null; @@ -2376,7 +2435,6 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { var = int_queue_pop(&mcsat->hinted_decision_vars); assert(var != variable_null); if (!trail_has_value(mcsat->trail, var)) { - force_decision = true; break; } var = variable_null; @@ -2390,13 +2448,13 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { FILE* out = trace_out(mcsat->ctx->trace); fprintf(out, "mcsat_decide(): var_order is "); - for (i = 0; i < order->size; ++ i) { + for (uint32_t i = 0; i < order->size; ++ i) { term_print_to_file(out, mcsat->ctx->terms, order->data[i]); fprintf(out, " "); } fprintf(out, "\n"); } - for (i = 0; var == variable_null && i < order->size; ++i) { + for (uint32_t i = 0; var == variable_null && i < order->size; ++i) { term_t ovar_term = order->data[i]; variable_t ovar = variable_db_get_variable_if_exists(mcsat->var_db, ovar_term); if (ovar == variable_null) continue; // Some variables are not used @@ -2408,21 +2466,22 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { } } - // Random decision: - if (var == variable_null && mcsat->heuristic_params.random_decision_freq > 0.0) { + // Random decision + if (var == variable_null && rand_freq > 0.0) { double* seed = &mcsat->heuristic_params.random_decision_seed; - double freq = mcsat->heuristic_params.random_decision_freq; - if (drand(seed) < freq && !var_queue_is_empty(&mcsat->var_queue)) { + if (drand(seed) < rand_freq && !var_queue_is_empty(&mcsat->var_queue)) { var = var_queue_random(&mcsat->var_queue, seed); if (trail_has_value(mcsat->trail, var)) { var = variable_null; - } else { - // fprintf(stderr, "random\n"); - var_queue_remove(&mcsat->var_queue, var); } } } + if (var == variable_null) { + // No auxiliary choice performed + aux_choice = false; + } + // Use the queue while (!var_queue_is_empty(&mcsat->var_queue) && var == variable_null) { // Get the next variable from the queue @@ -2441,53 +2500,21 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { } if (var != variable_null) { - // Get the owner that will decide that value of the variable - i = mcsat->decision_makers[variable_db_get_type_kind(mcsat->var_db, var)]; - assert(i != MCSAT_MAX_PLUGINS); - // Construct the token - trail_token_construct(&decision_token, mcsat->plugins[i].plugin_ctx, var); - // Decide - if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { - mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): with %s\n", mcsat->plugins[i].plugin_name); - mcsat_trace_printf(mcsat->ctx->trace, "mcsat_decide(): variable "); - variable_db_print_variable(mcsat->var_db, var, trace_out(mcsat->ctx->trace)); - mcsat_trace_printf(mcsat->ctx->trace, "\n"); - } - plugin = mcsat->plugins[i].plugin; - - // Ask the owner to decide - mcsat_push_internal(mcsat); - assert(plugin->decide); - plugin->decide(plugin, var, (trail_token_t*) &decision_token, force_decision); - - if (decision_token.used == 0) { - // If not decided, remember and go on - ivector_push(&skipped_variables, var); - mcsat_pop_internal(mcsat); - } else { - // Decided, we can continue with the search - (*mcsat->solver_stats.decisions)++; - // If plugin decided to cheat by deciding on another variable, put it back - if (!trail_has_value(mcsat->trail, var)) { - var_queue_insert(&mcsat->var_queue, var); - } else { - if (trace_enabled(mcsat->ctx->trace, "mcsat::decide")) { - FILE* out = trace_out(mcsat->ctx->trace); - fprintf(out, "mcsat_decide(): value = "); - mcsat_value_print(trail_get_value(mcsat->trail, var), out); - fprintf(out, "\n"); - } - } + bool made_decision = mcsat_decide_var(mcsat, var, force_decision); + if (made_decision) { break; + } else if (!aux_choice) { + ivector_push(&skipped_variables, var); } } else { + assert(!aux_choice); // No variables left to decide if (skipped_variables.size == 0) { // Didn't skip any, we're done break; } else { // Put the skipped back in the queue, and continue but force next decision - for (i = 0; i < skipped_variables.size; ++ i) { + for (uint32_t i = 0; i < skipped_variables.size; ++ i) { var_queue_insert(&mcsat->var_queue, skipped_variables.data[i]); } ivector_reset(&skipped_variables); @@ -2502,7 +2529,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { // the decided score assert(var != variable_null); double var_score = var_queue_get_activity(&mcsat->var_queue, var); - for (i = 0; i < skipped_variables.size; ++ i) { + for (uint32_t i = 0; i < skipped_variables.size; ++ i) { variable_t skipped_var = skipped_variables.data[i]; var_queue_set_activity(&mcsat->var_queue, skipped_var, var_score); var_queue_insert(&mcsat->var_queue, skipped_var); @@ -2748,8 +2775,6 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin break; } - // remove all the hints - int_queue_reset(&mcsat->hinted_decision_vars); // update the variable selection heuristic var_queue_decay_activities(&mcsat->var_queue); } From 957843b6bf6fffbc69d541c6ea13c63d1d93bd0d Mon Sep 17 00:00:00 2001 From: Thomas Hader Date: Wed, 13 Mar 2024 15:58:43 -0700 Subject: [PATCH 23/23] Added force_decision for top_variables --- src/mcsat/solver.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index c4243e69d..05b175974 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -2424,6 +2424,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) { var = mcsat->top_decision_vars.data[i]; assert(var != variable_null); if (!trail_has_value(mcsat->trail, var)) { + force_decision = true; break; } var = variable_null;