Merge e3d1482 into b0c8adb

.settings/language.settings.xml

@@ -0,0 +1,56 @@
+<?xml version="1.0" encoding="UTF-8" standalone="no"?>
+<project>
+
+    <configuration id="0.2076748749" name="debug">
+
+        <extension point="org.eclipse.cdt.core.LanguageSettingsProvider">
+
+            <provider copy-of="extension" id="org.eclipse.cdt.ui.UserLanguageSettingsProvider"/>
+
+            <provider-reference id="org.eclipse.cdt.core.ReferencedProjectsLanguageSettingsProvider" ref="shared-provider"/>
+
+            <provider class="org.eclipse.cdt.managedbuilder.language.settings.providers.GCCBuildCommandParser" id="org.eclipse.cdt.managedbuilder.core.GCCBuildCommandParser" keep-relative-paths="false" name="CDT GCC Build Output Parser" parameter="(g?cc)|([gc]\+\+)|(clang)" prefer-non-shared="true"/>
+
+            <provider class="org.eclipse.cdt.managedbuilder.language.settings.providers.GCCBuiltinSpecsDetector" console="false" env-hash="-1679152498045093462" id="org.eclipse.cdt.managedbuilder.core.GCCBuiltinSpecsDetector" keep-relative-paths="false" name="CDT GCC Built-in Compiler Settings" parameter="${COMMAND} ${FLAGS} -E -P -v -dD &quot;${INPUTS}&quot;" prefer-non-shared="true">
+
+                <language-scope id="org.eclipse.cdt.core.gcc"/>
+
+                <language-scope id="org.eclipse.cdt.core.g++"/>
+
+            </provider>
+
+            <provider-reference id="org.eclipse.cdt.managedbuilder.core.MBSLanguageSettingsProvider" ref="shared-provider"/>
+
+        </extension>
+
+    </configuration>
+
+    <configuration id="0.2076748749.1647107272" name="release">
+
+        <extension point="org.eclipse.cdt.core.LanguageSettingsProvider">
+
+            <provider copy-of="extension" id="org.eclipse.cdt.ui.UserLanguageSettingsProvider"/>
+
+            <provider-reference id="org.eclipse.cdt.core.ReferencedProjectsLanguageSettingsProvider" ref="shared-provider"/>
+
+            <provider-reference id="org.eclipse.cdt.managedbuilder.core.MBSLanguageSettingsProvider" ref="shared-provider"/>
+
+        </extension>
+
+    </configuration>
+
+    <configuration id="0.2076748749.1938501318" name="devel">
+
+        <extension point="org.eclipse.cdt.core.LanguageSettingsProvider">
+
+            <provider copy-of="extension" id="org.eclipse.cdt.ui.UserLanguageSettingsProvider"/>
+
+            <provider-reference id="org.eclipse.cdt.core.ReferencedProjectsLanguageSettingsProvider" ref="shared-provider"/>
+
+            <provider-reference id="org.eclipse.cdt.managedbuilder.core.MBSLanguageSettingsProvider" ref="shared-provider"/>
+
+        </extension>
+
+    </configuration>
+
+</project>

src/api/context_config.c

