3 ms·
Tried to use MiniZinc to write a model checker [1] for c programs a while back [2]. Essentially checking the equivalence of c functions that use only bit operat
by trex987 9y ago
Tried to use MiniZinc to write a model checker [1] for c programs a while back [2]. Essentially checking the equivalence of c functions that use only bit operations. It basically translates the programs into minizinc, then attempts to derive a case where the same input results in differing output. Was a fun way to experiment using the constraint solver for a practical application, though unfortunately didn't work as well on larger more complicated functions.
1) https://en.wikipedia.org/wiki/Model_checking https://en.wikipedia.org/wiki/Model_checking
2) https://github.com/dbunker/ArchStatMzn https://github.com/dbunker/ArchStatMzn
- hairtuq 9y agoI'd expect a SMT (Satisfiability modulo theory) solver like z3 to work better for this use case, might be worth giving it a try. E.g. x = z3.BitVec('x', 32) y = z3.BitVec('y', 32) i1 = x | y i2 = ~(~x | ~y) s = z3.Solver() s.add(i1 != i2) if s.check() == z3.sat: print "found counterexample" print s.model() else: print "always equal"