Tobias Grosser 7c62881a95 feat: bv_decide short-circuit a * x = b * x (#6496) ... This PR adds short-circuit support to bv_decide to accelerate multiplications with shared coefficients. In particular, `a * x = b * x` can be extended to `a = b v (a * x = b * x)`. The latter is faster if `a = b` is true, as `a = b` may be evaluated without considering the multiplication circuit. On the other hand, we require the multiplication circuit, as `a * x = b * x -> a = b` is not always true due to two's complement wrapping. We support multiplications through acNF, which takes into account shared terms across equality canonicalizing `a * (b * c1) = a * (b * c2)` to `(a * b) * c1 = (a * b) * c2`. As a result, the non-shared terms are lifted to the top such that canonical rewrites for binary multiplication with shared terms on the left/right are sufficient. We add an option `bv_decide +shortCircuit` which controls this feature (currently disabled by default). --------- Co-authored-by: Siddharth Bhat <siddu.druid@gmail.com> Co-authored-by: Henrik Böving <hargonix@gmail.com>		2025-03-20 19:51:53 +00:00
..
Deriving	feat: allow cond to be used in proofs (#7141)	2025-03-04 12:10:29 +00:00
InfoTree	feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457)	2025-03-13 15:09:00 +00:00
PreDefinition	feat: well-founded recursion: opaque well-foundedness proofs (#5182)	2025-03-19 09:21:04 +00:00
Quotation
Tactic	feat: bv_decide short-circuit a * x = b * x (#6496)	2025-03-20 19:51:53 +00:00
App.lean	fix: move auxDeclToFullName to LocalContext to fix name (un)resolution (#7075)	2025-03-03 16:10:54 +00:00
Arg.lean	chore: rename Array.back to back! (#5897)	2024-10-31 09:18:18 +00:00
Attributes.lean
AutoBound.lean
AuxDef.lean
BinderPredicates.lean
Binders.lean	feat: enable Elab.async by default (#7485)	2025-03-15 07:24:52 +00:00
BindersUtil.lean
BuiltinCommand.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
BuiltinEvalCommand.lean	chore: remove unused deriving handler argument syntax (#5265)	2024-11-01 22:41:38 +00:00
BuiltinNotation.lean	feat: debug_assert! (#7256)	2025-03-03 16:34:44 +00:00
BuiltinTerm.lean	feat: use new structInstFields parser to tag structure instance fields	2024-11-19 09:26:58 +01:00
Calc.lean	chore: add missing diff-exposing in type/value mismatch errors (#6484)	2024-12-31 17:47:12 +00:00
CheckTactic.lean	chore: add missing diff-exposing in type/value mismatch errors (#6484)	2024-12-31 17:47:12 +00:00
Command.lean	feat: elaborate theorem bodies in parallel (#7084)	2025-03-14 07:50:42 +00:00
ComputedFields.lean
Config.lean
Declaration.lean	feat: inlay hints for auto-implicits (#6768)	2025-02-04 17:36:49 +00:00
DeclarationRange.lean	feat: inlay hints for auto-implicits (#6768)	2025-02-04 17:36:49 +00:00
DeclModifiers.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
DeclNameGen.lean
DeclUtil.lean
DefView.lean	fix: cancel computations within command elaboration as soon as reuse is ruled out (#7241)	2025-03-03 10:37:10 +00:00
Deriving.lean	feat: upstream ToExpr deriving handler from Mathlib (#6473)	2024-12-31 15:11:53 +00:00
Do.lean	feat: debug_assert! (#7256)	2025-03-03 16:34:44 +00:00
ElabRules.lean
Eval.lean
Exception.lean
Extra.lean	refactor: elaborate forIn notation without extra let (#6977)	2025-02-08 10:32:34 +00:00
Frontend.lean	feat: enable Elab.async by default (#7485)	2025-03-15 07:24:52 +00:00
GenInjective.lean
GuardMsgs.lean	feat: 'unsolved goals' & 'goals accomplished' diagnostics (#7366)	2025-03-07 13:50:56 +00:00
Import.lean	feat: frontend & server support for plugins (#6893)	2025-02-04 23:36:18 +00:00
Inductive.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
InfoTree.lean
InfoTrees.lean	feat: allow async elab tasks to contribute to info trees reported to linters and request handlers (#7457)	2025-03-13 15:09:00 +00:00
InheritDoc.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
LetRec.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
Level.lean	chore: rename Array.back to back! (#5897)	2024-10-31 09:18:18 +00:00
Macro.lean
MacroArgUtil.lean
MacroRules.lean
Match.lean	feat: allow anonymous equality proofs in match expressions (#6853)	2025-02-04 16:09:21 +00:00
MatchAltView.lean
MatchExpr.lean
Mixfix.lean
MutualDef.lean	perf: async optimizations for Init.Data.BitVec.Lemmas (#7546)	2025-03-18 12:56:16 +00:00
MutualInductive.lean	fix: never transfer constants from checked environment into elab branches (#7306)	2025-03-05 17:12:27 +00:00
Notation.lean	chore: use Array.findFinIdx? where it is better than findIdx? (#6184)	2024-11-23 07:22:31 +00:00
Open.lean	chore: avoid runtime array bounds checks (#6134)	2024-11-21 05:04:52 +00:00
ParseImportsFast.lean	feat: align take/drop/extract across List/Array/Vector (#6860)	2025-01-30 01:24:25 +00:00
PatternVar.lean	fix: propagate Simp.Config when reducing terms and checking definitional equality in simp (#6123)	2024-12-14 00:59:40 +00:00
PreDefinition.lean
Print.lean	chore: in #print for structures, mention 'field notation' (#6406)	2024-12-17 02:21:03 +00:00
Quotation.lean	feat: align lemmas about List.getLast(!?) with Array/Vector.back(!?) (#7205)	2025-02-24 11:48:43 +00:00
RecAppSyntax.lean
RecommendedSpelling.lean	feat: recommended_spelling command (#6869)	2025-02-03 11:15:52 +00:00
SetOption.lean
StructInst.lean	perf: Environment blocker removals from async-proofs branch (#7483)	2025-03-14 13:37:01 +00:00
Structure.lean	feat: language reference links and examples in docstrings (#7240)	2025-03-12 09:17:27 +00:00
Syntax.lean	chore: avoid runtime array bounds checks (#6134)	2024-11-21 05:04:52 +00:00
SyntheticMVars.lean	chore: avoid runtime array bounds checks (#6134)	2024-11-21 05:04:52 +00:00
Tactic.lean	chore: remove save tactic (#7047)	2025-02-12 09:19:30 +00:00
Term.lean	perf: Environment blocker removals from async-proofs branch (#7483)	2025-03-14 13:37:01 +00:00
Time.lean
Util.lean	fix: convert kernel interrupt into elab interrupt (#6988)	2025-02-07 15:55:32 +00:00