mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-11 03:33:35 +00:00
Code Activity

add comments to hnf_cutter

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-07-02 16:17:11 -07:00
parent 80a4da9b1d
commit 49e49d6bb6
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/hnf_cutter.cpp
View file

@ -175,7 +175,7 @@ is equivalent to Hy≤b′ with y:=(U−1)x . Since the solution x0 of
A′x0=b′ is not integral, the corresponding vector y0=(U−1)x0 is not
integral, either. The cuts from proofs algorithm creates an extended
branch on one of the components y_i of y , i. e., y_i≤⌊y0_i⌋ or
y_i≥⌈y0_i⌉. Further on it the papetr there is a lemma showing that
y_i≥⌈y0_i⌉. Further on in the paper there is a lemma showing that
branch y_i≥⌈y0_i⌉ is impossible.
*/
lia_move hnf_cutter::create_cut(lar_term& t, mpq& k, explanation* ex, bool & upper