-
Notifications
You must be signed in to change notification settings - Fork 42
Closed
Description
The table of term replacements used in simplifyConjunctions should be kept in the SideCondition. Instead of running simplifyConjunctions in the Condition simplifier, the TermLike and Predicate simplifiers will look up their argument in the SideCondition.
This will enable us to apply assumptions from the SideCondition while applying equations, which is not currently possible.
- Make
SideConditionaMultiAndofPredicate.
Appetite: S. This is not the final form it will take, but this change will expose any places in the code where we make assumptions about the form ofSideCondition. At this point, we are still only using theSideConditionto send to the solver. There should be instancesFrom (Predicate variable) (SideCondition variable)andFrom (SideCondition variable) (Predicate variable). These instances must continue to work through the following steps. - Specialize for looking up
Predicate.
Appetite: S.TheTheSideConditionshould contain aHashSetfor looking up if a predicate is\topor\bottom.SideConditionshould contain aHashMapfromTermLike variableto the same, storing the map used here so it's not computed every time. ThePredicatesimplifier should look up its argument in theSideCondition. Before Predicate should have a distinguished representation #1442: We need to set the sort topredicateSortwhen storing or looking up aPredicate. After Predicate should have a distinguished representation #1442: Predicate sorts will be erased automatically. - Specialize the representation of
\equals.
Appetite: S. TheSideConditionshould contain aHashMapfor looking upTermLikes for substitution. - Combine
SideConditions with normalization.
Appetite: S. CombiningSideConditions (bysappendormappend) should apply the substitutions from each to the other so that the result is normalized.Note: This makes Include the side condition when evaluating functions in the side condition #1416 trivial.