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.

v2.8.1 (2024-11-29)

Added

• Added instances Semigroup, Monoid and Contravariant for Debugger

v2.8.0 (2024-11-28)

Changed

• Replaced representation of RealSort values in Haskell with Rational instead of Double

v2.7.2 (2024-11-27)

Added

• Added dependency constrained-some

Changed

• Replaced internal usages of custom existential SomeSMTSort with Some1 from constrained-some

Removed

• Removed module Language.Hasmtlib.Internal.Constraint

v2.7.1 (2024-10-05)

Changed

• Cardinality constraints in Language.Hasmtlib.Counting now use specialized and more efficient encodings for a few cases.
• Debugging with debugger statistically now prints a more comprehensive overview about the problem size.
• Fixed bug where setting multiple custom SMTOptions would only set the most recent.
• Fixed bug where timeout for SMT/OMT would not work.
• Added smart constructors for ite.

v2.7.0 (2024-09-12)

Added

• Added helpful instances for standard types for Codec to ease deriving.
• Added decorator timingout in Language.Hasmtlib.Type.Solver to set a time-out for solvers. Unfortunately as of SMTLib standard v2.6 there is no SMT-Option for this. Although some solvers like Z3 (unreliably) support it, we instead do it by internally coordinating the kill of the solver process from Haskell using System.Timeout.Lifted#timeout. Works like a charme.
• Added Language.Hasmtlib.Type.Debugger for debugging problem construction and solver interaction.

Changed

• (breaking change) Completely revised the way solver process-configurations are handled and debugged. Solvers which previously had the type Process.Config from smtlib-backends now have the type SolverConfig from Language.Hasmtlib.Type.Solver. This bundles information on the executable of the solver with additional information such as debugging and time-outs. Actual solver creation still is done by funtion solver. Therefore this change is only breaking, if you created custom solvers or debugged solvers.
• Debugging solvers changed from solveWith (debug z3 def) $ ... to solveWith (solver $ debugging z3 def) $ .... Also note that there are plenty debugging configurations besides def existing in Language.Hasmtlib.Type.Debugger now.
• Interactive solving before was a two-stepper like iZ3 <- interactiveSolver z3 ; interactiveWith iZ3 $ .... Leveraging SolverConfig this has been changed to a more uniform way with interactiveWith z3 $ do .... Also note that debugInteractiveWith z3 $ ... now is replaced by interactiveWith (debugging def z3) $ ....

Removed

• Removed Language.Hasmtlib.Solver.Common. Contents are now in Language.Hasmtlib.Type.Solver.

v2.6.3 (2024-09-07)

Added

• Added a solver configuration bitwuzlaKissat for Bitwuzla with underlying SAT-Solver Kissat.

Changed

• Removed solveMinimizedDebug & solveMaximizedDebug. Use the modified solveMinimized & solveMaximized instead. You can also provide a step-size now.
• Fixed a bug where MonadOMT#solve would run get-model although the solver did not necessarily respond with Sat.
• SharingMode for sharing common (sub-)expressions now defaults to None. The previous default StableNames in general is only worth using, when your program can benefit a lot from sharing. Otherwise it may drastically downgrade solver performance due to abundance of sharing-variables. If you still want to use it, run setSharingMode StableNames within the problems monad.

v2.6.2 (2024-09-04)

Changed

• Functions for enconding cardinality-constraints in Language.Hasmtlib.Counting now use specialized encodings for some cardinalities - improving solvers efficiency.

v2.6.1 (2024-09-02)

Added

• Added module 'Language.Hasmtlib.Type.Relation' for encoding binary relations
• Added rich documentation and usage examples for all public modules

v2.6.0 (2024-08-27)

Added

• Support for signed BitVec operations.
• Added constructor Rem for Expr t.

Changed

