From 49e49d6bb65d9e5ca3fc74845e887c37fc26be1d Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Thu, 2 Jul 2020 16:17:11 -0700 Subject: [PATCH] add comments to hnf_cutter Signed-off-by: Lev Nachmanson --- src/math/lp/hnf_cutter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/hnf_cutter.cpp b/src/math/lp/hnf_cutter.cpp index 87b6e1a01..2cf132873 100644 --- a/src/math/lp/hnf_cutter.cpp +++ b/src/math/lp/hnf_cutter.cpp @@ -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