search

vprover / vampire

The Vampire Theorem Prover
https://vprover.github.io/
Other
295 stars 51 forks source link

actually remove `_id` from Term, fix goof with TERM_DIST_VAR_UNKNOWN #514

Closed MichaelRawson closed 10 months ago

MichaelRawson commented 10 months ago

In #337 there was two separate mishaps.

  1. @quickbeam123 realised that _id could be moved from Term itself to its "info" TermList, but I failed to actually remove it from Term so there's been some waste bytes knocking around in Term. Aside: we might actually want to move it back if we can fit more useful stuff into the 32 bits in TermList.
  2. I meant to actually compute (2^21) - 1 to work out the maximum value of TERM_DIST_VAR_UNKNOWN, but instead wrote it down literally - where the ^ is interpreted as XOR. This means that since then TERM_DIST_VAR_UNKNOWN has been ...22. :facepalm:
quickbeam123 commented 10 months ago

Let's be the tough guys and just fix the expression (proposal incoming), what do you think?

By the way, isn't it suspicious we didn't see this crashing in any way? (Or could some heuristics have been broken?)

Otherwise, nice!

MichaelRawson commented 10 months ago

Let's be the tough guys and just fix the expression (proposal incoming), what do you think?

Good idea! I even checked the compiler output this time, just to be extra-safe.

#define TERM_DIST_VAR_UNKNOWN (1 << 21)-1

...better, but could it even be

#define TERM_DIST_VAR_UNKNOWN (1 << TERM_DIST_VAR_BITS) - 1

?

quickbeam123 commented 10 months ago

Yes, and between parentheses. Just fixed and force-pushed.