GaloisInc/what4
1
1
Fork 0
mirror of https://github.com/GaloisInc/what4.git synced 2024-10-06 00:22:49 +03:00
Code Issues Projects Releases Wiki Activity
Symbolic formula representation and solver interaction library
1,129 Commits 61 Branches 12 Tags 8.1 MiB
Haskell 100%
e384609f34
Go to file
Ryan Scott e384609f34 template_tests: Emit an error code if tests fail 
Running `hedgehog`'s `checkSequential` function alone isn't enough to cause a
test suite to fail if one or more of the test cases to fail. Per a comment in
the `hedgehog` source code
[here](3d4dde46e1/hedgehog-example/test/test.hs (L34-L42)),
the idiomatic way to do make a `checkSequential` failure imply test suite
failure is to check the result of running `checkSequential` and, if that is
`False`, throw `exitFailure`. This patch incorporates that advice into the
`test_templates` test suite.

Fixes #206.
2022-07-05 13:02:00 -04:00
.github/workflows Adding support for cvc5 (#204) 2022-07-01 13:36:44 -07:00
dependencies Allow building with GHC 9.2 2022-04-12 05:24:50 -04:00
what4 template_tests: Emit an error code if tests fail 2022-07-05 13:02:00 -04:00
what4-abc Allow building with GHC 9.2 2022-04-12 05:24:50 -04:00
what4-blt Allow building with GHC 9.2 2022-04-12 05:24:50 -04:00
what4-transition-system Bump what4 version to 1.3 2022-04-19 13:39:12 -04:00
.gitignore Add darcs and emacs backups to .gitignore. 2021-04-19 15:57:15 -07:00
.gitmodules Remove lingering references to Sally 2022-04-11 16:51:47 -04:00
.hlint.yaml Separate Travis build+test jobs from lint jobs (#247) 2019-05-23 17:46:19 -07:00
cabal.project Remove lingering references to Sally 2022-04-11 16:51:47 -04:00
README.md Adding support for cvc5 (#204) 2022-07-01 13:36:44 -07: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 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.

For an overview of What4 and how to use it, please see the package-level README.

This material is based upon work supported by the Defense Advanced Research Projects Agency (DARPA) under Contract No. HR0011-19-C-0070. The views, opinions, and/or findings expressed are those of the author(s) and should not be interpreted as representing the official views or policies of the Department of Defense or the U.S. Government.

Solver Compatibility

Feature ABC Boolector CVC4 CVC5 Dreal STP Yices Z3
Supported yes >= 3.2.0, ? >= 1.8, ? yes yes >= 2.3.3, ? 2.6.x, ? 4.8.8 -- 4.8.14
goal timeouts ? yes yes yes ? yes yes ! (4.8.11 or 4.8.12)
strings with unicode and escape codes ? ? >= 1.8 yes ? ? ? >= 4.8.11