@@ -82,6 +82,7 @@ static const int32_t solver_code[NUM_SOLVER_CODES] = {
 typedef enum ctx_config_key {
   CTX_CONFIG_KEY_MODE,
   CTX_CONFIG_KEY_SOLVER_TYPE,
+  CTX_CONFIG_KEY_TRACE_TAGS,
   CTX_CONFIG_KEY_ARITH_FRAGMENT,
   CTX_CONFIG_KEY_UF_SOLVER,
   CTX_CONFIG_KEY_ARRAY_SOLVER,
@@ -99,6 +100,7 @@ static const char *const config_key_names[NUM_CONFIG_KEYS] = {
   "bv-solver",
   "mode",
   "solver-type",
+  "trace",
   "uf-solver",
 };
 
@@ -109,6 +111,7 @@ static const int32_t config_key[NUM_CONFIG_KEYS] = {
   CTX_CONFIG_KEY_BV_SOLVER,
   CTX_CONFIG_KEY_MODE,
   CTX_CONFIG_KEY_SOLVER_TYPE,
+  CTX_CONFIG_KEY_TRACE_TAGS,
   CTX_CONFIG_KEY_UF_SOLVER,
 };
 
@@ -241,6 +244,7 @@ static const ctx_config_t default_config = {
   CTX_CONFIG_DEFAULT,     // bv
   CTX_CONFIG_DEFAULT,     // arith
   ARITH_LIRA,             // fragment
+  NULL,                   // trace tags
 };
 
 
@@ -360,6 +364,10 @@ int32_t config_set_field(ctx_config_t *config, const char *key, const char *valu
     }
     break;
 
+  case CTX_CONFIG_KEY_TRACE_TAGS:
+    config->trace_tags = strdup(value);
+    break;
+
   case CTX_CONFIG_KEY_ARITH_FRAGMENT:
     arith = arith_fragment_code(value);
     if (arith == ARITH_NONE) {

src/api/context_config.h

@@ -105,6 +105,7 @@ struct ctx_config_s {
   solver_code_t         bv_config;
   solver_code_t         arith_config;
   arith_fragment_t      arith_fragment;
+  char*                 trace_tags;
 };
 
 

src/api/yices_api.c

@@ -8290,7 +8290,25 @@ context_t *_o_yices_new_context(const ctx_config_t *config) {
     }
   }
 
-  return _o_yices_create_context(logic, arch, mode, iflag, qflag);
+  context_t* ctx = _o_yices_create_context(logic, arch, mode, iflag, qflag);
+
+  if (config->trace_tags != NULL) {
+    // Make new trace
+    tracer_t *trace = (tracer_t*) safe_malloc(sizeof(tracer_t));
+    init_trace(trace);
+    set_trace_file(trace, stderr);
+    // Copy over the trace tag to the tracer
+    char *saveptr = NULL;
+    char *tag = strtok_r(config->trace_tags, ",", &saveptr);
+    while (tag != NULL) {
+      pvector_push(&trace->trace_tags, tag);
+      tag = strtok_r(NULL, ",", &saveptr);
+    }
+    // Set it to the context
+    context_set_trace(ctx, trace);
+  }
+
+  return ctx;
 }
 
 
@@ -8993,6 +9011,96 @@ EXPORTED smt_status_t yices_check_context_with_assumptions(context_t *ctx, const
   return stat;
 }
 
+/*
+ * Check context with model
+ * - n = number of assumptions
+ * - a[0] ... a[n-1] = n assumptions. All of them must be Boolean terms.
+ */
+EXPORTED 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[]) {
+
+  param_t default_params;
+  smt_status_t stat;
+  uint32_t i;
+
+  // cleanup
+  switch (context_status(ctx)) {
+  case STATUS_UNKNOWN:
+  case STATUS_SAT:
+    if (! context_supports_multichecks(ctx)) {
+      error_report_t *error = get_yices_error();
+      error->code = CTX_OPERATION_NOT_SUPPORTED;
+      return STATUS_ERROR;
+    }
+    if (! context_has_mcsat(ctx)) {
+      error_report_t *error = get_yices_error();
+      error->code = CTX_OPERATION_NOT_SUPPORTED;
+      return STATUS_ERROR;
+    }
+    context_clear(ctx);
+    break;
+
+  case STATUS_IDLE:
+    break;
+
+  case STATUS_UNSAT:
+    if (!context_supports_multichecks(ctx)) {
+      error_report_t *error = get_yices_error();
+      error->code = CTX_OPERATION_NOT_SUPPORTED;
+      return STATUS_ERROR;
+    }
+    if (!context_has_mcsat(ctx)) {
+      error_report_t *error = get_yices_error();
+      error->code = CTX_OPERATION_NOT_SUPPORTED;
+      return STATUS_ERROR;
+    }
+    context_clear_unsat(ctx);
+    if (context_status(ctx) == STATUS_UNSAT) {
+      return STATUS_UNSAT;
+    }
+    break;
+
+  case STATUS_SEARCHING:
+  case STATUS_INTERRUPTED: {
+    error_report_t *error = get_yices_error();
+    error->code = CTX_INVALID_OPERATION;
+    return STATUS_ERROR;
+  }
+  case STATUS_ERROR:
+  default: {
+    error_report_t *error = get_yices_error();
+    error->code = INTERNAL_EXCEPTION;
+    return STATUS_ERROR;
+  }
+  }
+
+  assert(context_status(ctx) == STATUS_IDLE);
+
+  // Make sure only variables are allowed
+  for (i = 0; i < n; ++ i) {
+    bool is_variable = term_is_var_or_uninterpreted(ctx->terms, t[i]);
+    if (!is_variable) {
+      error_report_t *error = get_yices_error();
+      error->code = CTX_OPERATION_NOT_SUPPORTED;
+      return STATUS_ERROR;
+    }
+  }
+
+  // set parameters
+  if (params == NULL) {
+    yices_default_params_for_context(ctx, &default_params);
+    params = &default_params;
+  }
+
+  // call check
+  stat = check_context_with_model(ctx, params, mdl, n, t);
+  if (stat == STATUS_INTERRUPTED && context_supports_cleaninterrupt(ctx)) {
+    context_cleanup(ctx);
+  }
+
+  return stat;
+}
+
 
 /*
  * Interrupt the search:
@@ -9031,6 +9139,13 @@ EXPORTED int32_t yices_get_unsat_core(context_t *ctx, term_vector_t *v) {
   return 0;
 }
 
+/*
+ * Construct a model interpolant core.
+ */
+EXPORTED term_t yices_get_model_interpolant(context_t *ctx) {
+  return context_get_unsat_model_interpolant(ctx);
+}
+
 
 /************
  *  MODELS  *

src/context/context.c

@@ -6363,6 +6363,8 @@ void context_clear_unsat(context_t *ctx) {
   if (ctx->mcsat == NULL) {
     smt_clear_unsat(ctx->core);
     assert(smt_base_level(ctx->core) == ctx->base_level);
+  } else {
+    mcsat_clear(ctx->mcsat);
   }
 }
 

src/context/context.h

@@ -194,6 +194,22 @@ extern smt_status_t check_context(context_t *ctx, const param_t *parameters);
  */
 extern smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *parameters, uint32_t n, const literal_t *a);
 
