Support strings in refinements

[nilehmann]

We should have a string sort encoded as a string in z3/fixpoint and refine str by it. The following is a minimal test case we should support

#[flux::spec(
fn require_eq(x: &str[@a], &{str[@b] | a == b}))]
fn require_eq(x: &str, y: &str) {}

fn test_good() {
    require_eq("a", "a");
}

fn test_bad() {
    require_eq("a", "b");
}

Right now both test_good and test_bad are accepted by Flux, because strings are refined by unit.