Commit 2020-06-18 21:08 73caeaa5

perf(tactic/linarith): implement redundancy test to reduce number of comparisons (#3079) This implements a redundancy check in linarith which can drastically reduce the size of the sets of comparisons that the tactic needs to deal with. linarith iteratively transforms sets of inequalities to equisatisfiable sets by eliminating a single variable. If there are n comparisons in the set, we expect O(n^2) comparisons after one elimination step. Many of these comparisons are redundant, i.e. removing them from the set does not change its satisfiability. Deciding redundancy is expensive, but there are cheap approximations that are very useful in practice. This PR tests comparisons for non-minimal history (http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.51.493&rep=rep1&type=pdf p.13, theorem 7). Non-minimal history implies redundancy.