Add Flex/Bison parser

[makaimann]

This PR adds an SmtLibReader class with virtual methods for common SMT-LIB commands. This way, a user can inherit the class and perform their own actions on standard commands. By default, it just executes the commands on the provided solver.

Currently supports:

• Bool/Int/Real/BV/Array/UF
• quantifiers
• let bindings
• declare-fun/declare-const/define-fun
• set-logic/set-option/set-info
• check-sat/check-sat-assuming/push/pop/exit

The infrastructure is based on the calc++ example.

I'm new to Flex/Bison so please let me know if there are any inefficiencies/broken conventions that you notice. Of course, trying to balance making it nice vs. getting it done soon so it's not going to be perfect. One particularly ugly part right now is here:
https://github.com/makaimann/smt-switch/blob/9b7fe79103648da4d5e7fc4ea0bf973abfd0e4a7/src/smtlibscanner.l#L72

Basically, there can be multiline string literals in set-info, or in a pipe-quoted symbol, e.g.:

(set-logic QF_LIA)
(declare-const |a
                multi-line
                symbol|
                Int)

Currently, the lexer combines that into one token. However, this can mess up error reporting since the line number is off. So that linked code just increments the line number accordingly. I did briefly try splitting them into one token per line and recombining them in the bison parser but ran into some issues. I could probably get it working if you think that's better. Let me know if you think that's a lot better than the current solution.

[makaimann]

Here are the initial parser results. Note: incremental benchmarks have more solved than the total since each sat/unsat counts as a solve. I have no idea why smt-switch solves so many fewer QF_AUFLIA benchmarks. It could be a parser issue, but since all the others seem to be fine, I'm guessing it's actually a difference in the default options. I'll look into that more today.

The most important thing is that the status is "ok", meaning there were no disagreements.

[makaimann]

Btw, the tests above were ran with an older version. I'll run tests again soon with the latest. Looking into cvc4's default options first.

[makaimann]

All right, I found the slowdown. The crash3.smt2 benchmark in the safari set was very large and made frequent use of define-funs. My define-fun handling uses naive substitution, and the substitution operation was slow for CVC4. Fixed with: #184. Here are the latest results where smt-switch wins in most categories:

[barrettcw]

Awesome!

[ahmed-irfan]

Looks great!

I guess the get commands (get-unsat-core, get-value, get-model etc) are left for future work. RIght?

[ahmed-irfan]

All right, I found the slowdown. The crash3.smt2 benchmark in the safari set was very large and made frequent use of define-funs. My define-fun handling uses naive substitution, and the substitution operation was slow for CVC4. Fixed with: #184. Here are the latest results where smt-switch wins in most categories:

That is indeed great!

Interestingly, smt-switch-cvc4 solves way more in the QF_AUFLIA

[makaimann]

Thanks for the review!

I guess the get commands (get-unsat-core, get-value, get-model etc) are left for future work. Right?

Yeah that's right -- I haven't thought about those much yet. get-value would be easy if we need that. I think get-unsat-core and get-model would take a bit more thought.

[makaimann]

Interestingly, smt-switch-cvc4 solves way more in the QF_AUFLIA

Right, so that's actually entirely from the single crash3.smt2 benchmark. It has a huge number of check-sat calls (1,109,912 total) and they're all very quick (at least all the ones that we get to in the time limit). So I think there's a noticeable difference there just because flex/bison is faster than ANTLR and there's very little time in the solver.

[amaleewilson]

Looks good to me

[ahmed-irfan]

LGTM.

Suggestion: please open issues for the todos, like supporting getter functions in the parser.

[makaimann]

Thanks for the reviews! Made an issue for the getters: #190.