Skip to content

WIP - Implement Generalizer #1022

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.

Sign up for GitHub

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

Draft
wants to merge 51 commits into
base: main
Choose a base branch
from
+1,179 −0
Draft

WIP - Implement Generalizer #1022

Changes from all commits
Commits
Show all changes
51 commits
Select commit Hold shift + click to select a range
ac644d4
Set up function
oluwatimilehin Mar 10, 2025
19854fd
Undo experimentation code
oluwatimilehin Mar 10, 2025
e677cf9
Move to separate file, return unit
oluwatimilehin Mar 14, 2025
ce1d306
Remove unused imports
oluwatimilehin Mar 14, 2025
aeb8a19
Clean up
oluwatimilehin Mar 14, 2025
ba4a4b2
Remove unused imports and change return type
oluwatimilehin Mar 15, 2025
ce9e029
Skeleton exists/foralll
oluwatimilehin Mar 17, 2025
1721d8e
Revert whitespace changes
oluwatimilehin Mar 17, 2025
8944c4d
Reconstruct counterexamples
oluwatimilehin Mar 24, 2025
a76bc9a
Cleanup exists/for-all impl
oluwatimilehin Mar 29, 2025
255e14e
Exists/For-all valid(?) impl
oluwatimilehin Mar 30, 2025
93948ed
cleanup
oluwatimilehin Mar 31, 2025
24b944e
Undo whitespace changes 1
oluwatimilehin Mar 31, 2025
fff4102
Add whitespace
oluwatimilehin Mar 31, 2025
7c9f338
Add whitespace (3)
oluwatimilehin Mar 31, 2025
486d1af
Restore newline
oluwatimilehin Mar 31, 2025
e0e97ad
Add more examples, document examples
oluwatimilehin Mar 31, 2025
56874d2
Remove exists-for-all config
oluwatimilehin Mar 31, 2025
47493ff
Set up inductive synthesis
oluwatimilehin Mar 31, 2025
5cedec0
whitespace
oluwatimilehin Mar 31, 2025
f780799
Basic inductive synthesis
oluwatimilehin Mar 31, 2025
a4fbb39
Refactor
oluwatimilehin Apr 1, 2025
c4386cc
Implement enumerative synthesis
oluwatimilehin Apr 1, 2025
98aef44
inductive_synthesis => expression_synthesis
oluwatimilehin Apr 1, 2025
9dda0c2
Support subtraction (with caveats)
oluwatimilehin Apr 1, 2025
8c367bd
Document subtraction bug
oluwatimilehin Apr 1, 2025
de2ada3
Refactor expression synthesis test
oluwatimilehin Apr 1, 2025
d67ae3a
Implement getting negative examples
oluwatimilehin Apr 2, 2025
e4f1a90
clean up subtraction bug; set up precondition synthesis
oluwatimilehin Apr 4, 2025
480b8d5
Precondition synthesis impl
oluwatimilehin Apr 4, 2025
cfb5f01
Set up conversion to BVExpr
oluwatimilehin Apr 8, 2025
2a36479
Match most patterns
oluwatimilehin Apr 9, 2025
0f58fef
Set up conversion to BVExpr
oluwatimilehin Apr 9, 2025
92e45ef
Set up to use state monad
oluwatimilehin Apr 9, 2025
c329818
Wrap in state monad
oluwatimilehin Apr 9, 2025
6efd99f
Implement reduce width command
oluwatimilehin Apr 9, 2025
32a0942
Print state in results
oluwatimilehin Apr 10, 2025
ecd5c38
Rename variables; cleanup reduce width
oluwatimilehin Apr 10, 2025
81e4037
End-to-end wiring; incorporate precondition synthesis
oluwatimilehin Apr 11, 2025
01c0698
Basic precondition synthesis works
oluwatimilehin Apr 11, 2025
b88a6df
Add new example
oluwatimilehin Apr 12, 2025
17ee985
Add new failing examples
oluwatimilehin Apr 15, 2025
7d07acf
Rewrite inductive synthesis to not use solver and prevent runaway cha…
oluwatimilehin Apr 16, 2025
605b319
Uncomment examples
oluwatimilehin Apr 17, 2025
1440929
Rank & combine preconditions; perform inductive synthesis on original…
oluwatimilehin Apr 23, 2025
ef88437
Add tests for model count
oluwatimilehin Apr 23, 2025
4c4b017
Iterate over a set of BVLogicalExprs
oluwatimilehin Apr 23, 2025
b709538
Fix combining logic to use option
oluwatimilehin Apr 23, 2025
61620a3
Cleanup: replace io_synthesis and reducewidth tactics with commands
oluwatimilehin Apr 24, 2025
ed90d62
Use signextend in evalBVExpr; fix enumerative synthesis sketch example
oluwatimilehin Apr 24, 2025
a20dc4d
Fix enumerative synthesis sketching logic
oluwatimilehin Apr 24, 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