sbv 9.0 → 14.4

raw patch · 1463 files changed

Files

• CHANGES.md +944/−29
• COPYRIGHT +1/−1
• Data/SBV.hs +564/−174
• Data/SBV/Char.hs +39/−12
• Data/SBV/Client.hs +698/−96
• Data/SBV/Client/BaseIO.hs +73/−329
• Data/SBV/Compilers/C.hs +117/−90
• Data/SBV/Compilers/CodeGen.hs +15/−21
• Data/SBV/Control.hs +11/−27
• Data/SBV/Control/BaseIO.hs +42/−39
• Data/SBV/Control/Query.hs +124/−260
• Data/SBV/Control/Types.hs +21/−39
• Data/SBV/Control/Utils.hs +2173/−1823
• Data/SBV/Core/AlgReals.hs +52/−16
• Data/SBV/Core/Concrete.hs +222/−209
• Data/SBV/Core/Data.hs +648/−239
• Data/SBV/Core/Floating.hs +78/−71
• Data/SBV/Core/Kind.hs +213/−210
• Data/SBV/Core/Model.hs +4837/−2722
• Data/SBV/Core/Operations.hs +2047/−1426
• Data/SBV/Core/Sized.hs +69/−197
• Data/SBV/Core/SizedFloats.hs +310/−53
• Data/SBV/Core/Symbolic.hs +2325/−2112
• Data/SBV/Core/TH.hs +142/−0
• Data/SBV/Dynamic.hs +40/−28
• Data/SBV/Either.hs +48/−136
• Data/SBV/Internals.hs +38/−14
• Data/SBV/Lambda.hs +485/−0
• Data/SBV/List.hs +1536/−403
• Data/SBV/Maybe.hs +57/−99
• Data/SBV/Provers/ABC.hs +20/−19
• Data/SBV/Provers/Bitwuzla.hs +21/−20
• Data/SBV/Provers/Boolector.hs +20/−19
• Data/SBV/Provers/CVC4.hs +30/−24
• Data/SBV/Provers/CVC5.hs +31/−25
• Data/SBV/Provers/DReal.hs +20/−21
• Data/SBV/Provers/MathSAT.hs +20/−21
• Data/SBV/Provers/OpenSMT.hs +54/−0
• Data/SBV/Provers/Prover.hs +483/−516
• Data/SBV/Provers/Yices.hs +20/−21
• Data/SBV/Provers/Z3.hs +24/−25
• Data/SBV/Rational.hs +62/−4
• Data/SBV/RegExp.hs +38/−37
• Data/SBV/SCase.hs +1409/−0
• Data/SBV/SEnum.hs +203/−0
• Data/SBV/SMT/SMT.hs +315/−287
• Data/SBV/SMT/SMTLib.hs +7/−33
• Data/SBV/SMT/SMTLib2.hs +1359/−1388
• Data/SBV/SMT/SMTLibNames.hs +6/−2
• Data/SBV/SMT/Utils.hs +178/−74
• Data/SBV/Set.hs +57/−92
• Data/SBV/String.hs +0/−442
• Data/SBV/TP.hs +84/−0
• Data/SBV/TP/Kernel.hs +379/−0
• Data/SBV/TP/TP.hs +1583/−0
• Data/SBV/TP/Utils.hs +707/−0
• Data/SBV/Tools/BMC.hs +76/−30
• Data/SBV/Tools/BVOptimize.hs +126/−0
• Data/SBV/Tools/BoundedFix.hs +0/−88
• Data/SBV/Tools/BoundedList.hs +0/−149
• Data/SBV/Tools/CodeGen.hs +1/−1
• Data/SBV/Tools/GenTest.hs +75/−55
• Data/SBV/Tools/Induction.hs +26/−20
• Data/SBV/Tools/Overflow.hs +98/−251
• Data/SBV/Tools/Polynomial.hs +13/−10
• Data/SBV/Tools/Range.hs +24/−19
• Data/SBV/Tools/STree.hs +1/−1
• Data/SBV/Tools/WeakestPreconditions.hs +54/−54
• Data/SBV/Trans.hs +14/−22
• Data/SBV/Trans/Control.hs +5/−8
• Data/SBV/Tuple.hs +63/−5
• Data/SBV/Utils/CrackNum.hs +64/−30
• Data/SBV/Utils/ExtractIO.hs +5/−5
• Data/SBV/Utils/Lib.hs +168/−9
• Data/SBV/Utils/Numeric.hs +39/−7
• Data/SBV/Utils/PrettyNum.hs +170/−193
• Data/SBV/Utils/SExpr.hs +287/−110
• Data/SBV/Utils/TDiff.hs +34/−1
• Documentation/SBV/Examples/ADT/Expr.hs +172/−0
• Documentation/SBV/Examples/ADT/Param.hs +191/−0
• Documentation/SBV/Examples/ADT/Types.hs +131/−0
• Documentation/SBV/Examples/BitPrecise/Adders.hs +185/−0
• Documentation/SBV/Examples/BitPrecise/BitTricks.hs +1/−2
• Documentation/SBV/Examples/BitPrecise/BrokenSearch.hs +12/−8
• Documentation/SBV/Examples/BitPrecise/Legato.hs +14/−14
• Documentation/SBV/Examples/BitPrecise/MergeSort.hs +11/−4
• Documentation/SBV/Examples/BitPrecise/MultMask.hs +0/−64
• Documentation/SBV/Examples/BitPrecise/PEXT_PDEP.hs +163/−0
• Documentation/SBV/Examples/BitPrecise/PrefixSum.hs +14/−13
• Documentation/SBV/Examples/CodeGeneration/Fibonacci.hs +15/−8
• Documentation/SBV/Examples/CodeGeneration/GCD.hs +7/−4
• Documentation/SBV/Examples/CodeGeneration/PopulationCount.hs +5/−2
• Documentation/SBV/Examples/CodeGeneration/Uninterpreted.hs +5/−1
• Documentation/SBV/Examples/Crypto/AES.hs +380/−68
• Documentation/SBV/Examples/Crypto/Prince.hs +267/−0
• Documentation/SBV/Examples/Crypto/RC4.hs +4/−6
• Documentation/SBV/Examples/Crypto/SHA.hs +21/−5
• Documentation/SBV/Examples/Existentials/CRCPolynomial.hs +0/−89
• Documentation/SBV/Examples/Existentials/Diophantine.hs +68/−37
• Documentation/SBV/Examples/Lists/BoundedMutex.hs +55/−67
• Documentation/SBV/Examples/Lists/Nested.hs +0/−45
• Documentation/SBV/Examples/Misc/Auxiliary.hs +1/−3
• Documentation/SBV/Examples/Misc/Definitions.hs +160/−37
• Documentation/SBV/Examples/Misc/Enumerate.hs +10/−17
• Documentation/SBV/Examples/Misc/FirstOrderLogic.hs +470/−0
• Documentation/SBV/Examples/Misc/Floating.hs +60/−60
• Documentation/SBV/Examples/Misc/LambdaArray.hs +70/−0
• Documentation/SBV/Examples/Misc/ModelExtract.hs +3/−3
• Documentation/SBV/Examples/Misc/NestedArray.hs +2/−2
• Documentation/SBV/Examples/Misc/Newtypes.hs +21/−16
• Documentation/SBV/Examples/Misc/Polynomials.hs +2/−2
• Documentation/SBV/Examples/Misc/ProgramPaths.hs +83/−0
• Documentation/SBV/Examples/Misc/SetAlgebra.hs +8/−22
• Documentation/SBV/Examples/Misc/SoftConstrain.hs +1/−1
• Documentation/SBV/Examples/Misc/Tuple.hs +5/−5
• Documentation/SBV/Examples/Optimization/Enumerate.hs +16/−13
• Documentation/SBV/Examples/Optimization/ExtField.hs +5/−2
• Documentation/SBV/Examples/Optimization/LinearOpt.hs +5/−2
• Documentation/SBV/Examples/Optimization/Production.hs +5/−2
• Documentation/SBV/Examples/Optimization/VM.hs +5/−2
• Documentation/SBV/Examples/ProofTools/AddHorn.hs +108/−0
• Documentation/SBV/Examples/ProofTools/BMC.hs +28/−28
• Documentation/SBV/Examples/ProofTools/Fibonacci.hs +12/−24
• Documentation/SBV/Examples/ProofTools/Strengthen.hs +17/−17
• Documentation/SBV/Examples/ProofTools/Sum.hs +11/−15
• Documentation/SBV/Examples/Puzzles/AOC_2021_24.hs +15/−6
• Documentation/SBV/Examples/Puzzles/Birthday.hs +49/−67
• Documentation/SBV/Examples/Puzzles/Coins.hs +9/−6
• Documentation/SBV/Examples/Puzzles/Counts.hs +4/−4
• Documentation/SBV/Examples/Puzzles/DieHard.hs +113/−0
• Documentation/SBV/Examples/Puzzles/Drinker.hs +6/−35
• Documentation/SBV/Examples/Puzzles/Euler185.hs +2/−2
• Documentation/SBV/Examples/Puzzles/Fish.hs +12/−12
• Documentation/SBV/Examples/Puzzles/Garden.hs +13/−33
• Documentation/SBV/Examples/Puzzles/HexPuzzle.hs +11/−13
• Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs +134/−0
• Documentation/SBV/Examples/Puzzles/MagicSquare.hs +2/−2
• Documentation/SBV/Examples/Puzzles/Murder.hs +19/−15
• Documentation/SBV/Examples/Puzzles/NQueens.hs +1/−1
• Documentation/SBV/Examples/Puzzles/Newspaper.hs +104/−0
• Documentation/SBV/Examples/Puzzles/Orangutans.hs +117/−0
• Documentation/SBV/Examples/Puzzles/Rabbits.hs +64/−0
• Documentation/SBV/Examples/Puzzles/SquareBirthday.hs +202/−0
• Documentation/SBV/Examples/Puzzles/Sudoku.hs +118/−181
• Documentation/SBV/Examples/Puzzles/Tower.hs +153/−0
• Documentation/SBV/Examples/Puzzles/U2Bridge.hs +31/−25
• Documentation/SBV/Examples/Queries/Abducts.hs +50/−0
• Documentation/SBV/Examples/Queries/AllSat.hs +2/−2
• Documentation/SBV/Examples/Queries/CaseSplit.hs +4/−4
• Documentation/SBV/Examples/Queries/Concurrency.hs +11/−11
• Documentation/SBV/Examples/Queries/Enums.hs +6/−6
• Documentation/SBV/Examples/Queries/FourFours.hs +28/−29
• Documentation/SBV/Examples/Queries/GuessNumber.hs +11/−12
• Documentation/SBV/Examples/Queries/Interpolants.hs +11/−8
• Documentation/SBV/Examples/Queries/UnsatCore.hs +2/−2
• Documentation/SBV/Examples/Strings/RegexCrossword.hs +11/−13
• Documentation/SBV/Examples/Strings/SQLInjection.hs +5/−5
• Documentation/SBV/Examples/TP/Ackermann.hs +279/−0
• Documentation/SBV/Examples/TP/Adder.hs +395/−0
• Documentation/SBV/Examples/TP/Basics.hs +427/−0
• Documentation/SBV/Examples/TP/BinarySearch.hs +269/−0
• Documentation/SBV/Examples/TP/CaseSplit.hs +48/−0
• Documentation/SBV/Examples/TP/Coins.hs +114/−0
• Documentation/SBV/Examples/TP/Collatz.hs +119/−0
• Documentation/SBV/Examples/TP/ConstFold.hs +1523/−0
• Documentation/SBV/Examples/TP/Countdown.hs +135/−0
• Documentation/SBV/Examples/TP/Fibonacci.hs +86/−0
• Documentation/SBV/Examples/TP/GCD.hs +1063/−0
• Documentation/SBV/Examples/TP/InsertionSort.hs +225/−0
• Documentation/SBV/Examples/TP/Kadane.hs +175/−0
• Documentation/SBV/Examples/TP/Kleene.hs +140/−0
• Documentation/SBV/Examples/TP/Lists.hs +2064/−0
• Documentation/SBV/Examples/TP/Majority.hs +157/−0
• Documentation/SBV/Examples/TP/McCarthy91.hs +94/−0
• Documentation/SBV/Examples/TP/MergeSort.hs +314/−0
• Documentation/SBV/Examples/TP/MutualCorecursion.hs +187/−0
• Documentation/SBV/Examples/TP/NatStream.hs +121/−0
• Documentation/SBV/Examples/TP/Numeric.hs +370/−0
• Documentation/SBV/Examples/TP/Peano.hs +926/−0
• Documentation/SBV/Examples/TP/PigeonHole.hs +53/−0
• Documentation/SBV/Examples/TP/PowerMod.hs +507/−0
• Documentation/SBV/Examples/TP/Primes.hs +522/−0
• Documentation/SBV/Examples/TP/Queue.hs +197/−0
• Documentation/SBV/Examples/TP/QuickSort.hs +698/−0
• Documentation/SBV/Examples/TP/RevAcc.hs +81/−0
• Documentation/SBV/Examples/TP/Reverse.hs +176/−0
• Documentation/SBV/Examples/TP/RunLength.hs +198/−0
• Documentation/SBV/Examples/TP/ShefferStroke.hs +689/−0
• Documentation/SBV/Examples/TP/SortHelpers.hs +195/−0
• Documentation/SBV/Examples/TP/Sqrt2IsIrrational.hs +111/−0
• Documentation/SBV/Examples/TP/StrongInduction.hs +336/−0
• Documentation/SBV/Examples/TP/SumReverse.hs +85/−0
• Documentation/SBV/Examples/TP/Tao.hs +58/−0
• Documentation/SBV/Examples/TP/TautologyChecker.hs +1124/−0
• Documentation/SBV/Examples/TP/UpDown.hs +114/−0
• Documentation/SBV/Examples/TP/VM.hs +448/−0
• Documentation/SBV/Examples/Transformers/SymbolicEval.hs +13/−16
• Documentation/SBV/Examples/Uninterpreted/AUF.hs +11/−20
• Documentation/SBV/Examples/Uninterpreted/Deduce.hs +10/−37
• Documentation/SBV/Examples/Uninterpreted/EUFLogic.hs +340/−0
• Documentation/SBV/Examples/Uninterpreted/Function.hs +4/−1
• Documentation/SBV/Examples/Uninterpreted/Multiply.hs +18/−19
• Documentation/SBV/Examples/Uninterpreted/Shannon.hs +1/−1
• Documentation/SBV/Examples/Uninterpreted/Sort.hs +8/−11
• Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs +27/−28
• Documentation/SBV/Examples/WeakestPreconditions/Append.hs +17/−28
• Documentation/SBV/Examples/WeakestPreconditions/Basics.hs +11/−9
• Documentation/SBV/Examples/WeakestPreconditions/Fib.hs +12/−17
• Documentation/SBV/Examples/WeakestPreconditions/GCD.hs +14/−31
• Documentation/SBV/Examples/WeakestPreconditions/IntDiv.hs +11/−11
• Documentation/SBV/Examples/WeakestPreconditions/IntSqrt.hs +11/−11
• Documentation/SBV/Examples/WeakestPreconditions/Length.hs +21/−34
• Documentation/SBV/Examples/WeakestPreconditions/Sum.hs +27/−26
• INSTALL +1/−1
• LICENSE +1/−1
• README.md +282/−4
• SBVBenchSuite/BenchSuite/Bench/Bench.hs +9/−9
• SBVBenchSuite/BenchSuite/BitPrecise/MultMask.hs +0/−31
• SBVBenchSuite/BenchSuite/CodeGeneration/Uninterpreted.hs +2/−0
• SBVBenchSuite/BenchSuite/Crypto/AES.hs +2/−0
• SBVBenchSuite/BenchSuite/Existentials/CRCPolynomial.hs +0/−23
• SBVBenchSuite/BenchSuite/Existentials/Diophantine.hs +1/−1
• SBVBenchSuite/BenchSuite/Lists/Nested.hs +0/−25
• SBVBenchSuite/BenchSuite/Misc/Enumerate.hs +6/−6
• SBVBenchSuite/BenchSuite/Misc/NoDiv0.hs +1/−1
• SBVBenchSuite/BenchSuite/Misc/SetAlgebra.hs +2/−0
• SBVBenchSuite/BenchSuite/Optimization/Instances.hs +1/−1
• SBVBenchSuite/BenchSuite/ProofTools/BMC.hs +1/−1
• SBVBenchSuite/BenchSuite/ProofTools/Fibonacci.hs +1/−1
• SBVBenchSuite/BenchSuite/ProofTools/Strengthen.hs +1/−1
• SBVBenchSuite/BenchSuite/ProofTools/Sum.hs +2/−2
• SBVBenchSuite/BenchSuite/Puzzles/Coins.hs +1/−1
• SBVBenchSuite/BenchSuite/Puzzles/Counts.hs +1/−2
• SBVBenchSuite/BenchSuite/Puzzles/Garden.hs +1/−1
• SBVBenchSuite/BenchSuite/Puzzles/MagicSquare.hs +1/−1
• SBVBenchSuite/BenchSuite/Puzzles/NQueens.hs +1/−1
• SBVBenchSuite/BenchSuite/Puzzles/Sudoku.hs +6/−8
• SBVBenchSuite/BenchSuite/Puzzles/U2Bridge.hs +1/−1
• SBVBenchSuite/BenchSuite/Queries/Enums.hs +1/−1
• SBVBenchSuite/BenchSuite/Queries/GuessNumber.hs +1/−1
• SBVBenchSuite/BenchSuite/Transformers/SymbolicEval.hs +1/−1
• SBVBenchSuite/BenchSuite/Uninterpreted/AUF.hs +2/−2
• SBVBenchSuite/BenchSuite/Uninterpreted/Deduce.hs +7/−4
• SBVBenchSuite/BenchSuite/Uninterpreted/Multiply.hs +2/−0
• SBVBenchSuite/BenchSuite/Uninterpreted/Shannon.hs +3/−1
• SBVBenchSuite/BenchSuite/Uninterpreted/Sort.hs +3/−3
• SBVBenchSuite/BenchSuite/WeakestPreconditions/Append.hs +2/−2
• SBVBenchSuite/BenchSuite/WeakestPreconditions/Basics.hs +1/−1
• SBVBenchSuite/BenchSuite/WeakestPreconditions/Fib.hs +1/−1
• SBVBenchSuite/BenchSuite/WeakestPreconditions/GCD.hs +1/−1
• SBVBenchSuite/BenchSuite/WeakestPreconditions/Instances.hs +1/−1
• SBVBenchSuite/BenchSuite/WeakestPreconditions/IntDiv.hs +1/−1
• SBVBenchSuite/BenchSuite/WeakestPreconditions/IntSqrt.hs +1/−1
• SBVBenchSuite/BenchSuite/WeakestPreconditions/Length.hs +1/−5
• SBVBenchSuite/BenchSuite/WeakestPreconditions/Sum.hs +1/−1
• SBVBenchSuite/SBVBench.hs +5/−7
• SBVBenchSuite/Utils/SBVBenchFramework.hs +15/−3
• SBVTestSuite/GoldFiles/adt00.gold +94/−0
• SBVTestSuite/GoldFiles/adt01.gold +102/−0
• SBVTestSuite/GoldFiles/adt02.gold +96/−0
• SBVTestSuite/GoldFiles/adt03.gold +95/−0
• SBVTestSuite/GoldFiles/adt04.gold +180/−0
• SBVTestSuite/GoldFiles/adt05.gold +130/−0
• SBVTestSuite/GoldFiles/adt06.gold +103/−0
• SBVTestSuite/GoldFiles/adt_chk01.gold +40/−0
• SBVTestSuite/GoldFiles/adt_expr00.gold +219/−0
• SBVTestSuite/GoldFiles/adt_expr00c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr01.gold +219/−0
• SBVTestSuite/GoldFiles/adt_expr01c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr02.gold +219/−0
• SBVTestSuite/GoldFiles/adt_expr02c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr03.gold +219/−0
• SBVTestSuite/GoldFiles/adt_expr03c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr04.gold +30/−0
• SBVTestSuite/GoldFiles/adt_expr05.gold +30/−0
• SBVTestSuite/GoldFiles/adt_expr06.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr06c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr07.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr07c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr08.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr08c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr09.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr09c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr10.gold +454/−0
• SBVTestSuite/GoldFiles/adt_expr10c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr11.gold +102/−0
• SBVTestSuite/GoldFiles/adt_expr11c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr12.gold +319/−0
• SBVTestSuite/GoldFiles/adt_expr12c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr13.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr13c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr14.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr14c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr15.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr15c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr16.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr16c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr17.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr17c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_expr18.gold +75/−0
• SBVTestSuite/GoldFiles/adt_expr18c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_gen00.gold +277/−0
• SBVTestSuite/GoldFiles/adt_gen01.gold +83/−0
• SBVTestSuite/GoldFiles/adt_gen02.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen03.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen04.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen05.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen06.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen07.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen08.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen09.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen10.gold +85/−0
• SBVTestSuite/GoldFiles/adt_gen11.gold +83/−0
• SBVTestSuite/GoldFiles/adt_gen12.gold +82/−0
• SBVTestSuite/GoldFiles/adt_lit00.gold +240/−0
• SBVTestSuite/GoldFiles/adt_lit00c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_lit01.gold +240/−0
• SBVTestSuite/GoldFiles/adt_lit01c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_lit02.gold +241/−0
• SBVTestSuite/GoldFiles/adt_lit02c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_lit03.gold +241/−0
• SBVTestSuite/GoldFiles/adt_lit03c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_lit04.gold +241/−0
• SBVTestSuite/GoldFiles/adt_lit04c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_lit05.gold +240/−0
• SBVTestSuite/GoldFiles/adt_lit05c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_mr00.gold +69/−0
• SBVTestSuite/GoldFiles/adt_mr01.gold +73/−0
• SBVTestSuite/GoldFiles/adt_mr02.gold +50/−0
• SBVTestSuite/GoldFiles/adt_mr03.gold +47/−0
• SBVTestSuite/GoldFiles/adt_mr04.gold +51/−0
• SBVTestSuite/GoldFiles/adt_nested00.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested00c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested01.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested01c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested02.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested02c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested03.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested03c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested04.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested04c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested05.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested05c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested06.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested06c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested07.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested07c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested08.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested08c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested09.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested09c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested10.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested10c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested11.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested11c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested12.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested12c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested13.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested13c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested14.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested14c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested15.gold +114/−0
• SBVTestSuite/GoldFiles/adt_nested15c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested16.gold +113/−0
• SBVTestSuite/GoldFiles/adt_nested16c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested17.gold +114/−0
• SBVTestSuite/GoldFiles/adt_nested17c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested18.gold +252/−0
• SBVTestSuite/GoldFiles/adt_nested19.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested19c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested20.gold +79/−0
• SBVTestSuite/GoldFiles/adt_nested20c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested21.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested21c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested22.gold +80/−0
• SBVTestSuite/GoldFiles/adt_nested22c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested23.gold +253/−0
• SBVTestSuite/GoldFiles/adt_nested24.gold +253/−0
• SBVTestSuite/GoldFiles/adt_nested25.gold +71/−0
• SBVTestSuite/GoldFiles/adt_nested25c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested26.gold +71/−0
• SBVTestSuite/GoldFiles/adt_nested26c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested27.gold +70/−0
• SBVTestSuite/GoldFiles/adt_nested27c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested28.gold +70/−0
• SBVTestSuite/GoldFiles/adt_nested28c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested29.gold +243/−0
• SBVTestSuite/GoldFiles/adt_nested30.gold +108/−0
• SBVTestSuite/GoldFiles/adt_nested30c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested31.gold +108/−0
• SBVTestSuite/GoldFiles/adt_nested31c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested32.gold +108/−0
• SBVTestSuite/GoldFiles/adt_nested32c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested33.gold +108/−0
• SBVTestSuite/GoldFiles/adt_nested33c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_nested34.gold +157/−0
• SBVTestSuite/GoldFiles/adt_pchk01.gold +40/−0
• SBVTestSuite/GoldFiles/adt_pexpr00.gold +219/−0
• SBVTestSuite/GoldFiles/adt_pexpr00c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr01.gold +219/−0
• SBVTestSuite/GoldFiles/adt_pexpr01c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr02.gold +219/−0
• SBVTestSuite/GoldFiles/adt_pexpr02c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr03.gold +219/−0
• SBVTestSuite/GoldFiles/adt_pexpr03c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr04.gold +30/−0
• SBVTestSuite/GoldFiles/adt_pexpr05.gold +30/−0
• SBVTestSuite/GoldFiles/adt_pexpr06.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr06c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr07.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr07c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr08.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr08c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr09.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr09c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr10.gold +454/−0
• SBVTestSuite/GoldFiles/adt_pexpr10c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr11.gold +102/−0
• SBVTestSuite/GoldFiles/adt_pexpr11c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr12.gold +319/−0
• SBVTestSuite/GoldFiles/adt_pexpr12c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr13.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr13c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr14.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr14c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr15.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr15c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr16.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr16c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr17.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr17c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr18.gold +75/−0
• SBVTestSuite/GoldFiles/adt_pexpr18c.gold +25/−0
• SBVTestSuite/GoldFiles/adt_pexpr19.gold +41/−0
• SBVTestSuite/GoldFiles/adt_pexpr20.gold +51/−0
• SBVTestSuite/GoldFiles/adt_pexpr21.gold +52/−0
• SBVTestSuite/GoldFiles/adt_pgen00.gold +277/−0
• SBVTestSuite/GoldFiles/adt_pgen01.gold +83/−0
• SBVTestSuite/GoldFiles/adt_pgen02.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen03.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen04.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen05.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen06.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen07.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen08.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen09.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen10.gold +85/−0
• SBVTestSuite/GoldFiles/adt_pgen11.gold +83/−0
• SBVTestSuite/GoldFiles/adt_pgen12.gold +82/−0
• SBVTestSuite/GoldFiles/aes128Lib.gold +1762/−203
• SBVTestSuite/GoldFiles/allSat1.gold +2/−2
• SBVTestSuite/GoldFiles/allSat2.gold +6/−6
• SBVTestSuite/GoldFiles/allSat6.gold +5/−5
• SBVTestSuite/GoldFiles/allSat7.gold +34434/−34440
• SBVTestSuite/GoldFiles/allSat8.gold +60/−0
• SBVTestSuite/GoldFiles/arbFp_opt_1.gold +3/−2
• SBVTestSuite/GoldFiles/arrayGetValTest1.gold +36/−0
• SBVTestSuite/GoldFiles/array_caching_01.gold +22/−37
• SBVTestSuite/GoldFiles/array_caching_02.gold +22/−37
• SBVTestSuite/GoldFiles/array_misc_1.gold +35/−0
• SBVTestSuite/GoldFiles/array_misc_11.gold +41/−0
• SBVTestSuite/GoldFiles/array_misc_12.gold +41/−0
• SBVTestSuite/GoldFiles/array_misc_13.gold +40/−0
• SBVTestSuite/GoldFiles/array_misc_14.gold +37/−0
• SBVTestSuite/GoldFiles/array_misc_15.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_16.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_17.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_18.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_19.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_2.gold +57/−0
• SBVTestSuite/GoldFiles/array_misc_20.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_21.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_22.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_23.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_24.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_25.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_26.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_27.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_28.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_29.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_3.gold +27/−0
• SBVTestSuite/GoldFiles/array_misc_30.gold +38/−0
• SBVTestSuite/GoldFiles/array_misc_31.gold +27/−0
• SBVTestSuite/GoldFiles/array_misc_5.gold +33/−0
• SBVTestSuite/GoldFiles/array_misc_7.gold +27/−0
• SBVTestSuite/GoldFiles/array_misc_9.gold +26/−0
• SBVTestSuite/GoldFiles/auf-1.gold +19/−23
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int16_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int32_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int64_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Int8_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word16_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word32_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word64_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word64_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word64_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word64_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word8_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word8_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word8_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Left_Word8_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int16_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int16_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int16_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int16_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int32_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int32_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int32_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int32_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int64_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int64_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int64_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int64_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int8_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int8_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int8_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Int8_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word16_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word16_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word16_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word16_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word32_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word32_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word32_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word32_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word64_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word64_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word64_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word64_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word8_Word16.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word8_Word32.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word8_Word64.gold +6/−12
• SBVTestSuite/GoldFiles/barrelRotate_Right_Word8_Word8.gold +6/−12
• SBVTestSuite/GoldFiles/basic-2_1.gold +1/−2
• SBVTestSuite/GoldFiles/basic-2_2.gold +1/−2
• SBVTestSuite/GoldFiles/basic-2_3.gold +1/−2
• SBVTestSuite/GoldFiles/basic-2_4.gold +1/−2
• SBVTestSuite/GoldFiles/basic-3_1.gold +1/−2
• SBVTestSuite/GoldFiles/basic-3_2.gold +1/−2
• SBVTestSuite/GoldFiles/basic-3_3.gold +1/−2
• SBVTestSuite/GoldFiles/basic-3_4.gold +1/−2
• SBVTestSuite/GoldFiles/basic-3_5.gold +1/−2
• SBVTestSuite/GoldFiles/basic-4_1.gold +1/−2
• SBVTestSuite/GoldFiles/basic-4_2.gold +1/−2
• SBVTestSuite/GoldFiles/basic-4_3.gold +1/−2
• SBVTestSuite/GoldFiles/basic-4_4.gold +1/−2
• SBVTestSuite/GoldFiles/basic-4_5.gold +1/−2
• SBVTestSuite/GoldFiles/basic-5_1.gold +1/−2
• SBVTestSuite/GoldFiles/basic-5_2.gold +1/−2
• SBVTestSuite/GoldFiles/basic-5_3.gold +1/−2
• SBVTestSuite/GoldFiles/basic-5_4.gold +1/−2
• SBVTestSuite/GoldFiles/basic-5_5.gold +1/−2
• SBVTestSuite/GoldFiles/ccitt.gold +2192/−2194
• SBVTestSuite/GoldFiles/charConstr00.gold +5/−11
• SBVTestSuite/GoldFiles/charConstr01.gold +7/−13
• SBVTestSuite/GoldFiles/charConstr02.gold +8/−13
• SBVTestSuite/GoldFiles/charConstr03.gold +17/−20
• SBVTestSuite/GoldFiles/charConstr04.gold +15/−18
• SBVTestSuite/GoldFiles/charConstr05.gold +16/−19
• SBVTestSuite/GoldFiles/charConstr06.gold +16/−19
• SBVTestSuite/GoldFiles/charConstr07.gold +20/−24
• SBVTestSuite/GoldFiles/charConstr08.gold +7/−13
• SBVTestSuite/GoldFiles/charConstr09.gold +5/−11
• SBVTestSuite/GoldFiles/charConstr10.gold +5/−11
• SBVTestSuite/GoldFiles/charConstr11.gold +9/−13
• SBVTestSuite/GoldFiles/check1.gold +39/−0
• SBVTestSuite/GoldFiles/check2.gold +29/−0
• SBVTestSuite/GoldFiles/coins.gold +7/−8
• SBVTestSuite/GoldFiles/concreteFoldl.gold +0/−29
• SBVTestSuite/GoldFiles/concreteFoldr.gold +0/−29
• SBVTestSuite/GoldFiles/concreteReverse.gold +0/−29
• SBVTestSuite/GoldFiles/concreteSort.gold +0/−29
• SBVTestSuite/GoldFiles/constArr2_SArray.gold +13/−36
• SBVTestSuite/GoldFiles/constArr_SArray.gold +13/−37
• SBVTestSuite/GoldFiles/counts.gold +1/−2
• SBVTestSuite/GoldFiles/crcPolyExist.gold +0/−14
• SBVTestSuite/GoldFiles/doctest_sanity.gold +3/−0
• SBVTestSuite/GoldFiles/dsat01.gold +5/−11
• SBVTestSuite/GoldFiles/exceptionLocal1.gold +10/−19
• SBVTestSuite/GoldFiles/exceptionLocal2.gold +3/−10
• SBVTestSuite/GoldFiles/exceptionRemote1.gold +1/−1
• SBVTestSuite/GoldFiles/foldlABC1.gold +0/−55
• SBVTestSuite/GoldFiles/foldlABC2.gold +0/−63
• SBVTestSuite/GoldFiles/foldlABC3.gold +0/−70
• SBVTestSuite/GoldFiles/foldrAB1.gold +0/−49
• SBVTestSuite/GoldFiles/foldrAB2.gold +0/−57
• SBVTestSuite/GoldFiles/foldrAB3.gold +0/−64
• SBVTestSuite/GoldFiles/freshVars.gold +63/−66
• SBVTestSuite/GoldFiles/genBenchMark1.gold +5/−11
• SBVTestSuite/GoldFiles/genBenchMark2.gold +5/−11
• SBVTestSuite/GoldFiles/iteTest1.gold +0/−12
• SBVTestSuite/GoldFiles/iteTest2.gold +0/−12
• SBVTestSuite/GoldFiles/iteTest3.gold +0/−12
• SBVTestSuite/GoldFiles/lambda01.gold +1/−0
• SBVTestSuite/GoldFiles/lambda02.gold +4/−0
• SBVTestSuite/GoldFiles/lambda03.gold +5/−0
• SBVTestSuite/GoldFiles/lambda04.gold +151/−0
• SBVTestSuite/GoldFiles/lambda05.gold +273/−0
• SBVTestSuite/GoldFiles/lambda06.gold +216/−0
• SBVTestSuite/GoldFiles/lambda07.gold +459/−0
• SBVTestSuite/GoldFiles/lambda08.gold +172/−0
• SBVTestSuite/GoldFiles/lambda09.gold +172/−0
• SBVTestSuite/GoldFiles/lambda10.gold +157/−0
• SBVTestSuite/GoldFiles/lambda11.gold +172/−0
• SBVTestSuite/GoldFiles/lambda12.gold +157/−0
• SBVTestSuite/GoldFiles/lambda13.gold +196/−0
• SBVTestSuite/GoldFiles/lambda14.gold +198/−0
• SBVTestSuite/GoldFiles/lambda15.gold +281/−0
• SBVTestSuite/GoldFiles/lambda16.gold +281/−0
• SBVTestSuite/GoldFiles/lambda17.gold +286/−0
• SBVTestSuite/GoldFiles/lambda18.gold +438/−0
• SBVTestSuite/GoldFiles/lambda19.gold +281/−0
• SBVTestSuite/GoldFiles/lambda20.gold +281/−0
• SBVTestSuite/GoldFiles/lambda21.gold +286/−0
• SBVTestSuite/GoldFiles/lambda22.gold +231/−0
• SBVTestSuite/GoldFiles/lambda23.gold +572/−0
• SBVTestSuite/GoldFiles/lambda24.gold +240/−0
• SBVTestSuite/GoldFiles/lambda25.gold +456/−0
• SBVTestSuite/GoldFiles/lambda26.gold +167/−0
• SBVTestSuite/GoldFiles/lambda27.gold +178/−0
• SBVTestSuite/GoldFiles/lambda28.gold +183/−0
• SBVTestSuite/GoldFiles/lambda29.gold +179/−0
• SBVTestSuite/GoldFiles/lambda30.gold +184/−0
• SBVTestSuite/GoldFiles/lambda31.gold +177/−0
• SBVTestSuite/GoldFiles/lambda32.gold +177/−0
• SBVTestSuite/GoldFiles/lambda33.gold +1/−0
• SBVTestSuite/GoldFiles/lambda34.gold +4/−0
• SBVTestSuite/GoldFiles/lambda35.gold +2/−0
• SBVTestSuite/GoldFiles/lambda36.gold +3/−0
• SBVTestSuite/GoldFiles/lambda37.gold +3/−0
• SBVTestSuite/GoldFiles/lambda38.gold +6/−0
• SBVTestSuite/GoldFiles/lambda40.gold +1/−0
• SBVTestSuite/GoldFiles/lambda41.gold +4/−0
• SBVTestSuite/GoldFiles/lambda42.gold +2/−0
• SBVTestSuite/GoldFiles/lambda43.gold +1/−0
• SBVTestSuite/GoldFiles/lambda44.gold +4/−0
• SBVTestSuite/GoldFiles/lambda45.gold +2/−0
• SBVTestSuite/GoldFiles/lambda46.gold +45/−0
• SBVTestSuite/GoldFiles/lambda47.gold +143/−0
• SBVTestSuite/GoldFiles/lambda47_c.gold +38/−0
• SBVTestSuite/GoldFiles/lambda48.gold +156/−0
• SBVTestSuite/GoldFiles/lambda48_c.gold +38/−0
• SBVTestSuite/GoldFiles/lambda49.gold +215/−0
• SBVTestSuite/GoldFiles/lambda49_c.gold +35/−0
• SBVTestSuite/GoldFiles/lambda50.gold +215/−0
• SBVTestSuite/GoldFiles/lambda50_c.gold +37/−0
• SBVTestSuite/GoldFiles/lambda51.gold +215/−0
• SBVTestSuite/GoldFiles/lambda51_c.gold +37/−0
• SBVTestSuite/GoldFiles/lambda52.gold +215/−0
• SBVTestSuite/GoldFiles/lambda52_c.gold +35/−0
• SBVTestSuite/GoldFiles/lambda53.gold +36/−0
• SBVTestSuite/GoldFiles/lambda54.gold +58/−0
• SBVTestSuite/GoldFiles/lambda55.gold +58/−0
• SBVTestSuite/GoldFiles/lambda56.gold +458/−0
• SBVTestSuite/GoldFiles/lambda57.gold +120/−0
• SBVTestSuite/GoldFiles/lambda57a.gold +928/−0
• SBVTestSuite/GoldFiles/lambda57b.gold +824/−0
• SBVTestSuite/GoldFiles/lambda57c.gold +225/−0
• SBVTestSuite/GoldFiles/lambda58.gold +5/−0
• SBVTestSuite/GoldFiles/lambda59.gold +6/−0
• SBVTestSuite/GoldFiles/lambda60.gold +31/−0
• SBVTestSuite/GoldFiles/lambda61.gold +29/−0
• SBVTestSuite/GoldFiles/lambda62.gold +35/−0
• SBVTestSuite/GoldFiles/lambda63.gold +37/−0
• SBVTestSuite/GoldFiles/lambda64.gold +39/−0
• SBVTestSuite/GoldFiles/lambda65.gold +41/−0
• SBVTestSuite/GoldFiles/lambda66.gold +44/−0
• SBVTestSuite/GoldFiles/lambda67.gold +44/−0
• SBVTestSuite/GoldFiles/lambda68.gold +43/−0
• SBVTestSuite/GoldFiles/lambda69.gold +44/−0
• SBVTestSuite/GoldFiles/lambda70.gold +63/−0
• SBVTestSuite/GoldFiles/lambda71.gold +13/−0
• SBVTestSuite/GoldFiles/lambda72.gold +7/−0
• SBVTestSuite/GoldFiles/lambda73.gold +6/−0
• SBVTestSuite/GoldFiles/lambda74.gold +15/−0
• SBVTestSuite/GoldFiles/lambda75.gold +15/−0
• SBVTestSuite/GoldFiles/lambda76.gold +3/−0
• SBVTestSuite/GoldFiles/lambda77.gold +3/−0
• SBVTestSuite/GoldFiles/lambda78.gold +3/−0
• SBVTestSuite/GoldFiles/lambda79.gold +10/−0
• SBVTestSuite/GoldFiles/lambda80.gold +13/−0
• SBVTestSuite/GoldFiles/lambda81.gold +279/−0
• SBVTestSuite/GoldFiles/lambda82.gold +201/−0
• SBVTestSuite/GoldFiles/lambda83.gold +32/−0
• SBVTestSuite/GoldFiles/lambda84.gold +32/−0
• SBVTestSuite/GoldFiles/lambda85.gold +219/−0
• SBVTestSuite/GoldFiles/lambda86.gold +219/−0
• SBVTestSuite/GoldFiles/lambda87.gold +453/−0
• SBVTestSuite/GoldFiles/lambda88.gold +89/−0
• SBVTestSuite/GoldFiles/legato.gold +73/−74
• SBVTestSuite/GoldFiles/legato_c.gold +65/−65
• SBVTestSuite/GoldFiles/listFloat1.gold +18/−0
• SBVTestSuite/GoldFiles/listFloat2.gold +168/−0
• SBVTestSuite/GoldFiles/listFloat3.gold +33/−0
• SBVTestSuite/GoldFiles/mapNoFailure.gold +0/−162
• SBVTestSuite/GoldFiles/mapWithFailure.gold +0/−190
• SBVTestSuite/GoldFiles/maxlWithFailure.gold +0/−168
• SBVTestSuite/GoldFiles/maxrWithFailure.gold +0/−177
• SBVTestSuite/GoldFiles/nested1.gold +8/−0
• SBVTestSuite/GoldFiles/nested2.gold +8/−0
• SBVTestSuite/GoldFiles/nested3.gold +30/−0
• SBVTestSuite/GoldFiles/nested4.gold +8/−0
• SBVTestSuite/GoldFiles/noOpt1.gold +7/−14
• SBVTestSuite/GoldFiles/noOpt2.gold +7/−14
• SBVTestSuite/GoldFiles/nonlinear_cvc4.gold +35/−0
• SBVTestSuite/GoldFiles/nonlinear_cvc5.gold +34/−0
• SBVTestSuite/GoldFiles/nonlinear_z3.gold +40/−0
• SBVTestSuite/GoldFiles/optBasicsRange_08_signed_max.gold +3/−2
• SBVTestSuite/GoldFiles/optBasicsRange_08_signed_min.gold +3/−2
• SBVTestSuite/GoldFiles/optBasicsRange_16_signed_max.gold +3/−2
• SBVTestSuite/GoldFiles/optBasicsRange_16_signed_min.gold +3/−2
• SBVTestSuite/GoldFiles/optBasicsRange_32_signed_max.gold +3/−2
• SBVTestSuite/GoldFiles/optBasicsRange_32_signed_min.gold +3/−2
• SBVTestSuite/GoldFiles/optBasicsRange_64_signed_max.gold +3/−2
• SBVTestSuite/GoldFiles/optBasicsRange_64_signed_min.gold +3/−2
• SBVTestSuite/GoldFiles/optFloat1a.gold +17/−3
• SBVTestSuite/GoldFiles/optFloat1b.gold +13/−2
• SBVTestSuite/GoldFiles/optFloat1c.gold +17/−3
• SBVTestSuite/GoldFiles/optFloat1d.gold +13/−2
• SBVTestSuite/GoldFiles/optFloat2a.gold +17/−3
• SBVTestSuite/GoldFiles/optFloat2b.gold +13/−2
• SBVTestSuite/GoldFiles/optFloat2c.gold +17/−3
• SBVTestSuite/GoldFiles/optFloat2d.gold +13/−2
• SBVTestSuite/GoldFiles/optFloat3.gold +33/−19
• SBVTestSuite/GoldFiles/optFloat4.gold +31/−17
• SBVTestSuite/GoldFiles/optQuant1.gold +5/−5
• SBVTestSuite/GoldFiles/optQuant5.gold +4/−5
• SBVTestSuite/GoldFiles/pareto1.gold +110/−110
• SBVTestSuite/GoldFiles/pareto2.gold +148/−148
• SBVTestSuite/GoldFiles/pbAtLeast.gold +5/−11
• SBVTestSuite/GoldFiles/pbAtMost.gold +5/−11
• SBVTestSuite/GoldFiles/pbEq.gold +5/−11
• SBVTestSuite/GoldFiles/pbEq2.gold +21/−28
• SBVTestSuite/GoldFiles/pbExactly.gold +5/−11
• SBVTestSuite/GoldFiles/pbGe.gold +5/−11
• SBVTestSuite/GoldFiles/pbLe.gold +5/−11
• SBVTestSuite/GoldFiles/pbMutexed.gold +5/−11
• SBVTestSuite/GoldFiles/pbStronglyMutexed.gold +5/−11
• SBVTestSuite/GoldFiles/qEnum1.gold +39/−22
• SBVTestSuite/GoldFiles/qOpt_1.gold +109/−0
• SBVTestSuite/GoldFiles/qOpt_2.gold +119/−0
• SBVTestSuite/GoldFiles/qUninterp1.gold +15/−16
• SBVTestSuite/GoldFiles/quantifiedB_0.gold +44/−0
• SBVTestSuite/GoldFiles/quantifiedB_1.gold +33/−0
• SBVTestSuite/GoldFiles/quantifiedB_2.gold +33/−0
• SBVTestSuite/GoldFiles/quantifiedB_3.gold +36/−0
• SBVTestSuite/GoldFiles/quantifiedB_4.gold +32/−0
• SBVTestSuite/GoldFiles/quantifiedB_5.gold +32/−0
• SBVTestSuite/GoldFiles/quantifiedB_6.gold +28/−0
• SBVTestSuite/GoldFiles/quantifiedB_7.gold +30/−0
• SBVTestSuite/GoldFiles/quantifiedB_8.gold +30/−0
• SBVTestSuite/GoldFiles/quantifiedB_9.gold +30/−0
• SBVTestSuite/GoldFiles/quantifiedB_A.gold +33/−0
• SBVTestSuite/GoldFiles/quantifiedB_B.gold +33/−0
• SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_existsexists_contradiction_p.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_prove_existsexists_satisfiable_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_existsexists_satisfiable_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_prove_existsexists_thm_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_existsexists_thm_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_existsforall_contradiction_p.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_existsforall_satisfiable_p.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_prove_existsforall_thm_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_existsforall_thm_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_forallexists_contradiction_p.gold +12/−21
• SBVTestSuite/GoldFiles/quantified_prove_forallexists_satisfiable_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_forallexists_satisfiable_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_prove_forallexists_thm_c.gold +0/−35
• SBVTestSuite/GoldFiles/quantified_prove_forallexists_thm_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_prove_forallforall_contradiction_c.gold +0/−36
• SBVTestSuite/GoldFiles/quantified_prove_forallforall_contradiction_p.gold +12/−22
• SBVTestSuite/GoldFiles/quantified_prove_forallforall_satisfiable_c.gold +0/−36
• SBVTestSuite/GoldFiles/quantified_prove_forallforall_satisfiable_p.gold +12/−22
• SBVTestSuite/GoldFiles/quantified_prove_forallforall_thm_c.gold +0/−36
• SBVTestSuite/GoldFiles/quantified_prove_forallforall_thm_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_existsexists_contradiction_c.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_existsexists_contradiction_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_existsexists_satisfiable_c.gold +12/−22
• SBVTestSuite/GoldFiles/quantified_sat_existsexists_satisfiable_p.gold +12/−22
• SBVTestSuite/GoldFiles/quantified_sat_existsexists_thm_c.gold +12/−22
• SBVTestSuite/GoldFiles/quantified_sat_existsexists_thm_p.gold +12/−22
• SBVTestSuite/GoldFiles/quantified_sat_existsforall_contradiction_c.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_existsforall_contradiction_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_existsforall_satisfiable_c.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_existsforall_satisfiable_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_c.gold +12/−21
• SBVTestSuite/GoldFiles/quantified_sat_existsforall_thm_p.gold +12/−21
• SBVTestSuite/GoldFiles/quantified_sat_forallexists_contradiction_c.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_forallexists_contradiction_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_c.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_sat_forallexists_satisfiable_p.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_c.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_sat_forallexists_thm_p.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_sat_forallforall_contradiction_c.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_forallforall_contradiction_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_forallforall_satisfiable_c.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_forallforall_satisfiable_p.gold +12/−18
• SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_c.gold +12/−19
• SBVTestSuite/GoldFiles/quantified_sat_forallforall_thm_p.gold +12/−19
• SBVTestSuite/GoldFiles/query1.gold +40/−29
• SBVTestSuite/GoldFiles/queryArrays1.gold +23/−30
• SBVTestSuite/GoldFiles/queryArrays10.gold +36/−0
• SBVTestSuite/GoldFiles/queryArrays11.gold +36/−0
• SBVTestSuite/GoldFiles/queryArrays12.gold +45/−0
• SBVTestSuite/GoldFiles/queryArrays13.gold +46/−0
• SBVTestSuite/GoldFiles/queryArrays14.gold +46/−0
• SBVTestSuite/GoldFiles/queryArrays15.gold +46/−0
• SBVTestSuite/GoldFiles/queryArrays16.gold +46/−0
• SBVTestSuite/GoldFiles/queryArrays17.gold +49/−0
• SBVTestSuite/GoldFiles/queryArrays2.gold +5/−11
• SBVTestSuite/GoldFiles/queryArrays3.gold +5/−11
• SBVTestSuite/GoldFiles/queryArrays4.gold +5/−11
• SBVTestSuite/GoldFiles/queryArrays5.gold +20/−30
• SBVTestSuite/GoldFiles/queryArrays6.gold +40/−55
• SBVTestSuite/GoldFiles/queryArrays7.gold +17/−25
• SBVTestSuite/GoldFiles/queryArrays8.gold +14/−25
• SBVTestSuite/GoldFiles/queryArrays9.gold +35/−0
• SBVTestSuite/GoldFiles/queryTables.gold +20/−24
• SBVTestSuite/GoldFiles/query_Chars1.gold +5/−11
• SBVTestSuite/GoldFiles/query_Interpolant1.gold +5/−11
• SBVTestSuite/GoldFiles/query_Interpolant2.gold +5/−11
• SBVTestSuite/GoldFiles/query_Interpolant3.gold +5/−11
• SBVTestSuite/GoldFiles/query_Interpolant4.gold +10/−13
• SBVTestSuite/GoldFiles/query_ListOfMaybe.gold +25/−33
• SBVTestSuite/GoldFiles/query_ListOfSum.gold +24/−33
• SBVTestSuite/GoldFiles/query_Lists1.gold +5/−11
• SBVTestSuite/GoldFiles/query_Maybe.gold +20/−22
• SBVTestSuite/GoldFiles/query_Strings1.gold +6/−12
• SBVTestSuite/GoldFiles/query_SumMaybeBoth.gold +22/−26
• SBVTestSuite/GoldFiles/query_Sums.gold +19/−22
• SBVTestSuite/GoldFiles/query_Tuples1.gold +5/−11
• SBVTestSuite/GoldFiles/query_Tuples2.gold +7/−13
• SBVTestSuite/GoldFiles/query_abc.gold +5/−11
• SBVTestSuite/GoldFiles/query_badOption.gold +2/−0
• SBVTestSuite/GoldFiles/query_bitwuzla.gold +6/−16
• SBVTestSuite/GoldFiles/query_boolector.gold +5/−11
• SBVTestSuite/GoldFiles/query_cvc4.gold +5/−11
• SBVTestSuite/GoldFiles/query_cvc5.gold +7/−13
• SBVTestSuite/GoldFiles/query_mathsat.gold +5/−11
• SBVTestSuite/GoldFiles/query_sumMergeEither1.gold +19/−24
• SBVTestSuite/GoldFiles/query_sumMergeEither2.gold +19/−24
• SBVTestSuite/GoldFiles/query_sumMergeMaybe1.gold +19/−24
• SBVTestSuite/GoldFiles/query_sumMergeMaybe2.gold +19/−24
• SBVTestSuite/GoldFiles/query_uiSat_test1.gold +7/−13
• SBVTestSuite/GoldFiles/query_uiSat_test2.gold +11/−14
• SBVTestSuite/GoldFiles/query_uisatex1.gold +92/−87
• SBVTestSuite/GoldFiles/query_uisatex2.gold +84/−85
• SBVTestSuite/GoldFiles/query_uisatex3.gold +37/−0
• SBVTestSuite/GoldFiles/query_yices.gold +5/−11
• SBVTestSuite/GoldFiles/query_z3.gold +5/−11
• SBVTestSuite/GoldFiles/recursive10_mutual.gold +212/−0
• SBVTestSuite/GoldFiles/recursive11_chain.gold +299/−0
• SBVTestSuite/GoldFiles/recursive12_badMutual.gold +526/−0
• SBVTestSuite/GoldFiles/recursive13_mutualMeasure.gold +212/−0
• SBVTestSuite/GoldFiles/recursive14_badMutualMeasure.gold +294/−0
• SBVTestSuite/GoldFiles/recursive15_mixedMutualMeasure.gold +212/−0
• SBVTestSuite/GoldFiles/recursive16_badMixedMutualMeasure.gold +1135/−0
• SBVTestSuite/GoldFiles/recursive17_chainMeasure.gold +299/−0
• SBVTestSuite/GoldFiles/recursive19_selfAndMutual.gold +297/−0
• SBVTestSuite/GoldFiles/recursive1_ack.gold +1003/−0
• SBVTestSuite/GoldFiles/recursive20_mutualTP.gold +221/−0
• SBVTestSuite/GoldFiles/recursive21_allSelfBadCross.gold +613/−0
• SBVTestSuite/GoldFiles/recursive22_allSelfGoodCross.gold +376/−0
• SBVTestSuite/GoldFiles/recursive23_mutualProductive.gold +74/−0
• SBVTestSuite/GoldFiles/recursive24_badMutualProductive.gold +15/−0
• SBVTestSuite/GoldFiles/recursive25_contractMutualRejected.gold +16/−0
• SBVTestSuite/GoldFiles/recursive26_selfAndMutualProductive.gold +83/−0
• SBVTestSuite/GoldFiles/recursive27_mutualProductive3.gold +93/−0
• SBVTestSuite/GoldFiles/recursive28_noTermCheck.gold +53/−0
• SBVTestSuite/GoldFiles/recursive2_enum.gold +158/−0
• SBVTestSuite/GoldFiles/recursive3_badMeasure.gold +94/−0
• SBVTestSuite/GoldFiles/recursive4_mcCarthy91.gold +175/−0
• SBVTestSuite/GoldFiles/recursive5_badContract.gold +159/−0
• SBVTestSuite/GoldFiles/recursive6_uselessContract.gold +153/−0
• SBVTestSuite/GoldFiles/recursive7_productive.gold +54/−0
• SBVTestSuite/GoldFiles/recursive8_badProductive.gold +12/−0
• SBVTestSuite/GoldFiles/recursive9_productive2.gold +56/−0
• SBVTestSuite/GoldFiles/reverse.gold +0/−128
• SBVTestSuite/GoldFiles/reverseAlt10.gold +0/−134
• SBVTestSuite/GoldFiles/safe1.gold +5/−11
• SBVTestSuite/GoldFiles/safe2.gold +5/−11
• SBVTestSuite/GoldFiles/seqConcat.gold +5/−11
• SBVTestSuite/GoldFiles/seqConcatBad.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples1.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples2.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples3.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples4.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples5.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples6.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples7.gold +5/−11
• SBVTestSuite/GoldFiles/seqExamples8.gold +5/−11
• SBVTestSuite/GoldFiles/seqIndexOf.gold +5/−11
• SBVTestSuite/GoldFiles/seqIndexOfBad.gold +5/−11
• SBVTestSuite/GoldFiles/set_compl1.gold +14/−20
• SBVTestSuite/GoldFiles/set_delete1.gold +12/−18
• SBVTestSuite/GoldFiles/set_diff1.gold +5/−11
• SBVTestSuite/GoldFiles/set_disj1.gold +8/−14
• SBVTestSuite/GoldFiles/set_empty1.gold +9/−15
• SBVTestSuite/GoldFiles/set_full1.gold +9/−15
• SBVTestSuite/GoldFiles/set_insert1.gold +12/−18
• SBVTestSuite/GoldFiles/set_intersect1.gold +5/−11
• SBVTestSuite/GoldFiles/set_member1.gold +8/−14
• SBVTestSuite/GoldFiles/set_notMember1.gold +8/−14
• SBVTestSuite/GoldFiles/set_psubset1.gold +24/−34
• SBVTestSuite/GoldFiles/set_subset1.gold +5/−11
• SBVTestSuite/GoldFiles/set_tupleSet.gold +5/−11
• SBVTestSuite/GoldFiles/set_uninterp1.gold +49/−60
• SBVTestSuite/GoldFiles/set_uninterp2.gold +15/−18
• SBVTestSuite/GoldFiles/set_union1.gold +5/−11
• SBVTestSuite/GoldFiles/smtFuncUniq_captureConflict.gold +9/−0
• SBVTestSuite/GoldFiles/smtFuncUniq_captureTagged.gold +43/−0
• SBVTestSuite/GoldFiles/smtFuncUniq_conflict.gold +9/−0
• SBVTestSuite/GoldFiles/smtFuncUniq_recursiveConflict.gold +9/−0
• SBVTestSuite/GoldFiles/smtFuncUniq_recursiveOk.gold +131/−0
• SBVTestSuite/GoldFiles/smtFuncUniq_sameOk.gold +40/−0
• SBVTestSuite/GoldFiles/sort.gold +0/−180
• SBVTestSuite/GoldFiles/strConcat.gold +5/−11
• SBVTestSuite/GoldFiles/strConcatBad.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples1.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples10.gold +6/−12
• SBVTestSuite/GoldFiles/strExamples11.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples12.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples13.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples2.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples3.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples4.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples5.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples6.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples7.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples8.gold +5/−11
• SBVTestSuite/GoldFiles/strExamples9.gold +6/−12
• SBVTestSuite/GoldFiles/strIndexOf.gold +5/−11
• SBVTestSuite/GoldFiles/strIndexOfBad.gold +5/−11
• SBVTestSuite/GoldFiles/sumBimapPlus.gold +29/−32
• SBVTestSuite/GoldFiles/sumEitherSat.gold +20/−23
• SBVTestSuite/GoldFiles/sumLiftEither.gold +17/−22
• SBVTestSuite/GoldFiles/sumLiftMaybe.gold +13/−16
• SBVTestSuite/GoldFiles/sumMaybe.gold +34/−39
• SBVTestSuite/GoldFiles/sumMaybeBoth.gold +23/−26
• SBVTestSuite/GoldFiles/sumMergeEither1.gold +20/−24
• SBVTestSuite/GoldFiles/sumMergeEither2.gold +20/−24
• SBVTestSuite/GoldFiles/sumMergeMaybe1.gold +20/−24
• SBVTestSuite/GoldFiles/sumMergeMaybe2.gold +20/−24
• SBVTestSuite/GoldFiles/tgen_c.gold +7/−7
• SBVTestSuite/GoldFiles/tgen_forte.gold +7/−7
• SBVTestSuite/GoldFiles/tgen_haskell.gold +7/−7
• SBVTestSuite/GoldFiles/tpCache_alias.gold +3/−0
• SBVTestSuite/GoldFiles/tpCache_barFail.gold +4/−0
• SBVTestSuite/GoldFiles/tpCache_calcCollapse.gold +4/−0
• SBVTestSuite/GoldFiles/tpCache_fooFail.gold +4/−0
• SBVTestSuite/GoldFiles/tpCache_hit.gold +2/−0
• SBVTestSuite/GoldFiles/tpCache_miss.gold +1/−0
• SBVTestSuite/GoldFiles/tpCache_nested.gold +3/−0
• SBVTestSuite/GoldFiles/tpCache_recallFail.gold +4/−0
• SBVTestSuite/GoldFiles/tpCache_statsHit.gold +4/−0
• SBVTestSuite/GoldFiles/tpCache_statsMiss.gold +3/−0
• SBVTestSuite/GoldFiles/tpCache_statsNested.gold +4/−0
• SBVTestSuite/GoldFiles/tuple_enum.gold +19/−22
• SBVTestSuite/GoldFiles/tuple_list.gold +5/−11
• SBVTestSuite/GoldFiles/tuple_nested.gold +5/−11
• SBVTestSuite/GoldFiles/tuple_swap.gold +5/−11
• SBVTestSuite/GoldFiles/tuple_twoTwo.gold +7/−13
• SBVTestSuite/GoldFiles/tuple_unequal.gold +5/−11
• SBVTestSuite/GoldFiles/uiSat_test1.gold +11/−16
• SBVTestSuite/GoldFiles/uiSat_test2.gold +88/−74
• SBVTestSuite/GoldFiles/uiSat_test3.gold +2354/−2285
• SBVTestSuite/GoldFiles/unint-axioms-empty.gold +47/−0
• SBVTestSuite/GoldFiles/unint-axioms-query.gold +32/−23
• SBVTestSuite/GoldFiles/unint-axioms.gold +48/−0
• SBVTestSuite/GoldFiles/unint-sort01.gold +37/−0
• SBVTestSuite/GoldFiles/uninterpreted-1a.gold +53/−0
• SBVTestSuite/GoldFiles/uninterpreted-3.gold +5/−11
• SBVTestSuite/GoldFiles/uninterpreted-3a.gold +8/−15
• SBVTestSuite/GoldFiles/uninterpreted-4.gold +10/−15
• SBVTestSuite/GoldFiles/uninterpreted-4a.gold +10/−15
• SBVTestSuite/GoldFiles/validate_0.gold +5/−11
• SBVTestSuite/GoldFiles/validate_1.gold +9/−15
• SBVTestSuite/GoldFiles/validate_2.gold +9/−15
• SBVTestSuite/GoldFiles/validate_3.gold +6/−11
• SBVTestSuite/GoldFiles/validate_4.gold +5/−12
• SBVTestSuite/GoldFiles/validate_5.gold +5/−11
• SBVTestSuite/GoldFiles/validate_6.gold +5/−11
• SBVTestSuite/GoldFiles/validate_7.gold +31/−30
• SBVTestSuite/SBVConnectionTest.hs +16/−8
• SBVTestSuite/SBVDocTest.hs +10/−2
• SBVTestSuite/SBVHLint.hs +4/−8
• SBVTestSuite/SBVTest.hs +34/−8
• SBVTestSuite/TestSuite/ADT/ADT.hs +131/−0
• SBVTestSuite/TestSuite/ADT/Expr.hs +419/−0
• SBVTestSuite/TestSuite/ADT/MutRec.hs +195/−0
• SBVTestSuite/TestSuite/ADT/PExpr.hs +230/−0
• SBVTestSuite/TestSuite/Arrays/Caching.hs +3/−1
• SBVTestSuite/TestSuite/Arrays/InitVals.hs +108/−40
• SBVTestSuite/TestSuite/Arrays/Memory.hs +5/−5
• SBVTestSuite/TestSuite/Arrays/Query.hs +82/−17
• SBVTestSuite/TestSuite/Basics/AllSat.hs +19/−9
• SBVTestSuite/TestSuite/Basics/ArithNoSolver.hs +71/−386
• SBVTestSuite/TestSuite/Basics/ArithNoSolver2.hs +536/−0
• SBVTestSuite/TestSuite/Basics/ArithSolver.hs +278/−101
• SBVTestSuite/TestSuite/Basics/BarrelRotate.hs +0/−1
• SBVTestSuite/TestSuite/Basics/BasicTests.hs +69/−13
• SBVTestSuite/TestSuite/Basics/BoundedList.hs +0/−199
• SBVTestSuite/TestSuite/Basics/EqSym.hs +45/−0
• SBVTestSuite/TestSuite/Basics/Exceptions.hs +1/−1
• SBVTestSuite/TestSuite/Basics/GenBenchmark.hs +5/−4
• SBVTestSuite/TestSuite/Basics/Index.hs +13/−13
• SBVTestSuite/TestSuite/Basics/IteTest.hs +6/−8
• SBVTestSuite/TestSuite/Basics/Lambda.hs +489/−0
• SBVTestSuite/TestSuite/Basics/List.hs +30/−6
• SBVTestSuite/TestSuite/Basics/ModelValidate.hs +11/−7
• SBVTestSuite/TestSuite/Basics/Nonlinear.hs +29/−0
• SBVTestSuite/TestSuite/Basics/ProofTests.hs +14/−14
• SBVTestSuite/TestSuite/Basics/PseudoBoolean.hs +2/−0
• SBVTestSuite/TestSuite/Basics/Quantifiers.hs +49/−15
• SBVTestSuite/TestSuite/Basics/Recursive.hs +415/−6
• SBVTestSuite/TestSuite/Basics/Set.hs +6/−10
• SBVTestSuite/TestSuite/Basics/SmtFunctionUnique.hs +84/−0
• SBVTestSuite/TestSuite/Basics/String.hs +11/−11
• SBVTestSuite/TestSuite/Basics/Sum.hs +7/−7
• SBVTestSuite/TestSuite/Basics/TPCaching.hs +178/−0
• SBVTestSuite/TestSuite/Basics/Tuple.hs +12/−16
• SBVTestSuite/TestSuite/Basics/UISat.hs +9/−11
• SBVTestSuite/TestSuite/BitPrecise/Legato.hs +1/−1
• SBVTestSuite/TestSuite/CRC/CCITT.hs +1/−1
• SBVTestSuite/TestSuite/CRC/CCITT_Unidir.hs +1/−1
• SBVTestSuite/TestSuite/CRC/GenPoly.hs +3/−6
• SBVTestSuite/TestSuite/CRC/USB5.hs +3/−3
• SBVTestSuite/TestSuite/CantTypeCheck/Misc.hs +72/−0
• SBVTestSuite/TestSuite/Char/Char.hs +4/−4
• SBVTestSuite/TestSuite/CodeGeneration/Floats.hs +1/−1
• SBVTestSuite/TestSuite/CompileTests/PCase.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/Expr.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase01.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase01.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase02.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase02.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase03.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase03.stderr +6/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase04.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase04.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase05.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase05.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase06.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase06.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase07.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase07.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase08.hs +22/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase08.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase09.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase09.stderr +17/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase10.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase10.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase11.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase11.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase12.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase12.stderr +30/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase13.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase13.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase14.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase14.stderr +30/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase15.hs +26/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase15.stderr +33/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase16.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase16.stderr +35/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase17.stderr +32/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase18.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase18.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase19.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase19.stderr +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase20.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase20.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase21.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase21.stderr +39/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase22.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase22.stderr +42/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase23.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase23.stderr +38/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase24.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase24.stderr +32/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase25.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase25.stderr +35/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase26.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase26.stderr +33/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase27.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase27.stderr +38/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase28.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase28.stderr +34/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase29.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase29.stderr +48/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase30.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase30.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase31.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase31.stderr +28/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase32.hs +23/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase32.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase33.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase33.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase34.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase34.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase35.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase35.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase36.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase36.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase37.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase37.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase38.stderr +32/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase39.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase39.stderr +28/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase40.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase40.stderr +36/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase41.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase41.stderr +13/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase42.hs +26/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase42.stderr +33/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase43.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase43.stderr +17/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase44.hs +26/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase44.stderr +48/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase45.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase45.stderr +35/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase46.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase46.stderr +42/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase47.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase47.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase48.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase48.stderr +28/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase49.hs +22/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase49.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase50.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase50.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase51.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase51.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase52.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase52.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase53.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase53.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase54.hs +26/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase54.stderr +31/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase55.hs +22/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase55.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase56.hs +23/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase56.stderr +62/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase57.hs +22/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase57.stderr +35/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase58.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase58.stderr +127/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase59.hs +25/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase59.stderr +35/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase60.hs +33/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase60.stderr +120/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase61.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase61.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase62.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase62.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase63.hs +22/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase63.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase64.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase64.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase65.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase65.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase66.hs +23/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase66.stderr +26/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase67.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase67.stderr +34/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase68.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase68.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase69.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase69.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase70.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase70.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase71.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase71.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase72.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase72.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase73.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase73.stderr +17/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase74.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase74.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase75.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase75.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase76.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase76.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase77.hs +30/−0
• SBVTestSuite/TestSuite/CompileTests/PCase/PCase77.stderr +24/−0
• SBVTestSuite/TestSuite/CompileTests/SCase.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/Expr.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase01.hs +11/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase01.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase02.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase02.stderr +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase03.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase03.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase04.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase04.stderr +6/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase05.hs +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase05.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase06.hs +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase06.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase07.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase07.stderr +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase08.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase08.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase09.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase09.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase10.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase10.stderr +28/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase100.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase100.stderr +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase101.stderr +31/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase102.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase102.stderr +10/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase103.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase103.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase104.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase104.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase105.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase105.stderr +34/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase106.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase106.stderr +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase107.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase107.stderr +31/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase11.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase11.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase12.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase12.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase13.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase13.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase14.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase14.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase15.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase15.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase16.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase16.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase17.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase17.stderr +24/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase18.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase18.stderr +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase19.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase19.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase20.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase20.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase21.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase21.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase22.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase22.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase23.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase23.stderr +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase24.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase24.stderr +26/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase25.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase25.stderr +30/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase26.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase26.stderr +1/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase27.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase27.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase28.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase28.stderr +25/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase29.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase29.stderr +22/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase30.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase30.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase31.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase32.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase33.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase33.stderr +34/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase34.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase34.stderr +32/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase35.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase35.stderr +32/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase36.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase36.stderr +27/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase37.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase37.stderr +29/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase38.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase38.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase39.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase39.stderr +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase40.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase40.stderr +29/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase41.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase41.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase42.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase42.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase43.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase43.stderr +24/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase44.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase44.stderr +29/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase45.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase45.stderr +25/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase46.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase46.stderr +32/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase47.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase47.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase48.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase48.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase49.hs +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase49.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase50.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase50.stderr +28/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase51.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase51.stderr +10/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase52.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase52.stderr +29/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase53.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase53.stderr +44/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase54.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase54.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase55.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase55.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase56.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase56.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase57.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase57.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase58.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase58.stderr +28/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase59.stderr +27/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase60.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase60.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase61.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase61.stderr +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase62.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase62.stderr +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase63.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase63.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase64.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase64.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase65.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase65.stderr +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase66.stderr +33/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase67.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase67.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase68.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase68.stderr +8/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase69.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase69.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase70.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase70.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase71.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase71.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase72.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase72.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase73.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase73.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase74.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase74.stderr +10/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase75.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase75.stderr +11/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase76.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase76.stderr +10/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase77.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase77.stderr +12/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase78.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase78.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase79.hs +15/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase79.stderr +10/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase80.hs +13/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase80.stderr +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase81.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase81.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase82.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase82.stderr +10/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase83.hs +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase83.stderr +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase84.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase84.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase85.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase85.stderr +9/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase86.hs +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase86.stderr +10/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase87.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase87.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase88.hs +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase88.stderr +14/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase89.stderr +43/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase90.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase90.stderr +16/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase91.hs +23/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase91.stderr +23/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase92.hs +22/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase92.stderr +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase93.hs +22/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase93.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase94.hs +20/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase94.stderr +18/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase95.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase95.stderr +21/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase96.hs +21/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase96.stderr +22/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase97.hs +23/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase97.stderr +17/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase98.hs +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase98.stderr +19/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase99.hs +24/−0
• SBVTestSuite/TestSuite/CompileTests/SCase/SCase99.stderr +26/−0
• SBVTestSuite/TestSuite/Crypto/AES.hs +1/−1
• SBVTestSuite/TestSuite/Existentials/CRCPolynomial.hs +0/−31
• SBVTestSuite/TestSuite/Optimization/AssertWithPenalty.hs +2/−2
• SBVTestSuite/TestSuite/Optimization/Basics.hs +25/−2
• SBVTestSuite/TestSuite/Optimization/Combined.hs +6/−6
• SBVTestSuite/TestSuite/Optimization/ExtensionField.hs +4/−4
• SBVTestSuite/TestSuite/Optimization/Floats.hs +5/−5
• SBVTestSuite/TestSuite/Optimization/NoOpt.hs +3/−5
• SBVTestSuite/TestSuite/Optimization/Quantified.hs +19/−25
• SBVTestSuite/TestSuite/Optimization/Reals.hs +1/−1
• SBVTestSuite/TestSuite/Optimization/Tuples.hs +1/−1
• SBVTestSuite/TestSuite/Overflows/Arithmetic.hs +124/−159
• SBVTestSuite/TestSuite/Overflows/Casts.hs +1/−1
• SBVTestSuite/TestSuite/Puzzles/Coins.hs +2/−2
• SBVTestSuite/TestSuite/Puzzles/Counts.hs +1/−2
• SBVTestSuite/TestSuite/Puzzles/MagicSquare.hs +1/−1
• SBVTestSuite/TestSuite/Puzzles/NQueens.hs +1/−1
• SBVTestSuite/TestSuite/Puzzles/Sudoku.hs +4/−5
• SBVTestSuite/TestSuite/Puzzles/Temperature.hs +1/−1
• SBVTestSuite/TestSuite/Puzzles/U2Bridge.hs +1/−1
• SBVTestSuite/TestSuite/Queries/ArrayGetVal.hs +37/−0
• SBVTestSuite/TestSuite/Queries/Enums.hs +3/−4
• SBVTestSuite/TestSuite/Queries/FreshVars.hs +9/−10
• SBVTestSuite/TestSuite/Queries/Interpolants.hs +1/−1
• SBVTestSuite/TestSuite/Queries/Lists.hs +2/−1
• SBVTestSuite/TestSuite/Queries/Sums.hs +18/−20
• SBVTestSuite/TestSuite/Queries/Tables.hs +9/−9
• SBVTestSuite/TestSuite/Queries/Tuples.hs +3/−3
• SBVTestSuite/TestSuite/Queries/UISatEx.hs +29/−7
• SBVTestSuite/TestSuite/Queries/Uninterpreted.hs +4/−5
• SBVTestSuite/TestSuite/QuickCheck/QC.hs +1/−1
• SBVTestSuite/TestSuite/Transformers/SymbolicEval.hs +1/−1
• SBVTestSuite/TestSuite/Uninterpreted/AUF.hs +2/−2
• SBVTestSuite/TestSuite/Uninterpreted/Axioms.hs +30/−27
• SBVTestSuite/TestSuite/Uninterpreted/EUFLogic.hs +48/−0
• SBVTestSuite/TestSuite/Uninterpreted/Function.hs +147/−0
• SBVTestSuite/TestSuite/Uninterpreted/Sort.hs +2/−6
• SBVTestSuite/TestSuite/Uninterpreted/Uninterpreted.hs +15/−6
• SBVTestSuite/Utils/SBVTestFramework.hs +151/−41
• sbv.cabal +299/−217

