grisette 0.3.1.1 → 0.4.0.0

raw patch · 121 files changed

+18228/−4916 lines, 121 filesdep +asyncdep +stmdep ~QuickCheckdep ~sbvdep ~template-haskellPVP ok

version bump matches the API change (PVP)

Dependencies added: async, stm

Dependency ranges changed: QuickCheck, sbv, template-haskell

API changes (from Hackage documentation)

Files

• CHANGELOG.md +58/−2
• LICENSE +1/−1
• README.md +14/−11
• grisette.cabal +70/−23
• src/Grisette.hs +0/−2
• src/Grisette/Backend/SBV.hs +0/−2
• src/Grisette/Backend/SBV/Data/SMT/Lowering.hs +86/−24
• src/Grisette/Backend/SBV/Data/SMT/Solving.hs +211/−258
• src/Grisette/Core.hs +67/−38
• src/Grisette/Core/Control/Exception.hs +5/−140
• src/Grisette/Core/Control/Monad/CBMCExcept.hs +13/−9
• src/Grisette/Core/Control/Monad/UnionM.hs +44/−96
• src/Grisette/Core/Control/Monad/UnionM.hs-boot +0/−31
• src/Grisette/Core/Data/BV.hs +58/−7
• src/Grisette/Core/Data/Class/BitVector.hs +0/−10
• src/Grisette/Core/Data/Class/Bool.hs +0/−413
• src/Grisette/Core/Data/Class/Bool.hs-boot +0/−36
• src/Grisette/Core/Data/Class/CEGISSolver.hs +222/−82
• src/Grisette/Core/Data/Class/Error.hs +88/−1
• src/Grisette/Core/Data/Class/Evaluate.hs +0/−241
• src/Grisette/Core/Data/Class/EvaluateSym.hs +286/−0
• src/Grisette/Core/Data/Class/ExtractSymbolics.hs +78/−31
• src/Grisette/Core/Data/Class/Function.hs +29/−0
• src/Grisette/Core/Data/Class/GPretty.hs +161/−112
• src/Grisette/Core/Data/Class/GenSym.hs +103/−39
• src/Grisette/Core/Data/Class/ITEOp.hs +88/−0
• src/Grisette/Core/Data/Class/LogicalOp.hs +106/−0
• src/Grisette/Core/Data/Class/Mergeable.hs +118/−113
• src/Grisette/Core/Data/Class/Mergeable.hs-boot +0/−28
• src/Grisette/Core/Data/Class/SEq.hs +306/−0
• src/Grisette/Core/Data/Class/SOrd.hs +279/−171
• src/Grisette/Core/Data/Class/SafeArith.hs +0/−444
• src/Grisette/Core/Data/Class/SafeDivision.hs +379/−0
• src/Grisette/Core/Data/Class/SafeLinearArith.hs +307/−0
• src/Grisette/Core/Data/Class/SafeSymRotate.hs +110/−0
• src/Grisette/Core/Data/Class/SafeSymShift.hs +190/−0
• src/Grisette/Core/Data/Class/SignConversion.hs +37/−0
• src/Grisette/Core/Data/Class/SimpleMergeable.hs +44/−22
• src/Grisette/Core/Data/Class/SimpleMergeable.hs-boot +0/−12
• src/Grisette/Core/Data/Class/Solvable.hs +10/−5
• src/Grisette/Core/Data/Class/Solver.hs +174/−54
• src/Grisette/Core/Data/Class/Substitute.hs +0/−289
• src/Grisette/Core/Data/Class/SubstituteSym.hs +318/−0
• src/Grisette/Core/Data/Class/SymRotate.hs +64/−0
• src/Grisette/Core/Data/Class/SymShift.hs +73/−0
• src/Grisette/Core/Data/Class/ToCon.hs +133/−26
• src/Grisette/Core/Data/Class/ToSym.hs +150/−23
• src/Grisette/Core/Data/FileLocation.hs +4/−3
• src/Grisette/Core/Data/Union.hs +100/−71
• src/Grisette/Experimental/GenSymConstrained.hs +8/−8
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs +50/−43
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/InternedCtors.hs-boot +33/−34
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs +97/−92
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/Term.hs-boot +41/−50
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermSubstitution.hs +18/−12
• src/Grisette/IR/SymPrim/Data/Prim/InternedTerm/TermUtils.hs +42/−28
• src/Grisette/IR/SymPrim/Data/Prim/Model.hs +20/−22
• src/Grisette/IR/SymPrim/Data/Prim/Model.hs-boot +0/−15
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/BV.hs +40/−70
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Bits.hs +90/−38
• src/Grisette/IR/SymPrim/Data/Prim/PartialEval/Num.hs +10/−0
• src/Grisette/IR/SymPrim/Data/SymPrim.hs +153/−665
• src/Grisette/IR/SymPrim/Data/SymPrim.hs-boot +0/−136
• src/Grisette/IR/SymPrim/Data/TabularFun.hs-boot +0/−22
• src/Grisette/Lib/Base.hs +6/−6
• src/Grisette/Lib/Control/Monad.hs +8/−8
• src/Grisette/Lib/Control/Monad.hs-boot +4/−4
• src/Grisette/Lib/Control/Monad/State/Class.hs +74/−0
• src/Grisette/Lib/Control/Monad/Trans.hs +3/−15
• src/Grisette/Lib/Control/Monad/Trans/Class.hs +31/−0
• src/Grisette/Lib/Control/Monad/Trans/State.hs +17/−0
• src/Grisette/Lib/Control/Monad/Trans/State/Lazy.hs +131/−0
• src/Grisette/Lib/Control/Monad/Trans/State/Strict.hs +131/−0
• src/Grisette/Lib/Data/List.hs +8/−8
• src/Grisette/Lib/Mtl.hs +0/−37
• test/Grisette/Backend/SBV/Data/SMT/CEGISTests.hs +292/−303
• test/Grisette/Backend/SBV/Data/SMT/LoweringTests.hs +50/−84
• test/Grisette/Backend/SBV/Data/SMT/TermRewritingGen.hs +112/−65
• test/Grisette/Backend/SBV/Data/SMT/TermRewritingTests.hs +94/−10
• test/Grisette/Core/Control/ExceptionTests.hs +168/−0
• test/Grisette/Core/Control/Monad/UnionMTests.hs +818/−10
• test/Grisette/Core/Control/Monad/UnionTests.hs +839/−0
• test/Grisette/Core/Data/BVTests.hs +9/−2
• test/Grisette/Core/Data/Class/BoolTests.hs +77/−0
• test/Grisette/Core/Data/Class/EvaluateSymTests.hs +929/−0
• test/Grisette/Core/Data/Class/ExtractSymbolicsTests.hs +264/−0
• test/Grisette/Core/Data/Class/GPrettyTests.hs +4/−4
• test/Grisette/Core/Data/Class/GenSymTests.hs +1265/−0
• test/Grisette/Core/Data/Class/MergeableTests.hs +1083/−0
• test/Grisette/Core/Data/Class/SEqTests.hs +715/−0
• test/Grisette/Core/Data/Class/SOrdTests.hs +1383/−0
• test/Grisette/Core/Data/Class/SafeSymRotateTests.hs +301/−0
• test/Grisette/Core/Data/Class/SafeSymShiftTests.hs +371/−0
• test/Grisette/Core/Data/Class/SimpleMergeableTests.hs +678/−0
• test/Grisette/Core/Data/Class/SubstituteSymTests.hs +418/−0
• test/Grisette/Core/Data/Class/SymRotateTests.hs +168/−0
• test/Grisette/Core/Data/Class/SymShiftTests.hs +168/−0
• test/Grisette/Core/Data/Class/TestValues.hs +39/−0
• test/Grisette/Core/Data/Class/ToConTests.hs +482/−0
• test/Grisette/Core/Data/Class/ToSymTests.hs +380/−0
• test/Grisette/Core/Data/Class/UnionLikeTests.hs +298/−0
• test/Grisette/IR/SymPrim/Data/Prim/BVTests.hs +2/−1
• test/Grisette/IR/SymPrim/Data/Prim/BitsTests.hs +150/−65
• test/Grisette/IR/SymPrim/Data/Prim/BoolTests.hs +2/−1
• test/Grisette/IR/SymPrim/Data/Prim/IntegralTests.hs +2/−1
• test/Grisette/IR/SymPrim/Data/Prim/ModelTests.hs +2/−1
• test/Grisette/IR/SymPrim/Data/Prim/NumTests.hs +16/−6
• test/Grisette/IR/SymPrim/Data/Prim/TabularFunTests.hs +2/−1
• test/Grisette/IR/SymPrim/Data/SymPrimTests.hs +116/−87
• test/Grisette/IR/SymPrim/Data/TabularFunTests.hs +1/−1
• test/Grisette/Lib/Control/Monad/ExceptTests.hs +34/−0
• test/Grisette/Lib/Control/Monad/State/ClassTests.hs +36/−0
• test/Grisette/Lib/Control/Monad/Trans/ClassTests.hs +33/−0
• test/Grisette/Lib/Control/Monad/Trans/State/Common.hs +288/−0
• test/Grisette/Lib/Control/Monad/Trans/State/LazyTests.hs +52/−0
• test/Grisette/Lib/Control/Monad/Trans/State/StrictTests.hs +52/−0
• test/Grisette/Lib/Control/MonadTests.hs +64/−0
• test/Grisette/Lib/Data/FoldableTests.hs +130/−0
• test/Grisette/Lib/Data/TraversableTests.hs +112/−0
• test/Grisette/TestUtil/SymbolicAssertion.hs +29/−0
• test/Main.hs +101/−91

@@ -5,8 +5,54 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). -## [Unreleased]+## [0.4.0.0] -- 2024-01-08 +### Added++- Added wrappers for state transformers. ([#132](https://github.com/lsrcz/grisette/pull/132))+- Added `toGuardList` function. ([#137](https://github.com/lsrcz/grisette/pull/137))+- Exported some previously hidden API (`BVSignConversion`, `runFreshTFromIndex`) that we found useful or forgot to export. ([#138](https://github.com/lsrcz/grisette/pull/138), [#139](https://github.com/lsrcz/grisette/pull/139))+- Provided `mrgRunFreshT` to run `FreshT` with merging. ([#140](https://github.com/lsrcz/grisette/pull/140))+- Added `Grisette.Data.Class.SignConversion.SignConversion` for types from `Data.Int` and `Data.Word`. ([#142](https://github.com/lsrcz/grisette/pull/142))+- Added shift functions by symbolic shift amounts. ([#151](https://github.com/lsrcz/grisette/pull/151))+- Added `apply` for uninterpreted functions. ([#155](https://github.com/lsrcz/grisette/pull/155))+- Added `liftFresh` to lift a `Fresh` into `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/156))+- Added a handle types for SBV solvers. This allows users to use SBV solvers without the need to wrap everything in the SBV monads. ([#159](https://github.com/lsrcz/grisette/pull/159))+- Added a new generic CEGIS interface. This allows any verifier/fuzzer to be used in the CEGIS loop. ([#159](https://github.com/lsrcz/grisette/pull/159))++### Removed++- [Breaking] Removed the `Grisette.Lib.Mtl` module. ([#132](https://github.com/lsrcz/grisette/pull/132))+- [Breaking] Removed `SymBoolOp` and `SymIntegerOp`. ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Removed `ExtractSymbolics` instance for `SymbolSet`. ([#146](https://github.com/lsrcz/grisette/pull/146))++### Fixed++- Removed the quotation marks around the pretty printed results for string-like data types. ([#127](https://github.com/lsrcz/grisette/pull/127))+- Fixed the `SOrd` instance for `VerificationConditions`. ([#131](https://github.com/lsrcz/grisette/pull/131))+- Fixed the missing `SubstituteSym` instance for `UnionM`. ([#131](https://github.com/lsrcz/grisette/pull/131))+- Fixed the symbolic generation order for `Maybe`. ([#131](https://github.com/lsrcz/grisette/pull/131))+- Fixed the `toInteger` function for `IntN 1`. ([#143](https://github.com/lsrcz/grisette/pull/143))+- Fixed the `abs` function for `WordN`. ([#144](https://github.com/lsrcz/grisette/pull/143))+- Fixed the QuickCheck shrink function for `WordN 1` and `IntN 1`. ([#149](https://github.com/lsrcz/grisette/pull/149))+- Fixed the heap overflow bug for `shiftL` for `WordN` and `IntN` by large numbers. ([#150](https://github.com/lsrcz/grisette/pull/150))++### Changed++- Reorganized the files for `MonadTrans`. ([#132](https://github.com/lsrcz/grisette/pull/132))+- [Breaking] Changed the name of `Union` constructors and patterns. ([#133](https://github.com/lsrcz/grisette/pull/133))+- The `Union` patterns, when used as constructors, now merges the result. ([#133](https://github.com/lsrcz/grisette/pull/133))+- Changed the symbolic identifier type from `String` to `Data.Text.Text`. ([#141](https://github.com/lsrcz/grisette/pull/141))+- [Breaking] `Grisette.Data.Class.BitVector.BVSignConversion` is now `Grisette.Data.Class.SignConversion.SignConversion`. ([#142](https://github.com/lsrcz/grisette/pull/142))+- [Breaking] Moved the `ITEOp`, `LogicalOp`, and `SEq` type classes to dedicated modules. ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Moved `Grisette.Data.Class.Evaluate` to `Grisette.Data.Class.EvaluateSym`. ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Moved `Grisette.Data.Class.Substitute` to `Grisette.Data.Class.SubstituteSym`. ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Split the `Grisette.Data.Class.SafeArith` module to `Grisette.Data.Class.SafeDivision` and `Grisette.Data.Class.SafeLinearArith`. ([#146](https://github.com/lsrcz/grisette/pull/146))+- [Breaking] Changed the API to `MonadFresh`. ([#156](https://github.com/lsrcz/grisette/pull/156))+- [Breaking] Renamed multiple symbolic operators. ([#158](https://github.com/lsrcz/grisette/pull/158))+- [Breaking] Changed the solver interface. ([#159](https://github.com/lsrcz/grisette/pull/159))+- [Breaking] Changed the CEGIS solver interface. ([#159](https://github.com/lsrcz/grisette/pull/159))+ ## [0.3.1.1] -- 2023-09-29  No user-facing changes.@@ -14,17 +60,20 @@ ## [0.3.1.0] -- 2023-07-19  ### Added+ - Added support to `Data.Text`. ([#95](https://github.com/lsrcz/grisette/pull/95)) - Added `Arbitrary` instances for bit vectors. ([#97](https://github.com/lsrcz/grisette/pull/97)) - Added pretty printers for Grisette data types. ([#101](https://github.com/lsrcz/grisette/pull/101)) - Added `ExtractSymbolics` instances for tuples longer than 2. ([#103](https://github.com/lsrcz/grisette/pull/103))  ### Fixed+ - Fixed the `Read` instance for bit vectors. ([#99](https://github.com/lsrcz/grisette/pull/99), [#100](https://github.com/lsrcz/grisette/pull/100))  ## [0.3.0.0] -- 2023-07-07  ### Added+ - Added the conversion between signed and unsigned bit vectors. ([#69](https://github.com/lsrcz/grisette/pull/69)) - Added the generation of `SomeSymIntN` and `SomeSymWordN` from a single `Int` for bit width. ([#73](https://github.com/lsrcz/grisette/pull/73)) - Added the `FiniteBits` instance for `SomeSymIntN` and `SomeSymWordN`. ([#83](https://github.com/lsrcz/grisette/pull/83))@@ -32,10 +81,12 @@ - Added an experimental `GenSymConstrained` type class. ([#89](https://github.com/lsrcz/grisette/pull/89))  ### Changed+ - Changed the operations for `SomeIntN` and `SomeWordN` to accepting dynamic runtime integers rather than compile-time integers. ([#71](https://github.com/lsrcz/grisette/pull/71)) - Comparing the equality of `SomeIntN`/`SomeWordN`/`SomeSymIntN`/`SomeSymWordN` with different bit widths returns false rather than crash now. ([#74](https://github.com/lsrcz/grisette/pull/74))  ### Fixed+ - Fixed the compatibility issue with sbv 10+. ([#66](https://github.com/lsrcz/grisette/pull/66)) - Fixed build error with newer GHC. ([#70](https://github.com/lsrcz/grisette/pull/70)) - Fixed the merging for `SomeSymIntN` and `SomeSymWordN`. ([#72](https://github.com/lsrcz/grisette/pull/72))@@ -43,6 +94,7 @@ ## [0.2.0.0] - 2023-04-13  ### Added+ - Add term size count API. ([#48](https://github.com/lsrcz/grisette/pull/48), [#53](https://github.com/lsrcz/grisette/pull/53)) - Add timeout to solver interface. ([#49](https://github.com/lsrcz/grisette/pull/49), [#50](https://github.com/lsrcz/grisette/pull/50)) - Add parallel do-notation for parallel symbolic compilation. ([#51](https://github.com/lsrcz/grisette/pull/51))@@ -50,15 +102,18 @@ - Add missing instances for `MonadFresh` and `FreshT`. ([#59](https://github.com/lsrcz/grisette/pull/59))  ### Changed+ - New safe operator interfaces. ([#56](https://github.com/lsrcz/grisette/pull/56)) - Redesigned symbolic value interface.   - `Sym Bool`/`Sym Integer`, etc., are no longer available and are replaced with `SymBool` and `SymInteger`. ([#41](https://github.com/lsrcz/grisette/pull/41))   - New symbolic bit vector interface. Added unsized bit vector. ([#41](https://github.com/lsrcz/grisette/pull/41))  ### Removed+ - Dropped merging cache for `UnionM`. This fixed some segmentation fault errors. ([#43](https://github.com/lsrcz/grisette/pull/43))  ### Fixed+ - Fix CEGIS when no symbolic input is present. ([#52](https://github.com/lsrcz/grisette/pull/52)) - Fix overlapping `ToSym` and `ToCon` instances. ([#54](https://github.com/lsrcz/grisette/pull/54)) - Fix uninterpreted function lowering. ([#57](https://github.com/lsrcz/grisette/pull/57), [#58](https://github.com/lsrcz/grisette/pull/58))@@ -67,9 +122,10 @@ ## [0.1.0.0] - 2023-01-20  ### Added+ - Initial release for Grisette. -[Unreleased]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...HEAD+[0.4.0.0]: https://github.com/lsrcz/grisette/compare/v0.4.0.0...v0.3.1.0 [0.3.1.1]: https://github.com/lsrcz/grisette/compare/v0.3.1.0...v0.3.1.1 [0.3.1.0]: https://github.com/lsrcz/grisette/compare/v0.3.0.0...v0.3.1.0 [0.3.0.0]: https://github.com/lsrcz/grisette/compare/v0.2.0.0...v0.3.0.0

@@ -1,4 +1,4 @@-Copyright (c) 2021-2023, Sirui Lu (siruilu@cs.washington.edu)+Copyright (c) 2021-2024, Sirui Lu (siruilu@cs.washington.edu)  All rights reserved. 

@@ -12,10 +12,10 @@ ## Features  - **Multi-path** symbolic evaluation with efficient (customizable) state merging.-- Symbolic evaluation is **purely functional**. The propagated symbolic value includes the assertion / error state of the execution, yet it is just a data structure. As a result, Grisette is a library that does not modify the Haskell compiler.  -- The separation of symbolic and concrete values is enforced with **static types**. These types help discover opportunities for partial evaluation as well as safe use of Haskell libraries. +- Symbolic evaluation is **purely functional**. The propagated symbolic value includes the assertion / error state of the execution, yet it is just a data structure. As a result, Grisette is a library that does not modify the Haskell compiler.+- The separation of symbolic and concrete values is enforced with **static types**. These types help discover opportunities for partial evaluation as well as safe use of Haskell libraries. -## Design and Benefits +## Design and Benefits  - Modular purely functional design, with a focus on composability.   - Allows for symbolic evaluation of user-defined data structures / data@@ -47,7 +47,7 @@ ```cabal library   ...-  build-depends: grisette >= 0.3 < 0.4+  build-depends: grisette >= 0.4 < 0.5 ```  #### Quick start template with `stack new`@@ -79,7 +79,7 @@  ### Install SMT Solvers -To run the examples, you also need to install an SMT solver and make it +To run the examples, you also need to install an SMT solver and make it available through `PATH`. We recommend that you start with [Z3](https://github.com/Z3Prover/z3), as it supports all our examples and is usually easier to install.@@ -114,17 +114,17 @@  ## Example -The following example uses Grisette to build a synthesizer of arithmetic programs. Given the input-output pair (2,5), the synthesizer may output the program (\x -> x+3).  The example is adapted from [this blog+The following example uses Grisette to build a synthesizer of arithmetic programs. Given the input-output pair (2,5), the synthesizer may output the program (\x -> x+3). The example is adapted from [this blog post](https://www.cs.utexas.edu/~bornholt/post/building-synthesizer.html) by James Bornholt. - The example has three parts:+ - We define the arithmetic language. The language is _symbolic_:   - its syntax tree represents a set of concrete syntax trees, and-  - its interpreter accepts such symbolic syntax trees, and interprete at once all represented concrete syntax trees. -- We define the candidate program space of the synthesizer by creating a particular symbolic syntax tree. The synthesizer will search the space of concrete trees for a solution. -- We interpret the symbolic syntax tree and pass the resulting constraints to the solver. If a solution exists, the solver returns a concrete tree that agrees with the input-out example. +  - its interpreter accepts such symbolic syntax trees, and interprete at once all represented concrete syntax trees.+- We define the candidate program space of the synthesizer by creating a particular symbolic syntax tree. The synthesizer will search the space of concrete trees for a solution.+- We interpret the symbolic syntax tree and pass the resulting constraints to the solver. If a solution exists, the solver returns a concrete tree that agrees with the input-out example.  ### Defining the Arithmetic Language @@ -183,6 +183,7 @@ -- UMrg (Single (SConst 1)) $(makeUnionWrapper "mrg" ''SExpr) ```+ Then we can define the program space. The following code defines a program space `\x -> x + {x, c}`. Some example programs in this space are `\x -> x + x`, `\x -> x + 1`, and `\x -> x + 2`.@@ -239,15 +240,17 @@  ## Documentation -- Haddock documentation at  [grisette](https://hackage.haskell.org/package/grisette).+- Haddock documentation at [grisette](https://hackage.haskell.org/package/grisette). - Grisette essentials (WIP). - Grisette tutorials (WIP).  ## License+ The Grisette library is distributed under the terms of the BSD3 license. The [LICENSE](LICENSE) file contains the full license text.  ## Citing Grisette+ If you use Grisette in your research, please use the following bibtex entry:  ```bibtex

@@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.35.2.+-- This file has been generated from package.yaml by hpack version 0.36.0. -- -- see: https://github.com/sol/hpack  name:           grisette-version:        0.3.1.1+version:        0.4.0.0 synopsis:       Symbolic evaluation as a library description:    Grisette is a reusable symbolic evaluation library for Haskell. By                 translating programs into constraints, Grisette can help the development of@@ -20,7 +20,7 @@ bug-reports:    https://github.com/lsrcz/grisette/issues author:         Sirui Lu, Rastislav Bodík maintainer:     Sirui Lu (siruilu@cs.washington.edu)-copyright:      2021-2023 Sirui Lu+copyright:      2021-2024 Sirui Lu license:        BSD3 license-file:   LICENSE build-type:     Simple@@ -28,8 +28,8 @@     GHC == 8.10.7   , GHC == 9.0.2   , GHC == 9.2.8-  , GHC == 9.4.6-  , GHC == 9.6.2+  , GHC == 9.4.8+  , GHC == 9.6.3 extra-source-files:     CHANGELOG.md     README.md@@ -38,7 +38,7 @@   type: git   location: https://github.com/lsrcz/grisette -flag fast+flag optimize   description: Compile with O2 optimization   manual: False   default: True@@ -59,22 +59,30 @@       Grisette.Core.Control.Monad.UnionM       Grisette.Core.Data.BV       Grisette.Core.Data.Class.BitVector-      Grisette.Core.Data.Class.Bool       Grisette.Core.Data.Class.CEGISSolver       Grisette.Core.Data.Class.Error-      Grisette.Core.Data.Class.Evaluate+      Grisette.Core.Data.Class.EvaluateSym       Grisette.Core.Data.Class.ExtractSymbolics       Grisette.Core.Data.Class.Function       Grisette.Core.Data.Class.GenSym       Grisette.Core.Data.Class.GPretty+      Grisette.Core.Data.Class.ITEOp+      Grisette.Core.Data.Class.LogicalOp       Grisette.Core.Data.Class.Mergeable       Grisette.Core.Data.Class.ModelOps-      Grisette.Core.Data.Class.SafeArith+      Grisette.Core.Data.Class.SafeDivision+      Grisette.Core.Data.Class.SafeLinearArith+      Grisette.Core.Data.Class.SafeSymRotate+      Grisette.Core.Data.Class.SafeSymShift+      Grisette.Core.Data.Class.SEq+      Grisette.Core.Data.Class.SignConversion       Grisette.Core.Data.Class.SimpleMergeable       Grisette.Core.Data.Class.Solvable       Grisette.Core.Data.Class.Solver       Grisette.Core.Data.Class.SOrd-      Grisette.Core.Data.Class.Substitute+      Grisette.Core.Data.Class.SubstituteSym+      Grisette.Core.Data.Class.SymRotate+      Grisette.Core.Data.Class.SymShift       Grisette.Core.Data.Class.ToCon       Grisette.Core.Data.Class.ToSym       Grisette.Core.Data.FileLocation@@ -113,12 +121,16 @@       Grisette.Lib.Base       Grisette.Lib.Control.Monad       Grisette.Lib.Control.Monad.Except+      Grisette.Lib.Control.Monad.State.Class       Grisette.Lib.Control.Monad.Trans+      Grisette.Lib.Control.Monad.Trans.Class       Grisette.Lib.Control.Monad.Trans.Cont+      Grisette.Lib.Control.Monad.Trans.State+      Grisette.Lib.Control.Monad.Trans.State.Lazy+      Grisette.Lib.Control.Monad.Trans.State.Strict       Grisette.Lib.Data.Foldable       Grisette.Lib.Data.List       Grisette.Lib.Data.Traversable-      Grisette.Lib.Mtl       Grisette.Qualified.ParallelUnionDo       Grisette.Utils       Grisette.Utils.Parameterized@@ -128,8 +140,9 @@       src   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns   build-depends:-      QuickCheck >=2.13.2 && <2.15+      QuickCheck ==2.14.*     , array >=0.5.4 && <0.6+    , async >=2.2.2 && <2.3     , base >=4.14 && <5     , bytestring >=0.10.12 && <0.13     , deepseq >=1.4.4 && <1.6@@ -141,14 +154,15 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <10.3-    , template-haskell >=2.16 && <2.21+    , sbv >=8.11 && <10.4+    , stm ==2.5.*+    , template-haskell >=2.16 && <2.22     , text >=1.2.4.1 && <2.2     , th-compat >=0.1.2 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3   default-language: Haskell2010-  if flag(fast)+  if flag(optimize)     ghc-options: -O2   else     ghc-options: -O0@@ -163,8 +177,9 @@   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N   build-depends:       Glob-    , QuickCheck >=2.13.2 && <2.15+    , QuickCheck ==2.14.*     , array >=0.5.4 && <0.6+    , async >=2.2.2 && <2.3     , base >=4.14 && <5     , bytestring >=0.10.12 && <0.13     , deepseq >=1.4.4 && <1.6@@ -178,14 +193,15 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <10.3-    , template-haskell >=2.16 && <2.21+    , sbv >=8.11 && <10.4+    , stm ==2.5.*+    , template-haskell >=2.16 && <2.22     , text >=1.2.4.1 && <2.2     , th-compat >=0.1.2 && <0.2     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3   default-language: Haskell2010-  if flag(fast)+  if flag(optimize)     ghc-options: -O2   else     ghc-options: -O0@@ -198,9 +214,28 @@       Grisette.Backend.SBV.Data.SMT.LoweringTests       Grisette.Backend.SBV.Data.SMT.TermRewritingGen       Grisette.Backend.SBV.Data.SMT.TermRewritingTests+      Grisette.Core.Control.ExceptionTests       Grisette.Core.Control.Monad.UnionMTests+      Grisette.Core.Control.Monad.UnionTests       Grisette.Core.Data.BVTests+      Grisette.Core.Data.Class.BoolTests+      Grisette.Core.Data.Class.EvaluateSymTests+      Grisette.Core.Data.Class.ExtractSymbolicsTests+      Grisette.Core.Data.Class.GenSymTests       Grisette.Core.Data.Class.GPrettyTests+      Grisette.Core.Data.Class.MergeableTests+      Grisette.Core.Data.Class.SafeSymRotateTests+      Grisette.Core.Data.Class.SafeSymShiftTests+      Grisette.Core.Data.Class.SEqTests+      Grisette.Core.Data.Class.SimpleMergeableTests+      Grisette.Core.Data.Class.SOrdTests+      Grisette.Core.Data.Class.SubstituteSymTests+      Grisette.Core.Data.Class.SymRotateTests+      Grisette.Core.Data.Class.SymShiftTests+      Grisette.Core.Data.Class.TestValues+      Grisette.Core.Data.Class.ToConTests+      Grisette.Core.Data.Class.ToSymTests+      Grisette.Core.Data.Class.UnionLikeTests       Grisette.IR.SymPrim.Data.Prim.BitsTests       Grisette.IR.SymPrim.Data.Prim.BoolTests       Grisette.IR.SymPrim.Data.Prim.BVTests@@ -210,14 +245,25 @@       Grisette.IR.SymPrim.Data.Prim.TabularFunTests       Grisette.IR.SymPrim.Data.SymPrimTests       Grisette.IR.SymPrim.Data.TabularFunTests+      Grisette.Lib.Control.Monad.ExceptTests+      Grisette.Lib.Control.Monad.State.ClassTests+      Grisette.Lib.Control.Monad.Trans.ClassTests+      Grisette.Lib.Control.Monad.Trans.State.Common+      Grisette.Lib.Control.Monad.Trans.State.LazyTests+      Grisette.Lib.Control.Monad.Trans.State.StrictTests+      Grisette.Lib.Control.MonadTests+      Grisette.Lib.Data.FoldableTests+      Grisette.Lib.Data.TraversableTests+      Grisette.TestUtil.SymbolicAssertion       Paths_grisette   hs-source-dirs:       test   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -threaded -rtsopts -with-rtsopts=-N   build-depends:       HUnit ==1.6.*-    , QuickCheck >=2.13.2 && <2.15+    , QuickCheck ==2.14.*     , array >=0.5.4 && <0.6+    , async >=2.2.2 && <2.3     , base >=4.14 && <5     , bytestring >=0.10.12 && <0.13     , deepseq >=1.4.4 && <1.6@@ -230,8 +276,9 @@     , mtl >=2.2.2 && <2.4     , parallel >=3.2.2.0 && <3.3     , prettyprinter >=1.5.0 && <1.8-    , sbv >=8.11 && <10.3-    , template-haskell >=2.16 && <2.21+    , sbv >=8.11 && <10.4+    , stm ==2.5.*+    , template-haskell >=2.16 && <2.22     , test-framework >=0.8.2 && <0.9     , test-framework-hunit >=0.3.0.2 && <0.4     , test-framework-quickcheck2 >=0.3.0.5 && <0.4@@ -240,7 +287,7 @@     , transformers >=0.5.6 && <0.7     , unordered-containers >=0.2.11 && <0.3   default-language: Haskell2010-  if flag(fast)+  if flag(optimize)     ghc-options: -O2   else     ghc-options: -O0

@@ -15,7 +15,6 @@      -- * Core libraries     module Grisette.Lib.Base,-    module Grisette.Lib.Mtl,      -- * Symbolic primitives     module Grisette.IR.SymPrim,@@ -32,5 +31,4 @@ import Grisette.Core import Grisette.IR.SymPrim import Grisette.Lib.Base-import Grisette.Lib.Mtl import Grisette.Utils

