diff --git a/scripts/update_api.py b/scripts/update_api.py index b082c96e1..22c0dea99 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1665,6 +1665,7 @@ for v in ('Z3_LIBRARY_PATH', 'PATH', 'PYTHONPATH'): _all_dirs.extend(_default_dirs) +_failures = [] for d in _all_dirs: try: d = os.path.realpath(d) @@ -1673,14 +1674,16 @@ for d in _all_dirs: if os.path.isfile(d): _lib = ctypes.CDLL(d) break - except: + except Exception as e: + _failures += [e] pass if _lib is None: # If all else failed, ask the system to find it. try: _lib = ctypes.CDLL('libz3.%s' % _ext) - except: + except Exception as e: + _failures += [e] pass if _lib is None: diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index 5828b0fcd..4f4da6bd4 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -384,12 +384,14 @@ extern "C" { Z3_symbol Z3_API Z3_get_decl_name(Z3_context c, Z3_func_decl d) { LOG_Z3_get_decl_name(c, d); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, nullptr); return of_symbol(to_func_decl(d)->get_name()); } unsigned Z3_API Z3_get_decl_num_parameters(Z3_context c, Z3_func_decl d) { LOG_Z3_get_decl_num_parameters(c, d); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); return to_func_decl(d)->get_num_parameters(); } @@ -397,6 +399,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_parameter_kind(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, Z3_PARAMETER_INT); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); return Z3_PARAMETER_INT; @@ -429,6 +432,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_int_parameter(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); return 0; @@ -446,6 +450,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_double_parameter(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); return 0; @@ -463,6 +468,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_symbol_parameter(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); return nullptr; @@ -480,6 +486,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_sort_parameter(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -497,6 +504,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_ast_parameter(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -514,6 +522,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_func_decl_parameter(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); @@ -531,6 +540,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_decl_rational_parameter(c, d, idx); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, ""); if (idx >= to_func_decl(d)->get_num_parameters()) { SET_ERROR_CODE(Z3_IOB, nullptr); return ""; @@ -549,6 +559,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_sort_name(c, t); RESET_ERROR_CODE(); + CHECK_VALID_AST(t, nullptr); return of_symbol(to_sort(t)->get_name()); Z3_CATCH_RETURN(nullptr); } @@ -567,6 +578,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_arity(c, d); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); return to_func_decl(d)->get_arity(); Z3_CATCH_RETURN(0); } @@ -575,6 +587,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_domain_size(c, d); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); return to_func_decl(d)->get_arity(); Z3_CATCH_RETURN(0); } @@ -583,6 +596,7 @@ extern "C" { Z3_TRY; LOG_Z3_get_domain(c, d, i); RESET_ERROR_CODE(); + CHECK_VALID_AST(d, 0); if (i >= to_func_decl(d)->get_arity()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index b5458cff2..4d0009fbe 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -26,6 +26,7 @@ Revision History: #include "ast/fpa_decl_plugin.h" bool is_numeral_sort(Z3_context c, Z3_sort ty) { + if (!ty) return false; sort * _ty = to_sort(ty); family_id fid = _ty->get_family_id(); if (fid != mk_c(c)->get_arith_fid() && @@ -145,7 +146,8 @@ extern "C" { Z3_bool Z3_API Z3_is_numeral_ast(Z3_context c, Z3_ast a) { Z3_TRY; LOG_Z3_is_numeral_ast(c, a); - RESET_ERROR_CODE(); + RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, Z3_FALSE); expr* e = to_expr(a); return mk_c(c)->autil().is_numeral(e) || @@ -160,11 +162,8 @@ extern "C" { Z3_TRY; // This function is not part of the public API RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, Z3_FALSE); expr* e = to_expr(a); - if (!e) { - SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return Z3_FALSE; - } if (mk_c(c)->autil().is_numeral(e, r)) { return Z3_TRUE; } @@ -187,6 +186,7 @@ extern "C" { // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_string(c, a); RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, Z3_FALSE); rational r; Z3_bool ok = Z3_get_numeral_rational(c, a, r); if (ok == Z3_TRUE) { @@ -232,11 +232,8 @@ extern "C" { Z3_TRY; LOG_Z3_get_numeral_decimal_string(c, a, precision); RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, ""); expr* e = to_expr(a); - if (!e) { - SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); - return ""; - } rational r; arith_util & u = mk_c(c)->autil(); if (u.is_numeral(e, r) && !r.is_int()) { @@ -267,6 +264,7 @@ extern "C" { // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_small(c, a, num, den); RESET_ERROR_CODE(); + CHECK_IS_EXPR(a, Z3_FALSE); rational r; Z3_bool ok = Z3_get_numeral_rational(c, a, r); if (ok == Z3_TRUE) { @@ -292,6 +290,7 @@ extern "C" { // This function invokes Z3_get_numeral_int64, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_int(c, v, i); RESET_ERROR_CODE(); + CHECK_IS_EXPR(v, Z3_FALSE); if (!i) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; @@ -310,6 +309,7 @@ extern "C" { // This function invokes Z3_get_numeral_uint64, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_uint(c, v, u); RESET_ERROR_CODE(); + CHECK_IS_EXPR(v, Z3_FALSE); if (!u) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; @@ -328,6 +328,7 @@ extern "C" { // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_uint64(c, v, u); RESET_ERROR_CODE(); + CHECK_IS_EXPR(v, Z3_FALSE); if (!u) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; @@ -348,6 +349,7 @@ extern "C" { // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_int64(c, v, i); RESET_ERROR_CODE(); + CHECK_IS_EXPR(v, Z3_FALSE); if (!i) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; @@ -367,6 +369,7 @@ extern "C" { // This function invokes Z3_get_numeral_rational, but it is still ok to add LOG command here because it does not return a Z3 object. LOG_Z3_get_numeral_rational_int64(c, v, num, den); RESET_ERROR_CODE(); + CHECK_IS_EXPR(v, Z3_FALSE); if (!num || !den) { SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); return Z3_FALSE; diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index a927df3b5..74166a78b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2406,7 +2406,6 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s *m_trace_stream << " #" << patterns[i]->get_id(); } *m_trace_stream << " #" << body->get_id() << "\n"; - } return r; @@ -2420,6 +2419,9 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort sort* s = autil.mk_array_sort(num_decls, decl_sorts, ::get_sort(body)); quantifier * new_node = new (mem) quantifier(num_decls, decl_sorts, decl_names, body, s); quantifier * r = register_node(new_node); + if (m_trace_stream && r == new_node) { + *m_trace_stream << "[mk-lambda] #" << r->get_id() << ": #" << body->get_id() << "\n"; + } return r; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index a65351a50..84c05d53e 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1881,7 +1881,7 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) { unsigned sz = s.length(); expr_ref_vector es(m()); for (unsigned j = 0; j < sz; ++j) { - es.push_back(m_util.str.mk_char(s, j)); + es.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, j))); } es.append(m_lhs.size() - i, m_lhs.c_ptr() + i); for (unsigned j = 0; j < sz; ++j) { @@ -1896,9 +1896,8 @@ bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) { if (m_util.str.is_string(b, s)) { expr* all = m_util.re.mk_full_seq(m_util.re.mk_re(m().get_sort(b))); - std::cout << sort_ref(m().get_sort(all), m()) << "\n"; disj.push_back(m_util.re.mk_in_re(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i), - m_util.re.mk_concat(all, m_util.str.mk_concat(m_util.re.mk_to_re(b), all)))); + m_util.re.mk_concat(all, m_util.re.mk_concat(m_util.re.mk_to_re(b), all)))); return true; } diff --git a/src/smt/old_interval.cpp b/src/smt/old_interval.cpp index da589893b..114f9cf29 100644 --- a/src/smt/old_interval.cpp +++ b/src/smt/old_interval.cpp @@ -561,15 +561,24 @@ interval & interval::operator/=(interval const & other) { TRACE("interval", other.display_with_dependencies(tout);); if (other.m_lower.is_pos() || (other.m_lower.is_zero() && other.m_lower_open)) { // other.lower > 0 + // x in ([0, 0] / [other.lo, other.up]), for other.lo > 0 + // <=> + // x >= 0: because y*x >= 0 & y > 0 + // x <= 0: because y*x <= 0 & y > 0 m_lower_dep = join(m_lower_dep, other.m_lower_dep); m_upper_dep = join(m_upper_dep, other.m_lower_dep); } else { // assertion must hold since !other.contains_zero() - SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open)); + SASSERT(other.m_upper.is_neg() || (other.m_upper.is_zero() && other.m_upper_open)); // other.upper < 0 - m_lower_dep = join(m_lower_dep, other.m_upper_dep); - m_upper_dep = join(m_upper_dep, other.m_upper_dep); + // x in ([0, 0] / [other.lo, other.up]), for up < 0 + // <=> + // x >= 0: because y*x <= 0 & y < 0 + // x <= 0: because y*x >= 0 & y < 0 + v_dependency* lower_dep = m_lower_dep; + m_lower_dep = join(m_upper_dep, other.m_upper_dep); + m_upper_dep = join(lower_dep, other.m_upper_dep); } return *this; } diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index aa7063dc1..6216d6592 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -228,7 +228,6 @@ namespace smt { } void context::copy_plugins(context& src, context& dst) { - // copy theory plugins for (theory* old_th : src.m_theory_set) { theory * new_th = old_th->mk_fresh(&dst); @@ -236,8 +235,8 @@ namespace smt { } } - context * context::mk_fresh(symbol const * l, smt_params * p) { - context * new_ctx = alloc(context, m_manager, p == nullptr ? m_fparams : *p); + context * context::mk_fresh(symbol const * l, smt_params * p, params_ref const& pa) { + context * new_ctx = alloc(context, m_manager, p ? *p : m_fparams, pa); new_ctx->set_logic(l == nullptr ? m_setup.get_logic() : *l); copy_plugins(*this, *new_ctx); return new_ctx; diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index b77f63e41..ff92f6f95 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -1493,7 +1493,7 @@ namespace smt { If l == 0, then the logic of this context is used in the new context. If p == 0, then this->m_params is used */ - context * mk_fresh(symbol const * l = nullptr, smt_params * p = nullptr); + context * mk_fresh(symbol const * l = nullptr, smt_params * smtp = nullptr, params_ref const & p = params_ref()); static void copy(context& src, context& dst); diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp index 8a75dc48c..2a46fd07f 100644 --- a/src/smt/smt_context_pp.cpp +++ b/src/smt/smt_context_pp.cpp @@ -422,8 +422,6 @@ namespace smt { out << "(check-sat)\n"; } -#define BUFFER_SZ 128 - unsigned context::display_lemma_as_smt_problem(unsigned num_antecedents, literal const * antecedents, literal consequent, symbol const& logic) const { std::stringstream strm; strm << "lemma_" << (++m_lemma_id) << ".smt2"; diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index ae023078a..1414cb522 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -678,8 +678,18 @@ namespace smt { push_trail(set_merge_tf_trail(n)); n->m_merge_tf = true; lbool val = get_assignment(v); - if (val != l_undef) - push_eq(n, val == l_true ? m_true_enode : m_false_enode, eq_justification(literal(v, val == l_false))); + switch (val) { + case l_undef: + break; + case l_true: + if (n->get_root() != m_true_enode->get_root()) + push_eq(n, m_true_enode, eq_justification(literal(v, false))); + break; + case l_false: + if (n->get_root() != m_false_enode->get_root()) + push_eq(n, m_false_enode, eq_justification(literal(v, true))); + break; + } } } diff --git a/src/smt/smt_literal.h b/src/smt/smt_literal.h index 7f554d740..598335cff 100644 --- a/src/smt/smt_literal.h +++ b/src/smt/smt_literal.h @@ -103,7 +103,7 @@ namespace smt { void display_compact(std::ostream & out, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map); - void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = " "); + void display_verbose(std::ostream & out, ast_manager& m, unsigned num_lits, literal const * lits, expr * const * bool_var2expr_map, char const* sep = "\n"); template void neg_literals(unsigned num_lits, literal const * lits, T & result) { diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp index f4c5c09d9..0fea4d13d 100644 --- a/src/smt/smt_model_checker.cpp +++ b/src/smt/smt_model_checker.cpp @@ -384,10 +384,13 @@ namespace smt { m_fparams = alloc(smt_params, m_context->get_fparams()); m_fparams->m_relevancy_lvl = 0; // no relevancy since the model checking problems are quantifier free m_fparams->m_case_split_strategy = CS_ACTIVITY; // avoid warning messages about smt.case_split >= 3. + m_fparams->m_arith_dump_lemmas = false; } if (!m_aux_context) { symbol logic; - m_aux_context = m_context->mk_fresh(&logic, m_fparams.get()); + params_ref p; + p.set_bool("arith.dump_lemmas", false); + m_aux_context = m_context->mk_fresh(&logic, m_fparams.get(), p); } } diff --git a/src/smt/smt_setup.cpp b/src/smt/smt_setup.cpp index 932ca597f..9e38fef69 100644 --- a/src/smt/smt_setup.cpp +++ b/src/smt/smt_setup.cpp @@ -627,9 +627,6 @@ namespace smt { m_params.m_phase_selection = PS_CACHING_CONSERVATIVE2; m_params.m_random_initial_activity = IA_ZERO; } - // if (st.m_num_arith_ineqs == st.m_num_diff_ineqs && st.m_num_arith_eqs == st.m_num_diff_eqs && st.arith_k_sum_is_small()) - // m_context.register_plugin(new smt::theory_si_arith(m_manager, m_params)); - // else setup_i_arith(); setup_arrays(); } @@ -654,7 +651,7 @@ namespace smt { // m_params.m_ng_lift_ite = LI_FULL; TRACE("setup", tout << "max_eager_multipatterns: " << m_params.m_qi_max_eager_multipatterns << "\n";); - setup_i_arith(); + m_context.register_plugin(alloc(smt::theory_i_arith, m_manager, m_params)); setup_arrays(); } @@ -832,7 +829,10 @@ namespace smt { m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); break; case AS_NEW_ARITH: - setup_lra_arith(); + if (st.m_num_non_linear != 0) + m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); + else + setup_lra_arith(); break; default: m_context.register_plugin(alloc(smt::theory_mi_arith, m_manager, m_params)); @@ -994,7 +994,7 @@ namespace smt { } if (st.num_theories() == 2 && st.has_uf() && is_arith(st)) { - if (!st.m_has_real) + if (!st.m_has_real && st.m_num_non_linear == 0) setup_QF_UFLIA(st); else if (!st.m_has_int && st.m_num_non_linear == 0) setup_QF_UFLRA(); diff --git a/src/smt/smt_theory.cpp b/src/smt/smt_theory.cpp index b5ad68adc..63c6d7417 100644 --- a/src/smt/smt_theory.cpp +++ b/src/smt/smt_theory.cpp @@ -123,7 +123,7 @@ namespace smt { context & ctx = get_context(); app * eq = ctx.mk_eq_atom(a, b); TRACE("mk_var_bug", tout << "mk_eq: " << eq->get_id() << " " << a->get_id() << " " << b->get_id() << "\n"; - tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager());); + tout << mk_ll_pp(a, get_manager()) << "\n" << mk_ll_pp(b, get_manager());); ctx.internalize(eq, gate_ctx); return ctx.get_literal(eq); } diff --git a/src/smt/theory_arith_aux.h b/src/smt/theory_arith_aux.h index daf285a54..9526637e9 100644 --- a/src/smt/theory_arith_aux.h +++ b/src/smt/theory_arith_aux.h @@ -731,35 +731,34 @@ namespace smt { template void theory_arith::derived_bound::push_justification(antecedents& a, numeral const& coeff, bool proofs_enabled) { + TRACE("arith", tout << m_lits << " " << m_eqs.size() << "\n";); if (proofs_enabled) { - for (unsigned i = 0; i < m_lits.size(); ++i) { - a.push_lit(m_lits[i], coeff, proofs_enabled); - } - for (unsigned i = 0; i < m_eqs.size(); ++i) { - a.push_eq(m_eqs[i], coeff, proofs_enabled); - } + for (literal l : m_lits) + a.push_lit(l, coeff, proofs_enabled); + for (auto const& e : m_eqs) + a.push_eq(e, coeff, proofs_enabled); } else { a.append(m_lits.size(), m_lits.c_ptr()); - a.append(m_eqs.size(), m_eqs.c_ptr()); + a.append(m_eqs.size(), m_eqs.c_ptr()); } } template void theory_arith::derived_bound::display(theory_arith const& th, std::ostream& out) const { - out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value(); - ast_manager& m = th.get_manager(); - for (unsigned i = 0; i < m_eqs.size(); ++i) { - enode* a = m_eqs[i].first; - enode* b = m_eqs[i].second; + out << "v" << bound::get_var() << " " << bound::get_bound_kind() << " " << bound::get_value() << "\n"; + out << "expr: " << mk_pp(th.var2expr(bound::get_var()), m) << "\n"; + + for (auto const& e : m_eqs) { + enode* a = e.first; + enode* b = e.second; out << " "; out << "#" << a->get_owner_id() << " " << mk_pp(a->get_owner(), m) << " = " - << "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m); + << "#" << b->get_owner_id() << " " << mk_pp(b->get_owner(), m) << "\n"; } - for (unsigned i = 0; i < m_lits.size(); ++i) { - literal l = m_lits[i]; - out << " " << l << ":"; th.get_context().display_detailed_literal(out, l); + for (literal l : m_lits) { + out << l << ":"; th.get_context().display_detailed_literal(out, l) << "\n"; } } @@ -882,13 +881,10 @@ namespace smt { } TRACE("derived_bound", tout << "explanation:\n"; - literal_vector::const_iterator it1 = new_bound->m_lits.begin(); - literal_vector::const_iterator end1 = new_bound->m_lits.end(); - for (; it1 != end1; ++it1) tout << *it1 << " "; + for (literal l : new_bound->m_lits) tout << l << " "; tout << " "; - eq_vector::const_iterator it2 = new_bound->m_eqs.begin(); - eq_vector::const_iterator end2 = new_bound->m_eqs.end(); - for (; it2 != end2; ++it2) tout << "#" << it2->first->get_owner_id() << "=#" << it2->second->get_owner_id() << " "; + for (auto const& e : new_bound->m_eqs) + tout << "#" << e.first->get_owner_id() << "=#" << e.second->get_owner_id() << " "; tout << "\n";); DEBUG_CODE(CTRACE("derived_bound", k != val, tout << "k: " << k << ", k_norm: " << k_norm << ", val: " << val << "\n";);); SASSERT(k == val); diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index cbd41f08c..01eb8a3d4 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -1708,7 +1708,7 @@ namespace smt { template theory* theory_arith::mk_fresh(context* new_ctx) { - return alloc(theory_arith, new_ctx->get_manager(), m_params); + return alloc(theory_arith, new_ctx->get_manager(), new_ctx->get_fparams()); } template @@ -1853,10 +1853,7 @@ namespace smt { void theory_arith::restore_assignment() { CASSERT("arith", valid_row_assignment()); TRACE("restore_assignment_bug", tout << "START restore_assignment...\n";); - typename svector::iterator it = m_update_trail_stack.begin(); - typename svector::iterator end = m_update_trail_stack.end(); - for(; it != end; ++it) { - theory_var v = *it; + for (theory_var v : m_update_trail_stack) { TRACE("restore_assignment_bug", tout << "restoring v" << v << " <- " << m_old_value[v] << "\n";); SASSERT(!is_quasi_base(v)); SASSERT(m_in_update_trail_stack.contains(v)); @@ -2237,11 +2234,7 @@ namespace smt { theory_var best = null_theory_var; inf_numeral best_error; inf_numeral curr_error; - typename var_heap::iterator it = m_to_patch.begin(); - typename var_heap::iterator end = m_to_patch.end(); - //unsigned n = 0; - for (; it != end; ++it) { - theory_var v = *it; + for (theory_var v : m_to_patch) { if (below_lower(v)) curr_error = lower(v)->get_value() - get_value(v); else if (above_upper(v)) @@ -2391,10 +2384,11 @@ namespace smt { TRACE("sign_row_conflict", tout << "v" << x_i << " is_below: " << is_below << " delta: " << delta << "\n"; display_var(tout, x_i); tout << "is_below_lower: " << below_lower(x_i) << ", is_above_upper: " << above_upper(x_i) << "\n"; + display_row(tout, r, true); + display_row(tout, r, false); ante.display(tout);); set_conflict(ante, ante, "farkas"); - // display_bounds_in_smtlib(); } // ----------------------------------- @@ -2535,10 +2529,9 @@ namespace smt { antecedents ante(*this); b1->push_justification(ante, numeral(1), coeffs_enabled()); b2->push_justification(ante, numeral(1), coeffs_enabled()); - - set_conflict(ante, ante, "farkas"); TRACE("arith_conflict", tout << "bound conflict v" << b1->get_var() << "\n"; tout << "bounds: " << b1 << " " << b2 << "\n";); + set_conflict(ante, ante, "farkas"); } // ----------------------------------- @@ -2771,8 +2764,10 @@ namespace smt { template void theory_arith::explain_bound(row const & r, int idx, bool is_lower, inf_numeral & delta, antecedents& ante) { SASSERT(delta >= inf_numeral::zero()); - if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty())) + TRACE("arith_conflict", tout << "relax: " << relax_bounds() << " lits: " << ante.lits().size() << " eqs: " << ante.eqs().size() << " idx: " << idx << "\n";); + if (!relax_bounds() && (!ante.lits().empty() || !ante.eqs().empty())) { return; + } context & ctx = get_context(); row_entry const & entry = r[idx]; numeral coeff = entry.m_coeff; @@ -2790,9 +2785,11 @@ namespace smt { if (!it->is_dead() && idx != idx2) { bound * b = get_bound(it->m_var, is_lower ? it->m_coeff.is_pos() : it->m_coeff.is_neg()); SASSERT(b); - if (!b->has_justification()) + if (!b->has_justification()) { continue; + } if (!relax_bounds() || delta.is_zero()) { + TRACE("propagate_bounds", tout << "push justification: v" << it->m_var << "\n";); b->push_justification(ante, it->m_coeff, coeffs_enabled()); continue; } @@ -2821,10 +2818,7 @@ namespace smt { inf_numeral k_2 = k_1; atom * new_atom = nullptr; atoms const & as = m_var_occs[it->m_var]; - typename atoms::const_iterator it = as.begin(); - typename atoms::const_iterator end = as.end(); - for (; it != end; ++it) { - atom * a = *it; + for (atom * a : as) { if (a == b) continue; bool_var bv = a->get_bool_var(); @@ -2880,10 +2874,7 @@ namespace smt { atoms const & as = m_var_occs[v]; inf_numeral const & epsilon = get_epsilon(v); inf_numeral delta; - typename atoms::const_iterator it = as.begin(); - typename atoms::const_iterator end = as.end(); - for (; it != end; ++it) { - atom * a = *it; + for (atom* a : as) { bool_var bv = a->get_bool_var(); literal l(bv); if (get_context().get_assignment(bv) == l_undef) { @@ -2952,8 +2943,29 @@ namespace smt { context & ctx = get_context(); if (dump_lemmas()) { TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";); - ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), + unsigned id = ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), l); + +#if 1 + if (id == 394) { + enable_trace("sign_row_conflict"); + enable_trace("nl_arith_bug"); + enable_trace("nl_evaluate"); + enable_trace("propagate_bounds"); + enable_trace("propagate_bounds_bug"); + enable_trace("arith_conflict"); + enable_trace("non_linear"); + enable_trace("non_linear_bug"); + } + SASSERT(id != 395); + if (id == 396) { + disable_trace("nl_arith_bug"); + disable_trace("propagate_bounds"); + disable_trace("arith_conflict"); + disable_trace("non_linear"); + disable_trace("non_linear_bug"); + } +#endif } } @@ -2961,8 +2973,28 @@ namespace smt { void theory_arith::dump_lemmas(literal l, derived_bound const& ante) { context & ctx = get_context(); if (dump_lemmas()) { - ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), + unsigned id = ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), l); +#if 1 + if (id == 394) { + enable_trace("nl_arith_bug"); + enable_trace("nl_evaluate"); + enable_trace("propagate_bounds"); + enable_trace("arith_conflict"); + enable_trace("propagate_bounds_bug"); + enable_trace("non_linear"); + enable_trace("non_linear_bug"); + } + SASSERT(id != 395); + if (id == 396) { + enable_trace("sign_row_conflict"); + disable_trace("nl_arith_bug"); + disable_trace("propagate_bounds"); + disable_trace("arith_conflict"); + disable_trace("non_linear"); + disable_trace("non_linear_bug"); + } +#endif } } @@ -2972,12 +3004,13 @@ namespace smt { context & ctx = get_context(); antecedents ante(*this); explain_bound(r, idx, is_lower, delta, ante); - dump_lemmas(l, ante); TRACE("propagate_bounds", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";); + dump_lemmas(l, ante); + if (ante.lits().size() < small_lemma_size() && ante.eqs().empty()) { literal_vector & lits = m_tmp_literal_vector2; lits.reset(); @@ -3060,14 +3093,14 @@ namespace smt { template void theory_arith::set_conflict(antecedents const& ante, antecedents& bounds, char const* proof_rule) { - dump_lemmas(false_literal, ante); set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule); + dump_lemmas(false_literal, ante); } template void theory_arith::set_conflict(derived_bound const& ante, antecedents& bounds, char const* proof_rule) { - dump_lemmas(false_literal, ante); set_conflict(ante.lits().size(), ante.lits().c_ptr(), ante.eqs().size(), ante.eqs().c_ptr(), bounds, proof_rule); + dump_lemmas(false_literal, ante); } template diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index ba6648dac..c27d3b44a 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -58,7 +58,6 @@ namespace smt { void theory_arith::mark_var(theory_var v, svector & vars, var_set & already_found) { if (already_found.contains(v)) return; - TRACE("non_linear", tout << "marking: v" << v << "\n";); already_found.insert(v); vars.push_back(v); } @@ -71,8 +70,7 @@ namespace smt { if (is_pure_monomial(v)) { expr * n = var2expr(v); SASSERT(m_util.is_mul(n)); - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) { - expr * curr = to_app(n)->get_arg(i); + for (expr * curr : *to_app(n)) { theory_var v = expr2var(curr); SASSERT(v != null_theory_var); mark_var(v, vars, already_found); @@ -118,22 +116,19 @@ namespace smt { var_set already_found; row_set already_visited_rows; context & ctx = get_context(); - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (theory_var v : m_nl_monomials) { expr * n = var2expr(v); if (ctx.is_relevant(n)) mark_var(v, vars, already_found); } - for (unsigned idx = 0; idx < vars.size(); idx++) { - TRACE("non_linear", tout << "marking dependents of: v" << vars[idx] << "\n";); - mark_dependents(vars[idx], vars, already_found, already_visited_rows); + // NB: vars changes inside of loop + for (unsigned idx = 0; idx < vars.size(); ++idx) { + theory_var v = vars[idx]; + TRACE("non_linear", tout << "marking dependents of: v" << v << "\n";); + mark_dependents(v, vars, already_found, already_visited_rows); } TRACE("non_linear", tout << "variables in non linear cluster:\n"; - svector::const_iterator it = vars.begin(); - svector::const_iterator end = vars.end(); - for (; it != end; ++it) tout << "v" << *it << " "; + for (theory_var v : vars) tout << "v" << v << " "; tout << "\n";); } @@ -227,9 +222,8 @@ namespace smt { SASSERT(!m_util.is_numeral(m)); if (m_util.is_mul(m)) { unsigned num_vars = 0; - expr * var = nullptr; - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - expr * curr = to_app(m)->get_arg(i); + expr * var = nullptr; + for (expr * curr : *to_app(m)) { if (var != curr) { num_vars++; var = curr; @@ -254,9 +248,7 @@ namespace smt { unsigned curr_idx = 0; expr * var = nullptr; unsigned power = 0; - unsigned j; - for (j = 0; j < to_app(m)->get_num_args(); j++) { - expr * arg = to_app(m)->get_arg(j); + for (expr * arg : *to_app(m)) { if (var == nullptr) { var = arg; power = 1; @@ -360,6 +352,7 @@ namespace smt { template interval theory_arith::evaluate_as_interval(expr * n) { expr* arg; + rational val; TRACE("nl_evaluate", tout << "evaluating: " << mk_bounded_pp(n, get_manager(), 10) << "\n";); if (has_var(n)) { TRACE("nl_evaluate", tout << "n has a variable associated with it\n";); @@ -370,8 +363,8 @@ namespace smt { else if (m_util.is_add(n)) { TRACE("nl_evaluate", tout << "is add\n";); interval r(m_dep_manager, rational(0)); - for (unsigned i = 0; i < to_app(n)->get_num_args(); i++) { - r += evaluate_as_interval(to_app(n)->get_arg(i)); + for (expr* arg : *to_app(n)) { + r += evaluate_as_interval(arg); } TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); return r; @@ -388,31 +381,28 @@ namespace smt { it.expt(power); r *= it; } - TRACE("cross_nested_eval_bug", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); + TRACE("nl_evaluate", display_nested_form(tout, n); tout << "\ninterval: " << r << "\n";); return r; } else if (m_util.is_to_real(n, arg)) { return evaluate_as_interval(arg); } + else if (m_util.is_numeral(n, val)) { + TRACE("nl_evaluate", tout << "is numeral\n";); + return interval(m_dep_manager, val); + } else { - rational val; - if (m_util.is_numeral(n, val)) { - TRACE("nl_evaluate", tout << "is numeral\n";); - return interval(m_dep_manager, val); - } - else { - TRACE("nl_evaluate", tout << "is unknown\n";); - return interval(m_dep_manager); - } + TRACE("nl_evaluate", tout << "is unknown\n";); + return interval(m_dep_manager); } } template - void theory_arith::display_monomial(std::ostream & out, expr * m) const { + void theory_arith::display_monomial(std::ostream & out, expr * n) const { bool first = true; - unsigned num_vars = get_num_vars_in_monomial(m); + unsigned num_vars = get_num_vars_in_monomial(n); for (unsigned i = 0; i < num_vars; i++) { - var_power_pair p = get_var_and_degree(m, i); + var_power_pair p = get_var_and_degree(n, i); SASSERT(p.first != 0); if (first) first = false; else out << " * "; out << mk_bounded_pp(p.first, get_manager()) << "^" << p.second; @@ -425,10 +415,8 @@ namespace smt { m_dep_manager.linearize(dep, bounds); m_tmp_lit_set.reset(); m_tmp_eq_set.reset(); - ptr_vector::const_iterator it = bounds.begin(); - ptr_vector::const_iterator end = bounds.end(); - for (; it != end; ++it) { - bound * b = static_cast(*it); + for (void* _b : bounds) { + bound * b = static_cast(_b); accumulate_justification(*b, new_bound, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set); } } @@ -544,21 +532,19 @@ namespace smt { the method returns without doing anything. */ template - bool theory_arith::propagate_nl_downward(expr * m, unsigned i) { - SASSERT(is_pure_monomial(m)); - SASSERT(i < get_num_vars_in_monomial(m)); - var_power_pair p = get_var_and_degree(m, i); + bool theory_arith::propagate_nl_downward(expr * n, unsigned i) { + SASSERT(is_pure_monomial(n)); + SASSERT(i < get_num_vars_in_monomial(n)); + var_power_pair p = get_var_and_degree(n, i); expr * v = p.first; unsigned power = p.second; - TRACE("propagate_nl_downward", tout << "m: " << mk_ismt2_pp(m, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) << - "\npower: " << power << "\n";); if (power != 1) return false; // TODO: remove, when the n-th root is implemented in interval. - unsigned num_vars = get_num_vars_in_monomial(m); + unsigned num_vars = get_num_vars_in_monomial(n); interval other_bounds(m_dep_manager, rational(1)); // TODO: the following code can be improved it is quadratic on the degree of the monomial. for (unsigned i = 0; i < num_vars; i++) { - var_power_pair p = get_var_and_degree(m, i); + var_power_pair p = get_var_and_degree(n, i); if (p.first == v) continue; expr * var = p.first; @@ -567,7 +553,13 @@ namespace smt { } if (other_bounds.contains_zero()) return false; // interval division requires that divisor doesn't contain 0. - interval r = mk_interval_for(m); + interval r = mk_interval_for(n); + TRACE("nl_arith_bug", tout << "m: " << mk_ismt2_pp(n, get_manager()) << "\nv: " << mk_ismt2_pp(v, get_manager()) << + "\npower: " << power << "\n"; + tout << "num_vars: " << num_vars << "\n"; + display_interval(tout << "monomial bounds\n", r); + display_interval(tout << "other bounds\n", other_bounds); + ); r /= other_bounds; return update_bounds_using_interval(v, r); } @@ -907,7 +899,6 @@ namespace smt { } TRACE("non_linear_bug", tout << "enode: " << get_context().get_enode(rhs) << " enode_id: " << get_context().get_enode(rhs)->get_owner_id() << "\n";); theory_var new_v = expr2var(rhs); - TRACE("non_linear_bug", ctx.display(tout);); SASSERT(new_v != null_theory_var); new_lower = alloc(derived_bound, new_v, inf_numeral(0), B_LOWER); new_upper = alloc(derived_bound, new_v, inf_numeral(0), B_UPPER); @@ -953,19 +944,17 @@ namespace smt { } accumulate_justification(*l, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set); - TRACE("non_linear", - for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) { - ctx.display_detailed_literal(tout, new_lower->m_lits[j]); - tout << " "; + TRACE("non_linear", + for (literal l : new_lower->m_lits) { + ctx.display_detailed_literal(tout, l) << " "; } tout << "\n";); accumulate_justification(*u, *new_lower, numeral::zero(), m_tmp_lit_set, m_tmp_eq_set); TRACE("non_linear", - for (unsigned j = 0; j < new_lower->m_lits.size(); ++j) { - ctx.display_detailed_literal(tout, new_lower->m_lits[j]); - tout << " "; + for (literal l : new_lower->m_lits) { + ctx.display_detailed_literal(tout, l) << " "; } tout << "\n";); @@ -977,9 +966,8 @@ namespace smt { TRACE("non_linear", new_lower->display(*this, tout << "lower: "); tout << "\n"; new_upper->display(*this, tout << "upper: "); tout << "\n"; - for (unsigned j = 0; j < new_upper->m_lits.size(); ++j) { - ctx.display_detailed_literal(tout, new_upper->m_lits[j]); - tout << " "; + for (literal lit : new_upper->m_lits) { + ctx.display_detailed_literal(tout, lit) << " "; } tout << "\n";); @@ -1123,14 +1111,14 @@ namespace smt { continue; if (is_pure_monomial(v)) { expr * m = var2expr(v); - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - theory_var curr = expr2var(to_app(m)->get_arg(i)); + for (expr* arg : *to_app(m)) { + theory_var curr = expr2var(arg); if (m_tmp_var_set.contains(curr)) return true; } SASSERT(m == var2expr(v)); - for (unsigned i = 0; i < to_app(m)->get_num_args(); i++) { - theory_var curr = expr2var(to_app(m)->get_arg(i)); + for (expr* arg : *to_app(m)) { + theory_var curr = expr2var(arg); if (!is_fixed(curr)) m_tmp_var_set.insert(curr); } @@ -1936,10 +1924,7 @@ namespace smt { derived_bound b(null_theory_var, inf_numeral(0), B_LOWER); dependency2new_bound(d, b); set_conflict(b, ante, "arith_nl"); - TRACE("non_linear", - for (unsigned i = 0; i < b.m_lits.size(); ++i) { - tout << b.m_lits[i] << " "; - }); + TRACE("non_linear", for (literal lit : b.m_lits) tout << lit << " "; tout << "\n";); } /** @@ -2387,7 +2372,7 @@ namespace smt { elim_quasi_base_rows(); move_non_base_vars_to_bounds(); - TRACE("non_linear", tout << "processing non linear constraints...\n"; get_context().display(tout);); + TRACE("non_linear_verbose", tout << "processing non linear constraints...\n"; get_context().display(tout);); if (!make_feasible()) { TRACE("non_linear", tout << "failed to move variables to bounds.\n";); failed(); diff --git a/src/smt/theory_arith_pp.h b/src/smt/theory_arith_pp.h index 6579856a4..59d386292 100644 --- a/src/smt/theory_arith_pp.h +++ b/src/smt/theory_arith_pp.h @@ -391,19 +391,19 @@ namespace smt { void theory_arith::display_vars(std::ostream & out) const { out << "vars:\n"; int n = get_num_vars(); - int inf_vars = 0; - int int_inf_vars = 0; - for (theory_var v = 0; v < n; v++) { - if ((lower(v) && lower(v)->get_value() > get_value(v)) - || (upper(v) && upper(v)->get_value() < get_value(v))) - inf_vars++; - if (is_int(v) && !get_value(v).is_int()) - int_inf_vars++; - } - out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl; - for (theory_var v = 0; v < n; v++) { - display_var(out, v); - } + int inf_vars = 0; + int int_inf_vars = 0; + for (theory_var v = 0; v < n; v++) { + if ((lower(v) && lower(v)->get_value() > get_value(v)) + || (upper(v) && upper(v)->get_value() < get_value(v))) + inf_vars++; + if (is_int(v) && !get_value(v).is_int()) + int_inf_vars++; + } + out << "infeasibles = " << inf_vars << " int_inf = " << int_inf_vars << std::endl; + for (theory_var v = 0; v < n; v++) { + display_var(out, v); + } } template @@ -418,9 +418,9 @@ namespace smt { th.get_context().display_literals_verbose(out, lits().size(), lits().c_ptr()); if (!lits().empty()) out << "\n"; ast_manager& m = th.get_manager(); - for (unsigned i = 0; i < m_eqs.size(); ++i) { - out << mk_pp(m_eqs[i].first->get_owner(), m) << " "; - out << mk_pp(m_eqs[i].second->get_owner(), m) << "\n"; + for (auto const& e : m_eqs) { + out << mk_pp(e.first->get_owner(), m) << " "; + out << mk_pp(e.second->get_owner(), m) << "\n"; } return out; } @@ -431,27 +431,24 @@ namespace smt { m_dep_manager.linearize(dep, bounds); m_tmp_lit_set.reset(); m_tmp_eq_set.reset(); - ptr_vector::const_iterator it = bounds.begin(); - ptr_vector::const_iterator end = bounds.end(); - for (; it != end; ++it) { - bound * b = static_cast(*it); - out << " "; - b->display(*this, out); + for (void *_b : bounds) { + bound * b = static_cast(_b); + b->display(*this, out << "\n"); } } template void theory_arith::display_interval(std::ostream & out, interval const& i) { i.display(out); - display_deps(out << " lo:", i.get_lower_dependencies()); - display_deps(out << " hi:", i.get_upper_dependencies()); + display_deps(out << "\nlo:", i.get_lower_dependencies()); + display_deps(out << "\nhi:", i.get_upper_dependencies()); } template void theory_arith::display_atoms(std::ostream & out) const { out << "atoms:\n"; - for (unsigned i = 0; i < m_atoms.size(); i++) - display_atom(out, m_atoms[i], false); + for (atom * a : m_atoms) + display_atom(out, a, false); } template diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 873d1692d..261881a3b 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -138,9 +138,9 @@ namespace smt { void theory_bv::process_args(app * n) { context & ctx = get_context(); - unsigned num_args = n->get_num_args(); - for (unsigned i = 0; i < num_args; i++) - ctx.internalize(n->get_arg(i), false); + for (expr* arg : *n) { + ctx.internalize(arg, false); + } } enode * theory_bv::mk_enode(app * n) { @@ -185,11 +185,9 @@ namespace smt { void theory_bv::get_bits(theory_var v, expr_ref_vector & r) { context & ctx = get_context(); literal_vector & bits = m_bits[v]; - literal_vector::const_iterator it = bits.begin(); - literal_vector::const_iterator end = bits.end(); - for (; it != end; ++it) { + for (literal lit : bits) { expr_ref l(get_manager()); - ctx.literal2expr(*it, l); + ctx.literal2expr(lit, l); r.push_back(l); } } @@ -358,18 +356,16 @@ namespace smt { void mark_bits(conflict_resolution & cr, literal_vector const & bits) { context & ctx = cr.get_context(); - literal_vector::const_iterator it = bits.begin(); - literal_vector::const_iterator end = bits.end(); - for (; it != end; ++it) { - if (it->var() != true_bool_var) { - if (ctx.get_assignment(*it) == l_true) - cr.mark_literal(*it); + for (literal lit : bits) { + if (lit.var() != true_bool_var) { + if (ctx.get_assignment(lit) == l_true) + cr.mark_literal(lit); else - cr.mark_literal(~(*it)); + cr.mark_literal(~lit); } } } - + void get_proof(conflict_resolution & cr, literal l, ptr_buffer & prs, bool & visited) { if (l.var() == true_bool_var) return; @@ -830,10 +826,9 @@ namespace smt { while (i > 0) { i--; theory_var arg = get_arg_var(e, i); - literal_vector::const_iterator it = m_bits[arg].begin(); - literal_vector::const_iterator end = m_bits[arg].end(); - for (; it != end; ++it) - add_bit(v, *it); + for (literal lit : m_bits[arg]) { + add_bit(v, lit); + } } find_wpos(v); } @@ -1308,10 +1303,9 @@ namespace smt { theory_var v = e->get_th_var(get_id()); if (v != null_theory_var) { literal_vector & bits = m_bits[v]; - literal_vector::iterator it = bits.begin(); - literal_vector::iterator end = bits.end(); - for (; it != end; ++it) - ctx.mark_as_relevant(*it); + for (literal lit : bits) { + ctx.mark_as_relevant(lit); + } } } } @@ -1463,35 +1457,27 @@ namespace smt { SASSERT(bv_size == get_bv_size(r2)); m_merge_aux[0].reserve(bv_size+1, null_theory_var); m_merge_aux[1].reserve(bv_size+1, null_theory_var); -#define RESET_MERGET_AUX() { \ - zero_one_bits::iterator it = bits1.begin(); \ - zero_one_bits::iterator end = bits1.end(); \ - for (; it != end; ++it) \ - m_merge_aux[it->m_is_true][it->m_idx] = null_theory_var; \ - } + +#define RESET_MERGET_AUX() for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = null_theory_var; + DEBUG_CODE(for (unsigned i = 0; i < bv_size; i++) { SASSERT(m_merge_aux[0][i] == null_theory_var || m_merge_aux[1][i] == null_theory_var); }); // save info about bits1 - zero_one_bits::iterator it = bits1.begin(); - zero_one_bits::iterator end = bits1.end(); - for (; it != end; ++it) - m_merge_aux[it->m_is_true][it->m_idx] = it->m_owner; + for (auto & zo : bits1) m_merge_aux[zo.m_is_true][zo.m_idx] = zo.m_owner; // check if bits2 is consistent with bits1, and copy new bits to bits1 - it = bits2.begin(); - end = bits2.end(); - for (; it != end; ++it) { - theory_var v2 = it->m_owner; - theory_var v1 = m_merge_aux[!it->m_is_true][it->m_idx]; + for (auto & zo : bits2) { + theory_var v2 = zo.m_owner; + theory_var v1 = m_merge_aux[!zo.m_is_true][zo.m_idx]; if (v1 != null_theory_var) { // conflict was detected ... v1 and v2 have complementary bits - SASSERT(m_bits[v1][it->m_idx] == ~(m_bits[v2][it->m_idx])); + SASSERT(m_bits[v1][zo.m_idx] == ~(m_bits[v2][zo.m_idx])); SASSERT(m_bits[v1].size() == m_bits[v2].size()); - mk_new_diseq_axiom(v1, v2, it->m_idx); + mk_new_diseq_axiom(v1, v2, zo.m_idx); RESET_MERGET_AUX(); return false; } - if (m_merge_aux[it->m_is_true][it->m_idx] == null_theory_var) { + if (m_merge_aux[zo.m_is_true][zo.m_idx] == null_theory_var) { // copy missing variable to bits1 - bits1.push_back(*it); + bits1.push_back(zo); } } // reset m_merge_aux vector @@ -1614,11 +1600,9 @@ namespace smt { out << std::right << ", bits:"; context & ctx = get_context(); literal_vector const & bits = m_bits[v]; - literal_vector::const_iterator it = bits.begin(); - literal_vector::const_iterator end = bits.end(); - for (; it != end; ++it) { + for (literal lit : bits) { out << " "; - ctx.display_literal(out, *it); + ctx.display_literal(out, lit); } numeral val; if (get_fixed_value(v, val)) @@ -1740,13 +1724,11 @@ namespace smt { SASSERT(_bits.size() == num_bits); svector already_found; already_found.resize(bv_sz, false); - zero_one_bits::const_iterator it = _bits.begin(); - zero_one_bits::const_iterator end = _bits.end(); - for (; it != end; ++it) { - SASSERT(find(it->m_owner) == v); - SASSERT(bits[it->m_is_true][it->m_idx]); - SASSERT(!already_found[it->m_idx]); - already_found[it->m_idx] = true; + for (auto & zo : _bits) { + SASSERT(find(zo.m_owner) == v); + SASSERT(bits[zo.m_is_true][zo.m_idx]); + SASSERT(!already_found[zo.m_idx]); + already_found[zo.m_idx] = true; } } return true; diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 2f89b7168..a49e0e4bb 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -516,7 +516,7 @@ class theory_lra::imp { rational r1; v = mk_var(t); svector vars; - ptr_vector todo; + ptr_buffer todo; todo.push_back(t); while (!todo.empty()) { expr* n = todo.back(); @@ -536,7 +536,7 @@ class theory_lra::imp { vars.push_back(get_var_index(mk_var(n))); } } - TRACE("arith", tout << mk_pp(t, m) << " " << _has_var << "\n";); + TRACE("arith", tout << "v" << v << "(" << get_var_index(v) << ") := " << mk_pp(t, m) << " " << _has_var << "\n";); if (!_has_var) { ensure_nra(); m_nra->add_monomial(get_var_index(v), vars.size(), vars.c_ptr()); @@ -1190,12 +1190,12 @@ public: if (m_solver->is_term(wi)) { const lp::lar_term& term = m_solver->get_term(wi); result += term.m_v * coeff; - for (const auto & i : term.m_coeffs) { - if (m_variable_values.count(i.first) > 0) { - result += m_variable_values[i.first] * coeff * i.second; + for (const auto & i : term) { + if (m_variable_values.count(i.var()) > 0) { + result += m_variable_values[i.var()] * coeff * i.coeff(); } else { - m_todo_terms.push_back(std::make_pair(i.first, coeff * i.second)); + m_todo_terms.push_back(std::make_pair(i.var(), coeff * i.coeff())); } } } @@ -1481,7 +1481,7 @@ public: } if (!m_nra) return l_true; if (!m_nra->need_check()) return l_true; - m_a1 = 0; m_a2 = 0; + m_a1 = nullptr; m_a2 = nullptr; lbool r = m_nra->check(m_explanation); m_a1 = alloc(scoped_anum, m_nra->am()); m_a2 = alloc(scoped_anum, m_nra->am()); @@ -2153,8 +2153,8 @@ public: vi = m_todo_vars.back(); m_todo_vars.pop_back(); lp::lar_term const& term = m_solver->get_term(vi); - for (auto const& coeff : term.m_coeffs) { - lp::var_index wi = coeff.first; + for (auto const& coeff : term) { + lp::var_index wi = coeff.var(); if (m_solver->is_term(wi)) { m_todo_vars.push_back(wi); } @@ -2605,19 +2605,23 @@ public: m_todo_terms.push_back(std::make_pair(vi, rational::one())); + TRACE("arith", tout << "v" << v << " := w" << vi << "\n"; + m_solver->print_term(m_solver->get_term(vi), tout); tout << "\n";); + m_nra->am().set(r, 0); while (!m_todo_terms.empty()) { rational wcoeff = m_todo_terms.back().second; - // lp::var_index wi = m_todo_terms.back().first; // todo : got a warning "wi is not used" + vi = m_todo_terms.back().first; m_todo_terms.pop_back(); lp::lar_term const& term = m_solver->get_term(vi); + TRACE("arith", m_solver->print_term(term, tout); tout << "\n";); scoped_anum r1(m_nra->am()); rational c1 = term.m_v * wcoeff; m_nra->am().set(r1, c1.to_mpq()); m_nra->am().add(r, r1, r); - for (auto const coeff : term.m_coeffs) { - lp::var_index wi = coeff.first; - c1 = coeff.second * wcoeff; + for (auto const & arg : term) { + lp::var_index wi = m_solver->local2external(arg.var()); + c1 = arg.coeff() * wcoeff; if (m_solver->is_term(wi)) { m_todo_terms.push_back(std::make_pair(wi, c1)); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index a906f0e6b..4c0e9b87d 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -889,38 +889,35 @@ bool theory_seq::branch_quat_variable(eq const& e) { return true; } -void theory_seq::len_offset(expr* const& e, rational val) { +void theory_seq::len_offset(expr* e, rational val) { context & ctx = get_context(); expr *l1 = nullptr, *l2 = nullptr, *l21 = nullptr, *l22 = nullptr; rational fact; if (m_autil.is_add(e, l1, l2) && m_autil.is_mul(l2, l21, l22) && - m_autil.is_numeral(l21, fact) && fact.is_minus_one()) { + m_autil.is_numeral(l21, fact) && fact.is_minus_one()) { if (ctx.e_internalized(l1) && ctx.e_internalized(l22)) { enode* r1 = ctx.get_enode(l1)->get_root(), *n1 = r1; enode* r2 = ctx.get_enode(l22)->get_root(), *n2 = r2; expr *e1 = nullptr, *e2 = nullptr; do { - if (!m_util.str.is_length(n1->get_owner(), e1)) - n1 = n1->get_next(); - else + if (m_util.str.is_length(n1->get_owner(), e1)) break; + n1 = n1->get_next(); } while (n1 != r1); do { - if (!m_util.str.is_length(n2->get_owner(), e2)) - n2 = n2->get_next(); - else + if (m_util.str.is_length(n2->get_owner(), e2)) break; + n2 = n2->get_next(); } while (n2 != r2); + obj_map tmp; if (m_util.str.is_length(n1->get_owner(), e1) - && m_util.str.is_length(n2->get_owner(), e2)) { - obj_map tmp; - m_len_offset.find(r1, tmp); + && m_util.str.is_length(n2->get_owner(), e2) && + m_len_offset.find(r1, tmp)) { tmp.insert(r2, val.get_int32()); m_len_offset.insert(r1, tmp); - TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) - << ", " << mk_pp(e2, m) << "\n";); + TRACE("seq", tout << "a length pair: " << mk_pp(e1, m) << ", " << mk_pp(e2, m) << "\n";); return; } } @@ -1307,32 +1304,34 @@ bool theory_seq::len_based_split(eq const& e) { y12 = mk_concat(Z, y12); } } - else - lenY11 = m_util.str.mk_length(y11); + else { + lenY11 = m_util.str.mk_length(y11); + } dependency* dep = e.dep(); literal_vector lits; literal lit1 = mk_eq(lenX11, lenY11, false); + if (ctx.get_assignment(lit1) != l_true) { + return false; + } lits.push_back(lit1); - if (ls.size()>=2 && rs.size()>=2 && (ls.size()>2 || rs.size()>2)) { + if (ls.size() >= 2 && rs.size() >= 2 && (ls.size() > 2 || rs.size() > 2)) { expr_ref len1(m_autil.mk_int(0),m), len2(m_autil.mk_int(0),m); for (unsigned i = 2; i < ls.size(); ++i) len1 = mk_add(len1, m_util.str.mk_length(ls[i])); for (unsigned i = 2; i < rs.size(); ++i) len2 = mk_add(len2, m_util.str.mk_length(rs[i])); - bool flag = false; + literal lit2; if (!m_autil.is_numeral(len1) && !m_autil.is_numeral(len2)) { - literal lit2 = mk_eq(len1, len2, false); - flag = ctx.get_assignment(lit2) == l_true; + lit2 = mk_eq(len1, len2, false); } else { expr_ref eq_len(m.mk_eq(len1, len2), m); - flag = ctx.find_assignment(eq_len) == l_true; + lit2 = mk_literal(eq_len); } - if (flag) { - literal lit2 = mk_eq(len1, len2, false); + if (ctx.get_assignment(lit2) == l_true) { lits.push_back(lit2); TRACE("seq", tout << mk_pp(len1, m) << " = " << mk_pp(len2, m) << "\n";); expr_ref lhs(m), rhs(m); @@ -5277,9 +5276,10 @@ void theory_seq::new_eq_eh(dependency* deps, enode* n1, enode* n2) { void theory_seq::new_diseq_eh(theory_var v1, theory_var v2) { enode* n1 = get_enode(v1); - enode* n2 = get_enode(v2); + enode* n2 = get_enode(v2); expr_ref e1(n1->get_owner(), m); expr_ref e2(n2->get_owner(), m); + SASSERT(n1->get_root() != n2->get_root()); m_exclude.update(e1, e2); expr_ref eq(m.mk_eq(e1, e2), m); TRACE("seq", tout << "new disequality " << get_context().get_scope_level() << ": " << eq << "\n";); diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index abb202884..23b044445 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -375,7 +375,7 @@ namespace smt { void init_model(expr_ref_vector const& es); - void len_offset(expr* const& e, rational val); + void len_offset(expr* e, rational val); void prop_arith_to_len_offset(); int find_fst_non_empty_idx(expr_ref_vector const& x) const; expr* find_fst_non_empty_var(expr_ref_vector const& x) const; diff --git a/src/util/lp/int_solver.h b/src/util/lp/int_solver.h index 65c818d1e..ec708918d 100644 --- a/src/util/lp/int_solver.h +++ b/src/util/lp/int_solver.h @@ -50,7 +50,6 @@ public: // main function to check that the solution provided by lar_solver is valid for integral values, // or provide a way of how it can be adjusted. lia_move check(lar_term& t, mpq& k, explanation& ex, bool & upper); - lia_move check_(lar_term& t, mpq& k, explanation& ex, bool & upper); bool move_non_basic_column_to_bounds(unsigned j); lia_move check_wrapper(lar_term& t, mpq& k, explanation& ex); bool is_base(unsigned j) const; diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 13ef79a96..c4f7ff196 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -540,11 +540,13 @@ lp_status lar_solver::maximize_term(unsigned ext_j, if (m_int_solver->is_base(j)) { if (!remove_from_basis(j)) { // consider a special version of remove_from_basis that would not remove inf_int columns m_mpq_lar_core_solver.m_r_x = backup; + term_max = prev_value; return lp_status::FEASIBLE; // it should not happen } } m_int_solver->patch_nbasic_column(j, false); if (!column_value_is_integer(j)) { + term_max = prev_value; m_mpq_lar_core_solver.m_r_x = backup; return lp_status::FEASIBLE; } diff --git a/src/util/lp/lar_solver.h b/src/util/lp/lar_solver.h index 3735fbb9f..283c13c38 100644 --- a/src/util/lp/lar_solver.h +++ b/src/util/lp/lar_solver.h @@ -247,6 +247,8 @@ public: void calculate_implied_bounds_for_row(unsigned i, bound_propagator & bp); unsigned adjust_column_index_to_term_index(unsigned j) const; + + var_index local2external(var_index idx) const { return m_var_register.local_to_external(idx); } void propagate_bounds_on_a_term(const lar_term& t, bound_propagator & bp, unsigned term_offset); diff --git a/src/util/lp/lia_move.h b/src/util/lp/lia_move.h index ec4643e20..65da5826e 100644 --- a/src/util/lp/lia_move.h +++ b/src/util/lp/lia_move.h @@ -28,4 +28,25 @@ enum class lia_move { undef, unsat }; +inline std::string lia_move_to_string(lia_move m) { + switch (m) { + case lia_move::sat: + return "sat"; + case lia_move::branch: + return "branch"; + case lia_move::cut: + return "cut"; + case lia_move::conflict: + return "conflict"; + case lia_move::continue_with_check: + return "continue_with_check"; + case lia_move::undef: + return "undef"; + case lia_move::unsat: + return "unsat"; + default: + lp_assert(false); + }; + return "strange"; +} } diff --git a/src/util/lp/nra_solver.cpp b/src/util/lp/nra_solver.cpp index a4930b357..0d28058e8 100644 --- a/src/util/lp/nra_solver.cpp +++ b/src/util/lp/nra_solver.cpp @@ -24,11 +24,12 @@ namespace nra { lp::lar_solver& s; reslimit& m_limit; params_ref m_params; - u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables + u_map m_lp2nl; // map from lar_solver variables to nlsat::solver variables scoped_ptr m_nlsat; + scoped_ptr m_zero; vector m_monomials; unsigned_vector m_monomials_lim; - mutable std::unordered_map m_variable_values; // current model + mutable std::unordered_map m_variable_values; // current model imp(lp::lar_solver& s, reslimit& lim, params_ref const& p): s(s), @@ -90,6 +91,7 @@ namespace nra { lbool check(lp::explanation_t& ex) { SASSERT(need_check()); m_nlsat = alloc(nlsat::solver, m_limit, m_params, false); + m_zero = alloc(scoped_anum, am()); m_lp2nl.reset(); vector core; @@ -208,12 +210,17 @@ namespace nra { if (!m_lp2nl.find(v, r)) { r = m_nlsat->mk_var(is_int(v)); m_lp2nl.insert(v, r); + TRACE("arith", tout << "v" << v << " := x" << r << "\n";); } return r; } nlsat::anum const& value(lp::var_index v) const { - return m_nlsat->value(m_lp2nl.find(v)); + polynomial::var pv; + if (m_lp2nl.find(v, pv)) + return m_nlsat->value(pv); + else + return *m_zero; } nlsat::anum_manager& am() {