Still trying to understand exactly what this is. It seems like its like a declarative DSL for interacting with an SMT solver? Is this supposed to be for different use cases than an SMT solver? Does it solve different classes of problems, or is it just a different "interface" to the same basic capabilities?