@@ -20,7 +20,6 @@     withApprox,     clearApprox,     GrisetteSMTConfig (..),-    SolvingFailure (..),      -- * SBV backend solver configuration     SBV.SMTConfig (..),@@ -40,7 +39,6 @@   ( ApproximationConfig (..),     ExtraConfig (..),     GrisetteSMTConfig (..),-    SolvingFailure (..),     approx,     clearApprox,     clearTimeout,

@@ -6,6 +6,7 @@ {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE LambdaCase #-}+{-# LANGUAGE OverloadedStrings #-} {-# LANGUAGE PatternSynonyms #-} {-# LANGUAGE PolyKinds #-} {-# LANGUAGE QuantifiedConstraints #-}@@ -32,17 +33,22 @@   ) where +import Control.Monad.IO.Class (MonadIO)+import Control.Monad.Reader (MonadTrans (lift), ReaderT)+import Control.Monad.State (StateT) import Data.Bifunctor (Bifunctor (bimap, first, second)) import Data.Bits-  ( Bits (complement, rotate, shift, xor, (.&.), (.|.)),+  ( Bits (complement, xor, (.&.), (.|.)),   ) import Data.Dynamic (Typeable, fromDyn, toDyn) import Data.Foldable (Foldable (foldl'), asum) import Data.Kind (Type) import Data.Maybe (fromMaybe)+import Data.SBV (SIntegral, sRotateLeft, sRotateRight, sShiftLeft, sShiftRight) import qualified Data.SBV as SBV-import qualified Data.SBV.Control as SBVC import qualified Data.SBV.Internals as SBVI+import qualified Data.SBV.Trans as SBVT+import qualified Data.SBV.Trans.Control as SBVTC import Data.Type.Equality (type (~~)) import Data.Typeable (Proxy (Proxy), type (:~:) (Refl)) import GHC.Exts (sortWith)@@ -92,8 +98,6 @@         BVConcatTerm,         BVExtendTerm,         BVSelectTerm,-        BVToSignedTerm,-        BVToUnsignedTerm,         BinaryTerm,         ComplementBitsTerm,         ConTerm,@@ -113,13 +117,17 @@         QuotIntegralTerm,         RemBoundedIntegralTerm,         RemIntegralTerm,-        RotateBitsTerm,-        ShiftBitsTerm,+        RotateLeftTerm,+        RotateRightTerm,+        ShiftLeftTerm,+        ShiftRightTerm,         SignumNumTerm,         SymTerm,         TabularFunApplyTerm,         TernaryTerm,         TimesNumTerm,+        ToSignedTerm,+        ToUnsignedTerm,         UMinusNumTerm,         UnaryTerm,         XorBitsTerm@@ -620,12 +628,18 @@ class (Monad m) => SBVFreshMonad m where   sbvFresh :: (SBV.SymVal a) => String -> m (SBV.SBV a) -instance SBVFreshMonad SBV.Symbolic where-  sbvFresh = SBV.free+instance (MonadIO m) => SBVFreshMonad (SBVT.SymbolicT m) where+  sbvFresh = SBVT.free -instance SBVFreshMonad SBVC.Query where-  sbvFresh = SBVC.freshVar+instance (MonadIO m) => SBVFreshMonad (SBVTC.QueryT m) where+  sbvFresh = SBVTC.freshVar +instance (SBVFreshMonad m) => SBVFreshMonad (ReaderT r m) where+  sbvFresh = lift . sbvFresh++instance (SBVFreshMonad m) => SBVFreshMonad (StateT s m) where+  sbvFresh = lift . sbvFresh+ lowerUnaryTerm ::   forall integerBitWidth a a1 x x1 m.   (Typeable x1, a1 ~ TermTy integerBitWidth a, SupportedPrim x, HasCallStack, SBVFreshMonad m) =>@@ -774,30 +788,67 @@   case (config, R.typeRep @a) of     ResolvedBitsType -> lowerUnaryTerm config t arg complement m     _ -> translateUnaryError "complement" (R.typeRep @a) (R.typeRep @a)-lowerSinglePrimImpl config t@(ShiftBitsTerm _ arg n) m =+lowerSinglePrimImpl config t@(ShiftLeftTerm _ arg n) m =   case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm config t arg (`shift` n) m-    _ -> translateBinaryError "shift" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl config t@(RotateBitsTerm _ arg n) m =+    ResolvedBitsType -> lowerBinaryTerm config t arg n sShiftLeft m+    _ -> translateBinaryError "shiftLeft" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)+lowerSinglePrimImpl config t@(ShiftRightTerm _ arg n) m =   case (config, R.typeRep @a) of-    ResolvedBitsType -> lowerUnaryTerm config t arg (`rotate` n) m-    _ -> translateBinaryError "rotate" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)-lowerSinglePrimImpl config t@(BVToSignedTerm _ (bv :: Term x)) m =+    ResolvedBitsType -> lowerBinaryTerm config t arg n sShiftRight m+    _ -> translateBinaryError "shiftRight" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)+-- SBV's rotateLeft and rotateRight are broken for signed values, so we have to+-- do this+-- https://github.com/LeventErkok/sbv/issues/673+lowerSinglePrimImpl config t@(RotateLeftTerm _ arg n) m =+  case (config, R.typeRep @a) of+    (_, SignedBVType (Proxy :: Proxy n)) ->+      lowerBinaryTerm+        config+        t+        arg+        n+        ( \x y ->+            SBV.sFromIntegral $+              sRotateLeft+                (SBV.sFromIntegral x :: SBV.SWord n)+                (SBV.sFromIntegral y :: SBV.SWord n)+        )+        m+    ResolvedBitsType -> lowerBinaryTerm config t arg n sRotateLeft m+    _ -> translateBinaryError "rotateLeft" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)+lowerSinglePrimImpl config t@(RotateRightTerm _ arg n) m =+  case (config, R.typeRep @a) of+    (_, SignedBVType (Proxy :: Proxy n)) ->+      lowerBinaryTerm+        config+        t+        arg+        n+        ( \x y ->+            SBV.sFromIntegral $+              sRotateRight+                (SBV.sFromIntegral x :: SBV.SWord n)+                (SBV.sFromIntegral y :: SBV.SWord n)+        )+        m+    ResolvedBitsType -> lowerBinaryTerm config t arg n sRotateRight m+    _ -> translateBinaryError "rotateRight" (R.typeRep @a) (R.typeRep @Int) (R.typeRep @a)+lowerSinglePrimImpl config t@(ToSignedTerm _ (bv :: Term x)) m =   case (R.typeRep @a, R.typeRep @x) of     (SignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx)) ->       case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of         Just R.HRefl ->           lowerUnaryTerm config t bv SBV.sFromIntegral m-        _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)-    _ -> translateUnaryError "bvu2s" (R.typeRep @x) (R.typeRep @a)-lowerSinglePrimImpl config t@(BVToUnsignedTerm _ (bv :: Term x)) m =+        _ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)+    _ -> translateUnaryError "u2s" (R.typeRep @x) (R.typeRep @a)+lowerSinglePrimImpl config t@(ToUnsignedTerm _ (bv :: Term x)) m =   case (R.typeRep @a, R.typeRep @x) of     (UnsignedBVType (_ :: Proxy na), SignedBVType (_ :: Proxy nx)) ->       case R.eqTypeRep (R.typeRep @na) (R.typeRep @nx) of         Just R.HRefl ->           lowerUnaryTerm config t bv SBV.sFromIntegral m-        _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a)-    _ -> translateUnaryError "bvs2u" (R.typeRep @x) (R.typeRep @a)+        _ -> translateUnaryError "s2u" (R.typeRep @x) (R.typeRep @a)+    _ -> translateUnaryError "s2u" (R.typeRep @x) (R.typeRep @a) lowerSinglePrimImpl config t@(BVConcatTerm _ (bv1 :: Term x) (bv2 :: Term y)) m =   case (R.typeRep @a, R.typeRep @x, R.typeRep @y) of     (UnsignedBVType (_ :: Proxy na), UnsignedBVType (_ :: Proxy nx), UnsignedBVType (_ :: Proxy ny)) ->@@ -915,8 +966,17 @@ bvIsNonZeroFromGEq1 r1 = case unsafeAxiom :: w :~: 1 of   Refl -> r1 -#if MIN_VERSION_sbv(10,0,0)+#if MIN_VERSION_sbv(10,3,0) preprocessUIFuncs ::+  [(String, (Bool, SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->+  Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))]+preprocessUIFuncs =+  traverse+    (\case+      (a, (_, b, Right c)) -> Just (a, (b, c))+      _ -> Nothing)+#elif MIN_VERSION_sbv(10,0,0)+preprocessUIFuncs ::   [(String, (SBVI.SBVType, Either String ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] ->   Maybe [(String, (SBVI.SBVType, ([([SBVI.CV], SBVI.CV)], SBVI.CV)))] preprocessUIFuncs =@@ -1795,7 +1855,9 @@   ( SimpleTypeConstraint integerBitWidth s s',     Bits (SBV.SBV s'),     Bits s',-    Bits s+    Bits s,+    SIntegral s',+    Integral s   )  data DictBitsType integerBitWidth s where

@@ -1,13 +1,11 @@ {-# LANGUAGE DataKinds #-}-{-# LANGUAGE DeriveLift #-} {-# LANGUAGE DerivingStrategies #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}-{-# LANGUAGE GeneralizedNewtypeDeriving #-}-{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-}+{-# LANGUAGE RecordWildCards #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneKindSignatures #-} {-# LANGUAGE TypeFamilies #-}@@ -23,7 +21,11 @@ -- Stability   :   Experimental -- Portability :   GHC only module Grisette.Backend.SBV.Data.SMT.Solving-  ( ApproximationConfig (..),+  ( -- * Term type computation+    TermTy,++    -- * SBV backend configuration+    ApproximationConfig (..),     ExtraConfig (..),     precise,     approx,@@ -32,65 +34,76 @@     withApprox,     clearApprox,     GrisetteSMTConfig (..),-    SolvingFailure (..),-    TermTy,++    -- * SBV monadic solver interface+    SBVIncrementalT,+    SBVIncremental,+    runSBVIncrementalT,+    runSBVIncremental,++    -- * SBV solver handle+    SBVSolverHandle,   ) where -import Control.DeepSeq (NFData)-import Control.Exception (handle)-import Control.Monad.IO.Class (liftIO)-import qualified Data.HashSet as S-import Data.Hashable (Hashable)+import Control.Concurrent.Async (Async (asyncThreadId), async, wait)+import Control.Concurrent.STM+  ( TMVar,+    atomically,+    newTMVarIO,+    putTMVar,+    takeTMVar,+    tryReadTMVar,+    tryTakeTMVar,+  )+import Control.Concurrent.STM.TChan (TChan, newTChan, readTChan, writeTChan)+import Control.Exception (handle, throwTo)+import Control.Monad.IO.Class (MonadIO, liftIO)+import Control.Monad.Reader+  ( MonadReader (ask),+    MonadTrans (lift),+    ReaderT (runReaderT),+  )+import Control.Monad.STM (STM)+import Control.Monad.State (MonadState (get, put), StateT, evalStateT) import Data.Kind (Type)-import Data.List (partition)-import Data.Maybe (fromJust) import qualified Data.SBV as SBV-import Data.SBV.Control (Query) import qualified Data.SBV.Control as SBVC+import qualified Data.SBV.Trans as SBVT+import qualified Data.SBV.Trans.Control as SBVTC+import GHC.IO.Exception (ExitCode (ExitSuccess)) import GHC.TypeNats (KnownNat, Nat) import Grisette.Backend.SBV.Data.SMT.Lowering   ( SymBiMap,-    lowerSinglePrim,     lowerSinglePrimCached,     parseModel,   )+import Grisette.Backend.SBV.Data.SMT.SymBiMap (emptySymBiMap) import Grisette.Core.Data.BV (IntN, WordN)-import Grisette.Core.Data.Class.Bool (LogicalOp (nots, (&&~)))-import Grisette.Core.Data.Class.CEGISSolver-  ( CEGISCondition (CEGISCondition),-    CEGISSolver (cegisMultiInputs),-  )-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))-import Grisette.Core.Data.Class.ExtractSymbolics-  ( ExtractSymbolics (extractSymbolics),-  )-import Grisette.Core.Data.Class.ModelOps-  ( ModelOps (exact, exceptFor),-    SymbolSetOps (isEmptySet),-  )-import Grisette.Core.Data.Class.Solvable (Solvable (con))-import Grisette.Core.Data.Class.Solver (Solver (solve, solveAll, solveMulti))-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.InternedCtors-  ( conTerm,+import Grisette.Core.Data.Class.Solver+  ( ConfigurableSolver (newSolver),+    MonadicSolver+      ( monadicSolverPop,+        monadicSolverPush,+        monadicSolverSolve+      ),+    Solver+      ( solverForceTerminate,+        solverRunCommand,+        solverSolve,+        solverTerminate+      ),+    SolverCommand (SolverPop, SolverPush, SolverSolve, SolverTerminate),+    SolvingFailure (SolvingError, Terminated, Unk, Unsat),   ) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-  ( SomeTypedSymbol (SomeTypedSymbol),-    Term,-    type (-->),+  ( type (-->),   ) import Grisette.IR.SymPrim.Data.Prim.Model as PM   ( Model,-    SymbolSet (unSymbolSet),-    equation,   )-import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool-  ( pevalNotTerm,-    pevalOrTerm,-  ) import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool)) import Grisette.IR.SymPrim.Data.TabularFun (type (=->))-import Language.Haskell.TH.Syntax (Lift)  -- $setup -- >>> import Grisette.Core@@ -120,8 +133,8 @@  -- | Configures how to approximate unbounded values. ----- For example, if we use @'Approx' ('Data.Proxy' :: 'Data.Proxy' 4)@ to approximate the--- following unbounded integer:+-- For example, if we use @'Approx' ('Data.Proxy' :: 'Data.Proxy' 4)@ to+-- approximate the following unbounded integer: -- -- > (+ a 9) --@@ -136,8 +149,12 @@ -- more details. data ApproximationConfig (n :: Nat) where   NoApprox :: ApproximationConfig 0-  Approx :: (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) => p n -> ApproximationConfig n+  Approx ::+    (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) =>+    p n ->+    ApproximationConfig n +-- | Grisette specific extra configurations for the SBV backend. data ExtraConfig (i :: Nat) = ExtraConfig   { -- | Timeout in milliseconds for each solver call. CEGIS may call the     -- solver multiple times and each call has its own timeout.@@ -203,31 +220,36 @@ -- one, and should work well when no overflow is possible, in which case the -- performance can be improved with almost no cost. ----- We must note that the bounded translation is an approximation and is __/not/__--- __/sound/__. As the approximation happens only during the final translation,--- the symbolic evaluation may aggressively optimize the term based on the--- properties of mathematical integer arithmetic. This may cause the solver yield--- results that is incorrect under both unbounded or bounded semantics.+-- We must note that the bounded translation is an approximation and is+-- __/not sound/__. As the approximation happens only during the final+-- translation, the symbolic evaluation may aggressively optimize the term based+-- on the properties of mathematical integer arithmetic. This may cause the+-- solver yield results that is incorrect under both unbounded or bounded+-- semantics. -- -- The following is an example that is correct under bounded semantics, while is -- incorrect under the unbounded semantics: -- -- >>> :set -XTypeApplications -XOverloadedStrings -XDataKinds -- >>> let a = "a" :: SymInteger--- >>> solve (precise z3) $ a >~ 7 &&~ a <~ 9+-- >>> solve (precise z3) $ a .> 7 .&& a .< 9 -- Right (Model {a -> 8 :: Integer})--- >>> solve (approx (Proxy @4) z3) $ a >~ 7 &&~ a <~ 9+-- >>> solve (approx (Proxy @4) z3) $ a .> 7 .&& a .< 9 -- Left Unsat -- -- This may be avoided by setting an large enough reasoning precision to prevent -- overflows.-data GrisetteSMTConfig (i :: Nat) = GrisetteSMTConfig {sbvConfig :: SBV.SMTConfig, extraConfig :: ExtraConfig i}+data GrisetteSMTConfig (i :: Nat) = GrisetteSMTConfig+  { sbvConfig :: SBV.SMTConfig,+    extraConfig :: ExtraConfig i+  }  -- | A precise reasoning configuration with the given SBV solver configuration. precise :: SBV.SMTConfig -> GrisetteSMTConfig 0 precise config = GrisetteSMTConfig config preciseExtraConfig --- | An approximate reasoning configuration with the given SBV solver configuration.+-- | An approximate reasoning configuration with the given SBV solver+-- configuration. approx ::   forall p n.   (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) =>@@ -238,228 +260,159 @@  -- | Set the timeout for the solver configuration. withTimeout :: Int -> GrisetteSMTConfig i -> GrisetteSMTConfig i-withTimeout t config = config {extraConfig = (extraConfig config) {timeout = Just t}}+withTimeout t config =+  config {extraConfig = (extraConfig config) {timeout = Just t}}  -- | Clear the timeout for the solver configuration. clearTimeout :: GrisetteSMTConfig i -> GrisetteSMTConfig i-clearTimeout config = config {extraConfig = (extraConfig config) {timeout = Nothing}}+clearTimeout config =+  config {extraConfig = (extraConfig config) {timeout = Nothing}}  -- | Set the reasoning precision for the solver configuration.-withApprox :: (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) => p n -> GrisetteSMTConfig i -> GrisetteSMTConfig n-withApprox p config = config {extraConfig = (extraConfig config) {integerApprox = Approx p}}+withApprox ::+  (KnownNat n, IsZero n ~ 'False, SBV.BVIsNonZero n) =>+  p n ->+  GrisetteSMTConfig i ->+  GrisetteSMTConfig n+withApprox p config =+  config {extraConfig = (extraConfig config) {integerApprox = Approx p}}  -- | Clear the reasoning precision and perform precise reasoning with the -- solver configuration. clearApprox :: GrisetteSMTConfig i -> GrisetteSMTConfig 0-clearApprox config = config {extraConfig = (extraConfig config) {integerApprox = NoApprox}}--data SolvingFailure-  = DSat (Maybe String)-  | Unsat-  | Unk-  | ResultNumLimitReached-  | SolvingError SBV.SBVException-  deriving (Show)+clearApprox config =+  config {extraConfig = (extraConfig config) {integerApprox = NoApprox}}  sbvCheckSatResult :: SBVC.CheckSatResult -> SolvingFailure sbvCheckSatResult SBVC.Sat = error "Should not happen"-sbvCheckSatResult (SBVC.DSat msg) = DSat msg+sbvCheckSatResult (SBVC.DSat _) = error "DSat is currently not supported" sbvCheckSatResult SBVC.Unsat = Unsat sbvCheckSatResult SBVC.Unk = Unk -applyTimeout :: GrisetteSMTConfig i -> Query a -> Query a+-- | Apply the timeout to the configuration.+applyTimeout ::+  (MonadIO m, SBVTC.MonadQuery m) => GrisetteSMTConfig i -> m a -> m a applyTimeout config q = case timeout (extraConfig config) of   Nothing -> q-  Just t -> SBVC.timeout t q+  Just t -> SBVTC.timeout t q -solveTermWith ::-  forall integerBitWidth.-  GrisetteSMTConfig integerBitWidth ->-  Term Bool ->-  IO (Either SolvingFailure PM.Model)-solveTermWith config term =-  handle (return . Left . SolvingError) $-    SBV.runSMTWith (sbvConfig config) $ do-      (m, a) <- lowerSinglePrim config term-      SBVC.query $ applyTimeout config $ do-        SBV.constrain a-        r <- SBVC.checkSat-        case r of-          SBVC.Sat -> do-            md <- SBVC.getModel-            return (Right $ parseModel config md m)-          _ -> return (Left $ sbvCheckSatResult r)+-- | Incremental solver monad transformer with the SBV backend.+type SBVIncrementalT n m =+  ReaderT (GrisetteSMTConfig n) (StateT SymBiMap (SBVTC.QueryT m)) -instance Solver (GrisetteSMTConfig n) SolvingFailure where-  solve config (SymBool t) = solveTermWith config t-  solveMulti config n s@(SymBool t)-    | n > 0 =-        handle-          ( \(x :: SBV.SBVException) -> do-              print "An SBV Exception occurred:"-              print x-              print $-                "Warning: Note that solveMulti do not fully support "-                  ++ "timeouts, and will return an empty list if the solver"-                  ++ "timeouts in any iteration."-              return ([], SolvingError x)-          )-          $ SBV.runSMTWith (sbvConfig config)-          $ do-            (newm, a) <- lowerSinglePrim config t-            SBVC.query $ applyTimeout config $ do-              SBV.constrain a-              r <- SBVC.checkSat-              case r of-                SBVC.Sat -> do-                  md <- SBVC.getModel-                  let model = parseModel config md newm-                  remainingModels n model newm-                _ -> return ([], sbvCheckSatResult r)-    | otherwise = return ([], ResultNumLimitReached)-    where-      allSymbols = extractSymbolics s :: SymbolSet-      next :: PM.Model -> SymBiMap -> Query (SymBiMap, Either SBVC.CheckSatResult PM.Model)-      next md origm = do-        let newtm =-              S.foldl'-                (\acc (SomeTypedSymbol _ v) -> pevalOrTerm acc (pevalNotTerm (fromJust $ equation v md)))-                (conTerm False)-                (unSymbolSet allSymbols)-        (newm, lowered) <- lowerSinglePrimCached config newtm origm-        SBV.constrain lowered-        r <- SBVC.checkSat-        case r of-          SBVC.Sat -> do-            md1 <- SBVC.getModel-            let model = parseModel config md1 newm-            return (newm, Right model)-          _ -> return (newm, Left r)-      remainingModels :: Int -> PM.Model -> SymBiMap -> Query ([PM.Model], SolvingFailure)-      remainingModels n1 md origm-        | n1 > 1 = do-            (newm, r) <- next md origm-            case r of-              Left r -> return ([md], sbvCheckSatResult r)-              Right mo -> do-                (rmmd, e) <- remainingModels (n1 - 1) mo newm-                return (md : rmmd, e)-        | otherwise = return ([md], ResultNumLimitReached)-  solveAll = undefined+-- | Incremental solver monad with the SBV backend.+type SBVIncremental n = SBVIncrementalT n IO -instance CEGISSolver (GrisetteSMTConfig n) SolvingFailure where-  cegisMultiInputs ::-    forall inputs.-    (ExtractSymbolics inputs, EvaluateSym inputs) =>-    GrisetteSMTConfig n ->-    [inputs] ->-    (inputs -> CEGISCondition) ->-    IO ([inputs], Either SolvingFailure PM.Model)-  cegisMultiInputs config inputs func =-    case symInputs of-      [] -> do-        m <- solve config (cexesAssertFun conInputs)-        return (conInputs, m)-      _ ->-        handle-          ( \(x :: SBV.SBVException) -> do-              print "An SBV Exception occurred:"-              print x-              print $-                "Warning: Note that CEGIS procedures do not fully support "-                  ++ "timeouts, and will return an empty counter example list if "-                  ++ "the solver timeouts during guessing phase."-              return ([], Left $ SolvingError x)-          )-          $ go1 (cexesAssertFun conInputs) conInputs (error "Should have at least one gen") [] (con True) (con True) symInputs-    where-      (conInputs, symInputs) = partition (isEmptySet . extractSymbolics) inputs-      go1 :: SymBool -> [inputs] -> PM.Model -> [inputs] -> SymBool -> SymBool -> [inputs] -> IO ([inputs], Either SolvingFailure PM.Model)-      go1 cexFormula cexes previousModel inputs pre post remainingSymInputs = do-        case remainingSymInputs of-          [] -> return (cexes, Right previousModel)-          newInput : vs -> do-            let CEGISCondition nextPre nextPost = func newInput-            let finalPre = pre &&~ nextPre-            let finalPost = post &&~ nextPost-            r <- go cexFormula newInput (newInput : inputs) finalPre finalPost-            case r of-              (newCexes, Left failure) -> return (cexes ++ newCexes, Left failure)-              (newCexes, Right mo) -> do-                go1-                  (cexFormula &&~ cexesAssertFun newCexes)-                  (cexes ++ newCexes)-                  mo-                  (newInput : inputs)-                  finalPre-                  finalPost-                  vs-      cexAssertFun input =-        let CEGISCondition pre post = func input in pre &&~ post-      cexesAssertFun :: [inputs] -> SymBool-      cexesAssertFun = foldl (\acc x -> acc &&~ cexAssertFun x) (con True)-      go ::-        SymBool ->-        inputs ->-        [inputs] ->-        SymBool ->-        SymBool ->-        IO ([inputs], Either SolvingFailure PM.Model)-      go cexFormula inputs allInputs pre post =-        SBV.runSMTWith (sbvConfig config) $ do-          let SymBool t = phi &&~ cexFormula-          (newm, a) <- lowerSinglePrim config t-          SBVC.query $-            applyTimeout config $-              snd <$> do-                SBV.constrain a-                r <- SBVC.checkSat-                mr <- case r of-                  SBVC.Sat -> do-                    md <- SBVC.getModel-                    return $ Right $ parseModel config md newm-                  _ -> return $ Left $ sbvCheckSatResult r-                loop ((forallSymbols `exceptFor`) <$> mr) [] newm-        where-          forallSymbols :: SymbolSet-          forallSymbols = extractSymbolics allInputs-          phi = pre &&~ post-          negphi = pre &&~ nots post-          check :: Model -> IO (Either SolvingFailure (inputs, PM.Model))-          check candidate = do-            let evaluated = evaluateSym False candidate negphi-            r <- solve config evaluated-            return $ do-              m <- r-              let newm = exact forallSymbols m-              return (evaluateSym False newm inputs, newm)-          guess :: Model -> SymBiMap -> Query (SymBiMap, Either SolvingFailure PM.Model)-          guess candidate origm = do-            let SymBool evaluated = evaluateSym False candidate phi-            (newm, lowered) <- lowerSinglePrimCached config evaluated origm-            SBV.constrain lowered-            r <- SBVC.checkSat-            case r of-              SBVC.Sat -> do-                md <- SBVC.getModel-                let model = parseModel config md newm-                return (newm, Right $ exceptFor forallSymbols model)-              _ -> return (newm, Left $ sbvCheckSatResult r)-          loop ::-            Either SolvingFailure PM.Model ->-            [inputs] ->-            SymBiMap ->-            Query (SymBiMap, ([inputs], Either SolvingFailure PM.Model))-          loop (Right mo) cexes origm = do-            r <- liftIO $ check mo-            case r of-              Left Unsat -> return (origm, (cexes, Right mo))-              Left v -> return (origm, (cexes, Left v))-              Right (cex, cexm) -> do-                (newm, res) <- guess cexm origm-                loop res (cex : cexes) newm-          loop (Left v) cexes origm = return (origm, (cexes, Left v))+-- | Run the incremental solver monad with a given configuration.+runSBVIncremental :: GrisetteSMTConfig n -> SBVIncremental n a -> IO a+runSBVIncremental = runSBVIncrementalT -newtype CegisInternal = CegisInternal Int-  deriving (Eq, Show, Ord, Lift)-  deriving newtype (Hashable, NFData)+-- | Run the incremental solver monad transformer with a given configuration.+runSBVIncrementalT ::+  (SBVTC.ExtractIO m) =>+  GrisetteSMTConfig n ->+  SBVIncrementalT n m a ->+  m a+runSBVIncrementalT config sbvIncrementalT =+  SBVT.runSMTWith (sbvConfig config) $+    SBVTC.query $+      applyTimeout config $+        flip evalStateT emptySymBiMap $+          runReaderT sbvIncrementalT config++instance (MonadIO m) => MonadicSolver (SBVIncrementalT n m) where+  monadicSolverSolve (SymBool formula) = do+    symBiMap <- get+    config <- ask+    (newSymBiMap, lowered) <- lowerSinglePrimCached config formula symBiMap+    lift $ lift $ SBV.constrain lowered+    put newSymBiMap+    checkSatResult <- SBVTC.checkSat+    case checkSatResult of+      SBVC.Sat -> do+        sbvModel <- SBVTC.getModel+        let model = parseModel config sbvModel newSymBiMap+        return $ Right model+      r -> return $ Left $ sbvCheckSatResult r+  monadicSolverPush = SBVTC.push+  monadicSolverPop = SBVTC.pop++data SBVSolverStatus = SBVSolverNormal | SBVSolverTerminated++-- | The handle type for the SBV solver.+--+-- See 'ConfigurableSolver' and 'Solver' for the interfaces.+data SBVSolverHandle = SBVSolverHandle+  { sbvSolverHandleMonad :: Async (),+    sbvSolverHandleStatus :: TMVar SBVSolverStatus,+    sbvSolverHandleInChan :: TChan SolverCommand,+    sbvSolverHandleOutChan :: TChan (Either SolvingFailure Model)+  }++setTerminated :: TMVar SBVSolverStatus -> STM ()+setTerminated status = do+  _ <- tryTakeTMVar status+  putTMVar status SBVSolverTerminated++instance ConfigurableSolver (GrisetteSMTConfig n) SBVSolverHandle where+  newSolver config = do+    sbvSolverHandleInChan <- atomically newTChan+    sbvSolverHandleOutChan <- atomically newTChan+    sbvSolverHandleStatus <- newTMVarIO SBVSolverNormal+    sbvSolverHandleMonad <- async $ do+      let handler e =+            liftIO $+              atomically $ do+                setTerminated sbvSolverHandleStatus+                writeTChan sbvSolverHandleOutChan (Left (SolvingError e))+      handle handler $ runSBVIncremental config $ do+        let loop = do+              nextFormula <- liftIO $ atomically $ readTChan sbvSolverHandleInChan+              case nextFormula of+                SolverPush n -> monadicSolverPush n >> loop+                SolverPop n -> monadicSolverPop n >> loop+                SolverTerminate -> return ()+                SolverSolve formula -> do+                  r <- monadicSolverSolve formula+                  liftIO $ atomically $ writeTChan sbvSolverHandleOutChan r+                  loop+        loop+        liftIO $ atomically $ do+          setTerminated sbvSolverHandleStatus+          writeTChan sbvSolverHandleOutChan $ Left Terminated+    return $ SBVSolverHandle {..}++instance Solver SBVSolverHandle where+  solverRunCommand f handle@(SBVSolverHandle _ status inChan _) command = do+    st <- liftIO $ atomically $ takeTMVar status+    case st of+      SBVSolverNormal -> do+        liftIO $ atomically $ writeTChan inChan command+        r <- f handle+        liftIO $ atomically $ do+          currStatus <- tryReadTMVar status+          case currStatus of+            Nothing -> putTMVar status SBVSolverNormal+            Just _ -> return ()+        return r+      SBVSolverTerminated -> do+        liftIO $ atomically $ setTerminated status+        return $ Left Terminated+  solverSolve handle nextFormula =+    solverRunCommand+      ( \(SBVSolverHandle _ _ _ outChan) ->+          liftIO $ atomically $ readTChan outChan+      )+      handle+      $ SolverSolve nextFormula+  solverTerminate (SBVSolverHandle thread status inChan _) = do+    liftIO $ atomically $ do+      setTerminated status+      writeTChan inChan SolverTerminate+    wait thread+  solverForceTerminate (SBVSolverHandle thread status _ outChan) = do+    liftIO $ atomically $ do+      setTerminated status+      writeTChan outChan (Left Terminated)+    throwTo (asyncThreadId thread) ExitSuccess+    wait thread

@@ -166,7 +166,7 @@     --     -- >>> let a = "a" :: SymInteger     -- >>> let b = "b" :: SymInteger-    -- >>> a ==~ b+    -- >>> a .== b     -- (= a b)      -- *** Creation of solvable type values@@ -181,16 +181,16 @@     LogicalOp (..),     ITEOp (..),     SEq (..),-    SymBoolOp,     SOrd (..),     BV (..),     bvExtract,     SizedBV (..),     sizedBVExtract,+    SignConversion (..),     SafeDivision (..),     SafeLinearArith (..),-    SymIntegerOp,     Function (..),+    Apply (..),      -- ** Unsolvable types @@ -600,8 +600,8 @@     merge,     mrgSingle,     UnionPrjOp (..),-    pattern SingleU,-    pattern IfU,+    pattern Single,+    pattern If,     MonadUnion,     MonadParallelUnion (..),     simpleMerge,@@ -609,7 +609,7 @@     onUnion2,     onUnion3,     onUnion4,-    (#~),+    (.#),      -- * Conversion between Concrete and Symbolic values     ToCon (..),@@ -711,10 +711,13 @@      -- ** Symbolic Generation Monad     MonadFresh (..),+    nextFreshIndex,+    liftFresh,     Fresh,-    FreshT,+    FreshT (..),     runFresh,     runFreshT,+    mrgRunFreshT,      -- ** Symbolic Generation Class     GenSym (..),@@ -749,7 +752,7 @@     -- for example, 'Grisette.Lib.Control.Monad.Except.mrgThrowError'.     --     -- >>> import Control.Monad.Except-    -- >>> import Grisette.Lib.Mtl+    -- >>> import Grisette.Lib.Control.Monad.Except     -- >>> mrgThrowError AssertionError :: ExceptT AssertionError UnionM ()     -- ExceptT {Left AssertionError}     --@@ -839,9 +842,9 @@     -- >>> import Grisette.Backend.SBV     -- >>> let x = "x" :: SymInteger     -- >>> let y = "y" :: SymInteger-    -- >>> solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)+    -- >>> solve (precise z3) (x + y .== 6 .&& x - y .== 20)     -- Right (Model {x -> 13 :: Integer, y -> -7 :: Integer})-    -- >>> solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 19)+    -- >>> solve (precise z3) (x + y .== 6 .&& x - y .== 19)     -- Left Unsat     --     -- The first parameter of 'solve' is the solver configuration.@@ -860,7 +863,7 @@     -- evaluate symbolic values. The following code evaluates the product of     -- x and y under the solution of the equation system.     ---    -- >>> Right m <- solve (precise z3) (x + y ==~ 6 &&~ x - y ==~ 20)+    -- >>> Right m <- solve (precise z3) (x + y .== 6 .&& x - y .== 20)     -- >>> evaluateSym False m (x * y)     -- -91     --@@ -918,7 +921,7 @@     --   res :: ExceptT Error UnionM ()     --   res = do     --     z <- x `sdiv` y-    --     mrgIf (z >~ 0) (assert (x >=~ y)) (return ())+    --     mrgIf (z .> 0) (assert (x .>= y)) (return ())     -- :}     --     -- Then we can ask the solver to find a counter-example that would lead to@@ -930,22 +933,38 @@     -- >>> res     -- ExceptT {If (|| (= y 0) (&& (< 0 (div x y)) (! (<= y x)))) (If (= y 0) (Left Arith) (Left Assert)) (Right ())}     ---    -- > >>> solveExcept (UnboundedReasoning z3) (==~ Left Assert) res+    -- > >>> solveExcept (UnboundedReasoning z3) (.== Left Assert) res     -- > Right (Model {x -> -6 :: Integer, y -> -3 :: Integer}) -- possible output     --     -- Grisette also provide implementation for counter-example guided inductive     -- synthesis (CEGIS) algorithm. See the documentation for 'CEGISSolver' for     -- more details. -    -- ** Solver interface+    -- ** Solver interfaces+    SolvingFailure (..),+    MonadicSolver (..),+    SolverCommand (..),+    ConfigurableSolver (..),     Solver (..),+    withSolver,+    solve,+    solveMulti,++    -- ** Union with exceptions     UnionWithExcept (..),     solveExcept,     solveMultiExcept, -    -- ** Counter-example Guided Inductive Synthesis (CEGIS)-    CEGISSolver (..),+    -- ** Generic Counter-example Guided Inductive Synthesis (CEGIS) interface+    SynthesisConstraintFun,+    VerifierResult (..),+    StatefulVerifierFun,+    CEGISResult (..),+    genericCEGIS,++    -- ** CEGIS interfaces with pre/post conditions     CEGISCondition (..),+    cegisMultiInputs,     cegisPostCond,     cegisPrePost,     cegis,@@ -1030,8 +1049,6 @@ import Grisette.Core.Control.Exception   ( AssertionError (..),     VerificationConditions (..),-    symAssert,-    symAssume,   ) import Grisette.Core.Control.Monad.CBMCExcept   ( CBMCEither (..),@@ -1049,7 +1066,7 @@     UnionM,     liftToMonadUnion,     unionSize,-    (#~),+    (.#),   ) import Grisette.Core.Data.Class.BitVector   ( BV (..),@@ -1057,15 +1074,12 @@     bvExtract,     sizedBVExtract,   )-import Grisette.Core.Data.Class.Bool-  ( ITEOp (..),-    LogicalOp (..),-    SEq (..),-    SymBoolOp,-  ) import Grisette.Core.Data.Class.CEGISSolver   ( CEGISCondition (..),-    CEGISSolver (..),+    CEGISResult (..),+    StatefulVerifierFun,+    SynthesisConstraintFun,+    VerifierResult (..),     cegis,     cegisExcept,     cegisExceptMultiInputs,@@ -1073,23 +1087,27 @@     cegisExceptStdVCMultiInputs,     cegisExceptVC,     cegisExceptVCMultiInputs,+    cegisMultiInputs,     cegisPostCond,     cegisPrePost,+    genericCEGIS,   ) import Grisette.Core.Data.Class.Error   ( TransformError (..),+    symAssert,     symAssertTransformableError,     symAssertWith,+    symAssume,     symThrowTransformableError,   )-import Grisette.Core.Data.Class.Evaluate+import Grisette.Core.Data.Class.EvaluateSym   ( EvaluateSym (..),     evaluateSymToCon,   ) import Grisette.Core.Data.Class.ExtractSymbolics   ( ExtractSymbolics (..),   )-import Grisette.Core.Data.Class.Function (Function (..))+import Grisette.Core.Data.Class.Function (Apply (..), Function (..)) import Grisette.Core.Data.Class.GPretty (GPretty (..)) import Grisette.Core.Data.Class.GenSym   ( EnumGenBound (..),@@ -1097,7 +1115,7 @@     Fresh,     FreshIdent (..),     FreshIndex (..),-    FreshT,+    FreshT (..),     GenSym (..),     GenSymSimple (..),     ListSpec (..),@@ -1114,11 +1132,16 @@     derivedSameShapeSimpleFresh,     genSym,     genSymSimple,+    liftFresh,+    mrgRunFreshT,     name,     nameWithInfo,+    nextFreshIndex,     runFresh,     runFreshT,   )+import Grisette.Core.Data.Class.ITEOp (ITEOp (..))+import Grisette.Core.Data.Class.LogicalOp (LogicalOp (..)) import Grisette.Core.Data.Class.Mergeable   ( DynamicSortedIdx (..),     Mergeable (..),@@ -1143,12 +1166,11 @@     SymbolSetOps (..),     SymbolSetRep (..),   )+import Grisette.Core.Data.Class.SEq (SEq (..)) import Grisette.Core.Data.Class.SOrd (SOrd (..))-import Grisette.Core.Data.Class.SafeArith-  ( SafeDivision (..),-    SafeLinearArith (..),-    SymIntegerOp,-  )+import Grisette.Core.Data.Class.SafeDivision (SafeDivision (..))+import Grisette.Core.Data.Class.SafeLinearArith (SafeLinearArith (..))+import Grisette.Core.Data.Class.SignConversion (SignConversion (..)) import Grisette.Core.Data.Class.SimpleMergeable   ( SimpleMergeable (..),     SimpleMergeable1 (..),@@ -1165,17 +1187,24 @@     onUnion3,     onUnion4,     simpleMerge,-    pattern IfU,-    pattern SingleU,+    pattern If,+    pattern Single,   ) import Grisette.Core.Data.Class.Solvable (Solvable (..), pattern Con) import Grisette.Core.Data.Class.Solver-  ( Solver (..),+  ( ConfigurableSolver (..),+    MonadicSolver (..),+    Solver (..),+    SolverCommand (..),+    SolvingFailure (..),     UnionWithExcept (..),+    solve,     solveExcept,+    solveMulti,     solveMultiExcept,+    withSolver,   )-import Grisette.Core.Data.Class.Substitute+import Grisette.Core.Data.Class.SubstituteSym   ( SubstituteSym (..),     SubstituteSym' (..),   )

@@ -4,7 +4,6 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE Trustworthy #-}  -- |@@ -19,39 +18,17 @@   ( -- * Predefined exceptions     AssertionError (..),     VerificationConditions (..),-    symAssert,-    symAssume,   ) where  import Control.DeepSeq (NFData)-import Control.Exception (ArithException, ArrayException)-import Control.Monad.Except (MonadError) import GHC.Generics (Generic)-import Generics.Deriving (Default (Default))-import Grisette.Core.Control.Monad.Union (MonadUnion)-import Grisette.Core.Data.Class.Bool (SEq)-import Grisette.Core.Data.Class.Error-  ( TransformError (transformError),-    symAssertTransformableError,-  )-import Grisette.Core.Data.Class.Evaluate (EvaluateSym)-import Grisette.Core.Data.Class.ExtractSymbolics-  ( ExtractSymbolics,-  )-import Grisette.Core.Data.Class.Mergeable (Mergeable)-import Grisette.Core.Data.Class.SOrd-  ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),-  )-import Grisette.Core.Data.Class.SimpleMergeable-  ( SimpleMergeable,-    mrgSingle,-  )-import Grisette.Core.Data.Class.Solvable (Solvable (con))-import Grisette.Core.Data.Class.ToCon (ToCon)-import Grisette.Core.Data.Class.ToSym (ToSym)-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool) +-- import Grisette.Core.Data.Class.Mergeable (Mergeable)+-- import Grisette.Core.Data.Class.SimpleMergeable+--   ( SimpleMergeable,+--   )+ -- $setup -- >>> import Grisette.Core -- >>> import Grisette.Lib.Base@@ -61,122 +38,10 @@ -- | Assertion error. data AssertionError = AssertionError   deriving (Show, Eq, Ord, Generic, NFData)-  deriving (ToCon AssertionError, ToSym AssertionError) via (Default AssertionError) -deriving via (Default AssertionError) instance Mergeable AssertionError--deriving via (Default AssertionError) instance SimpleMergeable AssertionError--deriving via (Default AssertionError) instance SEq AssertionError--instance SOrd AssertionError where-  _ <=~ _ = con True-  _ <~ _ = con False-  _ >=~ _ = con True-  _ >~ _ = con False-  _ `symCompare` _ = mrgSingle EQ--deriving via (Default AssertionError) instance EvaluateSym AssertionError--deriving via (Default AssertionError) instance ExtractSymbolics AssertionError- -- | Verification conditions. -- A crashed program path can terminate with either assertion violation errors or assumption violation errors. data VerificationConditions   = AssertionViolation   | AssumptionViolation   deriving (Show, Eq, Ord, Generic, NFData)-  deriving (ToCon VerificationConditions, ToSym VerificationConditions) via (Default VerificationConditions)--deriving via (Default VerificationConditions) instance Mergeable VerificationConditions--deriving via (Default VerificationConditions) instance SEq VerificationConditions--instance SOrd VerificationConditions where-  l >=~ r = con $ l <= r-  l >~ r = con $ l < r-  l <=~ r = con $ l >= r-  l <~ r = con $ l > r-  l `symCompare` r = mrgSingle $ l `compare` r--deriving via (Default VerificationConditions) instance EvaluateSym VerificationConditions--deriving via (Default VerificationConditions) instance ExtractSymbolics VerificationConditions--instance TransformError VerificationConditions VerificationConditions where-  transformError = id--instance TransformError AssertionError VerificationConditions where-  transformError _ = AssertionViolation--instance TransformError ArithException AssertionError where-  transformError _ = AssertionError--instance TransformError ArrayException AssertionError where-  transformError _ = AssertionError--instance TransformError AssertionError AssertionError where-  transformError = id---- | Used within a monadic multi path computation to begin exception processing.------ Checks the condition passed to the function.--- The current execution path will be terminated with assertion error if the condition is false.------ If the condition is symbolic, Grisette will split the execution into two paths based on the condition.--- The symbolic execution will continue on the then-branch, where the condition is true.--- For the else branch, where the condition is false, the execution will be terminated.------ The resulting monadic environment should be compatible with the 'AssertionError'--- error type. See 'TransformError' type class for details.------ __/Examples/__:------ Terminates the execution if the condition is false.--- Note that we may lose the 'Mergeable' knowledge here if no possible execution--- path is viable. This may affect the efficiency in theory, but in practice this--- should not be a problem as all paths are terminated and no further evaluation--- would be performed.------ >>> symAssert (con False) :: ExceptT AssertionError UnionM ()--- ExceptT {Left AssertionError}--- >>> do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError UnionM Integer--- ExceptT <Left AssertionError>------ No effect if the condition is true:------ >>> symAssert (con True) :: ExceptT AssertionError UnionM ()--- ExceptT {Right ()}--- >>> do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError UnionM Integer--- ExceptT {Right 1}------ Splitting the path and terminate one of them when the condition is symbolic.------ >>> symAssert (ssym "a") :: ExceptT AssertionError UnionM ()--- ExceptT {If (! a) (Left AssertionError) (Right ())}--- >>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError UnionM Integer--- ExceptT {If (! a) (Left AssertionError) (Right 1)}------ 'AssertionError' is compatible with 'VerificationConditions':------ >>> symAssert (ssym "a") :: ExceptT VerificationConditions UnionM ()--- ExceptT {If (! a) (Left AssertionViolation) (Right ())}-symAssert ::-  (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) =>-  SymBool ->-  erm ()-symAssert = symAssertTransformableError AssertionError---- | Used within a monadic multi path computation to begin exception processing.------ Similar to 'symAssert', but terminates the execution path with 'AssumptionViolation' error.------ /Examples/:------ >>> symAssume (ssym "a") :: ExceptT VerificationConditions UnionM ()--- ExceptT {If (! a) (Left AssumptionViolation) (Right ())}-symAssume ::-  (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) =>-  SymBool ->-  erm ()-symAssume = symAssertTransformableError AssumptionViolation

@@ -64,8 +64,8 @@ import Data.Functor.Contravariant (Contravariant (contramap)) import Data.Hashable (Hashable) import GHC.Generics (Generic, Generic1)-import Grisette.Core.Data.Class.Bool (SEq ((==~)))-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))+import Grisette.Core.Control.Monad.UnionM (UnionM)+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics   ( ExtractSymbolics (extractSymbolics),   )@@ -82,7 +82,8 @@     rootStrategy1,     wrapStrategy,   )-import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (<=~), (<~), (>=~), (>~)))+import Grisette.Core.Data.Class.SEq (SEq ((.==)))+import Grisette.Core.Data.Class.SOrd (SOrd (symCompare, (.<), (.<=), (.>), (.>=))) import Grisette.Core.Data.Class.SimpleMergeable   ( SimpleMergeable (mrgIte),     SimpleMergeable1 (liftMrgIte),@@ -350,8 +351,8 @@   {-# INLINE catchError #-}  instance (SEq (m (CBMCEither e a))) => SEq (CBMCExceptT e m a) where-  (CBMCExceptT a) ==~ (CBMCExceptT b) = a ==~ b-  {-# INLINE (==~) #-}+  (CBMCExceptT a) .== (CBMCExceptT b) = a .== b+  {-# INLINE (.==) #-}  instance (EvaluateSym (m (CBMCEither e a))) => EvaluateSym (CBMCExceptT e m a) where   evaluateSym fillDefault model (CBMCExceptT v) = CBMCExceptT $ evaluateSym fillDefault model v@@ -440,10 +441,10 @@   {-# INLINE unionIf #-}  instance (SOrd (m (CBMCEither e a))) => SOrd (CBMCExceptT e m a) where-  (CBMCExceptT l) <=~ (CBMCExceptT r) = l <=~ r-  (CBMCExceptT l) <~ (CBMCExceptT r) = l <~ r-  (CBMCExceptT l) >=~ (CBMCExceptT r) = l >=~ r-  (CBMCExceptT l) >~ (CBMCExceptT r) = l >~ r+  (CBMCExceptT l) .<= (CBMCExceptT r) = l .<= r+  (CBMCExceptT l) .< (CBMCExceptT r) = l .< r+  (CBMCExceptT l) .>= (CBMCExceptT r) = l .>= r+  (CBMCExceptT l) .> (CBMCExceptT r) = l .> r   symCompare (CBMCExceptT l) (CBMCExceptT r) = symCompare l r  instance@@ -469,3 +470,6 @@   UnionWithExcept (CBMCExceptT e u v) u e v   where   extractUnionExcept = merge . fmap runCBMCEither . runCBMCExceptT++instance UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v where+  extractUnionExcept = fmap runCBMCEither

@@ -33,7 +33,7 @@     liftToMonadUnion,     underlyingUnion,     isMerged,-    (#~),+    (.#),     IsConcrete,     unionSize,   )@@ -50,20 +50,12 @@ import Data.Hashable (Hashable (hashWithSalt)) import Data.String (IsString (fromString)) import GHC.TypeNats (KnownNat, type (<=))-import Grisette.Core.Control.Monad.CBMCExcept-  ( CBMCEither (runCBMCEither),-  ) import Grisette.Core.Control.Monad.Class.MonadParallelUnion   ( MonadParallelUnion (parBindUnion),   ) import Grisette.Core.Control.Monad.Union (MonadUnion) import Grisette.Core.Data.BV (IntN, WordN)-import Grisette.Core.Data.Class.Bool-  ( ITEOp (ites),-    LogicalOp (implies, nots, xors, (&&~), (||~)),-    SEq ((==~)),-  )-import Grisette.Core.Data.Class.Evaluate (EvaluateSym (evaluateSym))+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym (evaluateSym)) import Grisette.Core.Data.Class.ExtractSymbolics   ( ExtractSymbolics (extractSymbolics),   )@@ -72,18 +64,16 @@   ( GPretty (gpretty),     groupedEnclose,   )-import Grisette.Core.Data.Class.GenSym-  ( GenSym (fresh),-    GenSymSimple (simpleFresh),+import Grisette.Core.Data.Class.ITEOp (ITEOp (symIte))+import Grisette.Core.Data.Class.LogicalOp+  ( LogicalOp (symImplies, symNot, symXor, (.&&), (.||)),   ) import Grisette.Core.Data.Class.Mergeable   ( Mergeable (rootStrategy),     Mergeable1 (liftRootStrategy),     MergingStrategy (SimpleStrategy),   )-import Grisette.Core.Data.Class.SOrd-  ( SOrd (symCompare, (<=~), (<~), (>=~), (>~)),-  )+import Grisette.Core.Data.Class.SEq (SEq ((.==))) import Grisette.Core.Data.Class.SimpleMergeable   ( SimpleMergeable (mrgIte),     SimpleMergeable1 (liftMrgIte),@@ -93,17 +83,18 @@     mrgIf,     mrgSingle,     simpleMerge,-    (#~),+    (.#),   ) import Grisette.Core.Data.Class.Solvable   ( Solvable (con, conView, iinfosym, isym, sinfosym, ssym),     pattern Con,   ) import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))+import Grisette.Core.Data.Class.SubstituteSym (SubstituteSym (substituteSym)) import Grisette.Core.Data.Class.ToCon (ToCon (toCon)) import Grisette.Core.Data.Class.ToSym (ToSym (toSym)) import Grisette.Core.Data.Union-  ( Union (If, Single),+  ( Union (UnionIf, UnionSingle),     fullReconstruct,     ifWithStrategy,   )@@ -267,8 +258,8 @@   Int ->   Union a ->   ShowS-liftShowsPrecUnion sp _ i (Single a) = sp i a-liftShowsPrecUnion sp sl i (If _ _ cond t f) =+liftShowsPrecUnion sp _ i (UnionSingle a) = sp i a+liftShowsPrecUnion sp sl i (UnionIf _ _ cond t f) =   showParen (i > 10) $     showString "If"       . showChar ' '@@ -334,8 +325,8 @@   {-# INLINE (<*>) #-}  bindUnion :: Union a -> (a -> UnionM b) -> UnionM b-bindUnion (Single a') f' = f' a'-bindUnion (If _ _ cond ifTrue ifFalse) f' =+bindUnion (UnionSingle a') f' = f' a'+bindUnion (UnionIf _ _ cond ifTrue ifFalse) f' =   unionIf cond (bindUnion ifTrue f') (bindUnion ifFalse f') {-# INLINE bindUnion #-} @@ -344,12 +335,12 @@   {-# INLINE (>>=) #-}  parBindUnion'' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b-parBindUnion'' (Single a) f = merge $ f a+parBindUnion'' (UnionSingle a) f = merge $ f a parBindUnion'' u f = parBindUnion' u f  parBindUnion' :: (Mergeable b, NFData b) => Union a -> (a -> UnionM b) -> UnionM b-parBindUnion' (Single a') f' = f' a'-parBindUnion' (If _ _ cond ifTrue ifFalse) f' = runEval $ do+parBindUnion' (UnionSingle a') f' = f' a'+parBindUnion' (UnionIf _ _ cond ifTrue ifFalse) f' = runEval $ do   l <- rpar $ force $ parBindUnion' ifTrue f'   r <- rpar $ force $ parBindUnion' ifFalse f'   l' <- rseq l@@ -370,7 +361,8 @@   {-# INLINE mrgIte #-}  instance Mergeable1 UnionM where-  liftRootStrategy m = SimpleStrategy $ \cond t f -> unionIf cond t f >>= (UMrg m . Single)+  liftRootStrategy m = SimpleStrategy $+    \cond t f -> unionIf cond t f >>= (UMrg m . UnionSingle)   {-# INLINE liftRootStrategy #-}  instance SimpleMergeable1 UnionM where@@ -393,39 +385,17 @@   {-# INLINE unionIf #-}  instance (SEq a) => SEq (UnionM a) where-  x ==~ y = simpleMerge $ do+  x .== y = simpleMerge $ do     x1 <- x     y1 <- y-    mrgSingle $ x1 ==~ y1+    mrgSingle $ x1 .== y1  -- | Lift the 'UnionM' to any 'MonadUnion'. liftToMonadUnion :: (Mergeable a, MonadUnion u) => UnionM a -> u a liftToMonadUnion u = go (underlyingUnion u)   where-    go (Single v) = mrgSingle v-    go (If _ _ c t f) = mrgIf c (go t) (go f)--instance (SOrd a) => SOrd (UnionM a) where-  x <=~ y = simpleMerge $ do-    x1 <- x-    y1 <- y-    mrgSingle $ x1 <=~ y1-  x <~ y = simpleMerge $ do-    x1 <- x-    y1 <- y-    mrgSingle $ x1 <~ y1-  x >=~ y = simpleMerge $ do-    x1 <- x-    y1 <- y-    mrgSingle $ x1 >=~ y1-  x >~ y = simpleMerge $ do-    x1 <- x-    y1 <- y-    mrgSingle $ x1 >~ y1-  x `symCompare` y = liftToMonadUnion $ do-    x1 <- x-    y1 <- y-    x1 `symCompare` y1+    go (UnionSingle v) = mrgSingle v+    go (UnionIf _ _ c t f) = mrgIf c (go t) (go f)  instance {-# INCOHERENT #-} (ToSym a b, Mergeable b) => ToSym a (UnionM b) where   toSym = mrgSingle . toSym@@ -461,16 +431,16 @@ instance {-# INCOHERENT #-} (ToCon a b) => ToCon (UnionM a) b where   toCon v = go $ underlyingUnion v     where-      go (Single x) = toCon x+      go (UnionSingle x) = toCon x       go _ = Nothing  instance (ToCon a b, Mergeable b) => ToCon (UnionM a) (UnionM b) where   toCon v = go $ underlyingUnion v     where-      go (Single x) = case toCon x of+      go (UnionSingle x) = case toCon x of         Nothing -> Nothing         Just v -> Just $ mrgSingle v-      go (If _ _ c t f) = do+      go (UnionIf _ _ c t f) = do         t' <- go t         f' <- go f         return $ mrgIf c t' f'@@ -479,25 +449,23 @@   evaluateSym fillDefault model x = go $ underlyingUnion x     where       go :: Union a -> UnionM a-      go (Single v) = mrgSingle $ evaluateSym fillDefault model v-      go (If _ _ cond t f) =+      go (UnionSingle v) = mrgSingle $ evaluateSym fillDefault model v+      go (UnionIf _ _ cond t f) =         mrgIf           (evaluateSym fillDefault model cond)           (go t)           (go f) -{- instance (Mergeable a, SubstituteSym a) => SubstituteSym (UnionM a) where   substituteSym sym val x = go $ underlyingUnion x     where       go :: Union a -> UnionM a-      go (Single v) = mrgSingle $ substituteSym sym val v-      go (If _ _ cond t f) =+      go (UnionSingle v) = mrgSingle $ substituteSym sym val v+      go (UnionIf _ _ cond t f) =         mrgIf           (substituteSym sym val cond)           (go t)           (go f)-          -}  instance   (ExtractSymbolics a) =>@@ -505,8 +473,8 @@   where   extractSymbolics v = go $ underlyingUnion v     where-      go (Single x) = extractSymbolics x-      go (If _ _ cond t f) = extractSymbolics cond <> go t <> go f+      go (UnionSingle x) = extractSymbolics x+      go (UnionIf _ _ cond t f) = extractSymbolics cond <> go t <> go f  instance (Hashable a) => Hashable (UnionM a) where   s `hashWithSalt` (UAny u) = s `hashWithSalt` (0 :: Int) `hashWithSalt` u@@ -530,28 +498,28 @@   signum x = x >>= mrgSingle . signum  instance (ITEOp a, Mergeable a) => ITEOp (UnionM a) where-  ites = mrgIf+  symIte = mrgIf  instance (LogicalOp a, Mergeable a) => LogicalOp (UnionM a) where-  a ||~ b = do+  a .|| b = do     a1 <- a     b1 <- b-    mrgSingle $ a1 ||~ b1-  a &&~ b = do+    mrgSingle $ a1 .|| b1+  a .&& b = do     a1 <- a     b1 <- b-    mrgSingle $ a1 &&~ b1-  nots x = do+    mrgSingle $ a1 .&& b1+  symNot x = do     x1 <- x-    mrgSingle $ nots x1-  xors a b = do+    mrgSingle $ symNot x1+  symXor a b = do     a1 <- a     b1 <- b-    mrgSingle $ a1 `xors` b1-  implies a b = do+    mrgSingle $ a1 `symXor` b1+  symImplies a b = do     a1 <- a     b1 <- b-    mrgSingle $ a1 `implies` b1+    mrgSingle $ a1 `symImplies` b1  instance (Solvable c t, Mergeable t) => Solvable c (UnionM t) where   con = mrgSingle . con@@ -582,23 +550,6 @@ instance (IsString a, Mergeable a) => IsString (UnionM a) where   fromString = mrgSingle . fromString --- GenSym-instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a)--instance (GenSym spec a) => GenSymSimple spec (UnionM a) where-  simpleFresh spec = do-    res <- fresh spec-    if not (isMerged res) then error "Not merged" else return res--instance-  (GenSym a a, Mergeable a) =>-  GenSym (UnionM a) a-  where-  fresh spec = go (underlyingUnion $ merge spec)-    where-      go (Single x) = fresh x-      go (If _ _ _ t f) = mrgIf <$> simpleFresh () <*> go t <*> go f- -- AllSyms instance (AllSyms a) => AllSyms (UnionM a) where   allSymsS = allSymsS . underlyingUnion@@ -641,9 +592,6 @@ instance UnionWithExcept (UnionM (Either e v)) UnionM e v where   extractUnionExcept = id -instance UnionWithExcept (UnionM (CBMCEither e v)) UnionM e v where-  extractUnionExcept = fmap runCBMCEither- -- | The size of a union is defined as the number of branches. -- For example, --@@ -656,5 +604,5 @@ unionSize :: UnionM a -> Int unionSize = unionSize' . underlyingUnion   where-    unionSize' (Single _) = 1-    unionSize' (If _ _ _ l r) = unionSize' l + unionSize' r+    unionSize' (UnionSingle _) = 1+    unionSize' (UnionIf _ _ _ l r) = unionSize' l + unionSize' r

@@ -1,31 +0,0 @@-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}--module Grisette.Core.Control.Monad.UnionM (UnionM (..)) where--import Grisette.Core.Data.Class.Mergeable (MergingStrategy)-import Grisette.Core.Data.Class.SimpleMergeable (UnionLike)-import Grisette.Core.Data.Union (Union)--data UnionM a where-  -- | 'UnionM' with no 'Mergeable' knowledge.-  UAny ::-    -- | Original 'Union'.-    Union a ->-    UnionM a-  -- | 'UnionM' with 'Mergeable' knowledge.-  UMrg ::-    -- | Cached merging strategy.-    MergingStrategy a ->-    -- | Merged Union-    Union a ->-    UnionM a--instance UnionLike UnionM--instance Functor UnionM--instance Applicative UnionM--instance Monad UnionM

@@ -11,6 +11,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-} {-# LANGUAGE TemplateHaskellQuotes #-} {-# LANGUAGE TypeApplications #-} {-# LANGUAGE TypeOperators #-}@@ -108,9 +109,25 @@   ) import Grisette.Core.Data.Class.BitVector   ( BV (bvConcat, bvExt, bvSelect, bvSext, bvZext),-    BVSignConversion (toSigned, toUnsigned),-    SizedBV (sizedBVConcat, sizedBVExt, sizedBVSelect, sizedBVSext, sizedBVZext),+    SizedBV+      ( sizedBVConcat,+        sizedBVExt,+        sizedBVSelect,+        sizedBVSext,+        sizedBVZext+      ),   )+import Grisette.Core.Data.Class.SignConversion+  ( SignConversion (toSigned, toUnsigned),+  )+import Grisette.Core.Data.Class.SymRotate+  ( DefaultFiniteBitsSymRotate (DefaultFiniteBitsSymRotate),+    SymRotate,+  )+import Grisette.Core.Data.Class.SymShift+  ( DefaultFiniteBitsSymShift (DefaultFiniteBitsSymShift),+    SymShift,+  ) import Grisette.Utils.Parameterized   ( KnownProof (KnownProof),     LeqProof (LeqProof),@@ -372,9 +389,11 @@   bitSizeMaybe = Just . finiteBitSize   bitSize = finiteBitSize   isSigned _ = False+  shiftL w i | i >= finiteBitSize w = 0   shiftL (WordN a) i = WordN (a `shiftL` i) .&. maxBound    -- unsafeShiftL use default implementation+  shiftR w i | i >= finiteBitSize w = 0   shiftR (WordN a) i = WordN (a `shiftR` i)    -- unsafeShiftR use default implementation@@ -506,8 +525,14 @@  instance (KnownNat n, 1 <= n) => QC.Arbitrary (WordN n) where   arbitrary = QC.arbitrarySizedBoundedIntegral-  shrink = QC.shrinkIntegral +  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is+  -- not the case for 1-bit bit vector.+  shrink i+    | i == 0 = []+    | i == 1 = [0]+    | otherwise = QC.shrinkIntegral i+ minusOneIntN :: forall proxy n. (KnownNat n) => proxy n -> IntN n minusOneIntN _ = IntN (1 `shiftL` fromIntegral (natVal (Proxy :: Proxy n)) - 1) @@ -634,10 +659,10 @@         (q, r) -> (fromInteger q, fromInteger r)   toInteger i@(IntN n) = case signum i of     0 -> 0-    1 -> n     -1 ->       let x = negate i        in if signum x == -1 then -n else negate (toInteger x)+    1 -> n     _ -> undefined  instance Integral SomeIntN where@@ -687,8 +712,14 @@  instance (KnownNat n, 1 <= n) => QC.Arbitrary (IntN n) where   arbitrary = QC.arbitrarySizedBoundedIntegral-  shrink = QC.shrinkIntegral +  -- QC.shrinkIntegral assumes that 2 is representable by the number, which is+  -- not the case for 1-bit bit vector.+  shrink i+    | i == 0 = []+    | i == 1 = [0]+    | otherwise = QC.shrinkIntegral i+ instance SizedBV WordN where   sizedBVConcat :: forall l r. (KnownNat l, KnownNat r, 1 <= l, 1 <= r) => WordN l -> WordN r -> WordN (l + r)   sizedBVConcat (WordN a) (WordN b) = WordN ((a `shiftL` fromIntegral (natVal (Proxy :: Proxy r))) .|. b)@@ -784,10 +815,30 @@   bvSelect ix w = toSigned . bvSelect ix w . toUnsigned   {-# INLINE bvSelect #-} -instance (KnownNat n, 1 <= n) => BVSignConversion (WordN n) (IntN n) where+instance (KnownNat n, 1 <= n) => SignConversion (WordN n) (IntN n) where   toSigned (WordN i) = IntN i   toUnsigned (IntN i) = WordN i -instance BVSignConversion SomeWordN SomeIntN where+instance SignConversion SomeWordN SomeIntN where   toSigned (SomeWordN i) = SomeIntN $ toSigned i   toUnsigned (SomeIntN i) = SomeWordN $ toUnsigned i++deriving via+  (DefaultFiniteBitsSymShift (IntN n))+  instance+    (KnownNat n, 1 <= n) => SymShift (IntN n)++deriving via+  (DefaultFiniteBitsSymShift (WordN n))+  instance+    (KnownNat n, 1 <= n) => SymShift (WordN n)++deriving via+  (DefaultFiniteBitsSymRotate (IntN n))+  instance+    (KnownNat n, 1 <= n) => SymRotate (IntN n)++deriving via+  (DefaultFiniteBitsSymRotate (WordN n))+  instance+    (KnownNat n, 1 <= n) => SymRotate (WordN n)

@@ -1,7 +1,6 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE GADTs #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE RankNTypes #-}@@ -24,7 +23,6 @@     bvExtract,     SizedBV (..),     sizedBVExtract,-    BVSignConversion (..),   ) where @@ -234,11 +232,3 @@     (KnownProof, LeqProof, LeqProof) ->       sizedBVSelect (Proxy @j) (Proxy @(i - j + 1)) {-# INLINE sizedBVExtract #-}---- | Convert bitvectors from and to signed-class BVSignConversion ubv sbv | ubv -> sbv, sbv -> ubv where-  -- | Convert unsigned bitvector to signed-  toSigned :: ubv -> sbv--  -- | Convert signed bitvector to unsigned-  toUnsigned :: sbv -> ubv

@@ -1,413 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DerivingVia #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}---- |--- Module      :   Grisette.Core.Data.Class.Bool--- Copyright   :   (c) Sirui Lu 2021-2023--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Core.Data.Class.Bool-  ( -- * Symbolic equality-    SEq (..),-    SEq' (..),--    -- * Symbolic Boolean operations-    LogicalOp (..),-    SymBoolOp,-    ITEOp (..),-  )-where--import Control.Monad.Except (ExceptT (ExceptT))-import Control.Monad.Identity-  ( Identity (Identity),-    IdentityT (IdentityT),-  )-import Control.Monad.Trans.Maybe (MaybeT (MaybeT))-import qualified Control.Monad.Writer.Lazy as WriterLazy-import qualified Control.Monad.Writer.Strict as WriterStrict-import qualified Data.ByteString as B-import Data.Functor.Sum (Sum)-import Data.Int (Int16, Int32, Int64, Int8)-import qualified Data.Text as T-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, type (<=))-import Generics.Deriving-  ( Default (Default),-    Generic (Rep, from),-    K1 (K1),-    M1 (M1),-    U1,-    V1,-    type (:*:) ((:*:)),-    type (:+:) (L1, R1),-  )-import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)-import {-# SOURCE #-} Grisette.Core.Data.Class.SimpleMergeable-  ( SimpleMergeable,-  )-import Grisette.Core.Data.Class.Solvable (Solvable (con))-import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term-  ( LinkedRep,-    SupportedPrim,-  )-import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool-  ( pevalAndTerm,-    pevalITETerm,-    pevalImplyTerm,-    pevalNotTerm,-    pevalOrTerm,-    pevalXorTerm,-  )-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim-  ( SomeSymIntN,-    SomeSymWordN,-    SymBool (SymBool),-    SymIntN (SymIntN),-    SymInteger (SymInteger),-    SymWordN (SymWordN),-    binSomeSymIntNR1,-    binSomeSymWordNR1,-    type (-~>) (SymGeneralFun),-    type (=~>) (SymTabularFun),-  )---- $setup--- >>> import Grisette.Core--- >>> import Grisette.IR.SymPrim--- >>> :set -XDataKinds--- >>> :set -XBinaryLiterals--- >>> :set -XFlexibleContexts--- >>> :set -XFlexibleInstances--- >>> :set -XFunctionalDependencies---- | Auxiliary class for 'SEq' instance derivation-class SEq' f where-  -- | Auxiliary function for '(==~~) derivation-  (==~~) :: f a -> f a -> SymBool--  infix 4 ==~~--instance SEq' U1 where-  _ ==~~ _ = con True-  {-# INLINE (==~~) #-}--instance SEq' V1 where-  _ ==~~ _ = con True-  {-# INLINE (==~~) #-}--instance (SEq c) => SEq' (K1 i c) where-  (K1 a) ==~~ (K1 b) = a ==~ b-  {-# INLINE (==~~) #-}--instance (SEq' a) => SEq' (M1 i c a) where-  (M1 a) ==~~ (M1 b) = a ==~~ b-  {-# INLINE (==~~) #-}--instance (SEq' a, SEq' b) => SEq' (a :+: b) where-  (L1 a) ==~~ (L1 b) = a ==~~ b-  (R1 a) ==~~ (R1 b) = a ==~~ b-  _ ==~~ _ = con False-  {-# INLINE (==~~) #-}--instance (SEq' a, SEq' b) => SEq' (a :*: b) where-  (a1 :*: b1) ==~~ (a2 :*: b2) = (a1 ==~~ a2) &&~ (b1 ==~~ b2)-  {-# INLINE (==~~) #-}---- | Symbolic equality. Note that we can't use Haskell's 'Eq' class since--- symbolic comparison won't necessarily return a concrete 'Bool' value.------ >>> let a = 1 :: SymInteger--- >>> let b = 2 :: SymInteger--- >>> a ==~ b--- false--- >>> a /=~ b--- true------ >>> let a = "a" :: SymInteger--- >>> let b = "b" :: SymInteger--- >>> a /=~ b--- (! (= a b))--- >>> a /=~ b--- (! (= a b))------ __Note:__ This type class can be derived for algebraic data types.--- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.------ > data X = ... deriving Generic deriving SEq via (Default X)-class SEq a where-  (==~) :: a -> a -> SymBool-  a ==~ b = nots $ a /=~ b-  {-# INLINE (==~) #-}-  infix 4 ==~--  (/=~) :: a -> a -> SymBool-  a /=~ b = nots $ a ==~ b-  {-# INLINE (/=~) #-}-  infix 4 /=~-  {-# MINIMAL (==~) | (/=~) #-}--instance (Generic a, SEq' (Rep a)) => SEq (Default a) where-  Default l ==~ Default r = from l ==~~ from r-  {-# INLINE (==~) #-}---- | Symbolic logical operators for symbolic booleans.------ >>> let t = con True :: SymBool--- >>> let f = con False :: SymBool--- >>> let a = "a" :: SymBool--- >>> let b = "b" :: SymBool--- >>> t ||~ f--- true--- >>> a ||~ t--- true--- >>> a ||~ f--- a--- >>> a ||~ b--- (|| a b)--- >>> t &&~ f--- false--- >>> a &&~ t--- a--- >>> a &&~ f--- false--- >>> a &&~ b--- (&& a b)--- >>> nots t--- false--- >>> nots f--- true--- >>> nots a--- (! a)--- >>> t `xors` f--- true--- >>> t `xors` t--- false--- >>> a `xors` t--- (! a)--- >>> a `xors` f--- a--- >>> a `xors` b--- (|| (&& (! a) b) (&& a (! b)))-class LogicalOp b where-  -- | Symbolic disjunction-  (||~) :: b -> b -> b-  a ||~ b = nots $ nots a &&~ nots b-  {-# INLINE (||~) #-}--  infixr 2 ||~--  -- | Symbolic conjunction-  (&&~) :: b -> b -> b-  a &&~ b = nots $ nots a ||~ nots b-  {-# INLINE (&&~) #-}--  infixr 3 &&~--  -- | Symbolic negation-  nots :: b -> b--  -- | Symbolic exclusive disjunction-  xors :: b -> b -> b-  a `xors` b = (a &&~ nots b) ||~ (nots a &&~ b)-  {-# INLINE xors #-}--  -- | Symbolic implication-  implies :: b -> b -> b-  a `implies` b = nots a ||~ b-  {-# INLINE implies #-}--  {-# MINIMAL (||~), nots | (&&~), nots #-}--instance LogicalOp Bool where-  (||~) = (||)-  {-# INLINE (||~) #-}-  (&&~) = (&&)-  {-# INLINE (&&~) #-}-  nots = not-  {-# INLINE nots #-}---- | ITE operator for solvable (see "Grisette.Core#solvable")s, including symbolic boolean, integer, etc.------ >>> let a = "a" :: SymBool--- >>> let b = "b" :: SymBool--- >>> let c = "c" :: SymBool--- >>> ites a b c--- (ite a b c)-class ITEOp v where-  ites :: SymBool -> v -> v -> v---- | Aggregation for the operations on symbolic boolean types-class (SimpleMergeable b, SEq b, Eq b, LogicalOp b, Solvable Bool b, ITEOp b) => SymBoolOp b--#define CONCRETE_SEQ(type) \-instance SEq type where \-  l ==~ r = con $ l == r; \-  {-# INLINE (==~) #-}--#define CONCRETE_SEQ_BV(type) \-instance (KnownNat n, 1 <= n) => SEq (type n) where \-  l ==~ r = con $ l == r; \-  {-# INLINE (==~) #-}--#if 1-CONCRETE_SEQ(Bool)-CONCRETE_SEQ(Integer)-CONCRETE_SEQ(Char)-CONCRETE_SEQ(Int)-CONCRETE_SEQ(Int8)-CONCRETE_SEQ(Int16)-CONCRETE_SEQ(Int32)-CONCRETE_SEQ(Int64)-CONCRETE_SEQ(Word)-CONCRETE_SEQ(Word8)-CONCRETE_SEQ(Word16)-CONCRETE_SEQ(Word32)-CONCRETE_SEQ(Word64)-CONCRETE_SEQ(B.ByteString)-CONCRETE_SEQ(T.Text)-CONCRETE_SEQ_BV(WordN)-CONCRETE_SEQ_BV(IntN)-CONCRETE_SEQ(SomeWordN)-CONCRETE_SEQ(SomeIntN)-#endif---- List-deriving via (Default [a]) instance (SEq a) => SEq [a]---- Maybe-deriving via (Default (Maybe a)) instance (SEq a) => SEq (Maybe a)---- Either-deriving via (Default (Either e a)) instance (SEq e, SEq a) => SEq (Either e a)---- ExceptT-instance (SEq (m (Either e a))) => SEq (ExceptT e m a) where-  (ExceptT a) ==~ (ExceptT b) = a ==~ b-  {-# INLINE (==~) #-}---- MaybeT-instance (SEq (m (Maybe a))) => SEq (MaybeT m a) where-  (MaybeT a) ==~ (MaybeT b) = a ==~ b-  {-# INLINE (==~) #-}---- ()-instance SEq () where-  _ ==~ _ = con True-  {-# INLINE (==~) #-}---- (,)-deriving via (Default (a, b)) instance (SEq a, SEq b) => SEq (a, b)---- (,,)-deriving via (Default (a, b, c)) instance (SEq a, SEq b, SEq c) => SEq (a, b, c)---- (,,,)-deriving via-  (Default (a, b, c, d))-  instance-    (SEq a, SEq b, SEq c, SEq d) =>-    SEq (a, b, c, d)---- (,,,,)-deriving via-  (Default (a, b, c, d, e))-  instance-    (SEq a, SEq b, SEq c, SEq d, SEq e) =>-    SEq (a, b, c, d, e)---- (,,,,,)-deriving via-  (Default (a, b, c, d, e, f))-  instance-    (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) =>-    SEq (a, b, c, d, e, f)---- (,,,,,,)-deriving via-  (Default (a, b, c, d, e, f, g))-  instance-    (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) =>-    SEq (a, b, c, d, e, f, g)---- (,,,,,,,)-deriving via-  (Default (a, b, c, d, e, f, g, h))-  instance-    (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g, SEq h) =>-    SEq (a, b, c, d, e, f, g, h)---- Sum-deriving via-  (Default (Sum f g a))-  instance-    (SEq (f a), SEq (g a)) => SEq (Sum f g a)---- Writer-instance (SEq (m (a, s))) => SEq (WriterLazy.WriterT s m a) where-  (WriterLazy.WriterT l) ==~ (WriterLazy.WriterT r) = l ==~ r-  {-# INLINE (==~) #-}--instance (SEq (m (a, s))) => SEq (WriterStrict.WriterT s m a) where-  (WriterStrict.WriterT l) ==~ (WriterStrict.WriterT r) = l ==~ r-  {-# INLINE (==~) #-}---- Identity-instance (SEq a) => SEq (Identity a) where-  (Identity l) ==~ (Identity r) = l ==~ r-  {-# INLINE (==~) #-}---- IdentityT-instance (SEq (m a)) => SEq (IdentityT m a) where-  (IdentityT l) ==~ (IdentityT r) = l ==~ r-  {-# INLINE (==~) #-}--#define ITEOP_SIMPLE(type) \-instance ITEOp type where \-  ites (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \-  {-# INLINE ites #-}--#define ITEOP_BV(type) \-instance (KnownNat n, 1 <= n) => ITEOp (type n) where \-  ites (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \-  {-# INLINE ites #-}--#define ITEOP_BV_SOME(symtype, bf) \-instance ITEOp symtype where \-  ites c = bf (ites c) "ites"; \-  {-# INLINE ites #-}--#define ITEOP_FUN(op, cons) \-instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa op sb) where \-  ites (SymBool c) (cons t) (cons f) = cons $ pevalITETerm c t f; \-  {-# INLINE ites #-}--#if 1-ITEOP_SIMPLE(SymBool)-ITEOP_SIMPLE(SymInteger)-ITEOP_BV(SymIntN)-ITEOP_BV(SymWordN)-ITEOP_BV_SOME(SomeSymIntN, binSomeSymIntNR1)-ITEOP_BV_SOME(SomeSymWordN, binSomeSymWordNR1)-ITEOP_FUN(=~>, SymTabularFun)-ITEOP_FUN(-~>, SymGeneralFun)-#endif--instance LogicalOp SymBool where-  (SymBool l) ||~ (SymBool r) = SymBool $ pevalOrTerm l r-  (SymBool l) &&~ (SymBool r) = SymBool $ pevalAndTerm l r-  nots (SymBool v) = SymBool $ pevalNotTerm v-  (SymBool l) `xors` (SymBool r) = SymBool $ pevalXorTerm l r-  (SymBool l) `implies` (SymBool r) = SymBool $ pevalImplyTerm l r

@@ -1,36 +0,0 @@-module Grisette.Core.Data.Class.Bool (LogicalOp (..), ITEOp (..)) where--import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)--class LogicalOp b where-  -- | Symbolic disjunction-  (||~) :: b -> b -> b-  a ||~ b = nots $ nots a &&~ nots b-  {-# INLINE (||~) #-}--  infixr 2 ||~--  -- | Symbolic conjunction-  (&&~) :: b -> b -> b-  a &&~ b = nots $ nots a ||~ nots b-  {-# INLINE (&&~) #-}--  infixr 3 &&~--  -- | Symbolic negation-  nots :: b -> b--  -- | Symbolic exclusive disjunction-  xors :: b -> b -> b-  a `xors` b = (a &&~ nots b) ||~ (nots a &&~ b)-  {-# INLINE xors #-}--  -- | Symbolic implication-  implies :: b -> b -> b-  a `implies` b = nots a ||~ b-  {-# INLINE implies #-}--  {-# MINIMAL (||~), nots | (&&~), nots #-}--class ITEOp v where-  ites :: SymBool -> v -> v -> v

@@ -2,7 +2,6 @@ {-# LANGUAGE DerivingVia #-} {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}@@ -22,11 +21,19 @@      -- -    -- | The examples assumes a [z3](https://github.com/Z3Prover/z3) solver available in @PATH@.+    -- | The examples assumes that the [z3](https://github.com/Z3Prover/z3)+    -- solver is available in @PATH@. -    -- * CEGIS solver interfaces-    CEGISSolver (..),+    -- * Generic CEGIS interface+    SynthesisConstraintFun,+    VerifierResult (..),+    StatefulVerifierFun,+    CEGISResult (..),+    genericCEGIS,++    -- * CEGIS interfaces with pre/post conditions     CEGISCondition (..),+    cegisMultiInputs,     cegisPostCond,     cegisPrePost,     cegis,@@ -39,23 +46,39 @@   ) where +import Control.Monad (foldM, unless)+import Data.List (partition) import GHC.Generics (Generic) import Generics.Deriving (Default (Default)) import Grisette.Core.Control.Exception   ( VerificationConditions (AssertionViolation, AssumptionViolation),   )-import Grisette.Core.Data.Class.Evaluate (EvaluateSym)+import Grisette.Core.Data.Class.EvaluateSym (EvaluateSym, evaluateSym) import Grisette.Core.Data.Class.ExtractSymbolics   ( ExtractSymbolics,+    extractSymbolics,   )+import Grisette.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&))) import Grisette.Core.Data.Class.Mergeable (Mergeable)+import Grisette.Core.Data.Class.ModelOps+  ( ModelOps (exact, exceptFor),+    SymbolSetOps (isEmptySet),+  )+import Grisette.Core.Data.Class.SEq (SEq) import Grisette.Core.Data.Class.SimpleMergeable   ( SimpleMergeable,     UnionPrjOp,     simpleMerge,   ) import Grisette.Core.Data.Class.Solvable (Solvable (con))-import Grisette.Core.Data.Class.Solver (UnionWithExcept (extractUnionExcept))+import Grisette.Core.Data.Class.Solver+  ( ConfigurableSolver,+    Solver (solverSolve),+    SolvingFailure (Unsat),+    UnionWithExcept (extractUnionExcept),+    solve,+    withSolver,+  ) import Grisette.IR.SymPrim.Data.Prim.Model (Model) import Grisette.IR.SymPrim.Data.SymPrim (SymBool) @@ -65,6 +88,83 @@ -- >>> import Grisette.IR.SymPrim -- >>> import Grisette.Backend.SBV +-- | Synthesis constraint function.+--+-- The first argument is the iteration number, for angelic programs, you can use+-- it to instantiate the angelic variables in the program.+--+-- The second argument is the counter-example generated by the verifier.+--+-- The synthesizer will try to find a program that is true for all the synthesis+-- constraints.+type SynthesisConstraintFun input = Int -> input -> IO SymBool++-- | The result of the verifier.+data VerifierResult input exception+  = CEGISVerifierFoundCex input+  | CEGISVerifierNoCex+  | CEGISVerifierException exception++-- | The verifier function.+--+-- The first argument is the state of the verifier.+--+-- The second argument is the candidate model proposed by the synthesizer.+type StatefulVerifierFun state input exception =+  state -> Model -> IO (state, VerifierResult input exception)++-- | The result of the CEGIS procedure.+data CEGISResult exception+  = CEGISSuccess Model+  | CEGISVerifierFailure exception+  | CEGISSolverFailure SolvingFailure+  deriving (Show)++-- | Generic CEGIS procedure.+--+-- The CEGIS procedure will try to find a model that satisfies the initial+-- synthesis constraint, and satisfies all the inputs generated by the verifier.+genericCEGIS ::+  (ConfigurableSolver config handle) =>+  -- | Configuration of the solver.+  config ->+  -- | The initial synthesis constraint.+  SymBool ->+  -- | The synthesis constraint function.+  SynthesisConstraintFun input ->+  -- | The initial state of the verifier.+  verifierState ->+  -- | The verifier function.+  StatefulVerifierFun verifierState input exception ->+  IO ([input], CEGISResult exception)+genericCEGIS config initConstr synthConstr initVerifierState verifier =+  withSolver config $ \solver -> do+    firstResult <- solverSolve solver initConstr+    case firstResult of+      Left err -> return ([], CEGISSolverFailure err)+      Right model -> go solver model 0 initVerifierState+  where+    go solver prevModel iterNum verifierState = do+      (newVerifierState, verifierResult) <-+        verifier verifierState prevModel+      case verifierResult of+        CEGISVerifierFoundCex cex -> do+          newResult <- solverSolve solver =<< synthConstr iterNum cex+          case newResult of+            Left err -> return ([], CEGISSolverFailure err)+            Right model -> do+              (cexes, result) <- go solver model (iterNum + 1) newVerifierState+              return (cex : cexes, result)+        CEGISVerifierNoCex -> return ([], CEGISSuccess prevModel)+        CEGISVerifierException exception ->+          return ([], CEGISVerifierFailure exception)++data CEGISMultiInputsState input = CEGISMultiInputsState+  { _cegisMultiInputsRemainingSymInputs :: [input],+    _cegisMultiInputsPre :: SymBool,+    _cegisMultiInputsPost :: SymBool+  }+ -- | The condition for CEGIS to solve. -- -- The first argument is the pre-condition, and the second argument is the@@ -82,7 +182,9 @@ -- meets the pre-conditions on every possible inputs, and there are at least -- one possible input. The post-condition is used to specify the desired program -- behaviors.-data CEGISCondition = CEGISCondition SymBool SymBool deriving (Generic)+data CEGISCondition = CEGISCondition SymBool SymBool+  deriving (Generic)+  deriving (EvaluateSym) via (Default CEGISCondition)  -- | Construct a CEGIS condition with only a post-condition. The pre-condition -- would be set to true, meaning that all programs in the program space are@@ -98,56 +200,87 @@  deriving via (Default CEGISCondition) instance SimpleMergeable CEGISCondition --- | Counter-example guided inductive synthesis (CEGIS) solver interface.-class-  CEGISSolver config failure-    | config -> failure+-- |+-- CEGIS with multiple (possibly symbolic) inputs. Solves the following formula+-- (see 'CEGISCondition' for details).+--+-- \[+--   \forall P. (\exists I\in\mathrm{inputs}. \mathrm{pre}(P, I)) \wedge (\forall I\in\mathrm{inputs}. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I))+-- \]+--+-- For simpler queries, where the inputs are representable by a single+-- symbolic value, you may want to use 'cegis' or 'cegisExcept' instead.+-- We have an example for the 'cegis' call.+cegisMultiInputs ::+  ( EvaluateSym input,+    ExtractSymbolics input,+    ConfigurableSolver config handle+  ) =>+  config ->+  [input] ->+  (input -> CEGISCondition) ->+  IO ([input], CEGISResult SolvingFailure)+cegisMultiInputs config inputs toCEGISCondition = do+  initConstr <- cexesAssertFun conInputs+  genericCEGIS+    config+    initConstr+    synthConstr+    (CEGISMultiInputsState symInputs (con True) (con True))+    verifier   where-  -- |-  -- CEGIS with multiple (possibly symbolic) inputs. Solves the following formula (see-  -- 'CEGISCondition' for details).-  ---  -- \[-  --   \forall P. (\exists I\in\mathrm{inputs}. \mathrm{pre}(P, I)) \wedge (\forall I\in\mathrm{inputs}. \mathrm{pre}(P, I)\implies \mathrm{post}(P, I))-  -- \]-  ---  -- For simpler queries, where the inputs are representable by a single-  -- symbolic value, you may want to use 'cegis' or 'cegisExcept' instead.-  -- We have an example for the 'cegis' call.-  cegisMultiInputs ::-    (EvaluateSym inputs, ExtractSymbolics inputs) =>-    -- | The configuration of the solver-    config ->-    -- | Some initial counter-examples. Providing some concrete-    -- inputs may help the solver to find a model faster. Providing-    -- symbolic inputs would cause the solver to find the program-    -- that works on all the inputs representable by it (see-    -- 'CEGISCondition').-    [inputs] ->-    -- | The function mapping the inputs to-    -- the conditions for the solver to-    -- solve.-    (inputs -> CEGISCondition) ->-    -- | The counter-examples generated-    -- during the CEGIS loop, and the-    -- model found by the solver.-    IO ([inputs], Either failure Model)+    (conInputs, symInputs) = partition (isEmptySet . extractSymbolics) inputs+    forallSymbols = extractSymbolics symInputs+    cexAssertFun input = do+      unless (isEmptySet (extractSymbolics input)) $ error "BUG"+      CEGISCondition pre post <- return $ toCEGISCondition input+      return $ pre .&& post+    cexesAssertFun = foldM (\acc x -> (acc .&&) <$> cexAssertFun x) (con True)+    synthConstr _ = cexAssertFun+    verifier state@(CEGISMultiInputsState [] _ _) _ =+      return (state, CEGISVerifierNoCex)+    verifier+      (CEGISMultiInputsState (nextSymInput : symInputs) pre post)+      candidate = do+        CEGISCondition nextPre nextPost <-+          return $ toCEGISCondition nextSymInput+        let newPre = pre .&& nextPre+        let newPost = post .&& nextPost+        let evaluated =+              evaluateSym False (exceptFor forallSymbols candidate) $+                newPre .&& symNot newPost+        r <- solve config evaluated+        case r of+          Left Unsat ->+            verifier (CEGISMultiInputsState symInputs newPre newPost) candidate+          Left err ->+            return+              ( CEGISMultiInputsState [] newPre newPost,+                CEGISVerifierException err+              )+          Right model ->+            return+              ( CEGISMultiInputsState (nextSymInput : symInputs) newPre newPost,+                CEGISVerifierFoundCex $+                  evaluateSym False (exact forallSymbols model) nextSymInput+              )  -- | -- CEGIS with a single symbolic input to represent a set of inputs. -- -- The following example tries to find the value of @c@ such that for all--- positive @x@, @x * c < 0 && c > -2@. The @c >~ -2@ clause is used to make+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ clause is used to make -- the solution unique. -- -- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger]--- >>> cegis (precise z3) x (cegisPrePost (x >~ 0) (x * c <~ 0 &&~ c >~ -2))--- ([],Right (Model {c -> -1 :: Integer}))+-- >>> cegis (precise z3) x (\x -> cegisPrePost (x .> 0) (x * c .< 0 .&& c .> -2))+-- ([...],CEGISSuccess (Model {c -> -1 :: Integer})) cegis ::-  ( CEGISSolver config failure,+  ( ConfigurableSolver config handle,     EvaluateSym inputs,-    ExtractSymbolics inputs+    ExtractSymbolics inputs,+    SEq inputs   ) =>   -- | The configuration of the solver   config ->@@ -158,18 +291,18 @@   -- | The condition for the solver to solve. All the   -- symbolic constants that are not in the inputs will   -- be considered as part of the symbolic program.-  CEGISCondition ->+  (inputs -> CEGISCondition) ->   -- | The counter-examples generated   -- during the CEGIS loop, and the   -- model found by the solver.-  IO ([inputs], Either failure Model)-cegis config inputs cond = cegisMultiInputs config [inputs] (const cond)+  IO ([inputs], CEGISResult SolvingFailure)+cegis config inputs = cegisMultiInputs config [inputs]  -- | -- CEGIS for symbolic programs with error handling, using multiple (possibly -- symbolic) inputs to represent a set of inputs. cegisExceptMultiInputs ::-  ( CEGISSolver config failure,+  ( ConfigurableSolver config handle,     EvaluateSym inputs,     ExtractSymbolics inputs,     UnionWithExcept t u e v,@@ -180,9 +313,12 @@   [inputs] ->   (Either e v -> CEGISCondition) ->   (inputs -> t) ->-  IO ([inputs], Either failure Model)+  IO ([inputs], CEGISResult SolvingFailure) cegisExceptMultiInputs config cexes interpretFun f =-  cegisMultiInputs config cexes (simpleMerge . (interpretFun <$>) . extractUnionExcept . f)+  cegisMultiInputs+    config+    cexes+    (simpleMerge . (interpretFun <$>) . extractUnionExcept . f)  -- | -- CEGIS for symbolic programs with error handling, using multiple (possibly@@ -190,7 +326,7 @@ -- -- The errors should be translated to assertion or assumption violations. cegisExceptVCMultiInputs ::-  ( CEGISSolver config failure,+  ( ConfigurableSolver config handle,     EvaluateSym inputs,     ExtractSymbolics inputs,     UnionWithExcept t u e v,@@ -201,7 +337,7 @@   [inputs] ->   (Either e v -> u (Either VerificationConditions ())) ->   (inputs -> t) ->-  IO ([inputs], Either failure Model)+  IO ([inputs], CEGISResult SolvingFailure) cegisExceptVCMultiInputs config cexes interpretFun f =   cegisMultiInputs     config@@ -227,7 +363,7 @@ -- and translates assertion violations to failed post-conditions. -- The '()' result will not fail any conditions. cegisExceptStdVCMultiInputs ::-  ( CEGISSolver config failure,+  ( ConfigurableSolver config handle,     EvaluateSym inputs,     ExtractSymbolics inputs,     UnionWithExcept t u VerificationConditions (),@@ -237,7 +373,7 @@   config ->   [inputs] ->   (inputs -> t) ->-  IO ([inputs], Either failure Model)+  IO ([inputs], CEGISResult SolvingFailure) cegisExceptStdVCMultiInputs config cexes =   cegisExceptVCMultiInputs config cexes return @@ -251,18 +387,18 @@ -- readability and modularity of the code. -- -- The following example tries to find the value of @c@ such that for all--- positive @x@, @x * c < 0 && c > -2@. The @c >~ -2@ assertion is used to make+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make -- the solution unique. -- -- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger] -- >>> import Control.Monad.Except -- >>> :{---   res :: ExceptT VerificationConditions UnionM ()---   res = do---     symAssume $ x >~ 0---     symAssert $ x * c <~ 0---     symAssert $ c >~ -2+--   res :: SymInteger -> ExceptT VerificationConditions UnionM ()+--   res x = do+--     symAssume $ x .> 0+--     symAssert $ x * c .< 0+--     symAssert $ c .> -2 -- :} -- -- >>> :{@@ -272,21 +408,23 @@ -- :} -- -- >>> cegisExcept (precise z3) x translation res--- ([],Right (Model {c -> -1 :: Integer}))+-- ([...],CEGISSuccess (Model {c -> -1 :: Integer})) cegisExcept ::   ( UnionWithExcept t u e v,     UnionPrjOp u,     Functor u,     EvaluateSym inputs,     ExtractSymbolics inputs,-    CEGISSolver config failure+    ConfigurableSolver config handle,+    SEq inputs   ) =>   config ->   inputs ->   (Either e v -> CEGISCondition) ->-  t ->-  IO ([inputs], Either failure Model)-cegisExcept config inputs f v = cegis config inputs $ simpleMerge $ f <$> extractUnionExcept v+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+cegisExcept config inputs f v =+  cegis config inputs $ \i -> simpleMerge $ f <$> extractUnionExcept (v i)  -- | -- CEGIS for symbolic programs with error handling, using a single symbolic@@ -299,22 +437,23 @@     Monad u,     EvaluateSym inputs,     ExtractSymbolics inputs,-    CEGISSolver config failure+    ConfigurableSolver config handle,+    SEq inputs   ) =>   config ->   inputs ->   (Either e v -> u (Either VerificationConditions ())) ->-  t ->-  IO ([inputs], Either failure Model)-cegisExceptVC config inputs f v =-  cegis config inputs $+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure)+cegisExceptVC config inputs f v = do+  cegis config inputs $ \i ->     simpleMerge $       ( \case           Left AssumptionViolation -> cegisPrePost (con False) (con True)           Left AssertionViolation -> cegisPostCond (con False)           _ -> cegisPostCond (con True)       )-        <$> (extractUnionExcept v >>= f)+        <$> (extractUnionExcept (v i) >>= f)  -- | -- CEGIS for symbolic programs with error handling, using a single symbolic@@ -327,32 +466,33 @@ -- The '()' result will not fail any conditions. -- -- The following example tries to find the value of @c@ such that for all--- positive @x@, @x * c < 0 && c > -2@. The @c >~ -2@ assertion is used to make+-- positive @x@, @x * c < 0 && c > -2@. The @c .> -2@ assertion is used to make -- the solution unique. -- -- >>> :set -XOverloadedStrings -- >>> let [x,c] = ["x","c"] :: [SymInteger] -- >>> import Control.Monad.Except -- >>> :{---   res :: ExceptT VerificationConditions UnionM ()---   res = do---     symAssume $ x >~ 0---     symAssert $ x * c <~ 0---     symAssert $ c >~ -2+--   res :: SymInteger -> ExceptT VerificationConditions UnionM ()+--   res x = do+--     symAssume $ x .> 0+--     symAssert $ x * c .< 0+--     symAssert $ c .> -2 -- :} -- -- >>> cegisExceptStdVC (precise z3) x res--- ([],Right (Model {c -> -1 :: Integer}))+-- ([...],CEGISSuccess (Model {c -> -1 :: Integer})) cegisExceptStdVC ::   ( UnionWithExcept t u VerificationConditions (),     UnionPrjOp u,     Monad u,     EvaluateSym inputs,     ExtractSymbolics inputs,-    CEGISSolver config failure+    ConfigurableSolver config handle,+    SEq inputs   ) =>   config ->   inputs ->-  t ->-  IO ([inputs], Either failure Model)+  (inputs -> t) ->+  IO ([inputs], CEGISResult SolvingFailure) cegisExceptStdVC config inputs = cegisExceptVC config inputs return

@@ -1,3 +1,4 @@+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE Trustworthy #-}@@ -18,19 +19,27 @@     symAssertWith,     symAssertTransformableError,     symThrowTransformableError,+    symAssert,+    symAssume,   ) where +import Control.Exception (ArithException, ArrayException) import Control.Monad.Except (MonadError (throwError))+import Grisette.Core.Control.Exception+  ( AssertionError (AssertionError),+    VerificationConditions (AssertionViolation, AssumptionViolation),+  ) import Grisette.Core.Control.Monad.Union (MonadUnion) import Grisette.Core.Data.Class.Mergeable (Mergeable) import Grisette.Core.Data.Class.SimpleMergeable (merge, mrgIf)-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)+import Grisette.IR.SymPrim.Data.SymPrim (SymBool)  -- $setup -- >>> import Control.Exception -- >>> import Grisette.Core -- >>> import Grisette.IR.SymPrim+-- >>> import Grisette.Lib.Control.Monad -- >>> import Control.Monad.Except -- >>> :set -XOverloadedStrings -- >>> :set -XFlexibleContexts@@ -116,3 +125,81 @@   erm () symAssertWith err cond = mrgIf cond (return ()) (throwError err) {-# INLINE symAssertWith #-}++instance TransformError VerificationConditions VerificationConditions where+  transformError = id++instance TransformError AssertionError VerificationConditions where+  transformError _ = AssertionViolation++instance TransformError ArithException AssertionError where+  transformError _ = AssertionError++instance TransformError ArrayException AssertionError where+  transformError _ = AssertionError++instance TransformError AssertionError AssertionError where+  transformError = id++-- | Used within a monadic multi path computation to begin exception processing.+--+-- Checks the condition passed to the function.+-- The current execution path will be terminated with assertion error if the condition is false.+--+-- If the condition is symbolic, Grisette will split the execution into two paths based on the condition.+-- The symbolic execution will continue on the then-branch, where the condition is true.+-- For the else branch, where the condition is false, the execution will be terminated.+--+-- The resulting monadic environment should be compatible with the 'AssertionError'+-- error type. See 'TransformError' type class for details.+--+-- __/Examples/__:+--+-- Terminates the execution if the condition is false.+-- Note that we may lose the 'Mergeable' knowledge here if no possible execution+-- path is viable. This may affect the efficiency in theory, but in practice this+-- should not be a problem as all paths are terminated and no further evaluation+-- would be performed.+--+-- >>> symAssert (con False) :: ExceptT AssertionError UnionM ()+-- ExceptT {Left AssertionError}+-- >>> do; symAssert (con False); mrgReturn 1 :: ExceptT AssertionError UnionM Integer+-- ExceptT <Left AssertionError>+--+-- No effect if the condition is true:+--+-- >>> symAssert (con True) :: ExceptT AssertionError UnionM ()+-- ExceptT {Right ()}+-- >>> do; symAssert (con True); mrgReturn 1 :: ExceptT AssertionError UnionM Integer+-- ExceptT {Right 1}+--+-- Splitting the path and terminate one of them when the condition is symbolic.+--+-- >>> symAssert (ssym "a") :: ExceptT AssertionError UnionM ()+-- ExceptT {If (! a) (Left AssertionError) (Right ())}+-- >>> do; symAssert (ssym "a"); mrgReturn 1 :: ExceptT AssertionError UnionM Integer+-- ExceptT {If (! a) (Left AssertionError) (Right 1)}+--+-- 'AssertionError' is compatible with 'VerificationConditions':+--+-- >>> symAssert (ssym "a") :: ExceptT VerificationConditions UnionM ()+-- ExceptT {If (! a) (Left AssertionViolation) (Right ())}+symAssert ::+  (TransformError AssertionError to, Mergeable to, MonadError to erm, MonadUnion erm) =>+  SymBool ->+  erm ()+symAssert = symAssertTransformableError AssertionError++-- | Used within a monadic multi path computation to begin exception processing.+--+-- Similar to 'symAssert', but terminates the execution path with 'AssumptionViolation' error.+--+-- /Examples/:+--+-- >>> symAssume (ssym "a") :: ExceptT VerificationConditions UnionM ()+-- ExceptT {If (! a) (Left AssumptionViolation) (Right ())}+symAssume ::+  (TransformError VerificationConditions to, Mergeable to, MonadError to erm, MonadUnion erm) =>+  SymBool ->+  erm ()+symAssume = symAssertTransformableError AssumptionViolation

@@ -1,241 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE DerivingVia #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}---- |--- Module      :   Grisette.Core.Data.Class.Evaluate--- Copyright   :   (c) Sirui Lu 2021-2023--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Core.Data.Class.Evaluate-  ( -- * Evaluating symbolic values with model-    EvaluateSym (..),-    evaluateSymToCon,-  )-where--import Control.Monad.Except (ExceptT (ExceptT))-import Control.Monad.Identity-  ( Identity (Identity),-    IdentityT (IdentityT),-  )-import Control.Monad.Trans.Maybe (MaybeT (MaybeT))-import qualified Control.Monad.Writer.Lazy as WriterLazy-import qualified Control.Monad.Writer.Strict as WriterStrict-import qualified Data.ByteString as B-import Data.Functor.Sum (Sum)-import Data.Int (Int16, Int32, Int64, Int8)-import Data.Maybe (fromJust)-import qualified Data.Text as T-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, type (<=))-import Generics.Deriving-  ( Default (Default, unDefault),-    Generic (Rep, from, to),-    K1 (K1),-    M1 (M1),-    U1,-    type (:*:) ((:*:)),-    type (:+:) (L1, R1),-  )-import Generics.Deriving.Instances ()-import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)-import Grisette.Core.Data.Class.ToCon (ToCon (toCon))-import Grisette.IR.SymPrim.Data.Prim.Model (Model)---- $setup--- >>> import Grisette.Core--- >>> import Grisette.IR.SymPrim--- >>> import Data.Proxy--- >>> :set -XTypeApplications---- | Evaluating symbolic values with some model.------ >>> let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model--- >>> evaluateSym False model ([ssym "a", ssym "b"] :: [SymInteger])--- [1,b]------ If we set the first argument true, the missing variables will be filled in with--- some default values:------ >>> evaluateSym True model ([ssym "a", ssym "b"] :: [SymInteger])--- [1,0]------ __Note 1:__ This type class can be derived for algebraic data types.--- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.------ > data X = ... deriving Generic deriving EvaluateSym via (Default X)-class EvaluateSym a where-  -- | Evaluate a symbolic variable with some model, possibly fill in values for the missing variables.-  evaluateSym :: Bool -> Model -> a -> a--instance (Generic a, EvaluateSym' (Rep a)) => EvaluateSym (Default a) where-  evaluateSym fillDefault model = Default . to . evaluateSym' fillDefault model . from . unDefault--class EvaluateSym' a where-  evaluateSym' :: Bool -> Model -> a c -> a c--instance EvaluateSym' U1 where-  evaluateSym' _ _ = id--instance (EvaluateSym c) => EvaluateSym' (K1 i c) where-  evaluateSym' fillDefault model (K1 v) = K1 $ evaluateSym fillDefault model v--instance (EvaluateSym' a) => EvaluateSym' (M1 i c a) where-  evaluateSym' fillDefault model (M1 v) = M1 $ evaluateSym' fillDefault model v--instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :+: b) where-  evaluateSym' fillDefault model (L1 l) = L1 $ evaluateSym' fillDefault model l-  evaluateSym' fillDefault model (R1 r) = R1 $ evaluateSym' fillDefault model r--instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :*: b) where-  evaluateSym' fillDefault model (a :*: b) = evaluateSym' fillDefault model a :*: evaluateSym' fillDefault model b---- | Evaluate a symbolic variable with some model, fill in values for the missing variables,--- and transform to concrete ones------ >>> let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model--- >>> evaluateSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer]--- [1,0]-evaluateSymToCon :: (ToCon a b, EvaluateSym a) => Model -> a -> b-evaluateSymToCon model a = fromJust $ toCon $ evaluateSym True model a---- instances--#define CONCRETE_EVALUATESYM(type) \-instance EvaluateSym type where \-  evaluateSym _ _ = id--#define CONCRETE_EVALUATESYM_BV(type) \-instance (KnownNat n, 1 <= n) => EvaluateSym (type n) where \-  evaluateSym _ _ = id--#if 1-CONCRETE_EVALUATESYM(Bool)-CONCRETE_EVALUATESYM(Integer)-CONCRETE_EVALUATESYM(Char)-CONCRETE_EVALUATESYM(Int)-CONCRETE_EVALUATESYM(Int8)-CONCRETE_EVALUATESYM(Int16)-CONCRETE_EVALUATESYM(Int32)-CONCRETE_EVALUATESYM(Int64)-CONCRETE_EVALUATESYM(Word)-CONCRETE_EVALUATESYM(Word8)-CONCRETE_EVALUATESYM(Word16)-CONCRETE_EVALUATESYM(Word32)-CONCRETE_EVALUATESYM(Word64)-CONCRETE_EVALUATESYM(SomeIntN)-CONCRETE_EVALUATESYM(SomeWordN)-CONCRETE_EVALUATESYM(B.ByteString)-CONCRETE_EVALUATESYM(T.Text)-CONCRETE_EVALUATESYM_BV(IntN)-CONCRETE_EVALUATESYM_BV(WordN)-#endif---- ()-instance EvaluateSym () where-  evaluateSym _ _ = id---- Either-deriving via (Default (Either a b)) instance (EvaluateSym a, EvaluateSym b) => EvaluateSym (Either a b)---- Maybe-deriving via (Default (Maybe a)) instance (EvaluateSym a) => EvaluateSym (Maybe a)---- List-deriving via (Default [a]) instance (EvaluateSym a) => EvaluateSym [a]---- (,)-deriving via (Default (a, b)) instance (EvaluateSym a, EvaluateSym b) => EvaluateSym (a, b)---- (,,)-deriving via (Default (a, b, c)) instance (EvaluateSym a, EvaluateSym b, EvaluateSym c) => EvaluateSym (a, b, c)---- (,,,)-deriving via-  (Default (a, b, c, d))-  instance-    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d) => EvaluateSym (a, b, c, d)---- (,,,,)-deriving via-  (Default (a, b, c, d, e))-  instance-    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e) =>-    EvaluateSym (a, b, c, d, e)---- (,,,,,)-deriving via-  (Default (a, b, c, d, e, f))-  instance-    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e, EvaluateSym f) =>-    EvaluateSym (a, b, c, d, e, f)---- (,,,,,,)-deriving via-  (Default (a, b, c, d, e, f, g))-  instance-    ( EvaluateSym a,-      EvaluateSym b,-      EvaluateSym c,-      EvaluateSym d,-      EvaluateSym e,-      EvaluateSym f,-      EvaluateSym g-    ) =>-    EvaluateSym (a, b, c, d, e, f, g)---- (,,,,,,,)-deriving via-  (Default (a, b, c, d, e, f, g, h))-  instance-    ( EvaluateSym a,-      EvaluateSym b,-      EvaluateSym c,-      EvaluateSym d,-      EvaluateSym e,-      EvaluateSym f,-      EvaluateSym g,-      EvaluateSym h-    ) =>-    EvaluateSym ((,,,,,,,) a b c d e f g h)---- MaybeT-instance (EvaluateSym (m (Maybe a))) => EvaluateSym (MaybeT m a) where-  evaluateSym fillDefault model (MaybeT v) = MaybeT $ evaluateSym fillDefault model v---- ExceptT-instance (EvaluateSym (m (Either e a))) => EvaluateSym (ExceptT e m a) where-  evaluateSym fillDefault model (ExceptT v) = ExceptT $ evaluateSym fillDefault model v---- Sum-deriving via-  (Default (Sum f g a))-  instance-    (EvaluateSym (f a), EvaluateSym (g a)) => EvaluateSym (Sum f g a)---- WriterT-instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterLazy.WriterT s m a) where-  evaluateSym fillDefault model (WriterLazy.WriterT v) = WriterLazy.WriterT $ evaluateSym fillDefault model v--instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterStrict.WriterT s m a) where-  evaluateSym fillDefault model (WriterStrict.WriterT v) = WriterStrict.WriterT $ evaluateSym fillDefault model v---- Identity-instance (EvaluateSym a) => EvaluateSym (Identity a) where-  evaluateSym fillDefault model (Identity a) = Identity $ evaluateSym fillDefault model a---- IdentityT-instance (EvaluateSym (m a)) => EvaluateSym (IdentityT m a) where-  evaluateSym fillDefault model (IdentityT a) = IdentityT $ evaluateSym fillDefault model a

@@ -0,0 +1,286 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module      :   Grisette.Core.Data.Class.EvaluateSym+-- Copyright   :   (c) Sirui Lu 2021-2023+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Core.Data.Class.EvaluateSym+  ( -- * Evaluating symbolic values with model+    EvaluateSym (..),+    evaluateSymToCon,+  )+where++import Control.Monad.Except (ExceptT (ExceptT))+import Control.Monad.Identity+  ( Identity (Identity),+    IdentityT (IdentityT),+  )+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))+import qualified Control.Monad.Writer.Lazy as WriterLazy+import qualified Control.Monad.Writer.Strict as WriterStrict+import qualified Data.ByteString as B+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8)+import Data.Maybe (fromJust)+import qualified Data.Text as T+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeNats (KnownNat, type (<=))+import Generics.Deriving+  ( Default (Default, unDefault),+    Generic (Rep, from, to),+    K1 (K1),+    M1 (M1),+    U1,+    type (:*:) ((:*:)),+    type (:+:) (L1, R1),+  )+import Generics.Deriving.Instances ()+import Grisette.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)+import Grisette.Core.Data.Class.ToCon (ToCon (toCon))+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term (LinkedRep, SupportedPrim)+import Grisette.IR.SymPrim.Data.Prim.Model (Model, evaluateTerm)+import Grisette.IR.SymPrim.Data.SymPrim+  ( SomeSymIntN (SomeSymIntN),+    SomeSymWordN (SomeSymWordN),+    SymBool (SymBool),+    SymIntN (SymIntN),+    SymInteger (SymInteger),+    SymWordN (SymWordN),+    type (-~>) (SymGeneralFun),+    type (=~>) (SymTabularFun),+  )++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.IR.SymPrim+-- >>> import Data.Proxy+-- >>> :set -XTypeApplications++-- | Evaluating symbolic values with some model.+--+-- >>> let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model+-- >>> evaluateSym False model ([ssym "a", ssym "b"] :: [SymInteger])+-- [1,b]+--+-- If we set the first argument true, the missing variables will be filled in with+-- some default values:+--+-- >>> evaluateSym True model ([ssym "a", ssym "b"] :: [SymInteger])+-- [1,0]+--+-- __Note 1:__ This type class can be derived for algebraic data types.+-- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.+--+-- > data X = ... deriving Generic deriving EvaluateSym via (Default X)+class EvaluateSym a where+  -- | Evaluate a symbolic variable with some model, possibly fill in values for the missing variables.+  evaluateSym :: Bool -> Model -> a -> a++-- | Evaluate a symbolic variable with some model, fill in values for the missing variables,+-- and transform to concrete ones+--+-- >>> let model = insertValue (SimpleSymbol "a") (1 :: Integer) emptyModel :: Model+-- >>> evaluateSymToCon model ([ssym "a", ssym "b"] :: [SymInteger]) :: [Integer]+-- [1,0]+evaluateSymToCon :: (ToCon a b, EvaluateSym a) => Model -> a -> b+evaluateSymToCon model a = fromJust $ toCon $ evaluateSym True model a++-- instances++#define CONCRETE_EVALUATESYM(type) \+instance EvaluateSym type where \+  evaluateSym _ _ = id++#define CONCRETE_EVALUATESYM_BV(type) \+instance (KnownNat n, 1 <= n) => EvaluateSym (type n) where \+  evaluateSym _ _ = id++#if 1+CONCRETE_EVALUATESYM(Bool)+CONCRETE_EVALUATESYM(Integer)+CONCRETE_EVALUATESYM(Char)+CONCRETE_EVALUATESYM(Int)+CONCRETE_EVALUATESYM(Int8)+CONCRETE_EVALUATESYM(Int16)+CONCRETE_EVALUATESYM(Int32)+CONCRETE_EVALUATESYM(Int64)+CONCRETE_EVALUATESYM(Word)+CONCRETE_EVALUATESYM(Word8)+CONCRETE_EVALUATESYM(Word16)+CONCRETE_EVALUATESYM(Word32)+CONCRETE_EVALUATESYM(Word64)+CONCRETE_EVALUATESYM(SomeIntN)+CONCRETE_EVALUATESYM(SomeWordN)+CONCRETE_EVALUATESYM(B.ByteString)+CONCRETE_EVALUATESYM(T.Text)+CONCRETE_EVALUATESYM_BV(IntN)+CONCRETE_EVALUATESYM_BV(WordN)+#endif++-- ()+instance EvaluateSym () where+  evaluateSym _ _ = id++-- Either+deriving via (Default (Either a b)) instance (EvaluateSym a, EvaluateSym b) => EvaluateSym (Either a b)++-- Maybe+deriving via (Default (Maybe a)) instance (EvaluateSym a) => EvaluateSym (Maybe a)++-- List+deriving via (Default [a]) instance (EvaluateSym a) => EvaluateSym [a]++-- (,)+deriving via (Default (a, b)) instance (EvaluateSym a, EvaluateSym b) => EvaluateSym (a, b)++-- (,,)+deriving via (Default (a, b, c)) instance (EvaluateSym a, EvaluateSym b, EvaluateSym c) => EvaluateSym (a, b, c)++-- (,,,)+deriving via+  (Default (a, b, c, d))+  instance+    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d) => EvaluateSym (a, b, c, d)++-- (,,,,)+deriving via+  (Default (a, b, c, d, e))+  instance+    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e) =>+    EvaluateSym (a, b, c, d, e)++-- (,,,,,)+deriving via+  (Default (a, b, c, d, e, f))+  instance+    (EvaluateSym a, EvaluateSym b, EvaluateSym c, EvaluateSym d, EvaluateSym e, EvaluateSym f) =>+    EvaluateSym (a, b, c, d, e, f)++-- (,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g))+  instance+    ( EvaluateSym a,+      EvaluateSym b,+      EvaluateSym c,+      EvaluateSym d,+      EvaluateSym e,+      EvaluateSym f,+      EvaluateSym g+    ) =>+    EvaluateSym (a, b, c, d, e, f, g)++-- (,,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g, h))+  instance+    ( EvaluateSym a,+      EvaluateSym b,+      EvaluateSym c,+      EvaluateSym d,+      EvaluateSym e,+      EvaluateSym f,+      EvaluateSym g,+      EvaluateSym h+    ) =>+    EvaluateSym ((,,,,,,,) a b c d e f g h)++-- MaybeT+instance (EvaluateSym (m (Maybe a))) => EvaluateSym (MaybeT m a) where+  evaluateSym fillDefault model (MaybeT v) = MaybeT $ evaluateSym fillDefault model v++-- ExceptT+instance (EvaluateSym (m (Either e a))) => EvaluateSym (ExceptT e m a) where+  evaluateSym fillDefault model (ExceptT v) = ExceptT $ evaluateSym fillDefault model v++-- Sum+deriving via+  (Default (Sum f g a))+  instance+    (EvaluateSym (f a), EvaluateSym (g a)) => EvaluateSym (Sum f g a)++-- WriterT+instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterLazy.WriterT s m a) where+  evaluateSym fillDefault model (WriterLazy.WriterT v) = WriterLazy.WriterT $ evaluateSym fillDefault model v++instance (EvaluateSym (m (a, s))) => EvaluateSym (WriterStrict.WriterT s m a) where+  evaluateSym fillDefault model (WriterStrict.WriterT v) = WriterStrict.WriterT $ evaluateSym fillDefault model v++-- Identity+instance (EvaluateSym a) => EvaluateSym (Identity a) where+  evaluateSym fillDefault model (Identity a) = Identity $ evaluateSym fillDefault model a++-- IdentityT+instance (EvaluateSym (m a)) => EvaluateSym (IdentityT m a) where+  evaluateSym fillDefault model (IdentityT a) = IdentityT $ evaluateSym fillDefault model a++-- Symbolic primitives+#define EVALUATE_SYM_SIMPLE(symtype) \+instance EvaluateSym symtype where \+  evaluateSym fillDefault model (symtype t) = symtype $ evaluateTerm fillDefault model t++#define EVALUATE_SYM_BV(symtype) \+instance (KnownNat n, 1 <= n) => EvaluateSym (symtype n) where \+  evaluateSym fillDefault model (symtype t) = symtype $ evaluateTerm fillDefault model t++#define EVALUATE_SYM_FUN(op, cons) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => EvaluateSym (sa op sb) where \+  evaluateSym fillDefault model (cons t) = cons $ evaluateTerm fillDefault model t++#define EVALUATE_SYM_BV_SOME(somety, origty) \+instance EvaluateSym somety where \+  evaluateSym fillDefault model (somety (origty t)) = somety $ origty $ evaluateTerm fillDefault model t++#if 1+EVALUATE_SYM_SIMPLE(SymBool)+EVALUATE_SYM_SIMPLE(SymInteger)+EVALUATE_SYM_BV(SymIntN)+EVALUATE_SYM_BV(SymWordN)+EVALUATE_SYM_FUN(=~>, SymTabularFun)+EVALUATE_SYM_FUN(-~>, SymGeneralFun)+EVALUATE_SYM_BV_SOME(SomeSymIntN, SymIntN)+EVALUATE_SYM_BV_SOME(SomeSymWordN, SymWordN)+#endif++-- Exception+deriving via (Default AssertionError) instance EvaluateSym AssertionError++deriving via (Default VerificationConditions) instance EvaluateSym VerificationConditions++instance (Generic a, EvaluateSym' (Rep a)) => EvaluateSym (Default a) where+  evaluateSym fillDefault model = Default . to . evaluateSym' fillDefault model . from . unDefault++class EvaluateSym' a where+  evaluateSym' :: Bool -> Model -> a c -> a c++instance EvaluateSym' U1 where+  evaluateSym' _ _ = id++instance (EvaluateSym c) => EvaluateSym' (K1 i c) where+  evaluateSym' fillDefault model (K1 v) = K1 $ evaluateSym fillDefault model v++instance (EvaluateSym' a) => EvaluateSym' (M1 i c a) where+  evaluateSym' fillDefault model (M1 v) = M1 $ evaluateSym' fillDefault model v++instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :+: b) where+  evaluateSym' fillDefault model (L1 l) = L1 $ evaluateSym' fillDefault model l+  evaluateSym' fillDefault model (R1 r) = R1 $ evaluateSym' fillDefault model r++instance (EvaluateSym' a, EvaluateSym' b) => EvaluateSym' (a :*: b) where+  evaluateSym' fillDefault model (a :*: b) = evaluateSym' fillDefault model a :*: evaluateSym' fillDefault model b

