Skip to content

Commit

Permalink
fix links
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed May 10, 2024
1 parent 547294f commit f2632f5
Show file tree
Hide file tree
Showing 5 changed files with 7 additions and 7 deletions.
4 changes: 2 additions & 2 deletions CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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
Expand Down
2 changes: 1 addition & 1 deletion Data/SBV.hs
Original file line number Diff line number Diff line change
Expand Up @@ -801,7 +801,7 @@ by Rummer and Wahl: <http://www.philipp.ruemmer.org/publications/smt-fpa.pdf>.

{- $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.
-}
Expand Down
2 changes: 1 addition & 1 deletion Data/SBV/Char.hs
Original file line number Diff line number Diff line change
Expand Up @@ -14,7 +14,7 @@
-- 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,
Expand Down
4 changes: 2 additions & 2 deletions Data/SBV/Core/Data.hs
Original file line number Diff line number Diff line change
Expand Up @@ -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: <http://smtlib.cs.uiowa.edu/theories-UnicodeStrings.shtml>
-- see: <https://smt-lib.org/theories-UnicodeStrings.shtml>
-- for details.
type SChar = SBV Char

Expand Down Expand Up @@ -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: <http://smtlib.cs.uiowa.edu/theories-ArraysEx.shtml>
-- | Arrays implemented in terms of SMT-arrays: <https://smt-lib.org/theories-ArraysEx.shtml>
--
-- * Maps directly to SMT-lib arrays
--
Expand Down
2 changes: 1 addition & 1 deletion Data/SBV/SMT/SMTLib2.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1299,7 +1299,7 @@ declareName s t@(SBVType inputKS) mbCmnt = decl : restrict
in c1 ++ c2

-----------------------------------------------------------------------------------------------
-- Casts supported by SMTLib. (From: <http://smtlib.cs.uiowa.edu/theories-FloatingPoint.shtml>)
-- Casts supported by SMTLib. (From: <https://smt-lib.org/theories-FloatingPoint.shtml>)
-- ; from another floating point sort
-- ((_ to_fp eb sb) RoundingMode (_ FloatingPoint mb nb) (_ FloatingPoint eb sb))
--
Expand Down

0 comments on commit f2632f5

Please sign in to comment.