Hacker NewsHacker News
Some silly Z3 scripts I wrote
36 points by azhenley 4 days ago | 8 comments
jeremysalwen 6 hours ago
I'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
reply
ymherklotz 5 hours ago
No 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")
reply
hwayne 5 hours ago
...Whoops. Yup, SMT solvers can famously return `unknown` on top of `sat` and `unsat`. Just added a post addendum about the mistake.
reply
potato-peeler 8 hours ago
For 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...

reply
bjornsing 7 hours ago
The concept is called static analysis.
reply
ukuina 7 hours ago
Seems adjacent, with some overlap.
reply
mathisfun123 6 hours ago
in theory that's what a compiler is - a thin wrapper over a SAT solver. in practice most compilers just use heuristics <shrug>.
reply
iberator 8 hours ago
I was expecting a Z3 computer from Germany.
reply