Solver independent interpolation#432

Draft

baierd wants to merge 326 commits intomasterfrom solver_independent_interpolation

+1,102-92

This pull request is big! We're only showing the most recent 250 commits

Commits on Oct 27, 2024

Commits on Dec 13, 2024

Model ITP: Replace addConstraint with push to assert and create formulas in class IndependentInterpolation
stefaniesinner
committed
Model ITP: Add unsupported operation exception in method getTreeInterpolants of class AbstractInterpolatingProver to avoid unintended usage
stefaniesinner
committed
Model ITP: Change return type of method getFreeArithVars from ArrayList to ImmutableList
stefaniesinner
committed
Model ITP: Delete unused import statement
stefaniesinner
committed
Model ITP: Simplify method name of getFreeArithVars to getVars
stefaniesinner
committed
Model ITP: Simplify parameter name in getVars method from pFormulas to formulas
stefaniesinner
committed
Model ITP: Simplify parameter name in getSharedVars method from pVars to vars
stefaniesinner
committed
Model ITP: Rename method getModelBasedInterpolant to computeModelBasedInterpolant and add a new getModelBasedInterpolant method
stefaniesinner
committed
Model ITP: Store the currently asserted formulas in the stack in the originalStack variable
stefaniesinner
committed
Model ITP: Create new method clearStack to remove all asserted formulas from the current stack
stefaniesinner
committed
Model ITP: Create new method restoreStack to restore the original stack
stefaniesinner
committed
Model ITP: Call and return the result of method computeModelBasedInterpolant in getModelBasedInterpolant
stefaniesinner
committed
Model ITP: Extract the process of generating an ITP by declaring and calling an UF into a separate method
stefaniesinner
committed
Model ITP: Refactor of method
stefaniesinner
committed
Model ITP: Delete pop statement in computeModelBasedInterpolant
stefaniesinner
committed
Model ITP: Improve return type and documentation of method computeModelBasedInterpolant
stefaniesinner
committed
QE ITP: Create method getQEBasedInterpolant and declare and initialize formulas, variables and shared variables
stefaniesinner
committed
QE ITP: Create method getForwardInterpolant
stefaniesinner
committed
QE ITP: Create method getBoundVars and declare and initialize boundVars in method getForwardInterpolant
stefaniesinner
committed
QE ITP: Check if boundVars is empty and perform QE if needed and return QE ITP
stefaniesinner
committed
QE ITP: Refactor of method getBoundVars. Instead of returning an potentially empty result in getBoundVars, method getForwardInterpolant now checks if bound vars are equal to shared vars to avoid de…
stefaniesinner
committed
QE ITP: Implement method getBackwardInterpolant
stefaniesinner
committed
QE ITP: Delete unused import statement
stefaniesinner
committed
ITP: Assert 'ip0 != null' in class IndependentInterpolation
stefaniesinner
committed
ITP TESTING: Add option for model-based and QE-based solver independent interpolation in ProverOptions
stefaniesinner
committed
ITP TESTING: Add a new parameter to parametrized tests in SolverBasedTest0 to specify the interpolation strategies
stefaniesinner
committed
ITP TESTING: Rename class from ParameterizedSolverBasedTest0 to ParameterizedInterpolatingSolverBasedTest0
stefaniesinner
committed
Revert "ITP TESTING: Rename class from ParameterizedSolverBasedTest0 to ParameterizedInterpolatingSolverBasedTest0"
stefaniesinner
committed
Revert "ITP TESTING: Add a new parameter to parametrized tests in SolverBasedTest0 to specify the interpolation strategies"
stefaniesinner
committed
Reapply "ITP TESTING: Add a new parameter to parametrized tests in SolverBasedTest0 to specify the interpolation strategies"
stefaniesinner
committed
Revert "Reapply "ITP TESTING: Add a new parameter to parametrized tests in SolverBasedTest0 to specify the interpolation strategies""
stefaniesinner
committed
ITP TESTING: Create new class ParameterizedInterpolatingSolverBasedTest0 and let InterpolatingProverTest extend it
stefaniesinner
committed
ITP TESTING: Update prover environment in class InterpolatingProverTest to build the prover based on the new itp strategies
stefaniesinner
committed
QE ITP: Add documentary to methods
stefaniesinner
committed

Commits on Dec 16, 2024

Commits on Dec 17, 2024

Commits on Jan 9, 2025

Commits on Jan 14, 2025

Commits on Jan 20, 2025

Commits on Jan 21, 2025

Commits on Jan 24, 2025

Commits on Jan 25, 2025

Commits on Jan 26, 2025

disable Yices2 quantifiers, as they have problems (TODO: investigate)
BaierD
committed

Commits on Jan 27, 2025

Commits on Jan 28, 2025

Commits on Jan 29, 2025