From 352f4b5b37fe0c88f1e2803fbfeec9dc1e9b9182 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 26 Mar 2020 18:11:32 -0700 Subject: [PATCH] use u_set in random_update() Signed-off-by: Lev Nachmanson --- src/math/lp/random_updater.h | 8 ++++---- src/math/lp/random_updater_def.h | 1 + 2 files changed, 5 insertions(+), 4 deletions(-) diff --git a/src/math/lp/random_updater.h b/src/math/lp/random_updater.h index fbf4ced1d..4805cf937 100644 --- a/src/math/lp/random_updater.h +++ b/src/math/lp/random_updater.h @@ -25,17 +25,17 @@ Revision History: #include #include #include "math/lp/lp_settings.h" +#include "math/lp/u_set.h" // see http://research.microsoft.com/projects/z3/smt07.pdf // The class searches for a feasible solution with as many different values of variables as it can find namespace lp { template struct numeric_pair; // forward definition class lar_solver; // forward definition class random_updater { - std::set m_var_set; - lar_solver & m_lar_solver; - unsigned m_range; + u_set m_var_set; + lar_solver & m_lar_solver; + unsigned m_range; void add_column_to_sets(unsigned j); - bool random_shift_var(unsigned j); std::unordered_map, unsigned> m_values; // it maps a value to the number of time it occurs bool shift_var(unsigned j); void add_value(const numeric_pair& v); diff --git a/src/math/lp/random_updater_def.h b/src/math/lp/random_updater_def.h index b90175646..01aa5fd25 100644 --- a/src/math/lp/random_updater_def.h +++ b/src/math/lp/random_updater_def.h @@ -30,6 +30,7 @@ random_updater::random_updater( const vector & column_indices) : m_lar_solver(lar_solver), m_range(100000) { + m_var_set.resize(m_lar_solver.number_of_vars()); for (unsigned j : column_indices) add_column_to_sets(j); }