+/*
+ * Check satisfiability under model: 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)
+ *
+ * return status: either STATUS_UNSAT, STATUS_SAT, STATUS_UNKNOWN,
+ * STATUS_INTERRUPTED
+ *
+ * If status is STATUS_UNSAT then the context and model are inconsistent
+ */
+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[]);
+
 
 /*
  * Build a model: the context's status must be STATUS_SAT or STATUS_UNKNOWN
@@ -230,6 +246,11 @@ extern void clean_solver_models(context_t *ctx);
 extern void context_build_unsat_core(context_t *ctx, ivector_t *v);
 
 
+/*
+ * Get the model interpolant: the context's status must be STATUS_USAT
+ */
+extern term_t context_get_unsat_model_interpolant(context_t *ctx);
+
 /*
  * Interrupt the search
  * - this can be called after check_context from a signal handler

src/context/context_solver.c

@@ -549,7 +549,7 @@ static void context_set_search_parameters(context_t *ctx, const param_t *params)
 }
 
 static smt_status_t _o_call_mcsat_solver(context_t *ctx, const param_t *params) {
-  mcsat_solve(ctx->mcsat, params);
+  mcsat_solve(ctx->mcsat, params, NULL, 0, NULL);
   return mcsat_status(ctx->mcsat);
 }
 
@@ -595,8 +595,6 @@ smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *param
   smt_core_t *core;
   smt_status_t stat;
 
-  assert(ctx->mcsat == NULL); // MC-SAT doesn't support assumptions yet
-
   core = ctx->core;
   stat = smt_status(core);
   if (stat == STATUS_IDLE) {
@@ -612,6 +610,25 @@ smt_status_t check_context_with_assumptions(context_t *ctx, const param_t *param
   return stat;
 }
 
+/*
+ * Check with given model
+ * - if mcsat status is not IDLE, return the status.
+ */
+smt_status_t check_context_with_model(context_t *ctx, const param_t *params, model_t* mdl, uint32_t n, const term_t t[]) {
+  assert(ctx->mcsat != NULL);
+  smt_status_t stat;
+
+  stat = mcsat_status(ctx->mcsat);
+  if (stat == STATUS_IDLE) {
+    mcsat_solve(ctx->mcsat, params, mdl, n, t);
+    stat = mcsat_status(ctx->mcsat);
+    if (n > 0 && stat == STATUS_UNSAT && context_supports_multichecks(ctx)) {
+      context_clear(ctx);
+    }
+  }
+
+  return stat;
+}
 
 
 /*
@@ -1178,3 +1195,9 @@ void context_build_unsat_core(context_t *ctx, ivector_t *v) {
     v->data[i] = t;
   }
 }
+
+extern term_t context_get_unsat_model_interpolant(context_t *ctx) {
+  assert(ctx->mcsat != NULL);
+  return mcsat_get_unsat_model_interpolant(ctx->mcsat);
+}
+