fix memory smash

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>

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<var_info>            m_vars;
         svector<var_t>              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),

src/math/simplex/simplex_def.h

@@ -244,7 +244,10 @@ namespace simplex {
     void simplex<Ext>::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);
         }
     }
 

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<unsigned>       m_dead_rows;        // rows to recycle
         vector<column>          m_columns;          // per var
@@ -143,7 +143,7 @@ namespace simplex {
 
     public:
 
-        sparse_matrix() {}
+        sparse_matrix(manager& m): m(m) {}
         ~sparse_matrix();
         
         class row {

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() {

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);

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;
         }