search

sarsko / CreuSAT

CreuSAT - A formally verified SAT solver written in Rust and verified with Creusot.
MIT License
614 stars 12 forks source link

Use bump / arena allocator #16

Open xldenis opened 2 years ago

xldenis commented 2 years ago

I wonder how much time could be gained by having all formula data stored using arenas. We should investigate using bumpalo for this.

sarsko commented 2 years ago

Agreed. I see the gain from something like bumpalo much more than I do for smallvec. Still not a fan of additional dependencies, but I think it is worth experimentation at least.

xldenis commented 2 years ago

Still not a fan of additional dependencies, but I think it is worth experimentation at least.

While I appreciate the care, and I think it's a good idea, I don't think you should rule out all dependencies. Especially since I think JH and I might do a proof of a bumpalo arena in RHB sometime soon-ish, it's a fun type with a rather elegant model.