mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
change in a comment
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
79a8e9aab0
commit
1b62592015
|
@ -651,11 +651,11 @@ class mps_reader {
|
||||||
|
|
||||||
/*
|
/*
|
||||||
If rhs is a constraint's right-hand-side value and range is the constraint's range value, then the range interval is defined according to the following table:
|
If rhs is a constraint's right-hand-side value and range is the constraint's range value, then the range interval is defined according to the following table:
|
||||||
|
|
||||||
sense interval
|
sense interval
|
||||||
G [rhs, rhs + |range|]
|
G [rhs, rhs + |range|]
|
||||||
L [rhs - |range|, rhs]
|
L [rhs - |range|, rhs]
|
||||||
E [rhs, rhs + |range|] if range in [rhs - |range|, rhs] if range < 0
|
E [rhs, rhs + |range|] if range > 0,
|
||||||
|
[rhs - |range|, rhs] if range < 0
|
||||||
where |range| is range's absolute value.
|
where |range| is range's absolute value.
|
||||||
*/
|
*/
|
||||||
|
|
||||||
|
|
Loading…
Reference in a new issue