✧✦Catherine✦✧
hot take: SMT-LIB is designed by incompetent people for the sole purpose of having a dick measuring contest
for any real purpose it's unusable. anyone who is seriously using SMT-LIB has to build at least two wrappers around it, sometimes more, to make it baseline usable
✧✦Catherine✦✧
separately from that, Z3 is bad software
✧✦Catherine✦✧
@arnaugamez not enough experience to say
Z3 commits crimes, with one of the biggest ones is the pervasive use of semantically unforgivable operator overloading and silent truncation in the Python interface
`a >> b` you might think this works the same for bit vectors as it does for Python integers, but Z3 uses arithmetic right shift for it. guess who just lost like 8 hours to this?
Arnau
@whitequark opinions on cvc5? Others?
✧✦Catherine✦✧
imagine this code stomping on your face forever
this is the experience of using z3py with bitvectors
✧✦Catherine✦✧
if SMT-LIB was designed for actually useful applications it would have had a function to replace a chunk of a bitvector with something else, instead of forcing you to do a {let binder, extract, extract, concat} dance and hope whatever you're using to emit code is flexible enough that you can actually get the let binder to work (or you end up with quadratic growth of SMT-LIB terms)
✧✦Catherine✦✧
@soc no? SMT-LIB is its own language, vaguely lispy in nature
soc
@whitequark It's Python, isn't it?
✧✦Catherine✦✧
every time i have to interact with SMT solvers it leaves me incandescently angry in a way little other tooling does. would it fucking kill you to allow zero length bitvectors? did you take inspiration from verilog??
✧✦Catherine✦✧
whose fucking idea was it to require the shift amount to have the same width as the value to be shifted? is this purposefully designed to torture compiler developers??
✧✦Catherine✦✧
@skandhurkat this is completely irrelevant
Skand Hurkat
@whitequark if it is a shift where both the value and the shift amount are in registers, both quantities will have the same number of bits. If the shift amount is an immediate, then the number of bits available for the shift amount will match whatever the bit width for immediates is in that ISA, just to keep the decode easy.
✧✦Catherine✦✧
@ignaloidas i'm all for less crackhead APIs yes
Ignas Kiela
@whitequark@mastodon.social maybe now you better understand why I think using pure SAT is better for prjunnamed 😉
✧✦Catherine✦✧
@ignaloidas SMT doesn't even add that much value. arguably it adds negative value. I hate it so much
✧✦Catherine✦✧
your query is slow. you have decided to use theory of arrays
now your query doesn't complete at all _but_ at least it consumes 10x as much RAM in the first hour
✧✦Catherine✦✧
instead of: QF_BVA
have you considered: QF_BV and you concatenate all of your symbolic RAM into one big bit vector you shift by your load address
this will probably be faster and work on more solvers
GNU social JP is a social network, courtesy of GNU social JP管理人. It runs on GNU social, version 2.0.2-dev, available under the GNU Affero General Public License.
All GNU social JP content and data are available under the Creative Commons Attribution 3.0 license.