Use What4.Serialize.Parser to parse solver models/values.

[andreistefanescu]

The SMT-LIB2 parsing code in What4.Protocol.SMTLib2 (parseDefineFun/parseLambda) is copy-pasted and adapted from What4.Serialize.Parser. Changes:

• What4.Protocol.SExp.SExp instead of What4.Serialize.Printer.SExpr
• SMT-LIB2 operators (and/+/...) instead of the What4.Serialize operators (andp/intmul/...)
• operator left/right associativity
• define-fun/lambda syntax instead of definedfn

[RyanGlScott]

Relatedly, the return type for the runGetAbducts function is a list of Strings, rather than something like an Expr, as we didn't have the capability to parse solver values at the time runGetAbducts was added. If we unify the treatment of our parsers, a next logical step would be to change runGetAbducts to return something more structured than Strings. (See this discussion.)