projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 587e71e) | patch
an example that uses bitvectors to simulate sha1 computation and dumps an smt problem...
authorDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 14 Jul 2012 13:07:19 +0000 (13:07 +0000)
committerDejan Jovanović <dejan.jovanovic@gmail.com>
Sat, 14 Jul 2012 13:07:19 +0000 (13:07 +0000)
commit35637c2a760c35ca1c61edc276875cd91df0ab11
tree0f8c24212b425b977e4c22561347cd3ae9f28aactree
parent587e71e5de725968d8924cceb91c79d615edb660commit | diff
an example that uses bitvectors to simulate sha1 computation and dumps an smt problem corresponding to the hash-inversion problem
examples/Makefile.am diff | blob | history
examples/hashsmt/Makefile [new file with mode: 0644] blob
examples/hashsmt/Makefile.am [new file with mode: 0644] blob
examples/hashsmt/sha1.hpp [new file with mode: 0644] blob
examples/hashsmt/sha1smt.cpp [new file with mode: 0644] blob
examples/hashsmt/word.cpp [new file with mode: 0644] blob
examples/hashsmt/word.h [new file with mode: 0644] blob