Rewrite-based decision procedures