Strip SMT-LIB2 queries before parsing #401
Conversation
…andle comments and logics) TODO: escaped chars etc.
…e will first clean up the input string in parse(), and then call parseImpl() to have it parsed by the solver.
…made the method protected.
… This will make the implementation less lazy. However, most (native) solvers just dump the String anyway and we need this to add postprocessing later.
…n our Bitwuzla parser code
| BooleanFormula parsedForm = mgr.parse(BOOL_VARS_W_LOGIC_AND_COMMENT); | ||
| assertThatFormula(parsedForm).isEquivalentTo(expr); | ||
| } | ||
|
|
There was a problem hiding this comment.
We need a few more tests:
- remove/sanitize comments from SMTLIB
- allow/no sanitize weird names like with escaped keywords, if allowed.
| return new Appenders.AbstractAppender() { | ||
|
|
||
| StringBuilder builder = new StringBuilder(); | ||
| new Appenders.AbstractAppender() { |
There was a problem hiding this comment.
Is this Appender still required? Can't we just use the StringBuilder?
| String raw = dumpFormulaImpl(formulaCreator.extractInfo(t)); | ||
| out.append(sanitize(raw)); | ||
| } | ||
| }; | ||
| } |
There was a problem hiding this comment.
Is Lambda possible in this place? Maybe:
return out -> {
String raw = dumpFormulaImpl(formulaCreator.extractInfo(t));
out.append(sanitize(raw));
};
If not, looks also good.
There was a problem hiding this comment.
Yes, I think we need an actual AbstractAppender object for the toString overload. When I changed the code it created an Appender instance, but toString would just return the Object name and not the printed String.
src/org/sosy_lab/java_smt/basicimpl/AbstractFormulaManager.java
Outdated
Show resolved
Hide resolved
| protected static boolean isSetLogicToken(String token) { | ||
| return token.matches("\\(\\s*set-logic.*"); | ||
| } | ||
|
|
There was a problem hiding this comment.
Is the visibility required? Maybe make it "private"?
| protected static boolean isAssertToken(String token) { | ||
| return token.matches("\\(\\s*assert.*"); | ||
| } | ||
|
|
There was a problem hiding this comment.
Is the visibility required? Maybe make it "private"?
| protected static boolean isDeclarationToken(String token) { | ||
| return token.matches("\\(\\s*(declare-const|declare-fun).*"); | ||
| } | ||
|
|
There was a problem hiding this comment.
Is the visibility required? Maybe make it "private"?
There was a problem hiding this comment.
isDeclarationToken is actually used in BitwuzlaFormulaManger here. But I can make the other ones private.
| protected static boolean isDefinitionToken(String token) { | ||
| return token.matches("\\(\\s*define-fun.*"); | ||
| } | ||
|
|
There was a problem hiding this comment.
Is the visibility required? Maybe make it "private"?
| } | ||
| return builder.build(); | ||
| } | ||
|
|
There was a problem hiding this comment.
The parser looks impressive, and on first look it should work well.
Are there tests for all cases:
- valid brackets
- invalid brackets
- nested brackets
- empty brackets
- comments
- nested comments
- newlines for Unix
\nand Windows\ror\r\n(maybe use System.lineSeparator())
Hi Karlheinz, |
…sted by @kfriedberger" This reverts commit 8ab8c57.
… of the string. The original expression ".*" is problematic as "." does not include newline in Java. We worked around this by stripping newlines from the smtlib string before matching, but this won't work when the newline is escaped in a string literal or a quoted symbol.
…ix broken MathSAT tests
|
@kfriedberger |
Hello,
this MR adds some basic preprocessing for SMT-LIB2 queries before they are sent off to the solver for parsing. Most of the functionality has already been included as part of the OpenSMT/Bitwuzla backends, but it has now been improved and moved directly to
AbstractFormulaMangerwhere it can be used by all solvers. This should avoid further redundancies in the code and will help us solves the issues described in #372.The idea behind the MR is to restrict ourselves to a simplified version of the SMT-LIB2 format that is sufficient to parse (and print) SMT-LIB2 queries. For this we remove comments and commands like
(set-logic ...)and(exit)as they keep us from reusing the solver context. Operations like(push)or(get-value ..)are also removed, and we only keep declarations and assertions in our query. These simplified SMT-LIB2 scripts are then passed on to the solver where the actual parsing is done. We also use the same transformation to clean up the output ofdumpFormulain a solver independent way.