Caching of ordering status

[petarvukmirovic]

Like in E

[c-cube]

should have a lazy bitvector in Clause.t (depends on ordering, so can't be in Lit.t)

[petarvukmirovic]

@c-cube : in the branch cached_maxlits I implemented this.

However, there is a strange behaviour with lazy BV.t. Namely, it gets reset after being cached and being used for the second time. For that reason, I cached it to list and then when I want to use it I convert it to BV.t.

Is there something I should know about BV.t?

[c-cube]

Be careful that bit vectors are mutable, like arrays. You could use an option instead to implement the lazy semantics yourself (and never mutate it afterwards). Also be sure to copy if needed. -- Sent from my Android device with K-9 Mail. Please excuse my brevity.

[c-cube]

side note: orderings typically have their own cache, so if you compute s <? t repeatedly it's very likely that only the first time will be expensive.