@@ -47,10 +47,26 @@     type (:*:) ((:*:)),     type (:+:) (L1, R1),   )+import Grisette.Core.Control.Exception (AssertionError, VerificationConditions) import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.Prim.Model-  ( SymbolSet,+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+  ( LinkedRep,+    SupportedPrim,   )+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.TermUtils (extractSymbolicsTerm)+import Grisette.IR.SymPrim.Data.Prim.Model+  ( SymbolSet (SymbolSet),+  )+import Grisette.IR.SymPrim.Data.SymPrim+  ( SomeSymIntN (SomeSymIntN),+    SomeSymWordN (SomeSymWordN),+    SymBool (SymBool),+    SymIntN (SymIntN),+    SymInteger (SymInteger),+    SymWordN (SymWordN),+    type (-~>) (SymGeneralFun),+    type (=~>) (SymTabularFun),+  )  -- $setup -- >>> import Grisette.Core@@ -74,36 +90,7 @@ class ExtractSymbolics a where   extractSymbolics :: a -> SymbolSet -instance (Generic a, ExtractSymbolics' (Rep a)) => ExtractSymbolics (Default a) where-  extractSymbolics = extractSymbolics' . from . unDefault--class ExtractSymbolics' a where-  extractSymbolics' :: a c -> SymbolSet--instance ExtractSymbolics' U1 where-  extractSymbolics' _ = mempty--instance (ExtractSymbolics c) => ExtractSymbolics' (K1 i c) where-  extractSymbolics' = extractSymbolics . unK1--instance (ExtractSymbolics' a) => ExtractSymbolics' (M1 i c a) where-  extractSymbolics' = extractSymbolics' . unM1--instance-  (ExtractSymbolics' a, ExtractSymbolics' b) =>-  ExtractSymbolics' (a :+: b)-  where-  extractSymbolics' (L1 l) = extractSymbolics' l-  extractSymbolics' (R1 r) = extractSymbolics' r--instance-  (ExtractSymbolics' a, ExtractSymbolics' b) =>-  ExtractSymbolics' (a :*: b)-  where-  extractSymbolics' (l :*: r) = extractSymbolics' l <> extractSymbolics' r- -- instances- #define CONCRETE_EXTRACT_SYMBOLICS(type) \ instance ExtractSymbolics type where \   extractSymbolics _ = mempty@@ -274,3 +261,63 @@ -- IdentityT instance (ExtractSymbolics (m a)) => ExtractSymbolics (IdentityT m a) where   extractSymbolics (IdentityT a) = extractSymbolics a++#define EXTRACT_SYMBOLICS_SIMPLE(symtype) \+instance ExtractSymbolics symtype where \+  extractSymbolics (symtype t) = SymbolSet $ extractSymbolicsTerm t++#define EXTRACT_SYMBOLICS_BV(symtype) \+instance (KnownNat n, 1 <= n) => ExtractSymbolics (symtype n) where \+  extractSymbolics (symtype t) = SymbolSet $ extractSymbolicsTerm t++#define EXTRACT_SYMBOLICS_FUN(op, cons) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ExtractSymbolics (sa op sb) where \+  extractSymbolics (cons t) = SymbolSet $ extractSymbolicsTerm t++#define EXTRACT_SYMBOLICS_BV_SOME(somety, origty) \+instance ExtractSymbolics somety where \+  extractSymbolics (somety (origty t)) = SymbolSet $ extractSymbolicsTerm t++#if 1+EXTRACT_SYMBOLICS_SIMPLE(SymBool)+EXTRACT_SYMBOLICS_SIMPLE(SymInteger)+EXTRACT_SYMBOLICS_BV(SymIntN)+EXTRACT_SYMBOLICS_BV(SymWordN)+EXTRACT_SYMBOLICS_FUN(=~>, SymTabularFun)+EXTRACT_SYMBOLICS_FUN(-~>, SymGeneralFun)+EXTRACT_SYMBOLICS_BV_SOME(SomeSymIntN, SymIntN)+EXTRACT_SYMBOLICS_BV_SOME(SomeSymWordN, SymWordN)+#endif++-- Exception+deriving via (Default AssertionError) instance ExtractSymbolics AssertionError++deriving via (Default VerificationConditions) instance ExtractSymbolics VerificationConditions++instance (Generic a, ExtractSymbolics' (Rep a)) => ExtractSymbolics (Default a) where+  extractSymbolics = extractSymbolics' . from . unDefault++class ExtractSymbolics' a where+  extractSymbolics' :: a c -> SymbolSet++instance ExtractSymbolics' U1 where+  extractSymbolics' _ = mempty++instance (ExtractSymbolics c) => ExtractSymbolics' (K1 i c) where+  extractSymbolics' = extractSymbolics . unK1++instance (ExtractSymbolics' a) => ExtractSymbolics' (M1 i c a) where+  extractSymbolics' = extractSymbolics' . unM1++instance+  (ExtractSymbolics' a, ExtractSymbolics' b) =>+  ExtractSymbolics' (a :+: b)+  where+  extractSymbolics' (L1 l) = extractSymbolics' l+  extractSymbolics' (R1 r) = extractSymbolics' r++instance+  (ExtractSymbolics' a, ExtractSymbolics' b) =>+  ExtractSymbolics' (a :*: b)+  where+  extractSymbolics' (l :*: r) = extractSymbolics' l <> extractSymbolics' r

@@ -12,9 +12,21 @@ module Grisette.Core.Data.Class.Function   ( -- * Function operations     Function (..),+    Apply (..),   ) where +-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.IR.SymPrim+-- >>> :set -XDataKinds+-- >>> :set -XBinaryLiterals+-- >>> :set -XFlexibleContexts+-- >>> :set -XFlexibleInstances+-- >>> :set -XFunctionalDependencies+-- >>> :set -XOverloadedStrings+-- >>> :set -XTypeOperators+ -- | Abstraction for function-like types. class Function f where   -- | Argument type@@ -41,3 +53,20 @@   type Arg (a -> b) = a   type Ret (a -> b) = b   f # a = f a++-- | Applying an uninterpreted function.+--+-- >>> let f = "f" :: SymInteger =~> SymInteger =~> SymInteger+-- >>> apply f "a" "b"+-- (apply (apply f a) b)+--+-- Note that for implementation reasons, you can also use `apply` function on+-- a non-function symbolic value. In this case, the function is treated as an+-- `id` function.+class Apply uf where+  type FunType uf+  apply :: uf -> FunType uf++instance (Apply b) => Apply (a -> b) where+  type FunType (a -> b) = a -> FunType b+  apply f a = apply (f a)

@@ -27,6 +27,7 @@ import qualified Control.Monad.Writer.Lazy as WriterLazy import qualified Control.Monad.Writer.Strict as WriterStrict import qualified Data.ByteString as B+import qualified Data.ByteString.Char8 as C import Data.Functor.Sum (Sum) import Data.Int (Int16, Int32, Int64, Int8) import Data.String (IsString (fromString))@@ -51,6 +52,21 @@ import GHC.TypeLits (KnownNat, type (<=)) import Generics.Deriving (Default (Default, unDefault)) import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+  ( LinkedRep,+    SupportedPrim,+    prettyPrintTerm,+  )+import Grisette.IR.SymPrim.Data.SymPrim+  ( SomeSymIntN (SomeSymIntN),+    SomeSymWordN (SomeSymWordN),+    SymBool (SymBool),+    SymIntN (SymIntN),+    SymInteger (SymInteger),+    SymWordN (SymWordN),+    type (-~>) (SymGeneralFun),+    type (=~>) (SymTabularFun),+  )  #if MIN_VERSION_prettyprinter(1,7,0) import Prettyprinter@@ -99,116 +115,6 @@    {-# MINIMAL gpretty | gprettyPrec #-} -instance (Generic a, GPretty' (Rep a)) => GPretty (Default a) where-  gprettyPrec i v = gprettyPrec' Pref i $ from $ unDefault v--data Type = Rec | Tup | Pref | Inf String Int--class GPretty' a where-  gprettyPrec' :: Type -> Int -> a c -> Doc ann-  isNullary :: a c -> Bool-  isNullary = error "generic gpretty (isNullary): unnecessary case"--instance GPretty' V1 where-  gprettyPrec' _ _ x = case x of {}--instance GPretty' U1 where-  gprettyPrec' _ _ U1 = ""-  isNullary _ = True--instance (GPretty c) => GPretty' (K1 i c) where-  gprettyPrec' _ n (K1 a) = gprettyPrec n a-  isNullary _ = False--groupedEnclose :: Doc ann -> Doc ann -> Doc ann -> Doc ann-groupedEnclose l r d = group $ align $ vcat [l <> flatAlt " " "" <> d, r]--condEnclose :: Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann-condEnclose b = if b then groupedEnclose else const $ const id--instance (GPretty' a, Constructor c) => GPretty' (M1 C c a) where-  gprettyPrec' _ n c@(M1 x) =-    case t of-      Tup ->-        prettyBraces t (gprettyPrec' t 0 x)-      Inf _ m ->-        group $ condEnclose (n > m) "(" ")" $ gprettyPrec' t m x-      _ ->-        if isNullary x-          then pretty (conName c)-          else-            group $-              condEnclose (n > 10) "(" ")" $-                align $-                  nest 2 $-                    vsep-                      [ pretty (conName c),-                        prettyBraces t (gprettyPrec' t 11 x)-                      ]-    where-      prettyBraces :: Type -> Doc ann -> Doc ann-      prettyBraces Rec = groupedEnclose "{" "}"-      prettyBraces Tup = groupedEnclose "(" ")"-      prettyBraces Pref = id-      prettyBraces (Inf _ _) = id-      fixity = conFixity c-      t-        | conIsRecord c = Rec-        | conIsTuple c = Tup-        | otherwise = case fixity of-            Prefix -> Pref-            Infix _ i -> Inf (conName c) i-      conIsTuple :: C1 c f p -> Bool-      conIsTuple y = tupleName (conName y)-        where-          tupleName ('(' : ',' : _) = True-          tupleName _ = False--instance (Selector s, GPretty' a) => GPretty' (M1 S s a) where-  gprettyPrec' t n s@(M1 x)-    | selName s == "" =-        case t of-          Pref -> gprettyPrec' t (n + 1) x-          _ -> gprettyPrec' t (n + 1) x-    | otherwise =-        pretty (selName s) <+> "=" <+> gprettyPrec' t 0 x-  isNullary (M1 x) = isNullary x--instance (GPretty' a) => GPretty' (M1 D d a) where-  gprettyPrec' t n (M1 x) = gprettyPrec' t n x--instance (GPretty' a, GPretty' b) => GPretty' (a :+: b) where-  gprettyPrec' t n (L1 x) = gprettyPrec' t n x-  gprettyPrec' t n (R1 x) = gprettyPrec' t n x--instance (GPretty' a, GPretty' b) => GPretty' (a :*: b) where-  gprettyPrec' t@Rec n (a :*: b) =-    vcat-      [ gprettyPrec' t n a,-        "," <+> gprettyPrec' t n b-      ]-  gprettyPrec' t@(Inf s _) n (a :*: b) =-    align $-      nest 2 $-        vsep-          [ gprettyPrec' t n a,-            pretty s <+> gprettyPrec' t n b-          ]-  gprettyPrec' t@Tup _ (a :*: b) =-    vcat-      [ gprettyPrec' t 0 a,-        "," <> flatAlt " " "" <> gprettyPrec' t 0 b-      ]-  gprettyPrec' t@Pref n (a :*: b) =-    vsep-      [ gprettyPrec' t (n + 1) a,-        gprettyPrec' t (n + 1) b-      ]-  isNullary _ = False--viaShowsPrec :: (Int -> a -> ShowS) -> Int -> a -> Doc ann-viaShowsPrec f n a = pretty (f n a "")- #define GPRETTY_SIMPLE(type) \ instance GPretty type where gprettyPrec = viaShowsPrec showsPrec @@ -231,10 +137,14 @@ GPRETTY_SIMPLE(Word64) GPRETTY_SIMPLE(SomeIntN) GPRETTY_SIMPLE(SomeWordN)-GPRETTY_SIMPLE(B.ByteString)-GPRETTY_SIMPLE(T.Text) #endif +instance GPretty B.ByteString where+  gpretty = pretty . C.unpack++instance GPretty T.Text where+  gpretty = pretty+ instance (KnownNat n, 1 <= n) => GPretty (IntN n) where   gpretty = viaShow @@ -415,3 +325,142 @@           [ "IdentityT",             gprettyPrec 11 a           ]++-- Prettyprint+#define GPRETTY_SYM_SIMPLE(symtype) \+instance GPretty symtype where \+  gpretty (symtype t) = prettyPrintTerm t++#define GPRETTY_SYM_BV(symtype) \+instance (KnownNat n, 1 <= n) => GPretty (symtype n) where \+  gpretty (symtype t) = prettyPrintTerm t++#define GPRETTY_SYM_FUN(op, cons) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb)\+  => GPretty (sa op sb) where \+  gpretty (cons t) = prettyPrintTerm t++#define GPRETTY_SYM_SOME_BV(symtype) \+instance GPretty symtype where \+  gpretty (symtype t) = gpretty t++#if 1+GPRETTY_SYM_SIMPLE(SymBool)+GPRETTY_SYM_SIMPLE(SymInteger)+GPRETTY_SYM_BV(SymIntN)+GPRETTY_SYM_BV(SymWordN)+GPRETTY_SYM_FUN(=~>, SymTabularFun)+GPRETTY_SYM_FUN(-~>, SymGeneralFun)+GPRETTY_SYM_SOME_BV(SomeSymIntN)+GPRETTY_SYM_SOME_BV(SomeSymWordN)+#endif++instance (Generic a, GPretty' (Rep a)) => GPretty (Default a) where+  gprettyPrec i v = gprettyPrec' Pref i $ from $ unDefault v++data Type = Rec | Tup | Pref | Inf String Int++class GPretty' a where+  gprettyPrec' :: Type -> Int -> a c -> Doc ann+  isNullary :: a c -> Bool+  isNullary = error "generic gpretty (isNullary): unnecessary case"++instance GPretty' V1 where+  gprettyPrec' _ _ x = case x of {}++instance GPretty' U1 where+  gprettyPrec' _ _ U1 = ""+  isNullary _ = True++instance (GPretty c) => GPretty' (K1 i c) where+  gprettyPrec' _ n (K1 a) = gprettyPrec n a+  isNullary _ = False++groupedEnclose :: Doc ann -> Doc ann -> Doc ann -> Doc ann+groupedEnclose l r d = group $ align $ vcat [l <> flatAlt " " "" <> d, r]++condEnclose :: Bool -> Doc ann -> Doc ann -> Doc ann -> Doc ann+condEnclose b = if b then groupedEnclose else const $ const id++instance (GPretty' a, Constructor c) => GPretty' (M1 C c a) where+  gprettyPrec' _ n c@(M1 x) =+    case t of+      Tup ->+        prettyBraces t (gprettyPrec' t 0 x)+      Inf _ m ->+        group $ condEnclose (n > m) "(" ")" $ gprettyPrec' t m x+      _ ->+        if isNullary x+          then pretty (conName c)+          else+            group $+              condEnclose (n > 10) "(" ")" $+                align $+                  nest 2 $+                    vsep+                      [ pretty (conName c),+                        prettyBraces t (gprettyPrec' t 11 x)+                      ]+    where+      prettyBraces :: Type -> Doc ann -> Doc ann+      prettyBraces Rec = groupedEnclose "{" "}"+      prettyBraces Tup = groupedEnclose "(" ")"+      prettyBraces Pref = id+      prettyBraces (Inf _ _) = id+      fixity = conFixity c+      t+        | conIsRecord c = Rec+        | conIsTuple c = Tup+        | otherwise = case fixity of+            Prefix -> Pref+            Infix _ i -> Inf (conName c) i+      conIsTuple :: C1 c f p -> Bool+      conIsTuple y = tupleName (conName y)+        where+          tupleName ('(' : ',' : _) = True+          tupleName _ = False++instance (Selector s, GPretty' a) => GPretty' (M1 S s a) where+  gprettyPrec' t n s@(M1 x)+    | selName s == "" =+        case t of+          Pref -> gprettyPrec' t (n + 1) x+          _ -> gprettyPrec' t (n + 1) x+    | otherwise =+        pretty (selName s) <+> "=" <+> gprettyPrec' t 0 x+  isNullary (M1 x) = isNullary x++instance (GPretty' a) => GPretty' (M1 D d a) where+  gprettyPrec' t n (M1 x) = gprettyPrec' t n x++instance (GPretty' a, GPretty' b) => GPretty' (a :+: b) where+  gprettyPrec' t n (L1 x) = gprettyPrec' t n x+  gprettyPrec' t n (R1 x) = gprettyPrec' t n x++instance (GPretty' a, GPretty' b) => GPretty' (a :*: b) where+  gprettyPrec' t@Rec n (a :*: b) =+    vcat+      [ gprettyPrec' t n a,+        "," <+> gprettyPrec' t n b+      ]+  gprettyPrec' t@(Inf s _) n (a :*: b) =+    align $+      nest 2 $+        vsep+          [ gprettyPrec' t n a,+            pretty s <+> gprettyPrec' t n b+          ]+  gprettyPrec' t@Tup _ (a :*: b) =+    vcat+      [ gprettyPrec' t 0 a,+        "," <> flatAlt " " "" <> gprettyPrec' t 0 b+      ]+  gprettyPrec' t@Pref n (a :*: b) =+    vsep+      [ gprettyPrec' t (n + 1) a,+        gprettyPrec' t (n + 1) b+      ]+  isNullary _ = False++viaShowsPrec :: (Int -> a -> ShowS) -> Int -> a -> Doc ann+viaShowsPrec f n a = pretty (f n a "")

@@ -36,10 +36,13 @@      -- * Monad for fresh symbolic value generation     MonadFresh (..),-    FreshT,+    nextFreshIndex,+    liftFresh,+    FreshT (FreshT, runFreshTFromIndex),     Fresh,     runFreshT,     runFresh,+    mrgRunFreshT,      -- * Symbolic value generation     GenSym (..),@@ -82,7 +85,7 @@   ) import qualified Control.Monad.RWS.Lazy as RWSLazy import qualified Control.Monad.RWS.Strict as RWSStrict-import Control.Monad.Reader (ReaderT (ReaderT))+import Control.Monad.Reader (ReaderT) import Control.Monad.Signatures (Catch) import qualified Control.Monad.State.Lazy as StateLazy import qualified Control.Monad.State.Strict as StateStrict@@ -115,7 +118,7 @@     type (:*:) ((:*:)),     type (:+:) (L1, R1),   )-import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM (UnionM)+import Grisette.Core.Control.Monad.UnionM (UnionM, isMerged, underlyingUnion) import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN) import Grisette.Core.Data.Class.Mergeable   ( Mergeable (rootStrategy),@@ -136,11 +139,12 @@ import Grisette.Core.Data.Class.Solvable   ( Solvable (iinfosym, isym),   )+import Grisette.Core.Data.Union (Union (UnionIf, UnionSingle)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term   ( LinkedRep,     SupportedPrim,   )-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+import Grisette.IR.SymPrim.Data.SymPrim   ( SomeSymIntN (SomeSymIntN),     SomeSymWordN (SomeSymWordN),     SymBool,@@ -213,15 +217,15 @@ --     >>> nameWithInfo "a" (1 :: Int) --     a:1 data FreshIdent where-  FreshIdent :: String -> FreshIdent-  FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent+  FreshIdent :: T.Text -> FreshIdent+  FreshIdentWithInfo :: (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> a -> FreshIdent  instance Show FreshIdent where-  show (FreshIdent i) = i-  show (FreshIdentWithInfo s i) = s ++ ":" ++ show i+  show (FreshIdent i) = T.unpack i+  show (FreshIdentWithInfo s i) = T.unpack s ++ ":" ++ show i  instance IsString FreshIdent where-  fromString = name+  fromString = name . T.pack  instance Eq FreshIdent where   FreshIdent l == FreshIdent r = l == r@@ -260,7 +264,7 @@ -- -- The user may need to use unique names to avoid unintentional identifier -- collision.-name :: String -> FreshIdent+name :: T.Text -> FreshIdent name = FreshIdent  -- | Identifier with extra information.@@ -269,7 +273,7 @@ -- -- The user may need to use unique names or additional information to avoid -- unintentional identifier collision.-nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => String -> a -> FreshIdent+nameWithInfo :: forall a. (Typeable a, Ord a, Lift a, NFData a, Show a, Hashable a) => T.Text -> a -> FreshIdent nameWithInfo = FreshIdentWithInfo  -- | Monad class for fresh symbolic value generation.@@ -277,32 +281,54 @@ -- The monad should be a reader monad for the 'FreshIdent' and a state monad for -- the 'FreshIndex'. class (Monad m) => MonadFresh m where-  -- | Increase the index by one and return the new index.-  nextFreshIndex :: m FreshIndex+  -- | Get the current index for fresh variable generation.+  getFreshIndex :: m FreshIndex +  -- | Set the current index for fresh variable generation.+  setFreshIndex :: FreshIndex -> m ()+   -- | Get the identifier.   getFreshIdent :: m FreshIdent +-- | Get the next fresh index and increase the current index.+nextFreshIndex :: (MonadFresh m) => m FreshIndex+nextFreshIndex = do+  curr <- getFreshIndex+  let new = curr + 1+  setFreshIndex new+  return curr++-- | Lifts an @`Fresh` a@ into any `MonadFresh`.+liftFresh :: (MonadFresh m) => Fresh a -> m a+liftFresh (FreshT f) = do+  index <- nextFreshIndex+  ident <- getFreshIdent+  let (a, newIdx) = runIdentity $ f ident index+  setFreshIndex newIdx+  return a+ -- | A symbolic generation monad transformer. -- It is a reader monad transformer for identifiers and -- a state monad transformer for indices. -- -- Each time a fresh symbolic variable is generated, the index should be increased.-newtype FreshT m a = FreshT {runFreshT' :: FreshIdent -> FreshIndex -> m (a, FreshIndex)}+newtype FreshT m a = FreshT+  { runFreshTFromIndex :: FreshIdent -> FreshIndex -> m (a, FreshIndex)+  }  instance   (Mergeable a, Mergeable1 m) =>   Mergeable (FreshT m a)   where   rootStrategy =-    wrapStrategy (liftRootStrategy (liftRootStrategy rootStrategy1)) FreshT runFreshT'+    wrapStrategy (liftRootStrategy (liftRootStrategy rootStrategy1)) FreshT runFreshTFromIndex  instance (Mergeable1 m) => Mergeable1 (FreshT m) where   liftRootStrategy m =     wrapStrategy       (liftRootStrategy (liftRootStrategy (liftRootStrategy (liftRootStrategy2 m rootStrategy))))       FreshT-      runFreshT'+      runFreshTFromIndex  instance   (UnionLike m, Mergeable a) =>@@ -330,8 +356,15 @@  -- | Run the symbolic generation with the given identifier and 0 as the initial index. runFreshT :: (Monad m) => FreshT m a -> FreshIdent -> m a-runFreshT m ident = fst <$> runFreshT' m ident (FreshIndex 0)+runFreshT m ident = fst <$> runFreshTFromIndex m ident (FreshIndex 0) +mrgRunFreshT ::+  (Monad m, UnionLike m, Mergeable a) =>+  FreshT m a ->+  FreshIdent ->+  m a+mrgRunFreshT m ident = merge $ runFreshT m ident+ instance (Functor f) => Functor (FreshT f) where   fmap f (FreshT s) = FreshT $ \ident idx -> first f <$> s ident idx @@ -345,14 +378,14 @@ instance (Monad m) => Monad (FreshT m) where   (FreshT s) >>= f = FreshT $ \ident idx -> do     (a, idx') <- s ident idx-    runFreshT' (f a) ident idx'+    runFreshTFromIndex (f a) ident idx'  instance MonadTrans FreshT where   lift x = FreshT $ \_ index -> (,index) <$> x  liftFreshTCache :: (Functor m) => Catch e m (a, FreshIndex) -> Catch e (FreshT m) a liftFreshTCache catchE (FreshT m) h =-  FreshT $ \ident index -> m ident index `catchE` \e -> runFreshT' (h e) ident index+  FreshT $ \ident index -> m ident index `catchE` \e -> runFreshTFromIndex (h e) ident index  instance (MonadError e m) => MonadError e (FreshT m) where   throwError = lift . throwError@@ -374,36 +407,44 @@ instance (MonadRWS r w s m) => MonadRWS r w s (FreshT m)  instance (MonadFresh m) => MonadFresh (ExceptT e m) where-  nextFreshIndex = ExceptT $ Right <$> nextFreshIndex-  getFreshIdent = ExceptT $ Right <$> getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  instance (MonadFresh m, Monoid w) => MonadFresh (WriterLazy.WriterT w m) where-  nextFreshIndex = WriterLazy.WriterT $ (,mempty) <$> nextFreshIndex-  getFreshIdent = WriterLazy.WriterT $ (,mempty) <$> getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  instance (MonadFresh m, Monoid w) => MonadFresh (WriterStrict.WriterT w m) where-  nextFreshIndex = WriterStrict.WriterT $ (,mempty) <$> nextFreshIndex-  getFreshIdent = WriterStrict.WriterT $ (,mempty) <$> getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  instance (MonadFresh m) => MonadFresh (StateLazy.StateT s m) where-  nextFreshIndex = StateLazy.StateT $ \s -> (,s) <$> nextFreshIndex-  getFreshIdent = StateLazy.StateT $ \s -> (,s) <$> getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  instance (MonadFresh m) => MonadFresh (StateStrict.StateT s m) where-  nextFreshIndex = StateStrict.StateT $ \s -> (,s) <$> nextFreshIndex-  getFreshIdent = StateStrict.StateT $ \s -> (,s) <$> getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  instance (MonadFresh m) => MonadFresh (ReaderT r m) where-  nextFreshIndex = ReaderT $ const nextFreshIndex-  getFreshIdent = ReaderT $ const getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  instance (MonadFresh m, Monoid w) => MonadFresh (RWSLazy.RWST r w s m) where-  nextFreshIndex = RWSLazy.RWST $ \_ s -> (,s,mempty) <$> nextFreshIndex-  getFreshIdent = RWSLazy.RWST $ \_ s -> (,s,mempty) <$> getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  instance (MonadFresh m, Monoid w) => MonadFresh (RWSStrict.RWST r w s m) where-  nextFreshIndex = RWSStrict.RWST $ \_ s -> (,s,mempty) <$> nextFreshIndex-  getFreshIdent = RWSStrict.RWST $ \_ s -> (,s,mempty) <$> getFreshIdent+  getFreshIndex = lift getFreshIndex+  setFreshIndex newIdx = lift $ setFreshIndex newIdx+  getFreshIdent = lift getFreshIdent  -- | 'FreshT' specialized with Identity. type Fresh = FreshT Identity@@ -413,7 +454,8 @@ runFresh m ident = runIdentity $ runFreshT m ident  instance (Monad m) => MonadFresh (FreshT m) where-  nextFreshIndex = FreshT $ \_ idx -> return (idx, idx + 1)+  getFreshIndex = FreshT $ \_ idx -> return (idx, idx)+  setFreshIndex newIdx = FreshT $ \_ _ -> return ((), newIdx)   getFreshIdent = FreshT $ curry return  -- | Class of types in which symbolic values can be generated with respect to some specification.@@ -445,7 +487,7 @@   -- is ensured. No specification is needed.   --   -- >>> runFresh (fresh ()) "a" :: UnionM (Maybe Bool)-  -- {If a@1 Nothing (If a@0 (Just False) (Just True))}+  -- {If a@0 Nothing (If a@1 (Just False) (Just True))}   --   -- The following example generates lists of symbolic booleans with length 1 to 2.   --@@ -906,6 +948,7 @@  -- Maybe instance+  {-# OVERLAPPING #-}   (GenSym aspec a, Mergeable a) =>   GenSym (Maybe aspec) (Maybe a)   where@@ -919,10 +962,15 @@   simpleFresh Nothing = return Nothing   simpleFresh (Just aspec) = Just <$> simpleFresh aspec -instance (GenSym aspec a, Mergeable a) => GenSym aspec (Maybe a) where+instance+  {-# OVERLAPPABLE #-}+  (GenSym aspec a, Mergeable a) =>+  GenSym aspec (Maybe a)+  where   fresh aspec = do+    cond <- simpleFresh ()     a :: UnionM a <- fresh aspec-    chooseUnionFresh [return Nothing, Just <$> a]+    return $ mrgIf cond (mrgSingle Nothing) (Just <$> a)  -- List instance@@ -1749,3 +1797,19 @@ GENSYM_UNIT_FUN(-~>) GENSYM_UNIT_SIMPLE_FUN(-~>) #endif++instance (GenSym spec a, Mergeable a) => GenSym spec (UnionM a)++instance (GenSym spec a) => GenSymSimple spec (UnionM a) where+  simpleFresh spec = do+    res <- fresh spec+    if not (isMerged res) then error "Not merged" else return res++instance+  (GenSym a a, Mergeable a) =>+  GenSym (UnionM a) a+  where+  fresh spec = go (underlyingUnion $ merge spec)+    where+      go (UnionSingle x) = fresh x+      go (UnionIf _ _ _ t f) = mrgIf <$> simpleFresh () <*> go t <*> go f

@@ -0,0 +1,88 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module      :   Grisette.Core.Data.Class.ITEOp+-- Copyright   :   (c) Sirui Lu 2021-2023+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Core.Data.Class.ITEOp+  ( ITEOp (..),+  )+where++import GHC.TypeNats (KnownNat, type (<=))+import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term+  ( LinkedRep,+    SupportedPrim,+  )+import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool (pevalITETerm)+import Grisette.IR.SymPrim.Data.SymPrim+  ( SomeSymIntN,+    SomeSymWordN,+    SymBool (SymBool),+    SymIntN (SymIntN),+    SymInteger (SymInteger),+    SymWordN (SymWordN),+    binSomeSymIntNR1,+    binSomeSymWordNR1,+    type (-~>) (SymGeneralFun),+    type (=~>) (SymTabularFun),+  )++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.IR.SymPrim+-- >>> :set -XDataKinds+-- >>> :set -XBinaryLiterals+-- >>> :set -XFlexibleContexts+-- >>> :set -XFlexibleInstances+-- >>> :set -XFunctionalDependencies++-- | ITE operator for solvable (see "Grisette.Core#solvable")s, including symbolic boolean, integer, etc.+--+-- >>> let a = "a" :: SymBool+-- >>> let b = "b" :: SymBool+-- >>> let c = "c" :: SymBool+-- >>> symIte a b c+-- (ite a b c)+class ITEOp v where+  symIte :: SymBool -> v -> v -> v++-- ITEOp instances+#define ITEOP_SIMPLE(type) \+instance ITEOp type where \+  symIte (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \+  {-# INLINE symIte #-}++#define ITEOP_BV(type) \+instance (KnownNat n, 1 <= n) => ITEOp (type n) where \+  symIte (SymBool c) (type t) (type f) = type $ pevalITETerm c t f; \+  {-# INLINE symIte #-}++#define ITEOP_BV_SOME(symtype, bf) \+instance ITEOp symtype where \+  symIte c = bf (symIte c) "symIte"; \+  {-# INLINE symIte #-}++#define ITEOP_FUN(op, cons) \+instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => ITEOp (sa op sb) where \+  symIte (SymBool c) (cons t) (cons f) = cons $ pevalITETerm c t f; \+  {-# INLINE symIte #-}++#if 1+ITEOP_SIMPLE(SymBool)+ITEOP_SIMPLE(SymInteger)+ITEOP_BV(SymIntN)+ITEOP_BV(SymWordN)+ITEOP_BV_SOME(SomeSymIntN, binSomeSymIntNR1)+ITEOP_BV_SOME(SomeSymWordN, binSomeSymWordNR1)+ITEOP_FUN(=~>, SymTabularFun)+ITEOP_FUN(-~>, SymGeneralFun)+#endif

@@ -0,0 +1,106 @@+module Grisette.Core.Data.Class.LogicalOp+  ( LogicalOp (..),+  )+where++import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool+  ( pevalAndTerm,+    pevalImplyTerm,+    pevalNotTerm,+    pevalOrTerm,+    pevalXorTerm,+  )+import Grisette.IR.SymPrim.Data.SymPrim (SymBool (SymBool))++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.IR.SymPrim+-- >>> :set -XDataKinds+-- >>> :set -XBinaryLiterals+-- >>> :set -XFlexibleContexts+-- >>> :set -XFlexibleInstances+-- >>> :set -XFunctionalDependencies++-- | Symbolic logical operators for symbolic booleans.+--+-- >>> let t = con True :: SymBool+-- >>> let f = con False :: SymBool+-- >>> let a = "a" :: SymBool+-- >>> let b = "b" :: SymBool+-- >>> t .|| f+-- true+-- >>> a .|| t+-- true+-- >>> a .|| f+-- a+-- >>> a .|| b+-- (|| a b)+-- >>> t .&& f+-- false+-- >>> a .&& t+-- a+-- >>> a .&& f+-- false+-- >>> a .&& b+-- (&& a b)+-- >>> symNot t+-- false+-- >>> symNot f+-- true+-- >>> symNot a+-- (! a)+-- >>> t `symXor` f+-- true+-- >>> t `symXor` t+-- false+-- >>> a `symXor` t+-- (! a)+-- >>> a `symXor` f+-- a+-- >>> a `symXor` b+-- (|| (&& (! a) b) (&& a (! b)))+class LogicalOp b where+  -- | Symbolic disjunction+  (.||) :: b -> b -> b+  a .|| b = symNot $ symNot a .&& symNot b+  {-# INLINE (.||) #-}++  infixr 2 .||++  -- | Symbolic conjunction+  (.&&) :: b -> b -> b+  a .&& b = symNot $ symNot a .|| symNot b+  {-# INLINE (.&&) #-}++  infixr 3 .&&++  -- | Symbolic negation+  symNot :: b -> b++  -- | Symbolic exclusive disjunction+  symXor :: b -> b -> b+  a `symXor` b = (a .&& symNot b) .|| (symNot a .&& b)+  {-# INLINE symXor #-}++  -- | Symbolic implication+  symImplies :: b -> b -> b+  a `symImplies` b = symNot a .|| b+  {-# INLINE symImplies #-}++  {-# MINIMAL (.||), symNot | (.&&), symNot #-}++-- LogicalOp instances+instance LogicalOp Bool where+  (.||) = (||)+  {-# INLINE (.||) #-}+  (.&&) = (&&)+  {-# INLINE (.&&) #-}+  symNot = not+  {-# INLINE symNot #-}++instance LogicalOp SymBool where+  (SymBool l) .|| (SymBool r) = SymBool $ pevalOrTerm l r+  (SymBool l) .&& (SymBool r) = SymBool $ pevalAndTerm l r+  symNot (SymBool v) = SymBool $ pevalNotTerm v+  (SymBool l) `symXor` (SymBool r) = SymBool $ pevalXorTerm l r+  (SymBool l) `symImplies` (SymBool r) = SymBool $ pevalImplyTerm l r

@@ -111,6 +111,7 @@     type (:*:) ((:*:)),     type (:+:) (L1, R1),   )+import Grisette.Core.Control.Exception (AssertionError, VerificationConditions) import Grisette.Core.Data.BV   ( BitwidthMismatch,     IntN (IntN),@@ -118,12 +119,12 @@     SomeWordN (SomeWordN),     WordN (WordN),   )-import Grisette.Core.Data.Class.Bool (ITEOp (ites))+import Grisette.Core.Data.Class.ITEOp (ITEOp (symIte)) import Grisette.IR.SymPrim.Data.Prim.InternedTerm.Term   ( LinkedRep,     SupportedPrim,   )-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim+import Grisette.IR.SymPrim.Data.SymPrim   ( SomeSymIntN (SomeSymIntN),     SomeSymWordN (SomeSymWordN),     SymBool,@@ -193,13 +194,13 @@ -- The 'SimpleStrategy' merges values with a simple merge function. -- For example, -----    * the symbolic boolean values can be directly merged with 'ites'.+--    * the symbolic boolean values can be directly merged with 'symIte'. -- --    * the set @{1}@, which is a subset of the values of the type @Integer@, --        can be simply merged as the set contains only a single value. -- --    * all the 'Just' values of the type @Maybe SymBool@ can be simply merged---        by merging the wrapped symbolic boolean with 'ites'.+--        by merging the wrapped symbolic boolean with 'symIte'. -- -- The 'SortedStrategy' merges values by first grouping the values with an -- indexing function, and the values with the same index will be organized as@@ -242,7 +243,7 @@   --   -- For symbolic booleans, we can implement its merge strategy as follows:   ---  -- > SimpleStrategy ites :: MergingStrategy SymBool+  -- > SimpleStrategy symIte :: MergingStrategy SymBool   SimpleStrategy ::     -- | Merge function.     (SymBool -> a -> a -> a) ->@@ -260,7 +261,7 @@   -- >   (\idx ->   -- >      if idx   -- >        then SimpleStrategy $ \_ t _ -> t-  -- >        else SimpleStrategy $ \cond (Just l) (Just r) -> Just $ ites cond l r)+  -- >        else SimpleStrategy $ \cond (Just l) (Just r) -> Just $ symIte cond l r)   SortedStrategy ::     (Ord idx, Typeable idx, Show idx) =>     -- | Indexing function@@ -315,20 +316,6 @@   -- | The root merging strategy for the type.   rootStrategy :: MergingStrategy a -instance (Generic a, Mergeable' (Rep a)) => Mergeable (Default a) where-  rootStrategy = unsafeCoerce (derivedRootStrategy :: MergingStrategy a)-  {-# NOINLINE rootStrategy #-}---- | Generic derivation for the 'Mergeable' class.------ Usually you can derive the merging strategy with the @DerivingVia@ and--- @DerivingStrategies@ extension.------ > data X = ... deriving (Generic) deriving Mergeable via (Default X)-derivedRootStrategy :: (Generic a, Mergeable' (Rep a)) => MergingStrategy a-derivedRootStrategy = wrapStrategy rootStrategy' to from-{-# INLINE derivedRootStrategy #-}- -- | Lifting of the 'Mergeable' class to unary type constructors. class Mergeable1 (u :: Type -> Type) where   -- | Lift merge strategy through the type constructor.@@ -359,94 +346,6 @@ rootStrategy3 = liftRootStrategy3 rootStrategy rootStrategy rootStrategy {-# INLINE rootStrategy3 #-} -instance (Generic1 u, Mergeable1' (Rep1 u)) => Mergeable1 (Default1 u) where-  liftRootStrategy = unsafeCoerce (derivedLiftMergingStrategy :: MergingStrategy a -> MergingStrategy (u a))-  {-# NOINLINE liftRootStrategy #-}--class Mergeable1' (u :: Type -> Type) where-  liftRootStrategy' :: MergingStrategy a -> MergingStrategy (u a)--instance Mergeable1' U1 where-  liftRootStrategy' _ = SimpleStrategy (\_ t _ -> t)-  {-# INLINE liftRootStrategy' #-}--instance Mergeable1' V1 where-  liftRootStrategy' _ = SimpleStrategy (\_ t _ -> t)-  {-# INLINE liftRootStrategy' #-}--instance Mergeable1' Par1 where-  liftRootStrategy' m = wrapStrategy m Par1 unPar1-  {-# INLINE liftRootStrategy' #-}--instance (Mergeable1 f) => Mergeable1' (Rec1 f) where-  liftRootStrategy' m = wrapStrategy (liftRootStrategy m) Rec1 unRec1-  {-# INLINE liftRootStrategy' #-}--instance (Mergeable c) => Mergeable1' (K1 i c) where-  liftRootStrategy' _ = wrapStrategy rootStrategy K1 unK1-  {-# INLINE liftRootStrategy' #-}--instance (Mergeable1' a) => Mergeable1' (M1 i c a) where-  liftRootStrategy' m = wrapStrategy (liftRootStrategy' m) M1 unM1-  {-# INLINE liftRootStrategy' #-}--instance (Mergeable1' a, Mergeable1' b) => Mergeable1' (a :+: b) where-  liftRootStrategy' m =-    SortedStrategy-      ( \case-          L1 _ -> False-          R1 _ -> True-      )-      ( \idx ->-          if not idx-            then wrapStrategy (liftRootStrategy' m) L1 (\case (L1 v) -> v; _ -> error "impossible")-            else wrapStrategy (liftRootStrategy' m) R1 (\case (R1 v) -> v; _ -> error "impossible")-      )-  {-# INLINE liftRootStrategy' #-}--instance (Mergeable1' a, Mergeable1' b) => Mergeable1' (a :*: b) where-  liftRootStrategy' m = product2Strategy (:*:) (\(a :*: b) -> (a, b)) (liftRootStrategy' m) (liftRootStrategy' m)-  {-# INLINE liftRootStrategy' #-}---- | Generic derivation for the 'Mergeable' class.-derivedLiftMergingStrategy :: (Generic1 u, Mergeable1' (Rep1 u)) => MergingStrategy a -> MergingStrategy (u a)-derivedLiftMergingStrategy m = wrapStrategy (liftRootStrategy' m) to1 from1-{-# INLINE derivedLiftMergingStrategy #-}---- | Auxiliary class for the generic derivation for the 'Mergeable' class.-class Mergeable' f where-  rootStrategy' :: MergingStrategy (f a)--instance Mergeable' U1 where-  rootStrategy' = SimpleStrategy (\_ t _ -> t)-  {-# INLINE rootStrategy' #-}--instance Mergeable' V1 where-  rootStrategy' = SimpleStrategy (\_ t _ -> t)-  {-# INLINE rootStrategy' #-}--instance (Mergeable c) => Mergeable' (K1 i c) where-  rootStrategy' = wrapStrategy rootStrategy K1 unK1-  {-# INLINE rootStrategy' #-}--instance (Mergeable' a) => Mergeable' (M1 i c a) where-  rootStrategy' = wrapStrategy rootStrategy' M1 unM1-  {-# INLINE rootStrategy' #-}--instance (Mergeable' a, Mergeable' b) => Mergeable' (a :+: b) where-  rootStrategy' =-    SortedStrategy-      ( \case-          L1 _ -> False-          R1 _ -> True-      )-      ( \idx ->-          if not idx-            then wrapStrategy rootStrategy' L1 (\case (L1 v) -> v; _ -> undefined)-            else wrapStrategy rootStrategy' R1 (\case (R1 v) -> v; _ -> undefined)-      )-  {-# INLINE rootStrategy' #-}- -- | Useful utility function for building merge strategies for product types -- manually. --@@ -1026,15 +925,15 @@  #define MERGEABLE_SIMPLE(symtype) \ instance Mergeable symtype where \-  rootStrategy = SimpleStrategy ites+  rootStrategy = SimpleStrategy symIte  #define MERGEABLE_BV(symtype) \ instance (KnownNat n, 1 <= n) => Mergeable (symtype n) where \-  rootStrategy = SimpleStrategy ites+  rootStrategy = SimpleStrategy symIte  #define MERGEABLE_FUN(op) \ instance (SupportedPrim ca, SupportedPrim cb, LinkedRep ca sa, LinkedRep cb sb) => Mergeable (sa op sb) where \-  rootStrategy = SimpleStrategy ites+  rootStrategy = SimpleStrategy symIte  #if 1 MERGEABLE_SIMPLE(SymBool)@@ -1053,7 +952,7 @@           SimpleStrategy             ( \c (SomeSymIntN (l :: SymIntN l)) (SomeSymIntN (r :: SymIntN r)) ->                 case unsafeAxiom @l @r of-                  Refl -> SomeSymIntN $ ites c l r+                  Refl -> SomeSymIntN $ symIte c l r             )       ) @@ -1065,7 +964,7 @@           SimpleStrategy             ( \c (SomeSymWordN (l :: SymWordN l)) (SomeSymWordN (r :: SymWordN r)) ->                 case unsafeAxiom @l @r of-                  Refl -> SomeSymWordN $ ites c l r+                  Refl -> SomeSymWordN $ symIte c l r             )       ) @@ -1084,3 +983,109 @@       (const $ SimpleStrategy $ \_ l _ -> l)  deriving via (Default BitwidthMismatch) instance (Mergeable BitwidthMismatch)++deriving via (Default AssertionError) instance Mergeable AssertionError++deriving via (Default VerificationConditions) instance Mergeable VerificationConditions++instance (Generic a, Mergeable' (Rep a)) => Mergeable (Default a) where+  rootStrategy = unsafeCoerce (derivedRootStrategy :: MergingStrategy a)+  {-# NOINLINE rootStrategy #-}++-- | Generic derivation for the 'Mergeable' class.+--+-- Usually you can derive the merging strategy with the @DerivingVia@ and+-- @DerivingStrategies@ extension.+--+-- > data X = ... deriving (Generic) deriving Mergeable via (Default X)+derivedRootStrategy :: (Generic a, Mergeable' (Rep a)) => MergingStrategy a+derivedRootStrategy = wrapStrategy rootStrategy' to from+{-# INLINE derivedRootStrategy #-}++instance (Generic1 u, Mergeable1' (Rep1 u)) => Mergeable1 (Default1 u) where+  liftRootStrategy = unsafeCoerce (derivedLiftMergingStrategy :: MergingStrategy a -> MergingStrategy (u a))+  {-# NOINLINE liftRootStrategy #-}++class Mergeable1' (u :: Type -> Type) where+  liftRootStrategy' :: MergingStrategy a -> MergingStrategy (u a)++instance Mergeable1' U1 where+  liftRootStrategy' _ = SimpleStrategy (\_ t _ -> t)+  {-# INLINE liftRootStrategy' #-}++instance Mergeable1' V1 where+  liftRootStrategy' _ = SimpleStrategy (\_ t _ -> t)+  {-# INLINE liftRootStrategy' #-}++instance Mergeable1' Par1 where+  liftRootStrategy' m = wrapStrategy m Par1 unPar1+  {-# INLINE liftRootStrategy' #-}++instance (Mergeable1 f) => Mergeable1' (Rec1 f) where+  liftRootStrategy' m = wrapStrategy (liftRootStrategy m) Rec1 unRec1+  {-# INLINE liftRootStrategy' #-}++instance (Mergeable c) => Mergeable1' (K1 i c) where+  liftRootStrategy' _ = wrapStrategy rootStrategy K1 unK1+  {-# INLINE liftRootStrategy' #-}++instance (Mergeable1' a) => Mergeable1' (M1 i c a) where+  liftRootStrategy' m = wrapStrategy (liftRootStrategy' m) M1 unM1+  {-# INLINE liftRootStrategy' #-}++instance (Mergeable1' a, Mergeable1' b) => Mergeable1' (a :+: b) where+  liftRootStrategy' m =+    SortedStrategy+      ( \case+          L1 _ -> False+          R1 _ -> True+      )+      ( \idx ->+          if not idx+            then wrapStrategy (liftRootStrategy' m) L1 (\case (L1 v) -> v; _ -> error "impossible")+            else wrapStrategy (liftRootStrategy' m) R1 (\case (R1 v) -> v; _ -> error "impossible")+      )+  {-# INLINE liftRootStrategy' #-}++instance (Mergeable1' a, Mergeable1' b) => Mergeable1' (a :*: b) where+  liftRootStrategy' m = product2Strategy (:*:) (\(a :*: b) -> (a, b)) (liftRootStrategy' m) (liftRootStrategy' m)+  {-# INLINE liftRootStrategy' #-}++-- | Generic derivation for the 'Mergeable' class.+derivedLiftMergingStrategy :: (Generic1 u, Mergeable1' (Rep1 u)) => MergingStrategy a -> MergingStrategy (u a)+derivedLiftMergingStrategy m = wrapStrategy (liftRootStrategy' m) to1 from1+{-# INLINE derivedLiftMergingStrategy #-}++-- | Auxiliary class for the generic derivation for the 'Mergeable' class.+class Mergeable' f where+  rootStrategy' :: MergingStrategy (f a)++instance Mergeable' U1 where+  rootStrategy' = SimpleStrategy (\_ t _ -> t)+  {-# INLINE rootStrategy' #-}++instance Mergeable' V1 where+  rootStrategy' = SimpleStrategy (\_ t _ -> t)+  {-# INLINE rootStrategy' #-}++instance (Mergeable c) => Mergeable' (K1 i c) where+  rootStrategy' = wrapStrategy rootStrategy K1 unK1+  {-# INLINE rootStrategy' #-}++instance (Mergeable' a) => Mergeable' (M1 i c a) where+  rootStrategy' = wrapStrategy rootStrategy' M1 unM1+  {-# INLINE rootStrategy' #-}++instance (Mergeable' a, Mergeable' b) => Mergeable' (a :+: b) where+  rootStrategy' =+    SortedStrategy+      ( \case+          L1 _ -> False+          R1 _ -> True+      )+      ( \idx ->+          if not idx+            then wrapStrategy rootStrategy' L1 (\case (L1 v) -> v; _ -> undefined)+            else wrapStrategy rootStrategy' R1 (\case (R1 v) -> v; _ -> undefined)+      )+  {-# INLINE rootStrategy' #-}

@@ -1,28 +0,0 @@-{-# LANGUAGE GADTs #-}-{-# LANGUAGE MultiParamTypeClasses #-}-{-# LANGUAGE Trustworthy #-}--module Grisette.Core.Data.Class.Mergeable-  ( MergingStrategy (..),-    Mergeable' (..),-    Mergeable (..),-  )-where--import Data.Typeable (Typeable)-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)--data MergingStrategy a where-  SimpleStrategy :: (SymBool -> a -> a -> a) -> MergingStrategy a-  SortedStrategy ::-    (Ord idx, Typeable idx, Show idx) =>-    (a -> idx) ->-    (idx -> MergingStrategy a) ->-    MergingStrategy a-  NoStrategy :: MergingStrategy a--class Mergeable' f where-  rootStrategy' :: MergingStrategy (f a)--class Mergeable a where-  rootStrategy :: MergingStrategy a

@@ -0,0 +1,306 @@+{-# LANGUAGE CPP #-}+{-# LANGUAGE DataKinds #-}+{-# LANGUAGE DerivingVia #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE FlexibleInstances #-}+{-# LANGUAGE GADTs #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE Trustworthy #-}+{-# LANGUAGE TypeApplications #-}+{-# LANGUAGE TypeOperators #-}+{-# LANGUAGE UndecidableInstances #-}++-- |+-- Module      :   Grisette.Core.Data.Class.Bool+-- Copyright   :   (c) Sirui Lu 2021-2023+-- License     :   BSD-3-Clause (see the LICENSE file)+--+-- Maintainer  :   siruilu@cs.washington.edu+-- Stability   :   Experimental+-- Portability :   GHC only+module Grisette.Core.Data.Class.SEq+  ( -- * Symbolic equality+    SEq (..),+    SEq' (..),+  )+where++import Control.Monad.Except (ExceptT (ExceptT))+import Control.Monad.Identity+  ( Identity (Identity),+    IdentityT (IdentityT),+  )+import Control.Monad.Trans.Maybe (MaybeT (MaybeT))+import qualified Control.Monad.Writer.Lazy as WriterLazy+import qualified Control.Monad.Writer.Strict as WriterStrict+import qualified Data.ByteString as B+import Data.Functor.Sum (Sum)+import Data.Int (Int16, Int32, Int64, Int8)+import qualified Data.Text as T+import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))+import Data.Word (Word16, Word32, Word64, Word8)+import GHC.TypeLits (sameNat)+import GHC.TypeNats (KnownNat, type (<=))+import Generics.Deriving+  ( Default (Default),+    Generic (Rep, from),+    K1 (K1),+    M1 (M1),+    U1,+    V1,+    type (:*:) ((:*:)),+    type (:+:) (L1, R1),+  )+import Grisette.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)+import Grisette.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&)))+import Grisette.Core.Data.Class.Solvable (Solvable (con))+import Grisette.IR.SymPrim.Data.Prim.PartialEval.Bool (pevalEqvTerm)+import Grisette.IR.SymPrim.Data.SymPrim+  ( SomeSymIntN (SomeSymIntN),+    SomeSymWordN (SomeSymWordN),+    SymBool (SymBool),+    SymIntN (SymIntN),+    SymInteger (SymInteger),+    SymWordN (SymWordN),+  )++-- $setup+-- >>> import Grisette.Core+-- >>> import Grisette.IR.SymPrim+-- >>> :set -XDataKinds+-- >>> :set -XBinaryLiterals+-- >>> :set -XFlexibleContexts+-- >>> :set -XFlexibleInstances+-- >>> :set -XFunctionalDependencies++-- | Symbolic equality. Note that we can't use Haskell's 'Eq' class since+-- symbolic comparison won't necessarily return a concrete 'Bool' value.+--+-- >>> let a = 1 :: SymInteger+-- >>> let b = 2 :: SymInteger+-- >>> a .== b+-- false+-- >>> a ./= b+-- true+--+-- >>> let a = "a" :: SymInteger+-- >>> let b = "b" :: SymInteger+-- >>> a ./= b+-- (! (= a b))+-- >>> a ./= b+-- (! (= a b))+--+-- __Note:__ This type class can be derived for algebraic data types.+-- You may need the @DerivingVia@ and @DerivingStrategies@ extensions.+--+-- > data X = ... deriving Generic deriving SEq via (Default X)+class SEq a where+  (.==) :: a -> a -> SymBool+  a .== b = symNot $ a ./= b+  {-# INLINE (.==) #-}+  infix 4 .==++  (./=) :: a -> a -> SymBool+  a ./= b = symNot $ a .== b+  {-# INLINE (./=) #-}+  infix 4 ./=+  {-# MINIMAL (.==) | (./=) #-}++-- SEq instances+#define CONCRETE_SEQ(type) \+instance SEq type where \+  l .== r = con $ l == r; \+  {-# INLINE (.==) #-}++#define CONCRETE_SEQ_BV(type) \+instance (KnownNat n, 1 <= n) => SEq (type n) where \+  l .== r = con $ l == r; \+  {-# INLINE (.==) #-}++#if 1+CONCRETE_SEQ(Bool)+CONCRETE_SEQ(Integer)+CONCRETE_SEQ(Char)+CONCRETE_SEQ(Int)+CONCRETE_SEQ(Int8)+CONCRETE_SEQ(Int16)+CONCRETE_SEQ(Int32)+CONCRETE_SEQ(Int64)+CONCRETE_SEQ(Word)+CONCRETE_SEQ(Word8)+CONCRETE_SEQ(Word16)+CONCRETE_SEQ(Word32)+CONCRETE_SEQ(Word64)+CONCRETE_SEQ(B.ByteString)+CONCRETE_SEQ(T.Text)+CONCRETE_SEQ_BV(WordN)+CONCRETE_SEQ_BV(IntN)+CONCRETE_SEQ(SomeWordN)+CONCRETE_SEQ(SomeIntN)+#endif++-- List+deriving via (Default [a]) instance (SEq a) => SEq [a]++-- Maybe+deriving via (Default (Maybe a)) instance (SEq a) => SEq (Maybe a)++-- Either+deriving via (Default (Either e a)) instance (SEq e, SEq a) => SEq (Either e a)++-- ExceptT+instance (SEq (m (Either e a))) => SEq (ExceptT e m a) where+  (ExceptT a) .== (ExceptT b) = a .== b+  {-# INLINE (.==) #-}++-- MaybeT+instance (SEq (m (Maybe a))) => SEq (MaybeT m a) where+  (MaybeT a) .== (MaybeT b) = a .== b+  {-# INLINE (.==) #-}++-- ()+instance SEq () where+  _ .== _ = con True+  {-# INLINE (.==) #-}++-- (,)+deriving via (Default (a, b)) instance (SEq a, SEq b) => SEq (a, b)++-- (,,)+deriving via (Default (a, b, c)) instance (SEq a, SEq b, SEq c) => SEq (a, b, c)++-- (,,,)+deriving via+  (Default (a, b, c, d))+  instance+    (SEq a, SEq b, SEq c, SEq d) =>+    SEq (a, b, c, d)++-- (,,,,)+deriving via+  (Default (a, b, c, d, e))+  instance+    (SEq a, SEq b, SEq c, SEq d, SEq e) =>+    SEq (a, b, c, d, e)++-- (,,,,,)+deriving via+  (Default (a, b, c, d, e, f))+  instance+    (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f) =>+    SEq (a, b, c, d, e, f)++-- (,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g))+  instance+    (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g) =>+    SEq (a, b, c, d, e, f, g)++-- (,,,,,,,)+deriving via+  (Default (a, b, c, d, e, f, g, h))+  instance+    (SEq a, SEq b, SEq c, SEq d, SEq e, SEq f, SEq g, SEq h) =>+    SEq (a, b, c, d, e, f, g, h)++-- Sum+deriving via+  (Default (Sum f g a))+  instance+    (SEq (f a), SEq (g a)) => SEq (Sum f g a)++-- Writer+instance (SEq (m (a, s))) => SEq (WriterLazy.WriterT s m a) where+  (WriterLazy.WriterT l) .== (WriterLazy.WriterT r) = l .== r+  {-# INLINE (.==) #-}++instance (SEq (m (a, s))) => SEq (WriterStrict.WriterT s m a) where+  (WriterStrict.WriterT l) .== (WriterStrict.WriterT r) = l .== r+  {-# INLINE (.==) #-}++-- Identity+instance (SEq a) => SEq (Identity a) where+  (Identity l) .== (Identity r) = l .== r+  {-# INLINE (.==) #-}++-- IdentityT+instance (SEq (m a)) => SEq (IdentityT m a) where+  (IdentityT l) .== (IdentityT r) = l .== r+  {-# INLINE (.==) #-}++-- Symbolic types+#define SEQ_SIMPLE(symtype) \+instance SEq symtype where \+  (symtype l) .== (symtype r) = SymBool $ pevalEqvTerm l r++#define SEQ_BV(symtype) \+instance (KnownNat n, 1 <= n) => SEq (symtype n) where \+  (symtype l) .== (symtype r) = SymBool $ pevalEqvTerm l r++#define SEQ_BV_SOME(somety, origty) \+instance SEq somety where \+  somety (l :: origty l) .== somety (r :: origty r) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> l .== r; \+      Nothing -> con False); \+  {-# INLINE (.==) #-}; \+  somety (l :: origty l) ./= somety (r :: origty r) = \+    (case sameNat (Proxy @l) (Proxy @r) of \+      Just Refl -> l ./= r; \+      Nothing -> con True); \+  {-# INLINE (./=) #-}++#if 1+SEQ_SIMPLE(SymBool)+SEQ_SIMPLE(SymInteger)+SEQ_BV(SymIntN)+SEQ_BV(SymWordN)+SEQ_BV_SOME(SomeSymIntN, SymIntN)+SEQ_BV_SOME(SomeSymWordN, SymWordN)+#endif++-- Exceptions+deriving via (Default AssertionError) instance SEq AssertionError++deriving via (Default VerificationConditions) instance SEq VerificationConditions++-- | Auxiliary class for 'SEq' instance derivation+class SEq' f where+  -- | Auxiliary function for '(..==) derivation+  (..==) :: f a -> f a -> SymBool++  infix 4 ..==++instance SEq' U1 where+  _ ..== _ = con True+  {-# INLINE (..==) #-}++instance SEq' V1 where+  _ ..== _ = con True+  {-# INLINE (..==) #-}++instance (SEq c) => SEq' (K1 i c) where+  (K1 a) ..== (K1 b) = a .== b+  {-# INLINE (..==) #-}++instance (SEq' a) => SEq' (M1 i c a) where+  (M1 a) ..== (M1 b) = a ..== b+  {-# INLINE (..==) #-}++instance (SEq' a, SEq' b) => SEq' (a :+: b) where+  (L1 a) ..== (L1 b) = a ..== b+  (R1 a) ..== (R1 b) = a ..== b+  _ ..== _ = con False+  {-# INLINE (..==) #-}++instance (SEq' a, SEq' b) => SEq' (a :*: b) where+  (a1 :*: b1) ..== (a2 :*: b2) = (a1 ..== a2) .&& (b1 ..== b2)+  {-# INLINE (..==) #-}++instance (Generic a, SEq' (Rep a)) => SEq (Default a) where+  Default l .== Default r = from l ..== from r+  {-# INLINE (.==) #-}

@@ -4,6 +4,7 @@ {-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE FlexibleInstances #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE InstanceSigs #-} {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving #-}@@ -50,19 +51,33 @@     type (:*:) ((:*:)),     type (:+:) (L1, R1),   )-import {-# SOURCE #-} Grisette.Core.Control.Monad.UnionM (UnionM)+import Grisette.Core.Control.Exception (AssertionError, VerificationConditions)+import Grisette.Core.Control.Monad.UnionM (UnionM, liftToMonadUnion) import Grisette.Core.Data.BV (IntN, SomeIntN, SomeWordN, WordN)-import Grisette.Core.Data.Class.Bool-  ( LogicalOp ((&&~), (||~)),-    SEq ((/=~), (==~)),-    SEq' ((==~~)),-  )+import Grisette.Core.Data.Class.LogicalOp (LogicalOp (symNot, (.&&), (.||)))+import Grisette.Core.Data.Class.SEq (SEq ((./=), (.==)), SEq' ((..==))) import Grisette.Core.Data.Class.SimpleMergeable   ( mrgIf,     mrgSingle,+    simpleMerge,   ) import Grisette.Core.Data.Class.Solvable (Solvable (con))-import {-# SOURCE #-} Grisette.IR.SymPrim.Data.SymPrim (SymBool)+import Grisette.IR.SymPrim.Data.Prim.PartialEval.Num+  ( pevalGeNumTerm,+    pevalGtNumTerm,+    pevalLeNumTerm,+    pevalLtNumTerm,+  )+import Grisette.IR.SymPrim.Data.SymPrim+  ( SomeSymIntN,+    SomeSymWordN,+    SymBool (SymBool),+    SymIntN (SymIntN),+    SymInteger (SymInteger),+    SymWordN (SymWordN),+    binSomeSymIntN,+    binSomeSymWordN,+  )  -- $setup -- >>> import Grisette.Core@@ -73,129 +88,26 @@ -- >>> :set -XFlexibleInstances -- >>> :set -XFunctionalDependencies --- | Auxiliary class for 'SOrd' instance derivation-class (SEq' f) => SOrd' f where-  -- | Auxiliary function for '(<~~) derivation-  (<~~) :: f a -> f a -> SymBool--  infix 4 <~~--  -- | Auxiliary function for '(<=~~) derivation-  (<=~~) :: f a -> f a -> SymBool--  infix 4 <=~~--  -- | Auxiliary function for '(>~~) derivation-  (>~~) :: f a -> f a -> SymBool--  infix 4 >~~--  -- | Auxiliary function for '(>=~~) derivation-  (>=~~) :: f a -> f a -> SymBool--  infix 4 >=~~--  -- | Auxiliary function for 'symCompare' derivation-  symCompare' :: f a -> f a -> UnionM Ordering--instance SOrd' U1 where-  _ <~~ _ = con False-  _ <=~~ _ = con True-  _ >~~ _ = con False-  _ >=~~ _ = con True-  symCompare' _ _ = mrgSingle EQ--instance SOrd' V1 where-  _ <~~ _ = con False-  _ <=~~ _ = con True-  _ >~~ _ = con False-  _ >=~~ _ = con True-  symCompare' _ _ = mrgSingle EQ--instance (SOrd c) => SOrd' (K1 i c) where-  (K1 a) <~~ (K1 b) = a <~ b-  (K1 a) <=~~ (K1 b) = a <=~ b-  (K1 a) >~~ (K1 b) = a >~ b-  (K1 a) >=~~ (K1 b) = a >=~ b-  symCompare' (K1 a) (K1 b) = symCompare a b--instance (SOrd' a) => SOrd' (M1 i c a) where-  (M1 a) <~~ (M1 b) = a <~~ b-  (M1 a) <=~~ (M1 b) = a <=~~ b-  (M1 a) >~~ (M1 b) = a >~~ b-  (M1 a) >=~~ (M1 b) = a >=~~ b-  symCompare' (M1 a) (M1 b) = symCompare' a b--instance (SOrd' a, SOrd' b) => SOrd' (a :+: b) where-  (L1 _) <~~ (R1 _) = con True-  (L1 a) <~~ (L1 b) = a <~~ b-  (R1 _) <~~ (L1 _) = con False-  (R1 a) <~~ (R1 b) = a <~~ b-  (L1 _) <=~~ (R1 _) = con True-  (L1 a) <=~~ (L1 b) = a <=~~ b-  (R1 _) <=~~ (L1 _) = con False-  (R1 a) <=~~ (R1 b) = a <=~~ b--  (L1 _) >~~ (R1 _) = con False-  (L1 a) >~~ (L1 b) = a >~~ b-  (R1 _) >~~ (L1 _) = con True-  (R1 a) >~~ (R1 b) = a >~~ b-  (L1 _) >=~~ (R1 _) = con False-  (L1 a) >=~~ (L1 b) = a >=~~ b-  (R1 _) >=~~ (L1 _) = con True-  (R1 a) >=~~ (R1 b) = a >=~~ b--  symCompare' (L1 a) (L1 b) = symCompare' a b-  symCompare' (L1 _) (R1 _) = mrgSingle LT-  symCompare' (R1 a) (R1 b) = symCompare' a b-  symCompare' (R1 _) (L1 _) = mrgSingle GT--instance (SOrd' a, SOrd' b) => SOrd' (a :*: b) where-  (a1 :*: b1) <~~ (a2 :*: b2) = (a1 <~~ a2) ||~ ((a1 ==~~ a2) &&~ (b1 <~~ b2))-  (a1 :*: b1) <=~~ (a2 :*: b2) = (a1 <~~ a2) ||~ ((a1 ==~~ a2) &&~ (b1 <=~~ b2))-  (a1 :*: b1) >~~ (a2 :*: b2) = (a1 >~~ a2) ||~ ((a1 ==~~ a2) &&~ (b1 >~~ b2))-  (a1 :*: b1) >=~~ (a2 :*: b2) = (a1 >~~ a2) ||~ ((a1 ==~~ a2) &&~ (b1 >=~~ b2))-  symCompare' (a1 :*: b1) (a2 :*: b2) = do-    l <- symCompare' a1 a2-    case l of-      EQ -> symCompare' b1 b2-      _ -> mrgSingle l--derivedSymLt :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool-derivedSymLt x y = from x <~~ from y--derivedSymLe :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool-derivedSymLe x y = from x <=~~ from y--derivedSymGt :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool-derivedSymGt x y = from x >~~ from y--derivedSymGe :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool-derivedSymGe x y = from x >=~~ from y--derivedSymCompare :: (Generic a, SOrd' (Rep a)) => a -> a -> UnionM Ordering-derivedSymCompare x y = symCompare' (from x) (from y)- -- | Symbolic total order. Note that we can't use Haskell's 'Ord' class since -- symbolic comparison won't necessarily return a concrete 'Bool' or 'Ordering' -- value. -- -- >>> let a = 1 :: SymInteger -- >>> let b = 2 :: SymInteger--- >>> a <~ b+-- >>> a .< b -- true--- >>> a >~ b+-- >>> a .> b -- false -- -- >>> let a = "a" :: SymInteger -- >>> let b = "b" :: SymInteger--- >>> a <~ b+-- >>> a .< b -- (< a b)--- >>> a <=~ b+-- >>> a .<= b -- (<= a b)--- >>> a >~ b+-- >>> a .> b -- (< b a)--- >>> a >=~ b+-- >>> a .>= b -- (<= b a) -- -- For `symCompare`, `Ordering` is not a solvable type, and the result would@@ -210,46 +122,46 @@ -- -- > data X = ... deriving Generic deriving SOrd via (Default X) class (SEq a) => SOrd a where-  (<~) :: a -> a -> SymBool-  infix 4 <~-  (<=~) :: a -> a -> SymBool-  infix 4 <=~-  (>~) :: a -> a -> SymBool-  infix 4 >~-  (>=~) :: a -> a -> SymBool-  infix 4 >=~-  x <~ y = x <=~ y &&~ x /=~ y-  x >~ y = y <~ x-  x >=~ y = y <=~ x+  (.<) :: a -> a -> SymBool+  infix 4 .<+  (.<=) :: a -> a -> SymBool+  infix 4 .<=+  (.>) :: a -> a -> SymBool+  infix 4 .>+  (.>=) :: a -> a -> SymBool+  infix 4 .>=+  x .< y = x .<= y .&& x ./= y+  x .> y = y .< x+  x .>= y = y .<= x   symCompare :: a -> a -> UnionM Ordering   symCompare l r =     mrgIf-      (l <~ r)+      (l .< r)       (mrgSingle LT)-      (mrgIf (l ==~ r) (mrgSingle EQ) (mrgSingle GT))-  {-# MINIMAL (<=~) #-}+      (mrgIf (l .== r) (mrgSingle EQ) (mrgSingle GT))+  {-# MINIMAL (.<=) #-}  instance (SEq a, Generic a, SOrd' (Rep a)) => SOrd (Default a) where-  (Default l) <=~ (Default r) = l `derivedSymLe` r-  (Default l) <~ (Default r) = l `derivedSymLt` r-  (Default l) >=~ (Default r) = l `derivedSymGe` r-  (Default l) >~ (Default r) = l `derivedSymGt` r+  (Default l) .<= (Default r) = l `derivedSymLe` r+  (Default l) .< (Default r) = l `derivedSymLt` r+  (Default l) .>= (Default r) = l `derivedSymGe` r+  (Default l) .> (Default r) = l `derivedSymGt` r   symCompare (Default l) (Default r) = derivedSymCompare l r  #define CONCRETE_SORD(type) \ instance SOrd type where \-  l <=~ r = con $ l <= r; \-  l <~ r = con $ l < r; \-  l >=~ r = con $ l >= r; \-  l >~ r = con $ l > r; \+  l .<= r = con $ l <= r; \+  l .< r = con $ l < r; \+  l .>= r = con $ l >= r; \+  l .> r = con $ l > r; \   symCompare l r = mrgSingle $ compare l r  #define CONCRETE_SORD_BV(type) \ instance (KnownNat n, 1 <= n) => SOrd (type n) where \-  l <=~ r = con $ l <= r; \-  l <~ r = con $ l < r; \-  l >=~ r = con $ l >= r; \-  l >~ r = con $ l > r; \+  l .<= r = con $ l <= r; \+  l .< r = con $ l < r; \+  l .>= r = con $ l >= r; \+  l .> r = con $ l > r; \   symCompare l r = mrgSingle $ compare l r  #if 1@@ -278,7 +190,7 @@ symCompareSingleList isLess isStrict = go   where     go [] [] = con (not isStrict)-    go (x : xs) (y : ys) = (if isLess then x <~ y else x >~ y) ||~ (x ==~ y &&~ go xs ys)+    go (x : xs) (y : ys) = (if isLess then x .< y else x .> y) .|| (x .== y .&& go xs ys)     go [] _ = if isLess then con True else con False     go _ [] = if isLess then con False else con True @@ -294,10 +206,10 @@ symCompareList _ [] = mrgSingle GT  instance (SOrd a) => SOrd [a] where-  (<=~) = symCompareSingleList True False-  (<~) = symCompareSingleList True True-  (>=~) = symCompareSingleList False False-  (>~) = symCompareSingleList False True+  (.<=) = symCompareSingleList True False+  (.<) = symCompareSingleList True True+  (.>=) = symCompareSingleList False False+  (.>) = symCompareSingleList False True   symCompare = symCompareList  deriving via (Default (Maybe a)) instance (SOrd a) => SOrd (Maybe a)@@ -354,43 +266,239 @@     (SOrd (f a), SOrd (g a)) => SOrd (Sum f g a)  instance (SOrd (m (Maybe a))) => SOrd (MaybeT m a) where-  (MaybeT l) <=~ (MaybeT r) = l <=~ r-  (MaybeT l) <~ (MaybeT r) = l <~ r-  (MaybeT l) >=~ (MaybeT r) = l >=~ r-  (MaybeT l) >~ (MaybeT r) = l >~ r+  (MaybeT l) .<= (MaybeT r) = l .<= r+  (MaybeT l) .< (MaybeT r) = l .< r+  (MaybeT l) .>= (MaybeT r) = l .>= r+  (MaybeT l) .> (MaybeT r) = l .> r   symCompare (MaybeT l) (MaybeT r) = symCompare l r  instance (SOrd (m (Either e a))) => SOrd (ExceptT e m a) where-  (ExceptT l) <=~ (ExceptT r) = l <=~ r-  (ExceptT l) <~ (ExceptT r) = l <~ r-  (ExceptT l) >=~ (ExceptT r) = l >=~ r-  (ExceptT l) >~ (ExceptT r) = l >~ r+  (ExceptT l) .<= (ExceptT r) = l .<= r+  (ExceptT l) .< (ExceptT r) = l .< r+  (ExceptT l) .>= (ExceptT r) = l .>= r+  (ExceptT l) .> (ExceptT r) = l .> r   symCompare (ExceptT l) (ExceptT r) = symCompare l r  instance (SOrd (m (a, s))) => SOrd (WriterLazy.WriterT s m a) where-  (WriterLazy.WriterT l) <=~ (WriterLazy.WriterT r) = l <=~ r-  (WriterLazy.WriterT l) <~ (WriterLazy.WriterT r) = l <~ r-  (WriterLazy.WriterT l) >=~ (WriterLazy.WriterT r) = l >=~ r-  (WriterLazy.WriterT l) >~ (WriterLazy.WriterT r) = l >~ r+  (WriterLazy.WriterT l) .<= (WriterLazy.WriterT r) = l .<= r+  (WriterLazy.WriterT l) .< (WriterLazy.WriterT r) = l .< r+  (WriterLazy.WriterT l) .>= (WriterLazy.WriterT r) = l .>= r+  (WriterLazy.WriterT l) .> (WriterLazy.WriterT r) = l .> r   symCompare (WriterLazy.WriterT l) (WriterLazy.WriterT r) = symCompare l r  instance (SOrd (m (a, s))) => SOrd (WriterStrict.WriterT s m a) where-  (WriterStrict.WriterT l) <=~ (WriterStrict.WriterT r) = l <=~ r-  (WriterStrict.WriterT l) <~ (WriterStrict.WriterT r) = l <~ r-  (WriterStrict.WriterT l) >=~ (WriterStrict.WriterT r) = l >=~ r-  (WriterStrict.WriterT l) >~ (WriterStrict.WriterT r) = l >~ r+  (WriterStrict.WriterT l) .<= (WriterStrict.WriterT r) = l .<= r+  (WriterStrict.WriterT l) .< (WriterStrict.WriterT r) = l .< r+  (WriterStrict.WriterT l) .>= (WriterStrict.WriterT r) = l .>= r+  (WriterStrict.WriterT l) .> (WriterStrict.WriterT r) = l .> r   symCompare (WriterStrict.WriterT l) (WriterStrict.WriterT r) = symCompare l r  instance (SOrd a) => SOrd (Identity a) where-  (Identity l) <=~ (Identity r) = l <=~ r-  (Identity l) <~ (Identity r) = l <~ r-  (Identity l) >=~ (Identity r) = l >=~ r-  (Identity l) >~ (Identity r) = l >~ r+  (Identity l) .<= (Identity r) = l .<= r+  (Identity l) .< (Identity r) = l .< r+  (Identity l) .>= (Identity r) = l .>= r+  (Identity l) .> (Identity r) = l .> r   (Identity l) `symCompare` (Identity r) = l `symCompare` r  instance (SOrd (m a)) => SOrd (IdentityT m a) where-  (IdentityT l) <=~ (IdentityT r) = l <=~ r-  (IdentityT l) <~ (IdentityT r) = l <~ r-  (IdentityT l) >=~ (IdentityT r) = l >=~ r-  (IdentityT l) >~ (IdentityT r) = l >~ r+  (IdentityT l) .<= (IdentityT r) = l .<= r+  (IdentityT l) .< (IdentityT r) = l .< r+  (IdentityT l) .>= (IdentityT r) = l .>= r+  (IdentityT l) .> (IdentityT r) = l .> r   (IdentityT l) `symCompare` (IdentityT r) = l `symCompare` r++-- SOrd+#define SORD_SIMPLE(symtype) \+instance SOrd symtype where \+  (symtype a) .<= (symtype b) = SymBool $ pevalLeNumTerm a b; \+  (symtype a) .< (symtype b) = SymBool $ pevalLtNumTerm a b; \+  (symtype a) .>= (symtype b) = SymBool $ pevalGeNumTerm a b; \+  (symtype a) .> (symtype b) = SymBool $ pevalGtNumTerm a b; \+  a `symCompare` b = mrgIf \+    (a .< b) \+    (mrgSingle LT) \+    (mrgIf (a .== b) (mrgSingle EQ) (mrgSingle GT))++#define SORD_BV(symtype) \+instance (KnownNat n, 1 <= n) => SOrd (symtype n) where \+  (symtype a) .<= (symtype b) = SymBool $ pevalLeNumTerm a b; \+  (symtype a) .< (symtype b) = SymBool $ pevalLtNumTerm a b; \+  (symtype a) .>= (symtype b) = SymBool $ pevalGeNumTerm a b; \+  (symtype a) .> (symtype b) = SymBool $ pevalGtNumTerm a b; \+  a `symCompare` b = mrgIf \+    (a .< b) \+    (mrgSingle LT) \+    (mrgIf (a .== b) (mrgSingle EQ) (mrgSingle GT))++#define SORD_BV_SOME(somety, bf) \+instance SOrd somety where \+  (.<=) = bf (.<=) ".<="; \+  {-# INLINE (.<=) #-}; \+  (.<) = bf (.<) ".<"; \+  {-# INLINE (.<) #-}; \+  (.>=) = bf (.>=) ".>="; \+  {-# INLINE (.>=) #-}; \+  (.>) = bf (.>) ".>"; \+  {-# INLINE (.>) #-}; \+  symCompare = bf symCompare "symCompare"; \+  {-# INLINE symCompare #-}++instance SOrd SymBool where+  l .<= r = symNot l .|| r+  l .< r = symNot l .&& r+  l .>= r = l .|| symNot r+  l .> r = l .&& symNot r+  symCompare l r =+    mrgIf+      (symNot l .&& r)+      (mrgSingle LT)+      (mrgIf (l .== r) (mrgSingle EQ) (mrgSingle GT))++#if 1+SORD_SIMPLE(SymInteger)+SORD_BV(SymIntN)+SORD_BV(SymWordN)+SORD_BV_SOME(SomeSymIntN, binSomeSymIntN)+SORD_BV_SOME(SomeSymWordN, binSomeSymWordN)+#endif++-- Exception+instance SOrd AssertionError where+  _ .<= _ = con True+  _ .< _ = con False+  _ .>= _ = con True+  _ .> _ = con False+  _ `symCompare` _ = mrgSingle EQ++instance SOrd VerificationConditions where+  l .>= r = con $ l >= r+  l .> r = con $ l > r+  l .<= r = con $ l <= r+  l .< r = con $ l < r+  l `symCompare` r = mrgSingle $ l `compare` r++-- UnionM+instance (SOrd a) => SOrd (UnionM a) where+  x .<= y = simpleMerge $ do+    x1 <- x+    y1 <- y+    mrgSingle $ x1 .<= y1+  x .< y = simpleMerge $ do+    x1 <- x+    y1 <- y+    mrgSingle $ x1 .< y1+  x .>= y = simpleMerge $ do+    x1 <- x+    y1 <- y+    mrgSingle $ x1 .>= y1+  x .> y = simpleMerge $ do+    x1 <- x+    y1 <- y+    mrgSingle $ x1 .> y1+  x `symCompare` y = liftToMonadUnion $ do+    x1 <- x+    y1 <- y+    x1 `symCompare` y1++-- | Auxiliary class for 'SOrd' instance derivation+class (SEq' f) => SOrd' f where+  -- | Auxiliary function for '(..<) derivation+  (..<) :: f a -> f a -> SymBool++  infix 4 ..<++  -- | Auxiliary function for '(..<=) derivation+  (..<=) :: f a -> f a -> SymBool++  infix 4 ..<=++  -- | Auxiliary function for '(..>) derivation+  (..>) :: f a -> f a -> SymBool++  infix 4 ..>++  -- | Auxiliary function for '(..>=) derivation+  (..>=) :: f a -> f a -> SymBool++  infix 4 ..>=++  -- | Auxiliary function for 'symCompare' derivation+  symCompare' :: f a -> f a -> UnionM Ordering++instance SOrd' U1 where+  _ ..< _ = con False+  _ ..<= _ = con True+  _ ..> _ = con False+  _ ..>= _ = con True+  symCompare' _ _ = mrgSingle EQ++instance SOrd' V1 where+  _ ..< _ = con False+  _ ..<= _ = con True+  _ ..> _ = con False+  _ ..>= _ = con True+  symCompare' _ _ = mrgSingle EQ++instance (SOrd c) => SOrd' (K1 i c) where+  (K1 a) ..< (K1 b) = a .< b+  (K1 a) ..<= (K1 b) = a .<= b+  (K1 a) ..> (K1 b) = a .> b+  (K1 a) ..>= (K1 b) = a .>= b+  symCompare' (K1 a) (K1 b) = symCompare a b++instance (SOrd' a) => SOrd' (M1 i c a) where+  (M1 a) ..< (M1 b) = a ..< b+  (M1 a) ..<= (M1 b) = a ..<= b+  (M1 a) ..> (M1 b) = a ..> b+  (M1 a) ..>= (M1 b) = a ..>= b+  symCompare' (M1 a) (M1 b) = symCompare' a b++instance (SOrd' a, SOrd' b) => SOrd' (a :+: b) where+  (L1 _) ..< (R1 _) = con True+  (L1 a) ..< (L1 b) = a ..< b+  (R1 _) ..< (L1 _) = con False+  (R1 a) ..< (R1 b) = a ..< b+  (L1 _) ..<= (R1 _) = con True+  (L1 a) ..<= (L1 b) = a ..<= b+  (R1 _) ..<= (L1 _) = con False+  (R1 a) ..<= (R1 b) = a ..<= b++  (L1 _) ..> (R1 _) = con False+  (L1 a) ..> (L1 b) = a ..> b+  (R1 _) ..> (L1 _) = con True+  (R1 a) ..> (R1 b) = a ..> b+  (L1 _) ..>= (R1 _) = con False+  (L1 a) ..>= (L1 b) = a ..>= b+  (R1 _) ..>= (L1 _) = con True+  (R1 a) ..>= (R1 b) = a ..>= b++  symCompare' (L1 a) (L1 b) = symCompare' a b+  symCompare' (L1 _) (R1 _) = mrgSingle LT+  symCompare' (R1 a) (R1 b) = symCompare' a b+  symCompare' (R1 _) (L1 _) = mrgSingle GT++instance (SOrd' a, SOrd' b) => SOrd' (a :*: b) where+  (a1 :*: b1) ..< (a2 :*: b2) = (a1 ..< a2) .|| ((a1 ..== a2) .&& (b1 ..< b2))+  (a1 :*: b1) ..<= (a2 :*: b2) = (a1 ..< a2) .|| ((a1 ..== a2) .&& (b1 ..<= b2))+  (a1 :*: b1) ..> (a2 :*: b2) = (a1 ..> a2) .|| ((a1 ..== a2) .&& (b1 ..> b2))+  (a1 :*: b1) ..>= (a2 :*: b2) = (a1 ..> a2) .|| ((a1 ..== a2) .&& (b1 ..>= b2))+  symCompare' (a1 :*: b1) (a2 :*: b2) = do+    l <- symCompare' a1 a2+    case l of+      EQ -> symCompare' b1 b2+      _ -> mrgSingle l++derivedSymLt :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool+derivedSymLt x y = from x ..< from y++derivedSymLe :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool+derivedSymLe x y = from x ..<= from y++derivedSymGt :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool+derivedSymGt x y = from x ..> from y++derivedSymGe :: (Generic a, SOrd' (Rep a)) => a -> a -> SymBool+derivedSymGe x y = from x ..>= from y++derivedSymCompare :: (Generic a, SOrd' (Rep a)) => a -> a -> UnionM Ordering+derivedSymCompare x y = symCompare' (from x) (from y)

@@ -1,444 +0,0 @@-{-# LANGUAGE CPP #-}-{-# LANGUAGE DataKinds #-}-{-# LANGUAGE FlexibleContexts #-}-{-# LANGUAGE FlexibleInstances #-}-{-# LANGUAGE FunctionalDependencies #-}-{-# LANGUAGE GADTs #-}-{-# LANGUAGE RankNTypes #-}-{-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE Trustworthy #-}-{-# LANGUAGE TypeApplications #-}-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE UndecidableInstances #-}--{- HLINT ignore "Redundant bracket" -}---- |--- Module      :   Grisette.Core.Data.Class.SafeArith--- Copyright   :   (c) Sirui Lu 2021-2023--- License     :   BSD-3-Clause (see the LICENSE file)------ Maintainer  :   siruilu@cs.washington.edu--- Stability   :   Experimental--- Portability :   GHC only-module Grisette.Core.Data.Class.SafeArith-  ( -- * Symbolic integer operations-    ArithException (..),-    SafeDivision (..),-    SafeLinearArith (..),-    SymIntegerOp,-  )-where--import Control.Exception (ArithException (DivideByZero, Overflow, Underflow))-import Control.Monad.Except (MonadError (throwError))-import Data.Int (Int16, Int32, Int64, Int8)-import Data.Typeable (Proxy (Proxy), type (:~:) (Refl))-import Data.Word (Word16, Word32, Word64, Word8)-import GHC.TypeNats (KnownNat, sameNat, type (<=))-import Grisette.Core.Control.Monad.Union (MonadUnion)-import Grisette.Core.Data.BV-  ( BitwidthMismatch (BitwidthMismatch),-    IntN,-    SomeIntN (SomeIntN),-    SomeWordN (SomeWordN),-    WordN,-  )-import Grisette.Core.Data.Class.Bool-  ( LogicalOp ((&&~), (||~)),-    SEq ((==~)),-  )-import Grisette.Core.Data.Class.Mergeable (Mergeable)-import Grisette.Core.Data.Class.SOrd-  ( SOrd ((<=~), (<~), (>=~), (>~)),-  )-import Grisette.Core.Data.Class.SimpleMergeable-  ( merge,-    mrgIf,-    mrgSingle,-  )-import Grisette.Core.Data.Class.Solvable (Solvable (con))---- $setup--- >>> import Grisette.Core--- >>> import Grisette.IR.SymPrim--- >>> import Control.Monad.Except---- | Safe division with monadic error handling in multi-path--- execution. These procedures throw an exception when the--- divisor is zero. The result should be able to handle errors with--- `MonadError`.-class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeDivision e a | a -> e where-  -- | Safe signed 'div' with monadic error handling in multi-path execution.-  ---  -- >>> safeDiv (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger-  -- ExceptT {If (= b 0) (Left divide by zero) (Right (div a b))}-  safeDiv :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a-  safeDiv l r = do-    (d, _) <- safeDivMod l r-    mrgSingle d--  -- | Safe signed 'mod' with monadic error handling in multi-path execution.-  ---  -- >>> safeMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger-  -- ExceptT {If (= b 0) (Left divide by zero) (Right (mod a b))}-  safeMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a-  safeMod l r = do-    (_, m) <- safeDivMod l r-    mrgSingle m--  -- | Safe signed 'divMod' with monadic error handling in multi-path execution.-  ---  -- >>> safeDivMod (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymInteger, SymInteger)-  -- ExceptT {If (= b 0) (Left divide by zero) (Right ((div a b),(mod a b)))}-  safeDivMod :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)-  safeDivMod l r = do-    d <- safeDiv l r-    m <- safeMod l r-    mrgSingle (d, m)--  -- | Safe signed 'quot' with monadic error handling in multi-path execution.-  safeQuot :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a-  safeQuot l r = do-    (d, m) <- safeDivMod l r-    mrgIf-      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)-      (mrgSingle d)-      (mrgSingle $ d + 1)--  -- | Safe signed 'rem' with monadic error handling in multi-path execution.-  safeRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a-  safeRem l r = do-    (_, m) <- safeDivMod l r-    mrgIf-      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)-      (mrgSingle m)-      (mrgSingle $ m - r)--  -- | Safe signed 'quotRem' with monadic error handling in multi-path execution.-  safeQuotRem :: (MonadError e uf, MonadUnion uf) => a -> a -> uf (a, a)-  safeQuotRem l r = do-    (d, m) <- safeDivMod l r-    mrgIf-      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)-      (mrgSingle (d, m))-      (mrgSingle (d + 1, m - r))--  -- | Safe signed 'div' with monadic error handling in multi-path execution.-  -- The error is transformed.-  ---  -- >>> safeDiv' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger-  -- ExceptT {If (= b 0) (Left ()) (Right (div a b))}-  safeDiv' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a-  safeDiv' t l r = do-    (d, _) <- safeDivMod' t l r-    mrgSingle d--  -- | Safe signed 'mod' with monadic error handling in multi-path execution.-  -- The error is transformed.-  ---  -- >>> safeMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM SymInteger-  -- ExceptT {If (= b 0) (Left ()) (Right (mod a b))}-  safeMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a-  safeMod' t l r = do-    (_, m) <- safeDivMod' t l r-    mrgSingle m--  -- | Safe signed 'divMod' with monadic error handling in multi-path execution.-  -- The error is transformed.-  ---  -- >>> safeDivMod' (const ()) (ssym "a") (ssym "b") :: ExceptT () UnionM (SymInteger, SymInteger)-  -- ExceptT {If (= b 0) (Left ()) (Right ((div a b),(mod a b)))}-  safeDivMod' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)-  safeDivMod' t l r = do-    d <- safeDiv' t l r-    m <- safeMod' t l r-    mrgSingle (d, m)--  -- | Safe signed 'quot' with monadic error handling in multi-path execution.-  -- The error is transformed.-  safeQuot' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a-  safeQuot' t l r = do-    (d, m) <- safeDivMod' t l r-    mrgIf-      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)-      (mrgSingle d)-      (mrgSingle $ d + 1)--  -- | Safe signed 'rem' with monadic error handling in multi-path execution.-  -- The error is transformed.-  safeRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a-  safeRem' t l r = do-    (_, m) <- safeDivMod' t l r-    mrgIf-      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)-      (mrgSingle m)-      (mrgSingle $ m - r)--  -- | Safe signed 'quotRem' with monadic error handling in multi-path execution.-  -- The error is transformed.-  safeQuotRem' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf (a, a)-  safeQuotRem' t l r = do-    (d, m) <- safeDivMod' t l r-    mrgIf-      ((l >=~ 0 &&~ r >~ 0) ||~ (l <=~ 0 &&~ r <~ 0) ||~ m ==~ 0)-      (mrgSingle (d, m))-      (mrgSingle (d + 1, m - r))--  {-# MINIMAL (safeDivMod | (safeDiv, safeMod)), (safeDivMod' | (safeDiv', safeMod')) #-}--#define QUOTE() '-#define QID(a) a-#define QRIGHT(a) QID(a)'--#define QRIGHTT(a) QID(a)' t'-#define QRIGHTU(a) QID(a)' _'--#define SAFE_DIVISION_FUNC(name, op) \-name _ r | r == 0 = merge $ throwError DivideByZero; \-name l r = mrgSingle $ l `op` r; \-QRIGHTT(name) _ r | r == 0 = let _ = t' in merge $ throwError (t' DivideByZero); \-QRIGHTU(name) l r = mrgSingle $ l `op` r--#define SAFE_DIVISION_CONCRETE(type) \-instance SafeDivision ArithException type where \-  SAFE_DIVISION_FUNC(safeDiv, div); \-  SAFE_DIVISION_FUNC(safeMod, mod); \-  SAFE_DIVISION_FUNC(safeDivMod, divMod); \-  SAFE_DIVISION_FUNC(safeQuot, quot); \-  SAFE_DIVISION_FUNC(safeRem, rem); \-  SAFE_DIVISION_FUNC(safeQuotRem, quotRem)--#define SAFE_DIVISION_CONCRETE_BV(type) \-instance (KnownNat n, 1 <= n) => SafeDivision ArithException (type n) where \-  SAFE_DIVISION_FUNC(safeDiv, div); \-  SAFE_DIVISION_FUNC(safeMod, mod); \-  SAFE_DIVISION_FUNC(safeDivMod, divMod); \-  SAFE_DIVISION_FUNC(safeQuot, quot); \-  SAFE_DIVISION_FUNC(safeRem, rem); \-  SAFE_DIVISION_FUNC(safeQuotRem, quotRem)--#if 1-SAFE_DIVISION_CONCRETE(Integer)-SAFE_DIVISION_CONCRETE(Int8)-SAFE_DIVISION_CONCRETE(Int16)-SAFE_DIVISION_CONCRETE(Int32)-SAFE_DIVISION_CONCRETE(Int64)-SAFE_DIVISION_CONCRETE(Int)-SAFE_DIVISION_CONCRETE(Word8)-SAFE_DIVISION_CONCRETE(Word16)-SAFE_DIVISION_CONCRETE(Word32)-SAFE_DIVISION_CONCRETE(Word64)-SAFE_DIVISION_CONCRETE(Word)-#endif--#define SAFE_DIVISION_FUNC_SOME(stype, type, name, op) \-  name (stype (l :: type l)) (stype (r :: type r)) = \-    (case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> \-        if r == 0 \-          then merge $ throwError $ Right DivideByZero \-          else mrgSingle $ stype $ l `op` r; \-      Nothing -> merge $ throwError $ Left BitwidthMismatch); \-  QRIGHT(name) t (stype (l :: type l)) (stype (r :: type r)) = \-    (case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> \-        if r == 0 \-          then merge $ throwError $ t (Right DivideByZero) \-          else mrgSingle $ stype $ l `op` r; \-      Nothing -> merge $ throwError $ t (Left BitwidthMismatch))--#define SAFE_DIVISION_FUNC_SOME_DIVMOD(stype, type, name, op) \-  name (stype (l :: type l)) (stype (r :: type r)) = \-    (case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> \-        if r == 0 \-          then merge $ throwError $ Right DivideByZero \-          else (case l `op` r of (d, m) -> mrgSingle (stype d, stype m)); \-      Nothing -> merge $ throwError $ Left BitwidthMismatch); \-  QRIGHT(name) t (stype (l :: type l)) (stype (r :: type r)) = \-    (case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> \-        if r == 0 \-          then merge $ throwError $ t (Right DivideByZero) \-          else (case l `op` r of (d, m) -> mrgSingle (stype d, stype m)); \-      Nothing -> merge $ throwError $ t (Left BitwidthMismatch))--#if 1-SAFE_DIVISION_CONCRETE_BV(IntN)-SAFE_DIVISION_CONCRETE_BV(WordN)-instance SafeDivision (Either BitwidthMismatch ArithException) SomeIntN where-  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeDiv, div)-  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeMod, mod)-  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeIntN, IntN, safeDivMod, divMod)-  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeQuot, quot)-  SAFE_DIVISION_FUNC_SOME(SomeIntN, IntN, safeRem, rem)-  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeIntN, IntN, safeQuotRem, quotRem)--instance SafeDivision (Either BitwidthMismatch ArithException) SomeWordN where-  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeDiv, div)-  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeMod, mod)-  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeWordN, WordN, safeDivMod, divMod)-  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeQuot, quot)-  SAFE_DIVISION_FUNC_SOME(SomeWordN, WordN, safeRem, rem)-  SAFE_DIVISION_FUNC_SOME_DIVMOD(SomeWordN, WordN, safeQuotRem, quotRem)-#endif---- | Safe division with monadic error handling in multi-path--- execution. These procedures throw an exception when overflow or underflow happens.--- The result should be able to handle errors with `MonadError`.-class (SOrd a, Num a, Mergeable a, Mergeable e) => SafeLinearArith e a | a -> e where-  -- | Safe '+' with monadic error handling in multi-path execution.-  -- Overflows or underflows are treated as errors.-  ---  -- >>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger-  -- ExceptT {Right (+ a b)}-  -- >>> safeAdd (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)-  -- ExceptT {If (ite (< 0x0 a) (&& (< 0x0 b) (< (+ a b) 0x0)) (&& (< a 0x0) (&& (< b 0x0) (<= 0x0 (+ a b))))) (If (< 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a b))}-  safeAdd :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a--  -- | Safe 'negate' with monadic error handling in multi-path execution.-  -- Overflows or underflows are treated as errors.-  ---  -- >>> safeNeg (ssym "a") :: ExceptT ArithException UnionM SymInteger-  -- ExceptT {Right (- a)}-  -- >>> safeNeg (ssym "a") :: ExceptT ArithException UnionM (SymIntN 4)-  -- ExceptT {If (= a 0x8) (Left arithmetic overflow) (Right (- a))}-  safeNeg :: (MonadError e uf, MonadUnion uf) => a -> uf a--  -- | Safe '-' with monadic error handling in multi-path execution.-  -- Overflows or underflows are treated as errors.-  ---  -- >>> safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM SymInteger-  -- ExceptT {Right (+ a (- b))}-  -- >>> safeMinus (ssym "a") (ssym "b") :: ExceptT ArithException UnionM (SymIntN 4)-  -- ExceptT {If (ite (<= 0x0 a) (&& (< b 0x0) (< (+ a (- b)) 0x0)) (&& (< a 0x0) (&& (< 0x0 b) (< 0x0 (+ a (- b)))))) (If (<= 0x0 a) (Left arithmetic overflow) (Left arithmetic underflow)) (Right (+ a (- b)))}-  safeMinus :: (MonadError e uf, MonadUnion uf) => a -> a -> uf a--  -- | Safe '+' with monadic error handling in multi-path execution.-  -- Overflows or underflows are treated as errors.-  -- The error is transformed.-  safeAdd' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a--  -- | Safe 'negate' with monadic error handling in multi-path execution.-  -- Overflows or underflows are treated as errors.-  -- The error is transformed.-  safeNeg' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> uf a--  -- | Safe '-' with monadic error handling in multi-path execution.-  -- Overflows or underflows are treated as errors.-  -- The error is transformed.-  safeMinus' :: (MonadError e' uf, MonadUnion uf, Mergeable e') => (e -> e') -> a -> a -> uf a--instance SafeLinearArith ArithException Integer where-  safeAdd l r = mrgSingle (l + r)-  safeNeg l = mrgSingle (-l)-  safeMinus l r = mrgSingle (l - r)-  safeAdd' _ l r = mrgSingle (l + r)-  safeNeg' _ l = mrgSingle (-l)-  safeMinus' _ l r = mrgSingle (l - r)--#define SAFE_LINARITH_SIGNED_CONCRETE_BODY \-  safeAdd l r = let res = l + r in \-    mrgIf (con $ l > 0 && r > 0 && res < 0) \-          (throwError Overflow) \-          (mrgIf (con $ l < 0 && r < 0 && res >= 0) \-                 (throwError Underflow) \-                 (return res));\-  safeAdd' t' l r = let res = l + r in \-    mrgIf (con $ l > 0 && r > 0 && res < 0) \-          (throwError (t' Overflow)) \-          (mrgIf (con $ l < 0 && r < 0 && res >= 0) \-                 (throwError (t' Underflow)) \-                 (return res)); \-  safeMinus l r = let res = l - r in \-    mrgIf (con $ l >= 0 && r < 0 && res < 0) \-          (throwError Overflow) \-          (mrgIf (con $ l < 0 && r > 0 && res > 0) \-                 (throwError Underflow) \-                 (return res));\-  safeMinus' t' l r = let res = l - r in \-    mrgIf (con $ l >= 0 && r < 0 && res < 0) \-          (throwError (t' Overflow)) \-          (mrgIf (con $ l < 0 && r > 0 && res > 0) \-                 (throwError (t' Underflow)) \-                 (return res)); \-  safeNeg v = mrgIf (con $ v == minBound) (throwError Overflow) (return $ -v);\-  safeNeg' t' v = mrgIf (con $ v == minBound) (throwError (t' Overflow)) (return $ -v)--#define SAFE_LINARITH_SIGNED_CONCRETE(type) \-instance SafeLinearArith ArithException type where \-  SAFE_LINARITH_SIGNED_CONCRETE_BODY--#define SAFE_LINARITH_SIGNED_BV_CONCRETE(type) \-instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (type n) where \-  SAFE_LINARITH_SIGNED_CONCRETE_BODY--#define SAFE_LINARITH_UNSIGNED_CONCRETE_BODY \-  safeAdd l r = let res = l + r in \-    mrgIf (con $ l > res || r > res) \-          (throwError Overflow) \-          (return res);\-  safeAdd' t' l r = let res = l + r in \-    mrgIf (con $ l > res || r > res) \-          (throwError (t' Overflow)) \-          (return res); \-  safeMinus l r = \-    mrgIf (con $ r > l) \-          (throwError Underflow) \-          (return $ l - r);\-  safeMinus' t' l r = \-    mrgIf (con $ r > l) \-          (throwError $ t' Underflow) \-          (return $ l - r);\-  safeNeg v = mrgIf (con $ v /= 0) (throwError Underflow) (return $ -v);\-  safeNeg' t' v = mrgIf (con $ v /= 0) (throwError (t' Underflow)) (return $ -v)--#define SAFE_LINARITH_UNSIGNED_CONCRETE(type) \-instance SafeLinearArith ArithException type where \-  SAFE_LINARITH_UNSIGNED_CONCRETE_BODY--#define SAFE_LINARITH_UNSIGNED_BV_CONCRETE(type) \-instance (KnownNat n, 1 <= n) => SafeLinearArith ArithException (type n) where \-  SAFE_LINARITH_UNSIGNED_CONCRETE_BODY--#define SAFE_LINARITH_SOME_CONCRETE(type, ctype) \-instance SafeLinearArith (Either BitwidthMismatch ArithException) type where \-  safeAdd (type (l :: ctype l)) (type (r :: ctype r)) = merge (\-    case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> type <$> safeAdd' Right l r; \-      _ -> throwError $ Left BitwidthMismatch); \-  safeAdd' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\-    case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> type <$> safeAdd' (t . Right) l r; \-      _ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \-  safeMinus (type (l :: ctype l)) (type (r :: ctype r)) = merge (\-    case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> type <$> safeMinus' Right l r; \-      _ -> throwError $ Left BitwidthMismatch); \-  safeMinus' t (type (l :: ctype l)) (type (r :: ctype r)) = merge (\-    case sameNat (Proxy @l) (Proxy @r) of \-      Just Refl -> type <$> safeMinus' (t . Right) l r; \-      _ -> let t' = t; _ = t' in throwError $ t' $ Left BitwidthMismatch); \-  safeNeg (type l) = merge $ type <$> safeNeg' Right l; \-  safeNeg' t (type l) = merge $ type <$> safeNeg' (t . Right) l--#if 1-SAFE_LINARITH_SIGNED_CONCRETE(Int8)-SAFE_LINARITH_SIGNED_CONCRETE(Int16)-SAFE_LINARITH_SIGNED_CONCRETE(Int32)-SAFE_LINARITH_SIGNED_CONCRETE(Int64)-SAFE_LINARITH_SIGNED_CONCRETE(Int)-SAFE_LINARITH_SIGNED_BV_CONCRETE(IntN)-SAFE_LINARITH_SOME_CONCRETE(SomeIntN, IntN)-SAFE_LINARITH_UNSIGNED_CONCRETE(Word8)-SAFE_LINARITH_UNSIGNED_CONCRETE(Word16)-SAFE_LINARITH_UNSIGNED_CONCRETE(Word32)-SAFE_LINARITH_UNSIGNED_CONCRETE(Word64)-SAFE_LINARITH_UNSIGNED_CONCRETE(Word)-SAFE_LINARITH_UNSIGNED_BV_CONCRETE(WordN)-SAFE_LINARITH_SOME_CONCRETE(SomeWordN, WordN)-#endif---- | Aggregation for the operations on symbolic integer types-class (Num a, SEq a, SOrd a, Solvable Integer a) => SymIntegerOp a