refactor: the AIG framework to track negations in a more efficient way

[hargoniX]

TODO

[hargoniX]

!bench

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 20571a938baaa3088efdde29ab77f2dea0c26d24 --onto ca0d8226192e7c0cdcc71d6322c3226ad4f73f30. You can force Mathlib CI using the force-mathlib-ci label. (2025-03-07 15:48:05)

[leanprover-bot]

Here are the benchmark results for commit f88c3a2.
There were significant changes against commit 20571a9:

  Benchmark                   Metric                 Change
  =====================================================================
- bv_decide_inequality.lean   branches                19.5%  (3819.5 σ)
- bv_decide_inequality.lean   instructions            23.1%  (3848.1 σ)
- bv_decide_inequality.lean   maxrss                  21.5%   (364.9 σ)
- bv_decide_inequality.lean   task-clock              33.2%   (170.0 σ)
- bv_decide_inequality.lean   wall-clock              33.1%   (324.2 σ)
+ bv_decide_mod               branches                -9.1%  (-720.0 σ)
+ bv_decide_mod               instructions           -10.4%  (-821.1 σ)
+ bv_decide_mod               maxrss                  -2.1%  (-222.0 σ)
+ bv_decide_mod               task-clock             -22.4%   (-15.7 σ)
+ bv_decide_mod               wall-clock             -22.3%   (-15.4 σ)
+ bv_decide_mul               branches               -13.8% (-1039.8 σ)
+ bv_decide_mul               instructions           -15.0% (-1244.2 σ)
+ bv_decide_mul               maxrss                  -6.7% (-1777.0 σ)
- bv_decide_realworld         branches                81.7%  (3874.9 σ)
- bv_decide_realworld         instructions            77.4%  (4549.0 σ)
- bv_decide_realworld         maxrss                  49.5%  (3014.4 σ)
- bv_decide_realworld         task-clock              50.6%    (32.1 σ)
- bv_decide_realworld         wall-clock              49.6%    (19.4 σ)
+ ilean roundtrip             parse                   -3.5%   (-10.4 σ)
+ import Lean                 task-clock              -8.7%   (-83.1 σ)
+ import Lean                 wall-clock              -8.7%   (-74.9 σ)
- liasolver                   task-clock               3.5%    (61.7 σ)
- liasolver                   wall-clock               3.4%    (56.9 σ)
+ omega_stress.lean async     branch-misses           -5.6%   (-13.4 σ)
- stdlib                      instantiate metavars    13.6%    (14.6 σ)
+ workspaceSymbols            task-clock              -4.8%   (-12.0 σ)
+ workspaceSymbols            wall-clock              -4.8%   (-12.0 σ)

[hargoniX]

!bench

[leanprover-bot]

Here are the benchmark results for commit 35dc1d8.
There were significant changes against commit 20571a9:

  Benchmark                   Metric         Change
  =============================================================
+ bv_decide_inequality.lean   branches        -9.4% (-1289.4 σ)
+ bv_decide_inequality.lean   instructions    -9.1%  (-800.1 σ)
- bv_decide_mod               branches        10.2%   (141.4 σ)
- bv_decide_mod               instructions    12.1%   (166.5 σ)
- bv_decide_mod               task-clock      22.7%    (19.1 σ)
- bv_decide_mod               wall-clock      22.6%    (18.2 σ)
+ bv_decide_mul               branches        -4.0%  (-336.7 σ)
+ bv_decide_mul               instructions    -4.8%  (-374.6 σ)
+ bv_decide_mul               maxrss          -1.1%   (-27.1 σ)
- bv_decide_realworld         branches       947.2% (10772.1 σ)
- bv_decide_realworld         instructions   930.2% (14191.7 σ)
- bv_decide_realworld         maxrss         448.8% (24605.6 σ)
- bv_decide_realworld         task-clock     570.7%   (172.6 σ)
- bv_decide_realworld         wall-clock     562.7%   (195.1 σ)
- stdlib                      dsimp            3.7%    (46.0 σ)