what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

# what4-1.5.1: Solver-agnostic symbolic values support for issuing queries

What4 is a generic library for representing values as symbolic formulae which may contain references to symbolic values, representing unknown variables. It provides support for communicating with a variety of SAT and SMT solvers, including Z3, CVC4, CVC5, Yices, Boolector, STP, and dReal. The data representation types make heavy use of GADT-style type indices to ensure type-correct manipulation of symbolic values.

Modules

what4-1.5.1

- Test
  Submodules
  - Test.Verification Testing abstraction layer
- What4
  Submodules
  - What4.BaseTypes This module exports the types used in solver expressions.
  - What4.Concrete Concrete values of base types
  - What4.Config Declares attributes for simulator configuration settings.
  - What4.Expr Commonly-used reexports from the expression representation
    Submodules
    - What4.Expr.Allocator Expression allocators for controlling hash-consing
    - What4.Expr.App
    - What4.Expr.AppTheory Identifying the solver theory required by a core expression
    - What4.Expr.ArrayUpdateMap Datastructure for representing a sequence of updates to an SMT array
    - What4.Expr.BoolMap Datastructure for representing a conjunction of predicates
    - What4.Expr.Builder Main definitions of the What4 expression representation
    - What4.Expr.GroundEval Computing ground values for expressions from solver assignments
    - What4.Expr.MATLAB Low-level support for MATLAB-style arithmetic operations
    - What4.Expr.Simplify Simplification procedure for distributing operations through ifthenelse
    - What4.Expr.StringSeq Datastructure for sequences of appended strings
    - What4.Expr.UnaryBV A "unary" bitvector representation
    - What4.Expr.VarIdentification Compute the bound and free variables appearing in expressions
    - What4.Expr.WeightedSum Representations for weighted sums and products in semirings
  - What4.FloatMode Mode values for controlling the "interpreted" floating point mode.
  - What4.FunctionName Declarations for function names.
  - What4.IndexLit
  - What4.Interface Main interface for constructing What4 formulae
  - What4.InterpretedFloatingPoint
  - What4.LabeledPred Predicates with some metadata (a tag or label).
  - What4.Panic
  - What4.Partial Representation of partial values
  - What4.ProblemFeatures Descriptions of the "features" that can occur in queries
  - What4.ProgramLoc Datatype for handling program locations
  - Protocol
    Submodules
    - What4.Protocol.Online Online solver interactions
    - What4.Protocol.PolyRoot Representation for algebraic reals
    - What4.Protocol.ReadDecimal
    - What4.Protocol.SExp
    - What4.Protocol.SMTLib2 Interface for solvers that consume SMTLib2
      Submodules
      - What4.Protocol.SMTLib2.Parse
      - What4.Protocol.SMTLib2.Response
      - What4.Protocol.SMTLib2.Syntax
    - What4.Protocol.SMTWriter Infrastructure for rendering What4 expressions in the language of SMT solvers
    - What4.Protocol.VerilogWriter
      Submodules
      - What4.Protocol.VerilogWriter.ABCVerilog
      - What4.Protocol.VerilogWriter.AST
      - What4.Protocol.VerilogWriter.Backend
  - What4.SFloat
  - What4.SWord Dynamically-sized bitvector values
  - What4.SatResult Simple datastructure for capturing the result of a SAT/SMT query
  - What4.SemiRing Definitions related to semiring structures over base types.
  - Serialize
    Submodules
    - What4.Serialize.FastSExpr
    - What4.Serialize.Log Log msgs via a synchronized channel
    - What4.Serialize.Normalize
    - What4.Serialize.Parser
    - What4.Serialize.Printer
    - What4.Serialize.SETokens
  - What4.Solver Reexports for working with solvers
    Submodules
    - What4.Solver.Adapter Defines the low-level interface between a particular solver and the SimpleBuilder family of backends.
    - What4.Solver.Boolector Interface for running Boolector
    - What4.Solver.CVC4 Solver adapter code for CVC4
    - What4.Solver.CVC5 Solver adapter code for cvc5
    - What4.Solver.DReal Interface for running dReal
    - What4.Solver.ExternalABC Solver adapter code for an external ABC process via SMT-LIB2.
    - What4.Solver.STP Solver adapter code for STP
    - What4.Solver.Yices Solver adapter code for Yices
    - What4.Solver.Z3 Solver adapter code for Z3
  - What4.SpecialFunctions Utilities relating to special functions
  - What4.Symbol Datatype for representing names that can be communicated to solvers
  - Utils
    Submodules
    - What4.Utils.AbstractDomains Abstract domains for term simplification
    - What4.Utils.AnnotatedMap A finite map data structure with monoidal annotations
    - What4.Utils.Arithmetic Utility functions for computing arithmetic
    - What4.Utils.BVDomain Abstract domains for bitvectors
      Submodules
      - What4.Utils.BVDomain.Arith
      - What4.Utils.BVDomain.Bitwise
      - What4.Utils.BVDomain.XOR
    - What4.Utils.Complex Provides a complex representation that is more generic than Data.Complex.
    - What4.Utils.Endian
    - What4.Utils.Environment Provides functions for finding an executable, and expanding a path with referenced to environment variables.
    - What4.Utils.FloatHelpers
    - What4.Utils.HandleReader
    - What4.Utils.IncrHash
    - What4.Utils.LeqMap
    - What4.Utils.MonadST Typeclass for monads generalizing ST
    - What4.Utils.OnlyIntRepr
    - What4.Utils.Process
    - ResolveBounds
      Submodules
      - What4.Utils.ResolveBounds.BV Resolve the lower and upper bounds of a SymBV
    - What4.Utils.Serialize
    - What4.Utils.Streams IO stream utilities
    - What4.Utils.StringLiteral Utility definitions for strings
    - What4.Utils.Versions
    - What4.Utils.Word16String Utility definitions for wide (2-byte) strings
  - What4.WordMap Datastructure for mapping bitvectors to values