mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-10-05 07:23:58 +00:00
Code Activity

merge

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2017-05-18 13:18:16 -07:00
commit 942f8f8c49
5 changed files with 5 additions and 31 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/util/lp/lar_solver.h
View file

@ -62,7 +62,6 @@ class lar_solver : public column_namer {
vector<lar_term*> m_terms;
const var_index m_terms_start_index;
indexed_vector<mpq> m_column_buffer;
std::function<column_type (unsigned)> m_column_type_function;
public:
lar_core_solver m_mpq_lar_core_solver;
unsigned constraint_count() const;

2
src/util/lp/mps_reader.h
View file

@ -655,7 +655,7 @@ class mps_reader {
sense interval
G [rhs, rhs + |range|]
L [rhs - |range|, rhs]
E [rhs, rhs + |range|] if range ¡Ý 0 [rhs - |range|, rhs] if range < 0
E [rhs, rhs + |range|] if range in [rhs - |range|, rhs] if range < 0
where |range| is range's absolute value.
*/