Mcsat unsat core

doc/manual/manual.tex

@@ -66,7 +66,7 @@ \chapter{Introduction}
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 
 This  manual   is  an  introduction   to  the  logic,   language,  and
-architecture  of the  Yices~2 SMT  solver. Yices  is developed  at SRI
+architecture  of the Yices~2 SMT  solver. Yices  is developed  at SRI
 International's  Computer Science  Laboratory.   Since version  2.5.3,
 Yices  is released  under the  GNU  General Public  License version  3
 (reproduced  in   Appendix~\ref{license}).   Previous   versions  were

doc/sphinx/source/context-operations.rst

@@ -110,12 +110,6 @@ for combination of nonlinear arithmetic and uninterpreted functions.
 If you configure a context for a logic such as ``"QF_NRA"`` or ``"QF_UFNIA"``
 then MCSat will be automatically selected.
 
-The MCSat solver does not currently support as many features as the
-DPLL(T) implementation. In particular, MCSat does not yet support
-computing unsat cores. However, unsat cores in MCSat can be computed
-using :c:func:`yices_check_context_with_model` and
-:c:func:`yices_get_model_interpolant`.
-
 
 **Theory Solvers**
 

src/Makefile

@@ -134,6 +134,7 @@ core_src_c := \
 	exists_forall/efsolver.c \
 	frontend/smt2/attribute_values.c \
 	frontend/smt2/smt2_lexer.c \
+	frontend/smt2/smt2_term_utils.c \
 	frontend/yices/yices_lexer.c \
 	frontend/yices/yices_parser.c \
 	io/concrete_value_printer.c \

src/frontend/smt2/smt2_commands.c

@@ -76,6 +76,9 @@
 #include "mt/threads.h"
 #include "mt/thread_macros.h"
 
