mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 05:18:44 +00:00
Code Activity

use u_set in random_update()

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-03-26 18:11:32 -07:00
parent 12f62e73d5
commit 352f4b5b37
2 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/random_updater.h
View file

@ -25,17 +25,17 @@ Revision History:
#include <string>
#include <algorithm>
#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 <typename T> struct numeric_pair; // forward definition
class lar_solver; // forward definition
class random_updater {
std::set<var_index> 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<numeric_pair<mpq>, 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<mpq>& v);

1
src/math/lp/random_updater_def.h
View file

@ -30,6 +30,7 @@ random_updater::random_updater(
const vector<unsigned> & 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);
}