3 ms·
Some silly Z3 scripts I wrote
- iberator 8mo agoI was expecting a Z3 computer from Germany.
- potato-peeler 8mo agoFor the curious, solvers like z3 are used in programming languages to verify logic and constraints. Basically it can help find logic issues and bugs during compile time itself, instead of waiting for it to show up in runtime. https://en.wikipedia.org/wiki/Satisfiability_modulo_theories#Verification https://en.wikipedia.org/wiki/Satisfiability_modulo_theories...
- bjornsing 8mo agoThe concept is called static analysis.
- ukuina 8mo agoSeems adjacent, with some overlap.
- mathisfun123 8mo agoin theory that's what a compiler is - a thin wrapper over a SAT solver. in practice most compilers just use heuristics <shrug>.
- lkuty 8mo agoLike in the Dafny pogramming language. Cfr. https://www.youtube.com/watch?v=oLS_y842fMc https://www.youtube.com/watch?v=oLS_y842fMc
- jeremysalwen 8mo agoI'm suspicious of the theorem proving example. I thought Z3 could fail to return sat or unsat, but he is assuming that if it's not sat the theorem must be proven
- hwayne 8mo ago...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.
- ymherklotz 8mo agoNo I think it's fine. On another note, I have proven Fermat's Last Theorem with z3 using this setup :) and it goes faster if you reduce a variable called "timeout" for some reason! from z3 import * s = Solver() s.set("timeout", 600) a = Int('a') b = Int('b') c = Int('c') s.add(a > 0) s.add(b > 0) s.add(c > 0) theorem = a ** 3 + b ** 3 != c ** 3 if s.check(Not(theorem)) == sat: print(f"Counterexample: {s.model()}") else: print("Theorem true")