Symbolic formula representation and solver interaction library
Go to file
Rob Dockins c7ff6350e2 Pipe through "tan" and "tanh" in the SMTWriter. They are not
longer eagerly translated into ratios of sin* and cos*.
2021-09-27 18:06:45 -07:00
.github/workflows [CI] update comment on disabled step to indicatee reason. 2021-07-30 12:52:25 -07:00
dependencies Bump language-sally submodule 2021-06-16 10:18:12 -07:00
what4 Pipe through "tan" and "tanh" in the SMTWriter. They are not 2021-09-27 18:06:45 -07: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 Increase bounds for what4-transition-system 2021-06-16 10:18:12 -07: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 Add support for Verilog export (#65) 2020-12-14 13:54:31 -08:00

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.