From 11997afb5d1c0dd816bcd43dfa8298031e4ee743 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 19 Oct 2016 12:00:34 +0100 Subject: [PATCH 1/4] Fixed potential problems with invalidated iterators. --- src/smt/theory_arith_nl.h | 18 ++++++------------ 1 file changed, 6 insertions(+), 12 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index 04b974d6e..df9a71aaa 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -589,10 +589,8 @@ namespace smt { m_dep_manager.reset(); bool propagated = false; context & ctx = get_context(); - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned i = 0; i < m_nl_monomials.size(); i++) { + theory_var v = m_nl_monomials.size(); expr * m = var2expr(v); if (!ctx.is_relevant(m)) continue; @@ -706,10 +704,8 @@ namespace smt { bool bounded = false; unsigned n = 0; numeral range; - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned i = 0; i < m_nl_monomials.size(); i++) { + theory_var v = m_nl_monomials.size(); if (is_real(v)) continue; bool computed_epsilon = false; @@ -2340,10 +2336,8 @@ namespace smt { bool theory_arith::max_min_nl_vars() { var_set already_found; svector vars; - svector::const_iterator it = m_nl_monomials.begin(); - svector::const_iterator end = m_nl_monomials.end(); - for (; it != end; ++it) { - theory_var v = *it; + for (unsigned i = 0; i < m_nl_monomials.size(); i++) { + theory_var v = m_nl_monomials.size(); mark_var(v, vars, already_found); expr * n = var2expr(v); SASSERT(is_pure_monomial(n)); From 948bf9540f92a32da1450360a0e33e10dabbd7d2 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 19 Oct 2016 12:07:33 +0100 Subject: [PATCH 2/4] Fix for previous commit. --- src/smt/theory_arith_nl.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/smt/theory_arith_nl.h b/src/smt/theory_arith_nl.h index df9a71aaa..d47ecaa4e 100644 --- a/src/smt/theory_arith_nl.h +++ b/src/smt/theory_arith_nl.h @@ -590,7 +590,7 @@ namespace smt { bool propagated = false; context & ctx = get_context(); for (unsigned i = 0; i < m_nl_monomials.size(); i++) { - theory_var v = m_nl_monomials.size(); + theory_var v = m_nl_monomials[i]; expr * m = var2expr(v); if (!ctx.is_relevant(m)) continue; @@ -705,7 +705,7 @@ namespace smt { unsigned n = 0; numeral range; for (unsigned i = 0; i < m_nl_monomials.size(); i++) { - theory_var v = m_nl_monomials.size(); + theory_var v = m_nl_monomials[i]; if (is_real(v)) continue; bool computed_epsilon = false; @@ -2337,7 +2337,7 @@ namespace smt { var_set already_found; svector vars; for (unsigned i = 0; i < m_nl_monomials.size(); i++) { - theory_var v = m_nl_monomials.size(); + theory_var v = m_nl_monomials[i]; mark_var(v, vars, already_found); expr * n = var2expr(v); SASSERT(is_pure_monomial(n)); From f9bd8f674dd9d1783cee13c96d8caecbd0d72a55 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 19 Oct 2016 12:31:06 +0100 Subject: [PATCH 3/4] whitespace --- src/sat/sat_types.h | 66 ++++++++++++++++++++++----------------------- 1 file changed, 33 insertions(+), 33 deletions(-) diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 93109a74f..8e3460179 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -40,9 +40,9 @@ namespace sat { typedef unsigned bool_var; typedef svector bool_var_vector; - + const bool_var null_bool_var = UINT_MAX >> 1; - + /** \brief The literal b is represented by the value 2*b, and the literal (not b) by the value 2*b + 1 @@ -54,33 +54,33 @@ namespace sat { literal():m_val(null_bool_var << 1) { SASSERT(var() == null_bool_var && !sign()); } - + literal(bool_var v, bool _sign): m_val((v << 1) + static_cast(_sign)) { SASSERT(var() == v); SASSERT(sign() == _sign); } - - bool_var var() const { - return m_val >> 1; + + bool_var var() const { + return m_val >> 1; } - + bool sign() const { - return m_val & 1; + return m_val & 1; } literal unsign() const { return literal(m_val & ~1); } - + unsigned index() const { return m_val; } - + void neg() { m_val = m_val ^ 1; } - + friend literal operator~(literal l) { return literal(l.m_val ^ 1); } @@ -116,7 +116,7 @@ namespace sat { typedef approx_set_tpl literal_approx_set; typedef approx_set_tpl var_approx_set; - + enum phase { POS_PHASE, NEG_PHASE, PHASE_NOT_AVAILABLE }; @@ -128,7 +128,7 @@ namespace sat { typedef ptr_vector clause_vector; class solver_exception : public default_exception { - public: + public: solver_exception(char const * msg):default_exception(msg) {} }; @@ -138,7 +138,7 @@ namespace sat { inline lbool value_at(bool_var v, model const & m) { return m[v]; } inline lbool value_at(literal l, model const & m) { lbool r = value_at(l.var(), m); return l.sign() ? ~r : r; } - + inline std::ostream & operator<<(std::ostream & out, model const & m) { bool first = true; for (bool_var v = 0; v < m.size(); v++) { @@ -154,12 +154,12 @@ namespace sat { svector m_set; public: typedef svector::const_iterator iterator; - void insert(unsigned v) { + void insert(unsigned v) { m_in_set.reserve(v+1, false); - if (m_in_set[v]) - return; - m_in_set[v] = true; - m_set.push_back(v); + if (m_in_set[v]) + return; + m_in_set[v] = true; + m_set.push_back(v); } void remove(unsigned v) { @@ -178,22 +178,22 @@ namespace sat { m_set = other.m_set; return *this; } - - bool contains(unsigned v) const { - return v < m_in_set.size() && m_in_set[v] != 0; + + bool contains(unsigned v) const { + return v < m_in_set.size() && m_in_set[v] != 0; } - - bool empty() const { - return m_set.empty(); + + bool empty() const { + return m_set.empty(); } // erase some variable from the set - unsigned erase() { - SASSERT(!empty()); - unsigned v = m_set.back(); - m_set.pop_back(); - m_in_set[v] = false; - return v; + unsigned erase() { + SASSERT(!empty()); + unsigned v = m_set.back(); + m_set.pop_back(); + m_in_set[v] = false; + return v; } unsigned size() const { return m_set.size(); } iterator begin() const { return m_set.begin(); } @@ -280,10 +280,10 @@ namespace sat { return *this; } }; - + struct mem_stat { }; - + inline std::ostream & operator<<(std::ostream & out, mem_stat const & m) { double mem = static_cast(memory::get_allocation_size())/static_cast(1024*1024); out << " :memory " << std::fixed << std::setprecision(2) << mem; From f97ffce479e3283e59f5352d001e9ab4cd1dafc9 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 19 Oct 2016 12:31:35 +0100 Subject: [PATCH 4/4] Silenced GCC warning about empty loop body. --- src/sat/sat_types.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/sat/sat_types.h b/src/sat/sat_types.h index 8e3460179..00edaa593 100644 --- a/src/sat/sat_types.h +++ b/src/sat/sat_types.h @@ -166,7 +166,8 @@ namespace sat { if (contains(v)) { m_in_set[v] = false; unsigned i = 0; - for (i = 0; i < m_set.size() && m_set[i] != v; ++i); + for (i = 0; i < m_set.size() && m_set[i] != v; ++i) + ; SASSERT(i < m_set.size()); m_set[i] = m_set.back(); m_set.pop_back();