mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-12 14:10:54 +00:00
Code Activity

rename add_lcs to add_lc

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-08-08 10:40:39 -07:00 • committed by Lev Nachmanson
parent 88293bf45b
commit 8598a74cca
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/nlsat/nlsat_explain.cpp
View file

@ -646,8 +646,8 @@ namespace nlsat {
return true; return true;
} }
// For each p in ps add the leading or coefficent to the projection, // For each p in ps add the leading coefficent to the projection,
void add_lcs(polynomial_ref_vector &ps, var x) { void add_lc(polynomial_ref_vector &ps, var x) {
polynomial_ref p(m_pm); polynomial_ref p(m_pm);
polynomial_ref coeff(m_pm); polynomial_ref coeff(m_pm);
@ -1203,7 +1203,7 @@ namespace nlsat {
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x);
tout << "\npolynomials\n"; tout << "\npolynomials\n";
display(tout, ps); tout << "\n";); display(tout, ps); tout << "\n";);
add_lcs(ps, x); add_lc(ps, x);
psc_discriminant(ps, x); psc_discriminant(ps, x);
psc_resultant(ps, x); psc_resultant(ps, x);
if (m_todo.empty()) if (m_todo.empty())
@ -1251,7 +1251,7 @@ namespace nlsat {
} }
TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n"; TRACE(nlsat_explain, tout << "project loop, processing var "; display_var(tout, x); tout << "\npolynomials\n";
display(tout, ps); tout << "\n";); display(tout, ps); tout << "\n";);
add_lcs(ps, x); add_lc(ps, x);
psc_discriminant(ps, x); psc_discriminant(ps, x);
psc_resultant(ps, x); psc_resultant(ps, x);