620 smtlib2 parser tokenizer wrongly rejects set logic commands and has a non helpful error message for parse for 1 items

[baierd]

Fixes issues from #620 by adding a state-machine for processing SMT-LIB2 programs.

Closes #620.

[daniel-raffler]

Our SMTLIB2 parser, to be exact its tokenizer, rejects set-logic commands that are not at the very beginning of the SMT-LIB2 file. This is wrong, these commands are allowed to be everywhere in the file and may be repeated with distinct settings!

I think this is backwards. Here is the diagram from the standard:

(Source of diagram: https://smt-lib.org/papers/smt-lib-reference-v2.6-r2021-05-12.pdf , 4.1 General Requirements, page 53)

So set-logic must be used before anything else can be done, and set-info can appear anywhere in the file

Did you run into any parsing issues with their benchmarks?

[ThomasHaas]

Did you run into any parsing issues with their benchmarks?

The issues he faces come from the smtlib files I gave in #613. The output we generate conforms to the shape required by SMT-COMP because we once submitted our benchmarks there.

[daniel-raffler]

Did you run into any parsing issues with their benchmarks?

The issues he faces come from the smtlib files I gave in #613. The output we generate conforms to the shape required by SMT-COMP because we once submitted our benchmarks there.

Thanks! I've had a look at it, and there seem to be two issues:

• We expect set-logic to be the first command in the file
• We currently don't support push/pop while parsing

In this case the problem is easily fixed by just commenting out some lines:
manyRegReads.smt2.txt

When I now try the tests, I get a runtime of 8s with logic ALL and 3s for the BV logic. However, this is only true after adding back in the push/pop around the assertions. Otherwise, the runtime is <1s for both cases, and the BV logic appears to be slightly slower

@baierd: We could easily fix the first problem by skipping set-option/set-info before the set-logic command. However, I'm not sure how push/pop could be handled by our parser

[ThomasHaas]

In this case the problem is easily fixed by just commenting out some lines: manyRegReads.smt2.txt

When I now try the tests, I get a runtime of 8s with logic ALL and 3s for the BV logic. However, this is only true after adding back in the push/pop around the assertions. Otherwise, the runtime is <1s for both cases, and the BV logic appears to be slightly slower

If the query is not incremental, Z3 will use the SAT Solver independently of the logic set (easy to see by executing Z3 with higher verbosity levels). I think most solvers ignore (set-logic) for non-incremental queries: they might only check syntactic conformance to the specified logic but otherwise exploit the fact that they know the whole query and what settings are best for solving it.
But for incremental queries, the solver has do expect the worst-case, i.e., that every further query introduces new logics.
This is particularly true over the programmatic API, where the solver simply cannot know about future queries; all he knows is the upper bound on logics given by (set-logic).

However, I'm not sure how push/pop could be handled by our parser

I think you would need a more general concept of an SMTQuery which is a list of SMTCommands: assert(formula), push, pop, check-sat. I don't think the existing API can do it.

[kfriedberger]

lgtm.

Why does the formatter or Checkstyle not warn about the String concatenation?
Please fix, then merge. Thanks.

[kfriedberger]

String concatenation not required. Remove the PLUS.

[baierd]

So set-logic must be used before anything else can be done, and set-info can appear anywhere in the file

If you want to solve the query, it is needed before something is asserted. Which is less strict.
But we don't want to solve the query, we parse it to a formula. Hence it does not matter for us currently, as Karlheinz already stated.

Btw. i left the token detection in for if we actually decide that we want to do something with it + documentation.

The standard however states that For benchmarks in the official repository a call to set-info with this attribute can occur only as the first command of a script., hence i wanted to allow it explicitly.

@ThomasHaas do you know whether comments are allowed to be placed before this set-info command?
Also, thank you for the clarification!

[baierd]

However, I'm not sure how push/pop could be handled by our parser.

If there is only push and pop, everything is easy, you just need a list of lists of formulas. The problem occurs when check-sat is used, because that can not be easily reflected with generic data-structures without being easily confusing or wrongly used.

We could just add a class ParsingResult that returns the information in a proper form. This could easily also reflect the other commands like set-logic as well. With such a structure it would also be easy to add Prover support (i.e. solve the formulas as dictated in the SMTLIB2), and therefore a parsing command that also solves could easily be added.

[ThomasHaas]

@ThomasHaas do you know whether comments are allowed to be placed before this set-info command? Also, thank you for the clarification!

I'm not sure if this is permitted in SMT-COMP, but does it really matter? You want to parse general smtlib2 which is far less restrictive: you can have comments everywhere and (set-info) doesn't need to be called at all.
Only when dumping whole queries to smtlib you might want to adhere to a more strict form.

[daniel-raffler]

If you want to solve the query, it is needed before something is asserted. Which is less strict.
But we don't want to solve the query, we parse it to a formula. Hence it does not matter for us currently, as Karlheinz already stated.

But shouldn't we at least try to keep to the standard? If we just want to allow set-info before set-logic, it's easy enough to just add a flag:

There is really no need to remove the check for that

The standard however states that For benchmarks in the official repository a call to set-info with this attribute can occur only as the first command of a script., hence i wanted to allow it explicitly.

The problem here is that MathSAT adds (set-info :source |printed by MathSAT|) at the top of its output when dumping formulas. This will then cause the new precondition to fail:

private String sanitize(String formulaStr) {
    List<String> tokens = Tokenizer.tokenize(formulaStr);

    StringBuilder builder = new StringBuilder();
    int pos = 0; // index of the current token

    for (String token : tokens) {
      if (pos == 0 && Tokenizer.isSetInfoToken(token)) {
        // set-info call is allowed to be the very first command in the benchmark, but can also
        // appear repeatedly throughout a SMT2 program
        // Technically it is even required to be the very first command, and it must set the
        //  :smt-lib-version attribute. See SMT-LIB 2.7 §3.11.3
        // TODO: check that version >= 2?
        Preconditions.checkArgument(token.contains(":smt-lib-version"));

The token is (set-info :source |printed by MathSAT|) here, and does not contain :smt-lib-version

We could probably fix this, but I'm not sure the check is even needed. According to the standard these are additional requirements for their benchmark files:

Benchmarks in the official SMT-LIB repository at www.smt-lib.org must satisfy additional
requirements on the meta-level information they contain and the order in which it appears.

• :smt-lib-version, :source, :license, and :category must be set exactly once,
• :status must be set as many times as needed so that each occurrence of the command
  check-sat-assuming or check-sat in the benchmark is preceded (not necessarily immediately) by a corresponding :status info

Moreover, the set set-info call for attribute :smt-lib-version must be the very first com-
mand in the benchmark.

We're trying to parse "regular" SMTLIB files, so this shouldn't apply to us

If there is only push and pop, everything is easy, you just need a list of lists of formulas. The problem occurs when check-sat is used, because that can not be easily reflected with generic data-structures without being easily confusing or wrongly used.

Yes, that might be one way to solve it. In this particular example, however, the interesting assertion isn't even on the stack anymore at the end of the SMTLIB file. Instead, it was replaced by false, which makes the problem trivially unsat. We would need some way to get the assertions at different points in time. However, this might just become a little to confusing for the user

[baierd]

But shouldn't we at least try to keep to the standard?

Yes and no. We try to follow the standard as far as it makes sense. Many solvers do non-standard things and we adapt.

If we just want to allow set-info before set-logic, it's easy enough to just add a flag:

No. This is a clear example for a state-machine. Starting with flags etc. would lead to confusing/complex code.

And yes, as stated above, the rule with set-info having to specify :smt-lib-version first is only relevant for the competition, i will remove the precondition.
I find it curious that the standard specifies things about the competition though.

[baierd]

So the problem is the following: if we assume the diagram above to be accurate, most solvers don't produce valid SMT-LIB2. Since we know this, we allow some leniency, most notably; we assume implicit logic selection for logic ALL if there is none. This merges the 2 states essentially. Since we are only parsing, and not solving, the SAT_MODE and UNSAT_MODE are essentially merged into RESULT_MODE for us. And since we are not allowing reset currently, what is left is a very limited automaton with 2 states.

Btw. i also found that the diagram above is incomplete, as exit is for example not handled. But it is quite clear how it should be handled (additional sink state).

I now added a implementation that can easily switch between all of this, depending on a single boolean flag to control whether we allow implicit set-logic 'ALL'.

@daniel-raffler i found that Boolector seems to return an empty SMTLIB2 String in a test case (that i now disabled). Could you open a issue and take a look?

Also, i found that we throws exceptions every time we load Bitwuzlas options due to our "further options" implementation (in our code, not Bitwuzlas). While not part of this PR, I still added a small simplification to check for an empty options string to skip the evaluation (as it made my debugging harder ;D). @daniel-raffler would you be so kind and open another issue for this and take a look? Exception based control flow is Java is a very bad idea and we should not do it if possible.

[baierd]

TODO: is a SMTLIB2 program with only (check-sat) a valid program if we assume that the logic is set implicitly? (Because we don't allow this currently)

Edit: nvm we actually have tests for this. I need to change the current behavior.

[daniel-raffler]

Looks fine to me! There are a few TODOs left open, and a lot of the methods in SMTLIB2ProgramStateMachine are currently unused. Do you plan to extend this later? Otherwise, we could probably simplify the class a bit

[daniel-raffler]

This comment seems to have been cut off