Getting multiple candidates of syntax trees when the parser is ambiguous (DDM)

[aqjune-aws]

In the case of parsing an SMT response, there is a valid case where the parsing rules can be ambiguous and it can return multiple syntax trees.
It is the user that picks the right syntax tree, depending on the SMT command that the user has executed.

For example, if a user executes (get-model), the response of SMT solver will be something like this:

(
  (define-fun z () Real (- 2.0))
  (define-fun y () Real (- 2.0))
  (define-fun x () Real 1.0)
)

This corresponds to the get_model_response syntax category in SMT-LIB 2.7 (Appendix B) but this expression can also be parsed as get_proof_response and get_option_response categories.

Parsing the above response is simply failing for now, but it would be great if there is an option for #strata to return multiple parsing trees.

A relevant PR: #159