+#include "frontend/smt2/smt2_term_utils.h"
+
+#include "utils/int_hash_map.h"
 
 /*
  * DUMP CONTEXT: FOR TESTING/DEBUGGING
@@ -678,18 +681,50 @@ static smt_status_t check_with_assumptions(context_t *ctx, const param_t *params
   if (ctx->mcsat) {
     // Copy over to model
     model_t mdl;
+    // Map from temporary Boolean variables (labels) to the original assumptions.
+    int_hmap_t lmap;
+
     init_model(&mdl, ctx->terms, true);
+    init_int_hmap(&lmap, 0);
     init_ivector(&assumptions, n);
+
     for (i = 0; i < n; ++ i) {
-      term_t x = unsigned_term(a[i]);
-      value_t val = is_pos_term(a[i]) ? vtbl_mk_bool(&mdl.vtbl, true) : vtbl_mk_bool(&mdl.vtbl, false);
-      model_map_term(&mdl, x, val);
-      ivector_push(&assumptions, x);
+      // create temporary Boolean label for assumptions
+      term_t b = new_uninterpreted_term(ctx->terms, bool_id);
+      int_hmap_add(&lmap, b, a[i]);
+      yices_assert_formula(ctx, yices_implies(b, a[i]));
+      model_map_term(&mdl, b, vtbl_mk_bool(&mdl.vtbl, true));
+      ivector_push(&assumptions, b);
     }
+
     // Solve
     status = yices_check_context_with_model(ctx, params, &mdl, n, assumptions.data);
+
+    if (status == YICES_STATUS_UNSAT) {
+      term_t model_interp = context_get_unsat_model_interpolant(ctx);
+      if (model_interp != NULL_TERM) {
+	      ivector_t lcore;
+        init_ivector(&lcore, 0);
+        filter_assumptions_by_term(ctx, model_interp, &assumptions, &lcore);
+	      ivector_reset(core);
+	      for (i = 0; i < lcore.size; ++ i) {
+          int_hmap_pair_t* e = int_hmap_find(&lmap, lcore.data[i]);
+          if (e != NULL) {
+            // The unsat core from the solver may contain temporary Boolean variables.
+            // We use lmap to find the original assumption that corresponds to each
+            // temporary variable in the core.
+            ivector_push(core, e->val);
+            //print_term_full(stderr, ctx->terms, e->val);
+            //fflush(stdout);
+          }
+        }
+        delete_ivector(&lcore);
+      }
+    }
+
     // Remove temps
     delete_ivector(&assumptions);
+    delete_int_hmap(&lmap);
     delete_model(&mdl);
 
     return status;
@@ -2293,6 +2328,10 @@ static void set_unsat_core_option(smt2_globals_t *g, const char *name, aval_t va
       print_error("can't have both :produce-unsat-cores and :produce-unsat-assumptions true");
     } else {
       g->produce_unsat_cores = flag;
+      // Set model_interpolation if context is MCSAT or will use MCSAT architecture
+      if (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)) {
+        g->mcsat_options.model_interpolation = true;
+      }
       report_success();
     }
   } else {
@@ -2308,6 +2347,10 @@ static void set_unsat_assumption_option(smt2_globals_t *g, const char *name, ava
       print_error("can't have both :produce-unsat-cores and :produce-unsat-assumptions true");
     } else {
       g->produce_unsat_assumptions = flag;
+      // Set model_interpolation if context is MCSAT or will use MCSAT architecture
+      if (g->mcsat || (g->logic_code != SMT_UNKNOWN && arch_for_logic(g->logic_code) == CTX_ARCH_MCSAT)) {
+        g->mcsat_options.model_interpolation = true;
+      }
       report_success();
     }
   } else {
@@ -3189,7 +3232,7 @@ static void validate_unsat_core(smt2_globals_t *g) {
   int32_t code;
   smt_status_t status;
 
-  if (g->unsat_core->status == STATUS_UNSAT) {
+  if (g->unsat_core->status == YICES_STATUS_UNSAT) {
     saved_context = g->ctx;
     g->ctx = NULL;
     init_smt2_context(g);
@@ -3205,7 +3248,7 @@ static void validate_unsat_core(smt2_globals_t *g) {
       fflush(stdout);
     } else {
       status = check_context(g->ctx, &g->parameters);
-      if (status != STATUS_UNSAT) {
+      if (status != YICES_STATUS_UNSAT) {
         printf("**** BUG: INVALID UNSAT CORE ****\n");
         fflush(stdout);
       }
@@ -3282,7 +3325,7 @@ static void check_delayed_assertions_assuming(smt2_globals_t *g, uint32_t n, sig
       if (code < 0) {
         // error during assertion processing
         print_yices_error(true);
-	done = true;
+        done = true;
         return;
       }
       init_search_parameters(g);
@@ -3296,7 +3339,7 @@ static void check_delayed_assertions_assuming(smt2_globals_t *g, uint32_t n, sig
         // cleanup
         free_assumptions(assumptions);
         g->unsat_assumptions = NULL;
-	done = true;
+        done = true;
       }
     }
   }
@@ -6448,18 +6491,14 @@ void smt2_set_logic(const char *name) {
     }
   }
 
-  // if unsat cores or unsat assumptions are requested, we can't use the mcsat solver
-  if (__smt2_globals.produce_unsat_cores || __smt2_globals.produce_unsat_assumptions) {
-    if (__smt2_globals.mcsat) {
-      print_error("the mcsat solver does not support unsat cores");
-      return;
-    }
-    if (arch == CTX_ARCH_MCSAT) {
-      print_error("unsat cores are not supported in logic %s", name);
-      return;
-    }
+  // Set model_interpolation if unsat cores are enabled and architecture is MCSAT
+  if ((__smt2_globals.produce_unsat_cores || __smt2_globals.produce_unsat_assumptions) && 
+      (arch == CTX_ARCH_MCSAT || __smt2_globals.mcsat)) {
+    __smt2_globals.mcsat_options.model_interpolation = true;
   }
 
+
+
   smt2_lexer_activate_logic(code);
   __smt2_globals.logic_code = code;
   __smt2_globals.logic_name = clone_string(name);

src/frontend/smt2/smt2_term_utils.c

@@ -0,0 +1,112 @@
+/*
+ * This file is part of the Yices SMT Solver.
+ * Copyright (C) 2017 SRI International.
+ *
+ * Yices is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Yices is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#include "smt2_term_utils.h"
+#include "terms/term_explorer.h"
+#include "utils/int_hash_sets.h"
+#include "terms/terms.h"
+
+
+/*
+ * Explore a term t, add all boolean atoms to vector v.
+ * - h is a hash set used to record visited terms
+ */
+static void collect_atoms_recursive(context_t *ctx, term_t t, int_hset_t *atoms, int_hset_t *visited) {
+  term_table_t *terms;
+  uint32_t i, n;
+
+  if (t < 0) {
+    t = not(t);
+  }
+
+  if (int_hset_member(visited, t)) {
+    return;
+  }
+  int_hset_add(visited, t);
+
+  terms = ctx->terms;
+
+  if (term_type(terms, t) == bool_type(terms->types)) {
+    int_hset_add(atoms, t);
+  }
+
+  if (term_is_projection(terms, t)) {
+    collect_atoms_recursive(ctx, proj_term_arg(terms, t), atoms, visited);
+  } else if (term_is_sum(terms, t)) {
+    n = term_num_children(terms, t);
+    for (i=0; i<n; i++) {
+      term_t child;
+      mpq_t q;
+      mpq_init(q);
+      sum_term_component(terms, t, i, q, &child);
+      collect_atoms_recursive(ctx, child, atoms, visited);
+      mpq_clear(q);
+    }
+  } else if (term_is_bvsum(terms, t)) {
+    uint32_t nbits = term_bitsize(terms, t);
+    int32_t *a = (int32_t*) safe_malloc(nbits * sizeof(int32_t));
+    n = term_num_children(terms, t);
+    for (i=0; i<n; i++) {
+      term_t child;
+      bvsum_term_component(terms, t, i, a, &child);
+      collect_atoms_recursive(ctx, child, atoms, visited);
+    }
+    safe_free(a);
+  } else if (term_is_product(terms, t)) {
+    n = term_num_children(terms, t);
+    for (i=0; i<n; i++) {
+      term_t child;
+      uint32_t exp;
+      product_term_component(terms, t, i, &child, &exp);
+      collect_atoms_recursive(ctx, child, atoms, visited);
+    }
+  } else if (term_is_composite(terms, t)) {
+    n = term_num_children(terms, t);
+    for (i=0; i<n; i++) {
+      collect_atoms_recursive(ctx, term_child(terms, t, i), atoms, visited);
+    }
+  }
+}
+
+/*
+ * Wrapper: initialize hash set then call the recursive function
+ */
+void collect_atoms(context_t *ctx, term_t t, int_hset_t *h) {
+  int_hset_t visited;
+  init_int_hset(&visited, 0);
+  collect_atoms_recursive(ctx, t, h, &visited);
+  delete_int_hset(&visited);
+}
+
+void filter_assumptions_by_term(context_t *ctx, term_t t, const ivector_t *assumptions, ivector_t *result) {
+  int_hset_t seen_atoms;
+  uint32_t i;
+  term_t assumption;
+
+  init_int_hset(&seen_atoms, 0);
+  collect_atoms(ctx, t, &seen_atoms);
+
+  for (i = 0; i < assumptions->size; i++) {
+    assumption = assumptions->data[i];
+    if (int_hset_member(&seen_atoms, unsigned_term(assumption))) {
+      ivector_push(result, assumption);
+    }
+  }
+
+  delete_int_hset(&seen_atoms);
+} 

