mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-05-09 16:55:47 +00:00
Code Activity

implement imp of lar_solver as lar_solver::imp

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-05-07 13:53:28 -07:00
parent 97c6074156
commit d4f45e1528
2 changed files with 3 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/math/lp/lar_solver.cpp
View file

@ -15,7 +15,7 @@ namespace lp {
column m_column;
};
struct imp {
struct lar_solver::imp {
lar_solver &lra;
var_register m_var_register;
svector<column> m_columns;
@ -51,7 +51,6 @@ namespace lp {
};
};
imp* m_imp;
lp_settings& lar_solver::settings() { return m_settings; }
lp_settings const& lar_solver::settings() const { return m_settings; }
@ -188,7 +187,7 @@ namespace lp {
m_status = s;
}
const u_dependency* lar_solver::crossed_bounds_deps() const { return m_imp->m_crossed_bounds_deps;}
u_dependency*& crossed_bounds_deps() { return m_imp->m_crossed_bounds_deps;}
u_dependency*& lar_solver::crossed_bounds_deps() { return m_imp->m_crossed_bounds_deps;}
lpvar lar_solver::crossed_bounds_column() const { return m_imp->m_crossed_bounds_column; }
lpvar& lar_solver::crossed_bounds_column() { return m_imp->m_crossed_bounds_column; }
lpvar lar_solver::local_to_external(lpvar idx) const { return m_imp->m_var_register.local_to_external(idx); }

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

@ -47,9 +47,9 @@ namespace lp {
class int_branch;
class int_solver;
struct imp;
class lar_solver : public column_namer {
struct imp;
struct term_hasher {
std::size_t operator()(const lar_term& t) const {
using std::hash;