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
682 Commits 61 Branches 12 Tags 8.2 MiB
Haskell 100%
7927ec39b7
Go to file
Kevin Quick 7927ec39b7
Update upper bound for parameterized-utils release 2.1.0.
2020-05-08 17:26:15 -07:00
dependencies Relax base bounds for what4-abc and what4-blt 2020-05-07 13:09:38 -07:00
what4 Update upper bound for parameterized-utils release 2.1.0. 2020-05-08 17:26:15 -07:00
what4-abc Update what4-abc with new abstract domain representation. 2020-05-08 08:49:36 -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 Try to unstick the travis builds 2020-05-08 08:49:36 -07: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.