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
675 Commits 61 Branches 12 Tags 8.2 MiB
Haskell 100%
fcd94ded6e
Go to file
Rob Dockins fcd94ded6e Add tests to the BVDomain test suite that check to ensure that 
the results of domain operations are "proper", which means that
they satisfy their internal invariants.
2020-05-08 08:49:36 -07:00
dependencies Relax base bounds for what4-abc and what4-blt 2020-05-07 13:09:38 -07:00
what4 Add tests to the BVDomain test suite that check to ensure that 2020-05-08 08:49:36 -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.