From 0dc69eb4b87860982681b77db630241ce4643643 Mon Sep 17 00:00:00 2001 From: Ahmed <43099566+ahmed-irfan@users.noreply.github.com> Date: Mon, 27 Nov 2023 14:08:30 -0800 Subject: [PATCH] add more info in the doc --- doc/sphinx/source/context-operations.rst | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/doc/sphinx/source/context-operations.rst b/doc/sphinx/source/context-operations.rst index 0fce6c5d0..72ea93e27 100644 --- a/doc/sphinx/source/context-operations.rst +++ b/doc/sphinx/source/context-operations.rst @@ -1212,7 +1212,11 @@ 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 this operation will overwrite any previously set ordering. +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)