feat: `Std.Sat.AIG` #4953

hargoniX · 2024-08-08T07:52:43Z

Step 2/~7 in upstreaming LeanSAT.

tobiasgrosser

Very nicely prepared patch and a big step forward. 🥳 I left some stylistic comments.

src/Std/Sat/AIG/Basic.lean

src/Std/Sat/AIG/CNF.lean

src/Std/Sat/AIG/RefStreamOperator/Map.lean

src/Std/Sat/AIG/RelabelNat.lean

leanprover-community-mathlib4-bot · 2024-08-08T08:48:18Z

Mathlib CI status (docs):

❗ Batteries CI can not be attempted yet, as the nightly-testing-2024-08-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Batteries CI should run now. (2024-08-08 08:48:17)
❗ Mathlib CI can not be attempted yet, as the nightly-testing-2024-08-08 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. (2024-08-08 15:15:25)
💥 Mathlib branch lean-pr-testing-4953 build failed against this PR. (2024-08-09 14:01:16) View Log
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30a52b794a39256361050c52fe0e41bbff91bc8d --onto dd6ed124baef64a26ef5860f49597fdcef371239. (2024-08-09 20:00:27)
❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 30a52b794a39256361050c52fe0e41bbff91bc8d --onto 5f31e938c1bf5bb2d6d2d29b26ea932ade115357. (2024-08-12 07:46:39)

bollu

Thanks for the super clean implementation! I've read upon CNF.lean, and will get to the others in a bit.

src/Std/Sat/AIG/Basic.lean

src/Std/Sat/AIG/CNF.lean

src/Std/Sat/AIG/Basic.lean

src/Std/Sat/AIG/If.lean

src/Std/Sat/AIG/Basic.lean

src/Std/Sat/AIG/LawfulStreamOperator.lean

src/Std/Sat/AIG/Lemmas.lean

Co-authored-by: Tobias Grosser <[email protected]>

Co-authored-by: Siddharth <[email protected]>

Co-authored-by: Markus Himmel <[email protected]>

src/Std/Sat/AIG/LawfulOperator.lean

kim-em · 2024-08-12T01:59:57Z

❤️

Co-authored-by: Kim Morrison <[email protected]>

TwoFX

We could probably spend more time nitpicking here and there but I don't think there is much point, so let's get this merged after these final remarks.

src/Std/Sat/AIG/LawfulOperator.lean

src/Std/Sat/AIG/Basic.lean

TwoFX · 2024-08-12T12:48:11Z

src/Std/Sat/AIG/CachedGates.lean

+    {
+      lhs := {
+        ref := constRef
+        inv := false
+      }
+      rhs := {
+        ref := gate.cast <| by
+          intros
+          apply LawfulOperator.le_size_of_le_aig_size (f := mkConstCached)
+          omega
+        inv := true
+      }
+    }


I think there is no clear consensus in the existing Lean codebase at the moment (including mixing different styles within the same style), so I think in the interest of making progress I suggest leaving things as you have them now and not losing too much time on this as long as they adhere to one of these styles. However, neither style should have an opening brace on its own line (so this is not okay), and within a declaration you should stick to one style (so this is not okay).

hargoniX requested review from TwoFX and digama0 as code owners August 8, 2024 07:52

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 08:01 Inactive

github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 8, 2024

tobiasgrosser reviewed Aug 8, 2024

View reviewed changes

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 08:43 Inactive

bollu reviewed Aug 8, 2024

View reviewed changes

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 14:28 Inactive

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 14:37 Inactive

TwoFX reviewed Aug 8, 2024

View reviewed changes

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 15:08 Inactive

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 15:38 Inactive

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 8, 2024 15:54 Inactive

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 9, 2024 12:59 Inactive

leanprover-community-mathlib4-bot added a commit to leanprover-community/batteries that referenced this pull request Aug 9, 2024

Update lean-toolchain for testing leanprover/lean4#4953

187daf7

leanprover-community-mathlib4-bot added a commit to leanprover-community/mathlib4 that referenced this pull request Aug 9, 2024

