simple bump heuristic

SRI-CSL · Jan 4, 2024 · bef9601 · bef9601
1 parent ce04f1b
commit bef9601
Showing 1 changed file with 2 additions and 26 deletions.
diff --git a/src/mcsat/uf/uf_plugin.c b/src/mcsat/uf/uf_plugin.c
@@ -344,22 +344,10 @@ void uf_plugin_learn(plugin_t* plugin, trail_token_t* prop) {
     (*uf->stats.conflicts) ++;
     // extract terms used in the conflict
     term_t t;
-    term_table_t *terms = uf->ctx->terms;
-    composite_term_t* t_desc = NULL;
     uint32_t i;
     for (i = 0; i < uf->conflict.size; ++i) {
       t = uf->conflict.data[i];
-      if (term_kind(terms, t) == EQ_TERM) {
-	t_desc = eq_term_desc(terms, t);
-      } else if (term_kind(terms, t) == BV_EQ_ATOM) {
-	t_desc = bveq_atom_desc(terms, t);
-      } else if (term_kind(terms, t) == ARITH_BINEQ_ATOM) {
-	t_desc = arith_bineq_atom_desc(terms, t);
-      } else {
-	assert(false);
-      }
-      int_mset_add(&uf->tmp, t_desc->arg[0]);
-      int_mset_add(&uf->tmp, t_desc->arg[1]);
+      int_mset_add(&uf->tmp, t);
     }
     uf_plugin_bump_terms_and_reset(uf, &uf->tmp);
     statistic_avg_add(uf->stats.avg_conflict_size, uf->conflict.size);
@@ -421,22 +409,10 @@ void uf_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
       prop->conflict(prop);
       (*uf->stats.conflicts) ++;
       // extract terms used in the conflict
-      term_table_t *terms = uf->ctx->terms;
-      composite_term_t* t_desc = NULL;
       uint32_t i;
       for (i = 0; i < uf->conflict.size; ++i) {
         t = uf->conflict.data[i];
-	if (term_kind(terms, t) == EQ_TERM) {
-          t_desc = eq_term_desc(terms, t);
-        } else if (term_kind(terms, t) == BV_EQ_ATOM) {
-	  t_desc = bveq_atom_desc(terms, t);
-	} else if (term_kind(terms, t) == ARITH_BINEQ_ATOM) {
-	  t_desc = arith_bineq_atom_desc(terms, t);
-	} else {
-          assert(false);
-        }
-	int_mset_add(&uf->tmp, t_desc->arg[0]);
-	int_mset_add(&uf->tmp, t_desc->arg[1]);
+	int_mset_add(&uf->tmp, t);
       }
       uf_plugin_bump_terms_and_reset(uf, &uf->tmp);
       statistic_avg_add(uf->stats.avg_conflict_size, uf->conflict.size);