mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-09 09:21:56 +00:00
Code Activity

shring lar_solver.h

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-05-08 19:23:55 -07:00 • committed by Lev Nachmanson
parent 4abd9843a0
commit fef954c028
2 changed files with 59 additions and 67 deletions
Download patch file Download diff file Expand all files Collapse all files

29
src/math/lp/lar_solver.h
View file

@ -50,34 +50,8 @@ class int_solver;
class lar_solver : public column_namer {
struct imp;
struct term_hasher {
std::size_t operator()(const lar_term& t) const {
using std::hash;
using std::size_t;
using std::string;
size_t seed = 0;
int i = 0;
for (const auto p : t) {
hash_combine(seed, (unsigned)p.j());
hash_combine(seed, p.coeff());
if (i++ > 10)
break;
}
return seed;
}
};
struct term_comparer {
bool operator()(const lar_term& a, const lar_term& b) const {
return a == b;
}
};
// the struct imp of PIMPL
imp* m_imp;
////////////////// nested structs /////////////////////////
struct undo_add_column;
////////////////// methods ////////////////////////////////
static bool valid_index(unsigned j) { return static_cast<int>(j) >= 0; }
@ -158,9 +132,6 @@ class lar_solver : public column_namer {
void prepare_costs_for_r_solver(const lar_term& term);
bool maximize_term_on_feasible_r_solver(lar_term& term, impq& term_max, vector<std::pair<mpq,lpvar>>* max_coeffs);
u_dependency* get_dependencies_of_maximum(const vector<std::pair<mpq,lpvar>>& max_coeffs);
void pop_core_solver_params();
void pop_core_solver_params(unsigned k);
void set_upper_bound_witness(lpvar j, u_dependency* ci, impq const& high);
void set_lower_bound_witness(lpvar j, u_dependency* ci, impq const& low);
void substitute_terms_in_linear_expression(const vector<std::pair<mpq, lpvar>>& left_side_with_terms,