From 7e2783c6a2be38ffbf3d72de5dafaaa6972d2e2a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 8 Feb 2016 15:25:53 +0000 Subject: [PATCH 1/5] Fixed javadoc links in comments. Relates to #401. --- src/api/java/Solver.java | 14 +++++++------- 1 file changed, 7 insertions(+), 7 deletions(-) diff --git a/src/api/java/Solver.java b/src/api/java/Solver.java index f312da051..231326107 100644 --- a/src/api/java/Solver.java +++ b/src/api/java/Solver.java @@ -127,13 +127,13 @@ public class Solver extends Z3Object * using the Boolean constants in ps. * * Remarks: - * This API is an alternative to with assumptions for + * This API is an alternative to {@link check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using + * of the Boolean variables provided using {@link assertAndTrack} * and the Boolean literals - * provided using with assumptions. + * provided using {@link check} with assumptions. **/ public void assertAndTrack(BoolExpr[] constraints, BoolExpr[] ps) { @@ -152,13 +152,13 @@ public class Solver extends Z3Object * using the Boolean constant p. * * Remarks: - * This API is an alternative to with assumptions for + * This API is an alternative to {@link check} with assumptions for * extracting unsat cores. * Both APIs can be used in the same solver. The unsat core will contain a * combination - * of the Boolean variables provided using + * of the Boolean variables provided using {@link assertAndTrack} * and the Boolean literals - * provided using with assumptions. + * provided using {@link check} with assumptions. */ public void assertAndTrack(BoolExpr constraint, BoolExpr p) { @@ -294,7 +294,7 @@ public class Solver extends Z3Object } /** - * Create a clone of the current solver with respect to ctx. + * Create a clone of the current solver with respect to{@code ctx}. */ public Solver translate(Context ctx) { From a2f376f9d6dc84447c1a5b53b32a968ec1215d78 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 8 Feb 2016 17:17:49 +0000 Subject: [PATCH 2/5] Fixed memory leak in theory_fpa. Relates to #436 --- src/smt/theory_fpa.cpp | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp index 16f883548..23e1f746d 100644 --- a/src/smt/theory_fpa.cpp +++ b/src/smt/theory_fpa.cpp @@ -26,17 +26,17 @@ namespace smt { class fpa2bv_conversion_trail_elem : public trail { ast_manager & m; - obj_map & m_conversions; - expr * m_e; + obj_map & m_map; + expr_ref key; public: - fpa2bv_conversion_trail_elem(ast_manager & m, obj_map & c, expr * e) : - m(m), m_conversions(c), m_e(e) { m.inc_ref(e); } - virtual ~fpa2bv_conversion_trail_elem() {} + fpa2bv_conversion_trail_elem(ast_manager & m, obj_map & map, expr * e) : + m(m), m_map(map), key(e, m) { } + virtual ~fpa2bv_conversion_trail_elem() { } virtual void undo(theory_fpa & th) { - expr * v = m_conversions.find(m_e); - m_conversions.remove(m_e); - m.dec_ref(v); - m.dec_ref(m_e); + expr * val = m_map.find(key); + m_map.remove(key); + m.dec_ref(val); + key = 0; } }; @@ -153,6 +153,8 @@ namespace smt { theory_fpa::~theory_fpa() { + m_trail_stack.reset(); + if (m_is_initialized) { ast_manager & m = get_manager(); dec_ref_map_values(m, m_conversions); From 133e3693deb0cd5900058161c26739493e275d10 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Feb 2016 11:08:33 +0000 Subject: [PATCH 3/5] fix bug in replace built-in and move length-equality propagation to branch final check Signed-off-by: Nikolaj Bjorner --- src/ast/seq_decl_plugin.cpp | 7 +- src/smt/theory_seq.cpp | 141 +++++++++++++++++++++++++++--------- src/smt/theory_seq.h | 5 ++ 3 files changed, 115 insertions(+), 38 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index f3e696879..7517790a3 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -140,8 +140,8 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { return zstring(*this); } bool found = false; - for (unsigned i = 0; i <= length() - src.length(); ++i) { - bool eq = !found; + for (unsigned i = 0; i < length(); ++i) { + bool eq = !found && i + src.length() <= length(); for (unsigned j = 0; eq && j < src.length(); ++j) { eq = m_buffer[i+j] == src[j]; } @@ -154,9 +154,6 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { result.m_buffer.push_back(m_buffer[i]); } } - for (unsigned i = length() - src.length() + 1; i < length(); ++i) { - result.m_buffer.push_back(m_buffer[i]); - } return result; } diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp index df96f9c20..e11ca806a 100644 --- a/src/smt/theory_seq.cpp +++ b/src/smt/theory_seq.cpp @@ -266,6 +266,16 @@ bool theory_seq::branch_variable() { context& ctx = get_context(); unsigned sz = m_eqs.size(); int start = ctx.get_random_value(); + + for (unsigned i = 0; !ctx.inconsistent() && i < m_eqs.size(); ++i) { + eq const& e = m_eqs[(i + start) % m_eqs.size()]; + if (reduce_length_eq(e.ls(), e.rs(), e.dep())) { + TRACE("seq", tout << "length\n";); + return true; + } + } + + unsigned s = 0; for (unsigned i = 0; i < sz; ++i) { unsigned k = (i + start) % sz; @@ -488,6 +498,7 @@ bool theory_seq::check_length_coherence(expr* e) { } bool theory_seq::check_length_coherence() { + obj_hashtable::iterator it = m_length.begin(), end = m_length.end(); for (; it != end; ++it) { expr* e = *it; @@ -822,24 +833,9 @@ bool theory_seq::solve_unit_eq(expr_ref_vector const& l, expr_ref_vector const& return false; } + bool theory_seq::reduce_length(expr* l, expr* r, literal_vector& lits) { - rational val1, val2; - if (has_length(l) && has_length(r) && - get_length(l, val1) && get_length(r, val2) && val1 == val2) { - context& ctx = get_context(); - expr_ref len1(m_util.str.mk_length(l), m); - expr_ref len2(m_util.str.mk_length(r), m); - literal lit = mk_eq(len1, len2, false); - if (ctx.get_assignment(lit) == l_true) { - lits.push_back(lit); - return true; - } - else { - TRACE("seq", tout << "Assignment: " << len1 << " = " << len2 << " " << ctx.get_assignment(lit) << "\n";); - return false; - } - } expr_ref len1(m), len2(m); lits.reset(); if (get_length(l, len1, lits) && @@ -962,10 +958,6 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de TRACE("seq", tout << "unit\n";); return true; } - if (!ctx.inconsistent() && reduce_length_eq(ls, rs, deps)) { - TRACE("seq", tout << "length\n";); - return true; - } if (!ctx.inconsistent() && solve_binary_eq(ls, rs, deps)) { TRACE("seq", tout << "binary\n";); return true; @@ -1027,6 +1019,7 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con lhs.append(ls.size()-1, ls.c_ptr() + 1); rhs.append(rs.size()-1, rs.c_ptr() + 1); SASSERT(!lhs.empty() || !rhs.empty()); + deps = mk_join(deps, lits); m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps)); TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";); propagate_eq(deps, lits, l, r, true); @@ -1039,14 +1032,91 @@ bool theory_seq::reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector con lhs.append(ls.size()-1, ls.c_ptr()); rhs.append(rs.size()-1, rs.c_ptr()); SASSERT(!lhs.empty() || !rhs.empty()); + deps = mk_join(deps, lits); m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps)); TRACE("seq", tout << "Propagate equal lengths " << l << " " << r << "\n";); propagate_eq(deps, lits, l, r, true); return true; } + rational len1, len2, len; + if (ls.size() > 1 && get_length(ls[0], len1) && get_length(rs[0], len2) && len1 >= len2) { + unsigned j = 1; + for (; j < rs.size() && len1 > len2 && get_length(rs[j], len); ++j) { + len2 += len; + } + if (len1 == len2 && 0 < j && j < rs.size() && reduce_length(1, j, true, ls, rs, deps)) { + return true; + } + } + if (rs.size() > 1 && get_length(rs[0], len1) && get_length(ls[0], len2) && len1 > len2) { + unsigned j = 1; + for (; j < ls.size() && len1 > len2 && get_length(ls[j], len); ++j) { + len2 += len; + } + if (len1 == len2 && 0 < j && j < ls.size() && reduce_length(j, 1, true, ls, rs, deps)) { + return true; + } + } + if (ls.size() > 1 && get_length(ls.back(), len1) && get_length(rs.back(), len2) && len1 >= len2) { + unsigned j = rs.size()-1; + for (; j > 0 && len1 > len2 && get_length(rs[j-1], len); --j) { + len2 += len; + } + if (len1 == len2 && 0 < j && j < rs.size() && reduce_length(ls.size()-1, rs.size()-j, false, ls, rs, deps)) { + return true; + } + } + if (rs.size() > 1 && get_length(rs.back(), len1) && get_length(ls.back(), len2) && len1 > len2) { + unsigned j = ls.size()-1; + for (; j > 0 && len1 > len2 && get_length(ls[j-1], len); --j) { + len2 += len; + } + if (len1 == len2 && 0 < j && j < ls.size() && reduce_length(ls.size()-j, rs.size()-1, false, ls, rs, deps)) { + return true; + } + } return false; - } +} + +bool theory_seq::reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps) { + context& ctx = get_context(); + expr* const* ls1 = ls.c_ptr(); + expr* const* ls2 = ls.c_ptr()+i; + expr* const* rs1 = rs.c_ptr(); + expr* const* rs2 = rs.c_ptr()+j; + unsigned l1 = i; + unsigned l2 = ls.size()-i; + unsigned r1 = j; + unsigned r2 = rs.size()-j; + if (!front) { + std::swap(ls1, ls2); + std::swap(rs1, rs2); + std::swap(l1, l2); + std::swap(r1, r2); + } + SASSERT(0 < l1 && l1 < ls.size()); + SASSERT(0 < r1 && r1 < rs.size()); + expr_ref l(m_util.str.mk_concat(l1, ls1), m); + expr_ref r(m_util.str.mk_concat(r1, rs1), m); + expr_ref lenl(m_util.str.mk_length(l), m); + expr_ref lenr(m_util.str.mk_length(r), m); + literal lit = mk_eq(lenl, lenr, false); + if (ctx.get_assignment(lit) == l_true) { + literal_vector lits; + expr_ref_vector lhs(m), rhs(m); + lhs.append(l2, ls2); + rhs.append(r2, rs2); + deps = mk_join(deps, lit); + m_eqs.push_back(eq(m_eq_id++, lhs, rhs, deps)); + propagate_eq(deps, lits, l, r, true); + return true; + } + else { + //TRACE("seq", tout << "Assignment: " << lenl << " = " << lenr << " " << ctx.get_assignment(lit) << "\n";); + return false; + } +} bool theory_seq::solve_binary_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* dep) { context& ctx = get_context(); @@ -1191,9 +1261,6 @@ bool theory_seq::get_length(expr* e, expr_ref& len, literal_vector& lits) { len = m_autil.mk_int(1); return true; } - else { - TRACE("seq", tout << "unhandled: " << mk_pp(e, m) << "\n";); - } return false; } @@ -2314,7 +2381,10 @@ bool theory_seq::get_length(expr* e, rational& val) { else if (m_util.str.is_string(c, s)) { val += rational(s.length()); } - else { + else if (!has_length(c)) { + return false; + } + else { len = m_util.str.mk_length(c); if (ctx.e_internalized(len) && tha->get_value(ctx.get_enode(len), len_val) && @@ -2322,7 +2392,6 @@ bool theory_seq::get_length(expr* e, rational& val) { val += val1; } else { - TRACE("seq", tout << "No length provided for " << len << "\n";); return false; } } @@ -2595,8 +2664,7 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter } -expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, - expr* e2, expr* e3, sort* range) { +expr_ref theory_seq::mk_skolem(symbol const& name, expr* e1, expr* e2, expr* e3, sort* range) { expr* es[3] = { e1, e2, e3 }; unsigned len = e3?3:(e2?2:1); if (!range) { @@ -2609,6 +2677,17 @@ bool theory_seq::is_skolem(symbol const& s, expr* e) const { return m_util.is_skolem(e) && to_app(e)->get_decl()->get_parameter(0).get_symbol() == s; } +theory_seq::dependency* theory_seq::mk_join(dependency* deps, literal lit) { + return m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); +} + +theory_seq::dependency* theory_seq::mk_join(dependency* deps, literal_vector const& lits) { + for (unsigned i = 0; i < lits.size(); ++i) { + deps = mk_join(deps, lits[i]); + } + return deps; +} + void theory_seq::propagate_eq(literal lit, expr* e1, expr* e2, bool add_to_eqs) { literal_vector lits; lits.push_back(lit); @@ -2631,11 +2710,7 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp linearize(deps, eqs, lits); if (add_to_eqs) { - for (unsigned i = 0; i < _lits.size(); ++i) { - literal lit = _lits[i]; - SASSERT(l_true == ctx.get_assignment(lit)); - deps = m_dm.mk_join(deps, m_dm.mk_leaf(assumption(lit))); - } + deps = mk_join(deps, _lits); new_eq_eh(deps, n1, n2); } TRACE("seq", diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h index f0445aada..a28458e02 100644 --- a/src/smt/theory_seq.h +++ b/src/smt/theory_seq.h @@ -337,6 +337,7 @@ namespace smt { bool get_length(expr* s, expr_ref& len, literal_vector& lits); bool reduce_length(expr* l, expr* r, literal_vector& lits); bool reduce_length_eq(expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps); + bool reduce_length(unsigned i, unsigned j, bool front, expr_ref_vector const& ls, expr_ref_vector const& rs, dependency* deps); expr_ref mk_empty(sort* s) { return expr_ref(m_util.str.mk_empty(s), m); } expr_ref mk_concat(unsigned n, expr*const* es) { return expr_ref(m_util.str.mk_concat(n, es), m); } @@ -429,6 +430,10 @@ namespace smt { void tightest_prefix(expr* s, expr* x, literal lit, literal lit2 = null_literal); expr_ref mk_sub(expr* a, expr* b); enode* ensure_enode(expr* a); + + dependency* mk_join(dependency* deps, literal lit); + dependency* mk_join(dependency* deps, literal_vector const& lits); + // arithmetic integration bool lower_bound(expr* s, rational& lo); From 564343c39cb37359eff7fd848f78ae652dace20b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Tue, 9 Feb 2016 15:30:05 +0000 Subject: [PATCH 4/5] remove unused methods in ast.cpp --- src/ast/ast.h | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/ast/ast.h b/src/ast/ast.h index 0dba6039c..861fb997d 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -634,9 +634,6 @@ struct app_flags { unsigned m_ground:1; // application does not have free variables or nested quantifiers. unsigned m_has_quantifiers:1; // application has nested quantifiers. unsigned m_has_labels:1; // application has nested labels. - static app_flags mk_const_flags(); - static app_flags mk_default_app_flags(); - static app_flags mk_default_quantifier_flags(); }; class app : public expr { From 3df9fea54c92a2c74fba64f629836a1f486ade38 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Tue, 9 Feb 2016 16:38:35 +0000 Subject: [PATCH 5/5] removed unused variables --- src/api/api_fpa.cpp | 2 -- 1 file changed, 2 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 33c1448e7..37197e730 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -935,7 +935,6 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); - unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); unsynch_mpq_manager & mpqm = mpfm.mpq_manager(); family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(fid); @@ -1037,7 +1036,6 @@ extern "C" { RESET_ERROR_CODE(); ast_manager & m = mk_c(c)->m(); mpf_manager & mpfm = mk_c(c)->fpautil().fm(); - unsynch_mpz_manager & mpzm = mpfm.mpz_manager(); family_id fid = mk_c(c)->get_fpa_fid(); fpa_decl_plugin * plugin = (fpa_decl_plugin*)m.get_plugin(mk_c(c)->get_fpa_fid()); SASSERT(plugin != 0);