Skip to content

Commit

Permalink
Merge fdf86b4 into d62a1fe
Browse files Browse the repository at this point in the history
  • Loading branch information
@ahmed-irfan
ahmed-irfan committed Mar 19, 2024
2 parents d62a1fe + fdf86b4 commit a423b17
Show file tree
Hide file tree
Showing 2 changed files with 73 additions and 81 deletions.
43 changes: 11 additions & 32 deletions src/mcsat/uf/uf_plugin.c
View file
Expand Up @@ -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]);
t = unsigned_term(uf->conflict.data[i]);
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);
Expand Down Expand Up @@ -406,10 +394,13 @@ void uf_plugin_propagate(plugin_t* plugin, trail_token_t* prop) {
it != NULL;
it = int_hmap_next_record(&var_db->term_to_variable_map, it)) {
t = it->key;
if (t >= 0 && eq_graph_has_term(&uf->eq_graph, t) &&
!eq_graph_term_has_value(&uf->eq_graph, t)) {
all_assigned = false;
break;
if (t >= 0 && eq_graph_has_term(&uf->eq_graph, t)) {
variable_t t_var = variable_db_get_variable_if_exists(var_db, t);
assert(t_var != variable_null);
if (!trail_has_value(uf->ctx->trail, t_var)) {
all_assigned = false;
break;
}
}
}

Expand All @@ -421,22 +412,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]);
t = unsigned_term(uf->conflict.data[i]);
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);
Expand Down
111 changes: 62 additions & 49 deletions src/mcsat/weq/weak_eq_graph.c
View file
Expand Up @@ -1282,85 +1282,99 @@ void copy_uniques(ivector_t *to, ivector_t *from) {
delete_int_hset(&seen);
}

/* checks if the array terms (variable, select term, update term) are
* full assigned in the trail
*/
static
bool weq_is_fully_assigned(const weq_graph_t* weq, term_t t) {
variable_t t_var = variable_db_get_variable_if_exists(weq->ctx->var_db, t);
assert(t_var != variable_null);
if (!trail_has_value(weq->ctx->trail, t_var)) {
return false;
}

const term_table_t* terms = weq->ctx->terms;
composite_term_t* t_desc = NULL;

switch (term_kind(terms, t)) {
case UNINTERPRETED_TERM:
// already checked
break;
case APP_TERM:
t_desc = app_term_desc(terms, t);
break;
case UPDATE_TERM:
t_desc = update_term_desc(terms, t);
break;
default:
assert(false);
}

uint32_t i;
for (i = 0; t_desc && i < t_desc->arity; ++ i) {
term_t c = t_desc->arg[i];
variable_t c_var = variable_db_get_variable_if_exists(weq->ctx->var_db, c);
assert(c_var != variable_null);
if (!trail_has_value(weq->ctx->trail, c_var)) {
return false;
}
}

return true;
}

/* filter array-eq-terms based on the current model. We keep the
* array terms (array variables and update terms) that have been
* assigned a value in the equality graph. For array variables, it is
* assigned a value in the trail. For array variables, it is
* just a value assigned to the variable. For update terms, we check
* if update term, array term in the update, index term, value term
* have been assigned a value.
*/
static
void filter_array_eq_terms(const weq_graph_t* weq, const term_table_t* terms,
ivector_t *array_eq_terms) {
void filter_array_eq_terms(const weq_graph_t* weq,
ivector_t *array_eq_terms) {
const term_table_t* terms = weq->ctx->terms;

uint32_t i, j;
term_t t, arr1, arr2;
composite_term_t* t_desc;
composite_term_t* update_desc;

j = 0;
for (i = 0; i < array_eq_terms->size; ++i) {
t = array_eq_terms->data[i];
t_desc = eq_term_desc(terms, t);
arr1 = t_desc->arg[0];
arr2 = t_desc->arg[1];

if (!eq_graph_term_has_value(weq->eq_graph, arr1) ||
!eq_graph_term_has_value(weq->eq_graph, arr2)) {
if (!weq_is_fully_assigned(weq, arr1) ||
!weq_is_fully_assigned(weq, arr2)) {
continue;
}

if (term_kind(terms, arr1) == UPDATE_TERM) {
update_desc = update_term_desc(terms, arr1);
if (!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[0]) ||
!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[1]) ||
!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[2])) {
continue;
}
}
if (term_kind(terms, arr2) == UPDATE_TERM) {
update_desc = update_term_desc(terms, arr2);
if (!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[0]) ||
!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[1]) ||
!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[2])) {
continue;
}
}

