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
…las in class IndependentInterpolation
…polants of class AbstractInterpolatingProver to avoid unintended usage
…st to ImmutableList
…dInterpolant and add a new getModelBasedInterpolant method
…originalStack variable
…as from the current stack
…rpolant in getModelBasedInterpolant
…calling an UF into a separate method
getUniqueInterpolant to generate unique IDs for UFs
…elBasedInterpolant
…e formulas, variables and shared variables
…rs in method getForwardInterpolant
…ntially empty result in getBoundVars, method getForwardInterpolant now checks if bound vars are equal to shared vars to avoid deleting all variables in a formula by performing QE
…nt interpolation in ProverOptions
…Test0 to specify the interpolation strategies
…eterizedInterpolatingSolverBasedTest0
…eded to check if sharedVars is empty, since the shared variables are always generated
…eIndependentSequentialInterpolation in test binaryBVInterpolation1, since it already covers this method in its implementation and the test is using sequential interpolation
…eIndependentSequentialInterpolation in test binaryInterpolation1, since it already covers this method in its implementation and the test is using sequential interpolation
…ng the independent interpolation strategy 'model-based interpolation' because it returns Inconclusive
…lvers PRINCESS and CVC5 using one of the independent interpolation strategies by implementing a new method requireIndependentInterpolationWithConstantFalse, because both solvers return only TRUE instead of FALSE
…g one of the independent interpolation strategies because of wrong results by implementing a new method requireIndependentInterpolationSolvingIssue381()
…VC5 and PRINCESS using model-based interpolation because all solvers return null or unknown on sat check
…ialInterpolation() expected 1 positional arguments, but saw 0
…nterpolatingProverEnvironment to match pattern '^[A-Z][0-9]?$'
…BooleanFormula, Model, and SolverException) since using the '.*' form of import should be avoided
…ckward QE, because quantifier has not been eliminated properly in the interpolant. Instead of checking if the quantified formula is equals to the formula after QE, check if the formula after QE contains "ALL" (by backward) or "EX" (by forward)
…YMBOL_QUANTIFIER_EXISTS' for using "ALL" and "EX" in the quantifier elimination interpolation strategy
…uantifier-free interpolant after checking if it does not contain a quantifier. Improve SolverException message thrown if the resulting interpolant still contains quantifiers
…erpolation strategies. Add this exception and SolverException to the method signature
…ted during the process in both quantifier elimination interpolation strategies. Throw a new SolverException if they were accidentally deleted during the process.
…upport quantifier-elimination (for this logic)' to 'Solver does not support the complete theory of quantifiers' in both quantifier elimination interpolation strategies
…tion of Craig Interpolant correctly
…riable ip1 is declared and initialized, but not used. Use it for now to generate an itp
…g in Pipeline" This reverts commit 47af7f3.
…r.getModel() with a try-with-resources block
…onProver in satisfiesInterpolationCriteria with a try-with-resources block
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.