Add a parser for full Smtlib scripts - #717
Open
daniel-raffler wants to merge 106 commits into
Open
daniel-raffler wants to merge 106 commits into
daniel-raffler wants to merge 106 commits into
Conversation
…ITH_INTERPOLATION
…or as some solvers don't support all theories
Affected left associate operations like "substraction" where the arguments of the operation were in the wrong order
…luator" On second thought, it's probably best not to import the symbols and insist that every symbol that is used in the script must also be declared there. This avoids ambiguity about the type when capturing variables from the solver context
…one of them is not integer
# Conflicts: # lib/ivy.xml # src/org/sosy_lab/java_smt/SolverContextFactory.java # src/org/sosy_lab/java_smt/test/FormulaManagerTest.java # src/org/sosy_lab/java_smt/test/SolverBasedTest0.java
…add a new method `FormulaManager.parseScript` to run entire Smtlib scripts
…ke `check-sat` or `push` are not allowed
…printed in real-time
This was
linked to
issues
Oct 2, 2026
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Hello,
this PR adds a antlr parser and evaluator for Smtlib scripts to JavaSMT. To start the parser a new method
parseAndRunwas added toFormulaManger:The method will parse and evaluate a Smtlib script. Responses from the solver to commands such as
(check-sat)or(get-model)are logged and returned to the caller, so that they can be printed laterThere is also a asynchronous version of the method that returns solver responses right away, which can be useful for long running scripts:
While this PR is very large, a lot of the code is either boilerplate or autogenerated by Antlr. The interesting parts can be found here:
Smtlib.g4Antlr grammar for SmtlibPredefinedTheory symbol definitionsSmtlibEvaluatorSmtlib evaluator to run the script after parsingNote that the PR also includes a new
parsingdelegate to track user-defined symbols for the parser. It has some overlap with the various variable caches we already have for the solvers, and we may be able to get rid of it if we decide to make the Antlr parser the default optionKnown issues:
Z3 takes a very long time in(Mostly) fixed by enabling phantom referencesSolverContext.close()after parsing large files. This may be related to its garbage collector as all parsed terms now need to be tracked individually