Merge branch 'kissat_delegate' into smtcomp2020

src/Makefile

@@ -120,6 +120,7 @@ core_src_c := \
 	context/divmod_table.c \
 	context/eq_abstraction.c \
 	context/eq_learner.c \
+	context/hidden_bvites.c \
 	context/internalization_table.c \
 	context/ite_flattener.c \
 	context/pseudo_subst.c \
@@ -165,6 +166,7 @@ core_src_c := \
 	parser_utils/parser.c \
 	parser_utils/term_stack2.c \
 	parser_utils/term_stack_error.c \
+	solvers/bv/bdds.c \
 	solvers/bv/bit_blaster.c \
 	solvers/bv/bv64_intervals.c \
 	solvers/bv/bv_atomtable.c \

src/api/yices_api.c

@@ -8199,6 +8199,7 @@ static void context_set_default_options(context_t *ctx, smt_logic_t logic, conte
     // flattening makes things worse for QF_BV
     //   disable_diseq_and_or_flattening(ctx); FOR TESTING THE SHARING STUFF (2015/04/22)
     enable_diseq_and_or_flattening(ctx); // FOR TESTING THE SHARING STUFF (2015/04/22)
+    enable_chase_bvite(ctx); // TESTING TOO
     break;
 
   case CTX_ARCH_SPLX:

src/context/context.c

@@ -5898,6 +5898,14 @@ static int32_t _o_context_process_assertions(context_t *ctx, uint32_t n, const t
       break;
 
     default:
+      //// PROVISIONAL
+      if (context_chase_bvite_enabled(ctx)) {
+	chase_bv_ite(ctx);
+	if (ctx->aux_eqs.size > 0) {
+	  process_aux_eqs(ctx);
+	}
+      }
+
       /*
        * Process the candidate variable substitutions if any
        */
@@ -6247,6 +6255,9 @@ int32_t context_process_formulas(context_t *ctx, uint32_t n, term_t *f) {
       break;
 
     default:
+      if (context_chase_bvite_enabled(ctx)) {
+	chase_bv_ite(ctx);
+      }
       /*
        * Process the candidate variable substitutions if any
        */

src/context/context_simplifier.c

@@ -27,8 +27,9 @@
 #include "context/conditional_definitions.h"
 #include "context/context_simplifier.h"
 #include "context/context_utils.h"
-#include "context/internalization_codes.h"
 #include "context/eq_learner.h"
+#include "context/hidden_bvites.h"
+#include "context/internalization_codes.h"
 #include "context/symmetry_breaking.h"
 #include "terms/bvfactor_buffers.h"
 #include "terms/poly_buffer_terms.h"
@@ -3706,3 +3707,56 @@ void process_conditional_definitions(context_t *ctx) {
     delete_cond_def_collector(&collect);
   }
 }
+
+
+/*
+ * EXPERIMENTAL/SIMPLER FORM FOR BIT-VECTOR PROBLEMS
+ */
+void chase_bv_ite(context_t *ctx) {
+  half_ite_table_t table;
+  conditional_eq_t condeq;
+  term_table_t *terms;
+  ivector_t *v;
+  term_t t;
+  uint32_t i, j, n, m;
+
+  init_half_ite_table(&table, ctx);
+
+  terms = ctx->terms;
+  v = &ctx->top_formulas;
+  n = v->size;
+  for (i=0; i<n; i++) {
+    t = v->data[i];
+    if (is_cond_eq(terms, t, &condeq)) {
+      add_half_ite(&table, &condeq, t);
+    }
+  }
+
+  if (table.nelems > 0) {
+    //    printf("got %"PRIu32" semi-conditionals\n", table.nelems);
+    m = assert_hidden_ites(&table);
+    //    printf("found %"PRIu32" hidden if-then-elses\n", m);
+
+    if (m > 0) {
+      j = 0;
+      for (i=0; i<n; i++) {
+	t = v->data[i];
+	if (! subsumed_by_hidden_ite(&table, t)) {
+	  v->data[j] = t;
+	  j ++;
+#if 0
+	} else {
+	  assert(is_cond_eq(terms, t, &condeq));
+	  printf("  subsumed: assertion[%"PRIu32"] = ", i);
+	  print_term(stdout, terms, t);
+	  printf("\n");
+#endif
+	}
+      }
+      ivector_shrink(v, j);
+    }
+
+  }
+
+  delete_half_ite_table(&table);
+}

src/context/context_simplifier.h

@@ -392,6 +392,11 @@ extern void break_uf_symmetries(context_t *ctx);
 extern void process_conditional_definitions(context_t *ctx);
 
 
+/*
+ * A simpler form of conditional definitions for bit-vector benchmarks:
+ */
+extern void chase_bv_ite(context_t *ctx);
+
 
 /*
  * CONDITIONALS/FLATTENING OF NESTED IF-THEN-ELSE

src/context/context_types.h

@@ -143,13 +143,14 @@ typedef enum {
 #define CONDITIONAL_DEF_OPTION_MASK     0x4000
 #define FLATTEN_ITE_OPTION_MASK         0x8000
 #define FACTOR_OR_OPTION_MASK           0x10000
+#define CHASE_BVITE_OPTION_MASK         0x20000
 
 #define PREPROCESSING_OPTIONS_MASK \
  (VARELIM_OPTION_MASK|FLATTENOR_OPTION_MASK|FLATTENDISEQ_OPTION_MASK|\
   EQABSTRACT_OPTION_MASK|ARITHELIM_OPTION_MASK|KEEP_ITE_OPTION_MASK|\
   BVARITHELIM_OPTION_MASK|BREAKSYM_OPTION_MASK|PSEUDO_INVERSE_OPTION_MASK|\
   ITE_BOUNDS_OPTION_MASK|CONDITIONAL_DEF_OPTION_MASK|FLATTEN_ITE_OPTION_MASK|\
-  FACTOR_OR_OPTION_MASK)
+  FACTOR_OR_OPTION_MASK|CHASE_BVITE_OPTION_MASK)
 
 // SIMPLEX OPTIONS
 #define SPLX_EGRLMAS_OPTION_MASK  0x1000000

src/context/context_utils.c

@@ -884,6 +884,34 @@ void add_arith_aux_eq(context_t *ctx, term_t eq) {
 
 
 
+/*
+ * Add an auxiliary bit equality between bit-vector terms
+ */
+void add_bv_aux_eq(context_t *ctx, term_t x, term_t y) {
+  term_table_t *terms;
+  term_t eq;
+
+  x = intern_tbl_get_root(&ctx->intern, x);
+  y = intern_tbl_get_root(&ctx->intern, y);
+
+  if (x != y) {
+    /*
+     * Build/get term (bveq x y)
+     */
+    terms = ctx->terms;
+    if (x > y) {
+      eq = bveq_atom(terms, y, x);
+    } else {
+      eq = bveq_atom(terms, x, y);
+    }
+
+    assert(intern_tbl_is_root(&ctx->intern, eq));
+
+    ivector_push(&ctx->aux_eqs, eq);
+  }
+}
+
+
 /*
  * LEARNED ATOMS
  */

src/context/context_utils.h

@@ -296,6 +296,10 @@ extern void add_aux_eq(context_t *ctx, term_t x, term_t y);
  */
 extern void add_arith_aux_eq(context_t *ctx, term_t eq);
 
+/*
+ * Variant for bit-vector terms
+ */
+extern void add_bv_aux_eq(context_t *ctx, term_t x, term_t y);
 
 /*
  * Auxiliary atoms:
@@ -482,6 +486,13 @@ static inline void disable_or_factoring(context_t *ctx) {
   ctx->options &= ~FACTOR_OR_OPTION_MASK;
 }
 
+static inline void enable_chase_bvite(context_t *ctx) {
+  ctx->options |= CHASE_BVITE_OPTION_MASK;
+}
+
+static inline void disable_chase_bvite(context_t *ctx) {
+  ctx->options |= CHASE_BVITE_OPTION_MASK;
+}
 
 
 /*
@@ -539,6 +550,10 @@ static inline bool context_or_factoring_enabled(context_t *ctx) {
   return (ctx->options & FACTOR_OR_OPTION_MASK) != 0;
 }
 
+static inline bool context_chase_bvite_enabled(context_t *ctx) {
+  return (ctx->options & CHASE_BVITE_OPTION_MASK) != 0;
+}
+
 static inline bool context_has_preprocess_options(context_t *ctx) {
   return (ctx->options & PREPROCESSING_OPTIONS_MASK) != 0;
 }