reintroduce m_var_register, and avoid modulo gcd in normalize conflicts

added some comments

cleaning up the inner tightening code

avoid the variable mapping to m_ematrix and suppressing redundand con…

use more descriptive functions than casting comparisons

tidy

use pattern of matching with undef instead of matching with conflict …

fix a print out

attempt to use the gcd of fixed vars

fix #7590 logic alphabet soup

add comment on derivation of bound

Fix : typo-in-simplify-tactic (#7587)

detect more m_terms_to_tighten

remove an unused field

add public access to bijection key_val iterator

nit

neatify loops

use iterators on goal and other refactoring

remove 'unsat' move, we already have 'conflict'. Add display for canc…

code review updates, tidy pretty printer for column info

fix bug introduced while absstracting m_conflict_index

isolate m_conflict_index functionality

add systematic way to combine lia_move results

nits

print also column values

remove term sorting by the span

fix #7584

sort terms by weight for tightening

more aggressive term tightening

try another sorting of terms to tighten