search

cvc5 / LFSC

LFSC Proof Checker
Other
11 stars 9 forks source link

Lexer #40

Closed alex-ozdemir closed 4 years ago

alex-ozdemir commented 4 years ago

This PR introduces a flex-based lexer.

check is still a combined parser and checker, but it doesn't have to do tokenization.

This introduces flex as a build dependency.

I my benchmarks this actually gives a small speedup.

alex-ozdemir commented 4 years ago

Note: The Travis CI is broken. I believe that I've disabled it, and it will not affect future builds.

barrettcw commented 4 years ago

A few minor questions.

This is a really nice direction I think. I'm not very attached to the old lexing code :)

I'm not too familiar with flex, I assume adding this is a safe long-term decision?

flex has been around for a long time (we were using it when I was in grad school). It is probably the most popular open-source lexer. I think it's safe to depend on it.

alex-ozdemir commented 4 years ago

Also, do you have any more detailed information on the speedup you are seeing?

It's not very rigorous, but hyperfine reports that the new version is a bit faster. Log file attached. I'm mostly just glad we're not slower this way.

log.txt

ajreynol commented 4 years ago

LGTM, thanks again for adding this.