Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Mcsat array simplify var bump #496

Merged
merged 5 commits into from
Mar 19, 2024
Merged

Mcsat array simplify var bump #496

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
5 commits
Select commit Hold shift + click to select a range
bef9601
simple bump heuristic
ahmed-irfan Jan 4, 2024
6c38451
unsigned_term for bumping
ahmed-irfan Jan 5, 2024
39cc940
Merge branch 'master' into mcsat-array-simplify-var-bump
ahmed-irfan Mar 17, 2024
d58ec75
use trail values to check if weq can be run
ahmed-irfan Mar 18, 2024
fdf86b4
fix a warning
ahmed-irfan Mar 18, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
43 changes: 11 additions & 32 deletions src/mcsat/uf/uf_plugin.c
View file
Open in desktop
Original file line number Diff line number Diff line change
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
Open in desktop
Original file line number Diff line number Diff line change
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
Loading