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
702 Commits 61 Branches 12 Tags 8.2 MiB
Haskell 100%
9c711a7971
Go to file
Rob Dockins 9c711a7971 update code in a comment
2020-07-06 18:38:04 -07:00
dependencies migration to bv-sized representation (#34) 2020-06-04 15:07:57 -07:00
what4 update code in a comment 2020-07-06 18:38:04 -07:00
what4-abc Add realTrunc and realRoundEven operations to fill out the 2020-06-15 17:09:19 -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 migration to bv-sized representation (#34) 2020-06-04 15:07:57 -07: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
bv-sized-migration.md migration to bv-sized representation (#34) 2020-06-04 15:07:57 -07:00
cabal.project migration to bv-sized representation (#34) 2020-06-04 15:07:57 -07: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.