Merge pull request #472 from SRI-CSL/mcsat-check-model-with-hint

Mcsat check model with hint API method

doc/sphinx/source/context-operations.rst

@@ -939,10 +939,11 @@ Check Modulo a Model and Model Interpolant
 
 When checking satisfiability, it is possible to provide a partial
 model such that the satisfiability is checked for the assertions in
-conjunction with the provided model. To use this functionality, the
-context must be a context initialized with support for MCSAT (see
-yices_new_context, yices_new_config, yices_set_config).
-Here is an example::
+conjunction with the provided model. Moreover, it is possible to
+provide hints as initial model guesses when mcsat decides a
+variable. To use this functionality, the context must be a context
+initialized with support for MCSAT (see yices_new_context,
+yices_new_config, yices_set_config).  Here is an example::
 
    ctx_config_t* config = yices_new_config();
    yices_set_config(config, "solver-type", "mcsat");
@@ -958,6 +959,23 @@ uninterpreted terms ``a[0]``, ..., ``a[4]``.  This amounts to checking
 the conjunction of ``f`` and the equalities between the unintpreted
 terms and their value in the ``model``.
 
+Here is an example of checking context with model and hint::
+
+   ctx_config_t* config = yices_new_config();
+   yices_set_config(config, "solver-type", "mcsat");
+   context_t *ctx = yices_new_context(config);
+   yices_assert_formula(ctx, f);
+   status = yices_check_context_with_model_and_hint(ctx, NULL, model, 5, a, 3);
+
+In this fragment, similar to the earlier one, we assert a formula
+``f``.  In the call to check on the last line, we give an array of
+five uninterpreted terms ``a[0]``, ..., ``a[4]``.  However, this time
+we would be checking the conjunction of ``f`` and the equalities
+between the first three (the number is given as the last argument)
+unintpreted terms and their value in the ``model``. The remaining two
+terms and their values will be provided as hints to the internal mcsat
+decide method.
+
 The check modulo a model provides an additional functionality, namely,
 the construction of a model interpolant, if the yices context is
 unsatisfiable and supports model interpolation (see
@@ -1013,6 +1031,79 @@ yices_set_config). This model interpolant is constructed by calling
    - If *ctx*'s status is anything else, the function returns :c:enum:`STATUS_ERROR`.
 
 
