From e10850e66a6122f34a6f2f9c342850ee798c786c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Aug 2021 11:27:03 -0700 Subject: [PATCH 01/19] fix #5457 --- src/tactic/core/reduce_invertible_tactic.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 85062b03b..d8dc32809 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -327,7 +327,6 @@ private: // unsigned sz = m_bv.get_bv_size(p); expr_ref bit1(m_bv.mk_numeral(1, 1), m); - new_v = m_bv.mk_numeral(0, sz); unsigned sh = 0; @@ -335,9 +334,10 @@ private: r /= rational(2); ++sh; } - if (r.is_pos() && sh > 0) { + if (r.is_pos() && sh > 0) new_v = m_bv.mk_concat(m_bv.mk_extract(sz-sh-1, 0, v), m_bv.mk_numeral(0, sh)); - } + else + new_v = v; if (mc && !r.is_zero()) { ensure_mc(mc); expr_ref def(m); From dcfd7b76c9da57689fb7e529a2d90cbe6ffbdbd3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 5 Aug 2021 11:54:13 -0700 Subject: [PATCH 02/19] more rewrites based on example in #5457 --- src/tactic/core/reduce_invertible_tactic.cpp | 32 ++++++++++++++++++++ 1 file changed, 32 insertions(+) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index d8dc32809..23ae55da9 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -414,6 +414,38 @@ private: return true; } } + + // + // v <= u + // => u + 1 == 0 or delta + // v := delta ? u : u + 1 + // + if (m_bv.is_bv_ule(p, e1, e2) && e1 == v && mc) { + ensure_mc(mc); + unsigned sz = m_bv.get_bv_size(e2); + expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m); + expr_ref succ_e2(m_bv.mk_bv_add(e2, m_bv.mk_numeral(1, sz)), m); + new_v = m.mk_or(delta, m.mk_eq(succ_e2, m_bv.mk_numeral(0, sz))); + (*mc)->hide(delta); + (*mc)->add(v, m.mk_ite(delta, e2, succ_e2)); + return true; + } + + // + // u <= v + // => u == 0 or delta + // v := delta ? u : u - 1 + // + if (m_bv.is_bv_ule(p, e1, e2) && e2 == v && mc) { + ensure_mc(mc); + unsigned sz = m_bv.get_bv_size(e1); + expr_ref delta(m.mk_fresh_const("ule", m.mk_bool_sort()), m); + expr_ref pred_e1(m_bv.mk_bv_sub(e1, m_bv.mk_numeral(1, sz)), m); + new_v = m.mk_or(delta, m.mk_eq(e1, m_bv.mk_numeral(0, sz))); + (*mc)->hide(delta); + (*mc)->add(v, m.mk_ite(delta, e1, pred_e1)); + return true; + } return false; } From 1d3ee70af4d5d800d92143315b84e37a5c6a5cfd Mon Sep 17 00:00:00 2001 From: Jamey Sharp Date: Sun, 8 Aug 2021 15:52:54 -0700 Subject: [PATCH 03/19] support bit-blasting bvand (#5458) --- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index 1f220d639..a846795e1 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -285,6 +285,7 @@ void OP(unsigned num_args, expr * const * args, expr_ref & result) { \ MK_BIN_AC_REDUCE(reduce_add, reduce_bin_add, mk_adder); MK_BIN_AC_REDUCE(reduce_mul, reduce_bin_mul, mk_multiplier); + MK_BIN_AC_REDUCE(reduce_and, reduce_bin_and, mk_and); MK_BIN_AC_REDUCE(reduce_or, reduce_bin_or, mk_or); MK_BIN_AC_REDUCE(reduce_xor, reduce_bin_xor, mk_xor); @@ -472,6 +473,9 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); SASSERT(num == 2); reduce_sle(args[0], args[1], result); return BR_DONE; + case OP_BAND: + reduce_and(num, args, result); + return BR_DONE; case OP_BOR: reduce_or(num, args, result); return BR_DONE; From 5de5f5a442ea7344eddc5f81d9e3d9ccac2a19f2 Mon Sep 17 00:00:00 2001 From: Jamey Sharp Date: Sun, 8 Aug 2021 15:53:07 -0700 Subject: [PATCH 04/19] report which operator bit-blast failed on (#5459) --- src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp | 11 +++++++---- 1 file changed, 7 insertions(+), 4 deletions(-) diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp index a846795e1..13e6a3511 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp +++ b/src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp @@ -358,8 +358,11 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); result = mk_mkbv(m_out); } - void throw_unsupported() { - throw rewriter_exception("operator is not supported, you must simplify the goal before applying bit-blasting"); + void throw_unsupported(func_decl * f) { + std::string msg = "operator "; + msg += f->get_name().str(); + msg += " is not supported, you must simplify the goal before applying bit-blasting"; + throw rewriter_exception(std::move(msg)); } void blast_bv_term(expr * t, expr_ref & result, proof_ref & result_pr) { @@ -425,7 +428,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); case OP_BUREM: case OP_BSMOD: if (m_blast_mul) - throw_unsupported(); // must simplify to DIV_I AND DIV0 + throw_unsupported(f); // must simplify to DIV_I AND DIV0 return BR_FAILED; // keep them case OP_BSDIV0: @@ -549,7 +552,7 @@ MK_PARAMETRIC_UNARY_REDUCE(reduce_sign_extend, mk_sign_extend); default: TRACE("bit_blaster", tout << "non-supported operator: " << f->get_name() << "\n"; for (unsigned i = 0; i < num; i++) tout << mk_ismt2_pp(args[i], m()) << std::endl;); - throw_unsupported(); + throw_unsupported(f); } } From e27a71bbcba910a594301dda6cd4b47fba5467ef Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Aug 2021 16:29:31 -0700 Subject: [PATCH 05/19] #5460 --- src/tactic/core/pb_preprocess_tactic.cpp | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index c9ee5d532..406b52b0f 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -44,6 +44,7 @@ class pb_preprocess_tactic : public tactic { struct rec { unsigned_vector pos, neg; rec() { } }; typedef obj_map var_map; ast_manager& m; + expr_ref_vector m_trail; pb_util pb; var_map m_vars; unsigned_vector m_ge; @@ -99,7 +100,7 @@ class pb_preprocess_tactic : public tactic { public: pb_preprocess_tactic(ast_manager& m, params_ref const& p = params_ref()): - m(m), pb(m), m_r(m) {} + m(m), m_trail(m), pb(m), m_r(m) {} ~pb_preprocess_tactic() override {} @@ -157,7 +158,7 @@ public: m_progress = false; // first eliminate variables var_map::iterator it = next_resolvent(m_vars.begin()); - while (it != m_vars.end()) { + while (it != m_vars.end()) { app * e = it->m_key; rec const& r = it->m_value; TRACE("pb", tout << mk_pp(e, m) << " " << r.pos.size() << " " << r.neg.size() << "\n";); @@ -235,6 +236,7 @@ private: m_ge.reset(); m_other.reset(); m_vars.reset(); + m_trail.reset(); } expr* negate(expr* e) { @@ -410,6 +412,7 @@ private: void insert(unsigned i, app* e, bool pos) { SASSERT(is_uninterp_const(e)); if (!m_vars.contains(e)) { + m_trail.push_back(e); m_vars.insert(e, rec()); } if (pos) { From 85da7407dc9cbd33454263ec6bd53cd9d7cb070a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Aug 2021 17:18:31 -0700 Subject: [PATCH 06/19] #5460 NB @nunoplopes - the code path regarding rewrite_uncstr could use some unit tests. --- src/tactic/core/reduce_invertible_tactic.cpp | 47 ++++++++++++++------ 1 file changed, 33 insertions(+), 14 deletions(-) diff --git a/src/tactic/core/reduce_invertible_tactic.cpp b/src/tactic/core/reduce_invertible_tactic.cpp index 23ae55da9..57df65e83 100644 --- a/src/tactic/core/reduce_invertible_tactic.cpp +++ b/src/tactic/core/reduce_invertible_tactic.cpp @@ -93,10 +93,11 @@ public: g->update(idx, f_new, new_pr, g->dep(idx)); } if (mc) g->add(mc.get()); - g->inc_depth(); + TRACE("invertible_tactic", g->display(tout);); + g->inc_depth(); } result.push_back(g.get()); - CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout);); + CTRACE("invertible_tactic", g->mc(), g->mc()->display(tout);); } void cleanup() override {} @@ -223,28 +224,46 @@ private: rational r; app* a = to_app(v); expr* fst_arg = a->get_arg(0); - bool fst_is_var = is_var(fst_arg); - for (unsigned i = 0, n = a->get_num_args(); i != n; ++i) { - auto arg = a->get_arg(i); - if (!m_parents[arg->get_id()].get() || is_var(arg) != fst_is_var) + for (expr* arg : *a) + if (!m_parents[arg->get_id()].get()) return false; - if (fst_is_var && to_var(arg)->get_idx() >= max_var) - return false; - - if (m_bv.is_numeral(arg, r) && r != mdl) - return false; - - if (i > 0 && !is_var(arg) && (!is_app(arg) || to_app(arg)->get_num_args() > 0)) + if (is_var(fst_arg)) { + for (expr* arg : *a) { + if (!is_var(arg)) + return false; + if (to_var(arg)->get_idx() >= max_var) + return false; + } + } + else { + bool first = true; + for (expr* arg : *a) { + if (!is_app(arg)) + return false; + if (is_uninterp_const(arg)) + continue; + if (m_bv.is_numeral(arg, r) && r == mdl) { + if (first || mdl.is_zero()) { + first = false; + continue; + } + else + return false; + } return false; + } } if (mc) { ensure_mc(mc); expr_ref num(m_bv.mk_numeral(mdl, fst_arg->get_sort()), m); for (unsigned i = 1, n = a->get_num_args(); i != n; ++i) { - (*mc)->add(a->get_arg(i), num); + expr* arg = a->get_arg(i); + if (m_bv.is_numeral(arg)) + continue; + (*mc)->add(arg, num); } } new_v = fst_arg; From af5fd1014f453976c9b34d053b0ca0cb70780c01 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 8 Aug 2021 17:33:49 -0700 Subject: [PATCH 07/19] #5460 --- src/sat/smt/arith_axioms.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp index 7e41aeb46..b1398c836 100644 --- a/src/sat/smt/arith_axioms.cpp +++ b/src/sat/smt/arith_axioms.cpp @@ -418,6 +418,7 @@ namespace arith { expr* p = nullptr, * q = nullptr; VERIFY(a.is_idiv(n, p, q)); theory_var v1 = internalize_def(p); + ensure_column(v1); lp::impq r1 = get_ivalue(v1); rational r2; From 225204e2f4939c25477b53f1c9483d85363bc6d1 Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 9 Aug 2021 10:48:56 -0700 Subject: [PATCH 08/19] updates related to issue #5140 (#5463) * updates related to issue #5140 * updated/simplified some cases * fixing feedback comments * fixed comments and added missing case for get_re_head_tail_reversed * two bug fixes and some other code improvements --- src/ast/rewriter/seq_rewriter.cpp | 199 +++++++++++++++++++++++++----- src/ast/rewriter/seq_rewriter.h | 20 +++ src/ast/seq_decl_plugin.cpp | 19 ++- src/util/state_graph.cpp | 2 +- 4 files changed, 202 insertions(+), 38 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 6bf44f4ba..fcf06f34c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -14,6 +14,7 @@ Author: Nikolaj Bjorner (nbjorner) 2015-12-5 Murphy Berzish 2017-02-21 Caleb Stanford 2020-07-07 + Margus Veanes 2021 --*/ @@ -872,6 +873,65 @@ br_status seq_rewriter::mk_seq_length(expr* a, expr_ref& result) { return BR_FAILED; } +/* +* In general constructs nth(t,0) but if t = substring(s,j,..) then simplifies to nth(s,j) +* This method assumes that |t| > 0. +*/ +expr_ref seq_rewriter::mk_seq_first(expr* t) { + expr_ref result(m()); + expr* s, * j, * k; + if (str().is_extract(t, s, j, k)) + result = str().mk_nth_i(s, j); + else + result = str().mk_nth_i(t, m_autil.mk_int(0)); + return result; +} + +/* +* In general constructs substring(t,1,|t|-1) but if t = substring(s,j,k) then simplifies to substring(s,j+1,k-1) +* This method assumes that |t| > 0. +*/ +expr_ref seq_rewriter::mk_seq_rest(expr* t) { + expr_ref result(m()); + expr* s, * j, * k; + expr_ref one(m_autil.mk_int(1), m()); + if (str().is_extract(t, s, j, k)) + result = str().mk_substr(s, m_autil.mk_add(j, one), m_autil.mk_sub(k, one)); + else + result = str().mk_substr(t, one, m_autil.mk_sub(str().mk_length(t), one)); + return result; +} + +/* +* In general constructs nth(t,|t|-1) but if t = substring(s,j,k) then simplifies to nth(s,j+k-1) +* This method assumes that |t| > 0. +*/ +expr_ref seq_rewriter::mk_seq_last(expr* t) { + expr_ref result(m()); + expr* s, * j, * k; + expr_ref one(m_autil.mk_int(1), m()); + if (str().is_extract(t, s, j, k)) + result = str().mk_nth_i(s, m_autil.mk_sub(m_autil.mk_add(j, k), one)); + else + result = str().mk_nth_i(t, m_autil.mk_sub(str().mk_length(t), one)); + return result; +} + +/* +* In general constructs substring(t,0,|t|-1) but if t = substring(s,j,k) then simplifies to substring(s,j,k-1) +* This method assumes that |t| > 0 holds. +*/ +expr_ref seq_rewriter::mk_seq_butlast(expr* t) { + expr_ref result(m()); + expr* s, * j, * k; + expr_ref one(m_autil.mk_int(1), m()); + if (str().is_extract(t, s, j, k)) + result = str().mk_substr(s, j, m_autil.mk_sub(k, one)); + else + result = str().mk_substr(t, m_autil.mk_int(0), m_autil.mk_sub(str().mk_length(t), one)); + return result; +} + /* Lift all ite expressions to the top level, safely throttled to not blowup the size of the expression. @@ -1893,13 +1953,13 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& return BR_REWRITE1; } zstring s1, s2; + expr_ref_vector strs(m()); if (str().is_string(a, s1) && str().is_string(b, s2)) { SASSERT(s2.length() > 0); if (s1.length() < s2.length()) { result = a; return BR_DONE; } - expr_ref_vector strs(m()); for (unsigned i = 0; i < s1.length(); ++i) { if (s1.length() >= s2.length() + i && s2 == s1.extract(i, s2.length())) { @@ -1912,11 +1972,62 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& result = str().mk_concat(strs, a->get_sort()); return BR_REWRITE_FULL; } - // TBD: add case when a, b are concatenation of units that are values. - // in this case we can use a similar loop as for strings. + expr_ref_vector a_vals(m()); + expr_ref_vector b_vals(m()); + if (try_get_unit_values(a, a_vals) && try_get_unit_values(b, b_vals)) { + replace_all_subvectors(a_vals, b_vals, c, strs); + result = str().mk_concat(strs, a->get_sort()); + return BR_REWRITE_FULL; + } + + //TODO: the case when a is a unit or concatenation of units while b is a string + //or the other way around -- if that situation is possible at all -- is similar to the above return BR_FAILED; } +/* +* Returns false if s is not a single unit value or concatenation of unit values. +* Else extracts the units from s into vals and returns true. +*/ +bool seq_rewriter::try_get_unit_values(expr* s, expr_ref_vector& vals) { + expr* h, * t, * v; + t = s; + //collect all unit values from s, if not all elements are unit-values then fail + while (str().is_concat(t, h, t)) + if (str().is_unit(h, v) && m().is_value(v)) + vals.push_back(h); + else + return false; + //add the last element + if (str().is_unit(t, v) && m().is_value(v)) + vals.push_back(t); + else + return false; + return true; +} + +/* +* Replace all subvectors of b in a by c +*/ +void seq_rewriter::replace_all_subvectors(expr_ref_vector const& a, expr_ref_vector const& b, expr* c, expr_ref_vector& result) { + unsigned int i = 0; + unsigned int k = b.size(); + while (i + k <= a.size()) { + //if a[i..i+k-1] equals b then replace it by c and inceremnt i by k + int j = 0; + while (j < k && b[j] == a[i + j]) j += 1; + if (j < k) //the equality failed + result.push_back(a[i++]); + else { //the equality succeeded + result.push_back(c); + i += k; + } + } + //add the trailing elements from a + while (i < a.size()) + result.push_back(a[i++]); +} + br_status seq_rewriter::mk_seq_replace_re_all(expr* a, expr* b, expr* c, expr_ref& result) { return BR_FAILED; } @@ -2521,12 +2632,18 @@ bool seq_rewriter::get_re_head_tail_reversed(expr* r, expr_ref& head, expr_ref& if (re().is_concat(r, r1, r2)) { unsigned len = re().min_length(r2); if (len != UINT_MAX && re().max_length(r2) == len) { - head = r1; - tail = r2; + if (get_re_head_tail_reversed(r1, head, tail)) + // left associative binding of concat + tail = mk_re_append(tail, r2); + else { + // right associative binding of concat + head = r1; + tail = r2; + } return true; } if (get_re_head_tail_reversed(r2, head, tail)) { - head = re().mk_concat(r1, head); + head = mk_re_append(r1, head); return true; } } @@ -3059,7 +3176,8 @@ expr_ref seq_rewriter::mk_der_op_rec(decl_kind k, expr* a, expr* b) { return result; } // Order with higher IDs on the outside - if (get_id(ca) < get_id(cb)) { + bool is_symmetric = k == OP_RE_UNION || k == OP_RE_INTERSECT; + if (is_symmetric && get_id(ca) < get_id(cb)) { std::swap(a, b); std::swap(ca, cb); std::swap(notca, notcb); @@ -3348,7 +3466,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { //while mk_empty() = [], because deriv(epsilon) = [] = nothing return mk_empty(); } - else if (str().is_itos(r1, r2)) { + else if (str().is_itos(r1)) { // // here r1 = (str.from_int r2) and r2 is non-ground // or else the expression would have been simplified earlier @@ -3356,27 +3474,45 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { // '0' <= elem <= '9' // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] // - hd = str().mk_nth_i(r1, m_autil.mk_int(0)); + hd = mk_seq_first(r1); m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), m().mk_eq(hd, ele), result); - tl = re().mk_to_re(str().mk_substr(r1, m_autil.mk_int(1), m_autil.mk_sub(str().mk_length(r1), m_autil.mk_int(1)))); + tl = re().mk_to_re(mk_seq_rest(r1)); + return re_and(result, tl); + } + else { + // recall: [] denotes the empty language (nothing) regex, () denotes epsilon or empty sequence + // construct the term (if (r1 != () and (ele = (first r1)) then (to_re (rest r1)) else [])) + hd = mk_seq_first(r1); + m_br.mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); + tl = re().mk_to_re(mk_seq_rest(r1)); return re_and(result, tl); } } - else if (re().is_reverse(r, r1) && re().is_to_re(r1, r2)) { - // Reverses are rewritten so that the only derivative case is - // derivative of a reverse of a string. (All other cases stuck) - // This is analagous to the previous is_to_re case. - expr_ref hd(m()), tl(m()); - if (get_head_tail_reversed(r2, hd, tl)) { - // Use mk_der_cond to normalize - STRACE("seq_verbose", tout << "deriv reverse to_re" << std::endl;); - result = m().mk_eq(ele, tl); - result = mk_der_cond(result, ele, seq_sort); - result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd))); - return result; - } - else if (str().is_empty(r2)) { - return mk_empty(); + else if (re().is_reverse(r, r1)) { + if (re().is_to_re(r1, r2)) { + // First try to exctract hd and tl such that r = hd ++ tl and |tl|=1 + expr_ref hd(m()), tl(m()); + if (get_head_tail_reversed(r2, hd, tl)) { + // Use mk_der_cond to normalize + STRACE("seq_verbose", tout << "deriv reverse to_re" << std::endl;); + result = m().mk_eq(ele, tl); + result = mk_der_cond(result, ele, seq_sort); + result = mk_der_concat(result, re().mk_reverse(re().mk_to_re(hd))); + return result; + } + else if (str().is_empty(r2)) { + return mk_empty(); + } + else { + // construct the term (if (r2 != () and (ele = (last r2)) then reverse(to_re (butlast r2)) else [])) + // hd = first of reverse(r2) i.e. last of r2 + // tl = rest of reverse(r2) i.e. butlast of r2 + //hd = str().mk_nth_i(r2, m_autil.mk_sub(str().mk_length(r2), m_autil.mk_int(1))); + hd = mk_seq_last(r2); + m_br.mk_and(m().mk_not(m().mk_eq(r2, str().mk_empty(seq_sort))), m().mk_eq(hd, ele), result); + tl = re().mk_to_re(mk_seq_butlast(r2)); + return re_and(result, re().mk_reverse(tl)); + } } } else if (re().is_range(r, r1, r2)) { @@ -3423,10 +3559,7 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { STRACE("seq_verbose", tout << "deriv of_pred" << std::endl;); return mk_der_cond(result, ele, seq_sort); } - // stuck cases: re.derivative, variable, - // str.to_re if the head of the string can't be obtained, - // and re.reverse if not applied to a string or if the tail char - // of the string can't be obtained + // stuck cases: re.derivative, re variable, return expr_ref(re().mk_derivative(ele, r), m()); } @@ -3662,12 +3795,14 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { } if (get_re_head_tail_reversed(b, hd, tl)) { SASSERT(re().min_length(tl) == re().max_length(tl)); - expr_ref len_tl(m_autil.mk_int(re().min_length(tl)), m()); + expr_ref len_tl(m_autil.mk_int(re().min_length(tl)), m()); expr_ref len_a(str().mk_length(a), m()); expr_ref len_hd(m_autil.mk_sub(len_a, len_tl), m()); + expr* s = nullptr; result = m().mk_and(m_autil.mk_ge(len_a, len_tl), - re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd), - re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl)); + re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd), + (false && re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) : + re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl))); return BR_REWRITE_FULL; } diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h index c779a5f73..f726a4673 100644 --- a/src/ast/rewriter/seq_rewriter.h +++ b/src/ast/rewriter/seq_rewriter.h @@ -180,6 +180,16 @@ class seq_rewriter { expr_ref mk_seq_concat(expr* a, expr* b); + // Construct the expressions for taking the first element, the last element, the rest, and the butlast element + expr_ref mk_seq_first(expr* s); + expr_ref mk_seq_rest(expr* s); + expr_ref mk_seq_last(expr* s); + expr_ref mk_seq_butlast(expr* s); + + bool try_get_unit_values(expr* s, expr_ref_vector& result); + //replace b in a by c into result + void replace_all_subvectors(expr_ref_vector const& as, expr_ref_vector const& bs, expr* c, expr_ref_vector& result); + // Calculate derivative, memoized and enforcing a normal form expr_ref is_nullable_rec(expr* r); expr_ref mk_derivative_rec(expr* ele, expr* r); @@ -344,6 +354,16 @@ public: return result; } + /* + * makes concat and simplifies + */ + expr_ref mk_re_append(expr* r1, expr* r2) { + expr_ref result(m()); + if (mk_re_concat(r1, r2, result) == BR_FAILED) + result = re().mk_concat(r1, r2); + return result; + } + /** * check if regular expression is of the form all ++ s ++ all ++ t + u ++ all, where, s, t, u are sequences */ diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 6695d9497..273eac2c5 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -911,7 +911,7 @@ unsigned seq_util::str::max_length(expr* s) const { return UINT_MAX; }; while (is_concat(s, s1, s2)) { - result = u.max_plus(get_length(s), result); + result = u.max_plus(get_length(s1), result); s = s2; } result = u.max_plus(get_length(s), result); @@ -1058,6 +1058,7 @@ app* seq_util::rex::mk_epsilon(sort* seq_sort) { */ std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) const { SASSERT(re.u.is_seq(s)); + zstring z; if (re.u.str.is_empty(s)) out << "()"; else if (re.u.str.is_unit(s)) @@ -1068,6 +1069,10 @@ std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) for (expr* e : es) compact_helper_seq(out, e); } + else if (re.u.str.is_string(s, z)) { + for (int i = 0; i < z.length(); i++) + out << (char)z[i]; + } //using braces to indicate 'full' output //for example an uninterpreted constant X will be printed as {X} //while a unit sequence "X" will be printed as X @@ -1100,7 +1105,7 @@ bool seq_util::rex::pp::can_skip_parenth(expr* r) const { std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const { expr* e; unsigned n = 0; - if (re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) { + if ((re.u.str.is_unit(s, e) && re.u.is_const_char(e, n)) || re.u.is_const_char(s, n)) { char c = (char)n; if (c == '\n') out << "\\n"; @@ -1148,7 +1153,11 @@ std::ostream& seq_util::rex::pp::seq_unit(std::ostream& out, expr* s) const { std::ostream& seq_util::rex::pp::display(std::ostream& out) const { expr* r1 = nullptr, * r2 = nullptr, * s = nullptr, * s2 = nullptr; unsigned lo = 0, hi = 0; - if (re.is_full_char(e)) + if (re.u.is_char(e)) + return seq_unit(out, e); + else if (re.u.is_seq(e)) + return compact_helper_seq(out, e); + else if (re.is_full_char(e)) return out << "."; else if (re.is_full_seq(e)) return out << ".*"; @@ -1163,9 +1172,9 @@ std::ostream& seq_util::rex::pp::display(std::ostream& out) const { else if (re.is_concat(e, r1, r2)) return out << pp(re, r1) << pp(re, r2); else if (re.is_union(e, r1, r2)) - return out << pp(re, r1) << "|" << pp(re, r2); + return out << "(" << pp(re, r1) << "|" << pp(re, r2) << ")"; else if (re.is_intersection(e, r1, r2)) - return out << "(" << pp(re, r1) << (html_encode ? ")&(": ")&(" ) << pp(re, r2) << ")"; + return out << "(" << pp(re, r1) << "&" /*(html_encode ? ")&(" : ")&(")*/ << pp(re, r2) << ")"; else if (re.is_complement(e, r1)) { if (can_skip_parenth(r1)) return out << "~" << pp(re, r1); diff --git a/src/util/state_graph.cpp b/src/util/state_graph.cpp index 400d1f586..2cc4158c7 100644 --- a/src/util/state_graph.cpp +++ b/src/util/state_graph.cpp @@ -13,7 +13,7 @@ Abstract: Author: Caleb Stanford (calebstanford-msr / cdstanford) 2020-7 - + Margus Veanes 2020-8 --*/ #include "state_graph.h" From aa7e9b09f363c160af238eaaf0341b50b3fa0f2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Aug 2021 14:22:48 -0700 Subject: [PATCH 09/19] fix equality rewrite with itos Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index fcf06f34c..1a3208d0f 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -2014,8 +2014,9 @@ void seq_rewriter::replace_all_subvectors(expr_ref_vector const& a, expr_ref_vec unsigned int k = b.size(); while (i + k <= a.size()) { //if a[i..i+k-1] equals b then replace it by c and inceremnt i by k - int j = 0; - while (j < k && b[j] == a[i + j]) j += 1; + unsigned j = 0; + while (j < k && b[j] == a[i + j]) + ++j; if (j < k) //the equality failed result.push_back(a[i++]); else { //the equality succeeded @@ -5109,6 +5110,12 @@ bool seq_rewriter::reduce_itos(expr_ref_vector& ls, expr_ref_vector& rs, str().is_itos(ls.get(0), n) && is_string(rs.size(), rs.data(), s)) { std::string s1 = s.encode(); + for (auto c : s1) { + if (!('0' <= c && c <= '9')) + return false; + } + if (s1.size() > 1 && s1[0] == '0') + return false; try { rational r(s1.c_str()); if (s1 == r.to_string()) { @@ -5150,6 +5157,10 @@ bool seq_rewriter::reduce_eq_empty(expr* l, expr* r, expr_ref& result) { result = m().mk_or(fmls); return true; } + if (str().is_itos(r, s)) { + result = m_autil.mk_lt(s, m_autil.mk_int(0)); + return true; + } return false; } From 3eb849ad9e4a270ac0e2eddd01a7ba78f5b82df3 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 9 Aug 2021 15:32:04 -0700 Subject: [PATCH 10/19] rewrite equality too Signed-off-by: Nikolaj Bjorner --- src/ast/rewriter/seq_rewriter.cpp | 2 +- src/ast/seq_decl_plugin.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 1a3208d0f..12c0e560b 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -1950,7 +1950,7 @@ br_status seq_rewriter::mk_seq_replace_all(expr* a, expr* b, expr* c, expr_ref& } if (a == b) { result = m().mk_ite(str().mk_is_empty(b), str().mk_empty(a->get_sort()), c); - return BR_REWRITE1; + return BR_REWRITE2; } zstring s1, s2; expr_ref_vector strs(m()); diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 273eac2c5..82ab83681 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -1070,7 +1070,7 @@ std::ostream& seq_util::rex::pp::compact_helper_seq(std::ostream& out, expr* s) compact_helper_seq(out, e); } else if (re.u.str.is_string(s, z)) { - for (int i = 0; i < z.length(); i++) + for (unsigned i = 0; i < z.length(); i++) out << (char)z[i]; } //using braces to indicate 'full' output From 22bb4c2db731a9b1a077bb9d7ca42a54ce50ebce Mon Sep 17 00:00:00 2001 From: Margus Veanes Date: Mon, 9 Aug 2021 17:48:35 -0700 Subject: [PATCH 11/19] more fixes related to issue #5140 (#5466) * instead of u in to_re(s) make u = s * bug fix: added missing emptiness check --- src/ast/rewriter/seq_rewriter.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 12c0e560b..63a5044e5 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -3476,7 +3476,8 @@ expr_ref seq_rewriter::mk_derivative_rec(expr* ele, expr* r) { // if ((isdigit ele) and (ele = (hd r1))) then (to_re (tl r1)) else [] // hd = mk_seq_first(r1); - m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), m().mk_eq(hd, ele), result); + m_br.mk_and(u().mk_le(m_util.mk_char('0'), ele), u().mk_le(ele, m_util.mk_char('9')), + m().mk_and(m().mk_not(m().mk_eq(r1, str().mk_empty(seq_sort))), m().mk_eq(hd, ele)), result); tl = re().mk_to_re(mk_seq_rest(r1)); return re_and(result, tl); } @@ -3802,7 +3803,7 @@ br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) { expr* s = nullptr; result = m().mk_and(m_autil.mk_ge(len_a, len_tl), re().mk_in_re(str().mk_substr(a, m_autil.mk_int(0), len_hd), hd), - (false && re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) : + (re().is_to_re(tl, s) ? m().mk_eq(s, str().mk_substr(a, len_hd, len_tl)) : re().mk_in_re(str().mk_substr(a, len_hd, len_tl), tl))); return BR_REWRITE_FULL; } From 4beb29d45e76145caf8f67255ab442e50ec5c01d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Aug 2021 09:22:12 -0700 Subject: [PATCH 12/19] fix #5469 documentation bug --- src/ast/rewriter/seq_axioms.cpp | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index edc91e21f..6458e36af 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1043,12 +1043,19 @@ namespace seq { } /** + suffix(s, t): + - the sequence s is a suffix of t. - suffix(s, t) => s = seq.suffix_inv(s, t) + t + Positive case is handled by the solver when the atom is asserted + suffix(s, t) => t = seq.suffix_inv(s, t) + s + + Negative case is handled by axioms when the negation of the atom is asserted ~suffix(s, t) => len(s) > len(t) or s = y(s, t) + unit(c(s, t)) + x(s, t) ~suffix(s, t) => len(s) > len(t) or t = z(s, t) + unit(d(s, t)) + x(s, t) ~suffix(s, t) => len(s) > len(t) or c(s,t) != d(s,t) + Symmetric axioms are provided for prefix + */ void axioms::suffix_axiom(expr* e) { From 2075cb9fa4cef371a85845cf5a706897c3ecc0d4 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Aug 2021 09:29:39 -0700 Subject: [PATCH 13/19] remove useless literal found during review #5470 --- src/ast/rewriter/seq_axioms.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/ast/rewriter/seq_axioms.cpp b/src/ast/rewriter/seq_axioms.cpp index 6458e36af..bcda71e54 100644 --- a/src/ast/rewriter/seq_axioms.cpp +++ b/src/ast/rewriter/seq_axioms.cpp @@ -1108,7 +1108,7 @@ namespace seq { expr_ref c = m_sk.mk("seq.prefix.c", s, t, char_sort); expr_ref d = m_sk.mk("seq.prefix.d", s, t, char_sort); add_clause(lit, s_gt_t, mk_seq_eq(s, mk_concat(x, seq.str.mk_unit(c), y))); - add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z)), mk_seq_eq(t, x)); + add_clause(lit, s_gt_t, mk_seq_eq(t, mk_concat(x, seq.str.mk_unit(d), z))); add_clause(lit, s_gt_t, ~mk_eq(c, d)); #endif } From 391db898d36539b5755b69fc75582ba20a39d0a8 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Aug 2021 09:45:17 -0700 Subject: [PATCH 14/19] lost update from August 3 #5468 --- src/tactic/core/pb_preprocess_tactic.cpp | 5 +---- 1 file changed, 1 insertion(+), 4 deletions(-) diff --git a/src/tactic/core/pb_preprocess_tactic.cpp b/src/tactic/core/pb_preprocess_tactic.cpp index 406b52b0f..1d4805c67 100644 --- a/src/tactic/core/pb_preprocess_tactic.cpp +++ b/src/tactic/core/pb_preprocess_tactic.cpp @@ -507,10 +507,7 @@ private: bool found = false; for (unsigned j = 0; j < args2.size(); ++j) { if (is_complement(args1.get(i), args2.get(j))) { - if (i == 0) { - min_coeff = coeffs2[j]; - } - else if (min_coeff > coeffs2[j]) { + if (i == 0 || min_coeff > coeffs2[j]) { min_coeff = coeffs2[j]; min_index = j; } From 081cdbd762732445653206de95f7d791876ff00b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Aug 2021 10:46:47 -0700 Subject: [PATCH 15/19] fix #5468 --- .../portfolio/solver_subsumption_tactic.cpp | 37 +++++++++++-------- 1 file changed, 21 insertions(+), 16 deletions(-) diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index ac6cdede2..2e823b9ff 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -41,31 +41,36 @@ class solver_subsumption_tactic : public tactic { /** * Check subsumption (a \/ b \/ c) - * if (a \/ b) is already implied - * Use a naive algorithm (not binary disection here) + * if (a \/ b) is already implied or if b is false in F + * + * If + * F |= (a \/ b \/ c) + * Then replace (a \/ b \/ c) by true + * + * If + * F |= !b + * Then replace (a \/ b \/ c) by (a \/ c) + * */ bool simplify(expr_ref& f) { + expr_ref_vector fmls(m), ors(m), prefix(m); + expr_ref nf(m.mk_not(f), m); + fmls.push_back(nf); + lbool is_sat = m_solver->check_sat(fmls); + if (is_sat == l_false) { + f = m.mk_true(); + return true; + } if (!m.is_or(f)) return false; - expr_ref_vector ors(m); ors.append(to_app(f)->get_num_args(), to_app(f)->get_args()); - expr_ref_vector prefix(m); for (unsigned i = 0; i < ors.size(); ++i) { - expr_ref_vector fmls(m); - fmls.append(prefix); - for (unsigned k = i + 1; k < ors.size(); ++k) - fmls.push_back(m.mk_not(ors.get(k))); - lbool is_sat = m_solver->check_sat(fmls); - if (is_sat == l_false) - continue; fmls.reset(); - fmls.push_back(ors.get(i)); - + fmls.push_back(ors.get(i)); is_sat = m_solver->check_sat(fmls); - if (is_sat == l_false) - continue; - prefix.push_back(ors.get(i)); + if (is_sat != l_false) + prefix.push_back(ors.get(i)); } if (ors.size() != prefix.size()) { ors.reset(); From 7ab7b8646b9b4fbfec63a573175abea103f2c45d Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 10 Aug 2021 14:47:26 -0700 Subject: [PATCH 16/19] #5454 --- src/sat/smt/q_ematch.cpp | 4 ++++ src/sat/smt/q_mam.cpp | 15 +++++++-------- 2 files changed, 11 insertions(+), 8 deletions(-) diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index c83680f72..a2c27fd60 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -490,6 +490,10 @@ namespace q { TRACE("q", tout << "add " << mk_pp(_q, m) << "\n";); clause* c = clausify(_q); quantifier* q = c->q(); + if (m_q2clauses.contains(q)) { + dealloc(c); + return; + } ensure_ground_enodes(*c); m_clauses.push_back(c); m_q2clauses.insert(q, c->index()); diff --git a/src/sat/smt/q_mam.cpp b/src/sat/smt/q_mam.cpp index 000f76879..8b75e87ea 100644 --- a/src/sat/smt/q_mam.cpp +++ b/src/sat/smt/q_mam.cpp @@ -414,7 +414,7 @@ namespace q { enode_vector m_candidates; #ifdef Z3DEBUG egraph * m_egraph; - ptr_vector m_patterns; + svector> m_patterns; #endif #ifdef _PROFILE_MAM stopwatch m_watch; @@ -568,7 +568,7 @@ namespace q { m_egraph = ctx; } - ptr_vector & get_patterns() { + svector> & get_patterns() { return m_patterns; } #endif @@ -578,8 +578,8 @@ namespace q { if (m_egraph) { ast_manager & m = m_egraph->get_manager(); out << "patterns:\n"; - for (app* a : m_patterns) - out << mk_pp(a, m) << "\n"; + for (auto [q, a] : m_patterns) + out << mk_pp(q, m) << " " << mk_pp(a, m) << "\n"; } #endif out << "function: " << m_root_lbl->get_name(); @@ -2862,12 +2862,11 @@ namespace q { // The E-matching engine that was built when all + and * applications were binary. // We ignore the pattern if it does not have the expected number of arguments. // This is not the ideal solution, but it avoids possible crashes. - if (tree->expected_num_args() == p->get_num_args()) { + if (tree->expected_num_args() == p->get_num_args()) m_compiler.insert(tree, qa, mp, first_idx, false); - } } - DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(mp); - ctx.push(push_back_trail(m_trees[lbl_id]->get_patterns()));); + DEBUG_CODE(m_trees[lbl_id]->get_patterns().push_back(std::make_pair(qa, mp)); + ctx.push(push_back_trail, false>(m_trees[lbl_id]->get_patterns()));); TRACE("trigger_bug", tout << "after add_pattern, first_idx: " << first_idx << "\n"; m_trees[lbl_id]->display(tout);); } From 4f2211baab1951f588af9196162289664cc634ea Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Aug 2021 04:36:48 -0700 Subject: [PATCH 17/19] fix solver-subsumption again, #5468 (negation was swapped in original wrong subsumption check, then soundness fix removed core subsumption functionality) Signed-off-by: Nikolaj Bjorner --- .../portfolio/solver_subsumption_tactic.cpp | 27 +++++++++++-------- 1 file changed, 16 insertions(+), 11 deletions(-) diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index 2e823b9ff..5a4de001f 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -41,20 +41,19 @@ class solver_subsumption_tactic : public tactic { /** * Check subsumption (a \/ b \/ c) - * if (a \/ b) is already implied or if b is false in F + * + * If + * F |= (a \/ ~b \/ c) + * Then replace (a \/ b \/ c) by (a \/ c) * * If * F |= (a \/ b \/ c) * Then replace (a \/ b \/ c) by true * - * If - * F |= !b - * Then replace (a \/ b \/ c) by (a \/ c) - * */ bool simplify(expr_ref& f) { - expr_ref_vector fmls(m), ors(m), prefix(m); + expr_ref_vector fmls(m), ors(m), nprefix(m), prefix(m); expr_ref nf(m.mk_not(f), m); fmls.push_back(nf); lbool is_sat = m_solver->check_sat(fmls); @@ -65,12 +64,18 @@ class solver_subsumption_tactic : public tactic { if (!m.is_or(f)) return false; ors.append(to_app(f)->get_num_args(), to_app(f)->get_args()); + for (expr* arg : ors) + nprefix.push_back(mk_not(m, arg)); for (unsigned i = 0; i < ors.size(); ++i) { - fmls.reset(); - fmls.push_back(ors.get(i)); - is_sat = m_solver->check_sat(fmls); - if (is_sat != l_false) - prefix.push_back(ors.get(i)); + expr* arg = ors.get(i); + expr_ref save(nprefix.get(i), m); + nprefix[i] = arg; + is_sat = m_solver->check_sat(nprefix); + nprefix[i] = save; + if (is_sat == l_false) + nprefix[i] = m.mk_true(); + else + prefix.push_back(arg); } if (ors.size() != prefix.size()) { ors.reset(); From d1d64bbe599cb1634df86b87215a78a6ccbdbb0a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Aug 2021 04:55:20 -0700 Subject: [PATCH 18/19] #5454 --- src/sat/sat_simplifier.cpp | 12 ++++++++---- .../portfolio/solver_subsumption_tactic.cpp | 16 ++++++++-------- 2 files changed, 16 insertions(+), 12 deletions(-) diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp index 7a6957467..a9910852e 100644 --- a/src/sat/sat_simplifier.cpp +++ b/src/sat/sat_simplifier.cpp @@ -2022,10 +2022,14 @@ namespace sat { } remove_bin_clauses(pos_l); remove_bin_clauses(neg_l); - remove_clauses(pos_occs, pos_l); - remove_clauses(neg_occs, neg_l); - pos_occs.reset(); - neg_occs.reset(); + { + clause_use_list& pos_occs = m_use_list.get(pos_l); + clause_use_list& neg_occs = m_use_list.get(neg_l); + remove_clauses(pos_occs, pos_l); + remove_clauses(neg_occs, neg_l); + pos_occs.reset(); + neg_occs.reset(); + } return true; } diff --git a/src/tactic/portfolio/solver_subsumption_tactic.cpp b/src/tactic/portfolio/solver_subsumption_tactic.cpp index 5a4de001f..3a23f5984 100644 --- a/src/tactic/portfolio/solver_subsumption_tactic.cpp +++ b/src/tactic/portfolio/solver_subsumption_tactic.cpp @@ -53,7 +53,7 @@ class solver_subsumption_tactic : public tactic { */ bool simplify(expr_ref& f) { - expr_ref_vector fmls(m), ors(m), nprefix(m), prefix(m); + expr_ref_vector fmls(m), ors(m), nors(m), prefix(m); expr_ref nf(m.mk_not(f), m); fmls.push_back(nf); lbool is_sat = m_solver->check_sat(fmls); @@ -65,15 +65,15 @@ class solver_subsumption_tactic : public tactic { return false; ors.append(to_app(f)->get_num_args(), to_app(f)->get_args()); for (expr* arg : ors) - nprefix.push_back(mk_not(m, arg)); + nors.push_back(mk_not(m, arg)); for (unsigned i = 0; i < ors.size(); ++i) { expr* arg = ors.get(i); - expr_ref save(nprefix.get(i), m); - nprefix[i] = arg; - is_sat = m_solver->check_sat(nprefix); - nprefix[i] = save; + expr_ref save(nors.get(i), m); + nors[i] = arg; + is_sat = m_solver->check_sat(nors); + nors[i] = save; if (is_sat == l_false) - nprefix[i] = m.mk_true(); + nors[i] = m.mk_true(); else prefix.push_back(arg); } @@ -141,7 +141,7 @@ public: } void collect_param_descrs(param_descrs& r) override { - r.insert("max_conflicts", CPK_UINT, "(default: 10) maximal number of conflicts allowed per solver call."); + r.insert("max_conflicts", CPK_UINT, "(default: 2) maximal number of conflicts allowed per solver call."); } void operator()(goal_ref const& g, goal_ref_buffer& result) override { From 496ec5f2b44bf6c7460b16326311a8c2b43508bd Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 11 Aug 2021 05:00:02 -0700 Subject: [PATCH 19/19] #5454 Signed-off-by: Nikolaj Bjorner --- src/sat/smt/array_model.cpp | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/smt/array_model.cpp b/src/sat/smt/array_model.cpp index b4e7d3cab..74594e5a0 100644 --- a/src/sat/smt/array_model.cpp +++ b/src/sat/smt/array_model.cpp @@ -73,7 +73,7 @@ namespace array { obj_map num_occ; for (euf::enode* p : euf::enode_parents(n->get_root())) { if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n->get_root()) { - expr* v = values.get(p->get_root_id()); + expr* v = values.get(p->get_root_id(), nullptr); if (!v) continue; unsigned no = 0; @@ -92,7 +92,7 @@ namespace array { for (euf::enode* p : euf::enode_parents(n)) { if (a.is_select(p->get_expr()) && p->get_arg(0)->get_root() == n) { - expr* value = values.get(p->get_root_id()); + expr* value = values.get(p->get_root_id(), nullptr); if (!value || value == fi->get_else()) continue; args.reset();