4 ms·
Z3 is entirely different IMHO, once you get into solvers the question becomes not just 'is this satisfied' but 'what is the minimum sequence of steps necessary
by quesomaster9000 2y ago
Z3 is entirely different IMHO, once you get into solvers the question becomes not just 'is this satisfied' but 'what is the minimum sequence of steps necessary to arrive at the result'.
I have relied heavily on both Z3 and Alloy for ad-hoc jobs, and Prolog doesn't even come close to the inference power, and that's along-side Macsyma and Sage.
- gatlin 2y agoHave you tried sCASP?
- Karrot_Kream 2y agoWhat problem domain are you working in? I find usage of solvers and Prolog to be very domain specific.
- quesomaster9000 2y agoAt the moment I'm verifying a Rust floating point implementation, which has lead to many small snippets for not just generating test & edge cases (e.g. find inputs which falls outside of these conditions), but trying to prove completeness on all valid inputs.
- rscho 2y agoThe big advantage of prolog vs solvers is the logic programming aspect. If you can express parts of your program in a logically pure way, Prolog code will be much more concise than the Z3 equivalent, although probably slower. Another advantage is that Prolog outputs and reads Prolog terms, which makes it very good for metaprogramming. It's like lisp: incredible if you're solo prototyping, not so much if you're part of a team of corporate cogs.
- rurban 2y agoMost better prologs now include solvers already.