From 37b11cdc7479c5316c38b9ee468341e1f72d9782 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 7 Feb 2016 15:01:09 +0000 Subject: [PATCH 1/5] Comments, whitespace. --- src/ast/seq_decl_plugin.cpp | 68 +++++++++--------- src/ast/seq_decl_plugin.h | 74 ++++++++++---------- src/ast/simplifier/seq_simplifier_plugin.cpp | 4 +- 3 files changed, 73 insertions(+), 73 deletions(-) diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index f3e696879..05edb35c8 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -3,11 +3,11 @@ Copyright (c) 2011 Microsoft Corporation Module Name: - dl_decl_plugin.h + seq_decl_plugin.h Abstract: - + decl_plugin for the theory of sequences Author: @@ -43,7 +43,7 @@ static bool is_escape_char(char const *& s, unsigned& result) { if (*s != '\\' || *(s + 1) == 0) { return false; } - if (*(s + 1) == 'x' && + if (*(s + 1) == 'x' && is_hex_digit(*(s + 2), d1) && is_hex_digit(*(s + 3), d2)) { result = d1*16 + d2; s += 4; @@ -100,7 +100,7 @@ zstring::zstring(char const* s, encoding enc): m_encoding(enc) { if (is_escape_char(s, ch)) { m_buffer.push_back(ch); } - else { + else { m_buffer.push_back(*s); ++s; } @@ -115,7 +115,7 @@ zstring::zstring(zstring const& other) { zstring::zstring(unsigned num_bits, bool const* ch) { SASSERT(num_bits == 8 || num_bits == 16); m_encoding = (num_bits == 8)?ascii:unicode; - unsigned n = 0; + unsigned n = 0; for (unsigned i = 0; i < num_bits; ++i) { n |= (((unsigned)ch[i]) << i); } @@ -161,10 +161,10 @@ zstring zstring::replace(zstring const& src, zstring const& dst) const { } static const char esc_table[32][6] = - { "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n", "\\v", "\\f", "\\r", "\\x0E", "\\x0F", + { "\\x00", "\\x01", "\\x02", "\\x03", "\\x04", "\\x05", "\\x06", "\\x07", "\\x08", "\\x09", "\\n", "\\v", "\\f", "\\r", "\\x0E", "\\x0F", "\\x10", "\\x11", "\\x12", "\\x13", "\\x14", "\\x15", "\\x16", "\\x17", "\\x18", "\\x19", "\\x1A", "\\x1B", "\\x1C", "\\x1D", "\\x1E", "\\x1F" }; - + std::string zstring::encode() const { SASSERT(m_encoding == ascii); std::ostringstream strm; @@ -223,7 +223,7 @@ int zstring::indexof(zstring const& other, int offset) const { bool prefix = true; for (unsigned j = 0; prefix && j < other.length(); ++j) { prefix = m_buffer[i + j] == other[j]; - } + } if (prefix) { return static_cast(i); } @@ -253,7 +253,7 @@ std::ostream& zstring::operator<<(std::ostream& out) const { } -seq_decl_plugin::seq_decl_plugin(): m_init(false), +seq_decl_plugin::seq_decl_plugin(): m_init(false), m_stringc_sym("String"), m_charc_sym("Char"), m_string(0), @@ -261,7 +261,7 @@ seq_decl_plugin::seq_decl_plugin(): m_init(false), m_re(0) {} void seq_decl_plugin::finalize() { - for (unsigned i = 0; i < m_sigs.size(); ++i) + for (unsigned i = 0; i < m_sigs.size(); ++i) dealloc(m_sigs[i]); m_manager->dec_ref(m_string); m_manager->dec_ref(m_char); @@ -269,7 +269,7 @@ void seq_decl_plugin::finalize() { } bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) { - return + return s->get_name().is_numerical() && (idx = s->get_name().get_num(), true); } @@ -286,7 +286,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { return true; } - + if (s->get_family_id() == sP->get_family_id() && s->get_decl_kind() == sP->get_decl_kind() && s->get_num_parameters() == sP->get_num_parameters()) { @@ -311,7 +311,7 @@ bool seq_decl_plugin::match(ptr_vector& binding, sort* s, sort* sP) { void seq_decl_plugin::match_right_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) { ptr_vector binding; ast_manager& m = *m_manager; - TRACE("seq_verbose", + TRACE("seq_verbose", tout << sig.m_name << ": "; for (unsigned i = 0; i < dsz; ++i) tout << mk_pp(dom[i], m) << " "; if (range) tout << " range: " << mk_pp(range, m); @@ -378,7 +378,7 @@ void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* ran for (unsigned i = 0; i < dsz; ++i) { strm << mk_pp(sig.m_dom[i].get(), m) << " "; } - + m.raise_exception(strm.str().c_str()); } if (!range && dsz == 0) { @@ -441,7 +441,7 @@ void seq_decl_plugin::init() { m_sigs.resize(LAST_SEQ_OP); // TBD: have (par ..) construct and load parameterized signature from premable. m_sigs[OP_SEQ_UNIT] = alloc(psig, m, "seq.unit", 1, 1, &A, seqA); - m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA); + m_sigs[OP_SEQ_EMPTY] = alloc(psig, m, "seq.empty", 1, 0, 0, seqA); m_sigs[OP_SEQ_CONCAT] = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA); m_sigs[OP_SEQ_PREFIX] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT); m_sigs[OP_SEQ_SUFFIX] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT); @@ -551,10 +551,10 @@ func_decl* seq_decl_plugin::mk_assoc_fun(decl_kind k, unsigned arity, sort* cons match_right_assoc(*m_sigs[k], arity, domain, range, rng); func_decl_info info(m_family_id, k_seq); info.set_right_associative(); - return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info); + return m.mk_func_decl(m_sigs[(rng == m_string)?k_string:k_seq]->m_name, rng, rng, rng, info); } -func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, +func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range) { init(); ast_manager& m = *m_manager; @@ -571,7 +571,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, func_decl_info info(m_family_id, k, 1, ¶m); return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, info); } - + case OP_SEQ_UNIT: case OP_RE_PLUS: case OP_RE_STAR: @@ -596,7 +596,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, } match(*m_sigs[k], arity, domain, range, rng); return m.mk_func_decl(symbol("re.nostr"), arity, domain, rng, func_decl_info(m_family_id, OP_RE_EMPTY_SET)); - + case OP_RE_LOOP: switch (arity) { case 1: @@ -604,7 +604,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, if (num_parameters == 0 || num_parameters > 2 || !parameters[0].is_int() || (num_parameters == 2 && !parameters[1].is_int())) { m.raise_exception("Expecting two numeral parameters to function re-loop"); } - return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); + return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters)); case 2: if (m_re != domain[0] || !arith_util(m).is_int(domain[1])) { m.raise_exception("Incorrect type of arguments passed to re.loop. Expecting regular expression and two integer parameters"); @@ -616,26 +616,26 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, } return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, domain[0], func_decl_info(m_family_id, k, num_parameters, parameters)); default: - m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); + m.raise_exception("Incorrect number of arguments passed to loop. Expected 1 regular expression and two integer parameters"); } - + case OP_STRING_CONST: if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) { m.raise_exception("invalid string declaration"); - } + } return m.mk_const_decl(m_stringc_sym, m_string, func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters)); - + case OP_RE_UNION: - case OP_RE_CONCAT: - case OP_RE_INTERSECT: + case OP_RE_CONCAT: + case OP_RE_INTERSECT: return mk_assoc_fun(k, arity, domain, range, k, k); - case OP_SEQ_CONCAT: + case OP_SEQ_CONCAT: return mk_assoc_fun(k, arity, domain, range, k, _OP_STRING_CONCAT); - case _OP_STRING_CONCAT: + case _OP_STRING_CONCAT: return mk_assoc_fun(k, arity, domain, range, OP_SEQ_CONCAT, k); case OP_SEQ_REPLACE: @@ -746,8 +746,8 @@ app* seq_decl_plugin::mk_string(zstring const& s) { bool seq_decl_plugin::is_value(app* e) const { - return - is_app_of(e, m_family_id, OP_SEQ_EMPTY) || + return + is_app_of(e, m_family_id, OP_SEQ_EMPTY) || (is_app_of(e, m_family_id, OP_SEQ_UNIT) && m_manager->is_value(e->get_arg(0))); } @@ -785,7 +785,7 @@ app* seq_util::str::mk_char(char ch) { zstring s(ch, zstring::ascii); return mk_char(s, 0); } - + bool seq_util::str::is_char(expr* n, zstring& c) const { if (u.is_char(n)) { c = zstring(to_app(n)->get_decl()->get_parameter(0).get_symbol().bare_str()); @@ -812,7 +812,7 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const { while (is_concat(e, e1, e2)) { get_concat(e1, es); e = e2; - } + } if (!is_empty(e)) { es.push_back(e); } @@ -838,7 +838,7 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& h return true; } } - return false; + return false; } bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) { @@ -850,5 +850,5 @@ bool seq_util::re::is_loop(expr const* n, expr*& body, unsigned& lo) { return true; } } - return false; + return false; } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index a83878b0e..4739af84b 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -7,7 +7,7 @@ Module Name: Abstract: - + decl_plugin for the theory of sequences Author: @@ -41,7 +41,7 @@ enum seq_op_kind { OP_SEQ_EXTRACT, OP_SEQ_REPLACE, OP_SEQ_AT, - OP_SEQ_LENGTH, + OP_SEQ_LENGTH, OP_SEQ_INDEX, OP_SEQ_TO_RE, OP_SEQ_IN_RE, @@ -61,19 +61,19 @@ enum seq_op_kind { // string specific operators. OP_STRING_CONST, - OP_STRING_ITOS, - OP_STRING_STOI, + OP_STRING_ITOS, + OP_STRING_STOI, // internal only operators. Converted to SEQ variants. - _OP_STRING_STRREPL, - _OP_STRING_CONCAT, - _OP_STRING_LENGTH, + _OP_STRING_STRREPL, + _OP_STRING_CONCAT, + _OP_STRING_LENGTH, _OP_STRING_STRCTN, - _OP_STRING_PREFIX, - _OP_STRING_SUFFIX, - _OP_STRING_IN_REGEXP, - _OP_STRING_TO_REGEXP, - _OP_STRING_CHARAT, - _OP_STRING_SUBSTR, + _OP_STRING_PREFIX, + _OP_STRING_SUFFIX, + _OP_STRING_IN_REGEXP, + _OP_STRING_TO_REGEXP, + _OP_STRING_CHARAT, + _OP_STRING_SUBSTR, _OP_STRING_STRIDOF, _OP_REGEXP_EMPTY, _OP_REGEXP_FULL, @@ -85,10 +85,10 @@ enum seq_op_kind { class zstring { public: enum encoding { - ascii, + ascii, unicode }; -private: +private: buffer m_buffer; encoding m_encoding; public: @@ -101,7 +101,7 @@ public: zstring replace(zstring const& src, zstring const& dst) const; unsigned num_bits() const { return (m_encoding==ascii)?8:16; } encoding get_encoding() const { return m_encoding; } - std::string encode() const; + std::string encode() const; unsigned length() const { return m_buffer.size(); } unsigned operator[](unsigned i) const { return m_buffer[i]; } bool empty() const { return m_buffer.empty(); } @@ -113,7 +113,7 @@ public: zstring operator+(zstring const& other) const; std::ostream& operator<<(std::ostream& out) const; }; - + class seq_decl_plugin : public decl_plugin { struct psig { symbol m_name; @@ -161,18 +161,18 @@ public: virtual ~seq_decl_plugin() {} virtual void finalize(); - + virtual decl_plugin * mk_fresh() { return alloc(seq_decl_plugin); } - + virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters); - - virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, + + virtual func_decl * mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, unsigned arity, sort * const * domain, sort * range); - + virtual void get_op_names(svector & op_names, symbol const & logic); - + virtual void get_sort_names(svector & sort_names, symbol const & logic); - + virtual bool is_value(app * e) const; virtual bool is_unique_value(app * e) const { return is_value(e); } @@ -181,8 +181,8 @@ public: bool is_char(ast* a) const { return a == m_char; } - app* mk_string(symbol const& s); - app* mk_string(zstring const& s); + app* mk_string(symbol const& s); + app* mk_string(zstring const& s); }; @@ -244,12 +244,12 @@ public: bool is_string(expr const* n, symbol& s) const { return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true); } - + bool is_string(expr const* n, zstring& s) const; bool is_char(expr* n, zstring& s) const; - bool is_empty(expr const* n) const { symbol s; - return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); + bool is_empty(expr const* n) const { symbol s; + return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && *s.bare_str() == 0); } bool is_concat(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); } bool is_length(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); } @@ -265,7 +265,7 @@ public: bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); } bool is_unit(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_UNIT); } - + MATCH_BINARY(is_concat); MATCH_UNARY(is_length); MATCH_TERNARY(is_extract); @@ -278,7 +278,7 @@ public: MATCH_BINARY(is_suffix); MATCH_UNARY(is_itos); MATCH_UNARY(is_stoi); - MATCH_BINARY(is_in_re); + MATCH_BINARY(is_in_re); MATCH_UNARY(is_unit); void get_concat(expr* e, expr_ref_vector& es) const; @@ -301,7 +301,7 @@ public: app* mk_inter(expr* r1, expr* r2) { return m.mk_app(m_fid, OP_RE_INTERSECT, r1, r2); } app* mk_star(expr* r) { return m.mk_app(m_fid, OP_RE_STAR, r); } app* mk_plus(expr* r) { return m.mk_app(m_fid, OP_RE_PLUS, r); } - app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); } + app* mk_opt(expr* r) { return m.mk_app(m_fid, OP_RE_OPTION, r); } app* mk_loop(expr* r, unsigned lo); app* mk_loop(expr* r, unsigned lo, unsigned hi); @@ -325,23 +325,23 @@ public: MATCH_UNARY(is_plus); MATCH_UNARY(is_opt); bool is_loop(expr const* n, expr*& body, unsigned& lo, unsigned& hi); - bool is_loop(expr const* n, expr*& body, unsigned& lo); + bool is_loop(expr const* n, expr*& body, unsigned& lo); }; str str; re re; - seq_util(ast_manager& m): - m(m), + seq_util(ast_manager& m): + m(m), seq(*static_cast(m.get_plugin(m.mk_family_id("seq")))), m_fid(seq.get_family_id()), str(*this), - re(*this) { + re(*this) { } ~seq_util() {} family_id get_family_id() const { return m_fid; } - + }; #endif /* SEQ_DECL_PLUGIN_H_ */ diff --git a/src/ast/simplifier/seq_simplifier_plugin.cpp b/src/ast/simplifier/seq_simplifier_plugin.cpp index e31d6812c..0b7bddf0a 100644 --- a/src/ast/simplifier/seq_simplifier_plugin.cpp +++ b/src/ast/simplifier/seq_simplifier_plugin.cpp @@ -7,7 +7,7 @@ Module Name: Abstract: - Simplifier for the floating-point theory + Simplifier for the theory of sequences Author: @@ -24,7 +24,7 @@ m_rw(m) {} seq_simplifier_plugin::~seq_simplifier_plugin() {} bool seq_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); + set_reduce_invoked(); SASSERT(f->get_family_id() == get_family_id()); From e9d94e53f65931e8024c1642d5ea6d24a87dc3ad Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 7 Feb 2016 15:01:22 +0000 Subject: [PATCH 2/5] Improved FPA simplifier plugin --- src/ast/simplifier/fpa_simplifier_plugin.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/ast/simplifier/fpa_simplifier_plugin.cpp b/src/ast/simplifier/fpa_simplifier_plugin.cpp index 4aba9c76c..5775f1af0 100644 --- a/src/ast/simplifier/fpa_simplifier_plugin.cpp +++ b/src/ast/simplifier/fpa_simplifier_plugin.cpp @@ -24,16 +24,16 @@ m_rw(m) {} fpa_simplifier_plugin::~fpa_simplifier_plugin() {} bool fpa_simplifier_plugin::reduce(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) { - set_reduce_invoked(); + set_reduce_invoked(); SASSERT(f->get_family_id() == get_family_id()); - return m_rw.mk_app_core(f, num_args, args, result) == BR_DONE; + return m_rw.mk_app_core(f, num_args, args, result) != BR_FAILED; } bool fpa_simplifier_plugin::reduce_eq(expr * lhs, expr * rhs, expr_ref & result) { set_reduce_invoked(); - return m_rw.mk_eq_core(lhs, rhs, result) == BR_DONE; + return m_rw.mk_eq_core(lhs, rhs, result) != BR_FAILED; } From 92b6a3e1348484c8354365380e8ece24f870b929 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Sun, 7 Feb 2016 17:33:33 +0000 Subject: [PATCH 3/5] Fixed exponent cap for fp.add in fpa2bv_converter (was unsound for combinations of many sbits but few ebits). Fixes #439. --- src/ast/fpa/fpa2bv_converter.cpp | 15 ++++++++++----- 1 file changed, 10 insertions(+), 5 deletions(-) diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 1d66b793d..40bb7efe8 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -419,11 +419,16 @@ void fpa2bv_converter::add_core(unsigned sbits, unsigned ebits, dbg_decouple("fpa2bv_add_exp_delta", exp_delta); - // cap the delta - expr_ref cap(m), cap_le_delta(m); - cap = m_bv_util.mk_numeral(sbits+2, ebits); - cap_le_delta = m_bv_util.mk_ule(cap, exp_delta); - m_simp.mk_ite(cap_le_delta, cap, exp_delta, exp_delta); + if (log2(sbits + 2) < ebits + 2) + { + // cap the delta + expr_ref cap(m), cap_le_delta(m); + cap = m_bv_util.mk_numeral(sbits + 2, ebits + 2); + cap_le_delta = m_bv_util.mk_ule(cap, m_bv_util.mk_zero_extend(2, exp_delta)); + m_simp.mk_ite(cap_le_delta, cap, m_bv_util.mk_zero_extend(2, exp_delta), exp_delta); + exp_delta = m_bv_util.mk_extract(ebits - 1, 0, exp_delta); + dbg_decouple("fpa2bv_add_exp_cap", cap); + } dbg_decouple("fpa2bv_add_exp_delta_capped", exp_delta); From 7e2783c6a2be38ffbf3d72de5dafaaa6972d2e2a Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Mon, 8 Feb 2016 15:25:53 +0000 Subject: [PATCH 4/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 5/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);