SMTInterpol : the best interpolant generator by far and amazing performance for a Java solver.
-
-
Replying to @ciphernyx @geofflangdale and
SMTRAT : flying the flag for computer algebra and doing some seriously interesting things with cylindrical algebraic decomposition.
1 reply 0 retweets 3 likes -
Replying to @ciphernyx @geofflangdale and
STP : Another solver that has dodged death, like MathSAT, still crazy competitive where others would have lagged.
1 reply 0 retweets 3 likes -
Replying to @ciphernyx @geofflangdale and
SPASS : Not a native SMT solver but welcome anyway, especially given what they can teach us about integer problems.
1 reply 0 retweets 4 likes -
Replying to @ciphernyx @geofflangdale and
Vampire : fresh from their decade long dominance of the TPTP contest, a new challenge appears!
1 reply 0 retweets 5 likes -
Replying to @ciphernyx @geofflangdale and
veriT : everyone said generating proofs from a compact and competitive solver was impossible, veriT proves (ha ha) they are wrong.
1 reply 0 retweets 4 likes -
Replying to @ciphernyx @geofflangdale and
Yices : ever thought of a great idea, implemented it and then found you still couldn't beat another solver because they thought of it first? It was Yices that thought of it first.
1 reply 0 retweets 5 likes -
Replying to @ciphernyx @geofflangdale and
Z3 : the most famous and widely used solver because of it's robust performance and speedy support.
1 reply 0 retweets 4 likes -
Replying to @ciphernyx @geofflangdale and
All gratuitously my opinion, YMMV, hope that helps.
2 replies 0 retweets 4 likes -
Thanks so much! I've looked at SMTCOMP results before but still been a bit lost. Good advice on sticking to smtlib format - I was lazy and the Python interface was tempting. But I've seen most of my workload turn to bitvector stuff so CVC4, Boolector and Yices seem worth trying.
4 replies 0 retweets 5 likes
For CVC4 with bitvectors you will probably need to tweak it a bit for reasonable performance. For non-incremental problems I'd recommend --bitblast=eager --bv-sat-solver=cadical. (But I'm sure @ciphernyx can give more detailed hints. :)
-
-
Cadical is a good shout, eager YMMV depending on how heavy the bit vectors are and how much Boolean structure the problem has.
0 replies 0 retweets 1 likeThanks. Twitter will use this to make your timeline better. UndoUndo
-
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.