SMTChecker: Fix usage of Eldarica with SMT callback #14906
Merged
Conversation
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
blishko
changed the title
blishko
force-pushed
the
smt-eldarica
branch
2 times, most recently
from
692c306 to
65c6658
Compare
blishko
changed the title
ekpyron
reviewed
Mar 11, 2024
Previously, CHC engine with SMT interface would always call Eldarica if it was present in the system, regardless whether user specified model-checker-solver as smtlib2 or eld. Here we make sure Eldarica is called only when it is specified as the solver of choice. The proposed solution is to make SMTSolverCommand modifiable and set it up properly based on the user settings. This requires changes also in UniversalCallback, because in the compiler we must be able to check if the given callback is UniversalCallback provided by CommandLineInterface. This mechanism can be used to migrate also other solvers to the SMTLIB interface by further extending/adapting SMTSolverCommand. Its advantage is that meaning of the callback stays the same, thus there is not need to change anything on the side of solc-js.
|
Changelog entry added. |
ekpyron
approved these changes
Mar 11, 2024
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
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.
Previously, CHC engine with SMT interface would always call Eldarica if
it was present in the system, regardless whether user specified
model-checker-solverassmtlib2oreld.Here we make sure Eldarica is called only when it is specified as the
solver of choice.
The proposed solution is to make SMTSolverCommand modifiable and set it
up properly based on the user settings. This requires changes also in
UniversalCallback, because in the compiler we must be able to check if
the given callback is UniversalCallback provided by CommandLineInterface.
This mechanism can be used to migrate also other solvers to the SMTLIB
interface by further extending/adapting SMTSolverCommand.
Its advantage is that meaning of the callback stays the same, thus there
is not need to change anything on the side of solc-js.