GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-12-01 20:23:10 +03:00
Code Issues Projects Releases Wiki Activity
Symbolic formula representation and solver interaction library
668 Commits 61 Branches 12 Tags 8.2 MiB
Haskell 100%
0a44276206
Go to file
Rob Dockins 0a44276206 Relax base bounds for what4-abc and what4-blt
2020-05-07 13:09:38 -07:00
dependencies Relax base bounds for what4-abc and what4-blt 2020-05-07 13:09:38 -07:00
what4 Update for GHC 8.10 2020-05-05 15:55:52 -07:00
what4-abc Relax base bounds for what4-abc and what4-blt 2020-05-07 13:09:38 -07:00
what4-blt Relax base bounds for what4-abc and what4-blt 2020-05-07 13:09:38 -07:00
.gitignore Ignore GHC environment files 2018-12-06 10:45:23 -08:00
.gitmodules Set up travis CI 2020-02-29 12:53:17 -08:00
.hlint.yaml Separate Travis build+test jobs from lint jobs (#247) 2019-05-23 17:46:19 -07:00
.travis.yml Set up travis CI 2020-02-29 12:53:17 -08:00
cabal.project Add dependencies and a fresh cabal.project following repository split 2020-02-25 16:48:46 -08:00
README.md Add a basic README 2020-02-25 17:29:54 -08:00

README.md

What4 is a library for representing symbolic terms and communicating with satisfiability and SMT solvers (e.g. Yices and Z3).

It was originally a part of the Crucible (https://github.com/GaloisInc/crucible) project, but has found use cases that are independent of its original purpose as the representation language for the Crucible symbolic simulator, and has thus been split out into a separate repository.