Solver independent interpolation #432
Draft
Conversation
This file contains 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
…reconditions. Also make sure that interpolationStrategy is not null to remove the warning from the if-clause below. This may not be necessary, because it is already ensured that interpolationStrategy cannot be null at that time.
…ModelBasedInterpolant method to better understand the model-based approach and its implementation.
…ied, by adding checkArguments and delete the corresponding TODO.
…ifierEliminationBasedInterpolant to understand the quantifier-based approach and its implementation better
…hether they are empty and write a corresponding errorMessage
…ning go away. This may not be necessary since it is already certain that interpolationStrategy cannot be null at this point.
…ther a generated interpolant is really valid and satisfies the definition of Craig interpolation.
…he purpose of the method. TODO: You may want to rename the method to satisfyCraigInterpolationCriteria if the name is not too long and there is still some confusion.
…ion of Craig Interpolation by checking it in the getQuantifierEliminationBasedInterpolant method.
…ion about the context and check that the quantifier has been eliminated properly and return an error if its still present and do some clean up.
…etter understanding.
…een eliminated properly in the getForwardInterpolant method. And do some clean up.
…ter understanding of the implementation and the strategy.
…nding of the implementation.
…te on. TODO is done.
…InterpolationFormula already do it
baierd
commented
Jan 17, 2025
There was a problem hiding this comment.
Some small hints about the most urgent needed changes @stefaniesinner
| private BooleanFormula getModelBasedInterpolant( | ||
| Collection<BooleanFormula> formulasOfA, Collection<BooleanFormula> formulasOfB) | ||
| throws InterruptedException, SolverException { | ||
|
|
There was a problem hiding this comment.
The cases for empty interpolation groups A and/or B is missing.
| ProverOptions.GENERATE_UNIFORM_FORWARD_INTERPOLANTS); | ||
| itpStrat.retainAll(allIndependentInterpolationStrategies); | ||
| if (itpStrat.isEmpty()) { | ||
| return null; |
There was a problem hiding this comment.
Instead of null we could use Optional, avoiding the ugly null with code that needs explicit checking.
| private BooleanFormula getQuantifierEliminationBasedInterpolant( | ||
| Collection<BooleanFormula> formulasOfA, Collection<BooleanFormula> formulasOfB) | ||
| throws SolverException, InterruptedException { | ||
|
|
There was a problem hiding this comment.
The cases for empty interpolation groups A and/or B is missing.
Note: since this is the same for model based, you could handle it further up in the calling method.
baierd
commented
Jan 17, 2025
|
|
||
| // The non-interpolating delegates usually return nothing useful as itp points, so we have to | ||
| // track it here | ||
| @SuppressWarnings("unused") |
There was a problem hiding this comment.
This is not needed anymore.
| private static @Nullable ProverOptions getIndependentInterpolationStrategy( | ||
| Set<ProverOptions> options) { | ||
| List<ProverOptions> itpStrat = new ArrayList<>(options); | ||
| final Set<ProverOptions> allIndependentInterpolationStrategies = |
There was a problem hiding this comment.
This looks like a constant.
| if (itpStrat.isEmpty()) { | ||
| return null; | ||
| } | ||
| Preconditions.checkState(itpStrat.size() == 1); |
There was a problem hiding this comment.
Since we only allow exactly 1 solver independent interpolation option, we could fail here more gracefully with an InvalidConfigurationException explaining the problem.
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.
This MR adds solver independent interpolation as an option to JavaSMT.
Currently there are 2 distinct techniques used, model based and uniform interpolants based on quantifier elimination.
The uniform interpolants can be generated in a forward and backwards way.
Tests have been extended to test the native interpolation together with the new independent interpolation.
This is currently a WIP MR and not yet finished.