Permalink
Browse files

remove "portable" comment in file headers.

SBV really needs some GHC specific stuff, like stable-names and "default signatures" etc.; so portability to other Haskell compilers is not really realistic..
  • Loading branch information...
LeventErkok committed May 23, 2012
1 parent e6536b1 commit f8770a16cfdee815e0afded6b75a1c165c508c1d
Showing with 1 addition and 109 deletions.
  1. +0 −1 Data/SBV/BitVectors/AlgReals.hs
  2. +0 −1 Data/SBV/BitVectors/Data.hs
  3. +0 −1 Data/SBV/BitVectors/Model.hs
  4. +0 −1 Data/SBV/BitVectors/PrettyNum.hs
  5. +0 −1 Data/SBV/BitVectors/STree.hs
  6. +0 −1 Data/SBV/BitVectors/SignCast.hs
  7. +0 −1 Data/SBV/BitVectors/Splittable.hs
  8. +0 −1 Data/SBV/Compilers/C.hs
  9. +0 −1 Data/SBV/Compilers/CodeGen.hs
  10. +0 −1 Data/SBV/Examples/BitPrecise/BitTricks.hs
  11. +0 −1 Data/SBV/Examples/BitPrecise/Legato.hs
  12. +0 −1 Data/SBV/Examples/BitPrecise/MergeSort.hs
  13. +0 −1 Data/SBV/Examples/BitPrecise/PrefixSum.hs
  14. +0 −1 Data/SBV/Examples/CodeGeneration/AddSub.hs
  15. +0 −1 Data/SBV/Examples/CodeGeneration/CRC_USB5.hs
  16. +0 −1 Data/SBV/Examples/CodeGeneration/Fibonacci.hs
  17. +0 −1 Data/SBV/Examples/CodeGeneration/GCD.hs
  18. +0 −1 Data/SBV/Examples/CodeGeneration/PopulationCount.hs
  19. +0 −1 Data/SBV/Examples/CodeGeneration/Uninterpreted.hs
  20. +0 −1 Data/SBV/Examples/Crypto/AES.hs
  21. +0 −1 Data/SBV/Examples/Crypto/RC4.hs
  22. +0 −1 Data/SBV/Examples/Existentials/CRCPolynomial.hs
  23. +0 −1 Data/SBV/Examples/Existentials/Diophantine.hs
  24. +0 −1 Data/SBV/Examples/Polynomials/Polynomials.hs
  25. +0 −1 Data/SBV/Examples/Puzzles/Coins.hs
  26. +0 −1 Data/SBV/Examples/Puzzles/Counts.hs
  27. +0 −1 Data/SBV/Examples/Puzzles/DogCatMouse.hs
  28. +0 −1 Data/SBV/Examples/Puzzles/Euler185.hs
  29. +0 −1 Data/SBV/Examples/Puzzles/MagicSquare.hs
  30. +0 −1 Data/SBV/Examples/Puzzles/NQueens.hs
  31. +0 −1 Data/SBV/Examples/Puzzles/Sudoku.hs
  32. +0 −1 Data/SBV/Examples/Puzzles/U2Bridge.hs
  33. +0 −1 Data/SBV/Examples/Uninterpreted/AUF.hs
  34. +0 −1 Data/SBV/Examples/Uninterpreted/Deduce.hs
  35. +0 −1 Data/SBV/Examples/Uninterpreted/Function.hs
  36. +0 −1 Data/SBV/Examples/Uninterpreted/Sort.hs
  37. +0 −1 Data/SBV/Provers/Prover.hs
  38. +0 −1 Data/SBV/Provers/SExpr.hs
  39. +0 −1 Data/SBV/Provers/Yices.hs
  40. +0 −1 Data/SBV/Provers/Z3.hs
  41. +0 −1 Data/SBV/SMT/SMT.hs
  42. +0 −1 Data/SBV/SMT/SMTLib.hs
  43. +0 −1 Data/SBV/SMT/SMTLib1.hs
  44. +0 −1 Data/SBV/SMT/SMTLib2.hs
  45. +0 −1 Data/SBV/Tools/ExpectedValue.hs
  46. +0 −1 Data/SBV/Tools/GenTest.hs
  47. +0 −1 Data/SBV/Tools/Optimize.hs
  48. +0 −1 Data/SBV/Tools/Polynomial.hs
  49. +0 −1 Data/SBV/Utils/Boolean.hs
  50. +0 −1 Data/SBV/Utils/Lib.hs
  51. +0 −1 Data/SBV/Utils/TDiff.hs
  52. +0 −1 SBVUnitTest/Examples/Arrays/Memory.hs
  53. +0 −1 SBVUnitTest/Examples/Basics/BasicTests.hs
  54. +0 −1 SBVUnitTest/Examples/Basics/Higher.hs
  55. +0 −1 SBVUnitTest/Examples/Basics/Index.hs
  56. +0 −1 SBVUnitTest/Examples/Basics/ProofTests.hs
  57. +0 −1 SBVUnitTest/Examples/Basics/QRem.hs
  58. +0 −1 SBVUnitTest/Examples/CRC/CCITT.hs
  59. +0 −1 SBVUnitTest/Examples/CRC/CCITT_Unidir.hs
  60. +0 −1 SBVUnitTest/Examples/CRC/GenPoly.hs
  61. +0 −1 SBVUnitTest/Examples/CRC/Parity.hs
  62. +0 −1 SBVUnitTest/Examples/CRC/USB5.hs
  63. +0 −1 SBVUnitTest/Examples/Puzzles/PowerSet.hs
  64. +0 −1 SBVUnitTest/Examples/Puzzles/Temperature.hs
  65. +0 −1 SBVUnitTest/Examples/Uninterpreted/Uninterpreted.hs
  66. +0 −1 SBVUnitTest/SBVTest.hs
  67. +0 −1 SBVUnitTest/SBVUnitTest.hs
  68. +1 −1 SBVUnitTest/SBVUnitTestBuildTime.hs
  69. +0 −1 SBVUnitTest/TestSuite/Arrays/Memory.hs
  70. +0 −1 SBVUnitTest/TestSuite/Basics/Arithmetic.hs
  71. +0 −1 SBVUnitTest/TestSuite/Basics/BasicTests.hs
  72. +0 −1 SBVUnitTest/TestSuite/Basics/Higher.hs
  73. +0 −1 SBVUnitTest/TestSuite/Basics/Index.hs
  74. +0 −1 SBVUnitTest/TestSuite/Basics/ProofTests.hs
  75. +0 −1 SBVUnitTest/TestSuite/Basics/QRem.hs
  76. +0 −1 SBVUnitTest/TestSuite/BitPrecise/BitTricks.hs
  77. +0 −1 SBVUnitTest/TestSuite/BitPrecise/Legato.hs
  78. +0 −1 SBVUnitTest/TestSuite/BitPrecise/MergeSort.hs
  79. +0 −1 SBVUnitTest/TestSuite/BitPrecise/PrefixSum.hs
  80. +0 −1 SBVUnitTest/TestSuite/CRC/CCITT.hs
  81. +0 −1 SBVUnitTest/TestSuite/CRC/CCITT_Unidir.hs
  82. +0 −1 SBVUnitTest/TestSuite/CRC/GenPoly.hs
  83. +0 −1 SBVUnitTest/TestSuite/CRC/Parity.hs
  84. +0 −1 SBVUnitTest/TestSuite/CRC/USB5.hs
  85. +0 −1 SBVUnitTest/TestSuite/CodeGeneration/AddSub.hs
  86. +0 −1 SBVUnitTest/TestSuite/CodeGeneration/CRC_USB5.hs
  87. +0 −1 SBVUnitTest/TestSuite/CodeGeneration/CgTests.hs
  88. +0 −1 SBVUnitTest/TestSuite/CodeGeneration/Fibonacci.hs
  89. +0 −1 SBVUnitTest/TestSuite/CodeGeneration/GCD.hs
  90. +0 −1 SBVUnitTest/TestSuite/CodeGeneration/PopulationCount.hs
  91. +0 −1 SBVUnitTest/TestSuite/CodeGeneration/Uninterpreted.hs
  92. +0 −1 SBVUnitTest/TestSuite/Crypto/AES.hs
  93. +0 −1 SBVUnitTest/TestSuite/Crypto/RC4.hs
  94. +0 −1 SBVUnitTest/TestSuite/Existentials/CRCPolynomial.hs
  95. +0 −1 SBVUnitTest/TestSuite/Polynomials/Polynomials.hs
  96. +0 −1 SBVUnitTest/TestSuite/Puzzles/Coins.hs
  97. +0 −1 SBVUnitTest/TestSuite/Puzzles/Counts.hs
  98. +0 −1 SBVUnitTest/TestSuite/Puzzles/DogCatMouse.hs
  99. +0 −1 SBVUnitTest/TestSuite/Puzzles/Euler185.hs
  100. +0 −1 SBVUnitTest/TestSuite/Puzzles/MagicSquare.hs
  101. +0 −1 SBVUnitTest/TestSuite/Puzzles/NQueens.hs
  102. +0 −1 SBVUnitTest/TestSuite/Puzzles/PowerSet.hs
  103. +0 −1 SBVUnitTest/TestSuite/Puzzles/Sudoku.hs
  104. +0 −1 SBVUnitTest/TestSuite/Puzzles/Temperature.hs
  105. +0 −1 SBVUnitTest/TestSuite/Puzzles/U2Bridge.hs
  106. +0 −1 SBVUnitTest/TestSuite/Uninterpreted/AUF.hs
  107. +0 −1 SBVUnitTest/TestSuite/Uninterpreted/Function.hs
  108. +0 −1 SBVUnitTest/TestSuite/Uninterpreted/Uninterpreted.hs
  109. +0 −1 Setup.hs
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Algrebraic reals in Haskell.
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Internal data-structures for the sbv library
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Instance declarations for our symbolic world
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Number representations in hex/bin
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Implementation of full-binary symbolic trees, providing logarithmic
-- time access to elements. Both reads and writes are supported.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Implementation of casting between signed/unsigned variants of the
-- same type.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Implementation of bit-vector concatanetation and splits
-----------------------------------------------------------------------------
View
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Compilation of symbolic programs to C
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Code generation utilities
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Checks the correctness of a few tricks from the large collection found in:
-- <http://graphics.stanford.edu/~seander/bithacks.html>
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- An encoding and correctness proof of Legato's multiplier in Haskell. Bill Legato came
-- up with an interesting way to multiply two 8-bit numbers on Mostek, as described here:
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Symbolic implementation of merge-sort and its correctness.
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- The PrefixSum algorithm over power-lists and proof of
-- the Ladner-Fischer implementation.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Simple code generation example.
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Computing the CRC symbolically, using the USB polynomial. We also
-- generating C code for it as well. This example demonstrates the
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Computing Fibonacci numbers and generating C code. Inspired by Lee Pike's
-- original implementation, modified for inclusion in the package. It illustrates
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Computing GCD symbolically, and generating C code for it. This example
-- illustrates symbolic termination related issues when programming with
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Computing population-counts (number of set bits) and autimatically
-- generating C code.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Demonstrates the use of uninterpreted functions for the purposes of
-- code generation. This facility is important when we want to take
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- An implementation of AES (Advanced Encryption Standard), using SBV.
-- For details on AES, see FIPS-197: <http://csrc.nist.gov/publications/fips/fips197/fips-197.pdf>.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- An implementation of RC4 (AKA Rivest Cipher 4 or Alleged RC4/ARC4),
-- using SBV. For information on RC4, see: <http://en.wikipedia.org/wiki/RC4>.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- This program demonstrates the use of the existentials and the QBVF (quantified
-- bit-vector solver). We generate CRC polynomials of degree 16 that can be used
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Finding minimal natural number solutions to linear Diophantine equations,
-- using explicit quantification.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Simple usage of polynomials over GF(2^n), using Rijndael's
-- finite field: <http://en.wikipedia.org/wiki/Finite_field_arithmetic#Rijndael.27s_finite_field>
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Solves the following puzzle:
--
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Consider the sentence:
--
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Puzzle:
-- Spend exactly 100 dollars and buy exactly 100 animals.
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- A solution to Project Euler problem #185: <http://projecteuler.net/index.php?section=problems&id=185>
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Solves the magic-square puzzle. An NxN magic square is one where all entries
-- are filled with numbers from 1 to NxN such that sums of all rows, columns
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Solves the NQueens puzzle: <http://en.wikipedia.org/wiki/Eight_queens_puzzle>
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- The Sudoku solver, quintessential SMT solver example!
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- The famous U2 bridge crossing puzzle: <http://www.brainj.net/puzzle.php?id=u2>
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Formalizes and proves the following theorem, about arithmetic,
-- uninterpreted functions, and arrays. (For reference, see <http://research.microsoft.com/en-us/um/redmond/projects/z3/fmcad06-slides.pdf>
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Demonstrates uninterpreted sorts and how they can be used for deduction.
-- This example is inspired by the discussion at <http://stackoverflow.com/questions/10635783/using-axioms-for-deductions-in-z3>,
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Demonstrates function counter-examples
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Demonstrates uninterpreted sorts, together with axioms.
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Provable abstraction and the connection to SMT solvers
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Parsing of S-expressions (mainly used for parsing SMT-Lib get-value output)
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- The connection to the Yices SMT solver
-----------------------------------------------------------------------------
View
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- The connection to the Z3 SMT solver
-----------------------------------------------------------------------------
View
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Abstraction of SMT solvers
-----------------------------------------------------------------------------
View
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Conversion of symbolic programs to SMTLib format
-----------------------------------------------------------------------------
View
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Conversion of symbolic programs to SMTLib format, Using v1 of the standard
-----------------------------------------------------------------------------
View
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Conversion of symbolic programs to SMTLib format, Using v2 of the standard
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Computing the expected value of a symbolic variable
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Test generation from symbolic programs
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- SMT based optimization
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Implementation of polynomial arithmetic
-----------------------------------------------------------------------------
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Abstraction of booleans. Unfortunately, Haskell makes Bool's very hard to
-- work with, by making it a fixed-data type. This is our workaround
View
@@ -5,7 +5,6 @@
-- License : BSD3
-- Maintainer : erkokl@gmail.com
-- Stability : experimental
--- Portability : portable
--
-- Misc helpers
-----------------------------------------------------------------------------
Oops, something went wrong.

0 comments on commit f8770a1

Please sign in to comment.