Mcsat set initial var order api (#500)

* new api method

* rename api method

* update documentation

* fix doc

doc/sphinx/source/context-operations.rst

@@ -1207,20 +1207,54 @@ as follows::
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 
 
-Set Variable Ordering for MCSat
--------------------------------
+Set a Fixed Variable Ordering for MCSat
+---------------------------------------
 
-It is possible to give a variable ordering for the MCSat search --
+It is possible to give a fixed variable ordering for the MCSat search --
 this will make MCSAT to decide the variables in the given order. Note
 that the variables in the given ordering are always decided earlier
 than the ones not in the ordering. Therefore, the ordering variables
 are not affected by the dynamic variable decision heuristic like
 VSIDS. Moreover, a subsequent calls to this operation will overwrite
 previously set ordering.
 
-.. c:function:: smt_status_t yices_mcsat_set_var_order(context_t *ctx, const term_t t[], uint32_t n)
+.. c:function:: smt_status_t yices_mcsat_set_fixed_var_order(context_t *ctx, uint32_t n, const term_t t[])
 
-   Set the variable ordering for the MCSat search.
+   Set a fixed variable ordering for the MCSat search.
+
+   **Parameters**
+
+   - *ctx* is a context
+
+   - *t* is an array of variables
+
+   - *n* is the size of the *t* array
+
+   If the operation fails, it will return :c:enum:`STATUS_ERROR`,
+   otherwise it returns :c:enum:`STATUS_IDLE`.
+
+   **Error report**
+
+   - If the context is not configured for MCSat:
+
+     -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED`
+
+   - If the terms in the *t* array are not variables:
+
+     -- error code: :c:enum:`VARIABLE_REQUIRED`
+
+
+Set a Initial Variable Ordering for MCSat
+-----------------------------------------
+
+It is also possible to give a variable ordering that will be used only
+in the beginning of the MCSAT search -- once that order has been
+decided, MCSAT can choose according to its heuristics from that point
+onward. 
+
+.. c:function:: smt_status_t yices_mcsat_set_initial_var_order(context_t *ctx, uint32_t n, const term_t t[])
+
+   Set an initial variable ordering for the MCSat search.
 
    **Parameters**
 

src/api/yices_api.c

@@ -9319,11 +9319,11 @@ EXPORTED smt_status_t yices_check_context_with_model_and_hint(context_t *ctx, co
 }
 
 /*
- * Set variable ordering for making mcsat decisions.
+ * Set a fixed variable ordering for making mcsat decisions.
  *
  * NOTE: This will overwrite the previously set ordering.
  */
-EXPORTED smt_status_t yices_mcsat_set_var_order(context_t *ctx, uint32_t n, const term_t t[]) {
+EXPORTED smt_status_t yices_mcsat_set_fixed_var_order(context_t *ctx, uint32_t n, const term_t t[]) {
 
   if (! context_has_mcsat(ctx)) {
     set_error_code(CTX_OPERATION_NOT_SUPPORTED);
@@ -9341,6 +9341,27 @@ EXPORTED smt_status_t yices_mcsat_set_var_order(context_t *ctx, uint32_t n, cons
   return STATUS_IDLE;
 }
 
+/*
+ * Set an initial variable ordering for making mcsat decisions.
+ *
+ */
+EXPORTED smt_status_t yices_mcsat_set_initial_var_order(context_t *ctx, uint32_t n, const term_t t[]) {
+
+  if (! context_has_mcsat(ctx)) {
+    set_error_code(CTX_OPERATION_NOT_SUPPORTED);
+    return STATUS_ERROR;
+  }
+
+  if (! good_terms_for_check_with_model(n, t)) {
+    set_error_code(VARIABLE_REQUIRED);
+    return STATUS_ERROR;
+  }
+
+  ivector_t *order = &ctx->mcsat_initial_var_order;
+  ivector_copy(order, t, n);
+
+  return STATUS_IDLE;
+}
 
 /*
  * CHECK SAT AND COMPUTE INTERPOLANT

src/context/context.c

@@ -5715,6 +5715,7 @@ void init_context(context_t *ctx, term_table_t *terms, smt_logic_t logic,
   // mcsat options default
   init_mcsat_options(&ctx->mcsat_options);
   init_ivector(&ctx->mcsat_var_order, CTX_DEFAULT_VECTOR_SIZE);
+  init_ivector(&ctx->mcsat_initial_var_order, CTX_DEFAULT_VECTOR_SIZE);
   /*
    * Allocate and initialize the solvers and core
    * NOTE: no theory solver yet if arch is AUTO_IDL or AUTO_RDL
@@ -5774,6 +5775,7 @@ void delete_context(context_t *ctx) {
   delete_gate_manager(&ctx->gate_manager);
   /* delete_mcsat_options(&ctx->mcsat_options); // if used then the same memory is freed twice */
   delete_ivector(&ctx->mcsat_var_order);
+  delete_ivector(&ctx->mcsat_initial_var_order);
 
   delete_intern_tbl(&ctx->intern);
   delete_ivector(&ctx->top_eqs);

src/context/context_types.h

@@ -727,8 +727,10 @@ struct context_s {
 
   // options for the mcsat solver
   mcsat_options_t mcsat_options;
-  // ordering for forcing mcsat assignment order
+  // fixed ordering for forcing mcsat assignment order
   ivector_t mcsat_var_order;
+  // initial ordering for forcing mcsat assignment order
+  ivector_t mcsat_initial_var_order;
 
   // flag for enabling adding quant instances
   bool en_quant;

src/include/yices.h

@@ -3276,7 +3276,8 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model_and_hint(co
 									      uint32_t m);
 
 /*
- * Set variable ordering for making mcsat decisions.
+ * Set a fixed variable ordering for making mcsat decisions. MCSAT
+ * will always first decide these variables in the given order.
  *
  * - ctx must be a context initialized with support for MCSAT
  *   (see yices_new_context, yices_new_config, yices_set_config).
@@ -3291,9 +3292,29 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model_and_hint(co
  * If the context does not have the MCSAT solver enabled
  *   code = CTX_OPERATION_NOT_SUPPORTED
  */
-__YICES_DLLSPEC__ extern smt_status_t yices_mcsat_set_var_order(context_t *ctx,
-                                                                uint32_t n,
-								const term_t t[]);
+__YICES_DLLSPEC__ extern smt_status_t yices_mcsat_set_fixed_var_order(context_t *ctx,
+                                                                      uint32_t n,
+								      const term_t t[]);
+
+/*
+ * Set initial variable ordering for making mcsat decisions. This is
+ * one-time ordering that is done initially in the MCSAT search.
+ *
+ * - ctx must be a context initialized with support for MCSAT
+ *   (see yices_new_context, yices_new_config, yices_set_config).
+ * - t is an array of n terms
+ *
+ *
+ * Returns STATUS_ERROR if mcsat context is not enabled, otherwise returns STATUS_IDLE
+ *
+ * Error codes:
+ *
+ * If the context does not have the MCSAT solver enabled
+ *   code = CTX_OPERATION_NOT_SUPPORTED
+ */
+__YICES_DLLSPEC__ extern smt_status_t yices_mcsat_set_initial_var_order(context_t *ctx,
+                                                                        uint32_t n,
+                                                                        const term_t t[]);
 
 /*
  * Check satisfiability and compute interpolant.

src/mcsat/solver.c

@@ -2419,7 +2419,7 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
     var = variable_null;
     aux_choice = true;
 
-    // Us the top variables first
+    // Use the top variables first
     for (uint32_t i = 0; i < mcsat->top_decision_vars.size; ++i) {
       var = mcsat->top_decision_vars.data[i];
       assert(var != variable_null);
@@ -2430,19 +2430,7 @@ 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 there is a fixed order that was passed in, try that
     if (var == variable_null) {
       const ivector_t* order = &mcsat->ctx->mcsat_var_order;
       if (order->size > 0) {
@@ -2467,6 +2455,18 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
       }
     }
 
+    // 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;
+      }
+    }
+
     // Random decision
     if (var == variable_null && rand_freq > 0.0) {
       double* seed = &mcsat->heuristic_params.random_decision_seed;
@@ -2630,6 +2630,24 @@ void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_fi
   mcsat_pop(mcsat);
 }
 
+static
+void mcsat_set_initial_var_order(mcsat_solver_t* mcsat) {
+  const ivector_t* vars = &mcsat->ctx->mcsat_initial_var_order;
+  uint32_t n = vars->size;
+  if (n == 0) {
+    return;
+  }
+
+  assert(vars != NULL);
+
+  uint32_t i;
+  for (i = 0; i < n; ++n) {
+    term_t x = vars->data[i];
+    variable_t v = variable_db_get_variable(mcsat->var_db, unsigned_term(x));
+    int_queue_push(&mcsat->hinted_decision_vars, v);
+  }
+}
+
 void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uint32_t n_assumptions, const term_t assumptions[]) {
 
   uint32_t restart_resource;
@@ -2691,6 +2709,9 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params, model_t* mdl, uin
   mcsat_heuristics_init(mcsat);
   mcsat_notify_plugins(mcsat, MCSAT_SOLVER_START);
 
+  // set initial variable order
+  mcsat_set_initial_var_order(mcsat);
+
   // Initialize the Luby sequence with interval 10
   restart_resource = 0;
   luby_init(&luby, mcsat->heuristic_params.restart_interval);

tests/api/test_mcsat_set_var_order.c

@@ -35,7 +35,7 @@ int main(void)
   term_t order_vars[2];
   order_vars[0] = y;
   order_vars[1] = x;
-  yices_mcsat_set_var_order(ctx, 2, order_vars);
+  yices_mcsat_set_fixed_var_order(ctx, 2, order_vars);
 
   // model hint
   model_t* mdl = yices_new_model();