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
663 Commits 61 Branches 12 Tags 8.2 MiB
Haskell 100%
6678683eb8
Go to file
Brian Huffman 6678683eb8 Make code compile without warnings in ghc-8.6 and ghc-8.8.
2020-04-23 20:26:28 -07:00
dependencies Add dependencies and a fresh cabal.project following repository split 2020-02-25 16:48:46 -08:00
what4 Make code compile without warnings in ghc-8.6 and ghc-8.8. 2020-04-23 20:26:28 -07:00
what4-abc Add an Annotation term former to the NonceApp type, 2020-04-02 10:27:02 -07:00
what4-blt Add an Annotation term former to the NonceApp type, 2020-04-02 10:27:02 -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.