Skip to content

Adding Monomorphisation procedure to Zipperposition #101

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

Jump to bottom
Open
nartannt wants to merge 132 commits into
base: master
Choose a base branch
from
Open

Adding Monomorphisation procedure to Zipperposition #101

nartannt wants to merge 132 commits into from

Conversation

@nartannt
Copy link
Contributor

@nartannt nartannt commented Dec 11, 2025

Hi,
I have implemented the iterative monomorphisation procedure described here in a fork of Zipperposition, it allows for significant performance gains on polymorphic problems. It seems worthwhile to import it to the main Zipperposition repository.

As it stands, the code has the following issues:

  • the formatting is not compatible with the current code of the main repository, I have been unable to replicate that formatting style
  • I am unsure that the code quality and style are up to par with that of the main repository
  • There are some modifications of the codebase outside the scope of the Monomorphisation.ml file particularly in the eprover.ml file

nartannt and others added 30 commits October 6, 2023 11:08
@nartannt
fixed a couple of bugs and added flakes
a0058bf
@nartannt
added test-cached to the .gitignore
f3731f5
@nartannt
added small bash script for rough benchmarking as well as the file wh…
abedd6c 
…ere the monomorphisation magic will happen
@nartannt
added some auxiliary functions
85b004f
@nartannt
added missing labels to functions in order to get rid of warnings
baf4f42
@nartannt
some work on auxilliary functions
1ef7084
@nartannt
began type unification, when one type is monomorphic
04610cd
@nartannt
improved flake
477ab38
@nartannt
implementation of the monomorphisation algorithm, has not been tested
5cbdaa8
@nartannt
finished monomorphisation implementation and started interfacing it w…
be987e0 
…ith the rest of the prover
@nartannt
attempted finalising monomorphisation integration, many things are vi…
ff7e611 
…sibly not working, require debugging and fixing
@nartannt
attempting to fix integration of monomorphisation and debugging monom…
5a49ab0 
…orphisation
@nartannt
added portfolio/tmp to the .gitignore
24c2355
@nartannt
fixing monomorphisation, still needs some work, but progress was made
56ae7c5
@nartannt
continued debugging the monomorphisation implementation, making progress
2a2cd43
@nartannt
spotted potential unecessary loop
a5abfea
@loutr
fix: working nix flake, both for building and development
fd90f43
@nartannt
Merge pull request #1 from loutr/master
c2fa89b 
Working nix flake, both for building and development
@nartannt
continuing work on monomorphisation
8a27eb8
@nartannt
kind of restarting implementation, this time taking scoping into acco…
88652ff 
…unt properly
@nartannt
progress on the newer implementation
85f4881
@nartannt
finished initial implementation of reworked monomorphisation, compile…
4b90192 
…s, has not been tested or debugged
@nartannt
started debugging, made some progress still a lot of work to do
eb1caca
@nartannt
flake.lock
8356814
@nartannt
debugging monomorphisation, seems to work, now needs to be tested
035d6d9
@nartannt
started adding bounds
62ef382
@nartannt
adding bounds in a very hacky way
636d4a7
@nartannt
a couple of helpful commands
e53bdcd
@nartannt
attempted a more efficient implementation, now completely disfunctional
f5bf6cd
@nartannt
more debugging
6222916
nartannt added 30 commits February 8, 2024 12:59
@nartannt
more minor cleaning up changes
e578adb
@nartannt
cleaning up code
f0f9d08
@nartannt
finishing the cleaning phase and adding a timeout for monomorphisation
f11ab12
@nartannt
fixing some performance issues
57d52a2
@nartannt
i'll be honest, not entirely sure what i changed
162c48a
@nartannt
finishing renaming thing that was leftover
c529f7f
@nartannt
removed useless type arguments
d0d3820
@nartannt
need to test current version with interesting bounds
c61c10a
@nartannt
adapting run_zipp
6d178af
@nartannt
turned bounds into options
a9c67f7
@nartannt
option modification taken into account in options
2ea8c34
@nartannt
wipping things into shape
1c1481a
@nartannt
AAAAAAAAAAAAAAHHHHRRRG
306ed6c
@nartannt
probably fully working monomorphisation maybe some soundness bug, har…
acce990 
…d to be sure
@nartannt
more updates
f58d6ea
@nartannt
commit of monomorphisation step for 17-06
f90397b
@nartannt
fixing more bugs
8f698d8
@nartannt
Revert "fixing more bugs"
f7c5dcd 
This reverts commit 8f698d8.
@nartannt
removed poly_test
2028d6c
@nartannt
cleaning up files that don't belong
699b3a7
@nartannt
restored main.yml
59a90e0
@nartannt
git ignore
6bc03c4
@nartannt
reverting back to initial formatting style
e2c2c77
@nartannt
adjusting formatting
8700115
@nartannt
giving up on formatting
dd52060
@nartannt
returned file to its initial location
315d2d0
@nartannt
renamed file
a5e4ef1
@nartannt
some cleaning up
d9be903
@nartannt
more cleaning up
931f722
@nartannt
ready to start pull request I believe
8c6b410
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

No reviews

Assignees

No one assigned

Labels

None yet

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

2 participants

@nartannt @loutr