From ac61fcef5e892b11c7800d29d17027e14cd2e643 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 17 Apr 2024 00:47:38 -0700 Subject: [PATCH 1/6] also enable nra learning when using interpolation mode --- src/mcsat/nra/nra_plugin.c | 29 +++++++++++++++++------------ 1 file changed, 17 insertions(+), 12 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 422c3a3f3..21e2f2e31 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -2158,18 +2158,16 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) { // Approximate the value const mcsat_value_t* constraint_value = NULL; - if (!nra->ctx->options->model_interpolation) { - constraint_value = poly_constraint_db_approximate(nra->constraint_db, constraint_var, nra); - if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) { - ctx_trace_printf(nra->ctx, "nra_plugin_learn(): value = "); - FILE* out = ctx_trace_out(nra->ctx); - if (constraint_value != NULL) { - mcsat_value_print(constraint_value, out); - } else { - fprintf(out, "no value"); - } - fprintf(out, "\n"); + constraint_value = poly_constraint_db_approximate(nra->constraint_db, constraint_var, nra); + if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) { + ctx_trace_printf(nra->ctx, "nra_plugin_learn(): value = "); + FILE* out = ctx_trace_out(nra->ctx); + if (constraint_value != NULL) { + mcsat_value_print(constraint_value, out); + } else { + fprintf(out, "no value"); } + fprintf(out, "\n"); } if (constraint_value != NULL) { if (has_value) { @@ -2181,7 +2179,14 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) { break; } } else { - prop->add(prop, constraint_var, constraint_value); + if (!nra->ctx->options->model_interpolation) { + prop->add(prop, constraint_var, constraint_value); + } else { + if (ctx_trace_enabled(nra->ctx, "nra::learn")) { + ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", constraint_var); + } + nra->ctx->hint_next_decision(nra->ctx, constraint_var); + } } } } From 4d0d854c9503121a35f104b667d0232a3f1ca0b9 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 17 Apr 2024 14:33:57 -0700 Subject: [PATCH 2/6] test with interpolation option on --- tests/regress/mcsat/nra/hong_19.smt2 | 43 +++++++++++++++++++++++ tests/regress/mcsat/nra/hong_19.smt2.gold | 1 + 2 files changed, 44 insertions(+) create mode 100644 tests/regress/mcsat/nra/hong_19.smt2 create mode 100644 tests/regress/mcsat/nra/hong_19.smt2.gold diff --git a/tests/regress/mcsat/nra/hong_19.smt2 b/tests/regress/mcsat/nra/hong_19.smt2 new file mode 100644 index 000000000..a0c03adde --- /dev/null +++ b/tests/regress/mcsat/nra/hong_19.smt2 @@ -0,0 +1,43 @@ +(set-option :produce-unsat-model-interpolants true) + +(set-info :smt-lib-version 2.6) +(set-logic QF_NRA) +(set-info :source |These benchmarks used in the paper: + + Dejan Jovanovic and Leonardo de Moura. Solving Non-Linear Arithmetic. + In IJCAR 2012, published as LNCS volume 7364, pp. 339--354. + +The hong family is a set of crafted benchmarks, a parametrized +generalization of the problem of Hong, sum x_i^2 < 1 and prod x_i > 1. +See: + + H. Hong. Comparison of several decision algorithms for the existential + theory of the reals. 1991. + +Submitted by Dejan Jovanvic for SMT-LIB. +|) +(set-info :category "crafted") +(set-info :status unsat) +(declare-fun x_0 () Real) +(declare-fun x_1 () Real) +(declare-fun x_2 () Real) +(declare-fun x_3 () Real) +(declare-fun x_4 () Real) +(declare-fun x_5 () Real) +(declare-fun x_6 () Real) +(declare-fun x_7 () Real) +(declare-fun x_8 () Real) +(declare-fun x_9 () Real) +(declare-fun x_10 () Real) +(declare-fun x_11 () Real) +(declare-fun x_12 () Real) +(declare-fun x_13 () Real) +(declare-fun x_14 () Real) +(declare-fun x_15 () Real) +(declare-fun x_16 () Real) +(declare-fun x_17 () Real) +(declare-fun x_18 () Real) +(assert (< (+ (* x_0 x_0) (+ (* x_1 x_1) (+ (* x_2 x_2) (+ (* x_3 x_3) (+ (* x_4 x_4) (+ (* x_5 x_5) (+ (* x_6 x_6) (+ (* x_7 x_7) (+ (* x_8 x_8) (+ (* x_9 x_9) (+ (* x_10 x_10) (+ (* x_11 x_11) (+ (* x_12 x_12) (+ (* x_13 x_13) (+ (* x_14 x_14) (+ (* x_15 x_15) (+ (* x_16 x_16) (+ (* x_17 x_17) (* x_18 x_18))))))))))))))))))) 1)) +(assert (> (* x_0 (* x_1 (* x_2 (* x_3 (* x_4 (* x_5 (* x_6 (* x_7 (* x_8 (* x_9 (* x_10 (* x_11 (* x_12 (* x_13 (* x_14 (* x_15 (* x_16 (* x_17 x_18)))))))))))))))))) 1)) +(check-sat) +(exit) diff --git a/tests/regress/mcsat/nra/hong_19.smt2.gold b/tests/regress/mcsat/nra/hong_19.smt2.gold new file mode 100644 index 000000000..3f65111b0 --- /dev/null +++ b/tests/regress/mcsat/nra/hong_19.smt2.gold @@ -0,0 +1 @@ +unsat From ed02b9d23a148d6d411ed5f1936a4e7704a6bdd7 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Wed, 17 Apr 2024 19:22:33 -0700 Subject: [PATCH 3/6] add method to provide value hint --- src/mcsat/nra/nra_plugin.c | 1 + src/mcsat/plugin.h | 3 +++ src/mcsat/solver.c | 10 ++++++++++ 3 files changed, 14 insertions(+) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 21e2f2e31..978ff374d 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -2186,6 +2186,7 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) { ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", constraint_var); } nra->ctx->hint_next_decision(nra->ctx, constraint_var); + nra->ctx->hint_value(nra->ctx, constraint_var, constraint_value); } } } diff --git a/src/mcsat/plugin.h b/src/mcsat/plugin.h index 685dbedce..88ceded83 100644 --- a/src/mcsat/plugin.h +++ b/src/mcsat/plugin.h @@ -116,6 +116,9 @@ struct plugin_context_s { /** Request a variable to be a next decision variable */ void (*hint_next_decision) (plugin_context_t* self, variable_t x); + /** Add model value hint in the value cache */ + void (*hint_value) (plugin_context_t* self, variable_t x, const mcsat_value_t* val); + }; /** Token to add entries to the trail */ diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index 51ba2fc98..c8fc0de45 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -707,6 +707,15 @@ void mcsat_plugin_context_hint_next_decision(plugin_context_t* self, variable_t mcsat_add_decision_hint(mctx->mcsat, x); } +static +void mcsat_plugin_context_hint_value(plugin_context_t* self, variable_t x, const mcsat_value_t* val) { + mcsat_plugin_context_t* mctx; + mctx = (mcsat_plugin_context_t*) self; + if (!trail_has_value(mctx->mcsat->trail, x)) { + mcsat_model_set_value(&mctx->mcsat->trail->model, x, val); + } +} + static void mcsat_plugin_context_decision_calls(plugin_context_t* self, type_kind_t type) { mcsat_plugin_context_t* mctx; @@ -738,6 +747,7 @@ void mcsat_plugin_context_construct(mcsat_plugin_context_t* ctx, mcsat_solver_t* 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->ctx.hint_value = mcsat_plugin_context_hint_value; ctx->mcsat = mcsat; ctx->plugin_name = plugin_name; } From ca1ee64a2c681789688b9b7e1492c9a06e25e07f Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Thu, 18 Apr 2024 10:06:54 -0700 Subject: [PATCH 4/6] minor: use trace printing methods --- src/mcsat/nra/nra_plugin.c | 6 ++---- 1 file changed, 2 insertions(+), 4 deletions(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 978ff374d..36dcea5d7 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -2161,13 +2161,11 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) { constraint_value = poly_constraint_db_approximate(nra->constraint_db, constraint_var, nra); if (ctx_trace_enabled(nra->ctx, "mcsat::nra::learn")) { ctx_trace_printf(nra->ctx, "nra_plugin_learn(): value = "); - FILE* out = ctx_trace_out(nra->ctx); if (constraint_value != NULL) { - mcsat_value_print(constraint_value, out); + mcsat_value_print(constraint_value, ctx_trace_out(nra->ctx)); } else { - fprintf(out, "no value"); + ctx_trace_printf(nra->ctx, "no value"); } - fprintf(out, "\n"); } if (constraint_value != NULL) { if (has_value) { From 607460d30f1d556e3efa5ae581ee91fa03ea549b Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Thu, 18 Apr 2024 10:14:50 -0700 Subject: [PATCH 5/6] add comments --- src/mcsat/nra/nra_plugin.c | 1 + src/mcsat/solver.c | 7 +++++++ 2 files changed, 8 insertions(+) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 36dcea5d7..19a434b77 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -2184,6 +2184,7 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) { ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", constraint_var); } nra->ctx->hint_next_decision(nra->ctx, constraint_var); + // update the trail value cache nra->ctx->hint_value(nra->ctx, constraint_var, constraint_value); } } diff --git a/src/mcsat/solver.c b/src/mcsat/solver.c index c8fc0de45..f03439e5a 100644 --- a/src/mcsat/solver.c +++ b/src/mcsat/solver.c @@ -707,11 +707,18 @@ void mcsat_plugin_context_hint_next_decision(plugin_context_t* self, variable_t mcsat_add_decision_hint(mctx->mcsat, x); } +/* + * Provide hint to the trail cache. + */ static void mcsat_plugin_context_hint_value(plugin_context_t* self, variable_t x, const mcsat_value_t* val) { mcsat_plugin_context_t* mctx; mctx = (mcsat_plugin_context_t*) self; + // update only if the x value is not set in the trail if (!trail_has_value(mctx->mcsat->trail, x)) { + // we set the value in the model of the trail. + // Remark: This is not making a decision in the trail. The model + // in the trail is used as a cache for unassigned variables. mcsat_model_set_value(&mctx->mcsat->trail->model, x, val); } } From 0053b30d6be213d123b249d7d2aabed38cb63df9 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Thu, 18 Apr 2024 10:15:21 -0700 Subject: [PATCH 6/6] format --- src/mcsat/nra/nra_plugin.c | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/mcsat/nra/nra_plugin.c b/src/mcsat/nra/nra_plugin.c index 19a434b77..fa0e990c1 100644 --- a/src/mcsat/nra/nra_plugin.c +++ b/src/mcsat/nra/nra_plugin.c @@ -2184,7 +2184,7 @@ void nra_plugin_learn(plugin_t* plugin, trail_token_t* prop) { ctx_trace_printf(nra->ctx, "nra: hinting variable = %d\n", constraint_var); } nra->ctx->hint_next_decision(nra->ctx, constraint_var); - // update the trail value cache + // update the trail value cache nra->ctx->hint_value(nra->ctx, constraint_var, constraint_value); } }