Skip to content

Latest commit

 

History

History
213 lines (154 loc) · 9.36 KB

CHANGELOG.md

File metadata and controls

213 lines (154 loc) · 9.36 KB
Raw

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