Andrew V. Teylu
Andrew V. Teylu
> cnf_short.h is the only missing one, and it just seems to be a subset of cnf.h. Agreed! Too many race conditions on this issue 😂
@rgov take a look at https://github.com/stp/stp/pull/376
Haha, wow, so it looks like me, you and Mate have all pretty much done the same work! Links for reference: - https://github.com/stp/stp/commit/0d67a153384030bb014230b5320e1a3b14d60fe6 (Trevor's attempt) - https://github.com/stp/stp/commit/1e8ebd4ce2ee911cb98c048e56a04564eb3de60c (Mate's attempt) -...
Given we use submodules for other stuff in STP, I guess it would be reasonable to have a submodule for this (and maybe Bit-Vector) in a `ext-lib` folder (top-level, like...
@msoos what are your thoughts on the size of libabc.a? Is this an issue to you? I’m fine with this being like CMS (i.e., not a submodule): you build it...
Okay, I will move forward with this. I’ll get this wrapped-up and get ABC pulled down as part of CI. I also want to open-up some PRs against ABC to...
@TrevorHansen shall I attempt to get it working then we can try and assess performance? On that line: do we have a good way to easily measure if anything has...
To save people clicking through: KLEE is currently on 3.5, I don't think that STP's CMake should "outpace" KLEE unless we have a really good reason to.
As an FYI: cvc5 implements this with binary search on the optimisation terms
Ah, an optimise each term in the order that they're listed in the .smt2 input? So for `x + y == 10`, if `x` comes first, you get `x=10` and...