21–29 of 29 posts
Earlier quoted context omitted.
I personally like to avoid the “writing in C++” experience. :/
The authors of a powerful solver package thought differently.
Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex. If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar. Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
(scaling to 100s-1000s of units)
If the tutorial uses Rust, why didn't they use a solver written in Rust? Z3 was written in C++.
Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex. If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar. Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
Earlier quoted context omitted.
It might have more to do with the first release of Z3 being in 2012, with the first stable Rust release being in 2015. Rather than the authors of Z3 passing some kind of judgment on Rust…
Z3 uses a sophisticated and fast garbage collection scheme internally that doesn't mesh well with Rust idioms.
Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex. If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar. Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
That’s interesting. I’m a logic designer too. How do you make use of it?
For the former it's useful when there's already a well-defined contract at some interface, like "this bus interface follows these basic AHB5 manager rules" or "if x_valid is asserted, it remains asserted until x_ready is asserted, and the other x_foobar are stable during that time" or "a FIFO is never both empty and full".
Simple properties + exhaustive checking is good bang-for-buck because it often teases out subtle tangential issues without having to write checks for implementation details. This isn't "formal verification" per se but using formal checks in a lightweight way to help find bugs and inconsistencies in your design.
Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex. If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar. Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
Z3 struggles with larger problems. CVC5 or Bitwuzla do a lot better once you get into anything complex. If you're familiar with the Z3 Python API, you'll find the CVC5 one familiar. Caveat: I mostly do logic design, maybe there are some software verification tasks where Z3 comes out ahead. I've never seen one though.
I'm curious as to why Z3 is so much more popular than CVC5 if CVC5 is better for solving complex problems. Is it because Z3 is older?