Changelog for what4-1.4
1.4 (January 2023)
-
Allow building with GHC 9.4.
-
Remove the
MonadFail
instance forVarRecorder
, as this instance is no longer straightforward to define due to upstream changes inbase-4.17.0.0
. This instance ultimately callederror
anyways, so any uses offail
at typeVarRecorder
can be replaced witherror
without any change in behavior. -
Remove a dependency on
data-binary-ieee754
, which has been deprecated. -
Deprecate
allSupported
which represents the SMT logicALL_SUPPORTED
, and addallLogic
instead which represents the SMTLib standard logicALL
. -
Add support for the cvc5 SMT solver.
-
Add a
get-abduct
feature which is compatible with cvc5. -
Add modules to support serialization and deserialization of what4 terms into an s-expression format that is a superset of SMTLib2. See the
What4.Serialize.Printer
,What4.Serialize.Parser
, andWhat4.Serialize.FastSExpr
modules. Note that these modules have names that conflict with the now deprecated what4-serialize package, from which they were copied. If you are updating to this version of what4, delete your dependency on what4-serialize. -
Add support Syntax-Guided Synthesis (SyGuS) in CVC5 (through the
runCVC5SyGuS
function) and Constrained Horn Clauses (CHC) in Z3 (through therunZ3Horn
function). -
Make
what4
smarter about simplifyingintMin x y
andintMax x y
expressions when eitherx <= y
ory <= x
can be statically determined.
1.3 (April 2022)
-
Allow building with GHC 9.2.
-
According to this discussion, the
forall
identifier will be claimed, andforall
made into a full keyword. Therefore, theforall
andexists
combinators ofWhat4.Protocol.SMTLib2.Syntax
have been renamed intoforall_
andexists_
. -
Add operations for increased control over the scope of configuration options, both in the
What4.Config
andWhat4.Expr.Builder
modules. -
Previously, the
exprCounter
,sbUserState
,sbUnaryThreshold
, andsbCacheStartSize
fields ofExprBuilder
were directly exposed; in principle this allows users to modify them, which was not intended in some cases. These have been uniformly renamed to remove thesb
prefix, and exposed asGetter
orLens
values instead, as appropriate. -
The
sbBVDomainRangeLimit
fields ofExprBuilder
was obsolete and has been removed. -
Allow building with
hashable-1.4.*
:- Add
Eq
instances for all data types withHashable
instances that were missing correspondingEq
instances. This is required sincehashable-1.4.0.0
adds anEq
superclass toHashable
. - Some
Hashable
instances now have extra constraints to match the constraints in their correspondingEq
instances. For example, theHashable
instance forSymNat
now has an extraTestEquality
constraint to match itsEq
instance.
- Add
-
Add an
unsafeSetAbstractValue
function to theIsExpr
class which allows one to manually set theAbstractValue
used in a symbolic expression. As the name suggests, this function is unsound in the general case, so use this with caution. -
Add a
What4.Utils.ResolveBounds.BV
module, which provides aresolveSymBV
function that checks if aSymBV
is concrete. If it is not concrete, it returns the lower and upper version bounds, as determined by querying an online SMT solver. -
Add
arrayCopy
,arraySet
, andarrayRangeEq
methods toIsExprBuilder
. -
Add a
getUnannotatedTerm
method toIsExprBuilder
for retrieving the original, unannotated term out of an annotated term. -
IsExprBuilder
now hasfloatSpecialFunction{,0,1,2}
andrealSpecialFunction{,0,1,2}
methods which allow the use of special values or functions such aspi
, trigonometric functions, exponentials, or logarithms. Similarly,IsInterpretedFloatExprBuilder
now hasiFloatSpecialFunction{,0,1,2}
methods. Although little solver support exists for special functions,what4
may be able to prove properties about them in limited cases.- The
realPi
,realLog
,realExp
,realSin
,realCos
,realTan
,realSinh
,realCosh
,realTanh
, andrealAtan2
methods ofIsExprBuilder
now have default implementations in terms ofrealSpecialFunction{,0,1,2}
.
- The
-
Add an
exprUninterpConstants
method toIsSymExprBuilder
which returns the set of uninterpreted constants in a symbolic expression. -
Add a
natToIntegerPure
function which behaves likenatToInteger
but without usingIO
. -
asConcrete
now supports concretizing float expressions by way of the newConcreteFloat
constructor inConcreteVal
. -
Add a
z3Tactic
configuration option toWhat4.Solver.Z3
that allows specifying a custom tactic to pass toz3
. -
safeSymbol
now replaces exclamation marks (!
) with underscores (_
) so that the generated names are legal in Verilog. -
Add
Foldable
,Traversable
, andShow
instances forLabeledPred
. -
Fix a bug in which
what4
would generate incorrect SMTLib code for array lookups and updates when using the CVC4 backend. -
Fix a bug in which
what4
would incorrectly attempt to configure Boolector 3.2.2 or later. -
Fix a bug in which strings containing
\u
or ending with\
would be escaped incorrectly.
1.2.1 (June 2021)
- Include test suite data in the Hackage tarball.
1.2 (June 2021)
This is primarily a bugfix release, but also adds support for GHC 9.x
-
Tweaks to the
SolverEvent
data type to remove partial fields. -
Fix issue #126. The shift operations of
What4.SWord
were not correctly handling cases where the shift amount has more bits than the word to be shifted. -
Fix issue #121. The ordering of inputs in generated Verilog files is now more predictable. Previously, it was determined by the order the inputs were encountered during term traversal. Now the user can provide a list of (input, name) pairs which are declared in order. Any additional inputs discovered during traversal will be added after these specified inputs.
-
Fix issue #113. The
bvSliceLE
andbvSliceBE
functions ofWhat4.SWord
did not properly handle size 0 bit-vectors and requests for 0 length slices. They now correctly fail for slice lengths longer than 0 on 0-length vectors, and correctly allow 0 length slices regardless of the length of the input. -
Fix issue #103. Some of the string operations would give incorrect results when string offsets are out-of-bounds. The SMTLib 2.6 standard specifies precise results for these cases, which we now implement.
-
Configuration parameters relative to solvers have been renamed in a more consistent and heirarchical fashion; the old configuration parameters still work but will emit deprecation warnings when used.
default_solver
-->solver.default
abc_path
-->solver.abc.path
boolector_path
-->solver.boolector.path
cvc4_path
-->solver.cvc4.path
cvc4.random-seed
-->solver.cvc4.random-seed
cvc4_timeout
-->solver.cvc4.timeout
dreal_path
-->solver.dreal.path
stp_path
-->solver.stp.path
stp.random-seed
-->solver.stp.random-seed
yices_path
-->solver.yices.path
yices_enable-mcsat
-->solver.yices.enable-mcsat
yices_enable-interactive
-->solver.yices.enable-interactive
yices_goal_timeout
-->solver.yices.goal-timeout
yices.*
-->solver.yices.*
for many yices internal optionsz3_path
-->solver.z3.path
z3_timeout
-->solver.z3.timeout
-
Added the
solver.strict_parsing
configuration parameter. This is enabled by default but could be disabled to allow running solvers in debug mode or to workaround other unexpected output from solver processes.
1.1 (February 2021)
-
Use multithread-safe storage primitive for configuration options, and clarify single-threaded use assumptions for other data structures.
-
Fix issue #63, which caused traversals to include the bodies of defined functions at call sites, which yielded confusing results.
-
Add concrete evaluation and constant folding for floating-point operations via the
libBF
library. -
Add min and max operations for integers and reals to the expression interface.
-
Remove
BaseNatType
from the set of base types. There were bugs relating to having nat types appear in structs, arrays and functions that were difficult to fix. Natural number values are still available as scalars (where they are represented by integers with nonzero assumptions) via theSymNat
type. -
Support for exporting What4 terms to Verilog syntax.
-
Various documentation fixes and improvements.
-
Test coverage improvements.
-
Switch to use the
prettyprinter
package for user-facing output.
1.0 (July 2020)
- Initial Hackage release