+   This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is
+   configured for one-shot solving and *ctx*'s status is anything
+   other than :c:enum:`STATUS_IDLE`.
+
+   **Error report**
+
+   - If one of the terms *t[i]* is not an uninterpreted:
+
+     -- error code: :c:enum:`MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED`
+
+   - If the context does not have the MCSAT solver enabled:
+
+     -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED`
+
+   - If the resulting status is :c:enum:`STATUS_SAT` and context does not support multichecks:
+
+     -- error code: :c:enum:`CTX_OPERATION_NOT_SUPPORTED`
+
+
+.. c:function:: smt_status_t yices_check_context_with_model_and_hint(context_t* ctx, const param_t* params, model_t *mdl, uint32_t n, const term_t t[], uint32_t m)
+
+   Checks whether *n* assumptions are satisfiable in a context *ctx*.
+
+   **Parameters**
+
+   - *ctx* is a context
+
+   - *params* is an optional structure to a search-parameter structure.
+
+   - *mdl* is a model
+
+   - *n* is the number of terms in *t*
+
+   - *t* is an array of *n* uninterpreted terms
+
+   - *m* is the number of terms 
+
+   The *params* structure controls search heuristics. If *params* is NULL, default
+   settings are used. See :ref:`params` and :c:func:`yices_check_context`.
+
+   This function checks statisfiability of the constraints in ctx
+   conjoined with a conjunction of equalities defined by *t[i]* and the
+   model, namely,
+
+   *t[0] == v_0 /\ .... /\ t[n-1] = v_{m-1}*,
+
+   and the remaining n-m terms in t are provided with hints from the model, i.e.
+ 
+   *t[m], ... , t[n-1]* will be given *v_{m}, ... , v_{n-1}* values when deciding
+
+   where *v_i* is the value of *t[i]* in *mdl*.
+
+   NOTE: if *t[i]* does not have a value in *mdl*, then a default value is
+   picked for *v_i*.
+
+   If this function returns STATUS_UNSAT and the context supports
+   model interpolation, then one can construct a model interpolant by
+   calling function :c:func:`yices_get_model_interpolant`.
+
+   More precisely:
+
+   - If *ctx*'s current status is :c:enum:`STATUS_UNSAT` then the function does nothing
+     and returns :c:enum:`STATUS_UNSAT`.
+
+   - If *ctx*'s status is :c:enum:`STATUS_IDLE`, :c:enum:`STATUS_SAT`,
+     or :c:enum:`STATUS_UNKNOWN` then the function checks whether
+     *ctx* conjoined with the *n* equalities given by *mdl* and *t* is
+     satisfiable. This is done even if *n* is zero.  The function will
+     then return a code as in :c:func:`yices_check_context`.
+
+   - If *ctx*'s status is anything else, the function returns :c:enum:`STATUS_ERROR`.
+
+
    This operation fails and returns :c:enum:`STATUS_ERROR` if *ctx* is
    configured for one-shot solving and *ctx*'s status is anything
    other than :c:enum:`STATUS_IDLE`.
@@ -1045,7 +1136,9 @@ yices_set_config). This model interpolant is constructed by calling
    Otherwise, it sets an error code and return NULL_TERM.
 
    This is intended to be used after a call to
-   :c:func:`yices_check_context_with_model` that returned
+   :c:func:`yices_check_context_with_model` or
+   :c:func:`yices_check_context_with_model_and_hint`
+   that returned
    :c:enum:`STATUS_UNSAT`. In this case, the function builds an model
    interpolant. The model interpolant is a clause implied by the
    current context that is false in the model provides to

src/api/yices_api.c

@@ -9240,6 +9240,85 @@ EXPORTED smt_status_t yices_check_context_with_model(context_t *ctx, const param
 }
 
 
+/*
+ * Check context with model and hint
+ * - param = parameter for check sat (or NULL for default parameters)
+ * - mdl = a model
+ * - t = array of n variables or uninterpred terms
+ * - m = number of terms that are asserted to be equal to their model values,
+ *       the remaining are treated as hints
+ *
+ * This checks ctx /\ t[0] = val(mdl, t[0]) /\ .... /\ t[m-1] = val(mdl, t[m-1])
+ */
+EXPORTED smt_status_t yices_check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m) {
+
+  param_t default_params;
+  smt_status_t stat;
+
+  if (! context_has_mcsat(ctx)) {
+    set_error_code(CTX_OPERATION_NOT_SUPPORTED);
+    return STATUS_ERROR;
+  }
+
+  if (! good_terms_for_check_with_model(n, t)) {
+    // this sets the error code already (to VARIABLE_REQUIRED)
+    // but Dejan created another error code that means the same thing here.
+    set_error_code(MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED);
+    return STATUS_ERROR;
+  }
+
+  assert(m <= n);
+
+  // cleanup
+  switch (context_status(ctx)) {
+  case STATUS_UNKNOWN:
+  case STATUS_SAT:
+    if (! context_supports_multichecks(ctx)) {
+      set_error_code(CTX_OPERATION_NOT_SUPPORTED);
+      return STATUS_ERROR;
+    }
+    context_clear(ctx);
+    break;
+
+  case STATUS_IDLE:
+    break;
+
+  case STATUS_UNSAT:
+    context_clear_unsat(ctx);
+    if (context_status(ctx) == STATUS_UNSAT) {
+      return STATUS_UNSAT;
+    }
+    break;
+
+  case STATUS_SEARCHING:
+  case YICES_STATUS_INTERRUPTED:
+    set_error_code(CTX_INVALID_OPERATION);
+    return STATUS_ERROR;
+
+  case STATUS_ERROR:
+  default:
+    set_error_code(INTERNAL_EXCEPTION);
+    return STATUS_ERROR;
+  }
+
+  assert(context_status(ctx) == STATUS_IDLE);
+
+  // set parameters
+  if (params == NULL) {
+    yices_default_params_for_context(ctx, &default_params);
+    params = &default_params;
+  }
+
+  // call check
+  stat = check_context_with_model_and_hint(ctx, params, mdl, n, t, m);
+  if (stat == YICES_STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
+    context_cleanup(ctx);
+  }
+
+  return stat;
+}
+
+
 
 /*
  * CHECK SAT AND COMPUTE INTERPOLANT

src/context/context.h

@@ -242,6 +242,24 @@ extern smt_status_t check_context_with_assumptions(context_t *ctx, const param_t
 extern smt_status_t check_context_with_model(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[]);
 
 
+/*
+ * Check satisfiability under model with hint: check whether the assertions stored in ctx
+ * conjoined with the assignment that the model gives to t is satisfiable.
+ *
+ * - params is an optional structure to store heuristic parameters
+ * - if params is NULL, default parameter settings are used.
+ * - model = model to assume
+ * - t = variables to use from the model (size = n)
+ * - m = number of terms in t to be used as assumption
+ *
+ * return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
+ * YICES_STATUS_INTERRUPTED
+ *
+ * If status is STATUS_UNSAT then the context and model are inconsistent
+ */
+extern smt_status_t check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m);
+
+
 /*
  * Build a model: the context's status must be STATUS_SAT or STATUS_UNKNOWN
  * - model must be initialized (and empty)

src/context/context_solver.c

@@ -633,6 +633,18 @@ smt_status_t check_context_with_model(context_t *ctx, const param_t *params, mod
   return stat;
 }
 
+/*
+ * Check with given model and hints
+ * - set the model hint and call check_context_with_model
+ */
+smt_status_t check_context_with_model_and_hint(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[], uint32_t m) {
+  assert(m <= n);
+
+  mcsat_set_model_hint(ctx->mcsat, mdl, n, t);
+
+  return check_context_with_model(ctx, params, mdl, m, t);
+}
+
 
 /*
  * Precheck: force generation of clauses and other stuff that's

src/include/yices.h

@@ -3196,7 +3196,7 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte
  * This function checks statisfiability of the constraints in ctx conjoined with
  * a conjunction of equalities defined by t[i] and the model, namely,
  *
- *    t[0] == v_0 /\ .... /\ t[n-1] = v_{n-1}
+ *    t[0] = v_0 /\ .... /\ t[n-1] = v_{n-1}
  *
  * where v_i is the value of t[i] in mdl.
  *
@@ -3223,6 +3223,58 @@ __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_assumptions(conte
 __YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model(context_t *ctx, const param_t *params,
 								     model_t *mdl, uint32_t n, const term_t t[]);
 
+/*
+ * Check satisfiability modulo a model and hints.
+ *
+ * Check whether the assertions stored in ctx conjoined with a model are satisfiable.
+ * - ctx must be a context initialized with support for MCSAT
+ *   (see yices_new_context, yices_new_config, yices_set_config).
+ * - params is an optional structure to store heuristic parameters
+ *   if params is NULL, default parameter settings are used.
+ * - mdl is a model
+ * - t is an array of n terms
+ * - the terms t[0] ... t[n-1] must all be uninterpreted terms
+ *
+ * This function checks statisfiability of the constraints in ctx
+ * conjoined with a conjunction of equalities defined by first m terms
+ * in t and their model values, namely,
+ *
+ *    t[0] = v_0 /\ .... /\ t[m-1] = v_{m-1}
+ *
+ * and the remaining n-m terms in t are provided with hints from the
+ * model, i.e.
+ *
+ *    t[m], ... , t[n-1] will be given v_{m}, ... , v_{n-1} values when deciding
+ *
+ * where v_i is the value of t[i] in mdl.
+ *
+ * NOTE: if t[i] does not have a value in mdl, then a default value is picked for v_i.
+ *
+ * If this function returns STATUS_UNSAT and the context supports
+ * model interpolation, then one can construct a model interpolant by
+ * calling function yices_get_model_interpolant.
+ *
+ * Error codes:
+ *
+ * if one of the terms t[i] is not an uninterpreted term
+ *   code = MCSAT_ERROR_ASSUMPTION_TERM_NOT_SUPPORTED
+ *
+ * If the context does not have the MCSAT solver enabled
+ *   code = CTX_OPERATION_NOT_SUPPORTED
+ *
+ * If the resulting status is STATUS_SAT and context does not support multichecks
+ *   code = CTX_OPERATION_NOT_SUPPORTED
+ *
+ *
+ * Since 2.6.4.
+ */
+__YICES_DLLSPEC__ extern smt_status_t yices_check_context_with_model_and_hint(context_t *ctx,
+									      const param_t *params,
+									      model_t *mdl,
+									      uint32_t n,
+									      const term_t t[],
+									      uint32_t m);
+
 /*
  * Check satisfiability and compute interpolant.
  *

src/mcsat/no_mcsat.c

@@ -54,6 +54,9 @@ int32_t mcsat_assert_formulas(mcsat_solver_t *mcsat, uint32_t n, const term_t *f
   return 0;
 }
 
+void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_filter, const term_t mdl_filter[]) {
+}
+
 void mcsat_solve(mcsat_solver_t *mcsat, const param_t *params, model_t* mdl, uint32_t n, const term_t t[]) {
 }
 

src/mcsat/solver.c

@@ -2522,6 +2522,42 @@ void mcsat_check_model(mcsat_solver_t* mcsat, bool assert) {
 static
 void mcsat_assert_formulas_internal(mcsat_solver_t* mcsat, uint32_t n, const term_t *f, bool preprocess);
 
+void mcsat_set_model_hint(mcsat_solver_t* mcsat, model_t* mdl, uint32_t n_mdl_filter,
+			  const term_t mdl_filter[]) {
+  if (n_mdl_filter == 0) {
+    return;
+  }
+
+  assert(mdl != NULL);
+  assert(mdl_filter != NULL);
+
+  value_table_t* vtbl = model_get_vtbl(mdl);
+
+  mcsat_push(mcsat);
+
+  uint32_t i;
+  for (i = 0; i < n_mdl_filter; ++i) {
+    term_t x = mdl_filter[i];
+    assert(term_kind(mcsat->terms, x) == UNINTERPRETED_TERM || term_kind(mcsat->terms, x) == VARIABLE);
+    assert(is_pos_term(x));
+
+    variable_t x_var = variable_db_get_variable(mcsat->var_db, unsigned_term(x));
+    if (trail_has_value(mcsat->trail, x_var)) {
+      continue;
+    }
+
+    uint32_t plugin_i = mcsat->decision_makers[variable_db_get_type_kind(mcsat->var_db, x_var)];
+    value_t x_value = model_get_term_value(mdl, x);
+    mcsat_value_t value;
+    mcsat_value_construct_from_value(&value, vtbl, x_value);
+    assert(x_value >= 0);
+    trail_add_propagation(mcsat->trail, x_var, &value, plugin_i, mcsat->trail->decision_level);
+    mcsat_value_destruct(&value);
+  }
+
+  mcsat_pop(mcsat);
+}
+
 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;

src/mcsat/solver.h

@@ -75,6 +75,14 @@ void mcsat_pop(mcsat_solver_t* mcsat);
  */
 int32_t mcsat_assert_formulas(mcsat_solver_t *mcsat, uint32_t n, const term_t *f);
 
+/*
+ * Set model hint.
+ *
+ * @param mdl the model to use.
+ * @param mdl_filter part of the model to use.
+ */
+void mcsat_set_model_hint(mcsat_solver_t *mcsat, model_t* mdl, uint32_t n, const term_t mdl_filter[]);
+
 /*
  * Solve asserted constraints module given model.
  *