An implementation of compositional rewriting theory algorithms based upon the Microsoft Z3 SMT solver.
