Changelog for hasmtlib-2.2.0

Changelog

All notable changes to the hasmtlib library will be documented in this file.

The format is based on Keep a Changelog, and this project adheres to PVP versioning.

Added multiple basic instances for Equatable, Orderable, Iteable, Variable & Codec

(breaking change) Variable & Codec now ship with a Generic default implementation instead of relying on Applicative. This will break your instances if the type does not have an instance for Generic.

Yices now uses flag --incremental by default
(breaking change) Removed functional dependency m -> s from MonadIncrSMT s m. This forces you to specify the underlying state when using interactiveWith. Therefore interactiveWith cvc5Living $ do ... now becomes interactiveWith @Pipe cvc5Living $ do ....
(breaking change) Removed newtype ProcessSolver and replaced it with underlying SMTLIB.Backends.Process.Config. This may only affect you if you instantiated custom solvers.

Arithmetic functions: isIntSort, toIntSort & toRealSort
Asserting maybe-formulas: assertMaybe :: MonadSMT s m => Maybe (Expr BoolSort) -> m ()
Logical equivalence (<==>) & reverse logical implication (<==)
Solvers: OpenSMT, OptiMathSAT
Iterative refinement optimizations utilizing incremental stack
Custom solver options via Custom String String :: SMTOption
Optimization Modulo Theories (OMT) / MaxSMT support with: minimize, maximize & assertSoft

(breaking change) The functions solver and debug which create Solvers from ProcessSolvers are polymorph in the state s now. This requires you to annotate the mentioned functions with the targetted state. These are SMT and OMT. For example, solverWith (solver cvc5) $ do ... becomes solverWith (solver @SMT cvc5) $ do ....
Prefix xor now has an infix 4

(breaking change) When using interactiveWith the SMTOption Incremental is no longer set by default anymore