After recent changes in preprocessing, theory specific rewriting now
don't see the whole formula, only parts that have not been processed
yet. This, however, broke an assumption made by theory combination.
Previously, it assumed it will see the whole formula, and it extracts
interface variables from it.
To fix this problem, we remember all processed formulas and notify
Theory about them at the end of each preprocessing. This means, we do
not change how we extract and set interface variables, but we need to
keep this extra information about preprocessed formulas.
We also start storing information related to preprocessing in a new
Preprocessor class. We should eventually move all preprocessing related
matters out of MainSolver and into this helper class.
After recent changes in preprocessing, theory specific rewriting now don't see the whole formula, only parts that have not been processed yet. This, however, broke an assumption made by theory combination. Previously, it assumed it will see the whole formula, and it extracts interface variables from it.
To fix this problem, we remember all processed formulas and notify Theory about them at the end of each preprocessing. This means, we do not change how we extract and set interface variables, but we need to keep this extra information about preprocessed formulas.
We also start storing information related to preprocessing in a new Preprocessor class. We should eventually move all preprocessing related matters out of MainSolver and into this helper class.
Fixes #705.