From 60bb02b70971e815c1c1e3b1a958b21eeb91af2d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Jul 2018 15:31:49 +0100 Subject: [PATCH 1/6] updates Signed-off-by: Nikolaj Bjorner --- src/ast/arith_decl_plugin.cpp | 17 +++++++++++ src/ast/arith_decl_plugin.h | 1 + src/ast/rewriter/arith_rewriter.cpp | 6 ++++ src/ast/rewriter/arith_rewriter.h | 1 + src/ast/rewriter/seq_rewriter.cpp | 47 +++++++++++++++++++++++++++++ src/ast/rewriter/seq_rewriter.h | 2 ++ src/cmd_context/cmd_context.cpp | 2 +- src/smt/mam.cpp | 23 ++++++++------ src/smt/smt_context.cpp | 37 +++++++++-------------- src/smt/smt_context.h | 3 +- src/smt/theory_seq.cpp | 16 +++++++++- 11 files changed, 120 insertions(+), 35 deletions(-) diff --git a/src/ast/arith_decl_plugin.cpp b/src/ast/arith_decl_plugin.cpp index be3a02019..3c5e2e1c0 100644 --- a/src/ast/arith_decl_plugin.cpp +++ b/src/ast/arith_decl_plugin.cpp @@ -351,6 +351,7 @@ inline func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, bool is_real) { case OP_MUL: return is_real ? m_r_mul_decl : m_i_mul_decl; case OP_DIV: return m_r_div_decl; case OP_IDIV: return m_i_div_decl; + case OP_IDIVIDES: UNREACHABLE(); case OP_REM: return m_i_rem_decl; case OP_MOD: return m_i_mod_decl; case OP_TO_REAL: return m_to_real_decl; @@ -482,6 +483,14 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters m_manager->raise_exception("no arguments supplied to arithmetical operator"); return nullptr; } + if (k == OP_IDIVIDES) { + if (arity != 1 || domain[0] != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) { + m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer"); + } + return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), + func_decl_info(m_family_id, k, num_parameters, parameters)); + } + if (m_manager->int_real_coercions() && use_coercion(k)) { return mk_func_decl(fix_kind(k, arity), has_real_arg(arity, domain, m_real_decl)); } @@ -499,6 +508,13 @@ func_decl * arith_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters m_manager->raise_exception("no arguments supplied to arithmetical operator"); return nullptr; } + if (k == OP_IDIVIDES) { + if (num_args != 1 || m_manager->get_sort(args[0]) != m_int_decl || num_parameters != 1 || !parameters[0].is_int()) { + m_manager->raise_exception("invalid divides application. Expects integer parameter and one argument of sort integer"); + } + return m_manager->mk_func_decl(symbol("divides"), 1, &m_int_decl, m_manager->mk_bool_sort(), + func_decl_info(m_family_id, k, num_parameters, parameters)); + } if (m_manager->int_real_coercions() && use_coercion(k)) { return mk_func_decl(fix_kind(k, num_args), has_real_arg(m_manager, num_args, args, m_real_decl)); } @@ -533,6 +549,7 @@ void arith_decl_plugin::get_op_names(svector& op_names, symbol con op_names.push_back(builtin_name("*",OP_MUL)); op_names.push_back(builtin_name("/",OP_DIV)); op_names.push_back(builtin_name("div",OP_IDIV)); + op_names.push_back(builtin_name("divides",OP_IDIVIDES)); op_names.push_back(builtin_name("rem",OP_REM)); op_names.push_back(builtin_name("mod",OP_MOD)); op_names.push_back(builtin_name("to_real",OP_TO_REAL)); diff --git a/src/ast/arith_decl_plugin.h b/src/ast/arith_decl_plugin.h index f5f82b5fd..09f082522 100644 --- a/src/ast/arith_decl_plugin.h +++ b/src/ast/arith_decl_plugin.h @@ -46,6 +46,7 @@ enum arith_op_kind { OP_MUL, OP_DIV, OP_IDIV, + OP_IDIVIDES, OP_REM, OP_MOD, OP_TO_REAL, diff --git a/src/ast/rewriter/arith_rewriter.cpp b/src/ast/rewriter/arith_rewriter.cpp index 8035254b4..72ce9c761 100644 --- a/src/ast/rewriter/arith_rewriter.cpp +++ b/src/ast/rewriter/arith_rewriter.cpp @@ -66,6 +66,7 @@ br_status arith_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * c SASSERT(num_args == 2); st = mk_div_core(args[0], args[1], result); break; case OP_IDIV: if (num_args == 1) { result = args[0]; st = BR_DONE; break; } SASSERT(num_args == 2); st = mk_idiv_core(args[0], args[1], result); break; + case OP_IDIVIDES: SASSERT(num_args == 1); st = mk_idivides(f->get_parameter(0).get_int(), args[0], result); break; case OP_MOD: SASSERT(num_args == 2); st = mk_mod_core(args[0], args[1], result); break; case OP_REM: SASSERT(num_args == 2); st = mk_rem_core(args[0], args[1], result); break; case OP_UMINUS: SASSERT(num_args == 1); st = mk_uminus(args[0], result); break; @@ -792,6 +793,11 @@ br_status arith_rewriter::mk_div_core(expr * arg1, expr * arg2, expr_ref & resul return BR_FAILED; } +br_status arith_rewriter::mk_idivides(unsigned k, expr * arg, expr_ref & result) { + result = m().mk_eq(m_util.mk_mod(arg, m_util.mk_int(k)), m_util.mk_int(0)); + return BR_REWRITE2; +} + br_status arith_rewriter::mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result) { set_curr_sort(m().get_sort(arg1)); numeral v1, v2; diff --git a/src/ast/rewriter/arith_rewriter.h b/src/ast/rewriter/arith_rewriter.h index 93b6e5ad5..dd7623a9b 100644 --- a/src/ast/rewriter/arith_rewriter.h +++ b/src/ast/rewriter/arith_rewriter.h @@ -143,6 +143,7 @@ public: br_status mk_div_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_idiv_core(expr * arg1, expr * arg2, expr_ref & result); + br_status mk_idivides(unsigned k, expr * arg, expr_ref & result); br_status mk_mod_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_rem_core(expr * arg1, expr * arg2, expr_ref & result); br_status mk_power_core(expr* arg1, expr* arg2, expr_ref & result); diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index af5ef3b0b..a65351a50 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1866,6 +1866,53 @@ bool seq_rewriter::reduce_eq(expr* l, expr* r, expr_ref_vector& lhs, expr_ref_ve } } +bool seq_rewriter::reduce_contains(expr* a, expr* b, expr_ref_vector& disj) { + m_lhs.reset(); + m_util.str.get_concat(a, m_lhs); + TRACE("seq", tout << expr_ref(a, m()) << " " << expr_ref(b, m()) << "\n";); + zstring s; + for (unsigned i = 0; i < m_lhs.size(); ++i) { + expr* e = m_lhs.get(i); + if (m_util.str.is_empty(e)) { + continue; + } + + if (m_util.str.is_string(e, s)) { + 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.append(m_lhs.size() - i, m_lhs.c_ptr() + i); + for (unsigned j = 0; j < sz; ++j) { + disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(es.size() - j, es.c_ptr() + j))); + } + continue; + } + if (m_util.str.is_unit(e)) { + disj.push_back(m_util.str.mk_prefix(b, m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i))); + continue; + } + + 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)))); + return true; + } + + if (i == 0) { + return false; + } + disj.push_back(m_util.str.mk_contains(m_util.str.mk_concat(m_lhs.size() - i, m_lhs.c_ptr() + i), b)); + return true; + } + disj.push_back(m().mk_eq(b, m_util.str.mk_empty(m().get_sort(b)))); + return true; +} + + expr* seq_rewriter::concat_non_empty(unsigned n, expr* const* as) { SASSERT(n > 0); ptr_vector bs; diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c96096c65..f5878b2c2 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -168,6 +168,8 @@ public: bool reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_vector& lhs, expr_ref_vector& rhs, bool& change); + bool reduce_contains(expr* a, expr* b, expr_ref_vector& disj); + void add_seqs(expr_ref_vector const& ls, expr_ref_vector const& rs, expr_ref_vector& lhs, expr_ref_vector& rhs); diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 585dd0fa6..be3acc261 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -1063,7 +1063,7 @@ void cmd_context::mk_app(symbol const & s, unsigned num_args, expr * const * arg return; } if (num_indices > 0) - throw cmd_exception("invalid use of indexed indentifier, unknown builtin function ", s); + throw cmd_exception("invalid use of indexed identifier, unknown builtin function ", s); expr* _t; if (macros_find(s, num_args, args, _t)) { TRACE("macro_bug", tout << "well_sorted_check_enabled(): " << well_sorted_check_enabled() << "\n"; diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index c71a6e21d..5267800db 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -401,11 +401,11 @@ namespace smt { label_hasher & m_lbl_hasher; func_decl * m_root_lbl; unsigned m_num_args; //!< we need this information to avoid the nary *,+ crash bug - unsigned char m_filter_candidates; + bool m_filter_candidates; unsigned m_num_regs; unsigned m_num_choices; instruction * m_root; - enode_vector m_candidates; + obj_hashtable m_candidates; #ifdef Z3DEBUG context * m_context; ptr_vector m_patterns; @@ -531,7 +531,7 @@ namespace smt { } bool filter_candidates() const { - return m_filter_candidates != 0; + return m_filter_candidates; } const instruction * get_root() const { @@ -539,7 +539,7 @@ namespace smt { } void add_candidate(enode * n) { - m_candidates.push_back(n); + m_candidates.insert(n); } bool has_candidates() const { @@ -550,7 +550,7 @@ namespace smt { m_candidates.reset(); } - enode_vector const & get_candidates() const { + obj_hashtable const & get_candidates() const { return m_candidates; } @@ -2001,7 +2001,9 @@ namespace smt { TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout);); init(t); if (t->filter_candidates()) { + //t->display(std::cout << "ncf: " << t->get_candidates().size() << "\n"); for (enode* app : t->get_candidates()) { + TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (!app->is_marked() && app->is_cgr()) { if (m_context.resource_limits_exceeded() || !execute_core(t, app)) return; @@ -2014,6 +2016,9 @@ namespace smt { } } else { + //t->display(std::cout << "ncu: " << t->get_candidates().size() << "\n"); + //for (enode* app : t->get_candidates()) { std::cout << expr_ref(app->get_owner(), m_ast_manager) << "\n"; } + //std::cout.flush(); for (enode* app : t->get_candidates()) { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (app->is_cgr()) { @@ -3516,9 +3521,7 @@ namespace smt { std::cout << "Avg. " << static_cast(total_sz)/static_cast(counter) << ", Max. " << max_sz << "\n"; #endif - enode_vector::iterator it1 = v->begin(); - enode_vector::iterator end1 = v->end(); - for (; it1 != end1; ++it1) { + for (enode* n : *v) { // Two different kinds of mark are used: // - enode mark field: it is used to mark the already processed parents. // - enode mark2 field: it is used to mark the roots already added to be processed in the next level. @@ -3527,7 +3530,7 @@ namespace smt { // and Z3 may fail to find potential new matches. // // The file regression\acu.sx exposed this problem. - enode * curr_child = (*it1)->get_root(); + enode * curr_child = n->get_root(); if (m_use_filters && curr_child->get_plbls().empty_intersection(filter)) continue; @@ -3591,7 +3594,7 @@ namespace smt { is_eq(curr_tree->m_ground_arg, curr_parent->get_arg(curr_tree->m_ground_arg_idx)) )) { if (curr_tree->m_code) { - TRACE("mam_path_tree", tout << "found candidate\n";); + TRACE("mam_path_tree", tout << "found candidate " << expr_ref(curr_parent->get_owner(), m_ast_manager) << "\n";); add_candidate(curr_tree->m_code, curr_parent); } if (curr_tree->m_first_child) { diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 44147c668..aa7063dc1 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1351,18 +1351,9 @@ namespace smt { \remark The method assign_eq adds a new entry on this queue. */ bool context::propagate_eqs() { - for (unsigned i = 0; i < m_eq_propagation_queue.size(); i++) { + TRACE("add_eq", tout << m_eq_propagation_queue.size() << "\n";); + for (unsigned i = 0; i < m_eq_propagation_queue.size() && !get_cancel_flag(); i++) { new_eq & entry = m_eq_propagation_queue[i]; -#if 0 - static unsigned counter1 = 0; - static unsigned counter2 = 0; - if (entry.m_lhs->is_eq() || entry.m_rhs->is_eq()) - counter1++; - else - counter2++; - if ((counter1 + counter2) % 10000 == 0) - std::cout << counter1 << " " << counter2 << "\n"; -#endif add_eq(entry.m_lhs, entry.m_rhs, entry.m_justification); if (inconsistent()) return false; @@ -1376,7 +1367,7 @@ namespace smt { */ bool context::propagate_atoms() { SASSERT(!inconsistent()); - for (unsigned i = 0; i < m_atom_propagation_queue.size(); i++) { + for (unsigned i = 0; i < m_atom_propagation_queue.size() && !get_cancel_flag(); i++) { SASSERT(!inconsistent()); literal l = m_atom_propagation_queue[i]; bool_var v = l.var(); @@ -1558,16 +1549,17 @@ namespace smt { lbool context::get_assignment(expr * n) const { if (m_manager.is_false(n)) return l_false; - if (m_manager.is_not(n)) - return ~get_assignment_core(to_app(n)->get_arg(0)); + expr* arg = nullptr; + if (m_manager.is_not(n, arg)) + return ~get_assignment_core(arg); return get_assignment_core(n); } lbool context::find_assignment(expr * n) const { if (m_manager.is_false(n)) return l_false; - if (m_manager.is_not(n)) { - expr * arg = to_app(n)->get_arg(0); + expr* arg = nullptr; + if (m_manager.is_not(n, arg)) { if (b_internalized(arg)) return ~get_assignment_core(arg); return l_undef; @@ -1752,6 +1744,10 @@ namespace smt { return false; if (!propagate_eqs()) return false; + if (get_cancel_flag()) { + m_qhead = qhead; + return true; + } propagate_th_eqs(); propagate_th_diseqs(); if (inconsistent()) @@ -3264,6 +3260,7 @@ namespace smt { } void context::reset_assumptions() { + TRACE("unsat_core_bug", tout << "reset " << m_assumptions << "\n";); for (literal lit : m_assumptions) get_bdata(lit.var()).m_assumption = false; m_assumptions.reset(); @@ -4106,9 +4103,7 @@ namespace smt { } SASSERT(!inconsistent()); - unsigned sz = m_b_internalized_stack.size(); - for (unsigned i = 0; i < sz; i++) { - expr * curr = m_b_internalized_stack.get(i); + for (expr * curr : m_b_internalized_stack) { if (is_relevant(curr) && get_assignment(curr) == l_true) { // if curr is a label literal, then its tags will be copied to result. m_manager.is_label_lit(curr, result); @@ -4124,9 +4119,7 @@ namespace smt { void context::get_relevant_labeled_literals(bool at_lbls, expr_ref_vector & result) { SASSERT(!inconsistent()); buffer lbls; - unsigned sz = m_b_internalized_stack.size(); - for (unsigned i = 0; i < sz; i++) { - expr * curr = m_b_internalized_stack.get(i); + for (expr * curr : m_b_internalized_stack) { if (is_relevant(curr) && get_assignment(curr) == l_true) { lbls.reset(); if (m_manager.is_label_lit(curr, lbls)) { diff --git a/src/smt/smt_context.h b/src/smt/smt_context.h index 2ac5695b3..b77f63e41 100644 --- a/src/smt/smt_context.h +++ b/src/smt/smt_context.h @@ -491,7 +491,7 @@ namespace smt { } bool tracking_assumptions() const { - return m_search_lvl > m_base_lvl; + return !m_assumptions.empty() && m_search_lvl > m_base_lvl; } expr * bool_var2expr(bool_var v) const { @@ -1011,6 +1011,7 @@ namespace smt { void push_eq(enode * lhs, enode * rhs, eq_justification const & js) { SASSERT(lhs != rhs); + SASSERT(lhs->get_root() != rhs->get_root()); m_eq_propagation_queue.push_back(new_eq(lhs, rhs, js)); } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 48d4ddcc0..a906f0e6b 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5163,7 +5163,21 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { } } else if (m_util.str.is_contains(e, e1, e2)) { - if (is_true) { + expr_ref_vector disj(m); + if (m_seq_rewrite.reduce_contains(e1, e2, disj)) { + literal_vector lits; + literal lit = mk_literal(e); + lits.push_back(~lit); + for (expr* d : disj) { + lits.push_back(mk_literal(d)); + } + ++m_stats.m_add_axiom; + ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); + for (expr* d : disj) { + add_axiom(lit, ~mk_literal(d)); + } + } + else if (is_true) { expr_ref f1 = mk_skolem(m_indexof_left, e1, e2); expr_ref f2 = mk_skolem(m_indexof_right, e1, e2); f = mk_concat(f1, e2, f2); From d74978c2772fa5a474a6eb266ade720c613ecc64 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 26 Jul 2018 20:29:26 +0100 Subject: [PATCH 2/6] fix #1762, #1764, #1768 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 8 -------- src/opt/opt_context.cpp | 8 +++----- src/smt/mam.cpp | 24 ++++++++++-------------- src/smt/params/theory_arith_params.h | 2 +- src/smt/theory_lra.cpp | 5 +++-- src/util/approx_nat.h | 2 +- src/util/bit_vector.cpp | 2 +- src/util/fixed_bit_vector.cpp | 2 +- src/util/hashtable.h | 4 ++-- src/util/lp/lar_solver.cpp | 8 ++++++-- src/util/memory_manager.cpp | 2 +- src/util/mpz.h | 1 - src/util/nat_set.h | 2 +- src/util/scoped_timer.cpp | 2 +- src/util/symbol.h | 2 +- 15 files changed, 32 insertions(+), 42 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 7711ec4cd..0eeeeaecc 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -1675,7 +1675,6 @@ def Or(*args): class PatternRef(ExprRef): """Patterns are hints for quantifier instantiation. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. """ def as_ast(self): return Z3_pattern_to_ast(self.ctx_ref(), self.ast) @@ -1686,8 +1685,6 @@ class PatternRef(ExprRef): def is_pattern(a): """Return `True` if `a` is a Z3 pattern (hint for quantifier instantiation. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. - >>> f = Function('f', IntSort(), IntSort()) >>> x = Int('x') >>> q = ForAll(x, f(x) == 0, patterns = [ f(x) ]) @@ -1705,8 +1702,6 @@ def is_pattern(a): def MultiPattern(*args): """Create a Z3 multi-pattern using the given expressions `*args` - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. - >>> f = Function('f', IntSort(), IntSort()) >>> g = Function('g', IntSort(), IntSort()) >>> x = Int('x') @@ -1966,8 +1961,6 @@ def ForAll(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. - >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') >>> y = Int('y') @@ -1985,7 +1978,6 @@ def Exists(vs, body, weight=1, qid="", skid="", patterns=[], no_patterns=[]): The parameters `weight`, `qif`, `skid`, `patterns` and `no_patterns` are optional annotations. - See http://rise4fun.com/Z3Py/tutorial/advanced for more details. >>> f = Function('f', IntSort(), IntSort(), IntSort()) >>> x = Int('x') diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp index 566aaa1f6..e5c0bcddb 100644 --- a/src/opt/opt_context.cpp +++ b/src/opt/opt_context.cpp @@ -1012,8 +1012,7 @@ namespace opt { } } // fix types of objectives: - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective & obj = m_objectives[i]; + for (objective & obj : m_objectives) { expr* t = obj.m_term; switch(obj.m_type) { case O_MINIMIZE: @@ -1189,13 +1188,12 @@ namespace opt { void context::update_bound(bool is_lower) { expr_ref val(m); if (!m_model.get()) return; - for (unsigned i = 0; i < m_objectives.size(); ++i) { - objective const& obj = m_objectives[i]; + for (objective const& obj : m_objectives) { rational r; switch(obj.m_type) { case O_MINIMIZE: { val = (*m_model)(obj.m_term); - TRACE("opt", tout << obj.m_term << " " << val << " " << is_numeral(val, r) << "\n";); + TRACE("opt", tout << obj.m_term << " " << val << "\n";); if (is_numeral(val, r)) { inf_eps val = inf_eps(obj.m_adjust_value(r)); TRACE("opt", tout << "adjusted value: " << val << "\n";); diff --git a/src/smt/mam.cpp b/src/smt/mam.cpp index 5267800db..00e079989 100644 --- a/src/smt/mam.cpp +++ b/src/smt/mam.cpp @@ -405,7 +405,7 @@ namespace smt { unsigned m_num_regs; unsigned m_num_choices; instruction * m_root; - obj_hashtable m_candidates; + enode_vector m_candidates; #ifdef Z3DEBUG context * m_context; ptr_vector m_patterns; @@ -539,7 +539,7 @@ namespace smt { } void add_candidate(enode * n) { - m_candidates.insert(n); + m_candidates.push_back(n); } bool has_candidates() const { @@ -550,7 +550,7 @@ namespace smt { m_candidates.reset(); } - obj_hashtable const & get_candidates() const { + enode_vector const & get_candidates() const { return m_candidates; } @@ -1978,10 +1978,10 @@ namespace smt { #define INIT_ARGS_SIZE 16 public: - interpreter(context & ctx, mam & m, bool use_filters): + interpreter(context & ctx, mam & ma, bool use_filters): m_context(ctx), m_ast_manager(ctx.get_manager()), - m_mam(m), + m_mam(ma), m_use_filters(use_filters) { m_args.resize(INIT_ARGS_SIZE); } @@ -2001,7 +2001,6 @@ namespace smt { TRACE("trigger_bug", tout << "execute for code tree:\n"; t->display(tout);); init(t); if (t->filter_candidates()) { - //t->display(std::cout << "ncf: " << t->get_candidates().size() << "\n"); for (enode* app : t->get_candidates()) { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (!app->is_marked() && app->is_cgr()) { @@ -2016,9 +2015,6 @@ namespace smt { } } else { - //t->display(std::cout << "ncu: " << t->get_candidates().size() << "\n"); - //for (enode* app : t->get_candidates()) { std::cout << expr_ref(app->get_owner(), m_ast_manager) << "\n"; } - //std::cout.flush(); for (enode* app : t->get_candidates()) { TRACE("trigger_bug", tout << "candidate\n" << mk_ismt2_pp(app->get_owner(), m_ast_manager) << "\n";); if (app->is_cgr()) { @@ -2842,7 +2838,7 @@ namespace smt { mk_tree_trail(ptr_vector & t, unsigned id):m_trees(t), m_lbl_id(id) {} void undo(mam_impl & m) override { dealloc(m_trees[m_lbl_id]); - m_trees[m_lbl_id] = 0; + m_trees[m_lbl_id] = nullptr; } }; @@ -2875,8 +2871,8 @@ namespace smt { app * p = to_app(mp->get_arg(first_idx)); func_decl * lbl = p->get_decl(); unsigned lbl_id = lbl->get_decl_id(); - m_trees.reserve(lbl_id+1, 0); - if (m_trees[lbl_id] == 0) { + m_trees.reserve(lbl_id+1, nullptr); + if (m_trees[lbl_id] == nullptr) { m_trees[lbl_id] = m_compiler.mk_tree(qa, mp, first_idx, false); SASSERT(m_trees[lbl_id]->expected_num_args() == p->get_num_args()); DEBUG_CODE(m_trees[lbl_id]->set_context(m_context);); @@ -2961,7 +2957,7 @@ namespace smt { m_ground_arg(ground_arg), m_pattern_idx(pat_idx), m_child(child) { - SASSERT(ground_arg != 0 || ground_arg_idx == 0); + SASSERT(ground_arg != nullptr || ground_arg_idx == 0); } }; @@ -3228,7 +3224,7 @@ namespace smt { path_tree * mk_path_tree(path * p, quantifier * qa, app * mp) { SASSERT(m_ast_manager.is_pattern(mp)); - SASSERT(p != 0); + SASSERT(p != nullptr); unsigned pat_idx = p->m_pattern_idx; path_tree * head = nullptr; path_tree * curr = nullptr; diff --git a/src/smt/params/theory_arith_params.h b/src/smt/params/theory_arith_params.h index 9d09b4c38..fe7cc6060 100644 --- a/src/smt/params/theory_arith_params.h +++ b/src/smt/params/theory_arith_params.h @@ -19,7 +19,7 @@ Revision History: #ifndef THEORY_ARITH_PARAMS_H_ #define THEORY_ARITH_PARAMS_H_ -#include +#include #include "util/params.h" enum arith_solver_id { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index a057ace03..2f89b7168 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2648,6 +2648,7 @@ public: else { rational r = get_value(v); TRACE("arith", tout << "v" << v << " := " << r << "\n";); + SASSERT(!a.is_int(o) || r.is_int()); if (a.is_int(o) && !r.is_int()) r = floor(r); return alloc(expr_wrapper_proc, m_factory->mk_value(r, m.get_sort(o))); } @@ -2797,6 +2798,7 @@ public: lp::var_index vi = m_theory_var2var_index[v]; st = m_solver->maximize_term(vi, term_max); } + TRACE("arith", display(tout << st << " v" << v << "\n");); switch (st) { case lp::lp_status::OPTIMAL: { inf_rational val(term_max.x, term_max.y); @@ -2804,13 +2806,12 @@ public: return inf_eps(rational::zero(), val); } case lp::lp_status::FEASIBLE: { - inf_rational val(term_max.x, term_max.y); + inf_rational val = get_value(v); blocker = mk_gt(v); return inf_eps(rational::zero(), val); } default: SASSERT(st == lp::lp_status::UNBOUNDED); - TRACE("arith", tout << "Unbounded v" << v << "\n";); has_shared = false; blocker = m.mk_false(); return inf_eps(rational::one(), inf_rational()); diff --git a/src/util/approx_nat.h b/src/util/approx_nat.h index b5e1edb8f..be5fc4fb6 100644 --- a/src/util/approx_nat.h +++ b/src/util/approx_nat.h @@ -21,7 +21,7 @@ Notes: #define APPROX_NAT_H_ #include -#include +#include class approx_nat { unsigned m_value; diff --git a/src/util/bit_vector.cpp b/src/util/bit_vector.cpp index f9f0a0797..78b7f15aa 100644 --- a/src/util/bit_vector.cpp +++ b/src/util/bit_vector.cpp @@ -16,7 +16,7 @@ Author: Revision History: --*/ -#include +#include #include "util/bit_vector.h" #include "util/trace.h" diff --git a/src/util/fixed_bit_vector.cpp b/src/util/fixed_bit_vector.cpp index aafc58404..e227aa524 100644 --- a/src/util/fixed_bit_vector.cpp +++ b/src/util/fixed_bit_vector.cpp @@ -19,7 +19,7 @@ Revision History: --*/ -#include +#include #include "util/fixed_bit_vector.h" #include "util/trace.h" #include "util/hash.h" diff --git a/src/util/hashtable.h b/src/util/hashtable.h index 420e48949..55866065e 100644 --- a/src/util/hashtable.h +++ b/src/util/hashtable.h @@ -19,9 +19,9 @@ Revision History: #ifndef HASHTABLE_H_ #define HASHTABLE_H_ #include "util/debug.h" -#include +#include #include "util/util.h" -#include +#include #include "util/memory_manager.h" #include "util/hash.h" #include "util/vector.h" diff --git a/src/util/lp/lar_solver.cpp b/src/util/lp/lar_solver.cpp index 041b49389..13ef79a96 100644 --- a/src/util/lp/lar_solver.cpp +++ b/src/util/lp/lar_solver.cpp @@ -538,12 +538,16 @@ lp_status lar_solver::maximize_term(unsigned ext_j, if (column_value_is_integer(j)) continue; 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 + 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; return lp_status::FEASIBLE; // it should not happen + } } m_int_solver->patch_nbasic_column(j, false); - if (!column_value_is_integer(j)) + if (!column_value_is_integer(j)) { + m_mpq_lar_core_solver.m_r_x = backup; return lp_status::FEASIBLE; + } change = true; } if (change) { diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp index 59a6cb009..0a1d360c8 100644 --- a/src/util/memory_manager.cpp +++ b/src/util/memory_manager.cpp @@ -6,7 +6,7 @@ Copyright (c) 2015 Microsoft Corporation #include #include -#include +#include #include "util/trace.h" #include "util/memory_manager.h" #include "util/error_codes.h" diff --git a/src/util/mpz.h b/src/util/mpz.h index 187532a87..65f89f078 100644 --- a/src/util/mpz.h +++ b/src/util/mpz.h @@ -19,7 +19,6 @@ Revision History: #ifndef MPZ_H_ #define MPZ_H_ -#include #include #include "util/util.h" #include "util/small_object_allocator.h" diff --git a/src/util/nat_set.h b/src/util/nat_set.h index 6e9ab1b6d..f2f2cb8e1 100644 --- a/src/util/nat_set.h +++ b/src/util/nat_set.h @@ -19,7 +19,7 @@ Revision History: #ifndef NAT_SET_H_ #define NAT_SET_H_ -#include +#include #include "util/vector.h" class nat_set { diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp index 56d40c47a..8078c46ee 100644 --- a/src/util/scoped_timer.cpp +++ b/src/util/scoped_timer.cpp @@ -50,7 +50,7 @@ Revision History: #undef max #endif #include "util/util.h" -#include +#include #include "util/z3_omp.h" struct scoped_timer::imp { diff --git a/src/util/symbol.h b/src/util/symbol.h index 88e825551..40844cf3b 100644 --- a/src/util/symbol.h +++ b/src/util/symbol.h @@ -19,7 +19,7 @@ Revision History: #ifndef SYMBOL_H_ #define SYMBOL_H_ #include -#include +#include #include "util/util.h" #include "util/tptr.h" From 879e217fe69d3c95f99f9ca813b075a72c004950 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 28 Jul 2018 20:28:53 -0700 Subject: [PATCH 3/6] limits -> climits Signed-off-by: Nikolaj Bjorner --- src/util/approx_nat.h | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/util/approx_nat.h b/src/util/approx_nat.h index be5fc4fb6..354ead92b 100644 --- a/src/util/approx_nat.h +++ b/src/util/approx_nat.h @@ -21,7 +21,7 @@ Notes: #define APPROX_NAT_H_ #include -#include +#include class approx_nat { unsigned m_value; From 5380b01fd171cd2bc804b46c10027fb53e7994d9 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Jul 2018 00:44:40 -0700 Subject: [PATCH 4/6] bool -> string Signed-off-by: Nikolaj Bjorner --- src/api/api_numeral.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 4d0009fbe..2b77294d5 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -186,7 +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); + CHECK_IS_EXPR(a, ""); rational r; Z3_bool ok = Z3_get_numeral_rational(c, a, r); if (ok == Z3_TRUE) { From 64e570f1592f3e0007ca9fab84e39f2de2e44a3a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Jul 2018 02:22:28 -0700 Subject: [PATCH 5/6] fix #1766 Signed-off-by: Nikolaj Bjorner --- src/smt/theory_arith_core.h | 44 ++----------------------------------- src/smt/theory_bv.cpp | 2 ++ src/smt/theory_seq.cpp | 3 ++- 3 files changed, 6 insertions(+), 43 deletions(-) diff --git a/src/smt/theory_arith_core.h b/src/smt/theory_arith_core.h index 01eb8a3d4..54f61a09a 100644 --- a/src/smt/theory_arith_core.h +++ b/src/smt/theory_arith_core.h @@ -2943,29 +2943,9 @@ namespace smt { context & ctx = get_context(); if (dump_lemmas()) { TRACE("arith", ante.display(tout) << " --> "; ctx.display_detailed_literal(tout, l); tout << "\n";); - unsigned id = ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), + 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 } } @@ -2973,28 +2953,8 @@ namespace smt { void theory_arith::dump_lemmas(literal l, derived_bound const& ante) { context & ctx = get_context(); if (dump_lemmas()) { - unsigned id = ctx.display_lemma_as_smt_problem(ante.lits().size(), ante.lits().c_ptr(), + 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 } } diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 261881a3b..a0c62b959 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -161,6 +161,8 @@ namespace smt { theory_var v = n->get_th_var(get_id()); if (v == null_theory_var) { v = mk_var(n); + } + if (m_bits[v].empty()) { mk_bits(v); } return v; diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index 4c0e9b87d..d6937aa79 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -5163,7 +5163,8 @@ void theory_seq::assign_eh(bool_var v, bool is_true) { } else if (m_util.str.is_contains(e, e1, e2)) { expr_ref_vector disj(m); - if (m_seq_rewrite.reduce_contains(e1, e2, disj)) { + // disabled pending regression on issue 1196 + if (false && m_seq_rewrite.reduce_contains(e1, e2, disj)) { literal_vector lits; literal lit = mk_literal(e); lits.push_back(~lit); From 5509bf248aa1270083552292d7da3dc6fd21cca5 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 29 Jul 2018 08:02:56 -0700 Subject: [PATCH 6/6] coallesce lambda/quant tracing Signed-off-by: Nikolaj Bjorner --- src/ast/ast.cpp | 17 +++++++++++------ src/smt/theory_seq.cpp | 2 -- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp index 74166a78b..5fcc8d63b 100644 --- a/src/ast/ast.cpp +++ b/src/ast/ast.cpp @@ -2369,6 +2369,15 @@ bool ast_manager::is_pattern(expr const * n, ptr_vector &args) { return true; } +static void trace_quant(std::ostream& strm, quantifier* q) { + strm << (is_lambda(q) ? "[mk-lambda]" : "[mk-quant]") + << " #" << q->get_id() << " " << q->get_qid(); + for (unsigned i = 0; i < q->get_num_patterns(); ++i) { + strm << " #" << q->get_pattern(i)->get_id(); + } + strm << " #" << q->get_expr()->get_id() << "\n"; +} + quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, sort * const * decl_sorts, symbol const * decl_names, expr * body, int weight , symbol const & qid, symbol const & skid, @@ -2401,11 +2410,7 @@ quantifier * ast_manager::mk_quantifier(quantifier_kind k, unsigned num_decls, s quantifier * r = register_node(new_node); if (m_trace_stream && r == new_node) { - *m_trace_stream << "[mk-quant] #" << r->get_id() << " " << qid; - for (unsigned i = 0; i < num_patterns; ++i) { - *m_trace_stream << " #" << patterns[i]->get_id(); - } - *m_trace_stream << " #" << body->get_id() << "\n"; + trace_quant(*m_trace_stream, r); } return r; @@ -2420,7 +2425,7 @@ quantifier * ast_manager::mk_lambda(unsigned num_decls, sort * const * decl_sort 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"; + trace_quant(*m_trace_stream, r); } return r; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index d6937aa79..8f64544b4 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -4581,7 +4581,6 @@ bool theory_seq::lower_bound(expr* _e, rational& lo) const { if (thi && thi->get_lower(ctx.get_enode(e), _lo)) break; theory_lra* thr = get_th_arith(ctx, afid, e); if (thr && thr->get_lower(ctx.get_enode(e), _lo)) break; - TRACE("seq", tout << "no lower bound " << mk_pp(_e, m) << "\n";); return false; } while (false); @@ -4639,7 +4638,6 @@ bool theory_seq::upper_bound(expr* _e, rational& hi) const { if (thi && thi->get_upper(ctx.get_enode(e), _hi)) break; theory_lra* thr = get_th_arith(ctx, afid, e); if (thr && thr->get_upper(ctx.get_enode(e), _hi)) break; - TRACE("seq", tout << "no upper bound " << mk_pp(_e, m) << "\n";); return false; } while (false);