Skip to content

Commit

Permalink
add a comment in nla_order
Browse files Browse the repository at this point in the history
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
  • Loading branch information
levnach committed Nov 10, 2020
1 parent fc5e5a2 commit 4810b4c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion src/math/lp/nla_order_lemmas.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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;
Expand Down

0 comments on commit 4810b4c

Please # to comment.