src/frontend/smt2/smt2_term_utils.h

@@ -0,0 +1,46 @@
+/*
+ * This file is part of the Yices SMT Solver.
+ * Copyright (C) 2017 SRI International.
+ *
+ * Yices is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * Yices is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
+ */
+
+#ifndef __SMT2_TERM_UTILS_H
+#define __SMT2_TERM_UTILS_H
+
+#include "context/context.h"
+#include "utils/int_vectors.h"
+#include "utils/int_hash_sets.h"
+
+/*
+ * Collect all boolean atoms from a given term t.
+ * - ctx: the context, used to get the term table
+ * - t: the term to explore
+ * - h: the hash set where the atoms are stored.
+ *      the set must be initialized.
+ */
+extern void collect_atoms(context_t *ctx, term_t t, int_hset_t *h);
+
+/*
+ * Given a term t and a vector of assumptions, collect all assumptions
+ * that appear as sub-terms of t.
+ * - ctx: the context
+ * - t: the term to explore
+ * - assumptions: vector of assumption terms
+ * - result: output vector. The relevant assumptions are added to this vector.
+ */
+extern void filter_assumptions_by_term(context_t *ctx, term_t t, const ivector_t *assumptions, ivector_t *result);
+
+
+#endif /* __SMT2_TERM_UTILS_H */