also enable nra learning when using interpolation mode (#509)

* also enable nra learning when using interpolation mode

* test with interpolation option on

* add method to provide value hint

* minor: use trace printing methods

* add comments

* format

src/mcsat/nra/nra_plugin.c

@@ -2158,17 +2158,13 @@ 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 = ");
+      if (constraint_value != NULL) {
+        mcsat_value_print(constraint_value, ctx_trace_out(nra->ctx));
+      } else {
+        ctx_trace_printf(nra->ctx, "no value");
       }
     }
     if (constraint_value != NULL) {
@@ -2181,7 +2177,16 @@ 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);
+          // update the trail value cache
+          nra->ctx->hint_value(nra->ctx, constraint_var, constraint_value);
+        }
       }
     }
   }

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 */

src/mcsat/solver.c

@@ -707,6 +707,22 @@ 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);
+  }
+}
+
 static
 void mcsat_plugin_context_decision_calls(plugin_context_t* self, type_kind_t type) {
   mcsat_plugin_context_t* mctx;
@@ -738,6 +754,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;
 }

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)

tests/regress/mcsat/nra/hong_19.smt2.gold

@@ -0,0 +1 @@
+unsat