@@ -1,10 +1,933 @@ * Hackage: <http://hackage.haskell.org/package/sbv>-* GitHub:  <http://leventerkok.github.io/sbv/>+* GitHub:  <http://github.com/LeventErkok/sbv> -* Latest Hackage released version: 9.0, 2022-04-27+### Version 14.4, 2026-07-03 -### Version 9.0+  * Add `curry` and `uncurry` (for symbolic 2-tuples) and `curry3` and `uncurry3` (for+    symbolic 3-tuples) to `Data.SBV.Tuple`, mirroring `Prelude.curry`/`Prelude.uncurry`. +  * New example `Documentation.SBV.Examples.BitPrecise.Adders`, building ripple-carry and+    carry-lookahead adders out of logic gates and proving them correct (equal to bit-vector+    addition, equal to each other, and the carry-out equal to the overflow flag) fully+    automatically by bit-blasting.++  * New example `Documentation.SBV.Examples.TP.Adder`, the inductive companion to the above:+    it models the operands as arbitrary-length symbolic bit lists and proves, for all widths+    at once, that a ripple-carry adder computes the integer value of the bits, and that a+    parallel-prefix (carry-lookahead) tree computes the same carry as the ripple---resting on+    the associativity of the generate/propagate carry operator.++  * Use str.to_re (instead of str.to.re) in regular-expression construction, which is the standard+    naming in SMTLib2. Thanks to May Torrence for reporting the discrepancy.++### Version 14.3, 2026-06-19++  * Improve fpRoundToIntegralH to remove redundant internal check. Thanks to Ryan Scott for the report.++  * Add support for arctan/arcsin/arccos in CVC5. Thanks to Ryan Scott for pointing out support for it.++  * Improved backend-solver communication so that if a solver returns an error message SBV now makes+    sure it gets captured and displayed properly before the solver-process itself terminates.++  * Drop support for pi as an SReal: The whole premise of SReal is it represents algebraic-reals+    (i.e., those that are roots of polynomials) exactly. But pi is not representable as such, since+    it's transcendental. Older versions of SBV used an approximation, but that's confusing to say+    the least, and downright wrong. Note that you can still use pi at floating-point types, where+    precision loss is built into the semantics.++  * Fix the enumeration quasi-quoter for a zero step: `[sEnum| 1, 1 .. 5 |]` is now the+    (semantically infinite) list of 1's, instead of the empty list.++  * Soundness fix for termination measures: a real-valued measure is now rejected at compile+    time. The reals are not well-ordered (an infinite descending chain like 1, 1/2, 1/4, ...+    never reaches a minimum), so a non-negative, strictly-decreasing real measure does not+    imply termination. Use an integer-valued measure instead.++  * Termination measures may now be given over the bounded bit-vector types (`Word8`..`Word64`,+    `Int8`..`Int64`, `WordN n`, `IntN n`), in addition to the integer/float types supported before.++### Version 14.2, 2026-06-05++  * Fix float to integer conversions, which were ignoring the rounding mode previously. Thanks to+    Ryan Scott for the report.++  * Fix the implementation of properFraction for arbitrary-sized floats. Thanks to Ryan Scott+    for the report and the fix.++  * Fix a bug in pCase, where SBV was over-approximating the bound variables, causing the+    unused-variable warning checker to flag branches unnecessarily in generated code.++  * New TP example: Run-length encoding roundtrip (`Documentation.SBV.Examples.TP.RunLength`).+    Proves that `decode (encode xs) == xs` for a run-length encode/decode pair.++  * New TP example: Two-stack queue (`Documentation.SBV.Examples.TP.Queue`).+    Proves that a queue implemented with two lists (front/back) correctly implements+    FIFO semantics via an abstraction function.++  * New cabal flag `compile_examples` (default: True) controls whether the+    `Documentation.SBV.Examples.*` modules are built as part of the library.+    Disable with `-f-compile_examples` when using SBV as a dependency to skip+    compiling the example modules. Thanks to Robin Webbers for the contribution.++  * Add more floating-point operations to `Data.SBV.Dynamic`. Thanks to Ryan Scott for the patch.++### Version 14.1, 2026-05-04++  * [BACKWARDS COMPATIBILITY] Removed `tpRibbon`. The ribbon length for TP proof+    output is now auto-computed from the proof structure via a lightweight dry-run+    pass. Users no longer need to manually set it.++  * New TP combinators `whenDryRun` and `unlessDryRun` allow user code to guard+    actions (e.g., proof tree printing) that should only run during the real pass of a TP+    based proof.++  * TP `pCase` now supports nested `case` expressions as proof case-splits,+    mirroring how `sCase` treats nested `case` as symbolic cases.++  * Consolidated internal solver IPC timeouts into named constants.+    Set the environment variable `SBV_COMM_TIMEOUT_FACTOR` to scale them (e.g., `2` to double).++  * Better handling of logic-strings, accommodating solver differences. Thanks to Ryan Scott for the report.++  * Fixed a bug in fpRemH, which calculates the floating point reminder for concrete values. The result+    was rounded twice, which is against the specification. Thanks to Ryan Scott for the report and the fix.++  * Simplify how floating-point literals are printed. The older method worked for Z3/CVC5, but not for Bitwuzla.+    Thanks to Ryan Scott for the report and the fix.++  * Fix the definition of sRealToSIntegerTruncate to do proper truncation. Thanks to Ryan Scott for the+    report and the fix.++### Version 14.0, 2026-04-01++  * [BACKWARDS COMPATIBILITY] The most important change in this release is how SBV treats+    function definitions via `smtFunction` and its variants. In prior versions, these definitions were+    directly translated to SMT-lib, without checking that they actually terminate. Starting with+    this release, SBV now requires all functions to terminate (with an escape hatch where the user+    explicitly opts out), and it proves it for all functions involved in a proof. SBV guesses+    and verifies a termination measure, and in case it can't do so will tell the user to supply+    their own version. This major departure from the old style of ignoring termination is a step+    towards incorporating a better architecture for much improved (semi-)automated theorem proving+    in SBV. See below for more details.++  * [BACKWARDS COMPATIBILITY] Major improvements to the `sCase` and `pCase` quasi-quoters:+    - Type prefix is no longer required; the type is inferred automatically+      from the patterns. Old syntax: `[sCase|Expr e of ...]`. New syntax: `[sCase| e of ...]`.++    - Wildcard-only patterns are now supported. An unguarded wildcard generates the rhs directly,+      while guarded wildcards produce an `ite`-chain (for `sCase`) or proof obligations (for `pCase`).++    - Built-in types are now supported: `Maybe`, `Either`, `List`, and `Tuple2` through `Tuple8`.+      Nested patterns across built-in types are also supported (e.g., `Just (x:_)`, `Left (a, b)`).+      For single-constructor types, the generated code omits the redundant constructor tester guard.++    - Primitive types are now supported: `Bool`, `Integer`, `Char`, and `String`. Patterns can use+      `True`/`False`, integer literals, character literals, string literals, variable bindings,+      and wildcards.++       ```haskell+       [sCase| m of         [sCase| x of      [sCase| xs of                [sCase| c of+          Nothing -> 0         0 -> sTrue        []      -> 0                 'a' -> 1+          Just x  -> x + 1     _ -> sFalse       x : xs' -> x + f xs'         'b' -> 2+       |]                   |]                |]                               _   -> 0+                                                                           |]++       [sCase| x of                            [sCase| x of+          _ | x .> 0 -> x                         0         -> y+            | sTrue  -> -x                        _ | x .> y -> x+       |]                                           | sTrue  -> y+                                               |]+       ```++    - As-patterns (`x@pat`) are now supported in both top-level and nested positions.+      The as-name is bound to the scrutinee (top-level) or accessor (nested) via a+      let-binding, which is elided when the name is unused. This works with all pattern+      types: constructors, tuples, lists, wildcards, and in combination with nested `case`+      expressions.++       ```haskell+       [sCase| xs of+          a : tl@(_ : _) -> a + case tl of+                                   b : _ -> b+                                   []    -> 0+          _ : _           -> 0+          []              -> 0+       |]+       ```++    - Plain `case` expressions inside `[sCase|...|]` and `[pCase|...|]` are now automatically+      treated as symbolic case-splits. This works around GHC's quasi-quoter nesting limitation+      (`[sCase|` cannot contain `|]`), and makes nested symbolic case expressions natural:++       ```haskell+       [sCase| e of+          Zero      -> case m of+                         Nothing -> 0+                         Just v  -> v+          Num k     -> k+          Add a b   -> t a m + t b m+       |]+       ```++      All `case` expressions inside `sCase` and `pCase` become symbolic; use a `let` or helper+      function for regular Haskell case expressions.++  * Improved documentation for `lambdaArray`, explaining the model-theoretic distinction+    between the pure array theory (`select`/`store`/`const`) and the richer setting where+    arrays are identified with function spaces.++  * [BACKWARDS COMPATIBILITY] `recall` and `recallWith` no longer take a `String` argument.+    A recalled proof is now automatically cached and reused if the same proposition is+    encountered again. `tpNoCache` has been removed.++  * SBV now detects conflicting `smtFunction` definitions: if two calls use the same SMT+    name but have different bodies, an error is raised. Identical re-registrations (which+    happen naturally with recursive functions) remain allowed.++  * SBV now automatically checks termination of recursive functions defined via `smtFunction`.+    A measure (a non-negative expression that strictly decreases at each recursive call) is+    guessed automatically from argument types when possible. For functions that need an explicit+    measure, use `smtFunctionWithMeasure`:++    ```haskell+    ld = smtFunctionWithMeasure "ld" (\k n -> (n - k) `smax` 0, [])+       $ \k n -> ite (n `sMod` k .== 0) k (ld (k+1) n)+    ```++    When the measure requires inductive properties to verify, supply TP proof actions as helpers+    via `measureLemma`/`measureLemmaWith`:++    ```haskell+    normalize = smtFunctionWithMeasure "normalize"+                  ( \f -> tuple (ifComplexity f, ifDepth f)+                  , [measureLemma ifDepthNonNeg, measureLemma ifComplexityPos]+                  )+              $ \f -> ...+    ```++  * For nested recursive functions (like McCarthy's 91 function) where the termination argument+    depends on the function's return value at smaller inputs, use `smtFunctionWithContract`. This+    takes a measure and a contract (post-condition) that are verified simultaneously via well-founded+    induction:++    ```haskell+    mcCarthy91 = smtFunctionWithContract "mcCarthy91"+                   ( \n -> 0 `smax` (101 - n)+                   , \n r -> n .<= 100 .=> r .== 91+                   , []+                   )+               $ \n -> ite (n .> 100) (n - 10) (mcCarthy91 (mcCarthy91 (n + 11)))+    ```++  * Productive (corecursive) functions can now be defined via `smtProductiveFunction`. Unlike+    terminating functions, productive functions need not have a base case — they may produce+    infinite output, so long as every recursive call is guarded by a data constructor.++  * New function `smtFunctionNoTermination` for defining recursive SMT functions without any+    termination check. The function is emitted as `define-fun-rec` and the user takes+    responsibility for well-definedness. Use this for functions where termination is believed+    but cannot be proven. Any TP proof that depends on such a function will be marked as+    `[Modulo: <name> termination]` instead of `[Proven]` in its root of trust.++  * New example `Documentation.SBV.Examples.TP.Countdown`, proving properties of a+    list-building countdown function using induction.++  * New example `Documentation.SBV.Examples.TP.NatStream`, demonstrating `smtProductiveFunction`+    with the infinite stream `nats n = [n, n+1, n+2, ...]` and proofs about its head, length, and+    element access.++  * New example `Documentation.SBV.Examples.TP.MutualCorecursion`, demonstrating mutually+    corecursive productive functions. Two functions `ping` and `pong` take turns producing+    elements of a stream, and we prove elementwise equality and that the k-th element of+    `ping n` is `n + k`.++  * New example `Documentation.SBV.Examples.TP.Collatz`, using `smtFunctionNoTermination` to+    define the Collatz function (whose termination is a famous open problem) and proving that+    all powers of two reach 1.++### Version 13.6, 2026-03-02++  * The `sCase` quasi-quoter now supports nested constructor patterns. Sub-patterns+    in a constructor match can themselves be constructors, including nullary ones. For example:++    ```haskell+    normalize f = smtFunction "normalize" $ \f ->+      [sCase|Formula f of+        If (If p q r) left right -> normalize (sIf p (sIf q left right) (sIf r left right))+        If c          left right -> sIf c (normalize left) (normalize right)+        _                        -> f+      |]+    ```++    Nested patterns generate appropriate `isCstr`/`getCstr_i` guards and let-bindings+    automatically. Pattern guards (`, e1, e2`) may also be used alongside nested patterns.+    Additionally, `| True` is now accepted as a synonym for `| sTrue` in guards.++  * The `sCase` quasi-quoter now supports integer and string literal patterns in nested+    positions (and at the top level inside a constructor). For example:++    ```haskell+    p e = [sCase|Formula e of+             Val 0         -> 100          -- fires when the Val field equals 0+             Val 1         -> 200          -- fires when the Val field equals 1+             Add (Val 0) r -> eval r       -- nested literal: fires when left child is Val 0+             _             -> eval e+          |]+    ```++    A literal sub-pattern desugars to a symbolic equality guard (`getC_i e .== lit`),+    so the exhaustiveness checker correctly requires a fallback for any constructor+    that only appears with literal sub-patterns.++  * Add the `pCase` quasi-quoter for proof case-splits. Same syntax as `sCase`, but+    generates `cases [cond ==> proof, ...]` instead of `ite` chains. Wildcards are+    allowed as the last arm (with or without guards), generating a negated disjunction+    of all prior guards to do fall-thru proofs.++  * Add minimum and maximum to Data.SBV.List. If they receive empty list as argument,+    then the result is underspecified, i.e., can be any value of the element type.++  * Add mapConcat to Documentation.SBV.Examples.TP.Lists, which proves the theorem+    `map f . concat = concat . map (map f)`.++  * Add Documentation.SBV.Examples.TP.Kadane, proving the correctness of Kadane's algorithm+    for computing the maximum segment sum. The proof uses a generalized invariant lemma to relate+    the accumulator-based implementation to the specification. (This proof was completed with+    assistance from Claude, in particular the part where we had to come up with the invariant+    about the helper function.)++  * Add Documentation.SBV.Examples.TP.Coins, proving the classic coin change theorem: for any+    amount n >= 8, you can make exact change using only 3-cent and 5-cent coins. Inspired by+    an Imandra example at <https://github.com/imandra-ai/imandrax-examples/blob/main/src/coins.iml>.++  * Add Documentation.SBV.Examples.TP.Ackermann, proving the relationship between Ackermann's+    original function and R. Peter's version (1935). Inspired by an Imandra example at+    <https://github.com/imandra-ai/imandrax-examples/blob/main/src/ackermann.iml>. This proof+    was developed by Claude with minimal user prompting and guidance.++  * Add Documentation.SBV.Examples.TP.PigeonHole, proving the pigeonhole principle: If a list+    of numbers sum up to more than the length of the list, then some cell must have a value+    greater than one.++  * Add Documentation.SBV.Examples.TP.TautologyChecker, a verified tautology checker for+    propositional formulas using an unordered BDD-style SAT solver approach. The proof establishes+    both soundness (if the checker says a formula is a tautology, it evaluates to true under all+    bindings) and completeness (if the checker says a formula is not a tautology, falsify returns+    a counterexample binding). Inspired by an Imandra example at+    <https://github.com/imandra-ai/imandrax-examples/blob/main/src/tautology.iml>, originally+    based on Boyer-Moore '79. This proof was developed with Claude's assistance.++  * Add Documentation.SBV.Examples.TP.ConstFold, proving the correctness of a constant-folding+    optimizer for a simple expression language with variables, constants, arithmetic, and let-bindings.+    The optimizer performs bottom-up simplification including arithmetic identities (e.g., addition/+    multiplication by 0 or 1, constant propagation) and let-folding (inlining `Let x (Con v) b` via+    capture-avoiding substitution).++### Version 13.5, 2026-01-26++  * Replace internal SMT-lib program representation from plain String to Text. This+    should improve performance and memory behavior in certain cases. Since solver time+    dominates for most cases, this is not going to be noticeable by end-users, except+    for very large programs. In any case, it should at least improve memory usage.+    NB. Historical note: Most of these transformations were done by Claude code; the+    era of AI coding had its first contributions to SBV. I' duly impressed by Claude's+    ability to understand and manipulate Haskell. (I also tried Gemini, which was less+    successful, compared to Claude.) I, for one, welcome our new computer overlords.++  * Added Documentation.SBV.Examples.TP.UpDown.hs, demonstrating proof of a a couple of+    list-processing functions together with naturals using TP. The problem itself is inspired+    by a midterm exam question for an ACL2-class taught by J Moore at UT Austin back in 2011;+    a minor tribute to J's amazing legacy.++### Version 13.4, 2026-01-09++  * Remove Eq constraint on readArray, generalizing it to arbitrary types for array-reads.++  * Added 'freeArray', which creates an array with no constraints at all. (Compare to 'constArray'.)+    Note that this is useful for expression contexts. If you're in a symbolic context (i.e., in+    the Symbolic monad), you can just use 'free' or 'sArray' as usual.)++  * Add missing instance of SatModel for Arrays. Thanks to Robin Webbers for the patch.++  * Export ArrayModel, so it can be programmatically processed after a call.++  * Moved Data/SBV/TP/List.hs to Documentation/SBV/Examples/TP/Lists.hs, which aligns better with the+    haddock documentation.++  * Fixed closure-version implementations of list functions filter, partition, takeWhile, and dropWhile.+    Thanks to amigalemming on github for the bug report.++  * Query mode now works with optimization directives. In this case, we perform lexicographic+    optimization. (Let me know if you need other methods.) The advantage of this is that calls+    to getValue works in this mode, so it is easier to access optimized model values. In case+    the optimal value is in an extension field (i.e., involves epsilon or infinity values),+    then calls to  getValue  will throw an error and alert the user. In this latter case, you+    should resort back to using the regular optimize calls.++  * Added new puzzle example: Documentation.SBV.Examples.Puzzles.SquareBirthday++  * Add recallWith to Data.SBV.TP, which allows you to change the solver in a recalled proof.++### Version 13.3, 2025-12-05++  * Added 'constArray', which allows creation of constant valued symbolic arrays. The definition+    is semantically equivalent to 'lambdaArray . const', but we generate simpler SMTLib code+    for it. For the general case of initializing an array with arbitrary functions, continue+    using 'lambdaArray'. Thanks to Robin Webbers for the patch.++  * Improved the infinite-number-of-primes theorem statement slightly.++### Version 13.2, 2025-12-02++  * Improve support for SMTDefinable class, allowing support for on-the-fly generated functions.+    Thanks to Eddy Westbrook for the patch. This should have no impact on existing code or usage,+    just allowing new use cases. Let us know if it breaks anything.++  * SBV now supports uninterpreted functions of arbitrary arities. (Previously, we had support for upto+    12 args; Eddy's work above generalized this to arbitrary arity.)++  * Added Documentation.SBV.Examples.TP.Primes, which formalizes prime numbers and proves that there are+    an infinite number of primes.++### Version 13.1, 2025-10-31++  * Tweaks to make sure SBV compiles with GHC 9.8.4. No other changes on top of 13.0 below.++### Version 13.0, 2025-10-31++  * SBV now supports algebraic data-types. A new function 'mkSymbolic' is introduced, which take a list of types+    and turns them into types that you can symbolically process. Clearly, Haskell ADTs are extremely rich:+    Parameterized, self-referential, and mutually-recursive datatypes are supported. GADTs and more complicated+    forms of data-types (with higher-order fields, for instance) are not supported. What SBV covers should handle+    most use cases, please get in touch if you have a use case that is currently not supported.++  * Introduced a new quasiquoter, named sCase, which allows writing case-expressions over symbolic ADTs. It supports+    wildcards and guards. It does not support pattern guards, nor complex patterns. (Each pattern is either a+    variable or an underscore.) Symbolic-boolean guards allow for concise expressions. This construct makes+    symbolic programming with ADTs easier.++  * Added examples under Documentation.SBV.Examples.ADT, demonstrating the use of basic ADTs and a case study+    of modeling type-checking constraints.++  * Added Documentation.SBV.Examples.TP.Peano, modeling peano numbers using an ADT and demonstrating many proofs.++  * Added Documentation.SBV.Examples.TP.VM demonstrating the correctness of a simple interpreter over an expression+    language with respect to a version that compiles the expression and runs the instructions over a virtual machine.++  * [BACKWARDS COMPATIBILITY] The old functions 'mkSymbolicEnumeration' and 'mkUninterpretedSort' are now removed,+    since their functionality is subsumed by 'mkSymbolic'.++  * [BACKWARDS COMPATIBILITY] Strong-induction now takes extra proof objects that can be used to establish that+    the measure provided is non-negative. This is usually not needed, so simply pass []. However, in case of strong+    induction over ADTs in particular, it can come in handy to aid the solver in establishing the given measure+    is valid.++### Version 12.2, 2025-08-15++  * Fix floating-point constant-folding code, which inadvertently constant-folded for symbolic rounding modes.++  * Euclidian modulus/division does not restrict division by 0. Following SMTLib, we allow sEDiv and sEMod+    to underconstrain the value if the divisor is 0. The main motivation for this is to allow for direct translation+    to SMTLib for these operations where solvers perform much better. Fixed the code to avoid unintended constant+    folding for the euclidian case.++  * Add missing Num instance for SRational and beef up test suite. Thanks to Jan Grant for reporting.++  * [BACKWARDS COMPATIBILITY] Reworked OrdSymbolic and Numeric instances, making them more robust. While this should+    be mostly invisible to end-users, you might have to add an extra 'FlexibleInstances' pragma that wasn't needed+    before. Please get in touch if you see inadvertent effects due to uses of symbolic ordering.++  * TP: Add tpAsms, which explicitly prints the assumption-proving step for each proof transition. Default is False,+    as assumptions are typically simple to prove. But if you use complicated booleans, this step can come in handy+    in seeing where a proof gets stuck.++  * TP: Add 'recall': Which turns of printing for a TP computation. This allows for non-verbose output in proof-scripts+    when we reuse an old proof. Note that this is safe: We still run the proof mentioned so any failures in it will+    be caught; it's just that we do it quietly to reduce verbosity in the re-calling proof.++  * TP: Add '|->': This is similar to '|-', except it applies to a boolean-chain of reasoning where each step is+    equivalent to the conjunction of the previous and the next. This allows for concise expression of boolean+    reasoning steps. See gcdAdd in Documentation.SBV.Examples.TP.GCD for an example.++  * Added Documentation.SBV.Examples.TP.GCD, which proves correctness and several other properties of Euclidian+    GCD algorithm. We also prove subtraction based and the so-called binary-GCD algorithms correct.++### Version 12.1, 2025-07-11++  * Add missing instances for strong-equality, extending it to lists/Maybe etc. (Only impacts floats and structures+    that contain floats.)++  * Be more careful about applications of equality when floats are involved. Previously, we were using regular SMTLib+    equality for structures. (i.e., lists of values or any other container that have a float element stored somewhere.)+    Unfortunately the IEEE-754 semantics for equality does not correspond to SMTLib's notion of equality in these+    cases, causing semantic differences. Now we are more careful, and we also warn the user about performance+    implications and ask them to use custom-functions instead.++### Version 12.0, 2025-07-04++  * [BACKWARDS COMPATIBILITY] Renamed KnuckleDragger to TP, for theorem-proving. The original name was confusing, and+    the design has diverged from Phil's tool in significant ways and goals.++  * TP:+      - Keep track of proofs with a unique id.+      - Removed theorem variants; lemmas are almost exclusively used and the only difference was in printing.+      - Add method rootOfTrust which can be used to retrieve uses of sorry in a proof. The idea is that+        to get a proof clean, you need to resolve all the proofs returned by this call.+      - Renamed kdShowDepsHTML to showProofTreeHTML. (Along with showProofTree which renders in ASCII.)+      - Renamed the unicode symbol for hints from ⁇ to ∵, which is more mathematical.+      - TP utils:+          - Add tpQuiet : quiets TP proofs+          - Add tpRibbon: simplifies setting the ribbon size in a proof.+          - Add tpStats : makes TP proofs print detailed statistics+          - Add tpCache : makes TP proofs use caching. This option can save time in re-running proofs. It comes+                with the proof-obligation on the user that all the name/type pairs used in lemmas are unique. See+                Documentation.SBV.Examples.TP.Basics for an example demonstration.+        Note that all these utils will be in effect with the closest call to runTP/runTPWith. If you change the+        solver for a specific lemma, we'll only change the solver, not TP-options.+      - Generalize various TP list/sort proofs.+      - Added qc/qcWith helpers, which allow you to run quick-check on specific proof steps+      - Added disp as TP helper: It allows you to print the value of arbitrary expressions if a proof-step fails. Good for debugging.++   * New TP examples:+      - Documentation.SBV.Examples.TP.Fibonacci:  Proving tail-recursive fibonacci is equivalent to textbook definition+      - Documentation.SBV.Examples.TP.Majority:   Proof of Boyer-Moore's majority selection algorithm correct.+      - Documentation.SBV.Examples.TP.McCarthy91: Proof of correctness for McCarthy's 91 function.+      - Documentation.SBV.Examples.TP.PowerMod:   Proving arithmetic properties relating power operation and modular arithmetic.+      - Documentation.SBV.Examples.TP.ReverseAcc: Proving the accumulating reverse definition is correct.+      - Documentation.SBV.Examples.TP.Reverse:    Proving a definition of reverse that uses no auxiliary definitions is correct.+      - Documentation.SBV.Examples.TP.SumReverse: Proving summing a list and its reverse are equivalent.++  * [BACKWARDS COMPATIBILITY] Reworked enum instances for symbolic values. Removed old Enum class instances for symbolic values,+    as that API is not compatible with symbolic values, and only worked when the arguments used were literal constants. There is+    now a new class 'EnumSymbolic' which has the exact same methods as 'Enum', except their types are more symbolic friendly. (For+    instance, enumerations produce symbolic ists.) These definitions are now much more symbolic/proof friendly as well. In particular,+    there is now an sEnum quasiquoter that allows you to construct symbolic enumerations of the form [|sEnum|a, b .. c|] etc., akin to+    regular Haskell enumerations but working on symbolic values and constructing symbolic lists. If you had old code that relied+    on Enum instances over constant symbolic values, you might have to use the underlying type for the enum, and then lift to+    the symbolic level. Please get in touch if this causes issues.++  * [BACKWARDS COMPATIBILITY] Remove Data.SBV.Tools.NaturalInduction. The functionality provided by this tool is much better+    addressed by TP'sinduction methods. If you were using this functionality and have problems+    porting to TP, please get in touch!++  * Added functions 'takeWhile', 'dropWhile', 'sum', 'product', 'last', 'replicate', '\\', upFromTo, upFrom,+    downFromTo, and downFrom to Data.SBV.List; corresponding to the symbolic equivalents of usual list processing functions.++  * [BACKWARDS COMPATIBILITY] Removed Data.SBV.String, and unified list and string functions just as in Haskell. This was a+    long-time wart in SBV, where we distinguished strings and list of characters since SMTLib does not equate them. SBV now+    treats these uniformly, obviating the need for Data.SBV.String.++  * Improved smt-function definitions: You can now define polymorphic, recursive, and higher-order functions in SBV+    that will be translated to SMTLib functions, without expanding them. Polymorphic functions get monomorphised. Recursive+    functions are supported, including mutual recursion.++    NB. For higher-order functions, if the function passed (whether named or lambda defined) as the higher-order argument have+    free variables, you must create a closure. See the 'Closure' type. If they are already closed, then you can use them as is.++    See 'smtFunction' and 'smtHOFunction' for details.++### Version 11.7, 2025-05-16++  * KnuckleDragger: Add a proof of correctness for the quick-sort algorithm.++  * KnuckleDragger: Add methods 'getProofTree' and 'kdShowDepsHTML' to collect and render+    the proof as a dependency tree, unicode or as HTML. Useful for programming+    methods/tactics on top of knuckle-dragger provided facilities.++### Version 11.6, 2025-05-10++  * Make SBV compile cleanly with GHC 9.8.4. This is really as far back a GHC you should be using,+    unless you can't use anything newer.++  * KnuckleDragger:+      - Simplify and generalize inductive proofs. You can now do proofs with user-specified measure functions.+      - Tweak proof-traces to print user given hints (aids in debugging).+      - Add a proof of correctness for the binary-search algorithm.++### Version 11.5, 2025-04-25++  * Documentation updates++  * KnuckleDragger: Add support for case-splitting, trivial proofs, and other improvements.++  * KnuckleDragger: Add support for strong-induction principle over integers and lists.++### Version 11.4, 2025-03-12++  * Generalize the strong-induction principle to use lexicographic order for simultaneous+    induction over two lists.++  * Added a proof of correctness for the merge-sort algorithm using KnuckleDragger++  * More exports from Data.SBV.Internals to enable compilation of SBVPlugin.++### Version 11.3, 2025-03-10++  * Fix various haddock documentation links++  * KD: Clean-up proofs using the cases tactic++### Version 11.2, 2025-03-08++  * Renamed the all-sat partitioning function from 'partition' to 'allSatPartiton'++  * Added support for 'partition' and 'splitAt' to Data.SBV.List++  * KnuckleDragger:+      - Renamed ? to ?? (which aligns better), and added unicode equivalent of it, named ⁇+      - Added strong-induction as a proof-method, with examples for both numeric and list examples+      - Added a double-induction principle, allowing inductive proofs over two lists simultaneously+      - Added a case-splitting tactic for calculational style proofs+      - Added many other example KD proofs, for lists in particular+      - Added a proof of the (functional) insertion sort algorithm++### Version 11.1, 2025-02-21++  * Completely reworked KnuckleDragger interfaces and proof styles, adding calculational and induction+    based proof strategies. SBV can now prove many inductive theorems in this mode, where the user guides+    the SMT solver to find tricky proofs. See Documentation/SBV/Examples/KnuckleDragger directory for many+    examples demonstrating the new features.++  * Generalize support for polymorphic and higher-order functions. These are still experimental, as SMTLib's+    higher-order function support is nascent. (Version 3 of SMTLib will have proper support for such functions, which+    is not released yet.) Currently, SBV can handle polymorphic and higher-order usage of: 'reverse', 'any', 'all',+    'filter', 'map', 'foldl', 'foldr', 'zip', and 'zipWith'; all exported from the 'Data.SBV.List' module.+    These functions are supported polymorphically, and (except reverse and zip) all take a function as+    an argument. SBV firstifies these functions, and the resulting code is compatible with Z3 and CVC5.+    (Firstification might change in the future, as SMTLib gains support for more higher-order+    features itself.) Proof-support in backend solvers for higher-order functions is still quite weak,+    though KnuckleDragger makes things easier.++  * Generalize the signatures of the default project-embed implementations of the Queriable class.++  * [BACKWARDS COMPATIBILITY] Removed rarely used functions mapi, foldli, foldri from Data.SBV.List. These+    can now be defined by the user as we have proper support for fold and map using lambdas.++  * [BACKWARDS COMPATIBILITY] Removed "Data/SBV/Tools/BoundedFix.hs", and "Data/SBV/Tools/BoundedList.hs", which+    were relatively unused and are more or less obsolete with SBV's new support for sequences and recursive+    functions. If you were using these functions you could easily recreate them. Please get in touch if you+    need this old functionality.++  * [BACKWARDS COMPATIBILITY] Data.SBV no longer exports the class SatModel, which is more directed+    towards internal SBV purposes. If you need it, you can now import it from Data.SBV.Internals.++  * [BACKWARDS COMPATIBILITY] Added 'registerFunction' which comes in handy for telling SBV about functions+    that are used in query mode. This is typically not necessary as SBV will register them automatically, but+    there are certain scenarios where explicit control is needed. This function also generalizes the old+    'registerUISMTFunction', which was a special case of this function and is now removed.++  * [BACKWARDS COMPATIBILITY] The function 'registerSMTType' is renamed to 'registerType'.++  * Fix the time-out limit setting for CVC4/5. Thanks to Daniel Matichuk for reporting.++  * Fix a performance issue with nested-lambda/quantifiers. Thanks to Blake C. Rawlings for reporting and+    Jeff Young for analysis.++### Version 11.0, 2024-11-06++  * [BACKWARDS COMPATIBILITY] SBV now handles arrays in a much more uniform way, unifying+    their use with all the other symbolic types. This required some back-wards compatibility+    changes, mostly around replacing calls to newArray with sArray. I expect there to be+    no semantic changes, only syntactic ones. Please do get in touch if you have trouble+    porting your old code using arrays to the new API.++  * Turn on support for floats and uninterpreted sorts/functions in Bitwuzla.++  * Add Data.SBV.Tools.KnuckleDragger, inspired by and modeled after Philip Zucker's tool+    (https://github.com/philzook58/knuckledragger) by the same name.++  * Added several KnuckleDragger proof examples, see Documentation.SBV.Examples.KnuckleDragger modules.+    Amongst the proofs are the irrationality of square-root of 2, several list lemmas, and a few+    inductive proofs over naturals, amongst others.++  * Add sDivides, which takes a concrete integer and a (possibly symbolic), and returns sTrue+    if the first argument divides the second. It is essentially equivalent to @a `sMod` n .== 0`,+    but it translates to the built-in divisibility predicate in SMTLib, which (might) perform better.+    Note that the @n@ argument is concrete, and must be > 0.++  * Clarified SSet, SList, and SArray: keys/contents: In SMTLib, the semantics of these containers+    use object-equality. In Haskell, they use instances of the Eq class. Usually this is just fine,+    except when it isn't: Floats! Since NaN /= NaN, and +0 is distinguished from -0, what holds+    in Haskell doesn't in the SMTLib logic. So, we define the semantics of equality to follow+    the SMTLib semantics. If you are not using floats, then this doesn't matter. If you do, bear+    in mind that the values will be treated with object equality; which (honestly) is easier to understand.++  * SBV now prints the elements of uninterpreted sorts more simply for z3. Previously, we simply used the+    name z3 produced, which looked like @T!val!i@ for the uninterpreted type @T@, we know convert it to @T_i@.++  * Added Documentation/SBV/Examples/Puzzles/DieHard.hs, which solves the die-hard jug-water problem using+    a BMC style search.++  * [BACKWARDS COMPATIBILITY] Changed the signature of the functions bmc (and bmcWith), induct (and inductWith)+    functions, so they take the transition as a relation, instead of a function returning multiple values. This+    generalizes the use cases, and it is easy to translate from existing applications. Simply change your old+    'State -> [State]' function to 'State -> State -> SBool', which can be achieved by+    'newTrans s1 s2 = s2 `sElem` oldTrans s1', though you probably want to code this in a more readable way+    depending on the actual transition relation you want to model. Furthermore, the function bmc is now+    split into two bmcRefute and bmcCover, to indicate use cases more clearly.++  * [BACKWARDS COMPATIBILITY] Removed the Fresh class, which was used as a proxy for the Queriable class as+    an easier to instantiate version. The extra functionality unfortunately made writing custom Queriable+    instances harder, and it is usually not harder to write Queriable in the first place.+    If you were using the Fresh class, instead define Queriable, the definition should be fairly+    simple. Please contact if you have difficulty using the Queriable interface.++### Version 10.12, 2024-08-11++  * Fix a few custom-floating-point format conversion bugs. Thanks to Sirui Lu for the patch.++  * Add a few OVERLAPPABLE pragmas to generic Queriable instances to make them easily overridable by+    user programs. Thanks to Marco Zocca for reporting.++  * Add signedMulOverflow, which checks whether multiplication of two signed-bitvectors can overflow.+    SBV already had a method (bvMulO) that served this purpose, translating to the corresponding predicate+    in SMTLib. Unfortunately not all solvers support this predicate efficiently. In particular, as of Aug 2024,+    bitwuzla has a performant checker for this overflow, but z3 does not. In case you cannot use bitwuzla for+    some reason, you might want to use the new signedMulOverflow function for better performance.++### Version 10.11, 2024-07-26++  * Add Documentation.SBV.Examples.Puzzles.Tower module, solving the visible towers puzzle.++  * Fix several representation bugs related to arbitrary-precision floats. Thanks to Sirui+    Lu for the reports and patches.++  * Removed the generic Num a => Num (SBV a) instance. When used at a non-standard type, this+    created type-checking but invalid SBV programs. See https://github.com/LeventErkok/sbv/issues/706+    for details.++  * Add functions optLexicographic, optLexicographicWith, optPareto, optParetoWith, optIndependent, optIndependentWith+    which makes using optimization functions easier. These are simple wrappers over the existing optimization routines,+    simplifying their interface.++  * Change how optimization results are presented when the underlying metric space is different from the type+    being optimized. As noted in https://github.com/LeventErkok/sbv/issues/716, the format SBV used was confusing.+    We now be more explicit, and print the original value in its own right, along with the metric-space value.+    Thanks to Andrew Anderson for reporting.++### Version 10.10, 2024-05-11++  * Add EqSymbolic, OrdSymbolic and Mergeable instances for NonEmpty type++  * Better handling of spawned processes, avoiding zombies. Thanks to Sirui Lu for the patch.++### Version 10.9, 2024-04-05++  * Fix printing of floats to be more consistent, using lowercase letters++### Version 10.8, 2024-04-05++  * Increase the number of digits used in printing floats in decimal base, which leads to+    better output in most cases.++### Version 10.7, 2024-03-23++  * Fix SMTDefinable instances for functions of arity 8-12. Thanks to Nick Lewchenko for the patch.++### Version 10.6, 2024-03-16++  * Added Data.SBV.Tools.BVOptimize module, which implements a custom optimizer for unsigned bit-vector+    values. See 'minBV' and 'maxBV' methods. These algorithms use the incremental solver instead of+    the optimizer engines, and they can be more performant in certain cases. (For instance, z3's+    optimization engine isn't incremental, which makes it perform poorly on certain BV-optimization+    problems.) These algorithms scan the bits from most to least significant bit, and individually+    set/unset them in an incremental fashion to optimize quickly.++  * SBV web-page is no longer maintained. The info is put into the README.md instead.++### Version 10.5, 2024-02-20++  * Export svFloatingPointAsSWord through Data.SBV.Internals++  * crackNum: if verbose, alert the user if surface value of a NaN doesn't match its calculated value+    due to the redundancy in NaN representations.++### Version 10.4, 2024-02-15++  * Before issuing a get-value, make sure there are no outstanding assert calls.+    See: https://github.com/LeventErkok/sbv/issues/682 for details.++  * crackNum mode now displays the surface form of NaNs more faithfully, if provided+    with the input string. This functionality is used by the crackNum executable.++### Version 10.3, 2024-01-05++  * Clean-up GHC extensions required in the cabal file, and changes required to compile cleanly with GHC 9.8 series.++  * Added 'partition', which allows for partitioning all-sat search spaces when models are generated.++  * Added 'sSetBitTo', variant of 'setBitTo', but allows symbolic indexes.++  * Added 'uninterpretWithArgs', which allows for user given argument names for uninterpreted functions. These+    names come in handy when displaying models of uninterpreted functions.++  * Added `Documentation.SBV.Examples.Misc.ProgramPaths`, showing an example use of all-sat partitioning.++  * Added `Documentation.SBV.Examples.BitPrecise.PEXT_PDEP`, modeling x86 instructions PDEP and PEXT.++  * Added `Documentation.SBV.Examples.Puzzles.Newspaper`, another puzzle example.++  * Added `Documentation.SBV.Examples.ProofTools.AddHorn`, demonstrating the use of the horn-clause solver for+    invariant generation.++  * Add 'sbv2smt', which renders the given sbv definition as an SMTLib definition. Mainly useful for debugging purposes.+    It can render both ground definitions and functions, and the latter can be handy in producing SMTLib functions to+    be used in other settings.++  * Add support for OpenSMT from Università della Svizzera italiana https://verify.inf.usi.ch/opensmt++  * Fix a bug in bit-vector rotation that manifested itself in small-bv sizes. Thanks to Sirui Lu for reporting.++  * [BACKWARDS COMPATIBILITY] Change the overflow detection API to match the new SMTLib predicates. These predicates+    do not distinguish between over/underflow, so strictly speaking the new API is less powerful than the old one. However,+    we choose to follow SMTLib here for portability purposes. If you need separate overflow/underflow checking you can+    use the encodings from earlier implementations, please get in touch if this proves problematic.++  * [BACKWARDS COMPATIBILITY] Dropped hasSize, which checked cardinality of sets. This call hasn't been supported by+    z3 for some time, and its uses were thus limited, and behavior was problematic even when supported due to finiteness+    issues.++  * Removed a few examples, which were causing regression failures with changes in z3. These are trickier examples, and+    new releases of z3 had varying performance issues, making them not suitable regression and documentation purposes. In+    particular, 'Documentation.SBV.Examples.Existentials.CRCPolynomial', 'Documentation.SBV.Examples.Lists.Nested', and+    'Documentation.SBV.Examples.BitPrecise.MultMask' were removed.++  * SBV now keeps track of contexts, thus avoiding rare (but unsound) cases of incorrect API usage where contexts+    are mixed. We now issue a run-time error. See https://github.com/LeventErkok/sbv/issues/71 for details.++  * Improve the getFunction signature, to return more detailed info on the produced SMT functions, including the parse-tree.++  * SBV now tracks whether a declared uninterpreted function is curried or not. This helps in more precise printing of+    satisfying models with uninterpreted functions. (Previously all UI functions were displayed as if they were curried.)++### Version 10.2, 2023-06-09++  * Improve HLint pragmas. Thanks to George Thomas for the patch.++  * Added an implementation of the Prince encryption algorithm. See Documentation/SBV/Examples/Crypto/Prince.hs.++  * Added on-the-fly decryption mode for AES. See Documentation/SBV/Examples/Crypto/AES.hs for details.++  * Added functions `sEDivMod`, `sEDiv`, and `sEMod` which perform euclidian division over symbolic integers.++  * Added 'Data.SBV.Tools.NaturalInduction' which provides a proof method to perform induction over natural numbers. See the functions 'inductNat' and 'inductNatWith'.++### Version 10.1, 2023-04-14++  * [BACKWARDS COMPATIBILITY] SBV now handles quantifiers in a much more disciplined way. All of the previous+    ways of creating quantified variables (i.e., the functions sbvForall, sbvExists, universal, existential) are+    removed. Instead, we can now express quantifiers in a much straightforward way, by passing them to+    'constrain' directly. A simple example is:++        constrain $ \(Forall x) (Exists y) -> y .> (x :: SInteger)++    You can nest quantifiers as you wish, and the quantified parameters can be of arbitrary symbolic type.+    Additionally, you can convert such a quantified formula to a regular boolean, via a call to 'quantifiedBool'+    function, essentially performing quantifier elimination:++        other_condition .&& quantifiedBool (\(Forall x) (Exists y) -> y .> (x :: SInteger))++    Or you can prove/sat quantified formulas directly:++        prove $ \(Forall x) (Exists y) -> y .> (x :: SInteger)++    This facility makes quantifiers part of the regular SBV language, allowing them to be mixed/matched with all+    your other symbolic computations.++    SBV also supports the constructors ExistsUnique to create unique existentials, in addition to+    ForallN and ExistsN for creating multiple variables at the same time.++    The new function skolemize can be used to skolemize quantified formulas: The skolemized version of a+    formula has no existential (replaced by uninterpreted functions), and is equisatisfiable to the original.++    See the following files demonstrating reasoning with quantifiers:++       * Documentation/SBV/Examples/Puzzles/Birthday.hs+       * Documentation/SBV/Examples/Puzzles/KnightsAndKnaves.hs+       * Documentation/SBV/Examples/Puzzles/Rabbits.hs+       * Documentation/SBV/Examples/Misc/FirstOrderLogic.hs++  * You can now define new functions in the generated SMTLib output, via an smtFunction call. Typically, we simply+    unroll all definitions, but there are certain cases where we would like the functions+    remain intact in the output. This is especially true of recursive functions, where the termination would+    depend on a symbolic variable, which cannot be symbolically-simulated. By translating these to SMTLib+    functions, we can now handle such definitions. Note that such definitions will no longer be constant-folded+    on the Haskell side, and each call will induce a call in the solver instead. The new method smtFunction+    can handle both recursive and non-recursive functions. See "Documentation/SBV/Examples/Misc/Definitions.hs"+    for examples.++  * Added new SList functions: map, mapi, foldl, foldr, foldli, foldri, zip, zipWith, filter, all, any.+    Note that these work on arbitrary--but finite--length lists, with all terminating elements, per+    usual SBV interpretation. These functions map to the underlying solver's fold and map functions,+    via lambda-abstractions. Note that the SMT engines remain incomplete with respect to sequence+    theories. (That is, any property that requires induction for its proof will cause unknown+    answers, or will not terminate.) However, basic properties, especially when the solver can determine the+    shape of the sequence arguments (i.e., number of elements), should go through.++  * New function 'lambdaAsArray' allows creation of array values out of lambda-expressions. See+    "Documentation/SBV/Examples/Misc/LambdaArray.hs" for an example use. This adds expressive power,+    as we can now specify arrays with index dependent contents much more easily.++  * Added support for abduct-generation, as supported by CVC5. See "Documentation/SBV/Examples/Queries/Abducts.hs"+    for a basic example.++  * Added support for special-relations. You can now check if a relation is partial, linear, tree,+    or piecewise-linear orders in SBV. (Or you can constrain relations to satisfy the corresponding laws, thus+    creating relations with these properties.) Additionally, you can create transitive-closures of relations.+    See Documentation/SBV/Examples/Misc/FirstOrderLogic.hs for several examples.++  * [BACKWARDS COMPATIBILITY] The signature of Data.SBV.List's concat has changed. In previous releases+    this was a synonym for appending two lists, now it takes a list-of-lists and flattens it, matching the+    Haskell list function with the same name.++  * [BACKWARDS COMPATIBILITY] The function addAxiom is removed. Instead use quantified-constraints, as described+    above.++  * [BACKWARDS COMPATIBILITY] Renamed the Uninterpreted class to SMTDefinable, since its task has changed, handling+    both kinds of definitions. Unless you were referring to the name Uninterpreted in your code, this should not+    impact you. Otherwise, simply rename it to SMTDefinable.++  * [BACKWARDS COMPATIBILITY] The configuration variable 'allowQuantifiedQueries' is removed. It is no+    longer relevant with our new quantification strategy described above.++  * [BACKWARDS COMPATIBILITY] The function 'isVacuous' is renamed to 'isVacuousProof' (and 'isVacuousWith'+    became 'isVacuousProofWith') to better reflect this function applies to checking vacuity in a proof context.++  * [BACKWARDS COMPATIBILITY] Satisfiability and proof checks are now put in different classes, instead of sharing+    the same class. This should not have any impact on user-level code, unless you were building libraries+    on top of SBV. See the 'ProvableM' and 'SatisfiableM' classes.++  * [BACKWARDS COMPATIBILITY] Renamed 'Goal' to 'ConstraintSet' which is more indicative of its purpose. A set+    of constraints can be satisfied, but proving them does not make sense. The name goal, however, suggested+    something we can prove.++  * [BACKWARDS COMPATIBILITY] SBV is now more lenient in returning function-interpretations, returning the SMTLib+    string in complicated cases in case of bailing out. Note that we still don't support complicated function+    values in allSat calls, as there's no way to reject existing interpretations. Consequently, the+    parameter 'satTrackUFs' is renamed to 'allSatTrackUFs' to better capture its new role.++  * Addressed an issue on Windows where solver synchronization fails due to unmapped diagnostic-challenge.+    (See issue #644 for details.) Thanks to Ryan Scott for reporting and helping with debugging.++  * Add missing Arbitrary instances for WordN and IntN types, enabling quickcheck on these types.++  * Rewrote some of the older examples to use more modern SBV idioms.++  * Changes needed to compile with upcoming GHC 9.6. Thanks to Lars Kuhtz and Ryan Scott for several patches.++### Version 9.2, 2023-1-16++  * Handle uninterpreted sorts better, avoiding kind-registration issue.+    See #634 for details. Thanks to Nick Lewchenko for the report.++### Version 9.1, 2023-01-09++  * CVC5: Add support for algebraic reals in CVC5 models++  * Export more solvers from Trans/Dynamic interfaces. Thanks to Ryan Scott for the patch.++### Version 9.0, 2022-04-27+   * Changes required to compile cleanly with GHC 9.2 series.    * In future versions, GHC will make `forall` a reserved word, which will create a conflict with SBV's use of the same.@@ -44,7 +967,7 @@    * Added concrete type instances of Mergeable class.     * Fixed a bug in the implementation of the concrete-path for sPopCount-   +    * Added complement, power, and difference operators for regular expressions. Also added `everything`, `nothing`,      `anyChar` as new recognizers. @@ -60,7 +983,7 @@   * SBV now supports cvc5; the latest incarnation of CVC. See https://github.com/cvc5/cvc5     for details. -  * SBV now supports bitwuzla; the latest incarnation of Boolector. See https://github.com/bitwuzla/bitwuzla+  * SBV now supports bitwuzla; the latest incarnation of Boolector. See https://bitwuzla.github.io     for details.    * Fixed handling of CRational values in constant folding, which was missing a case.@@ -118,7 +1041,7 @@     significand. This format is affectionately called "brain-float"     because it's often used in modeling neural networks machine-learning     applications, offering a wider-range than IEEE's half-float, at the-    exponse of reduced precision. It has 8-exponent bits and 8-significand+    expense of reduced precision. It has 8-exponent bits and 8-significand     bits, including the hidden bit.    * Add support for SRational type, rational values built out of the ratio@@ -132,7 +1055,7 @@     use cases. (Essentially, when there are no uninterpreted values or sorts present.)     The new algorithm has been measured to be at least an order of magnitude     faster or more in common cases as it splits the search space into disjoint-    models, reducing the burden of accummulated lemmas over multiple calls. (See+    models, reducing the burden of accumulated lemmas over multiple calls. (See     http://theory.stanford.edu/%7Enikolaj/programmingz3.html#sec-blocking-evaluations     for details.) @@ -180,7 +1103,7 @@   * SBV now tracks constants more closely in query mode, providing more support     for constant arrays in a seamless way. (See #574 for details.) -  * Pop-calls are now support for Yices and Boolector. (#577)+  * Pop-calls are now supported for Yices and Boolector. (#577)    * Changes required to make SBV work with latest version of z3 regarding     String and Characters, which now allow for unicode characters. This required@@ -195,7 +1118,7 @@   * Use SMTLib's int2bv if supported by the backend solver. If not, we still     do a manual translation. (CVC4 and z3 support it natively, Yices and     MathSAT does not, for which we do the manual translation. ABC and dReal-    doesn't support the coversion at all, since former doesn't support integers+    doesn't support the conversion at all, since former doesn't support integers     and the latter doesn't support bit-vectors.) Thanks to Martin Lundfall     for the initial pull request. @@ -234,11 +1157,11 @@   * Add "extraArgs" parameter to SMTConfig to simplify passing extra command line     arguments to the solver. -  * Add a method +  * Add a method          sListArray :: (HasKind a, SymVal b) => b -> [(SBV a, SBV b)] -> array a b -    to the `SymArray` class, which allows for creation of arrays from lists of constant or +    to the `SymArray` class, which allows for creation of arrays from lists of constant or     symbolic lists of pairs. The first argument is the value to use for uninitialized entries.     Note that the initializer must be a known constant, i.e., it cannot be symbolic. Latter     elements of the list will overwrite the earlier ones, if there are repeated keys.@@ -283,7 +1206,7 @@     need its functionality back.    * Reworked SBVBenchSuite api, Phase 1 of BenchSuite completed.-  +   * Add support for addAxiom command to work in the interactive mode.     Thanks to Martin Lundfall for the feedback. @@ -936,7 +1859,7 @@     'sAssert' calls were run in the context of the final output boolean,     which is simply the wrong thing to do. -### Version 7.8, Released 2018-05-18+### Version 7.8, 2018-05-18    * Fix printing of min-bounds for signed 32/64 bit numbers in C     code generation: These are tricky since C does not allow@@ -972,7 +1895,7 @@     showing how to code cover properties using SBV, using a form     of bounded model checking. -### Version 7.7, Released 2018-04-29+### Version 7.7, 2018-04-29    * Add support for Symbolic characters ('SChar') and strings ('SString'.)     Thanks to Joel Burget for the initial implementation.@@ -982,7 +1905,7 @@     due to the current limitations in SMT-solvers. However, there     is a pending SMTLib proposal to support unicode, and SBV will track     these changes to have full unicode support: For further details-    see: http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml+    see: https://smt-lib.org/theories-UnicodeStrings.shtml      The 'SString' type is the type of symbolic strings, consisting     of characters from the Latin-1 character set currently, just@@ -1000,7 +1923,7 @@     Note that currently only Z3 and CVC4 has support for this logic,     and they do differ in some details. Various character/string     operations are supported, including length, concatenation,-    regular-expression matching, substrig operations, recognizers, etc.+    regular-expression matching, substring operations, recognizers, etc.     If you use this logic, you are likely to find bugs in solvers themselves     as support is rather new: Please report. @@ -1028,7 +1951,7 @@     reals from the Internals module for further user processing.     Thanks  to Jan Path for the patch. -### Version 7.6, Released 2018-03-18+### Version 7.6, 2018-03-18    * GHC 8.4.1 compatibility: Work around compilation issues. SBV     now compiles cleanly with GHC 8.4.1.@@ -1038,7 +1961,7 @@     bit sizes. These are similar to sWord8, sInt8, etc.; except     they create dynamic counterparts that can be of arbitrary bit size. -### Version 7.5, Released 2018-01-13+### Version 7.5, 2018-01-13    * Remove obsolete references to tactics in a few haddock comments. Thanks     to Matthew Pickering for reporting.@@ -1894,7 +2817,7 @@ ### Version 4.1, 2015-03-06    * Add support for the ABC solver from Berkeley. Thanks to Adam Foltzer-    for the required infrastructure! See: http://www.eecs.berkeley.edu/~alanmi/abc/+    for the required infrastructure! See: https://github.com/berkeley-abc/abc     And Alan Mishchenko for adding infrastructure to ABC to work with SBV.    * Upgrade the Boolector connection to use a SMT-Lib2 based interaction. NB. You@@ -1903,7 +2826,7 @@   * Tracking changes in the SMT-Lib floating-point theory. If you are     using symbolic floating-point types (i.e., SFloat and SDouble), then     you should upgrade to this version and also get a very latest (unstable)-    Z3 release. See http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml+    Z3 release. See https://smt-lib.org/theories-FloatingPoint.shtml     for details.    * Introduce a new class, 'RoundingFloat', which supports floating-point@@ -2019,10 +2942,6 @@  ### Version 3.1, 2014-07-12 - NB: GHC 7.8.1 and 7.8.2 has a serious bug <http://ghc.haskell.org/trac/ghc/ticket/9078>-     that causes SBV to crash under heavy/repeated calls. The bug is addressed-     in GHC 7.8.3; so upgrading to GHC 7.8.3 is essential for using SBV!-  New features/bug-fixes in v3.1:   * Using multiple-SMT solvers in parallel:@@ -2118,7 +3037,7 @@ ### Version 2.10, 2013-03-22   * Add support for the Boolector SMT solver-    * See: http://fmv.jku.at/boolector/+    * See: https://boolector.github.io     * Use `import Data.SBV.Bridge.Boolector` to use Boolector from SBV     * Boolector supports QF_BV (with an without arrays). In the last       SMT-Lib competition it won both bit-vector categories. It is definitely@@ -2176,7 +3095,6 @@     to the chosen solver as determined by the imported module. (The latter is     useful for modifying options to the SMT solver in an solver-agnostic way.)   * Various improvements to Z3 model parsing routines.-  * New web page for SBV: http://leventerkok.github.io/sbv/ is now online.  ### Version 2.8, 2012-11-29 @@ -2342,9 +3260,6 @@    * Add a hook so users can add custom script segments for SMT solvers. The new     "solverTweaks" field in the SMTConfig data-type can be used for this purpose.-    The need for this came about due to the need to workaround a Z3 v3.2 issue-    detailed below:-      http://stackoverflow.com/questions/9426420/soundness-issue-with-integer-bv-mixed-benchmarks     As a consequence, mixed Integer/BV problems can cause soundness issues in Z3     and does in SBV. Unfortunately, it is too severe for SBV to add the workaround     option, as it slows down the solver as a side effect as well. Thus, we are

