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,079 Commits 61 Branches 12 Tags 8.1 MiB
Haskell 100%
0ac42a32ba
Go to file
Rob Dockins 0ac42a32ba Fix some issues with string escaping/unescaping in the SMTLib2 writer. 
Previously, we were too liberal with the characters we would emit
without escaping, and we would incorrectly fail to escape `\` characters
if they had a following `u` character.  In addition, our unescaping routine
was incorrectly rejecting strings from solvers if they ended with a literal
`\` character.

Fixes #184
Fixes #185
2022-02-25 10:45:40 -08:00
.github/workflows [what4] Remove 9.2.1 from CI: not ready yet 2022-01-10 08:18:43 -08:00
dependencies Bump language-sally submodule 2021-06-16 10:18:12 -07:00
what4 Fix some issues with string escaping/unescaping in the SMTLib2 writer. 2022-02-25 10:45:40 -08:00
what4-abc Fix compile errors in what4-abc 2021-09-27 17:11:19 -07:00
what4-blt Support building with GHC 9.0 2021-05-18 09:11:19 -04:00
what4-transition-system Update tests and examples to use the new EmptyExprBuilderState. 2022-01-21 10:57:26 -08:00
.gitignore Add darcs and emacs backups to .gitignore. 2021-04-19 15:57:15 -07:00
.gitmodules Update to changes in language-sally. 2021-05-07 14:01:57 -07:00
.hlint.yaml Separate Travis build+test jobs from lint jobs (#247) 2019-05-23 17:46:19 -07:00
cabal.project what4-transition-system: v0.0.3.0 2021-05-06 14:16:02 -07:00
README.md Update solver compatibility matrix for goal timeouts and unicode strings. 2022-01-10 20:46:56 -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 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 Dreal STP Yices Z3
Supported yes 3.2.2, ? 1.8, ? yes 2.3.3, ? 2.6.4, ? 4.8.8 -- 4.8.14
goal timeouts ? yes yes ? yes yes ! 4.8.12
strings with unicode and escape codes ? ? yes ? ? ? >= 4.8.12