Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat: implement ac_nf', an alternative normalizer that takes terms shared across both sides of an equality into account #43

Draft
wants to merge 92 commits into
base: master
Choose a base branch
from
Draft
Show file tree
Hide file tree
Changes from 51 commits
Commits
Show all changes
92 commits
Select commit Hold shift + click to select a range
8b2f332
feat: compute coefficients of an ACExpr
alexkeizer Jan 17, 2025
f30abf7
feat: implement `ac_nf!`, an alternative normalizer that takes terms …
alexkeizer Jan 22, 2025
0996840
test cases
alexkeizer Jan 22, 2025
79013b5
chore: move tests to test file
alexkeizer Jan 23, 2025
2420466
chore: scaling test
alexkeizer Jan 23, 2025
be2b58a
fix typo
alexkeizer Jan 23, 2025
0bef55f
replace List with Range in `getAllVarIndices`
alexkeizer Jan 23, 2025
a3cd091
rollback unneeded changes to AC/main
alexkeizer Jan 23, 2025
14681f3
optimize toExpr
alexkeizer Jan 23, 2025
811ac2a
import `AC.Sharing` in the AC module
alexkeizer Jan 24, 2025
4b87cb0
rename ac_nf! to ac_nf'
alexkeizer Jan 24, 2025
7b01436
code review with Sid
alexkeizer Jan 24, 2025
31f7bd2
fix universe handling
alexkeizer Jan 24, 2025
7f8f636
fix tests to use guard_target
alexkeizer Jan 24, 2025
90c29d0
reduce the number of unneeded calls to ac_nf
alexkeizer Jan 24, 2025
f7a525b
skeleton for neutral element recognition
alexkeizer Jan 24, 2025
52433ec
comments
alexkeizer Jan 24, 2025
550f6a7
remove now-implemented TODO
alexkeizer Jan 24, 2025
d1a3979
refactor: ensure linear modification
alexkeizer Jan 24, 2025
3f101fd
WIP: implement
alexkeizer Jan 24, 2025
1d86485
implement checking for neutrals
alexkeizer Jan 24, 2025
8ae36e8
add comments
alexkeizer Jan 28, 2025
9bc5bbd
comments
alexkeizer Jan 28, 2025
0c6a493
feat: use ac_nf` in bv_decide pass
alexkeizer Jan 28, 2025
50ea152
add note about generalizing to BEq
alexkeizer Jan 28, 2025
077c1e8
reduce repetition amount in scaling test to reduce flakiness
alexkeizer Jan 28, 2025
61344db
add docstring
alexkeizer Jan 28, 2025
5a3bc26
add two more test cases
tobiasgrosser Jan 28, 2025
7c3a693
feat: add support for BEq
luisacicolini Jan 29, 2025
f4f9000
chore: progress
luisacicolini Jan 29, 2025
165022a
chore: working def
luisacicolini Jan 29, 2025
f7772f4
chore: cleaner way to get type
luisacicolini Jan 29, 2025
9cddbfe
chore: clean
luisacicolini Jan 29, 2025
90fe330
chore: examples and cleaning
luisacicolini Jan 29, 2025
3414102
chore: clean code
luisacicolini Jan 29, 2025
99e890a
chore: comment test to fix build
luisacicolini Jan 29, 2025
ed9fae4
chore: formatting
luisacicolini Jan 29, 2025
8428d45
chore: dedup
luisacicolini Jan 29, 2025
294c2bd
chore: add builder
luisacicolini Jan 30, 2025
9f29bed
chore: separate congr, dedup
luisacicolini Jan 30, 2025
e3e5c44
refactor: remove the need for congruence lemmas, by constructing the …
alexkeizer Jan 30, 2025
903fc6e
refactor: remove predBuilder
alexkeizer Jan 30, 2025
5a2b491
feat: move files around to live purely in bv_decide
bollu Jan 31, 2025
de22da2
chore: fix build
bollu Jan 31, 2025
e606725
feat: fix broken test case.
bollu Jan 31, 2025
ac9b22c
feat: improve perf to O(min)
bollu Jan 31, 2025
14a8052
feat: guard multiplication
bollu Jan 31, 2025
91dcd68
chore: newline
bollu Jan 31, 2025
cb4cb1e
chore: fixup tests wrt mul
bollu Jan 31, 2025
39846ba
chore: cleanup
bollu Jan 31, 2025
622900a
chore: refactor to qsort instead of iterating over the whole array
bollu Jan 31, 2025
c1dad96
feat: checkpoint
bollu Feb 4, 2025
11d8ef4
feat: abstract out operation
bollu Feb 4, 2025
e20a5a3
feat: use op
bollu Feb 4, 2025
d7f2079
feat: refactor to use Op that keeps track of multiplication
bollu Feb 4, 2025
94ad1f2
feat: cleanup
bollu Feb 4, 2025
f2cfcdd
rewrite bv_ac_nf docstring to be accurate wrt latest changes to speci…
alexkeizer Feb 11, 2025
a368974
add testcase for now docstring example
alexkeizer Feb 11, 2025
e660840
fix: properly search for *applications* of a bitvector Op in `Op.ofApp?`
alexkeizer Feb 11, 2025
edb8287
chore: delete example whose 'sorry' was causing build to fail
bollu Feb 13, 2025
f6f64fa
chore: add bollu to author list
bollu Feb 13, 2025
453a428
feat: fixup tests
bollu Feb 13, 2025
d74c9fa
feat: fixup test case of the BV rewriter
bollu Feb 14, 2025
c65ebf1
Merge remote-tracking branch 'origin/master' into ac-rfl-term-sharing
bollu Feb 14, 2025
93d8987
revert changes to bv_ac_nf example
alexkeizer Feb 14, 2025
7cefba3
refactor: rename test file to emphasize relation to bv_decide
alexkeizer Feb 14, 2025
129d18b
refactor: rename ofApp? -> ofApp2?
alexkeizer Feb 14, 2025
061f2e7
refactor: move `bv_ac_nf` tactic to test file
alexkeizer Feb 14, 2025
468fc4e
remove flawed test
alexkeizer Feb 14, 2025
79bce4e
add bv_normalize integration tests
alexkeizer Feb 14, 2025
0058b8c
extra documentation
alexkeizer Feb 14, 2025
84ba5c2
refactor: better linear modification in exprToVar
alexkeizer Feb 14, 2025
f60887f
golf in SharedCoefficients.compute
alexkeizer Feb 14, 2025
f18aa99
remove debugging trace
alexkeizer Feb 14, 2025
ce546db
refactor exprToVar to be obviously linear
alexkeizer Feb 14, 2025
2be4aca
remove unneeded Grind import
alexkeizer Feb 14, 2025
8aaeb58
Apply suggestions from code review
alexkeizer Feb 14, 2025
fbb0804
Apply suggestions from code review
alexkeizer Feb 14, 2025
0c2e8f9
copyright year
alexkeizer Feb 14, 2025
d89d891
refactor `ofExpr?`
alexkeizer Feb 14, 2025
e67e708
refactor: reconstruct HMul instance
alexkeizer Feb 14, 2025
9780397
refactor: mkBitVecLit helper
alexkeizer Feb 14, 2025
69cc122
chore: indentation in computeCoefficients
alexkeizer Feb 14, 2025
fc284d1
chore: wrap too-long line
alexkeizer Feb 14, 2025
20988c9
refactor: remove isDefEq check
alexkeizer Feb 14, 2025
2ad8b1c
chore: close namespace
alexkeizer Feb 14, 2025
3ad78ab
refactor: remove match for Eq
alexkeizer Feb 14, 2025
799d60e
refactor: replace match_expr with match
alexkeizer Feb 14, 2025
b886439
update canonicalizeWithSharing docstring
alexkeizer Feb 14, 2025
b141f32
rename `post` to `bvAcNfpost`
alexkeizer Feb 14, 2025
71b38d5
revert match_expr -> match change
alexkeizer Feb 14, 2025
4219d75
feat: also match against Eq
bollu Feb 17, 2025
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Loading
Loading