Symbolic formula representation and solver interaction library
Go to file
2020-02-29 12:53:17 -08:00
dependencies Add dependencies and a fresh cabal.project following repository split 2020-02-25 16:48:46 -08:00
what4 The delegate_ctlc flag actually has undesirable consequences 2020-02-19 13:44:23 -08:00
what4-abc what4: Remove DisjPred constructor. 2020-01-22 17:02:50 -08:00
what4-blt what4: Remove DisjPred constructor. 2020-01-22 17:02:50 -08: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

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.