Rewrite-based satisfiability procedures for recursive data structures