Commit 2020-06-24 10:22 dd9b5c68

refactor(tactic/linarith): big refactor and docs (#3113) This PR:

• Splits linarith into multiple files for organizational purposes
• Uses the general zify and cancel_denom tactics instead of weaker custom versions
• Refactors many components of linarith, in particular,
• Modularizes linarith preprocessing, so that users can insert custom steps
• Implements nlinarith preprocessing as such a custom step, so it happens at the correct point of the preprocessing stage
• Better encapsulates the FM elimination module, to make it easier to plug in alternate oracles if/when they exist
• Docs, docs, docs The change to zification means that some goals which involved multiplication of natural numbers will no longer be solved. However, others are now in scope. nlinarith is a possible drop-in replacement; otherwise, generalize the product of naturals to a single natural, and linarith should still succeed.