mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

fixing #1847

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-10-02 17:13:46 -07:00
parent 8b981e545d
commit fd9fd52271
2 changed files with 41 additions and 25 deletions
Download patch file Download diff file Expand all files Collapse all files

60
src/smt/theory_array_full.cpp
View file

@ -339,19 +339,14 @@ namespace smt {
SASSERT(v != null_theory_var);
v = find(v);
var_data* d = m_var_data[v];
TRACE("array", tout << "v" << v << "\n";);
TRACE("array", tout << "v" << v << " " << d->m_prop_upward << " " << m_params.m_array_delay_exp_axiom << "\n";);
for (enode * store : d->m_stores) {
SASSERT(is_store(store));
instantiate_default_store_axiom(store);
}
if (!m_params.m_array_weak && !m_params.m_array_delay_exp_axiom && d->m_prop_upward) {
for (enode * store : d->m_parent_stores) {
SASSERT(is_store(store));
if (!m_params.m_array_cg || store->is_cgr()) {
instantiate_default_store_axiom(store);
}
}
instantiate_parent_stores_default(v);
}
}
@ -382,23 +377,14 @@ namespace smt {
}
void theory_array_full::relevant_eh(app* n) {
TRACE("array", tout << mk_pp(n, get_manager()) << "\n";);
TRACE("array", tout << mk_pp(n, get_manager()) << "\n";);
theory_array::relevant_eh(n);
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n) && !is_store(n)) {
if (!is_default(n) && !is_select(n) && !is_map(n) && !is_const(n) && !is_as_array(n)){
return;
}
context & ctx = get_context();
enode* node = ctx.get_enode(n);
if (is_store(n)) {
enode * arg = ctx.get_enode(n->get_arg(0));
if (is_const(arg)) {
TRACE("array", tout << expr_ref(arg->get_owner(), get_manager()) << " " << is_const(arg) << "\n";);
theory_var v = arg->get_th_var(get_id());
set_prop_upward(v);
add_parent_default(v);
}
}
else if (is_select(n)) {
if (is_select(n)) {
enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v = arg->get_th_var(get_id());
SASSERT(v != null_theory_var);
@ -408,14 +394,18 @@ namespace smt {
enode * arg = ctx.get_enode(n->get_arg(0));
theory_var v = arg->get_th_var(get_id());
SASSERT(v != null_theory_var);
set_prop_upward(v);
add_parent_default(find(v));
}
else if (is_const(n)) {
instantiate_default_const_axiom(node);
theory_var v = node->get_th_var(get_id());
set_prop_upward(v);
add_parent_default(find(v));
}
else if (is_map(n)) {
for (unsigned i = 0; i < n->get_num_args(); ++i) {
enode* arg = ctx.get_enode(n->get_arg(i));
for (expr * e : *n) {
enode* arg = ctx.get_enode(e);
theory_var v_arg = find(arg->get_th_var(get_id()));
add_parent_map(v_arg, node);
set_prop_upward(v_arg);
@ -505,7 +495,7 @@ namespace smt {
app* map = mp->get_owner();
ast_manager& m = get_manager();
context& ctx = get_context();
if (!ctx.add_fingerprint(this, 0, 1, &mp)) {
if (!ctx.add_fingerprint(this, m_default_map_fingerprint, 1, &mp)) {
return false;
}
TRACE("array", tout << mk_bounded_pp(map, get_manager()) << "\n";);
@ -530,7 +520,7 @@ namespace smt {
bool theory_array_full::instantiate_default_const_axiom(enode* cnst) {
context& ctx = get_context();
if (!ctx.add_fingerprint(this, 0, 1, &cnst)) {
if (!ctx.add_fingerprint(this, m_default_const_fingerprint, 1, &cnst)) {
return false;
}
m_stats.m_num_default_const_axiom++;
@ -551,7 +541,7 @@ namespace smt {
return false;
#if 0
context& ctx = get_context();
if (!ctx.add_fingerprint(this, 0, 1, &arr)) {
if (!ctx.add_fingerprint(this, m_default_as_array_fingerprint, 1, &arr)) {
return false;
}
m_stats.m_num_default_as_array_axiom++;
@ -668,7 +658,7 @@ namespace smt {
app* store_app = store->get_owner();
context& ctx = get_context();
ast_manager& m = get_manager();
if (!ctx.add_fingerprint(this, 0, 1, &store)) {
if (!ctx.add_fingerprint(this, m_default_store_fingerprint, 1, &store)) {
return false;
}
@ -741,6 +731,10 @@ namespace smt {
var_data * d = m_var_data[v];
if (d->m_prop_upward && instantiate_axiom_map_for(v))
r = FC_CONTINUE;
if (d->m_prop_upward && !m_params.m_array_weak) {
if (instantiate_parent_stores_default(v))
r = FC_CONTINUE;
}
}
}
while (!m_eqsv.empty()) {
@ -755,6 +749,22 @@ namespace smt {
return r;
}
bool theory_array_full::instantiate_parent_stores_default(theory_var v) {
SASSERT(v != null_theory_var);
TRACE("array", tout << "v" << v << "\n";);
v = find(v);
var_data* d = m_var_data[v];
bool result = false;
for (enode * store : d->m_parent_stores) {
TRACE("array", tout << expr_ref(store->get_owner(), get_manager()) << "\n";);
SASSERT(is_store(store));
if (!m_params.m_array_cg || store->is_cgr()) {
if (instantiate_default_store_axiom(store))
result = true;
}
}
return result;
}
bool theory_array_full::try_assign_eq(expr* v1, expr* v2) {
TRACE("array",

6
src/smt/theory_array_full.h
View file

@ -38,6 +38,11 @@ namespace smt {
ast2ast_trailmap<sort,app> m_sort2epsilon;
obj_pair_map<expr,expr,bool> m_eqs;
svector<literal> m_eqsv;
static unsigned const m_default_map_fingerprint = UINT_MAX - 112;
static unsigned const m_default_store_fingerprint = UINT_MAX - 113;
static unsigned const m_default_const_fingerprint = UINT_MAX - 115;
static unsigned const m_default_as_array_fingerprint = UINT_MAX - 116;
protected:
@ -70,6 +75,7 @@ namespace smt {
bool instantiate_default_store_axiom(enode* store);
bool instantiate_default_map_axiom(enode* map);
bool instantiate_default_as_array_axiom(enode* arr);
bool instantiate_parent_stores_default(theory_var v);
bool has_large_domain(app* array_term);
app* mk_epsilon(sort* s);