From f2632f5afd043fb19636eb75d7d4fb5733f4ade5 Mon Sep 17 00:00:00 2001 From: Levent Erkok Date: Fri, 10 May 2024 14:37:52 -0700 Subject: [PATCH] fix links --- CHANGES.md | 4 ++-- Data/SBV.hs | 2 +- Data/SBV/Char.hs | 2 +- Data/SBV/Core/Data.hs | 4 ++-- Data/SBV/SMT/SMTLib2.hs | 2 +- 5 files changed, 7 insertions(+), 7 deletions(-) diff --git a/CHANGES.md b/CHANGES.md index d629a3dc7..f40ca7640 100644 --- a/CHANGES.md +++ b/CHANGES.md @@ -1199,7 +1199,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 @@ -2120,7 +2120,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 diff --git a/Data/SBV.hs b/Data/SBV.hs index ca1ab26df..a19d2c487 100644 --- a/Data/SBV.hs +++ b/Data/SBV.hs @@ -801,7 +801,7 @@ by Rummer and Wahl: . {- $strings Support for characters, strings, and regular expressions (initial version contributed by Joel Burget) -adds support for QF_S logic, described here: +adds support for QF_S logic, described here: See "Data.SBV.Char", "Data.SBV.String", "Data.SBV.RegExp" for related functions. -} diff --git a/Data/SBV/Char.hs b/Data/SBV/Char.hs index 06ff0b13f..22bc284c3 100644 --- a/Data/SBV/Char.hs +++ b/Data/SBV/Char.hs @@ -14,7 +14,7 @@ -- and strings. -- -- 'SChar' type only covers all unicode characters, following the specification --- in . +-- in . -- 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, diff --git a/Data/SBV/Core/Data.hs b/Data/SBV/Core/Data.hs index 1b35e1f87..0f6f24c50 100644 --- a/Data/SBV/Core/Data.hs +++ b/Data/SBV/Core/Data.hs @@ -174,7 +174,7 @@ type SFPDouble = SBV FPDouble type SFPQuad = SBV FPQuad -- | A symbolic character. Note that this is the full unicode character set. --- see: +-- see: -- for details. type SChar = SBV Char @@ -717,7 +717,7 @@ class SymArray array where -- newArray, we must provide a dummy implementation for newArrayInState: newArrayInState = error "undefined: newArrayInState" --- | Arrays implemented in terms of SMT-arrays: +-- | Arrays implemented in terms of SMT-arrays: -- -- * Maps directly to SMT-lib arrays -- diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs index e31c8cee3..6dbb00029 100644 --- a/Data/SBV/SMT/SMTLib2.hs +++ b/Data/SBV/SMT/SMTLib2.hs @@ -1299,7 +1299,7 @@ declareName s t@(SBVType inputKS) mbCmnt = decl : restrict in c1 ++ c2 ----------------------------------------------------------------------------------------------- --- Casts supported by SMTLib. (From: ) +-- Casts supported by SMTLib. (From: ) -- ; from another floating point sort -- ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb)) --