Sarek Høverstad Skotåm

Thanks! I agree that adding an API (and perhaps getting it published on crates.io) would be nice. I'll probably not be able to prioritize it immediately (even though it should...

> Also I read the dissertation in the repo. I was surprised at how long it was and wasn't sure I would finish. I read it completely! As someone with...

Agreed. It should be noted that all runtime checks are not equal. The worst kind (which currently occur in a couple of places) are the ones that return an `Err`...

Hmm I don't see what problem would be solved by using `smallvec`. Also in general not a fan of using external crates as I feel the trust/gain tradeoff is usually...

> > Hmm I don't see what problem would be solved by using smallvec. > > It will store the data inline under a certain size rather than performing a...

> > I think the good design is to have the clause db be a 1d vec with manual handling of clauses as a header and lits. > > This...

> If we just add a ClauseDB but keep the same layout then we get soemthing like this instead: It seems like we might be talking past each other. ClauseDB...

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...

> I actually would love this feature as well, I'm writing a library for the development and prototyping of formal verification algorithms in rust and I'd love to have this...

Yeah, I realized after creating the issue that I already did the correct thing in the implementation of [Node](https://github.com/sarsko/CreuSAT/blob/master/CreuSAT/src/decision.rs#L18-L32) in the VMTF implementation. Tbh, both the `ensures` and the `is_default`...