@@ -1,4 +1,4 @@-Copyright (c) 2010-2022, Levent Erkok (erkokl@gmail.com)+Copyright (c) 2010-2026, Levent Erkok (erkokl@gmail.com) All rights reserved.  The sbv library is distributed with the BSD3 license. See the LICENSE file

@@ -21,17 +21,20 @@ -- Falsifiable. Counter-example: --   s0 = 64 :: Word8 ----- The function 'prove' has the following type:+-- And similarly, 'sat' finds a satisfying instance. The types involved are: -- -- @---     'prove' :: 'Provable' a => a -> 'IO' 'ThmResult'+--     'prove' :: 'Provable' a => a -> 'IO' t'ThmResult'+--     'sat'   :: 'Data.SBV.Provers.Satisfiable' a => a -> 'IO' t'SatResult' -- @ ----- The class 'Provable' comes with instances for n-ary predicates, for arbitrary n.+-- The classes 'Provable' and 'Data.SBV.Provers.Satisfiable' come with instances for n-ary predicates, for arbitrary n. -- The predicates are just regular Haskell functions over symbolic types listed below. -- Functions for checking satisfiability ('sat' and 'allSat') are also -- provided. --+-- __Symbolic Types__+-- -- The sbv library introduces the following symbolic types: -- --   * 'SBool': Symbolic Booleans (bits).@@ -78,6 +81,14 @@ -- --   * Uninterpreted sorts, and proofs over such sorts, potentially with axioms. --+--   *  Algebraic data types, including recursive fields..+--+--   * Ability to define SMTLib functions, generated directly from Haskell versions,+--     including support for recursive and mutually recursive functions.+--+--   * Express quantified formulas (both universals and existentials, including+--     alternating quantifiers), covering first-order logic.+-- --   * Model validation: SBV can validate models returned by solvers, which allows --     for protection against bugs in SMT solvers and SBV itself. (See the 'validateModel' --     parameter.)@@ -105,8 +116,11 @@ -- return a satisfying assignment, if there is one. The 'allSat' function returns -- all satisfying assignments. --+--+-- __Solvers__+-- -- The sbv library uses third-party SMT solvers via the standard SMT-Lib interface:--- <http://smtlib.cs.uiowa.edu/>+-- <https://smt-lib.org> -- -- The SBV library is designed to work with any SMT-Lib compliant SMT-solver. -- Currently, we support the following SMT-Solvers out-of-the box:@@ -115,15 +129,17 @@ -- --   * CVC4, and CVC5 from Stanford University and the University of Iowa. <https://cvc4.github.io/> and <https://cvc5.github.io> -----   * Boolector from Johannes Kepler University: <http://fmv.jku.at/boolector/> and its successor Bitwuzla from Stanford---     university: <https://github.com/bitwuzla/bitwuzla>+--   * Boolector from Johannes Kepler University: <https://boolector.github.io> and its successor Bitwuzla from Stanford+--     university: <https://bitwuzla.github.io> -- --   * MathSAT from Fondazione Bruno Kessler and DISI-University of Trento: <http://mathsat.fbk.eu/> -----   * Yices from SRI: <http://yices.csl.sri.com/>+--   * Yices from SRI: <http://github.com/SRI-CSL/yices2> -- --   * DReal from CMU: <http://dreal.github.io/> --+--   * OpenSMT from Università della Svizzera italiana <https://verify.inf.usi.ch/opensmt>+-- --   * Z3 from Microsoft: <http://github.com/Z3Prover/z3/wiki> -- -- SBV requires recent versions of these solvers; please see the file@@ -134,14 +150,50 @@ -- -- Support for other compliant solvers can be added relatively easily, please -- get in touch if there is a solver you'd like to see included.+--+--+-- __TP: Semi-automated theorem proving__+--+-- While SMT solvers are quite powerful, there is a certain class of problems that they are just not well suited for. In particular, SMT+-- solvers are not good at proofs that require induction, or those that require complex chains of reasoning. Induction is necessary to reason about+-- any recursive algorithm, and most such proofs require carefully constructed equational steps.+--+-- SBV allows for a style of semi-automated theorem proving, called TP, which can be used to construct such proofs.+-- The documentation includes example proofs for many list functions, and even inductive proofs for+-- the familiar insertion, merge, quick-sort algorithms, along with a proof that the square-root of 2 is irrational.+-- While a proper theorem prover (such as Lean, Isabelle etc.) is a more appropriate choice for such proofs, with some+-- guidance (and acceptance of a much larger trusted code base!), SBV can be used to establish correctness of various mathematical+-- claims and algorithms that are usually beyond the scope of SMT solvers alone.+-- See "Data.SBV.TP" for the API, and+--+--    - "Documentation.SBV.Examples.TP.BinarySearch"+--    - "Documentation.SBV.Examples.TP.GCD"+--    - "Documentation.SBV.Examples.TP.InsertionSort"+--    - "Documentation.SBV.Examples.TP.MergeSort"+--    - "Documentation.SBV.Examples.TP.QuickSort"+--    - "Documentation.SBV.Examples.TP.Sqrt2IsIrrational"+--    - "Documentation.SBV.Examples.TP.ShefferStroke"+--    - "Documentation.SBV.Examples.TP.Lists"+--+-- for various proofs performed in this style.+--+-- Note that SBV's TP proofs are upto termination, i.e., if you axiomatize+-- non-terminating behavior, then you can prove arbitrary results. SBV neither+-- checks nor ensures termination, which is beyond its scope and capabilities.+-- So, any TP proof should be considered true so long as all functions+-- used in the property are terminating. ----------------------------------------------------------------------------- -{-# LANGUAGE DataKinds            #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE ScopedTypeVariables  #-}-{-# LANGUAGE TypeApplications     #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeOperators        #-}+{-# LANGUAGE CPP                   #-}+{-# LANGUAGE DataKinds             #-}+{-# LANGUAGE DefaultSignatures     #-}+{-# LANGUAGE FlexibleContexts      #-}+{-# LANGUAGE FlexibleInstances     #-}+{-# LANGUAGE MultiParamTypeClasses #-}+{-# LANGUAGE ScopedTypeVariables   #-}+{-# LANGUAGE TypeApplications      #-}+{-# LANGUAGE TypeFamilies          #-}+{-# LANGUAGE TypeOperators         #-}  {-# OPTIONS_GHC -Wall -Werror #-} @@ -161,7 +213,7 @@   , SWord8, SWord16, SWord32, SWord64, SWord, WordN   -- *** Signed bit-vectors   , SInt8, SInt16, SInt32, SInt64, SInt, IntN-  -- *** Converting between fixed-size and arbitrary bitvectors+  -- *** Converting between fixed-size and arbitrary bit-vectors   , BVIsNonZero, FromSized, ToSized, fromSized, toSized   -- ** Unbounded integers   -- $unboundedLimitations@@ -175,8 +227,9 @@   , SFPSingle, FPSingle   , SFPDouble, FPDouble   , SFPQuad, FPQuad+  , fpFromInteger   -- ** Rationals-  , SRational+  , SRational, (.%)   -- ** Algebraic reals   -- $algReals   , SReal, AlgReal(..), sRealToSInteger, algRealToRational, RealPoint(..), realPoint, RationalCV(..)@@ -185,16 +238,18 @@   , SChar, SString   -- ** Symbolic lists   -- $lists-  , SList+  , SList, (.:)+  -- ** Symbolic enumerators+  , EnumSymbolic(..), sEnum+  -- ** Symbolic case-expressions+  , sCase, pCase   -- ** Tuples   -- $tuples   , SymTuple, STuple, STuple2, STuple3, STuple4, STuple5, STuple6, STuple7, STuple8-  -- ** Sum types-  , SMaybe, SEither   -- ** Sets   , RCSet(..), SSet   -- * Arrays of symbolic values-  , SymArray(readArray, writeArray, mergeArrays, sListArray), newArray_, newArray, SArray+  , SArray, sArray, sArray_, sArrays, readArray, writeArray, lambdaArray, constArray, freeArray, listArray, ArrayModel(..)    -- * Creating symbolic values   -- ** Single value@@ -217,10 +272,14 @@   , sString, sString_   , sList, sList_   , sTuple, sTuple_-  , sEither, sEither_-  , sMaybe, sMaybe_   , sSet, sSet_ +  -- * Symbolic 'Maybe'+  , SMaybe, sMaybe, sMaybe_, sMaybes++  -- * Symbolic 'Either'+  , SEither, sEither, sEither_, sEithers+   -- ** List of values   -- $createSyms   , sBools@@ -241,13 +300,11 @@   , sStrings   , sLists   , sTuples-  , sEithers-  , sMaybes   , sSets    -- * Symbolic Equality and Comparisons   -- $distinctNote-  , EqSymbolic(..), OrdSymbolic(..), Equality(..)+  , EqSymbolic(..), OrdSymbolic(..), Zero(..), MeasureOf, Equality(..)   -- * Conditionals: Mergeable values   , Mergeable(..), ite, iteLazy @@ -255,6 +312,8 @@   , SIntegral   -- * Division and Modulus   , SDivisible(..)+  -- $euclidianNote+  , sEDivMod, sEDiv, sEMod, sDivides   -- * Bit-vector operations   -- ** Conversions   , sFromIntegral@@ -288,40 +347,53 @@   -- ** Showing values in detail   , crack -  -- * Enumerations-  -- $enumerations-  , mkSymbolicEnumeration+  -- * Symbolic data types+  -- $symbolicADT+  , mkSymbolic -  -- * Uninterpreted sorts, axioms, constants, and functions-  -- $uninterpreted-  , mkUninterpretedSort, Uninterpreted(..), addAxiom+  -- * Stopping unrolling: Defined functions+  , SMTDefinable(..)+  , smtFunction+  , smtFunctionWithMeasure+  , smtFunctionWithContract+  , smtProductiveFunction+  , smtFunctionNoTermination+  , ContractOf, MeasureHelper(..)+  , smtHOFunction, smtHOFunctionWithMeasure, Closure(..), registerType -  -- * Adding SMT functions-  , addSMTDefinition+  -- * Special relations+  -- $specialRels+  , Relation, isPartialOrder, isLinearOrder, isTreeOrder, isPiecewiseLinearOrder, mkTransitiveClosure    -- * Properties, proofs, and satisfiability   -- $proveIntro-  -- $noteOnNestedQuantifiers   -- $multiIntro-  , Predicate, Goal-  , Provable, universal_, universal, existential_, existential+  , Predicate, ConstraintSet, Provable, Satisfiable   , prove, proveWith   , dprove, dproveWith   , sat, satWith   , dsat, dsatWith   , allSat, allSatWith-  , optimize, optimizeWith, isVacuous-  , isVacuousWith, isTheorem, isTheoremWith, isSatisfiable, isSatisfiableWith-  , proveWithAll, proveWithAny, satWithAll-  , proveConcurrentWithAny, proveConcurrentWithAll, satConcurrentWithAny, satConcurrentWithAll-  , satWithAny, generateSMTBenchmark+  , isVacuousProof, isVacuousProofWith+  , isTheorem, isTheoremWith, isSatisfiable, isSatisfiableWith+  , proveWithAny, proveWithAll, proveConcurrentWithAny, proveConcurrentWithAll+  , satWithAny,   satWithAll,   satConcurrentWithAny,   satConcurrentWithAll+  , generateSMTBenchmarkSat, generateSMTBenchmarkProof   , solve-  -- * Constraints+  -- ** Partitioning result space+  -- $partitionIntro+  , allSatPartition++  -- * Constraints and Quantifiers   -- $constrainIntro   -- ** General constraints   -- $generalConstraints   , constrain, softConstrain +  -- ** Quantified constraints, quantifier elimination, and skolemization+  -- $quantifiers+  , QuantifiedBool, quantifiedBool, Forall(..), Exists(..), ExistsUnique(..), ForallN(..), ExistsN(..), QNot(..), Skolemize(..)+   -- ** Constraint Vacuity   -- $constraintVacuity @@ -338,13 +410,17 @@    -- * Checking safety   -- $safeIntro-  , sAssert, isSafe, SExecutable, sName_, sName, safe, safeWith+  , sAssert, isSafe, SExecutable, sName, safe, safeWith    -- * Quick-checking   , sbvQuickCheck    -- * Optimization   -- $optiIntro+  , optimize, optimizeWith+  , optLexicographic, optLexicographicWith+  , optPareto, optParetoWith+  , optIndependent, optIndependentWith    -- ** Multiple optimization goals   -- $multiOpt@@ -356,7 +432,7 @@   -- $softAssertions   , assertWithPenalty , Penalty(..)   -- ** Field extensions-  -- | If an optimization results in an infinity/epsilon value, the returned `CV` value will be in the corresponding extension field.+  -- | If an optimization results in an infinity/epsilon value, the returned t'CV' value will be in the corresponding extension field.   , ExtCV(..), GeneralizedCV(..)    -- * Model extraction@@ -372,16 +448,16 @@    -- ** Programmable model extraction   -- $programmableExtraction-  , SatModel(..), Modelable(..), displayModels, extractModels-  , getModelDictionaries, getModelValues, getModelUninterpretedValues+  , Modelable(..), displayModels, extractModels+  , getModelDictionaries, getModelValues    -- * SMT Interface-  , SMTConfig(..), Timing(..), SMTLibVersion(..), Solver(..), SMTSolver(..)+  , SMTConfig(..), TPOptions(..), Timing(..), SMTLibVersion(..), Solver(..), SMTSolver(..)   -- ** Controlling verbosity   -- $verbosity    -- ** Solvers-  , boolector, bitwuzla, cvc4, cvc5, yices, dReal, z3, mathSAT, abc+  , boolector, bitwuzla, cvc4, cvc5, yices, dReal, z3, mathSAT, abc, openSMT   -- ** Configurations   , defaultSolverConfig, defaultSMTCfg, defaultDeltaSMTCfg, sbvCheckSolverInstallation, getAvailableSolvers   , setLogic, Logic(..), setOption, setInfo, setTimeOut@@ -390,11 +466,14 @@    -- * Abstract SBV type   , SBV, HasKind(..), Kind(..)-  , SymVal, sbvForall, sbvForall_, mkForallVars, sbvExists, sbvExists_, mkExistVars, free-  , free_, mkFreeVars, symbolic, symbolics, literal, unliteral, fromCV+  , SymVal, free, free_, mkFreeVars, symbolic, symbolics, literal, unliteral, fromCV   , isConcrete, isSymbolic, isConcretely, mkSymVal   , MonadSymbolic(..), Symbolic, SymbolicT, label, output, runSMT, runSMTWith+  , some +  -- * Queriable values+  , Queriable(..), freshVar, freshVar_+   -- * Module exports   -- $moduleExportIntro @@ -404,14 +483,16 @@   , module Data.Ratio   ) where +import Control.Monad       (unless)+import Control.Monad.Trans (MonadIO)++import qualified Data.Text as T+ import Data.SBV.Core.AlgReals-import Data.SBV.Core.Data       hiding (sbvForall, sbvForall_,-                                        mkForallVars, sbvExists, sbvExists_,-                                        mkExistVars, free, free_, mkFreeVars,+import Data.SBV.Core.Data       hiding (free, free_, mkFreeVars,                                         output, symbolic, symbolics, mkSymVal,-                                        newArray, newArray_)+                                        bvExtract, bvDrop, bvTake, (#)) import Data.SBV.Core.Model      hiding (assertWithPenalty, minimize, maximize,-                                        sbvForall, sbvForall_, sbvExists, sbvExists_,                                         solve, sBool, sBool_, sBools, sChar, sChar_, sChars,                                         sDouble, sDouble_, sDoubles, sFloat, sFloat_, sFloats,                                         sFloatingPoint, sFloatingPoint_, sFloatingPoints,@@ -419,35 +500,42 @@                                         sFPDouble, sFPDouble_, sFPDoubles, sFPQuad, sFPQuad_, sFPQuads,                                         sInt8, sInt8_, sInt8s, sInt16, sInt16_, sInt16s, sInt32, sInt32_, sInt32s,                                         sInt64, sInt64_, sInt64s, sInteger, sInteger_, sIntegers,+                                        sWord, sWords, sWord_, sInt, sInts, sInt_,                                         sList, sList_, sLists, sTuple, sTuple_, sTuples,                                         sReal, sReal_, sReals, sString, sString_, sStrings,                                         sRational, sRational_, sRationals,                                         sWord8, sWord8_, sWord8s, sWord16, sWord16_, sWord16s,                                         sWord32, sWord32_, sWord32s, sWord64, sWord64_, sWord64s,-                                        sMaybe, sMaybe_, sMaybes, sEither, sEither_, sEithers, sSet, sSet_, sSets,-                                        sBarrelRotateLeft, sBarrelRotateRight)--import qualified Data.SBV.Core.Model as M (sBarrelRotateLeft, sBarrelRotateRight)+                                        sSet, sSet_, sSets,+                                        sArray, sArray_, sArrays,+                                        sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend, sObserve) -import           Data.SBV.Core.Sized       hiding (sWord, sWord_, sWords, sInt, sInt_, sInts, bvExtract, (#), zeroExtend, signExtend, bvDrop, bvTake)-import qualified Data.SBV.Core.Sized as CS+import qualified Data.SBV.Core.Model as M  (sBarrelRotateLeft, sBarrelRotateRight, zeroExtend, signExtend)+import qualified Data.SBV.Core.Data  as CD (bvExtract, (#), bvDrop, bvTake)  import Data.SBV.Core.Kind  import Data.SBV.Core.SizedFloats +import Data.SBV.Maybe hiding (map)+import Data.SBV.Either+ import Data.SBV.Core.Floating-import Data.SBV.Core.Symbolic   (MonadSymbolic(..), SymbolicT)+import Data.SBV.Core.Symbolic   ( MonadSymbolic(..), SymbolicT, registerKind+                                , ProgInfo(..), rProgInfo, SpecialRelOp(..), UICodeKind(UINone)+                                , getRootState, UIName(UIGiven)+                                ) -import Data.SBV.Provers.Prover hiding (universal_, universal, existential_, existential,-                                       prove, proveWith, sat, satWith, allSat,+import Data.SBV.Provers.Prover hiding (prove, proveWith, sat, satWith, allSat,                                        dsat, dsatWith, dprove, dproveWith,                                        allSatWith, optimize, optimizeWith,-                                       isVacuous, isVacuousWith, isTheorem,-                                       isTheoremWith, isSatisfiable,+                                       isVacuousProof, isVacuousProofWith,+                                       isTheorem, isTheoremWith, isSatisfiable,                                        isSatisfiableWith, runSMT, runSMTWith,-                                       sName_, sName, safe, safeWith)+                                       sName, safe, safeWith) +import Data.IORef (modifyIORef', readIORef)+ import Data.SBV.Client import Data.SBV.Client.BaseIO @@ -459,25 +547,34 @@ import Data.Word  import Data.SBV.SMT.Utils (SBVException(..))+ import Data.SBV.Control.Types (SMTReasonUnknown(..), Logic(..))+import Data.SBV.Control.Utils (getValue, freshVar, freshVar_)  import qualified Data.SBV.Utils.CrackNum as CN  import Data.Proxy (Proxy(..))-import GHC.TypeLits+import Data.Kind  (Type)+import GHC.TypeLits (KnownNat, type (<=), type (+), type (-)) -import Prelude hiding((+), (-), (*)) -- to avoid the haddock ambiguity+import Data.Char (isSpace, isPunctuation)+import Data.SBV.List (EnumSymbolic(..))+import Data.SBV.SEnum (sEnum)+import Data.SBV.SCase (sCase, pCase) +import Data.SBV.Rational++#ifdef DOCTEST --- $setup---- >>> -- For doctest purposes only:---- >>> :set -XDataKinds+--- >>> :set -XDataKinds -XFlexibleContexts -XTypeApplications -XRankNTypes --- >>> import Data.Proxy+#endif  -- | Show a value in detailed (cracked) form, if possible. -- This makes most sense with numbers, and especially floating-point types.-crack :: SBV a -> String-crack (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv = s-crack (SBV sv)                                            = show sv+crack :: Bool -> SBV a -> String+crack verb (SBV (SVal _ (Left cv))) | Just s <- CN.crackNum cv verb Nothing = s+crack _    (SBV sv)                                                         = show sv  -- Haddock section documentation {- $progIntro@@ -514,7 +611,7 @@ design goal is to let SMT solvers be used without any knowledge of how SMT solvers work or how different logics operate. The details are hidden behind the SBV framework, providing Haskell programmers with a clean API that is unencumbered by the details of individual solvers.-To that end, we use the SMT-Lib standard (<http://smtlib.cs.uiowa.edu/>)+To that end, we use the SMT-Lib standard (<https://smt-lib.org>) to communicate with arbitrary SMT solvers. -} @@ -593,7 +690,7 @@   Goals can be lexicographically (default), independently, or pareto-front optimized. The relevant functions are:        * 'minimize': Minimize a given arithmetic goal-      * 'maximize': Minimize a given arithmetic goal+      * 'maximize': Maximize a given arithmetic goal    Goals can be optimized at a regular or an extended value: An extended value is either positive or negative infinity   (for unbounded integers and reals) or positive or negative epsilon differential from a real value (for reals).@@ -686,8 +783,8 @@         @          'assertWithPenalty' "bounded_x" (x .< 5) 'DefaultPenalty'-         'assertWithPenalty' "bounded_x" (x .< 5) ('Penalty' 2.3 Nothing)-         'assertWithPenalty' "bounded_x" (x .< 5) ('Penalty' 4.7 (Just "group-1")) @+         'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 2.3 Nothing+         'assertWithPenalty' "bounded_x" (x .< 5) $ v'Penalty' 4.7 (Just "group-1") @    In the first form, we are saying that the constraint @x .< 5@ must be satisfied, if possible,   but if this constraint can not be satisfied to find a model, it can be violated with the default penalty of 1.@@ -708,7 +805,7 @@ -}  {- $resultTypes-'ThmResult', 'SatResult', and 'AllSatResult' are simple newtype wrappers over 'SMTResult'. Their+t'ThmResult', t'SatResult', and t'AllSatResult' are simple newtype wrappers over t'SMTResult'. Their main purpose is so that we can provide custom 'Show' instances to print results accordingly. -} @@ -739,7 +836,7 @@ overflow/underflow as it is the case with the bounded types, such as 'SWord8', 'SInt16', etc. However, some bit-vector based operations are /not/ supported for the 'SInteger' type while in the verification mode. That is, you can use these operations on 'SInteger' values during normal programming/simulation.-but the SMT translation will not support these operations since there corresponding operations are not supported in SMT-Lib.+but the SMT translation will not support these operations since their corresponding operations are not supported in SMT-Lib. Note that this should rarely be a problem in practice, as these operations are mostly meaningful on fixed-size bit-vectors. The operations that are restricted to bounded word/int sizes are: @@ -749,7 +846,7 @@     * Extraction and concatenation: 'bvExtract', '#', 'zeroExtend', 'signExtend', 'bvDrop', and 'bvTake' -Usual arithmetic ('+', '-', '*', 'sQuotRem', 'sQuot', 'sRem', 'sDivMod', 'sDiv', 'sMod') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are+Usual arithmetic ('Prelude.+', 'Prelude.-', '*', 'sQuotRem', 'sQuot', 'sRem', 'sDivMod', 'sDiv', 'sMod') and logical operations ('.<', '.<=', '.>', '.>=', '.==', './=') operations are supported for 'SInteger' fully, both in programming and verification modes. -} @@ -761,7 +858,7 @@ others are not (such as pi and e).  SBV can deal with real numbers just fine, since the theory of reals is decidable. (See-<http://smtlib.cs.uiowa.edu/theories-Reals.shtml>.) In addition, by leveraging backend+<https://smt-lib.org/theories-Reals.shtml>.) In addition, by leveraging backend solver capabilities, SBV can also represent and solve non-linear equations involving real-variables. (For instance, the Z3 SMT solver, supports polynomial constraints on reals starting with v4.0.) -}@@ -774,9 +871,9 @@  {- $strings Support for characters, strings, and regular expressions (initial version contributed by Joel Burget)-adds support for QF_S logic, described here: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>+adds support for QF_S logic, described here: <https://smt-lib.org/theories-UnicodeStrings.shtml> -See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for related functions.+See "Data.SBV.Char", "Data.SBV.List", "Data.SBV.RegExp" for related functions. -}  {- $lists@@ -795,20 +892,81 @@ specialized type-signatures since Haskell insists on an 'Int' second argument for them. -} +{- $partitionIntro+The function 'allSatPartition' allows one to restrict the results returned by calls to 'Data.SBV.allSat'.+In certain cases, we might consider certain models to be "equivalent," i.e., we might want to+create equivalence classes over the search space when it comes to what we consider all satisfying+solutions. In these cases, we can use 'allSatPartition' to tell SBV what classes of solutions to consider+as unique. Consider:++>>> :{+allSat $ do+   x <- sInteger "x"+   y <- sInteger "y"+   allSatPartition "p1" $ x .>= 0+   allSatPartition "p2" $ y .>= 0+:}+Solution #1:+  x  =    -1 :: Integer+  y  =     0 :: Integer+  p1 = False :: Bool+  p2 =  True :: Bool+Solution #2:+  x  =    0 :: Integer+  y  =    0 :: Integer+  p1 = True :: Bool+  p2 = True :: Bool+Solution #3:+  x  =     0 :: Integer+  y  =    -1 :: Integer+  p1 =  True :: Bool+  p2 = False :: Bool+Solution #4:+  x  =    -1 :: Integer+  y  =    -1 :: Integer+  p1 = False :: Bool+  p2 = False :: Bool+Found 4 different solutions.++Without the call to 'allSatPartition' the above example, 'allSat' would return all possible combinations of @x@ and @y@ subject to the constraints. (Since we have none here,+the call would try to enumerate the infinite set of all integer tuples!) But 'allSatPartition' allows us to restrict our attention to the examples that satisfy the partitioning+constraints. The first argument to 'allSatPartition' is simply a name, for diagnostic purposes. Note that the conditions given by 'allSatPartition' are /not/ imposed on the search+space at all: They're only used when we construct the search space. In the above example, we pick one example from each quadrant. Furthermore, while it is typical to pass+a boolean as a partitioning argument, it is not required: Any expression is OK, whose value creates the equivalence class:++>>> :{+allSat $ do+   x <- sInteger "x"+   allSatPartition "p" $ x `sMod` 3+:}+Solution #1:+  x = 2 :: Integer+  p = 2 :: Integer+Solution #2:+  x = 1 :: Integer+  p = 1 :: Integer+Solution #3:+  x = 0 :: Integer+  p = 0 :: Integer+Found 3 different solutions.++In the above, we get three examples, as the expression @x mod 3@ can take only three different values.+-}+ {- $constrainIntro A constraint is a means for restricting the input domain of a formula. Here's a simple example:  @-   do x <- 'sbvExists' \"x\"-      y <- 'sbvExists' \"y\"+   do x <- 'free' \"x\"+      y <- 'free' \"y\"       'constrain' $ x .> y       'constrain' $ x + y .>= 12       'constrain' $ y .>= 3       ... @ -The first constraint requires @x@ to be larger than @y@. The scond one says that+The first constraint requires @x@ to be larger than @y@. The second one says that sum of @x@ and @y@ must be at least @12@, and the final one says that @y@ to be at least @3@. Constraints provide an easy way to assert additional properties on the input domain, right at the point of the introduction of variables.@@ -839,7 +997,7 @@  {- $generalConstraints A good use case (in fact the motivating use case) for 'constrain' is attaching a-constraint to a universally or existentially quantified variable at the time of its creation.+constraint to a variable at the time of its creation. Also, the conjunctive semantics for 'sat' and the implicative semantics for 'prove' simplify programming by choosing the correct interpretation automatically. However, one should be aware of the semantic difference. For instance, in@@ -847,7 +1005,7 @@ /satisfiable/. To wit, consider:   @-    do x <- 'sbvExists' \"x\"+    do x <- 'free' \"x\"        'constrain' $ x .< x        return $ x .< (x :: 'SWord8')  @@@ -855,17 +1013,68 @@ This predicate is unsatisfiable since no element of 'SWord8' is less than itself. But it's (vacuously) true, since it excludes the entire domain of values, thus making the proof trivial. Hence, this predicate is provable, but is not satisfiable. To make sure the given-constraints are not vacuous, the functions 'isVacuous' (and 'isVacuousWith') can be used.+constraints are not vacuous, the functions 'isVacuousProof' (and 'isVacuousProofWith') can be used.  Also note that this semantics imply that test case generation ('Data.SBV.Tools.GenTest.genTest') and quick-check can take arbitrarily long in the presence of constraints, if the random input values generated rarely satisfy the constraints. (As an extreme case, consider @'constrain' 'sFalse'@.) -} +{- $quantifiers+You can write quantified formulas, and reason with them as in first-order logic. Here is a simple example:++@+    constrain $ \\(Forall x) (Exists y) -> y .> (x :: SInteger)+@++You can nest quantifiers as you wish, and the quantified parameters can be of arbitrary symbolic type.+Additionally, you can convert such a quantified formula to a regular boolean, via a call to 'quantifiedBool'+function, essentially performing quantifier elimination:++@+    other_condition .&& quantifiedBool (\\(Forall x) (Exists y) -> y .> (x :: SInteger))+@++Or you can prove/sat quantified formulas directly:++@+    prove $ \\(Forall x) (Exists y) -> y .> (x :: SInteger)+@++This facility makes quantifiers part of the regular SBV language, allowing them to be mixed/matched with all+your other symbolic computations.  See the following files demonstrating reasoning with quantifiers:++   * "Documentation.SBV.Examples.Puzzles.Birthday"+   * "Documentation.SBV.Examples.Puzzles.KnightsAndKnaves"+   * "Documentation.SBV.Examples.Puzzles.Rabbits"+   * "Documentation.SBV.Examples.Misc.FirstOrderLogic"++SBV also supports the constructors t'ExistsUnique' to create unique existentials, in addition+to t'ForallN' and t'ExistsN' for creating multiple variables at the same time.++In general, SBV will not display the values of quantified variables for a satisfying instance.+For a satisfiability problem, you can apply skolemization manually to have these values+computed by the backend solver. Note that skolemization will produce functions for+existentials under universals, and SBV generally cannot translate function values back+to Haskell, except in certain simple cases. However, for prefix existentials, the manual+transformation can pay off. As an example, compare:++>>> sat $ \(Exists x) (Forall y) -> x .<= (y :: SWord8)+Satisfiable++to:++>>> sat $ do { x <- free "x"; pure (quantifiedBool (\(Forall y) -> x .<= (y :: SWord8))) }+Satisfiable. Model:+  x = 0 :: Word8++where we have skolemized the top-level existential out, and received a witness value for it.+-}+ {- $constraintVacuity  When adding constraints, one has to be careful about-making sure they are not inconsistent. The function 'isVacuous' can be use for this purpose.+making sure they are not inconsistent. The function 'isVacuousProof' can be used for this purpose. Here is an example. Consider the following predicate:      >>> let pred = do { x <- free "x"; constrain $ x .< x; return $ x .>= (5 :: SWord8) }@@ -877,9 +1086,9 @@     >>> prove pred     Q.E.D. -We can use 'isVacuous' to make sure to see that the pass was vacuous:+We can use 'isVacuousProof' to make sure to see that the pass was vacuous: -    >>> isVacuous pred+    >>> isVacuousProof pred     True  While the above example is trivial, things can get complicated if there are multiple constraints with@@ -895,7 +1104,7 @@  And the proof is not vacuous: -     >>> isVacuous pred'+     >>> isVacuousProof pred'      False -} @@ -918,90 +1127,76 @@ See 'Data.SBV.Control.getUnsatCore' for details and "Documentation.SBV.Examples.Queries.UnsatCore" for an example use case. -} -{- $uninterpreted+{- $symbolicADT Users can introduce new uninterpreted sorts simply by defining an empty data-type in Haskell and registering it as such. The following example demonstrates:    @      data B-     mkUninterpretedSort ''B+     mkSymbolic [''B]   @ -(Note that you'll also need to use pragmas @TemplateHaskell@, @StandAloneDeriving@, @DeriveDataTypeable@, and @DeriveAnyClass@ for this to work, follow GHC's error messages!)- This is all it takes to introduce @B@ as an uninterpreted sort in SBV, which makes the type @SBV B@ automagically become available as the type of symbolic values that ranges over @B@ values. Note that this will also introduce the type @SB@ into your environment, which is a synonym for @SBV B@. --Uninterpreted functions over both uninterpreted and regular sorts can be declared using the facilities introduced by-the 'Data.SBV.Core.Model.Uninterpreted' class.--}--{- $enumerations-If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then -tou can use the 'mkSymbolicEnumeration' functio to turn it into an enumeration in SMTLib.-A simple example is:+If the uninterpreted sort definition takes the form of an enumeration (i.e., a simple data type with all nullary constructors), then+it will turn into an enumeration in SMTLib.  A simple example is:  @     data X = A | B | C-    mkSymbolicEnumeration ''X+    mkSymbolic [''X] @ -Note the magic incantation @mkSymbolicEnumeration ''X@. For this to work, you need to have the following-options turned on:-->   LANGUAGE TemplateHaskell->   LANGUAGE StandaloneDeriving->   LANGUAGE DeriveDataTypeable->   LANGUAGE DeriveAnyClass+Note the magic incantation @mkSymbolic [''X]@, requires the following extensions:+@TemplateHaskell@, @TypeApplications@, and @FlexibleInstances@.+Parametric data-types also require @ScopedTypeVariables@. -The declaration will automatically introduce the type:+SBV also supports good old ADT's as well, with fields. The support for this is similar, where SBV will create the+corresponding datatype in a symbolic manner:  @-    type SX = SBV X+-- | A basic arithmetic expression type.+data Expr = Num Integer+          | Var String+          | Add Expr Expr+          | Mul Expr Expr+          | Let String Expr Expr++-- | Create a symbolic version of expressions.+mkSymbolic [''Expr] @ -along with symbolic values of each of the enumerated values @sA@, @sB@, and @sC@. This way,-you can refer to the symbolic version as @SX@, treating it as a regular symbolic type ranging over the values @A@, @B@, and @C@. Such values can be compared for equality, and with the usual-other comparison operators, such as @.==@, @./=@, @.>@, @.>=@, @<@, and @<=@. For each enumerated value @X@, the symbolic versions @sX@ is defined to be equal to @literal X@.+These types can also be parameterized, per usual Haskell usage. -A simple query would look like:+We also support a symbolic case-expression quasi-quoter, allowing us to write:  @-     allSat $ \x -> x .== (x :: SX)-@--which would list all three elements of this domain as satisfying solutions.+eval :: SExpr -> SInteger+eval = go []+ where go :: SList (String, Integer) -> SExpr -> SInteger+       go = smtFunction "eval"+          $ \env expr -> [sCase| expr of+                            Num i     -> i+                            Var s     -> get env s+                            Add l r   -> go env l + go env r+                            Mul l r   -> go env l * go env r+                            Let s e r -> go (tuple (s, go env e) SL..: env) r+                         |] -@-     Solution #1:-       s0 = A :: X-     Solution #2:-       s0 = B :: X-     Solution #3:-       s0 = C :: X-     Found 3 different solutions.+       get :: SList (String, Integer) -> SString -> SInteger+       get = smtFunction "get"+           $ \env s -> ite (SL.null env) 0+                     $ let (k, v) = untuple (SL.head env)+                       in ite (s .== k) v (get (SL.tail env) s) @ -Note that the result is properly typed as @X@ elements; these are not mere strings.--See "Documentation.SBV.Examples.Misc.Enumerate" for an extended example on how to use symbolic enumerations.--}--{- $noteOnNestedQuantifiers-=== A note on reasoning in the presence of quantifiers #noteOnNested#+which defines an interpreter for this data-type. Such definitions also come with an induction principle+to perform TP based proofs on. These can be accessed using the 'Data.SBV.TP.inductiveLemma' function. -Note that SBV allows reasoning with quantifiers: Inputs can be existentially or universally quantified. Predicates can be built-with arbitrary nesting of such quantifiers as well. However, SBV always /assumes/ that the input is in-prenex-normal form: <http://en.wikipedia.org/wiki/Prenex_normal_form>. That is,-all the input declarations are treated as happening at the beginning of a predicate, followed by the actual formula. Unfortunately,-the way predicates are written can be misleading at times, since symbolic inputs can be created at arbitrary points; interleaving them-with other code. The rule is simple, however: All inputs are assumed at the top, in the order declared, regardless of their quantifiers.-SBV will apply skolemization to get rid of existentials before sending predicates to backend solvers. However, if you do want nested-quantification, you will manually have to first convert to prenex-normal form (which produces an equisatisfiable but not necessarily-equivalent formula), and code that explicitly in SBV. See [Issue 256](http://github.com/LeventErkok/sbv/issues/256) and [Issue 623](https://github.com/LeventErkok/sbv/issues/623) for a detailed discussion-of this issue.+The argument to @mkSymbolic@ is typically a list of types. The requirement is that if the types you pass on+are mutually recursively defined, you should give them as a list. Otherwise, you can give them all together,+or one at a time. -}  {- $cardIntro@@ -1030,7 +1225,7 @@  {- $verbosity -SBV provides various levels of verbosity to aid in debugging, by using the 'SMTConfig' fields:+SBV provides various levels of verbosity to aid in debugging, by using the t'SMTConfig' fields:    * ['verbose'] Print on stdout a shortened account of what is sent/received. This is specifically trimmed to reduce noise     and is good for quick debugging. The output is not supposed to be machine-readable.@@ -1059,10 +1254,10 @@            return $ observe "Expected" spec .== observe "Result" res :} Falsifiable. Counter-example:-  Expected = 34 :: Word8-  Result   =  1 :: Word8   i1       = 12 :: Word8   i2       = 22 :: Word8+  Expected = 34 :: Word8+  Result   =  1 :: Word8  The 'observeIf' variant allows the user to specify a boolean condition when the value is interesting to observe. Useful when you have lots of "debugging" points, but not all are of interest. Use the 'sObserve' variant when you are at the 'Symbolic'@@ -1085,13 +1280,39 @@ Q.E.D. -} +{- $euclidianNote+=== Euclidian division and modulus++Euclidian division and modulus for integers differ from regular division modulus when+the divisor is negative. It satisfies the following desirable property: For any @m@, @n@, we have:++@+  Given @m@, @n@, s.t., n /= 0+  Let (q, r) = m `sEDivMod` n+  Then: m = n * q + r+   and 0 <= r <= |n| - 1+@++That is, the modulus is always positive.+There's no standard Haskell function that performs this operation. The main reason to prefer this+function is that SMT solvers can deal with them better.+Compare:++>>> sDivMod @SInteger 3 (-2)+(-2 :: SInteger,-1 :: SInteger)+>>> sEDivMod 3 (-2)+(-1 :: SInteger,1 :: SInteger)+>>> prove $ \x y -> y .> 0 .=> x `sDivMod` y .== x `sEDivMod` y+Q.E.D.+-}+ {- $conversionNote Capture convertability from/to FloatingPoint representations.  Conversions to float: 'toSFloat' and 'toSDouble' simply return the nearest representable float from the given type based on the rounding mode provided. Similarly, 'toSFloatingPoint' converts to a generalized-floating-point number with specified exponent and significand bith widths.+floating-point number with specified exponent and significand bit widths.  Conversions from float: 'fromSFloat', 'fromSDouble', 'fromSFloatingPoint' functions do the reverse conversion. However some care is needed when given values@@ -1120,7 +1341,7 @@ same thing! Same goes for Haskell, which seems to convert via Int64, but we do not model that behavior in SBV as it doesn't seem to be intentional nor well documented. -You can check for @NaN@, @oo@ and @-oo@, using the predicates 'fpIsNaN', 'fpIsInfinite',+You can check for @NaN@, @oo@ and @-oo@, using the predicates 'Data.SBV.Core.Floating.fpIsNaN', 'Data.SBV.Core.Floating.fpIsInfinite', and 'fpIsPositive', 'fpIsNegative' predicates, respectively; and do the proper conversion based on your needs. (0 is a good choice, as are min/max bounds of the target type.) @@ -1147,15 +1368,15 @@ Q.E.D. >>> prove $ roundTrip @Int32 Falsifiable. Counter-example:-  s0 = RoundNearestTiesToEven :: RoundingMode-  s1 =             -156765620 :: Int32+  s0 = RoundNearestTiesToAway :: RoundingMode+  s1 =               22049281 :: Int32  Note how we get a failure on `Int32`. The counter-example value is not representable exactly as a single precision float: ->>> toRational (-156765620 :: Float)-(-156765616) % 1+>>> toRational (22049281 :: Float)+22049280 % 1 -Note how the numerator is different, it is off by 4. This is hardly surprising, since floats become sparser as+Note how the numerator is different, it is off by 1. This is hardly surprising, since floats become sparser as the magnitude increases to be able to cover all the integer values representable.  >>> :{@@ -1177,20 +1398,20 @@ Q.E.D. >>> prove $ roundTrip @Int64 Falsifiable. Counter-example:-  s0 = RoundTowardNegative :: RoundingMode-  s1 =    9007199254740995 :: Int64+  s0 = RoundNearestTiesToEven :: RoundingMode+  s1 =    2305843026393563113 :: Int64  Just like in the `SFloat` case, once we reach 64-bits, we no longer can exactly represent the integer value for all possible values: ->>>  toRational (9007199254740995 :: Double)-9007199254740996 % 1+>>> toRational (fromIntegral (2305843026393563113 :: Int64) :: Double)+2305843026393563136 % 1 -In this case the numerator is off by 1.+In this case the numerator is off by 23. -}  -- | An implementation of rotate-left, using a barrel shifter like design. Only works when both--- arguments are finite bitvectors, and furthermore when the second argument is unsigned.+-- arguments are finite bit-vectors, and furthermore when the second argument is unsigned. -- The first condition is enforced by the type, but the second is dynamically checked. -- We provide this implementation as an alternative to `sRotateLeft` since SMTLib logic -- does not support variable argument rotates (as opposed to shifts), and thus this@@ -1223,9 +1444,9 @@                                       -> proxy j                -- ^ @j@: End position, numbered from @n-1@ to @0@, @j <= i@ must hold                                       -> SBV (bv n)             -- ^ Input bit vector of size @n@                                       -> SBV (bv (i - j + 1))   -- ^ Output is of size @i - j + 1@-bvExtract = CS.bvExtract+bvExtract = CD.bvExtract --- | Join two bitvectors.+-- | Join two bit-vectors. -- -- >>> prove $ \x y -> x .== bvExtract (Proxy @79) (Proxy @71) ((x :: SWord 9) # (y :: SWord 71)) -- Q.E.D.@@ -1234,7 +1455,7 @@        ) => SBV (bv n)                     -- ^ First input, of size @n@, becomes the left side          -> SBV (bv m)                     -- ^ Second input, of size @m@, becomes the right side          -> SBV (bv (n + m))               -- ^ Concatenation, of size @n+m@-(#) = (CS.#)+(#) = (CD.#) infixr 5 #  -- | Zero extend a bit-vector.@@ -1248,7 +1469,7 @@                              , BVIsNonZero (m - n)                              ) => SBV (bv n)    -- ^ Input, of size @n@                                -> SBV (bv m)    -- ^ Output, of size @m@. @n < m@ must hold-zeroExtend = CS.zeroExtend+zeroExtend = M.zeroExtend  -- | Sign extend a bit-vector. --@@ -1261,10 +1482,10 @@                              , n + 1 <= m                              , SFiniteBits (bv n)                              , SIntegral   (bv (m - n))-                             , BVIsNonZero   (m - n)+                             , BVIsNonZero (m - n)                              ) => SBV (bv n)  -- ^ Input, of size @n@                                -> SBV (bv m)  -- ^ Output, of size @m@. @n < m@ must hold-signExtend = CS.signExtend+signExtend = M.signExtend  -- | Drop bits from the top of a bit-vector. --@@ -1280,7 +1501,7 @@                                  ) => proxy i                    -- ^ @i@: Number of bits to drop. @i < n@ must hold.                                    -> SBV (bv n)                 -- ^ Input, of size @n@                                    -> SBV (bv m)                 -- ^ Output, of size @m@. @m = n - i@ holds.-bvDrop = CS.bvDrop+bvDrop = CD.bvDrop  -- | Take bits from the top of a bit-vector. --@@ -1296,7 +1517,7 @@                                ) => proxy i                  -- ^ @i@: Number of bits to take. @0 < i <= n@ must hold.                                  -> SBV (bv n)               -- ^ Input, of size @n@                                  -> SBV (bv i)               -- ^ Output, of size @i@-bvTake = CS.bvTake+bvTake = CD.bvTake  -- | A helper class to convert sized bit-vectors to/from bytes. class ByteConverter a where@@ -1465,4 +1686,173 @@      = error $ "fromBytes:SWord 1024: Incorrect number of bytes: " ++ show l      where l = length as -{-# ANN module ("HLint: ignore Use import/export shortcut" :: String) #-}+{- $specialRels+A special relation is a binary relation that has additional properties. SBV allows for the checking of various kinds+of special relations respecting various axioms, and allows for creating transitive closures.+See "Documentation.SBV.Examples.Misc.FirstOrderLogic" for several examples.+-}++-- | A type synonym for binary relations.+type Relation a = (SBV a, SBV a) -> SBool++-- | Check if a relation is a partial order. The string argument must uniquely identify this order.+isPartialOrder :: SymVal a => String -> Relation a -> SBool+isPartialOrder = checkSpecialRelation . IsPartialOrder++-- | Check if a relation is a linear order. The string argument must uniquely identify this order.+isLinearOrder :: SymVal a => String -> Relation a -> SBool+isLinearOrder = checkSpecialRelation . IsLinearOrder++-- | Check if a relation is a tree order. The string argument must uniquely identify this order.+isTreeOrder :: SymVal a => String -> Relation a -> SBool+isTreeOrder = checkSpecialRelation . IsTreeOrder++-- | Check if a relation is a piece-wise linear order. The string argument must uniquely identify this order.+isPiecewiseLinearOrder :: SymVal a => String -> Relation a -> SBool+isPiecewiseLinearOrder = checkSpecialRelation . IsPiecewiseLinearOrder++-- | Make sure it's internally acceptable+sanitizeRelName :: String -> String+sanitizeRelName s = "__internal_sbv_" ++ map sanitize s+  where sanitize c | isSpace c || isPunctuation c = '_'+                               | True             = c++-- | Create the transitive closure of a given relation. The string argument must uniquely identify the newly created relation.+mkTransitiveClosure :: forall a. SymVal a => String -> Relation a -> Relation a+mkTransitiveClosure nm rel = res+  where ka = kindOf (Proxy @a)++        -- The internal name of this relation+        inm = sanitizeRelName $ "_TransitiveClosure_" ++ nm ++ "_"+        key = (inm, nm)++        res (a, b) = SBV $ SVal KBool $ Right $ cache result+          where result st = do -- Is this new? If so create it, otherwise reuse+                               ProgInfo{progTransClosures = curProgTransClosures} <- readIORef (rProgInfo st)++                               unless (key `elem` curProgTransClosures) $ do++                                  registerKind st ka++                                  -- Add to the end so if we get incremental ones the order doesn't change for old ones!+                                  modifyIORef' (rProgInfo st) (\u -> u{progTransClosures = curProgTransClosures ++ [key]})++                                  -- Equate it to the relation we are given. We want to do this in the root state+                                  let SBV eq = quantifiedBool $ \(Forall x) (Forall y) -> rel (x, y) .== uninterpret inm x y+                                  internalConstraint (getRootState st) False [] eq++                               sa <- sbvToSV st a+                               sb <- sbvToSV st b++                               newExpr st KBool $ SBVApp (Uninterpreted (T.pack nm)) [sa, sb]++-- | Check if the given relation satisfies the required axioms+checkSpecialRelation :: forall a. SymVal a => SpecialRelOp -> Relation a -> SBool+checkSpecialRelation op rel = SBV $ SVal KBool $ Right $ cache result+  where ka = kindOf (Proxy @a)++        internalize nm = case op of+                           IsPartialOrder         _ -> IsPartialOrder         nm+                           IsLinearOrder          _ -> IsLinearOrder          nm+                           IsTreeOrder            _ -> IsTreeOrder            nm+                           IsPiecewiseLinearOrder _ -> IsPiecewiseLinearOrder nm++        result st = do -- The internal name of this relation+                       let nm  = sanitizeRelName (show op)+                           iop = internalize nm++                       -- Is this new? If so create it, otherwise reuse+                       ProgInfo{progSpecialRels = curSpecialRels} <- readIORef (rProgInfo st)++                       unless (op `elem` curSpecialRels) $ do++                          registerKind st ka+                          uop <- newUninterpreted st (UIGiven nm) Nothing (SBVType [ka, ka, KBool]) (UINone True)++                          let nm' = case uop of+                                      Uninterpreted s -> T.unpack s+                                      _               -> error $ "Data.SBV: Impossible happened: checkSpecialRelation received: " ++ show op++                          -- Add to the end so if we get incremental ones the order doesn't change for old ones!+                          modifyIORef' (rProgInfo st) (\u -> u{progSpecialRels = curSpecialRels ++ [iop]})++                          -- Equate it to the relation we are given. We want to do this in the parent state+                          let SBV eq = quantifiedBool $ \(Forall x) (Forall y) -> rel (x, y) .== uninterpret nm' x y+                          internalConstraint (getRootState st) False [] eq++                       newExpr st KBool $ SBVApp (SpecialRelOp ka iop) []++-- | Optimize lexicographically, with the default solver.+optLexicographic :: Satisfiable a => a -> IO SMTResult+optLexicographic = optLexicographicWith defaultSMTCfg++-- | Optimize lexicographically, using the given solver.+optLexicographicWith :: Satisfiable a => SMTConfig -> a -> IO SMTResult+optLexicographicWith config p = do+   res <- optimizeWith config Lexicographic p+   case res of+     LexicographicResult r -> pure r+     _                     -> error $ "A lexicographic optimization call resulted in a bad result:"+                                    ++ "\n" ++ show res++-- | Pareto front optimization, with the default solver.+optPareto :: Satisfiable a => Maybe Int -> a -> IO (Bool, [SMTResult])+optPareto = optParetoWith defaultSMTCfg++-- | Pareto front optimization, with the given solver. The optional integer argument is the number of fronts to return. If 'Nothing', then+-- we will return all pareto fronts. If the first component of the result is 'True' then we reached the pareto-query limit specified by+-- the user, so there might be more unqueried results remaining. If 'False', it means that all the pareto fronts are returned.+optParetoWith :: Satisfiable a => SMTConfig -> Maybe Int -> a -> IO (Bool, [SMTResult])+optParetoWith config mbLim p = do+   res <- optimizeWith config (Pareto mbLim) p+   case res of+     ParetoResult r -> pure r+     _              -> error $ "A pareto optimization call resulted in a bad result:"+                             ++ "\n" ++ show res++-- | Independent optimization, with the default solver. In each result, string is the name of the objective optimized given by the user.+optIndependent :: Satisfiable a => a -> IO [(String, SMTResult)]+optIndependent = optIndependentWith defaultSMTCfg++-- | Independent optimization, with the given solver. In each result, string is the name of the objective optimized given by the user.+optIndependentWith :: Satisfiable a => SMTConfig -> a -> IO [(String, SMTResult)]+optIndependentWith config p = do+   res <- optimizeWith config Independent p+   case res of+     IndependentResult r -> pure r+     _                   -> error $ "An independent optimization call resulted in a bad result:"+                                  ++ "\n" ++ show res++-- | An queriable value: Mapping between concrete/symbolic values. If your type is traversable and simply embeds+-- symbolic equivalents for one type, then you can simply define 'create'. (Which is the most common case.)+class Queriable m a where+  type QueryResult a :: Type++  -- | ^ Create a new symbolic value of type @a@+  create  :: QueryT m a++  -- | ^ Extract the current value in a SAT context+  project :: a -> QueryT m (QueryResult a)++  -- | ^ Create a literal value. Morally, 'embed' and 'project' are inverses of each other+  -- via the t'QueryT' monad transformer.+  embed   :: QueryResult a -> QueryT m a++  default project :: (a ~ t e, QueryResult (t e) ~ t (QueryResult e), Traversable t, Monad m, Queriable m e) =>  a -> QueryT m (QueryResult a)+  project = mapM project++  default embed   :: (a ~ t e, QueryResult (t e) ~ t (QueryResult e), Traversable t, Monad m, Queriable m e) => QueryResult a -> QueryT m a+  embed = mapM embed+  {-# MINIMAL create #-}++-- | Generic 'Queriable' instance for 'SymVal' values. This provides the base case for the generic definitions for project and embed+-- when we automatically derive them. We make this instance overlappable should the user have a different mapping in mind, for instance+-- mapping a symbolic boolean to a concrete integer for whatever reason.+instance {-# OVERLAPPABLE #-} (MonadIO m, SymVal a) => Queriable m (SBV a) where+  type QueryResult (SBV a) = a++  create  = freshVar_+  project = getValue+  embed   = pure . literal++{- HLint ignore module "Use import/export shortcut" -}

