mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-06 17:44:08 +00:00
Code Activity

comment change

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-02-06 13:41:14 -10:00 committed by Lev Nachmanson
parent d90b94d0e2
commit 17d68c18aa
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/dioph_eq.cpp
View file

@ -27,7 +27,7 @@
(k,xt,t) is added to m_fresh_k2xt_terms, where xt is the fresh variable, and t it the term defining the substitution: something like k - xt + 5z + 6y = 0. (k,xt,t) is added to m_fresh_k2xt_terms, where xt is the fresh variable, and t it the term defining the substitution: something like k - xt + 5z + 6y = 0.
The set of pairs (k, xt) is a one to one mapping The set of pairs (k, xt) is a one to one mapping
m_row2fresh_defs[i]: is the list of all xt that were defined for row m_e_matrix[i]. m_row2fresh_defs[i]: is the list of all xt that were defined for row m_e_matrix[i].
Invariant: Every xt in m_row2resh[i] must have a corresponding entry in m_fresh_k2xt_terms Invariant: Every xt in m_row2fresh[i] must have a corresponding entry in m_fresh_k2xt_terms
The mapping between the columns of lar_solver and m_e_matrix is controlled by m_var_register. The mapping between the columns of lar_solver and m_e_matrix is controlled by m_var_register.
local_to_lar_solver(lar_solver_to_local(j)) == j. If local_to_lar_solver(j) == -1 local_to_lar_solver(lar_solver_to_local(j)) == j. If local_to_lar_solver(j) == -1