5 ms·
Instead of brute force, it looks like it's comparing automatically-generated models of the two implementations symbolically. Success! Amazingly, this proof sys
by panic 13y ago
Instead of brute force, it looks like it's comparing automatically-generated models of the two implementations symbolically.
Success! Amazingly, this proof systems scales to large values of n where exhaustive checking is not feasible:
$ time make n=1000
Proving function equivalent to reference:
encode_aig : [1000][8] -> [1336][8]
Q.E.D.
real: 17.882s user: 16.31s cpu: 1.50s*
- pjscott 13y agoModern SMT solvers are astonishingly fast for most real-world inputs. Not bad, considering that the problem they solve is NP-complete!