Fixes/updates to the incremental solver from the mcsat-bv branch.

.travis/build.sh

@@ -2,29 +2,26 @@
 # Make sure we exit if there is a failure
 set -e
 
-#build and install libpoly (Dejan when will this be a ubuntu package?)
+# Build and install libpoly
+pushd .
 git clone https://github.com/SRI-CSL/libpoly.git
 cd libpoly/build
 cmake ..
 make
 sudo make install
+popd
 
-#now build yices
-cd ../..
+#Build Yices
 autoconf
 ./configure --enable-mcsat
 
-make MODE=gcov 
-
-#this is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default?
+# This is needed for yices2 to find libpoly.so.0. /usr/local/lib not searched by default?
 export LD_LIBRARY_PATH=/usr/local/lib/:${LD_LIBRARY_PATH}
 
+make MODE=gcov 
 make MODE=gcov check
 
-
 RETURN="$?"
-
-
 if [ "${RETURN}" != "0" ]; then
     echo "Building and checking yices2 failed!"
     exit 1

Makefile.build

@@ -90,7 +90,7 @@ srcsubdirs = \
     solvers/bv solvers/egraph solvers/cdcl solvers/simplex \
     parser_utils model scratch api frontend frontend/smt1 \
     frontend/yices frontend/smt2 context exists_forall \
-    mcsat mcsat/uf  mcsat/bool mcsat/ite mcsat/nra mcsat/utils
+    mcsat mcsat/uf mcsat/bool mcsat/ite mcsat/nra mcsat/utils
 
 testdir = tests/unit
 regressdir = tests/regress

configure.ac

