Lab 3 assessment

[grammarware]

Parsers are usually tested by round-tripping: given a correctly formed term, unparsing it and parsing the result should yield the same term. (A round trip may start with a grammatically formed string, but it is harder since determining whether two strings are equivalent with respect to a given grammar, is not trivial — see some explanation here in §3). Your tests are necessary but impractically far from sufficient. An easy way to see it is to notice your conditions are formulated in a regular way (“foo should be followed by bar”), and an expression language is context-free and therefore can only be approximated by regular means. Theoretically if I remember correctly it is proven that a combination of a Dyk language and regular expressions is as expressive as CFG — practically it means you should have checked for balanced brackets ;)

It is just as traditional to leverage basic algebraic laws by any normalisation — in your case it would mean at least removing duplicate clauses in all conjunctions and disjunctions. You could do this while flattening if it's bottom up, or after flattening (as in Jan’s reference solution). Same things in a more severe incarnation are needed in the bonus assignment due to the nature of SAT solving. For details I refer again to the reference implementation.

Why ndiv2 in the random formula generator? n - 1 is too mainstream?

With some rough edges, it is still well :heavy_plus_sign::heavy_plus_sign: worth of effort.

[stil4m]

Thanks for the feedback @grammarware. I think it would be a good idea to improve the tests so I will leave the ticket open for now.

For the n-1 or n``div``2 (@pacbeckh asked the same question to Jan yesterday). I wouldn't say that n-1 is too mainstream. In the online and Jan's examples we found the n``div``2. Together with the idea that we wanted to decrease the size of the sub formulas in rather big steps made us pick the n``div``2.