From 3b6c9ba696d40d5519435e3bc8c33e690f4b41df Mon Sep 17 00:00:00 2001
From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com>
Date: Fri, 17 Nov 2023 18:06:17 -0800
Subject: [PATCH] new api method for setting variable order

---
 src/api/yices_api.c | 22 ++++++++++++++++++++++
 src/include/yices.h | 22 +++++++++++++++++++++-
 2 files changed, 43 insertions(+), 1 deletion(-)

diff --git a/src/api/yices_api.c b/src/api/yices_api.c
index 13be62ee5..e9267d457 100644
--- a/src/api/yices_api.c
+++ b/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;
+  }
+
+  ivector_t *order = &ctx->mcsat_var_order;
+  ivector_reset(order);
+
+  uint32_t i;
+  for (i = 0; i < n; ++i) {
+    ivector_push(order, t[i]);
+  }
+
+  return STATUS_IDLE;
+}
 
 
 /*
diff --git a/src/include/yices.h b/src/include/yices.h
index c8e0b9a6f..aea0b62e5 100644
--- a/src/include/yices.h
+++ b/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.
  *