From eb6d39ba46a712ecc3dcfd6eb810c75e34094528 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 27 Feb 2014 11:49:25 -0800 Subject: [PATCH] fix memory smash Signed-off-by: Nikolaj Bjorner --- src/math/simplex/simplex.h | 5 +++-- src/math/simplex/simplex_def.h | 5 ++++- src/math/simplex/sparse_matrix.h | 4 ++-- src/opt/opt_solver.cpp | 12 +++++++++++- src/opt/weighted_maxsat.cpp | 4 ++++ src/smt/theory_pb.cpp | 6 +++--- 6 files changed, 27 insertions(+), 9 deletions(-) diff --git a/src/math/simplex/simplex.h b/src/math/simplex/simplex.h index 1370d4bae..26d471246 100644 --- a/src/math/simplex/simplex.h +++ b/src/math/simplex/simplex.h @@ -92,12 +92,12 @@ namespace simplex { }; static const var_t null_var = UINT_MAX; + mutable manager m; + mutable eps_manager em; mutable matrix M; unsigned m_max_iterations; volatile bool m_cancel; var_heap m_to_patch; - mutable manager m; - mutable eps_manager em; vector m_vars; svector m_row2base; bool m_bland; @@ -110,6 +110,7 @@ namespace simplex { public: simplex(): + M(m), m_max_iterations(UINT_MAX), m_cancel(false), m_to_patch(1024), diff --git a/src/math/simplex/simplex_def.h b/src/math/simplex/simplex_def.h index fa6cdf234..93b061dda 100644 --- a/src/math/simplex/simplex_def.h +++ b/src/math/simplex/simplex_def.h @@ -244,7 +244,10 @@ namespace simplex { void simplex::ensure_var(var_t v) { while (v >= m_vars.size()) { M.ensure_var(m_vars.size()); - m_vars.push_back(var_info()); + m_vars.push_back(var_info()); + } + if (m_to_patch.get_bounds() <= v) { + m_to_patch.set_bounds(2*v+1); } } diff --git a/src/math/simplex/sparse_matrix.h b/src/math/simplex/sparse_matrix.h index e4cb33f07..b0b77d4dc 100644 --- a/src/math/simplex/sparse_matrix.h +++ b/src/math/simplex/sparse_matrix.h @@ -129,7 +129,7 @@ namespace simplex { void del_col_entry(unsigned idx); }; - manager m; + manager& m; vector<_row> m_rows; svector m_dead_rows; // rows to recycle vector m_columns; // per var @@ -143,7 +143,7 @@ namespace simplex { public: - sparse_matrix() {} + sparse_matrix(manager& m): m(m) {} ~sparse_matrix(); class row { diff --git a/src/opt/opt_solver.cpp b/src/opt/opt_solver.cpp index 5443b6872..699a7898c 100644 --- a/src/opt/opt_solver.cpp +++ b/src/opt/opt_solver.cpp @@ -29,6 +29,7 @@ Notes: #include "pp_params.hpp" #include "opt_params.hpp" #include "model_smt2_pp.h" +#include "stopwatch.h" namespace opt { @@ -113,14 +114,23 @@ namespace opt { tout << mk_pp(m_context.get_formulas()[i], m_context.m()) << "\n"; } }); + stopwatch w; if (dump_benchmarks()) { + w.start(); std::stringstream file_name; file_name << "opt_solver" << ++m_dump_count << ".smt2"; std::ofstream buffer(file_name.str().c_str()); to_smt2_benchmark(buffer, num_assumptions, assumptions, "opt_solver", ""); buffer.close(); + IF_VERBOSE(1, verbose_stream() << "(created benchmark: " << file_name.str() << "..."; + verbose_stream().flush();); } - return m_context.check(num_assumptions, assumptions); + lbool r = m_context.check(num_assumptions, assumptions); + if (dump_benchmarks()) { + w.stop(); + IF_VERBOSE(1, verbose_stream() << ".. " << r << " " << std::fixed << w.get_seconds() << ")\n";); + } + return r; } void opt_solver::maximize_objectives() { diff --git a/src/opt/weighted_maxsat.cpp b/src/opt/weighted_maxsat.cpp index b5f31e6b5..dcf9313b5 100644 --- a/src/opt/weighted_maxsat.cpp +++ b/src/opt/weighted_maxsat.cpp @@ -518,6 +518,7 @@ namespace opt { }; lbool incremental_solve() { + IF_VERBOSE(3, verbose_stream() << "(incremental solve)\n";); TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); solver::scoped_push _s(s); @@ -541,6 +542,7 @@ namespace opt { s.assert_expr(fml); was_sat = true; } + IF_VERBOSE(3, verbose_stream() << "(incremental bound)\n";); } if (was_sat) { wth().get_assignment(m_assignment); @@ -605,6 +607,7 @@ namespace opt { } lbool conditional_solve(expr* cond) { + IF_VERBOSE(3, verbose_stream() << "(conditional solve)\n";); smt::theory_weighted_maxsat& wth = *get_theory(); bool was_sat = false; lbool is_sat = l_true; @@ -1169,6 +1172,7 @@ namespace opt { // cost becomes 0 lbool bisection_solve() { + IF_VERBOSE(3, verbose_stream() << "(bisection solve)\n";); TRACE("opt", tout << "weighted maxsat\n";); scoped_ensure_theory wth(*this); solver::scoped_push _s(s); diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp index 191481ae4..176fb66a4 100644 --- a/src/smt/theory_pb.cpp +++ b/src/smt/theory_pb.cpp @@ -476,7 +476,7 @@ namespace smt { ctx.mk_th_axiom(get_id(), lit, ~c->lit(i)); } ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr()); - return true; + // return true; } // maximal coefficient: @@ -490,7 +490,7 @@ namespace smt { } // pre-compile threshold for cardinality - bool enable_compile = m_enable_compilation && c->is_ge(); + bool enable_compile = m_enable_compilation && c->is_ge() && !c->k().is_one(); for (unsigned i = 0; enable_compile && i < args.size(); ++i) { enable_compile = (args[i].second <= m_max_compiled_coeff); } @@ -504,7 +504,7 @@ namespace smt { c->m_compilation_threshold = th; IF_VERBOSE(2, verbose_stream() << "(smt.pb setting compilation threhshold to " << th << ")\n";); TRACE("pb", tout << "compilation threshold: " << th << "\n";); - } + } else { c->m_compilation_threshold = UINT_MAX; }