Update lean-toolchain for testing leanprover/lean4#4953

9e172f5

leanprover-community-mathlib4-bot added breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan release-ci Enable all CI checks for a PR, like is done for releases labels Aug 9, 2024

hargoniX and others added 11 commits August 9, 2024 16:50

feat: Array.getElem_of_mem

454dd66

feat: Std.Sat.AIG

7d73b71

Apply suggestions from code review

1053932

Co-authored-by: Tobias Grosser <[email protected]>

Apply suggestions from code review

265f98d

Apply suggestions from code review

76624f7

Co-authored-by: Siddharth <[email protected]>

apply suggestions from code review

138748a

simp normal form

be6d87f

Update src/Std/Sat/AIG/Basic.lean

d3644c8

Co-authored-by: Markus Himmel <[email protected]>

Update src/Std/Sat/AIG/Basic.lean

02871d5

Co-authored-by: Markus Himmel <[email protected]>

address feedback

c374f41

doc: docstrings in AIG.Basic

85b50f7

kim-em reviewed Aug 12, 2024

View reviewed changes

src/Std/Sat/AIG/LawfulOperator.lean Outdated Show resolved Hide resolved

kim-em added awaiting-author Waiting for PR author to address issues and removed awaiting-review Waiting for someone to review the PR labels Aug 12, 2024

hargoniX and others added 4 commits August 12, 2024 09:12

Apply suggestions from code review

f01a446

Co-authored-by: Kim Morrison <[email protected]>

Apply suggestions from code review

80b3764

Co-authored-by: Kim Morrison <[email protected]>

chore: AIG.inv -> AIG.invariant

758c0c6

chore: RefStream -> RefVec

7d1e2fe

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 12, 2024 07:47 Inactive

Further stylistic review fixes

1379a61

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 12, 2024 08:17 Inactive

hargoniX added 2 commits August 12, 2024 10:20

doc: strings for bundle structures

4c8b10b

chore: more stream -> vec

624c7dc

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 12, 2024 08:33 Inactive

hargoniX added 2 commits August 12, 2024 10:41

doc: AIG style

c84492f

doc: Cache

ea5b735

hargoniX added awaiting-review Waiting for someone to review the PR and removed awaiting-author Waiting for PR author to address issues labels Aug 12, 2024

hargoniX requested a review from kim-em August 12, 2024 08:46

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 12, 2024 08:50 Inactive

TwoFX approved these changes Aug 12, 2024

View reviewed changes

naming: fix IsPrefix in theorem names

edd41db

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 12, 2024 14:04 Inactive

style: format structure literals

a895d21

hargoniX added will-merge-soon …unless someone speaks up and removed awaiting-review Waiting for someone to review the PR labels Aug 12, 2024

github-actions bot temporarily deployed to lean-lang.org/lean4/doc August 12, 2024 14:42 Inactive

hargoniX added this pull request to the merge queue Aug 12, 2024

Merged via the queue into master with commit dc3eccd Aug 12, 2024
16 checks passed

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

feat: `Std.Sat.AIG` #4953

feat: `Std.Sat.AIG` #4953

hargoniX commented Aug 8, 2024

tobiasgrosser left a comment

leanprover-community-mathlib4-bot commented Aug 8, 2024 •

edited

Loading

bollu left a comment

kim-em commented Aug 12, 2024

TwoFX left a comment

TwoFX Aug 12, 2024

feat: Std.Sat.AIG #4953

feat: Std.Sat.AIG #4953

Conversation

hargoniX commented Aug 8, 2024

tobiasgrosser left a comment

Choose a reason for hiding this comment

leanprover-community-mathlib4-bot commented Aug 8, 2024 • edited Loading

bollu left a comment

Choose a reason for hiding this comment

kim-em commented Aug 12, 2024

TwoFX left a comment

Choose a reason for hiding this comment

TwoFX Aug 12, 2024

Choose a reason for hiding this comment

feat: `Std.Sat.AIG` #4953

feat: `Std.Sat.AIG` #4953

leanprover-community-mathlib4-bot commented Aug 8, 2024 •

edited

Loading