GitHub - moyix/fpsmt_gpu: Solving floating point SMT constraints on a GPU

To use:

$ ./generate.sh readme.smt2
$ bin/smt-readme-smt2 
Padding varsize from 16 to 16
Launching kernel on GPU0...
Padding varsize from 16 to 16
Launching kernel on GPU1...
Waiting on GPUs...
Search completed on device 0
Found a satisfying assignment on device 0 thread 39984:
08ff15d56d64377e0c66b83009bbe3ee

Name	Name	Last commit message	Last commit date
Latest commit wabscale ADD cmake files to gitignore Dec 8, 2020 2dc2f8c · Dec 8, 2020 History 19 Commits
SMTLIB	SMTLIB	Add moar optimization flags to nvcc	Dec 7, 2020
sample_smt	sample_smt	Add timing info and sample SMT files	Nov 28, 2020
.gitignore	.gitignore	ADD cmake files to gitignore	Dec 8, 2020
CMakeLists.txt	CMakeLists.txt	ADD cmake build configuration	Dec 8, 2020
Makefile	Makefile	ADD cmake build configuration	Dec 8, 2020
README.md	README.md	Fixes to generate.sh and a minimal README	Nov 27, 2020
TODO.txt	TODO.txt	More optimizations and usability enhancements	Nov 25, 2020
aes.cu	aes.cu	Reduce AES rounds to 2 instead of 10	Dec 7, 2020
aes_table.h	aes_table.h	Add input mutation using GPU-accelerated AES	Nov 24, 2020
cuda_aes.h	cuda_aes.h	More optimizations and usability enhancements	Nov 25, 2020
generate.sh	generate.sh	Run jfs-opt before jfs-smt2cxx, per mc-imperial/jfs#39	Dec 7, 2020
smt.cu	smt.cu	Use shared memory for variable storage try to do a bit more randomiza…	Dec 7, 2020
smt.h	smt.h	Use shared memory for variable storage try to do a bit more randomiza…	Dec 7, 2020
theory.h	theory.h	Add compile time smt to cxx compilation	Nov 25, 2020
theory.smt2	theory.smt2	Add compile time smt to cxx compilation	Nov 25, 2020

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Repository files navigation

About

Releases

Packages

Contributors 2

Languages

moyix/fpsmt_gpu

Folders and files

Latest commit

History

Repository files navigation

About

Resources

Stars

Watchers

Forks

Releases

Packages 0

Contributors 2

Languages

Packages