@@ -14,18 +14,19 @@ -- and strings. -- -- 'SChar' type only covers all unicode characters, following the specification--- in <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>.+-- in <https://smt-lib.org/theories-UnicodeStrings.shtml>. -- However, some of the recognizers only support the Latin1 subset, suffixed -- by @L1@. The reason for this is that there is no performant way of performing -- these functions for the entire unicode set. As SMTLib's capabilities increase, -- we will provide full unicode versions as well. ----------------------------------------------------------------------------- -{-# LANGUAGE OverloadedStrings   #-}-{-# LANGUAGE Rank2Types          #-}-{-# LANGUAGE ScopedTypeVariables #-}+{-# LANGUAGE CPP               #-}+{-# LANGUAGE OverloadedLists   #-}+{-# LANGUAGE OverloadedStrings #-}+{-# LANGUAGE TypeApplications  #-} -{-# OPTIONS_GHC -Wall -Werror #-}+{-# OPTIONS_GHC -Wall -Werror -Wno-orphans #-}  module Data.SBV.Char (         -- * Occurrence in a string@@ -43,7 +44,7 @@         , isAscii, isLatin1, isAsciiUpper, isAsciiLower         ) where -import Prelude hiding (elem, notElem)+import Prelude hiding (elem, notElem, Enum(..)) import qualified Prelude as P  import Data.SBV.Core.Data@@ -51,19 +52,22 @@  import qualified Data.Char as C -import Data.SBV.String (isInfixOf, singleton)+import Data.SBV.List (EnumSymbolic(..))+import qualified Data.SBV.List as SL +#ifdef DOCTEST -- $setup--- >>> -- For doctest purposes only: -- >>> import Data.SBV--- >>> import Data.SBV.String (isInfixOf, singleton)+-- >>> import Data.SBV.List (isInfixOf) -- >>> import Prelude hiding(elem, notElem)+-- >>> :set -XOverloadedLists -- >>> :set -XOverloadedStrings+#endif  -- | Is the character in the string? -- -- >>> :set -XOverloadedStrings--- >>> prove $ \c -> c `elem` singleton c+-- >>> prove $ \c -> c `elem` [c] -- Q.E.D. -- >>> prove $ \c -> sNot (c `elem` "") -- Q.E.D.@@ -74,7 +78,7 @@  | Just cs <- unliteral s                            -- If only the second string is concrete, element-wise checking is still much better!  = sAny (c .==) $ map literal cs  | True- = singleton c `isInfixOf` s+ = [c] `SL.isInfixOf` s  -- | Is the character not in the string? --@@ -208,7 +212,7 @@ isPrintL1 :: SChar -> SBool isPrintL1 = liftPredL1 C.isPrint --- | Is this an ASCII digit, i.e., one of @0@..@9@. Note that this is a subset of 'isNumberL1' +-- | Is this an ASCII digit, i.e., one of @0@..@9@. Note that this is a subset of 'isNumberL1'. -- -- >>> prove $ \c -> isDigit c .=> isNumberL1 c -- Q.E.D.@@ -286,3 +290,26 @@ -- Q.E.D. isAsciiLower :: SChar -> SBool isAsciiLower = liftPredL1 C.isAsciiLower++-- | Symbolic enum instance for symbolic characters+instance EnumSymbolic Char where+   succ     = smtFunction "EnumSymbolic.Char.succ"   (\x -> ite (x .== maxBound) (some "EnumSymbolic.Char.succ_maxBound" (const sTrue)) (chr (ord x + 1)))+   pred     = smtFunction "EnumSymbolic.Char.pred"   (\x -> ite (x .== minBound) (some "EnumSymbolic.Char.pred_minBound" (const sTrue)) (chr (ord x - 1)))+   toEnum   = smtFunction "EnumSymbolic.Char.toEnum" (\x ->+                            ite (x .< ord (minBound :: SChar)) (some "EnumSymbolic.Char.toEnum.<minBound" (const sTrue))+                          $ ite (x .> ord (maxBound :: SChar)) (some "EnumSymbolic.Char.toEnum.>maxBound" (const sTrue))+                          $ chr x)++   fromEnum = ord++   enumFrom n   = SL.map chr (enumFromTo @Integer (ord n) (ord (maxBound @SChar)))+   enumFromThen = smtFunction "EnumSymbolic.Char.enumFromThen" $ \n1 n2 ->+                              let i_n1, i_n2 :: SInteger+                                  i_n1 = ord n1+                                  i_n2 = ord n2+                              in SL.map chr (ite (i_n2 .>= i_n1)+                                                 (enumFromThenTo i_n1 i_n2 (ord (maxBound @SChar)))+                                                 (enumFromThenTo i_n1 i_n2 (ord (minBound @SChar))))++   enumFromTo     n m   = SL.map chr (enumFromTo     @Integer (ord n) (ord m))+   enumFromThenTo n m t = SL.map chr (enumFromThenTo @Integer (ord n) (ord m) (ord t))

