CHANGES

NEXT

0.9.6.3 (2024-01-29)

• For now we stopped folding constants that contain NaN #670

0.9.4.7

• Support GHC 9.6 tuples with --extensionality #666 #667

0.9.2.5

• Adopt smtlib-backends for interactions with the SMT solvers #641

0.9.0.2

• Simplified the equalities dumped by PLE #569 #605
• Add PLE implementation based on interpreting expressions #502

0.8.10.2

• Dump equalities discovered by PLE #491 #569
• Dump prettified version of constraints #473
• Constraints now indicate the source code location that originated them #471
• Add support for term rewriting to PLE #428

0.8.6.4

• Fix bugs in PLE
• Move to GHC 8.6.4
• Add fuel parameter to debug unfolding in PLE

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.