Canonized Rewriting and Ground AC Completion Modulo Shostak Theories : Design and Implementation (Logical Methods in Computer Science, 2012)