From 4339722e98d809730351d71cd60e1c35c4856105 Mon Sep 17 00:00:00 2001 From: Arie Gurfinkel Date: Wed, 27 Jun 2018 14:36:59 -0400 Subject: [PATCH] Fix segfaults in qgen --- src/muz/spacer/spacer_quant_generalizer.cpp | 64 +++++++++++---------- src/muz/spacer/spacer_util.cpp | 17 ++++-- src/muz/spacer/spacer_util.h | 2 +- 3 files changed, 46 insertions(+), 37 deletions(-) diff --git a/src/muz/spacer/spacer_quant_generalizer.cpp b/src/muz/spacer/spacer_quant_generalizer.cpp index f66fe7b29..95e884d42 100644 --- a/src/muz/spacer/spacer_quant_generalizer.cpp +++ b/src/muz/spacer/spacer_quant_generalizer.cpp @@ -114,7 +114,7 @@ void lemma_quantifier_generalizer::find_candidates(expr *e, if (!contains_selects(e, m)) return; app_ref_vector indices(m); - get_select_indices(e, indices, m); + get_select_indices(e, indices); app_ref_vector extra(m); expr_sparse_mark marked_args; @@ -155,7 +155,7 @@ bool lemma_quantifier_generalizer::match_sk_idx(expr *e, app_ref_vector const &z if (!contains_selects(e, m)) return false; app_ref_vector indicies(m); - get_select_indices(e, indicies, m); + get_select_indices(e, indicies); if (indicies.size() > 2) return false; unsigned i=0; @@ -255,15 +255,17 @@ void lemma_quantifier_generalizer::cleanup(expr_ref_vector &cube, app_ref_vector lb and ub are null if no bound was found */ -void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var *var, +void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, + var *var, expr_ref_vector &gnd_cube, expr_ref_vector &abs_cube, - expr *&lb, expr *&ub, unsigned &stride) { + expr *&lb, expr *&ub, + unsigned &stride) { // create an abstraction function that maps candidate term to variables expr_safe_replace sub(m); // term -> var - sub.insert(term , var); + sub.insert(term, var); rational val; if (m_arith.is_numeral(term, val)) { bool is_int = val.is_int(); @@ -285,19 +287,17 @@ void lemma_quantifier_generalizer::mk_abs_cube(lemma_ref &lemma, app *term, var for (expr *lit : m_cube) { expr_ref abs_lit(m); - sub (lit, abs_lit); - if (lit == abs_lit) { - gnd_cube.push_back(lit); - } + sub(lit, abs_lit); + if (lit == abs_lit) {gnd_cube.push_back(lit);} else { expr *e1, *e2; // generalize v=num into v>=num if (m.is_eq(abs_lit, e1, e2) && (e1 == var || e2 == var)) { - if (m_arith.is_numeral(e1)) { - abs_lit = m_arith.mk_ge (var, e1); + if (m_arith.is_numeral(e1)) { + abs_lit = m_arith.mk_ge(var, e1); } else if (m_arith.is_numeral(e2)) { abs_lit = m_arith.mk_ge(var, e2); - } + } } abs_cube.push_back(abs_lit); if (contains_selects(abs_lit, m)) { @@ -464,7 +464,7 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { if (ub) tout << mk_pp(ub, m); else tout << "none"; tout << "\n";); - if (!lb && !ub) + if (!lb && !ub) return false; // -- guess lower or upper bound if missing @@ -542,46 +542,50 @@ bool lemma_quantifier_generalizer::generalize (lemma_ref &lemma, app *term) { return false; } -bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &c, expr_ref &pattern, unsigned &stride) { +bool lemma_quantifier_generalizer::find_stride(expr_ref_vector &cube, + expr_ref &pattern, + unsigned &stride) { expr_ref tmp(m); - tmp = mk_and(c); + tmp = mk_and(cube); normalize(tmp, tmp, false, true); - c.reset(); - flatten_and(tmp, c); + cube.reset(); + flatten_and(tmp, cube); app_ref_vector indices(m); - get_select_indices(pattern, indices, m); + get_select_indices(pattern, indices); - // TODO - if (indices.size() > 1) - return false; + CTRACE("spacer_qgen", indices.empty(), + tout << "Found no select indices in: " << pattern << "\n";); + + // TBD: handle multi-dimensional arrays and literals with multiple + // select terms + if (indices.size() != 1) return false; app *p_index = indices.get(0); - if (is_var(p_index)) return false; - std::vector instances; - for (expr* lit : c) { + unsigned_vector instances; + for (expr* lit : cube) { if (!contains_selects(lit, m)) continue; indices.reset(); - get_select_indices(lit, indices, m); + get_select_indices(lit, indices); - // TODO: - if (indices.size() > 1) + // TBD: handle multi-dimensional arrays + if (indices.size() != 1) continue; app *candidate = indices.get(0); unsigned size = p_index->get_num_args(); unsigned matched = 0; - for (unsigned p=0; p < size; p++) { + for (unsigned p = 0; p < size; p++) { expr *arg = p_index->get_arg(p); if (is_var(arg)) { rational val; - if (p < candidate->get_num_args() && - m_arith.is_numeral(candidate->get_arg(p), val) && + if (p < candidate->get_num_args() && + m_arith.is_numeral(candidate->get_arg(p), val) && val.is_unsigned()) { instances.push_back(val.get_unsigned()); } diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp index 42b40c665..3ea0917b7 100644 --- a/src/muz/spacer/spacer_util.cpp +++ b/src/muz/spacer/spacer_util.cpp @@ -900,17 +900,22 @@ namespace { struct collect_indices { app_ref_vector& m_indices; array_util a; - collect_indices(app_ref_vector& indices): m_indices(indices), a(indices.get_manager()) {} + collect_indices(app_ref_vector& indices): m_indices(indices), + a(indices.get_manager()) {} void operator()(expr* n) {} void operator()(app* n) { - if (a.is_select(n)) - for (unsigned i = 1; i < n->get_num_args(); ++i) - if (is_app(n->get_arg(i))) - m_indices.push_back(to_app(n->get_arg(i))); + if (a.is_select(n)) { + // for all but first argument + for (unsigned i = 1; i < n->get_num_args(); ++i) { + expr *arg = n->get_arg(i); + if (is_app(arg)) + m_indices.push_back(to_app(arg)); + } + } } }; - void get_select_indices(expr* fml, app_ref_vector &indices, ast_manager& m) { + void get_select_indices(expr* fml, app_ref_vector &indices) { collect_indices ci(indices); for_each_expr(ci, fml); } diff --git a/src/muz/spacer/spacer_util.h b/src/muz/spacer/spacer_util.h index 9912769c5..8da574d0e 100644 --- a/src/muz/spacer/spacer_util.h +++ b/src/muz/spacer/spacer_util.h @@ -121,7 +121,7 @@ namespace spacer { void mbqi_project(model &mdl, app_ref_vector &vars, expr_ref &fml); bool contains_selects (expr* fml, ast_manager& m); - void get_select_indices (expr* fml, app_ref_vector& indices, ast_manager& m); + void get_select_indices (expr* fml, app_ref_vector& indices); void find_decls (expr* fml, app_ref_vector& decls, std::string& prefix);