Try the latest master with --sygus-repair-const
-
-
Thanks!
1 reply 0 retweets 1 like -
No worries. I fear I may be the only CVC4 person openly here...
2 replies 0 retweets 2 likes -
From a SMT noob perspective - who happened upon Z3 first and got used to the Python interface, without ever really being 100% convinced that Z3 was specifically better for my purposes - is there a reasonable comparison of strengths and weaknesses of the big SMT systems somewhere?
2 replies 0 retweets 5 likes -
Ummm... that's a bit complicated because there are not only many variables but also many /kinds/ of variable. Do you care about "performance", lots of theories, support, community, etc.?
1 reply 0 retweets 3 likes -
Replying to @ciphernyx @geofflangdale and
My general advice would be to stick ( as much as possible ) to the SMT-LIB standard, set up your architecture so you can swap out solvers then try everything you can and see what works for your application. That will work better than anything I can tweet at you now.
1 reply 0 retweets 7 likes -
Replying to @ciphernyx @geofflangdale and
BUT... SMT-COMP is a reasonable guide to performance, modulo all of the problems with this kind of endeavour. What follows is pure personal opinion; your experience with your application matters more.
1 reply 0 retweets 1 like -
Replying to @ciphernyx @geofflangdale and
In alphabetical order from SMT-COMP 18, let's say something nice about every solver. Alt-Ergo : Interestingly different architecture means they handle quantifiers well compared to some.
1 reply 5 retweets 30 likes -
Replying to @ciphernyx @geofflangdale and
AProVE : Carsten knows when things terminate! This gives a very different viewpoint on integer problems.
1 reply 0 retweets 5 likes -
Replying to @ciphernyx @geofflangdale and
Boolector : THE bitvector solver; *still* the one to beat, although many have tried.
2 replies 0 retweets 3 likes
Yices2 is pretty good on bitvectors plus arrays and/or uninterpreted functions.
9:00 AM - 5 Nov 2018
0 replies
0 retweets
1 like
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.