Mcsat api var order (#478)

* moving var_order vector from mcsat_options to context

* new api method for setting variable order

* mcsat-set-var-order test

* minor

* fix registration-queue error in mcsat-model-hint

* fix warnings

* enable Werror in CI

* one more warning fix

* Update test_model_hint.c

* check good vars

* api text -- to be checked with sphinx, which is not running with brew

* add more info in the doc

doc/sphinx/source/context-operations.rst

@@ -1207,6 +1207,43 @@ as follows::
      -- error code: :c:enum:`CTX_INVALID_OPERATION`
 
 
+Set Variable Ordering for MCSat
+-------------------------------
+
+It is possible to give a 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)
+
+   Set the 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`
+
+
 .. _params:
 
 Search Parameters

src/api/yices_api.c

@@ -9318,6 +9318,28 @@ EXPORTED smt_status_t yices_check_context_with_model_and_hint(context_t *ctx, co
   return stat;
 }
 
+/*
+ * Set 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, const term_t t[], uint32_t n) {
+
+  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_var_order;
+  ivector_copy(order, t, n);
+
+  return STATUS_IDLE;
+}
 
 
 /*

src/context/context.c

@@ -5714,7 +5714,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);
   /*
    * Allocate and initialize the solvers and core
    * NOTE: no theory solver yet if arch is AUTO_IDL or AUTO_RDL
@@ -5773,6 +5773,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_intern_tbl(&ctx->intern);
   delete_ivector(&ctx->top_eqs);

src/context/context_types.h

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

src/frontend/smt2/smt2_commands.c

@@ -2620,6 +2620,7 @@ static void init_smt2_context(smt2_globals_t *g) {
 
   // Set the mcsat options
   g->ctx->mcsat_options = g->mcsat_options;
+  ivector_copy(&g->ctx->mcsat_var_order, g->var_order.data, g->var_order.size);
 
   /*
    * TODO: override the default context options based on
@@ -5343,7 +5344,7 @@ static bool yices_get_option(smt2_globals_t *g, yices_param_t p) {
     break;
 
   case PARAM_MCSAT_VAR_ORDER:
-    print_terms_value(g,g->mcsat_options.var_order);
+    print_terms_value(g, &g->var_order);
     break;
 
   case PARAM_UNKNOWN:
@@ -6125,10 +6126,9 @@ static void yices_set_option(smt2_globals_t *g, const char *param, const param_v
 
   case PARAM_MCSAT_VAR_ORDER:
     if (param_val_to_terms(param, val, &terms, &reason)) {
-      g->mcsat_options.var_order = terms;
       context = g->ctx;
       if (context != NULL) {
-        context->mcsat_options.var_order = terms;
+        ivector_copy(&context->mcsat_var_order, terms->data, terms->size);
       }
     }
     break;

src/include/yices.h

@@ -3266,7 +3266,7 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t *
  *   code = CTX_OPERATION_NOT_SUPPORTED
  *
  *
- * Since 2.6.4.
+ * Since 2.7.0
  */
 __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model_and_hint(context_t *ctx,
 									      const param_t *params,
@@ -3275,6 +3275,26 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model_and_hint(co
 									      const term_t t[],
 									      uint32_t m);
 
+/*
+ * Set variable ordering for making mcsat decisions.
+ *
+ * - 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
+ *
+ * NOTE: This will overwrite the previously set ordering.
+ *
+ * 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_var_order(context_t *ctx,
+                                                                const term_t t[],
+                                                                uint32_t n);
+
 /*
  * Check satisfiability and compute interpolant.
  *

src/mcsat/options.c

@@ -27,7 +27,6 @@ extern void init_mcsat_options(mcsat_options_t *opts) {
   opts->nra_bound_min = -1;
   opts->nra_bound_max = -1;
   opts->bv_var_size = -1;
-  opts->var_order = NULL;
   opts->model_interpolation = false;
 }
 

src/mcsat/options.h

@@ -35,8 +35,6 @@ typedef struct mcsat_options_s {
   int32_t nra_bound_max;
   int32_t bv_var_size;
   bool model_interpolation;
-  // ordering for forcing assignment order
-  ivector_t* var_order;
 } mcsat_options_t;
 
 /** Initialize options with default values. */

src/mcsat/solver.c

@@ -2340,8 +2340,8 @@ bool mcsat_decide(mcsat_solver_t* mcsat) {
 
     // If there is an order that was passed in, try that
     if (var == variable_null) {
-      const ivector_t* order = mcsat->ctx->mcsat_options.var_order;
-      if (order != 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);

tests/api/test_mcsat_set_var_order.c

@@ -0,0 +1,70 @@
+#ifdef NDEBUG
+#undef NDEBUG
+#endif
+
+#include <stdlib.h>
+
+#include "assert.h"
+
+#include <yices.h>
+
+int main(void)
+{
+  if (! yices_has_mcsat()) {
+    return 1; // skipped
+  }
+  yices_init();
+
+  ctx_config_t* config = yices_new_config();
+  yices_default_config_for_logic(config, "QF_NIA");
+  context_t* ctx = yices_new_context(config);
+
+  term_t x = yices_new_uninterpreted_term(yices_int_type());
+  yices_set_term_name(x, "x");
+
+  term_t y = yices_new_uninterpreted_term(yices_int_type());
+  yices_set_term_name(y, "y");
+
+  assert(!yices_error_code());
+
+  // assertion
+  term_t a = yices_arith_gt_atom(x, yices_mul(y, y));
+  yices_assert_formula(ctx, a);
+
+  // variable order
+  term_t order_vars[2];
+  order_vars[0] = y;
+  order_vars[1] = x;
+  yices_mcsat_set_var_order(ctx, order_vars, 2);
+
+  // model hint
+  model_t* mdl = yices_new_model();
+  int32_t code;
+  code = yices_model_set_int32(mdl, y, 4);
+  if (code < 0) {
+    yices_print_error(stderr);
+    exit(1);
+  }
+
+  term_t vars[2];
+  vars[0] = y;
+  vars[1] = x;
+
+  smt_status_t status;
+  status = yices_check_context_with_model_and_hint(ctx, NULL,  mdl, 1, vars, 0);
+  assert(!yices_error_code());
+
+  assert(status == STATUS_SAT);
+
+  model_t* res_mdl = yices_get_model(ctx, 1);
+  // we should have decided y first and because of the hint its value should be 4
+  assert(yices_formula_true_in_model(res_mdl, yices_arith_eq_atom(y, yices_int32(4))));
+  // x value should be greater than 16 (because x > y*y and y is assigned 4)
+  assert(yices_formula_true_in_model(res_mdl, yices_arith_gt_atom(x, yices_int32(16))));
+
+  yices_free_model(mdl);
+  yices_free_context(ctx);
+  yices_exit();
+
+  return 0;
+}