CHANGES

NEXT

0.9.6.3.4 (2026-01-14)

• Implement --sortedsolution to keep elaborated sorts in fqout/solution #821
• Retire old parser for horn queries #820
• Stop the parser from simplifying expressions during parsing #819
• Add --explicitKvars option and generalize horn syntax to accept expressions for kvars arguments #818
• Provide more comments in the SMT queries to relate them to the source code #814
• Remove --no-lazy-ple #813
• Allow PLE to unfold in kvar solutions #811
• Remove redundant question marks from expression #807
• Remove distinction of predicates and expressions in the parser #805
• Shrink kvar solutions #799 #809 #821
• Disable the progress bar when not on a terminal #798
• Retire existential binds #797
• Provide stack traces for more crashes #794
• Support string operators #793
• Apply kvar solutions to constraints before PLE #792
• Retire implementation of gradual refinement types #789
• Retire old PLE variations #788
• Add set cardinality support when using cvc5 #774
• Have --scrape consider global constants and ADTs #772
• Shorten flags of a few flags and add git-version #762
• Add support/conversions for Bitv8 and Bitv16 #759
• Support the finite field theory of CVC5 #755
• Fix SMT crashes on reflected functions on polymorphic data types #753
• Allow function names to start with prefix mod #751
• Implement let bindings for Horn queries #748
• Fix elaboration of define_fun declarations #747 #749

0.9.6.3.3 (2025-03-22)

• Add support for GHC HEAD (9.13) #745.
• Expose SMTLIB define-fun to users of liquid-fixpoint #744.
• Check that expressions in refinements are Bool-sorted #743.
• Fix crashes when a datatype is declared with a Map_t field #738.
• Simplify expressions in fqout files #741.

0.9.6.3.2 (2025-03-06)

• Expose relatedSymbols from EnvironmentReduction. Needed for improving error messages in LH #2346.
• Support extensionality in PLE #704
• Add a new flag --etabeta to reason with lambdas in PLE #705
• Add support for reflected lambdas in PLE #725
• Implement Bags and Maps reasoning with Arrays #703
• Support conditional elaboration of theories for cvc5 #734
• Generate smt2 files only when using --save #712
• Parameterize Expr and Reft by the variable type #708
• Preserve location of operators in the parser #721
• Optimize elaboration #736

0.9.6.3.1 (2024-08-21)

• Added support for ghc-9.10.1
• Use ; for comments in SMTParse (as done in SMTLIB) #700.
• Extend SMTParser to support lits e.g. for bitvec #698.
• refactor Set->Array elaboration #696.
• Fixed the polymorphism-related crash caused by a restrictive Set theory encoding #688.
• Do not constant-fold div by zero #686.
• Copy over the HOF configuraration options in hornFInfo #684.
• Use SMTLIB style serialization/deserialization for Horn queries #683.
• Print SMT preamble to the logfile when constructing context #681.
• Allow reading/saving horn queries from/to JSON #680.
• Extend parser to allow boolean function arguments #678.

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.