@@ -10,44 +10,71 @@ -----------------------------------------------------------------------------  {-# LANGUAGE CPP                 #-}+{-# LANGUAGE DeriveLift          #-}+{-# LANGUAGE LambdaCase          #-} {-# LANGUAGE PackageImports      #-}-{-# LANGUAGE QuasiQuotes         #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE StandaloneDeriving  #-} {-# LANGUAGE TemplateHaskell     #-}+{-# LANGUAGE TupleSections       #-} -{-# OPTIONS_GHC -Wall -Werror #-}+#if MIN_VERSION_template_haskell(2,22,1)+-- No need for newer versions of TH+#else+{-# LANGUAGE FlexibleInstances   #-}+#endif +{-# OPTIONS_GHC -Wall -Werror -Wno-orphans #-}+ module Data.SBV.Client   ( sbvCheckSolverInstallation   , defaultSolverConfig   , getAvailableSolvers-  , mkSymbolicEnumeration-  , mkUninterpretedSort+  , mkSymbolic+  , getConstructors   ) where -import Control.Monad (filterM)+import Data.SBV.Core.TH (getConstructors, bad, report)+ import Data.Generics +import Control.Monad (filterM, mapAndUnzipM, zipWithM)+import Data.Function (fix)+import Test.QuickCheck (Arbitrary(..), elements)+ import qualified Control.Exception as C +import Data.Char+import Data.Word+import Data.Int+import Data.Ratio+ import qualified "template-haskell" Language.Haskell.TH        as TH-#if MIN_VERSION_template_haskell(2,18,0) import qualified "template-haskell" Language.Haskell.TH.Syntax as TH-#endif +import Language.Haskell.TH.ExpandSyns as TH++import Data.SBV.Core.Concrete (cvRank) import Data.SBV.Core.Data import Data.SBV.Core.Model+import Data.SBV.Core.SizedFloats+import Data.SBV.Core.Symbolic (registerKind)+ import Data.SBV.Provers.Prover+import qualified Data.SBV.List as SL +import Data.List (genericLength)++import Data.SBV.TP.Kernel+ -- | Check whether the given solver is installed and is ready to go. This call does a -- simple call to the solver to ensure all is well. sbvCheckSolverInstallation :: SMTConfig -> IO Bool-sbvCheckSolverInstallation cfg = check `C.catch` (\(_ :: C.SomeException) -> return False)+sbvCheckSolverInstallation cfg = check `C.catch` (\(_ :: C.SomeException) -> pure False)   where check = do ThmResult r <- proveWith cfg $ \x -> sNot (sNot x) .== (x :: SBool)                    case r of-                     Unsatisfiable{} -> return True-                     _               -> return False+                     Unsatisfiable{} -> pure True+                     _               -> pure False  -- | The default configs corresponding to supported SMT solvers defaultSolverConfig :: Solver -> SMTConfig@@ -58,6 +85,7 @@ defaultSolverConfig CVC5      = cvc5 defaultSolverConfig DReal     = dReal defaultSolverConfig MathSAT   = mathSAT+defaultSolverConfig OpenSMT   = openSMT defaultSolverConfig Yices     = yices defaultSolverConfig Z3        = z3 @@ -65,111 +93,685 @@ getAvailableSolvers :: IO [SMTConfig] getAvailableSolvers = filterM sbvCheckSolverInstallation (map defaultSolverConfig [minBound .. maxBound]) --- | Turn a name into a symbolic type. If first argument is true, we'll also derive Eq and Ord instances.-declareSymbolic :: Bool -> TH.Name -> TH.Q [TH.Dec]-declareSymbolic isEnum typeName = do-    let typeCon = TH.conT typeName+#if MIN_VERSION_template_haskell(2,22,1)+-- Starting template haskell 2.22.1 the following instances are automatically provided+#else+deriving instance TH.Lift TH.OccName+deriving instance TH.Lift TH.NameSpace+deriving instance TH.Lift TH.PkgName+deriving instance TH.Lift TH.ModName+deriving instance TH.Lift TH.NameFlavour+deriving instance TH.Lift TH.Name+deriving instance TH.Lift TH.Type+deriving instance TH.Lift TH.Specificity+deriving instance TH.Lift (TH.TyVarBndr TH.Specificity)+deriving instance TH.Lift (TH.TyVarBndr ())+deriving instance TH.Lift TH.TyLit+#endif -    cstrs <- if isEnum then ensureEnumeration typeName-                       else ensureEmptyData   typeName+-- A few other things we need to TH lift+deriving instance TH.Lift Kind -    deriveEqOrds <- if isEnum-                       then [d| deriving instance Eq       $typeCon-                                deriving instance Ord      $typeCon-                            |]-                       else pure []+data ADTKind = ADTUninterpreted -- Completely uninterpreted+             | ADTEnum          -- Enumeration+             | ADTFull          -- A full datatype -    derives <- [d| deriving instance Show     $typeCon-                   deriving instance Read     $typeCon-                   deriving instance Data     $typeCon-                   deriving instance SymVal   $typeCon-                   deriving instance HasKind  $typeCon-                   deriving instance SatModel $typeCon-               |]+-- | Create a mutually recursive group of ADTs.+mkSymbolic :: [TH.Name] -> TH.Q [TH.Dec]+mkSymbolic ts = concat <$> mapM mkSymbolicADT ts +-- | Create a symbolic ADT.+mkSymbolicADT :: TH.Name -> TH.Q [TH.Dec]+mkSymbolicADT typeName = do -    sType <- TH.conT ''SBV `TH.appT` typeCon+     (tKind, params, cstrs) <- dissect typeName+     ds <- mkADT tKind typeName params cstrs -    let declConstructor c = ((nm, bnm), [sig, def])-          where bnm  = TH.nameBase c-                nm   = TH.mkName $ 's' : bnm-                def  = TH.FunD nm [TH.Clause [] (TH.NormalB body) []]-                body = TH.AppE (TH.VarE 'literal) (TH.ConE c)-                sig  = TH.SigD nm sType+     -- declare an "undefiner" so we don't have stray names+     nm <- TH.newName $ "_undefiner_" ++ TH.nameBase typeName+     addDoc "Autogenerated definition to avoid unused-variable warnings from GHC." nm -        (constrNames, cdecls) = unzip (map declConstructor cstrs)+     -- undefiner must be careful in putting ascriptions+     aVar <- TH.newName "a"+     let undefine n+           | base == "sCase" ++ tbase = wrap 1   -- Needs an extra param+           | True                     = wrap 0+           where tbase  = TH.nameBase typeName+                 base   = TH.nameBase n+                 wrap c = foldl TH.AppTypeE (TH.VarE n) (replicate (c + length params) (TH.ConT ''Integer)) +         names     = [undefine n | TH.FunD n _ <- ds]+         body      = foldl TH.AppE (TH.VarE 'undefined)+                                   (names ++ [TH.SigE (TH.VarE 'undefined)+                                                      (foldl TH.AppT (TH.ConT (TH.mkName ('S' : TH.nameBase typeName)))+                                                                     (map (const (TH.ConT ''Integer)) params))])++         undefSig  = TH.SigD nm (TH.ForallT [] [] (TH.VarT aVar))+         undefBody = TH.FunD nm [TH.Clause [] (TH.NormalB body) []]++     pure $ ds ++ [undefSig, undefBody]++-- | Add document to a generated declaration for the declaration+addDeclDocs :: (TH.Name, String) -> [(TH.Name, String)] -> TH.Q ()+addDeclDocs (tnm, ts) cnms = do add True (tnm, ts)+                                mapM_  (add False) cnms+   where add True  (cnm, cs) = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc cnm) $ "Symbolic version of the type t'"        ++ cs ++ "'."+         add False (cnm, cs) = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc cnm) $ "Symbolic version of the constructor v'" ++ cs ++ "'."++-- | Add document to a generated function+addDoc :: String -> TH.Name -> TH.Q ()+addDoc what tnm = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc tnm) what++-- | Symbolic version of a type+mkSBV :: TH.Type -> TH.Type+mkSBV a = TH.ConT ''SBV `TH.AppT` a++-- | Saturate the type with its parameters+saturate :: TH.Type -> [TH.Name] -> TH.Type+saturate t ps = foldr (\p b -> TH.AppT b (TH.VarT p)) t (reverse ps)++-- | Create a symbolic ADT+mkADT ::  ADTKind                                       -- What kind of ADT are we generating?+       -> TH.Name                                       -- type name+       -> [TH.Name]                                     -- parameters+       -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -- constructors+       -> TH.Q [TH.Dec]                                 -- declarations+mkADT adtKind typeName params cstrs = do++    let typeCon = saturate (TH.ConT typeName) params+        sType   = mkSBV typeCon++        inSymValContext = TH.ForallT [] [TH.AppT (TH.ConT ''SymVal) (TH.VarT n) | n <- params]++        isEnum = case adtKind of+                  ADTUninterpreted -> False+                  ADTEnum          -> True+                  ADTFull          -> False++        -- Given Cstr f1 f2 f3, generate the clause:+        --     inp@(Cstr [f1, f2, f3]) = case sequenceA [unlitCV (literal f1), unlitCV (literal f2), unlitCV (literal f3)] of+        --                                 Just c  -> let k = kindOf inp+        --                                            in SBV $ SVal k (Left (CV k (CADT (Cstr, c))))+        --                                 Nothing -> sCstr (literal f1)+        --+        mkLitClause (n, fs) = do+           as  <- mapM (const (TH.newName "a")) fs+           inp <- TH.newName "inp"+           c   <- TH.newName "c"++           let app a b = [| $a (literal $b) |]++           TH.clause [TH.asP inp (TH.conP n (map TH.varP as))]+                     (TH.normalB+                           (TH.caseE [| sequenceA $(TH.listE [ [| unlitCV (literal $(TH.varE a)) |] | a <- as ]) |]+                                     [ TH.match [p|Just $(TH.varP c)|]+                                                (TH.normalB [| let k = kindOf $(TH.varE inp)+                                                               in SBV $ SVal k (Left (CV k (CADT (TH.nameBase n, $(TH.varE c)))))+                                                            |])+                                                []+                                     , TH.match [p|Nothing|]+                                                (TH.normalB (foldl app (TH.varE (TH.mkName ('s' : TH.nameBase n))) (map TH.varE as)))+                                                []+                                     ]))+                     []++    litFun <- case adtKind of+                ADTUninterpreted -> do noLit <- [| error $ unlines [ "Data.SBV: unexpected call to derived literal implementation"+                                                                   , "***"+                                                                   , "*** Type: " ++ show typeName+                                                                   , ""+                                                                   , "***Please report this as a bug!"+                                                                   ]+                                                |]+                                       pure $ TH.FunD 'literal [TH.Clause [TH.WildP] (TH.NormalB noLit) []]++                ADTEnum          -> TH.FunD 'literal <$> mapM mkLitClause cstrs+                ADTFull          -> TH.FunD 'literal <$> mapM mkLitClause cstrs++    fromCVFunName <- TH.newName ("cv2" ++ TH.nameBase typeName)+    addDoc ("Conversion from SMT values to " ++ TH.nameBase typeName ++ " values.") fromCVFunName++    let fromCVSig = TH.SigD fromCVFunName+                            (inSymValContext (foldr (TH.AppT . TH.AppT TH.ArrowT) typeCon+                                                    [TH.ConT ''String, TH.AppT TH.ListT (TH.ConT ''CV)]))++        fromCVCls :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q TH.Clause+        fromCVCls (nm, args) = do+            ns <- mapM (\(i, _) -> TH.newName ("a" ++ show i)) (zip [(1::Int)..] args)+            let pat = foldr ((\p acc -> TH.ConP '(:) [] [p, acc]) . TH.VarP) (TH.ConP '[] [] []) ns+            pure $ TH.Clause [TH.LitP (TH.StringL (TH.nameBase nm)), pat]+                             (TH.NormalB (foldl TH.AppE (TH.ConE nm)+                                                        [TH.AppE (TH.VarE 'fromCV) (TH.VarE n) | n <- ns]))+                             []++    catchAll <- do s <- TH.newName "s"+                   l <- TH.newName "l"+                   let errStr   = TH.LitE (TH.StringL ("fromCV " ++ TH.nameBase typeName ++ ": Unexpected constructor/arity: "))+                       tup      = TH.TupE [Just (TH.VarE s), Just (TH.AppE (TH.VarE 'length) (TH.VarE l))]+                       showCall = TH.AppE (TH.VarE 'show) tup+                       errMsg   = TH.InfixE (Just errStr) (TH.VarE '(++)) (Just showCall)+                   pure $ TH.Clause [TH.VarP s, TH.VarP l] (TH.NormalB (TH.AppE (TH.VarE 'error) errMsg)) []++    fromCVFun <- do clss <- mapM fromCVCls cstrs+                    pure $ TH.FunD fromCVFunName (clss ++ [catchAll])++    getFromCV <- [| let unexpected w = error $ "fromCV: " ++ show typeName ++ ": " ++ w+                        kindName (KADT n _ _) = n+                        kindName (KApp n _)   = n+                        kindName k            = unexpected $ "An ADT kind was expected, but got: " ++ show k+                    in \case CV k (CADT (c, kvs)) | kindName k == unmod typeName+                                                 -> $(TH.varE fromCVFunName) c (map (uncurry CV) kvs)+                             CV k e -> unexpected $ "Was expecting a CADT value, but got kind: " ++ show k ++ " (rank: " ++ show (cvRank e) ++ ")"+                 |]++    symCtx  <- TH.cxt [TH.appT (TH.conT ''SymVal) (TH.varT n) | n <- params]++    mmBound <- if isEnum+                  then let universe     = [TH.conE con | (con, _) <- cstrs]+                           (minb, maxb) = case (universe, reverse universe) of+                                             (x:_, y:_) -> (x, y)+                                             _          -> error $ "Impossible: Ran out of elements in determining bounds: " ++ show cstrs+                       in [| Just ($minb, $maxb) |]+                  else [| Nothing |]++    -- make the initializer to get the subtypes registered+    st <- TH.newName "_st"  -- Get an underscored name here, since st might go unused if there're no subtypes+    register <- do let concretize b@TH.ConT{}     = b+                       concretize TH.VarT{}       = TH.ConT ''Integer+                       concretize (TH.AppT l arg) = TH.AppT (concretize l) (concretize arg)+                       concretize r               = r++                   end <- TH.noBindS [| pure () |]+                   pure $ TH.DoE Nothing $ [TH.NoBindS (TH.AppE (TH.AppE (TH.VarE 'registerKind) (TH.VarE st))+                                                                (TH.AppE (TH.VarE 'kindOf)+                                                                         (TH.AppTypeE (TH.ConE 'Proxy) (concretize t))))+                                           | (_, fts) <- cstrs, (_, t, KApp n _) <- fts, n /= TH.nameBase typeName+                                           ] ++ [end]++    let regFun = TH.FunD 'mkSymValInit [TH.Clause [TH.VarP st, TH.WildP] (TH.NormalB register) []]++    let symVal = TH.InstanceD+                      Nothing+                      symCtx+                      (TH.AppT (TH.ConT ''SymVal) typeCon)+                      [ litFun+                      , regFun+                      , TH.FunD 'minMaxBound [TH.Clause [] (TH.NormalB mmBound)   []]+                      , TH.FunD 'fromCV      [TH.Clause [] (TH.NormalB getFromCV) []]+                       ]++    defCstrs <- [| [(unmod n, map (\(_, _, t) -> t) ntks) | (n, ntks) <- cstrs] |]++    kindCtx <- TH.cxt [TH.appT (TH.conT ''HasKind) (TH.varT p) | p <- params]++    let mkPair a b = TH.TupE [Just a, Just b]+        kindDef = foldl1 TH.AppE [ TH.ConE 'KADT+                                 , TH.LitE (TH.StringL (unmod typeName))+                                 , TH.ListE [ mkPair (TH.LitE (TH.StringL (TH.nameBase p)))+                                                     (TH.AppE (TH.VarE 'kindOf) (TH.AppTypeE (TH.ConE 'Proxy) (TH.VarT p)))+                                            | p <- params+                                            ]+                                 , defCstrs+                                 ]++        kindDecl = TH.InstanceD+                        Nothing+                        kindCtx+                        (TH.AppT (TH.ConT ''HasKind) typeCon)+                        [TH.FunD 'kindOf [TH.Clause [TH.WildP] (TH.NormalB kindDef) []]]++    hasArbitrary <- TH.isInstance ''Arbitrary [typeCon]+    arbDecl <- case () of+                () | hasArbitrary -> pure []+                   | isEnum       -> let universe  = TH.listE [TH.conE con | (con, _) <- cstrs]+                                     in [d|instance Arbitrary $(pure typeCon) where+                                             arbitrary = elements $universe+                                        |]+                   | True         -> [d|instance {-# OVERLAPPABLE #-} Arbitrary $(pure typeCon) where+                                          arbitrary = error $ unlines [ ""+                                                                      , "*** Data.SBV: Cannot quickcheck the given property."+                                                                      , "***"+                                                                      , "*** Default arbitrary instance for " ++ TH.nameBase typeName ++ " is too limited."+                                                                      , "***"+                                                                      , "*** You can overcome this by giving your own Arbitrary instance."+                                                                      , "*** Please get in touch if this workaround is not suitable for your case."+                                                                      ]+                                    |]++    -- Declare constructors+    let declConstructor :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q ((TH.Name, String), [TH.Dec])+        declConstructor (n, ntks) = do+            let ats = map (mkSBV . (\(_, t, _) -> t)) ntks+                ty  = inSymValContext $ foldr (TH.AppT . TH.AppT TH.ArrowT) sType ats+                bnm = TH.nameBase n+                nm  = TH.mkName $ 's' : bnm++            as    <- mapM (const (TH.newName "a")) ntks+            c     <- TH.newName "c"++            cls <- TH.clause (map TH.varP as)+                             (TH.normalB+                                   (TH.caseE [| sequenceA $(TH.listE [ [| unlitCV $(TH.varE a) |] | a <- as ]) |]+                                             [ TH.match [p|Just $(TH.varP c)|]+                                                        -- We need the kind of the result type to build the value, but the+                                                        -- result type can only be recovered from the (signature-pinned) result+                                                        -- itself: a parametric type may carry the parameter in a phantom+                                                        -- position (e.g. the @a@ in @Right :: b -> Either a b@) that no argument+                                                        -- mentions. We tie the kind to the result via 'fix'. Crucially, 'fix'+                                                        -- binds @res@ as a /lambda-bound/ variable, which is always monomorphic;+                                                        -- a plain @let@ group would be generalized when the monomorphism+                                                        -- restriction is off (as it is at the GHCi prompt), yielding a spurious+                                                        -- ambiguous @HasKind@. ('kindOf' ignores its argument, so 'fix' is safe.)+                                                        (TH.normalB [| fix (\res -> let k = kindOf res+                                                                                    in SBV $ SVal k (Left (CV k (CADT (bnm, $(TH.varE c)))))) |])+                                                        []+                                             , TH.match [p|Nothing|]+                                                        (TH.normalB (foldl (\a b -> [| $a $b |]) [| mkADTConstructor bnm |] (map TH.varE as)))+                                                        []+                                             ]))+                             []++            pure ((nm, bnm), [TH.SigD nm ty, TH.FunD nm [cls]])++    (constrNames, cdecls) <- mapAndUnzipM declConstructor cstrs+     let btname = TH.nameBase typeName         tname  = TH.mkName ('S' : btname)-        tdecl  = TH.TySynD tname [] sType+        tdecl  = TH.TySynD tname [TH.PlainTV p TH.BndrReq | p <- params] sType -    addDocs (tname, btname) constrNames+    addDeclDocs (tname, btname) constrNames -    pure $ deriveEqOrds ++ derives ++ [tdecl] ++ concat cdecls+    -- Declare accessors+    let -- NB. field count starts at 1!+        declAccessor :: TH.Name -> (Maybe TH.Name, TH.Type, Kind) -> Int -> TH.Q [((TH.Name, String), [TH.Dec])]+        declAccessor c (mbUN, ft, _) i = do+                let bnm  = TH.nameBase c+                    anm  = "get" ++ bnm ++ "_" ++ show i+                    nm   = TH.mkName anm+                    ty    = inSymValContext $ TH.AppT (TH.AppT TH.ArrowT sType) (mkSBV ft) - where addDocs :: (TH.Name, String) -> [(TH.Name, String)] -> TH.Q ()-#if MIN_VERSION_template_haskell(2,18,0)-       addDocs (tnm, ts) cnms = do addDoc True (tnm, ts)-                                   mapM_  (addDoc False) cnms-          where addDoc True  (cnm, cs) = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc cnm) $ "Symbolic version of the type '"        ++ cs ++ "'."-                addDoc False (cnm, cs) = TH.addModFinalizer $ TH.putDoc (TH.DeclDoc cnm) $ "Symbolic version of the constructor '" ++ cs ++ "'."-#else-       addDocs _ _ = pure ()-#endif+                cls <- do inp <- TH.newName "inp"+                          TH.clause [TH.varP inp]+                                    (TH.normalB+                                          (TH.caseE [| unlitCV $(TH.varE inp) |]+                                                    [ TH.match [p|Just (_, CADT (got, kv))|]+                                                               (TH.guardedB [do g <- TH.normalG [| got == bnm |]+                                                                                e <- [| let (k, v) = (kv !! (i-1))+                                                                                        in SBV $ SVal k (Left (CV k v))+                                                                                     |]+                                                                                pure (g, e)+                                                                            ])+                                                               []+                                                    , TH.match [p|_|]+                                                               (TH.normalB [| mkADTAccessor anm $(TH.varE inp) |])+                                                               []+                                                    ]))+                                    [] --- | Make an enumeration a symbolic type.-mkSymbolicEnumeration :: TH.Name -> TH.Q [TH.Dec]-mkSymbolicEnumeration = declareSymbolic True+                -- If there's a custom accessor given, declare that here too+                extras <- case mbUN of+                            Nothing -> pure []+                            Just un -> do let sun = TH.mkName $ 's' : TH.nameBase un+                                          pure [((sun, bnm), [TH.SigD sun ty, TH.FunD sun [cls]])] --- | Make an uninterpred sort.-mkUninterpretedSort :: TH.Name -> TH.Q [TH.Dec]-mkUninterpretedSort = declareSymbolic False+                pure $ ((nm, bnm), [TH.SigD nm ty, TH.FunD nm [cls]]) : extras --- | Make sure the given type is an enumeration-ensureEnumeration :: TH.Name -> TH.Q [TH.Name]-ensureEnumeration nm = do-        c <- TH.reify nm-        case c of-          TH.TyConI d -> case d of-                           TH.DataD _ _ _ _ cons _ -> case cons of-                                                        [] -> bad "The datatype given has no constructors."-                                                        xs -> concat <$> mapM check xs-                           _                       -> bad "The name given is not a datatype."+    allDefs <- sequence [zipWithM (declAccessor c) fs [(1::Int) ..] | (c, fs) <- cstrs]+    let (accessorNames, accessorDecls) = unzip $ concat (concat allDefs) -          _        -> bad "The name given is not a datatype."- where n = TH.nameBase nm+    mapM_ (addDoc "Field accessor function." . fst) accessorNames -       check (TH.NormalC c xs) = case xs of-                                   [] -> pure [c]-                                   _  -> bad $ "Constructor " ++ show c ++ " has arguments."+    testerDecls <- mkTesters sType inSymValContext cstrs -       check c                 = bad $ "Constructor " ++ show c ++ " is not an enumeration value."+    -- Get the case analyzer+    caseSigFuns <- mkCaseAnalyzer adtKind typeName params cstrs -       bad m = do TH.reportError $ unlines [ "Data.SBV.mkSymbolicEnumeration: Invalid argument " ++ show n-                                           , ""-                                           , "    Expected an enumeration. " ++ m-                                           , ""-                                           , "    To create an enumerated sort, use a simple Haskell enumerated type."-                                           ]-                  pure []+    -- Get the induction schema, upto 5 extra args. Only for enums and adts+    indDecs <- do let schemas = mapM (mkInductionSchema typeName params cstrs) [0 .. 5]+                  case adtKind of+                    ADTUninterpreted -> pure []+                    ADTEnum          -> schemas+                    ADTFull          -> schemas --- | Make sure the given type is an empty data-ensureEmptyData :: TH.Name -> TH.Q [TH.Name]-ensureEmptyData nm = do-        c <- TH.reify nm-        case c of-          TH.TyConI d -> case d of-                           TH.DataD _ _ _ _ cons _ -> case cons of-                                                        [] -> pure []-                                                        _  -> bad "The datatype given has constructors."-                           _                       -> bad "The name given is not a datatype."+    -- If this is an enumeration get EnumSymbolic and OrSymbolic instances+    symEnum <- case adtKind of+                ADTUninterpreted -> pure []+                ADTFull          -> pure []+                ADTEnum          ->+                  let universe  = TH.listE [TH.conE                          con   | (con, _) <- cstrs]+                      universeS = TH.listE [TH.litE (TH.stringL (TH.nameBase con)) | (con, _) <- cstrs]+                  in [d| instance SatModel $(TH.conT typeName) where+                           parseCVs (CV _ (CADT (s, [])) : r)+                             | Just v <- s `lookup` zip $universeS $universe+                             = Just (v, r)+                           parseCVs _ = Nothing -          _        -> bad "The name given is not a datatype."- where n = TH.nameBase nm-       bad m = do TH.reportError $ unlines [ "Data.SBV.mkUninterpretedSort: Invalid argument " ++ show n-                                           , ""-                                           , "    Expected an empty datatype. " ++ m-                                           , ""-                                           , "    To create an uninterpreted sort, use an empty datatype declaration."-                                           ]-                  pure []+                         instance SL.EnumSymbolic $(TH.conT typeName) where+                           succ x = go (zip $universe (drop 1 $universe))+                             where go []              = some ("succ_" ++ show typeName ++ "_maximal") (const sTrue)+                                   go ((c, s) : rest) = ite (x .== literal c) (literal s) (go rest)++                           pred x = go (zip (drop 1 $universe) $universe)+                             where go []              = some ("pred_" ++ show typeName ++ "_minimal") (const sTrue)+                                   go ((c, s) : rest) = ite (x .== literal c) (literal s) (go rest)++                           toEnum x = go (zip $universe [0..])+                             where go []              = some ("toEnum_" ++ show typeName ++ "_out_of_range") (const sTrue)+                                   go ((c, i) : rest) = ite (x .== literal i) (literal c) (go rest)++                           fromEnum x = go 0 $universe+                             where go _ []     = error "fromEnum: Impossible happened, ran out of elements."+                                   go i [_]    = i+                                   go i (c:cs) = ite (x .== literal c) i (go (i+1) cs)++                           enumFrom n = SL.map SL.toEnum (SL.enumFromTo (SL.fromEnum n) (genericLength $universe - 1))++                           enumFromThen = smtFunction ("EnumSymbolic." ++ TH.nameBase typeName ++ ".enumFromThen") $ \n1 n2 ->+                                                      let i_n1, i_n2 :: SInteger+                                                          i_n1 = SL.fromEnum n1+                                                          i_n2 = SL.fromEnum n2+                                                      in SL.map SL.toEnum (ite (i_n2 .>= i_n1)+                                                                               (SL.enumFromThenTo i_n1 i_n2 (genericLength $universe - 1))+                                                                               (SL.enumFromThenTo i_n1 i_n2 0))++                           enumFromTo     n m   = SL.map SL.toEnum (SL.enumFromTo     (SL.fromEnum n) (SL.fromEnum m))++                           enumFromThenTo n m t = SL.map SL.toEnum (SL.enumFromThenTo (SL.fromEnum n) (SL.fromEnum m) (SL.fromEnum t))++                         instance OrdSymbolic (SBV $(TH.conT typeName)) where+                           a .<  b = SL.fromEnum a .<  SL.fromEnum b+                           a .<= b = SL.fromEnum a .<= SL.fromEnum b+                           a .>  b = SL.fromEnum a .>  SL.fromEnum b+                           a .>= b = SL.fromEnum a .>= SL.fromEnum b+                     |]++    pure $  [tdecl, symVal, kindDecl]+         ++ arbDecl+         ++ concat cdecls+         ++ testerDecls+         ++ concat accessorDecls+         ++ symEnum+         ++ [fromCVSig, fromCVFun]+         ++ caseSigFuns+         ++ concat indDecs++-- | Make a case analyzer for the type. Works for ADTs and enums. Returns sig and defn+mkCaseAnalyzer :: ADTKind -> TH.Name -> [TH.Name] -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -> TH.Q [TH.Dec]+mkCaseAnalyzer kind typeName params cstrs = case kind of+                                              ADTUninterpreted -> pure [] -- no case analyzer for fully uninterpreted types+                                              ADTEnum          -> mk+                                              ADTFull          -> mk+  where mk = do let typeCon = saturate (TH.ConT typeName) params+                    sType   = mkSBV typeCon++                    bnm = TH.nameBase typeName+                    cnm = TH.mkName $ "sCase" ++ bnm++                se   <- TH.newName ('s' : bnm)+                fs   <- mapM (\(nm, _) -> TH.newName ('f' : TH.nameBase nm)) cstrs+                res  <- TH.newName "result"++                let def = TH.FunD cnm [TH.Clause (map TH.VarP (fs ++ [se])) (TH.NormalB (iteChain (zipWith (mkCase se) fs cstrs))) []]++                    iteChain :: [(TH.Exp, TH.Exp)] -> TH.Exp+                    iteChain []       = error $ unlines [ "Data.SBV.mkADT: Impossible happened!"+                                                        , ""+                                                        , "   Received an empty list for: " ++ show typeName+                                                        , ""+                                                        , "While building the case-analyzer."+                                                        , "Please report this as a bug."+                                                        ]+                    iteChain [(_, l)]        = l+                    iteChain ((t, e) : rest) = foldl TH.AppE (TH.VarE 'ite) [TH.AppE t (TH.VarE se), e, iteChain rest]++                    mkCase :: TH.Name -> TH.Name -> (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> (TH.Exp, TH.Exp)+                    mkCase cexpr func (c, fields) = (TH.VarE (TH.mkName ("is" ++ TH.nameBase c)), foldl TH.AppE (TH.VarE func) args)+                       where getters = [TH.mkName ("get" ++ TH.nameBase c ++ "_" ++ show i) | (i, _) <- zip [(1 :: Int) ..] fields]+                             args    = map (\g -> TH.AppE (TH.VarE g) (TH.VarE cexpr)) getters++                    rvar   = TH.VarT res+                    mkFun  = foldr (TH.AppT . TH.AppT TH.ArrowT) rvar+                    fTypes = [mkFun (map (mkSBV . (\(_, t, _) -> t)) ftks) | (_, ftks) <- cstrs]+                    sig    = TH.SigD cnm (TH.ForallT []+                                                     (TH.AppT (TH.ConT ''Mergeable) (TH.VarT res)+                                                     : [TH.AppT (TH.ConT ''SymVal) (TH.VarT p) | p <- params]+                                                     )+                                                     (mkFun (fTypes ++ [sType])))++                addDoc ("Case analyzer for the type " ++ bnm ++ ".") cnm+                pure [sig, def]++-- | Declare testers+mkTesters :: TH.Type -> (TH.Type -> TH.Type) -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -> TH.Q [TH.Dec]+mkTesters sType inSymValContext cstrs = do+    let declTester :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q ((TH.Name, String), [TH.Dec])+        declTester (c, _) = do+             let ty  = inSymValContext $ TH.AppT (TH.AppT TH.ArrowT sType) (TH.ConT ''SBool)+                 bnm = TH.nameBase c+                 nm  = TH.mkName $ "is" ++ bnm++             inp <- TH.newName "inp"+             cls <- TH.clause [TH.varP inp]+                              (TH.normalB+                                    (TH.caseE [| unlitCV $(TH.varE inp) |]+                                              [ TH.match [p|Just (_, CADT (got, _))|]+                                                         (TH.normalB [| literal (got == bnm) |])+                                                         []+                                              , TH.match [p|Nothing|]+                                                         (TH.normalB [| mkADTTester ("is-" ++ bnm) $(TH.varE inp) |])+                                                         []+                                              ]))+                              []+             pure ((nm, bnm), [TH.SigD nm ty, TH.FunD nm [cls]])++    (testerNames, testerDecls) <- mapAndUnzipM declTester cstrs++    mapM_ (addDoc "Field recognizer predicate." . fst) testerNames++    pure $ concat testerDecls++-- We'll just drop the modules to keep this simple+-- If you use multiple expressions named the same (coming from different modules), oh well.+unmod :: TH.Name -> String+unmod = reverse . takeWhile (/= '.') . reverse . show++-- | Given a type name, determine what kind of a data-type it is.+dissect :: TH.Name -> TH.Q (ADTKind, [TH.Name], [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])])+dissect typeName = do+        (args, tcs) <- getConstructors typeName++        let mk n (mbfn, t) = do k <- expandSyns t >>= toSBV typeName n+                                pure (mbfn, t, k)++        cs <- mapM (\(n, ts) -> (n,) <$> mapM (mk n) ts) tcs++        let k | null cs             = ADTUninterpreted+              | all (null . snd) cs = ADTEnum+              | True                = ADTFull++        pure (k, args, cs)++-- | Find the SBV kind for this type+toSBV :: TH.Name -> TH.Name -> TH.Type -> TH.Q Kind+toSBV typeName constructorName = go+  where hasArrows (TH.AppT TH.ArrowT _)   = True+        hasArrows (TH.AppT lhs       rhs) = hasArrows lhs || hasArrows rhs+        hasArrows _                       = False++        -- Handle type variables (parameters)+        go (TH.VarT v) = pure $ KVar (TH.nameBase v)++        -- tuples+        go t | Just ps <- getTuple t = KTuple <$> mapM go ps++        -- recognize strings, since we don't (yet) support chars+        go (TH.AppT TH.ListT (TH.ConT t)) | t == ''Char = pure KString++        -- lists+        go (TH.AppT TH.ListT t) = KList <$> go t++        -- arbitrary words/ints+        go (TH.AppT (TH.ConT nm) (TH.LitT (TH.NumTyLit n)))+            | nm == ''WordN = pure $ KBounded False (fromIntegral n)+            | nm == ''IntN  = pure $ KBounded True  (fromIntegral n)++        -- arbitrary floats+        go (TH.AppT (TH.AppT (TH.ConT nm) (TH.LitT (TH.NumTyLit eb))) (TH.LitT (TH.NumTyLit sb)))+            | nm == ''FloatingPoint = pure $ KFP (fromIntegral eb) (fromIntegral sb)++        -- Rational+        go (TH.AppT (TH.ConT nm) (TH.ConT i))+            | nm == ''Ratio && i == ''Integer+            = pure KRational++        -- deal with base types+        go t@(TH.ConT constr)+            | Just base <- getBase constr+            = case base of+                Left (w, r) -> bad w $ [ "Datatype   : " ++ show typeName+                                       , "Constructor: " ++ show constructorName+                                       , "Kind       : " ++ TH.pprint t+                                       , ""+                                       ] ++ r+                Right k     -> pure k++        -- deal with constructors+        go t+           | Just (c, ps) <- getConApp t+           = KApp (TH.nameBase c) <$> mapM go ps++        -- giving up+        go t = bad "Unsupported constructor kind" [ "Datatype   : " ++ TH.nameBase typeName+                                                  , "Constructor: " ++ TH.nameBase constructorName+                                                  , "Kind       : " ++ TH.pprint t+                                                  , ""+                                                  , if hasArrows t+                                                    then "Higher order fields (i.e., function values) are not supported."+                                                    else report+                                                  ]++        -- Extract application of a constructor to some type-variables+        getConApp t = locate t []+          where locate (TH.ConT c)     sofar = Just (c, sofar)+                locate (TH.AppT l arg) sofar = locate l (arg : sofar)+                locate _               _     = Nothing++        -- Extract an N-tuple+        getTuple = tup []+          where tup sofar (TH.TupleT _) = Just sofar+                tup sofar (TH.AppT t p) = tup (p : sofar) t+                tup _     _             = Nothing++        -- Given the name of a base type, what's the equivalent in the SBV domain (if we have it)+        getBase :: TH.Name -> Maybe (Either (String, [String]) Kind)+        getBase t+          | t == ''Bool     = Just $ Right KBool+          | t == ''Integer  = Just $ Right KUnbounded+          | t == ''Float    = Just $ Right KFloat+          | t == ''Double   = Just $ Right KDouble+          | t == ''Char     = Just $ Right KChar+          | t == ''String   = Just $ Right KString+          | t == ''AlgReal  = Just $ Right KReal+          | t == ''Rational = Just $ Right KRational+          | t == ''Word8    = Just $ Right $ KBounded False  8+          | t == ''Word16   = Just $ Right $ KBounded False 16+          | t == ''Word32   = Just $ Right $ KBounded False 32+          | t == ''Word64   = Just $ Right $ KBounded False 64+          | t == ''Int8     = Just $ Right $ KBounded True   8+          | t == ''Int16    = Just $ Right $ KBounded True  16+          | t == ''Int32    = Just $ Right $ KBounded True  32+          | t == ''Int64    = Just $ Right $ KBounded True  64++          -- Platform specific, flag:+          |    t == ''Int+            || t == ''Word  = Just $ Left ( "Platform specific type: " ++ show t+                                          , [ "Please pick a more specific type, such as"+                                            , "Integer, Word8, WordN 32, IntN 16 etc."+                                            ])++          -- Otherwise, can't translate+          | True            = Nothing++-- | Make an induction schema for the type, with n extra arguments.+mkInductionSchema :: TH.Name -> [TH.Name] -> [(TH.Name, [(Maybe TH.Name, TH.Type, Kind)])] -> Int -> TH.Q [TH.Dec]+mkInductionSchema typeName params cstrs extraArgCnt = do+   let btype = TH.nameBase typeName+       nm    = "induct" ++ btype ++ if extraArgCnt == 0 then "" else show extraArgCnt++   pf <- TH.newName "pf"++   extraNames <- mapM (const (TH.newName "extraN")) [0 .. extraArgCnt-1]+   extraSyms  <- mapM (const (TH.newName "extraS")) [0 .. extraArgCnt-1]+   extraTypes <- mapM (const (TH.newName "extraT")) [0 .. extraArgCnt-1]++   let mkLam = TH.lamE . map (\a -> TH.conP 'Forall [TH.varP a])++   let mkIndCase :: (TH.Name, [(Maybe TH.Name, TH.Type, Kind)]) -> TH.Q TH.Exp+       mkIndCase (cstr, flds)+         | null flds && null extraNames+         = [| $(TH.varE pf) $(scstr) |]+         | True+         = do as <- mapM (const (TH.newName "a")) flds+              let -- When can we have the inductive hypothesis?+                  --  (1) same type+                  --  (2) applied at exactly the same types+                  isRecursive (_, _, k) = case k of+                                            KApp t ps -> t == btype && ps == map (KVar . TH.nameBase) params+                                            _         -> False+                  recFields = [a | (a, f) <- zip as flds, isRecursive f]++              TH.appE (TH.varE 'quantifiedBool)+                      (mkLam (as ++ extraNames)+                             (mkImp recFields (foldl TH.appE+                                                     (TH.appE (TH.varE pf) (foldl TH.appE scstr (map TH.varE as)))+                                                     (map TH.varE extraNames))))+         where cnm   = TH.nameBase cstr+               lcnm  = map toLower cnm+               scstr = TH.varE (TH.mkName ('s' : cnm))++               mkImp []  e = e+               mkImp [i] e = foldl1 TH.appE [TH.varE '(.=>), assume i, e]+               mkImp is  e = foldl1 TH.appE [TH.varE '(.=>), foldl1 TH.appE [TH.varE 'sAnd, TH.listE (map assume is)], e]++               assume :: TH.Name -> TH.Q TH.Exp+               assume n = do en <- mapM (const (TH.newName (lcnm ++ "_extraN"))) [0 .. extraArgCnt-1]+                             TH.appE (TH.varE 'quantifiedBool)+                                     (mkLam en (foldl TH.appE (TH.varE pf) (map TH.varE (n : en))))++   cases <- mapM mkIndCase cstrs+   post  <- do a <- TH.newName "recVal"+               TH.appE (TH.varE 'quantifiedBool)+                       (mkLam (a : extraNames) $ foldl TH.appE (TH.varE pf) (map TH.varE (a : extraNames)))++   propName <- TH.newName "prop"+   argName  <- TH.newName "a"+   taName   <- TH.newName "ta"++   let pre    = foldl1 TH.AppE [TH.VarE 'sAnd,  TH.ListE cases]+       schema = foldl1 TH.AppE [TH.VarE '(.=>), pre, post]+       ihB    = TH.AppE (TH.VarE 'proofOf) (foldl1 TH.AppE [TH.VarE 'internalAxiom, TH.LitE (TH.StringL nm), schema])++       instHead = TH.AppT (TH.ConT ''HasInductionSchema)+                          (foldr (TH.AppT . TH.AppT TH.ArrowT)+                                 (TH.ConT ''SBool)+                                 [  TH.AppT (TH.ConT ''Forall) (TH.VarT es) `TH.AppT` et+                                  | (es, et) <- zip (taName : extraSyms)+                                                    (saturate (TH.ConT typeName) params : map TH.VarT extraTypes)+                                 ])++       pfFun = TH.FunD pf [TH.Clause (map TH.VarP (argName : extraNames))+                                     (TH.NormalB (foldl TH.AppE+                                                        (TH.VarE propName)+                                                        [TH.AppE (TH.ConE 'Forall) (TH.VarE a) | a <- argName : extraNames]))+                                     []+                          ]++       method = TH.FunD 'inductionSchema+                        [TH.Clause [TH.VarP propName]+                                   (TH.NormalB (TH.LetE [pfFun] ihB))+                                   []+                        ]++   context <- TH.cxt [TH.appT (TH.conT ''SymVal) (TH.varT n) | n <- params ++ extraTypes]++   pure [TH.InstanceD Nothing context instHead [method]]

@@ -11,106 +11,37 @@ -- @Data.SBV@, where we restrict the underlying monad to be IO. ----------------------------------------------------------------------------- -{-# LANGUAGE DataKinds            #-}-{-# LANGUAGE DefaultSignatures    #-}-{-# LANGUAGE FlexibleContexts     #-}-{-# LANGUAGE FlexibleInstances    #-}-{-# LANGUAGE TypeFamilies         #-}-{-# LANGUAGE TypeOperators        #-}-{-# LANGUAGE UndecidableInstances #-}+{-# LANGUAGE FlexibleContexts #-}+{-# LANGUAGE NamedFieldPuns   #-}  {-# OPTIONS_GHC -Wall -Werror #-}  module Data.SBV.Client.BaseIO where -import Data.SBV.Core.Data      (HasKind, Kind, Outputtable, Penalty, SymArray,-                                SymVal, SBool, SBV, SChar, SDouble, SFloat,+import Data.SBV.Core.Data      (Kind, Outputtable, Penalty,+                                SymVal, SBool, SBV, SChar, SDouble, SFloat, SWord, SInt,                                 SFPHalf, SFPBFloat, SFPSingle, SFPDouble, SFPQuad, SFloatingPoint,                                 SInt8, SInt16, SInt32, SInt64, SInteger, SList,                                 SReal, SString, SV, SWord8, SWord16, SWord32,-                                SWord64, SEither, SRational, SMaybe, SSet)-import Data.SBV.Core.Sized     (SInt, SWord, IntN, WordN)+                                SWord64, SRational, SSet, SArray, constrain, (.==)) import Data.SBV.Core.Kind      (BVIsNonZero, ValidFloat) import Data.SBV.Core.Model     (Metric(..), SymTuple)-import Data.SBV.Core.Symbolic  (Objective, OptimizeStyle, Result, VarContext,-                                Symbolic, SBVRunMode, SMTConfig, SVal)+import Data.SBV.Core.Symbolic  (Objective, OptimizeStyle, Result, VarContext, Symbolic, SBVRunMode, SMTConfig,+                                SVal, symbolicEnv, rPartitionVars, State(..)) import Data.SBV.Control.Types  (SMTOption)-import Data.SBV.Provers.Prover (Provable, SExecutable, ThmResult)-import Data.SBV.SMT.SMT        (AllSatResult, SafeResult, SatResult,-                                OptimizeResult)+import Data.SBV.Provers.Prover (Provable, Satisfiable, SExecutable, ThmResult)+import Data.SBV.SMT.SMT        (AllSatResult, SafeResult, SatResult, OptimizeResult) -import GHC.TypeLits-import Data.Kind+import GHC.TypeLits (KnownNat) -import Data.Int-import Data.Word+import Data.IORef(readIORef, modifyIORef')  import qualified Data.SBV.Core.Data      as Trans-import qualified Data.SBV.Core.Sized     as Trans import qualified Data.SBV.Core.Model     as Trans import qualified Data.SBV.Core.Symbolic  as Trans import qualified Data.SBV.Provers.Prover as Trans --- Data.SBV.Provers.Prover:---- | Turns a value into a universally quantified predicate, internally naming the inputs.--- In this case the sbv library will use names of the form @s1, s2@, etc. to name these variables--- Example:------ >  universal_ $ \(x::SWord8) y -> x `shiftL` 2 .== y------ is a predicate with two arguments, captured using an ordinary Haskell function. Internally,--- @x@ will be named @s0@ and @y@ will be named @s1@.------ Remember that SBV assumes that the input is in prenex-normal form.--- That is, all quantifiers are at the beginning of the predicate. See--- [note on reasoning in the presence of--- quantifiers]("Data.SBV#noteOnNested") for more information.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.universal_'-universal_ :: Provable a => a -> Symbolic SBool-universal_ = Trans.universal_---- | Turns a value into a predicate, allowing users to provide names for the inputs.--- If the user does not provide enough number of names for the variables, the remaining ones--- will be internally generated. Note that the names are only used for printing models and has no--- other significance; in particular, we do not check that they are unique. Example:------ >  universal ["x", "y"] $ \(x::SWord8) y -> x `shiftL` 2 .== y------ This is the same as above, except the variables will be named @x@ and @y@ respectively,--- simplifying the counter-examples when they are printed.------ Remember that SBV assumes that the input is in prenex-normal form.--- That is, all quantifiers are at the beginning of the predicate. See--- [note on reasoning in the presence of--- quantifiers]("Data.SBV#noteOnNested") for more information.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.universal'-universal :: Provable a => [String] -> a -> Symbolic SBool-universal = Trans.universal---- | Turns a value into an existentially quantified predicate.------ Remember that SBV assumes that the input is in prenex-normal form.--- That is, all quantifiers are at the beginning of the predicate. See--- [note on reasoning in the presence of--- quantifiers]("Data.SBV#noteOnNested") for more information.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.existential_'-existential_ :: Provable a => a -> Symbolic SBool-existential_ = Trans.existential_---- | Version of 'existential_' that allows user defined names.------ Remember that SBV assumes that the input is in prenex-normal form.--- That is, all quantifiers are at the beginning of the predicate. See--- [note on reasoning in the presence of--- quantifiers]("Data.SBV#noteOnNested") for more information.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.existential'-existential :: Provable a => [String] -> a -> Symbolic SBool-existential = Trans.existential+import Control.Monad.Trans (liftIO)  -- | Prove a predicate, using the default solver. --@@ -139,32 +70,32 @@ -- | Find a satisfying assignment for a predicate, using the default solver. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sat'-sat :: Provable a => a -> IO SatResult+sat :: Satisfiable a => a -> IO SatResult sat = Trans.sat  -- | Find a satisfying assignment using the given SMT-solver. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.satWith'-satWith :: Provable a => SMTConfig -> a -> IO SatResult+satWith :: Satisfiable a => SMTConfig -> a -> IO SatResult satWith = Trans.satWith  -- | Find a delta-satisfying assignment for a predicate, using the default solver for delta-satisfiability. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.dsat'-dsat :: Provable a => a -> IO SatResult+dsat :: Satisfiable a => a -> IO SatResult dsat = Trans.dsat  -- | Find a satisfying assignment using the given SMT-solver. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.satWith'-dsatWith :: Provable a => SMTConfig -> a -> IO SatResult+dsatWith :: Satisfiable a => SMTConfig -> a -> IO SatResult dsatWith = Trans.dsatWith  -- | Find all satisfying assignments, using the default solver. -- Equivalent to @'allSatWith' 'Data.SBV.defaultSMTCfg'@. See 'allSatWith' for details. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.allSat'-allSat :: Provable a => a -> IO AllSatResult+allSat :: Satisfiable a => a -> IO AllSatResult allSat = Trans.allSat  -- | Return all satisfying assignments for a predicate.@@ -180,32 +111,32 @@ --  Find all satisfying assignments using the given SMT-solver -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.allSatWith'-allSatWith :: Provable a => SMTConfig -> a -> IO AllSatResult+allSatWith :: Satisfiable a => SMTConfig -> a -> IO AllSatResult allSatWith = Trans.allSatWith  -- | Optimize a given collection of `Objective`s. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.optimize'-optimize :: Provable a => OptimizeStyle -> a -> IO OptimizeResult+optimize :: Satisfiable a => OptimizeStyle -> a -> IO OptimizeResult optimize = Trans.optimize  -- | Optimizes the objectives using the given SMT-solver. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.optimizeWith'-optimizeWith :: Provable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult+optimizeWith :: Satisfiable a => SMTConfig -> OptimizeStyle -> a -> IO OptimizeResult optimizeWith = Trans.optimizeWith --- | Check if the constraints given are consistent, using the default solver.+-- | Check if the constraints given are consistent in a prove call using the default solver. ----- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isVacuous'-isVacuous :: Provable a => a -> IO Bool-isVacuous = Trans.isVacuous+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isVacuousProof'+isVacuousProof :: Provable a => a -> IO Bool+isVacuousProof = Trans.isVacuousProof --- | Determine if the constraints are vacuous using the given SMT-solver.+-- | Determine if the constraints are vacuous in a SAT call using the given SMT-solver. ----- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isVacuousWith'-isVacuousWith :: Provable a => SMTConfig -> a -> IO Bool-isVacuousWith = Trans.isVacuousWith+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isVacuousProofWith'+isVacuousProofWith :: Provable a => SMTConfig -> a -> IO Bool+isVacuousProofWith = Trans.isVacuousProofWith  -- | Checks theoremhood using the default solver. --@@ -222,13 +153,13 @@ -- | Checks satisfiability using the default solver. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isSatisfiable'-isSatisfiable :: Provable a => a -> IO Bool+isSatisfiable :: Satisfiable a => a -> IO Bool isSatisfiable = Trans.isSatisfiable  -- | Check whether a given property is satisfiable. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.isSatisfiableWith'-isSatisfiableWith :: Provable a => SMTConfig -> a -> IO Bool+isSatisfiableWith :: Satisfiable a => SMTConfig -> a -> IO Bool isSatisfiableWith = Trans.isSatisfiableWith  -- | Run an arbitrary symbolic computation, equivalent to @'runSMTWith' 'Data.SBV.defaultSMTCfg'@@@ -243,12 +174,10 @@ runSMTWith :: SMTConfig -> Symbolic a -> IO a runSMTWith = Trans.runSMTWith --- | NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sName_'-sName_ :: SExecutable IO a => a -> Symbolic ()-sName_ = Trans.sName_---- | NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sName'-sName :: SExecutable IO a => [String] -> a -> Symbolic ()+-- | Create an argument for a name used in a safety-checking call.+--+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sName_'+sName :: SExecutable IO a => a -> Symbolic () sName = Trans.sName  -- | Check safety using the default solver.@@ -284,41 +213,23 @@ output :: Outputtable a => a -> Symbolic a output = Trans.output --- | Create a user named input (universal)------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sbvForall'-sbvForall :: SymVal a => String -> Symbolic (SBV a)-sbvForall = Trans.sbvForall---- | Create an automatically named input------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sbvForall_'-sbvForall_ :: SymVal a => Symbolic (SBV a)-sbvForall_ = Trans.sbvForall_---- | Get a bunch of new words------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.mkForallVars'-mkForallVars :: SymVal a => Int -> Symbolic [SBV a]-mkForallVars = Trans.mkForallVars---- | Create an existential variable------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sbvExists'-sbvExists :: SymVal a => String -> Symbolic (SBV a)-sbvExists = Trans.sbvExists+-- | Create a partitioning constraint, for all-sat calls.+allSatPartition :: SymVal a => String -> SBV a -> Symbolic ()+allSatPartition nm term = do+   State{rPartitionVars} <- symbolicEnv --- | Create an automatically named existential variable------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sbvExists_'-sbvExists_ :: SymVal a => Symbolic (SBV a)-sbvExists_ = Trans.sbvExists_+   -- Generate a unique variable with the prefix nm if necessary and+   -- add it to partitions+   fresh <- liftIO $ do olds <- readIORef rPartitionVars+                        let new = case filter (`notElem` olds) (nm : [nm ++ "_" ++ show i | i <- [(1 :: Int) ..]]) of+                                    h:_ -> h+                                    []  -> error $ "Impossible: Can't get a fresh variable from infinite list in partition." ++ show (nm, term)+                        modifyIORef' rPartitionVars (++ [new])+                        pure new --- | Create a bunch of existentials------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.mkExistVars'-mkExistVars :: SymVal a => Int -> Symbolic [SBV a]-mkExistVars = Trans.mkExistVars+   -- declare and constrain+   v <- free fresh+   constrain $ v .== term  -- | Create a free variable, universal in a proof, existential in sat --@@ -356,18 +267,6 @@ mkSymVal :: SymVal a => VarContext -> Maybe String -> Symbolic (SBV a) mkSymVal = Trans.mkSymVal --- | Create a new anonymous array, possibly with a default initial value.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.newArray_'-newArray_ :: (SymArray array, HasKind a, HasKind b) => Maybe (SBV b) -> Symbolic (array a b)-newArray_ = Trans.newArray_---- | Create a named new array, possibly with a default initial value.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.newArray'-newArray :: (SymArray array, HasKind a, HasKind b) => String -> Maybe (SBV b) -> Symbolic (array a b)-newArray = Trans.newArray- -- Data.SBV.Core.Model:  -- | Generically make a symbolic var@@ -826,24 +725,6 @@ sTuples :: (SymTuple tup, SymVal tup) => [String] -> Symbolic [SBV tup] sTuples = Trans.sTuples --- | Declare a named 'Data.SBV.SEither'.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sEither'-sEither :: (SymVal a, SymVal b) => String -> Symbolic (SEither a b)-sEither = Trans.sEither---- | Declare an unnamed 'Data.SBV.SEither'.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sEither_'-sEither_ :: (SymVal a, SymVal b) => Symbolic (SEither a b)-sEither_ = Trans.sEither_---- | Declare a list of 'Data.SBV.SEither' values.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sEithers'-sEithers :: (SymVal a, SymVal b) => [String] -> Symbolic [SEither a b]-sEithers = Trans.sEithers- -- | Declare a named 'Data.SBV.SRational'. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sRational'@@ -862,24 +743,6 @@ sRationals :: [String] -> Symbolic [SRational] sRationals = Trans.sRationals --- | Declare a named 'Data.SBV.SMaybe'.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sMaybe'-sMaybe :: SymVal a => String -> Symbolic (SMaybe a)-sMaybe = Trans.sMaybe---- | Declare an unnamed 'Data.SBV.SMaybe'.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sMaybe_'-sMaybe_ :: SymVal a => Symbolic (SMaybe a)-sMaybe_ = Trans.sMaybe_---- | Declare a list of 'Data.SBV.SMaybe' values.------ NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sMaybes'-sMaybes :: SymVal a => [String] -> Symbolic [SMaybe a]-sMaybes = Trans.sMaybes- -- | Declare a named 'Data.SBV.SSet'. -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sSet'@@ -898,6 +761,24 @@ sSets :: (Ord a, SymVal a) => [String] -> Symbolic [SSet a] sSets = Trans.sSets +-- | Declare a named 'SArray'+--+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sArray'+sArray :: (SymVal a, SymVal b) => String -> Symbolic (SArray a b)+sArray = Trans.sArray++-- | Declare an unnamed 'SArray'+--+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sArray_'+sArray_ :: (SymVal a, SymVal b) => Symbolic (SArray a b)+sArray_ = Trans.sArray_++-- | Declare a list of 'SArray' values.+--+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sArrays'+sArrays :: (SymVal a, SymVal b) => [String] -> Symbolic [SArray a b]+sArrays = Trans.sArrays+ -- | Form the symbolic conjunction of a given list of boolean conditions. Useful in expressing -- problems with constraints, like the following: --@@ -939,7 +820,7 @@ -- | Run a symbolic computation, and return a extra value paired up with the 'Result' -- -- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.runSymbolic'-runSymbolic :: SBVRunMode -> Symbolic a -> IO (a, Result)+runSymbolic :: SMTConfig -> SBVRunMode -> Symbolic a -> IO (a, Result) runSymbolic = Trans.runSymbolic  -- | Add a new option@@ -967,145 +848,8 @@ outputSVal :: SVal -> Symbolic () outputSVal = Trans.outputSVal --- | Capturing non-matching instances for better error messages, conversions from sized-type FromSizedErr (arg :: Type) =     'Text "fromSized: Cannot convert from type: " ':<>: 'ShowType arg-                                ':$$: 'Text "           Source type must be one of SInt N, SWord N, IntN N, WordN N"-                                ':$$: 'Text "           where N is 8, 16, 32, or 64."---- | Capturing non-matching instances for better error messages, conversions to sized-type ToSizedErr (arg :: Type) =      'Text "toSized: Cannot convert from type: " ':<>: 'ShowType arg-                              ':$$: 'Text "          Source type must be one of Int8/16/32/64"-                              ':$$: 'Text "                                  OR Word8/16/32/64"-                              ':$$: 'Text "                                  OR their symbolic variants."---- | Capture the correspondence between sized and fixed-sized BVs-type family FromSized (t :: Type) :: Type where-   FromSized (WordN  8) = Word8-   FromSized (WordN 16) = Word16-   FromSized (WordN 32) = Word32-   FromSized (WordN 64) = Word64-   FromSized (IntN   8) = Int8-   FromSized (IntN  16) = Int16-   FromSized (IntN  32) = Int32-   FromSized (IntN  64) = Int64-   FromSized (SWord  8) = SWord8-   FromSized (SWord 16) = SWord16-   FromSized (SWord 32) = SWord32-   FromSized (SWord 64) = SWord64-   FromSized (SInt   8) = SInt8-   FromSized (SInt  16) = SInt16-   FromSized (SInt  32) = SInt32-   FromSized (SInt  64) = SInt64---- | Capture the correspondence, in terms of a constraint-type family FromSizedCstr (t :: Type) :: Constraint where-   FromSizedCstr (WordN  8) = ()-   FromSizedCstr (WordN 16) = ()-   FromSizedCstr (WordN 32) = ()-   FromSizedCstr (WordN 64) = ()-   FromSizedCstr (IntN   8) = ()-   FromSizedCstr (IntN  16) = ()-   FromSizedCstr (IntN  32) = ()-   FromSizedCstr (IntN  64) = ()-   FromSizedCstr (SWord  8) = ()-   FromSizedCstr (SWord 16) = ()-   FromSizedCstr (SWord 32) = ()-   FromSizedCstr (SWord 64) = ()-   FromSizedCstr (SInt   8) = ()-   FromSizedCstr (SInt  16) = ()-   FromSizedCstr (SInt  32) = ()-   FromSizedCstr (SInt  64) = ()-   FromSizedCstr arg        = TypeError (FromSizedErr arg)---- | Conversion from a sized BV to a fixed-sized bit-vector.-class FromSizedBV a where-   -- | Convert a sized bit-vector to the corresponding fixed-sized bit-vector,-   -- for instance 'SWord 16' to 'SWord16'. See also 'toSized'.-   fromSized :: a -> FromSized a--   default fromSized :: (Num (FromSized a), Integral a) => a -> FromSized a-   fromSized = fromIntegral--instance {-# OVERLAPPING  #-} FromSizedBV (WordN   8)-instance {-# OVERLAPPING  #-} FromSizedBV (WordN  16)-instance {-# OVERLAPPING  #-} FromSizedBV (WordN  32)-instance {-# OVERLAPPING  #-} FromSizedBV (WordN  64)-instance {-# OVERLAPPING  #-} FromSizedBV (IntN    8)-instance {-# OVERLAPPING  #-} FromSizedBV (IntN   16)-instance {-# OVERLAPPING  #-} FromSizedBV (IntN   32)-instance {-# OVERLAPPING  #-} FromSizedBV (IntN   64)-instance {-# OVERLAPPING  #-} FromSizedBV (SWord   8) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} FromSizedBV (SWord  16) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} FromSizedBV (SWord  32) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} FromSizedBV (SWord  64) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} FromSizedBV (SInt    8) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} FromSizedBV (SInt   16) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} FromSizedBV (SInt   32) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} FromSizedBV (SInt   64) where fromSized = Trans.sFromIntegral-instance {-# OVERLAPPABLE #-} FromSizedCstr arg => FromSizedBV arg where fromSized = error "unreachable"---- | Capture the correspondence between fixed-sized and sized BVs-type family ToSized (t :: Type) :: Type where-   ToSized Word8   = WordN  8-   ToSized Word16  = WordN 16-   ToSized Word32  = WordN 32-   ToSized Word64  = WordN 64-   ToSized Int8    = IntN   8-   ToSized Int16   = IntN  16-   ToSized Int32   = IntN  32-   ToSized Int64   = IntN  64-   ToSized SWord8  = SWord  8-   ToSized SWord16 = SWord 16-   ToSized SWord32 = SWord 32-   ToSized SWord64 = SWord 64-   ToSized SInt8   = SInt   8-   ToSized SInt16  = SInt  16-   ToSized SInt32  = SInt  32-   ToSized SInt64  = SInt  64---- | Capture the correspondence in terms of a constraint-type family ToSizedCstr (t :: Type) :: Constraint where-   ToSizedCstr Word8   = ()-   ToSizedCstr Word16  = ()-   ToSizedCstr Word32  = ()-   ToSizedCstr Word64  = ()-   ToSizedCstr Int8    = ()-   ToSizedCstr Int16   = ()-   ToSizedCstr Int32   = ()-   ToSizedCstr Int64   = ()-   ToSizedCstr SWord8  = ()-   ToSizedCstr SWord16 = ()-   ToSizedCstr SWord32 = ()-   ToSizedCstr SWord64 = ()-   ToSizedCstr SInt8   = ()-   ToSizedCstr SInt16  = ()-   ToSizedCstr SInt32  = ()-   ToSizedCstr SInt64  = ()-   ToSizedCstr arg     = TypeError (ToSizedErr arg)---- | Conversion from a fixed-sized BV to a sized bit-vector.-class ToSizedBV a where-   -- | Convert a fixed-sized bit-vector to the corresponding sized bit-vector,-   -- for instance 'SWord16' to 'SWord 16'. See also 'fromSized'.-   toSized :: a -> ToSized a--   default toSized :: (Num (ToSized a), Integral a) => (a -> ToSized a)-   toSized = fromIntegral--instance {-# OVERLAPPING  #-} ToSizedBV Word8-instance {-# OVERLAPPING  #-} ToSizedBV Word16-instance {-# OVERLAPPING  #-} ToSizedBV Word32-instance {-# OVERLAPPING  #-} ToSizedBV Word64-instance {-# OVERLAPPING  #-} ToSizedBV Int8-instance {-# OVERLAPPING  #-} ToSizedBV Int16-instance {-# OVERLAPPING  #-} ToSizedBV Int32-instance {-# OVERLAPPING  #-} ToSizedBV Int64-instance {-# OVERLAPPING  #-} ToSizedBV SWord8  where toSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} ToSizedBV SWord16 where toSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} ToSizedBV SWord32 where toSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} ToSizedBV SWord64 where toSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} ToSizedBV SInt8   where toSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} ToSizedBV SInt16  where toSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} ToSizedBV SInt32  where toSized = Trans.sFromIntegral-instance {-# OVERLAPPING  #-} ToSizedBV SInt64  where toSized = Trans.sFromIntegral-instance {-# OVERLAPPABLE #-} ToSizedCstr arg => ToSizedBV arg where toSized = error "unreachable"+-- | A variant of observe that you can use at the top-level. This is useful with quick-check, for instance.+--+-- NB. For a version which generalizes over the underlying monad, see 'Data.SBV.Trans.sObserve'+sObserve :: SymVal a => String -> SBV a -> Symbolic ()+sObserve m x = Trans.sObserve m (Trans.unSBV x)