Why does Z3 use such operation in get_model() from Simplex?

[yuffon]

I have a question about the linear programming implemented in Z3. In src/math/lp/lar_solver.cpp, lar_solver::get_model(), the get_model() function fetches values from the model created by the tableau methods. The get_model() function contains the following code.

z3/src/math/lp/lar_solver.cpp

Line 1172 in 0a7e003

mpq x = rp.x + m_delta * rp.y;

In the context of QF_LIA, the value of each variable is stored in numeric_pair & rp. I want to know why each value is represented by a numeric pair of two rationals. Why the final value of each variable is computed by mpq x = rp.x + delta * rp.y; What does delta mean?

[NikolajBjorner]

the values in the tableau are of the form x + yepsilon, where epsilon is so small that |yepsilon| is smaller than any |x| value. To compute that epsilon we calculate the required delta. @levnach

[yuffon]

Thanks for your reply. In my two examples, I see that the initial value of delta is 1/2. y always takes 0. The value of delta will become delta/2 if some condition is satisfied. I think 1/2 is not a small number. Why not use a rational in the tableau directly?

[NikolajBjorner]

Not sure what to say here. There is some disconnect in what the solver does and what you believe it should do.
There are some starting points, such as CAV 2006 paper by Dutertre and de Moura, papers by Dana Scott from 1960s on non-standard arithmetic. See also Enderton textbook's section on non-standard arithmetic.
Simply put, Simplex uses an extended number field. There are many textbooks on this.

[yuffon]

Thanks for your answers.

[yuffon]

I had read the non-standard analysis section in Enderton's logic textbook. Just now I checked the CAV 2006 paper. It is due to the strict bounds. I think I had read this part in the past. I just forget it somehow.