From 4810b4cac29ce1ae255fdc3bc1a0718ce7b4b673 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Tue, 10 Nov 2020 11:12:28 -0800 Subject: [PATCH] add a comment in nla_order Signed-off-by: Lev Nachmanson --- src/math/lp/nla_order_lemmas.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nla_order_lemmas.cpp b/src/math/lp/nla_order_lemmas.cpp index fd33f5f38..800bc8bf1 100644 --- a/src/math/lp/nla_order_lemmas.cpp +++ b/src/math/lp/nla_order_lemmas.cpp @@ -293,7 +293,7 @@ void order::generate_ol(const monic& ac, lemma |= ineq(term(rational(1), ac.var(), -rational(1), bc.var()), var_val(ac) < var_val(bc) ? llc::GT : llc::LT, 0); // The value of factor k is val(k) = k.rat_sign()*val(k.var()). // That is why we need to use the factor signs of a and b in the term, - // but the constraint of the term is defined by val(a) and val(b). + // but the constraint of the lemma is defined by val(a) and val(b). lemma |= ineq(term(a.rat_sign(), a.var(), -b.rat_sign(), b.var()), val(a) < val(b) ? llc::GE : llc::LE, 0); lemma &= ac;