Revision d4c6f6f15c1b33773937e952c68e24a6bd6d279e authored by Anish Tondwalkar on 08 November 2019, 23:31:48 UTC, committed by Anish Tondwalkar on 08 November 2019, 23:31:48 UTC
1 parent 1fc8b1d
CHANGES.md
# CHANGES
## NEXT
- Fix bugs in PLE
- Move to GHC 8.6.4
## 0.8.0.1
- Support for HORN-NNF format clauses, see `tests/horn/{pos,neg}/*.smt2`
- Support for "existential binders", see `tests/pos/ebind-*.fq` for example.
This only works with `--eliminate`.
- Move to GHC 8.4.3
## 0.7.0.0
- New `eliminate` based solver (see ICFP 2017 paper for algorithm)
- Proof by Logical Evaluation see `tests/proof`
- SMTLIB2 ADTs to make data constructors injective
- Uniformly support polymorphic functions via `apply` and elaborate
## 0.3.0.0
- Make interpreted mul and div the default, when `solver = z3`
- Use `higherorder` flag to allow higher order binders into the environment
## 0.2.2.0
- Added support for theory of Arrays `Map_t`, `Map_select`, `Map_store`
- Added support for theory of Bitvectors -- see `Language.Fixpoint.Smt.Bitvector`
- Added support for string literals
## 0.2.1.0
- Pre-compiled binaries of the underlying ocaml solver are now
provided for Linux, Mac OSX, and Windows.
No more need to install Ocaml!
## 0.2.0.0
- Parsing has been improved to require *much* fewer parentheses.
- Experimental support for Z3's theory of real numbers with the `--real` flag.
Computing file changes ...