Open bvssvni opened 3 years ago
Currently, every equivalence found under automated theorem proving is added to a BinaryHeap.
BinaryHeap
Every traversed equivalence is added to a HashSet. This could be replaced by a Cuckoo filter, by choosing a sufficient low positive false rate.
HashSet
It is much harder to find a replacement of BinaryHeap. However, the overall idea is to compress the memory.
Currently, every equivalence found under automated theorem proving is added to a
BinaryHeap.Every traversed equivalence is added to a
HashSet. This could be replaced by a Cuckoo filter, by choosing a sufficient low positive false rate.It is much harder to find a replacement of
BinaryHeap. However, the overall idea is to compress the memory.