array_eq_terms->data[j++] = array_eq_terms->data[i];
}
ivector_shrink(array_eq_terms, j);
}

/* filter array-terms based on the current model. We keep the
* array terms (array variables and update terms) that have been
* assigned a value in the equality graph. For array variables, it is
* assigned a value in the trail. For array variables, it is
* just a value assigned to the variable. For update terms, we check
* if update term, array term in the update, index term, value term
* have been assigned a value.
*/
static
void filter_array_terms(const weq_graph_t* weq, const term_table_t* terms,
ivector_t *array_terms) {
void filter_array_terms(const weq_graph_t* weq,
ivector_t *array_terms) {
uint32_t i, j;
term_t t;
composite_term_t* update_desc;

j = 0;
for (i = 0; i < array_terms->size; ++i) {
t = array_terms->data[i];
if (!eq_graph_term_has_value(weq->eq_graph, t)) {
if (!weq_is_fully_assigned(weq, t)) {
continue;
}

if (term_kind(terms, t) == UPDATE_TERM) {
update_desc = update_term_desc(terms, t);
if (!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[0]) ||
!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[1]) ||
!eq_graph_term_has_value(weq->eq_graph, update_desc->arg[2])) {
continue;
}
}

array_terms->data[j++] = array_terms->data[i];
}
ivector_shrink(array_terms, j);
Expand All @@ -1370,12 +1384,14 @@ void filter_array_terms(const weq_graph_t* weq, const term_table_t* terms,
* according to the current array terms.
* Basically, we keep select terms whose first argument (i.e. an array)
* is present in the arrays_terms vector.
* Moreover, we filter terms that don't have values assigned in the equality graph.
* Moreover, we filter terms that don't have values assigned in the trail.
*/
static
void filter_select_terms(const weq_graph_t* weq,
const term_table_t* terms, ivector_t *select_terms,
ivector_t *select_terms,
const ivector_t *array_terms) {
const term_table_t* terms = weq->ctx->terms;

uint32_t i, j;
composite_term_t* select_desc;
term_t t;
Expand All @@ -1390,13 +1406,10 @@ void filter_select_terms(const weq_graph_t* weq,
j = 0;
for (i = 0; i < select_terms->size; ++i) {
t = select_terms->data[i];
select_desc = app_term_desc(terms, t);
// check if the equality graph contains model values.
if (!eq_graph_term_has_value(weq->eq_graph, t) ||
!eq_graph_term_has_value(weq->eq_graph, select_desc->arg[0]) ||
!eq_graph_term_has_value(weq->eq_graph, select_desc->arg[1])) {
if (!weq_is_fully_assigned(weq, t)) {
continue;
}
select_desc = app_term_desc(terms, t);

do {
/* The array term (first arg) in the select term can be a select
Expand Down Expand Up @@ -1433,19 +1446,19 @@ void weq_graph_check_array_conflict(weq_graph_t* weq, ivector_t* conflict) {

init_ivector(&array_eq_terms, 0);
copy_uniques(&array_eq_terms, &weq->array_eq_terms);
filter_array_eq_terms(weq, weq->ctx->terms, &array_eq_terms);
filter_array_eq_terms(weq, &array_eq_terms);

init_ivector(&array_terms, 0);
copy_uniques(&array_terms, &weq->array_terms);
// filter array terms
filter_array_terms(weq, weq->ctx->terms, &array_terms);
filter_array_terms(weq, &array_terms);
// store array terms according to heuristic score
int_array_sort2(array_terms.data, array_terms.size, weq->ctx, weq_graph_array_terms_compare);

init_ivector(&select_terms, 0);
copy_uniques(&select_terms, &weq->select_terms);
// filter select terms
filter_select_terms(weq, weq->ctx->terms, &select_terms, &array_terms);
filter_select_terms(weq, &select_terms, &array_terms);
// store select terms according to heuristic score
int_array_sort2(select_terms.data, select_terms.size, weq->ctx, weq_graph_array_terms_compare);

Expand Down Expand Up @@ -1473,7 +1486,7 @@ void weq_graph_check_array_conflict(weq_graph_t* weq, ivector_t* conflict) {
(*weq->stats.array_check_calls) ++;

if (USE_ARRAY_DIFF) {
ok = weq_graph_array_ext_diff_check(weq, conflict, &array_eq_terms, NULL);
ok = weq_graph_array_ext_diff_check(weq, conflict, &array_eq_terms, NULL);
}
}

Expand Down

0 comments on commit a423b17

Please sign in to comment.