• (breaking change) Enhanced the type of BvSort Nat to BvSort BvEnc Nat where BvEnc = Unsigned | Signed. Before, the API only allowed unsigned BitVec, therefore BvSort n now becomes BvSort Unsigned n. The promoted type BvEnc is phantom and only used for differentiating instances for Num, ...
• Moved Language.Hasmtlib.Internal.Bitvec to Language.Hasmtlib.Type.Bitvec, exported API with Language.Hasmtlib
• Removed constructors StrLT and StrLTHE from Expr t.
• Fixed wrong implementation of Num for Bitvec. (+), (-) and (*) had invalid definitions.

v2.5.1 (2024-08-26)

Added

• Added SharingMode = None | StableNames in Language.Hasmtlib.Internal.Sharing. Defaults to StableNames.
• Added function setSharingMode which allows you to change the SharingMode.

Changed

• runSharing in Language.Hasmtlib.Internal.Sharing now differentiates sharing behavior based on newly given argument of type SharingMode

v2.5.0 (2024-08-25)

Added

• added instances Eq, Ord, GEq and GCompare for Expr t
• added instances Real and Enum for Expr IntSort, Expr RealSort and Expr (BvSort n)
• added instance Integral for Expr IntSort and Expr (BvSort n)
• added instance Bits for Expr BoolSort and Expr (BvSort n)

Changed

• Removed Language.Hasmtlib.Integraled: use the added Integral instance instead
• Removed redundant BitVec constructors from Expr and replaced usage in instances with the more generic existing ones. For example: Where BvNot was used previously, we now use Not which is already used for Expr BoolSort. Differentiation between such operations now takes place in Language.Hasmtlib.Internal.Render#render when rendering expressions, e.g. rendering bvnot for BvSort and not for BoolSort. Therefore there is no behavioral change for the solver.
• Removed functions bvRotL and bvRotR from Language.Hasmtlib.Type.Expr: use the added Bits instance instead with rotateL and rotateR

v2.4.0 (2024-08-21)

Added

• Added observable sharing with Language.Hasmtlib.Internal.Sharing. Thank you fabeulous@github for the great help!
• Added Language.Hasmtlib.Internal.Uniplate1 for plating GADTs

Changed

• Deleted and moved Language.Hasmtlib.Equatable, Language.Hasmtlib.Orderable, Language.Hasmtlib.Iteable & Language.Hasmtlib.Internal.Expr into Language.Hasmtlib.Type.Expr

v2.3.2 (2024-08-17)

Changed

• Internal replacement of Prelude.liftA2 for backwards compatiblity
• Fixed bug where solveMaximizedDebug would solve minimized instead of maximized

v2.3.1 (2024-08-16)

Changed

• Instances for Boolean, Num & Fractional on Expr now use smart constructors

v2.3.0 (2024-08-12)

Added

• Added full SMTLib2.6-standard support for sort String
• Added module Language.Hasmtlib.Lens featuring instance Plated (Expr t) for rewriting

Changed

• Export constructors of Expr t
• instance Show (Expr t) now displays expressions in SMTLib2-Syntax

v2.2.0 (2024-08-09)

Added

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

Changed

• (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.

v2.1.0 (2024-07-26)

Added

• Added solver Bitwuzla
• Added debugging capabilities for Pipe by introducing debugInteractiveWith

Changed

• 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.

v2.0.1 (2024-07-23)

Added

• Added more documentation

Changed

• (<==>) now has infixr 4
• (<==) now has infixl 0

v2.0.0 (2024-07-23)

Added

• 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

Changed

• (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

v1.3.1 (2024-07-12)

Added

• Added count in Language.Hasmtlib.Counting

v1.3.0 (2024-07-12)

Added

• Added cardinality constraints with Language.Hasmtlib.Counting

v1.2.0 (2024-07-11)

Added

• Added n-ary comparisons distinct & equal

Changed

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

v1.1.2 (2024-07-02)

Changed

• Minor internal changes

v1.1.1 (2024-06-25)

Added

• Added this CHANGELOG.md file

v1.1.0 (2024-06-21)

Added

• Added ArraySort and full support for its SMTLib2 standard specification