@@ -246,7 +246,7 @@ dnl the static libraries, using the same conventions as for GMP.
 dnl
 use_mcsat="no"
 AC_ARG_ENABLE([mcsat],
-   [AS_HELP_STRING([--enable-mcsat],[Enable support for MCSAT. This requires the libpoly library.])],
+   [AS_HELP_STRING([--enable-mcsat],[Enable support for MCSAT. This requires the LibPoly library and the CUDD library.])],
    [if test "$enableval" = yes ; then 
       use_mcsat="yes"
       AC_MSG_NOTICE([Enabling support for MCSAT])

src/frontend/smt2/smt2_commands.c

@@ -4707,6 +4707,7 @@ void smt2_set_logic(const char *name) {
   } else {
     // in benchmark mode (or exists/forall) set the parameters to defaults for the logic
     // the context is not initialized yet
+    arch = arch_for_logic(code);
     default_ctx_params(&__smt2_globals.ctx_parameters, code, arch, CTX_MODE_ONECHECK);
     yices_set_default_params(&__smt2_globals.parameters, code, arch, CTX_MODE_ONECHECK);
   }

src/frontend/smt2/smt2_model_printer.c

@@ -29,6 +29,7 @@
 #include "frontend/smt2/smt2_printer.h"
 #include "model/model_eval.h"
 #include "utils/int_vectors.h"
+#include "utils/int_array_sort.h"
 
 
 /*
@@ -168,6 +169,8 @@ void smt2_pp_model(yices_pp_t *printer, model_t *model) {
   init_ivector(&v, 0);
   model_collect_terms(model, false, model->terms, is_named_unint, &v);
 
+  int_array_sort(v.data, v.size);
+
   n = v.size;
   a = v.data;
   smt2_pp_bool_assignments(printer, model, a, n);
@@ -338,6 +341,10 @@ void smt2_pp_full_model(yices_pp_t *printer, model_t *model) {
     model_collect_terms(model, false, model->terms, is_named_unint, &v);
     evaluator_collect_cached_terms(&eval, model->terms, is_named_unint, &v);
 
+    // sort the terms so that we have consistent printouts with different
+    // algorithms
+    int_array_sort(v.data, v.size);
+
     // print everything
     n = v.size;
     a = v.data;

src/mcsat/bool/bool_plugin.c

@@ -630,7 +630,9 @@ void bool_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
             break;
           } else {
             // Literal is false, see if at level 0, to push to back
-            if (literal_get_level(clause->literals[k], trail) == trail->decision_level_base) {
+            // TODO: We can check == clause level, but it's not clear
+            // this optimization has any merit
+            if (literal_get_level(clause->literals[k], trail) == 0) {
               clause->size --;
               clause_swap_literals(clause, k, clause->size);
               -- k;
@@ -786,7 +788,6 @@ void bool_plugin_pop(plugin_t* plugin) {
     propagated_var = ivector_pop2(&bp->propagated);
     bool_plugin_set_reason_ref(bp, propagated_var, clause_ref_null);
   }
-
 }
 
 /**

src/mcsat/bool/cnf.c

@@ -346,7 +346,10 @@ void cnf_gc_mark(cnf_t* cnf, gc_info_t* gc_clauses, const gc_info_t* gc_vars) {
   // CNF marks only the clauses that are definitions of the variables to keep
   for (; i < gc_vars->marked.size; ++ i) {
     var = gc_vars->marked.data[i];
-    if(cnf_is_converted(cnf, var)) {
+    if (trace_enabled(cnf->ctx->tracer, "mcsat::gc")) {
+      ctx_trace_term(cnf->ctx, variable_db_get_term(cnf->ctx->var_db, var));
+    }
+    if (cnf_is_converted(cnf, var)) {
       int_lset_iterator_construct(&it, &cnf->converted, var);
       while (!int_lset_iterator_done(&it)) {
         clause_ref = *int_lset_iterator_get(&it);

src/mcsat/nra/feasible_set_db.c

@@ -298,7 +298,7 @@ bool feasible_set_db_update(feasible_set_db_t* db, variable_t x, lp_feasibility_
   assert(db->updates_size == db->updates.size);
 
   // If fixed, put into the fixed array
-  if (lp_feasibility_set_is_point(new_set)) {
+  if (lp_feasibility_set_is_point(intersect)) {
     ivector_push(&db->fixed_variables, x);
     db->fixed_variable_size ++;
   }

src/mcsat/nra/nra_plugin.c

@@ -16,12 +16,6 @@
  * along with Yices.  If not, see <http://www.gnu.org/licenses/>.
  */
 
-#if defined(CYGWIN) || defined(MINGW)
-#ifndef __YICES_DLLSPEC__
-#define __YICES_DLLSPEC__ __declspec(dllexport)
-#endif
-#endif
-
 #include <poly/polynomial.h>
 #include <poly/polynomial_context.h>
 #include <poly/variable_db.h>
@@ -256,11 +250,17 @@ void nra_plugin_new_term_notify(plugin_t* plugin, term_t t, trail_token_t* prop)
 
   assert(!is_neg_term(t));
 
+  term_kind_t t_kind = term_kind(terms, t);
+
+  // Only process power terms if they are real ones
+  if (t_kind == POWER_PRODUCT && !is_arithmetic_term(terms, t)) {
+    return;
+  }
+
   // The variable
   variable_t t_var = variable_db_get_variable(nra->ctx->var_db, t);
 
   // Check for div and mod
-  term_kind_t t_kind = term_kind(terms, t);
   if (t_kind == ARITH_MOD) {
     // Just make sure that the div is registered
     composite_term_t* mod = arith_mod_term_desc(terms, t);
@@ -1496,8 +1496,6 @@ void nra_plugin_new_lemma_notify(plugin_t* plugin, ivector_t* lemma, trail_token
         ctx_trace_printf(nra->ctx, "\n");
       }
 
-
-
       lp_feasibility_set_add(lemma_feasible, constraint_feasible);
       lp_feasibility_set_delete(constraint_feasible);
     }

src/mcsat/nra/nra_plugin_internal.h

@@ -21,6 +21,7 @@
 #include <poly/poly.h>
 
 #include "mcsat/plugin.h"
+#include "mcsat/unit_info.h"
 #include "mcsat/watch_list_manager.h"
 #include "mcsat/utils/scope_holder.h"
 #include "mcsat/utils/int_mset.h"
@@ -39,15 +40,6 @@ typedef struct poly_constraint_struct poly_constraint_t;
 // #define TRACK_CONSTRAINT(x) (x == 2640)
 #define TRACK_CONSTRAINT(x) false
 
-typedef enum {
-  /** The constraint is not unit, nor fully assigned */
-  CONSTRAINT_UNKNOWN,
-  /** The constraint is unit */
-  CONSTRAINT_UNIT,
-  /** All variables of the constraint are assigned */
-  CONSTRAINT_FULLY_ASSIGNED
-} constraint_unit_info_t;
-
 struct nra_plugin_s {
 
   /** The plugin interface */

src/mcsat/preprocessor.c

@@ -540,9 +540,6 @@ term_t preprocessor_apply(preprocessor_t* pre, term_t t, ivector_t* out) {
       break;
     }
 
-
-      break;
-
     default:
       // UNSUPPORTED TERM/THEORY
       longjmp(*pre->exception, MCSAT_EXCEPTION_UNSUPPORTED_THEORY);

src/mcsat/solver.c

@@ -122,9 +122,12 @@ struct mcsat_solver_s {
   /** Size of the input table at entry to solve() */
   uint32_t terms_size_on_solver_entry;
 
-  /** The status */
+  /** The status (real status is in trail, this is for context integration) */
   smt_status_t status;
 
+  /** Number of inconsistent push calls */
+  uint32_t inconsistent_push_calls;
+
   /** Notifications for new variables */
   solver_new_variable_notify_t var_db_notify;
 
@@ -611,6 +614,7 @@ void mcsat_construct(mcsat_solver_t* mcsat, context_t* ctx) {
   mcsat->terms = ctx->terms;
   mcsat->terms_size_on_solver_entry = 0;
   mcsat->status = STATUS_IDLE;
+  mcsat->inconsistent_push_calls = 0;
 
   // The new variable listener
   mcsat->var_db_notify.mcsat = mcsat;
@@ -782,6 +786,16 @@ void mcsat_push(mcsat_solver_t* mcsat) {
 
   assert(mcsat->status == STATUS_IDLE); // We must have clear before
 
+  if (trace_enabled(mcsat->ctx->trace, "mcsat::push")) {
+    mcsat_trace_printf(mcsat->ctx->trace, "mcsat::push start\n");
+    trail_print(mcsat->trail, trace_out(mcsat->ctx->trace));
+  }
+
+  if (!trail_is_consistent(mcsat->trail)) {
+    mcsat->inconsistent_push_calls ++;
+    return;
+  }
+
   // Internal stuff push
   scope_holder_push(&mcsat->scope,
       &mcsat->assertion_vars.size,
@@ -792,6 +806,12 @@ void mcsat_push(mcsat_solver_t* mcsat) {
   trail_new_base_level(mcsat->trail);
   // Push the preprocessor
   preprocessor_push(&mcsat->preprocessor);
+
+  if (trace_enabled(mcsat->ctx->trace, "mcsat::push")) {
+    mcsat_trace_printf(mcsat->ctx->trace, "mcsat::pop end\n");
+    trail_print(mcsat->trail, trace_out(mcsat->ctx->trace));
+  }
+
 }
 
 
@@ -802,6 +822,17 @@ void mcsat_pop(mcsat_solver_t* mcsat) {
   // - assertions
   // - variables and terms
 
+  if (trace_enabled(mcsat->ctx->trace, "mcsat::pop")) {
+    mcsat_trace_printf(mcsat->ctx->trace, "mcsat::pop start\n");
+    trail_print(mcsat->trail, trace_out(mcsat->ctx->trace));
+  }
+
+  if (mcsat->inconsistent_push_calls > 0) {
+    mcsat->inconsistent_push_calls --;
+    mcsat->status = STATUS_IDLE;
+    return;
+  }
+
   // Backtrack trail
   uint32_t new_base_level = trail_pop_base_level(mcsat->trail);
 
@@ -827,6 +858,11 @@ void mcsat_pop(mcsat_solver_t* mcsat) {
 
   // Set the status back to idle
   mcsat->status = STATUS_IDLE;
+
+  if (trace_enabled(mcsat->ctx->trace, "mcsat::pop")) {
+    mcsat_trace_printf(mcsat->ctx->trace, "mcsat::pop end\n");
+    trail_print(mcsat->trail, trace_out(mcsat->ctx->trace));
+  }
 }
 
 void mcsat_clear(mcsat_solver_t* mcsat) {
@@ -945,6 +981,10 @@ void mcsat_gc(mcsat_solver_t* mcsat) {
     var = mcsat->assertion_vars.data[i];
     assert(variable_db_is_variable(mcsat->var_db, var, true));
     gc_info_mark(&gc_vars, var);
+    if (trace_enabled(mcsat->ctx->trace, "mcsat::gc")) {
+      mcsat_trace_printf(mcsat->ctx->trace, "mcsat_gc(): marking ");
+      trace_term_ln(mcsat->ctx->trace, mcsat->terms, variable_db_get_term(mcsat->var_db, var));
+    }
   }
 
   // Mark the trail variables as needed
@@ -1118,7 +1158,7 @@ void mcsat_assert_formula(mcsat_solver_t* mcsat, term_t f) {
   }
 
   // If we're unsat, no more assertions
-  if (mcsat->status == STATUS_UNSAT) {
+  if (!trail_is_consistent(mcsat->trail)) {
     return;
   }
 
@@ -1143,7 +1183,7 @@ void mcsat_assert_formula(mcsat_solver_t* mcsat, term_t f) {
     } else {
       // If negative already, we're inconsistent
       if (!trail_get_boolean_value(mcsat->trail, f_pos_var)) {
-        mcsat->status = STATUS_UNSAT;
+        trail_set_inconsistent(mcsat->trail);
         return;
       }
     }
@@ -1154,7 +1194,7 @@ void mcsat_assert_formula(mcsat_solver_t* mcsat, term_t f) {
     } else {
       // If positive already, we're inconsistent
       if (trail_get_boolean_value(mcsat->trail, f_pos_var)) {
-        mcsat->status = STATUS_UNSAT;
+        trail_set_inconsistent(mcsat->trail);
         return;
       }
     }
@@ -1638,7 +1678,8 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params) {
   luby_t luby;
 
   // If we're already unsat, just return
-  if (mcsat->status == STATUS_UNSAT) {
+  if (!trail_is_consistent(mcsat->trail)) {
+    mcsat->status = STATUS_UNSAT;
     return;
   }
 
@@ -1653,7 +1694,6 @@ void mcsat_solve(mcsat_solver_t* mcsat, const param_t *params) {
   restart_resource = 0;
   luby_init(&luby, mcsat->heuristic_params.restart_interval);
 
-
   for (;;) {
 
     // Do we restart

src/mcsat/tracing.c

@@ -34,7 +34,7 @@ void trace_term_ln(tracer_t* tracer, term_table_t* terms, term_t t) {
   trace_pp_term(tracer, 0, terms, t);
 }
 
-void ctx_trace_term(plugin_context_t* ctx, term_t t) {
+void ctx_trace_term(const plugin_context_t* ctx, term_t t) {
   trace_pp_term(ctx->tracer, 0, ctx->terms, t);
 }
 
@@ -104,7 +104,7 @@ void mcsat_trace_printf(tracer_t* tracer, const char* format, ...) {
   }
 }
 
-void ctx_trace_printf(plugin_context_t* ctx, const char* format, ...) {
+void ctx_trace_printf(const plugin_context_t* ctx, const char* format, ...) {
   va_list p;
   int code;
 

src/mcsat/tracing.h

@@ -24,7 +24,7 @@
 
 /** Check if the tag is enabled */
 static inline
-bool ctx_trace_enabled(plugin_context_t* ctx, const char* tag) {
+bool ctx_trace_enabled(const plugin_context_t* ctx, const char* tag) {
 #ifndef NDEBUG
   return (ctx->tracer != NULL && tracing_tag(ctx->tracer, tag));
 #else
@@ -44,7 +44,7 @@ bool trace_enabled(tracer_t* tracer, const char* tag) {
 
 /** Return the file associated with the trace */
 static inline
-FILE* ctx_trace_out(plugin_context_t* ctx) {
+FILE* ctx_trace_out(const plugin_context_t* ctx) {
   if (ctx->tracer != NULL && ctx->tracer->file != NULL) {
     return ctx->tracer->file;
   } else {
@@ -69,13 +69,13 @@ void term_print_to_file(FILE* out, term_table_t* terms, term_t t);
 void trace_term_ln(tracer_t* tracer, term_table_t* terms, term_t t);
 
 /** Print the term to the trace */
-void ctx_trace_term(plugin_context_t* ctx, term_t t);
+void ctx_trace_term(const plugin_context_t* ctx, term_t t);
 
 /** Print to the trace */
 void mcsat_trace_printf(tracer_t* tracer, const char* format, ...) __attribute__ ((format (printf, 2, 3)));
 
 /** Print to the trace */
-void ctx_trace_printf(plugin_context_t* ctx, const char* format, ...) __attribute__ ((format (printf, 2, 3)));
+void ctx_trace_printf(const plugin_context_t* ctx, const char* format, ...) __attribute__ ((format (printf, 2, 3)));
 
 /** String representation of the kind */
 const char* kind_to_string(term_kind_t kind);