Simplify T!val!n to T_n

Data/SBV/Control/Utils.hs

@@ -929,7 +929,7 @@ recoverKindedValue k e = case k of
                                        | EReal i     <- e      -> Just $ CV KReal (CAlgReal i)
                                        | True                  -> interpretInterval e
 
-                           KUserSort{} | ECon s <- e           -> Just $ CV k $ CUserSort (getUIIndex k s, s)
+                           KUserSort{} | ECon s <- e           -> Just $ CV k $ CUserSort (getUIIndex k s, trim s)
                                        | True                  -> Nothing
 
                            KFloat      | ENum (i, _) <- e      -> Just $ mkConstCV k i
@@ -965,6 +965,11 @@ recoverKindedValue k e = case k of
 
         stringLike xs = length xs >= 2 && "\"" `isPrefixOf` xs && "\"" `isSuffixOf` xs
 
+        -- z3 prints uninterpreted values like this: T!val!4. Turn that into T_4
+        trim "" = ""
+        trim ('!':'v':'a':'l':'!':rest) = '_' : trim rest
+        trim (c:cs) = c : trim cs
+
         -- Make sure strings are really strings
         interpretString xs
           | not (stringLike xs)

Documentation/SBV/Examples/KnuckleDragger/Basics.hs

@@ -116,14 +116,14 @@ existsDisjunction = runKD $ do
 -- *** Failed to prove forallConjunctionNot.
 -- Falsifiable. Counter-example:
 --   p :: T -> Bool
---   p T!val!2 = True
---   p T!val!0 = True
---   p _       = False
+--   p T_2 = True
+--   p T_0 = True
+--   p _   = False
 -- <BLANKLINE>
 --   q :: T -> Bool
---   q T!val!2 = False
---   q T!val!0 = False
---   q _       = True
+--   q T_2 = False
+--   q T_0 = False
+--   q _   = True
 --
 -- Note how @p@ assigns two selected values to @True@ and everything else to @False@, while @q@ does the exact opposite.
 -- So, there is no common value that satisfies both, providing a counter-example. (It's not clear why the solver finds
@@ -153,12 +153,12 @@ forallDisjunctionNot = runKD $ do
 -- *** Failed to prove existsConjunctionNot.
 -- Falsifiable. Counter-example:
 --   p :: T -> Bool
---   p T!val!1 = False
---   p _       = True
+--   p T_1 = False
+--   p _   = True
 -- <BLANKLINE>
 --   q :: T -> Bool
---   q T!val!1 = True
---   q _       = False
+--   q T_1 = True
+--   q _   = False
 --
 -- In this case, we again have a predicate That disagree at every point, providing a counter-example.
 existsConjunctionNot :: IO ()

Documentation/SBV/Examples/KnuckleDragger/RevLen.hs

@@ -66,7 +66,7 @@ revLen = runKD $ do
 -- Lemma: badRevLen
 -- *** Failed to prove badRevLen.
 -- Falsifiable. Counter-example:
---   xs = [Elt!val!1,Elt!val!2,Elt!val!1] :: [Elt]
+--   xs = [Elt_1,Elt_2,Elt_1] :: [Elt]
 badRevLen :: IO ()
 badRevLen = runKD $ do
    let p :: SList Elt -> SBool

Documentation/SBV/Examples/Misc/FirstOrderLogic.hs

@@ -132,20 +132,20 @@ We have:
 >>> prove $ (qe (\(Forall x) -> p x) .|| qe (\(Forall x) -> q x)) .<=> qe (\(Forall x) -> p x .|| q x)
 Falsifiable. Counter-example:
   P :: U -> Bool
-  P U!val!2 = True
-  P U!val!0 = True
-  P _       = False
+  P U_2 = True
+  P U_0 = True
+  P _   = False
 <BLANKLINE>
   Q :: U -> Bool
-  Q U!val!2 = False
-  Q U!val!0 = False
-  Q _       = True
+  Q U_2 = False
+  Q U_0 = False
+  Q _   = True
 
 The solver found us a falsifying instance: Pick a domain with at least three elements. We'll call
-the first element @U!val!2@, and the second element @U!val!0@, without naming the others. (Unfortunately the solver picks nonintuitive names, but you can substitute better names if you like. They're just names of two distinct
+the first element @U_2@, and the second element @U_0@, without naming the others. (Unfortunately the solver picks nonintuitive names, but you can substitute better names if you like. They're just names of two distinct
 objects that belong to the domain \(U\) with no other meaning.)
 
-Arrange so that \(P\) is true on @U!val!2@ and @U!val!0@, but false for everything else.
+Arrange so that \(P\) is true on @U_2@ and @U_0@, but false for everything else.
 Also arrange so that \(Q\) is false on these two elements, but true for everything else.
 
 With this

Documentation/SBV/Examples/Uninterpreted/Sort.hs

@@ -39,10 +39,10 @@ f = uninterpret "f"
 --
 -- >>> t1
 -- Satisfiable. Model:
---   x = Q!val!0 :: Q
+--   x = Q_0 :: Q
 -- <BLANKLINE>
 --   f :: Q -> Q
---   f _ = Q!val!1
+--   f _ = Q_1
 t1 :: IO SatResult
 t1 = sat $ do x <- free "x"
               return $ f x ./= x

Documentation/SBV/Examples/Uninterpreted/UISortAllSat.hs

@@ -54,35 +54,35 @@ classify = uninterpret "classify"
 --
 -- >>> allSat genLs
 -- Solution #1:
---   l  = L!val!2 :: L
---   l0 = L!val!0 :: L
---   l1 = L!val!1 :: L
---   l2 = L!val!2 :: L
+--   l  = L_2 :: L
+--   l0 = L_0 :: L
+--   l1 = L_1 :: L
+--   l2 = L_2 :: L
 -- <BLANKLINE>
 --   classify :: L -> Integer
---   classify L!val!2 = 2
---   classify L!val!1 = 1
---   classify _       = 0
+--   classify L_2 = 2
+--   classify L_1 = 1
+--   classify _   = 0
 -- Solution #2:
---   l  = L!val!1 :: L
---   l0 = L!val!0 :: L
---   l1 = L!val!1 :: L
---   l2 = L!val!2 :: L
+--   l  = L_1 :: L
+--   l0 = L_0 :: L
+--   l1 = L_1 :: L
+--   l2 = L_2 :: L
 -- <BLANKLINE>
 --   classify :: L -> Integer
---   classify L!val!2 = 2
---   classify L!val!1 = 1
---   classify _       = 0
+--   classify L_2 = 2
+--   classify L_1 = 1
+--   classify _   = 0
 -- Solution #3:
---   l  = L!val!0 :: L
---   l0 = L!val!0 :: L
---   l1 = L!val!1 :: L
---   l2 = L!val!2 :: L
+--   l  = L_0 :: L
+--   l0 = L_0 :: L
+--   l1 = L_1 :: L
+--   l2 = L_2 :: L
 -- <BLANKLINE>
 --   classify :: L -> Integer
---   classify L!val!2 = 2
---   classify L!val!1 = 1
---   classify _       = 0
+--   classify L_2 = 2
+--   classify L_1 = 1
+--   classify _   = 0
 -- Found 3 different solutions.
 genLs :: Predicate
 genLs = do [l, l0, l1, l2] <- symbolics ["l", "l0", "l1", "l2"]

SBVTestSuite/GoldFiles/allSat1.gold

@@ -1,4 +1,4 @@
 Solution #1:
-  x = Q!val!0 :: Q
-  y = Q!val!0 :: Q
-This is the only solution.
+  x = Q_0 :: Q
+  y = Q_0 :: Q
+This is the only solution.

SBVTestSuite/GoldFiles/allSat2.gold

@@ -1,9 +1,9 @@
 Solution #1:
-  x = Q!val!0 :: Q
-  y = Q!val!0 :: Q
-  z = Q!val!1 :: Q
+  x = Q_0 :: Q
+  y = Q_0 :: Q
+  z = Q_1 :: Q
 Solution #2:
-  x = Q!val!0 :: Q
-  y = Q!val!0 :: Q
-  z = Q!val!0 :: Q
-Found 2 different solutions.
+  x = Q_0 :: Q
+  y = Q_0 :: Q
+  z = Q_0 :: Q
+Found 2 different solutions.

SBVTestSuite/GoldFiles/uninterpreted-4.gold

@@ -36,6 +36,6 @@
 *** Exit code: ExitSuccess
 
  FINAL:Satisfiable. Model:
-  c = Q!val!0 :: Q
-  d = Q!val!1 :: Q
+  c = Q_0 :: Q
+  d = Q_1 :: Q
 DONE!

SBVTestSuite/GoldFiles/uninterpreted-4a.gold

@@ -46,7 +46,7 @@ Looking for solution 1
 *** Exit code: ExitSuccess
 
  FINAL:Solution #1:
-  c = Q!val!0 :: Q
-  d = Q!val!1 :: Q
+  c = Q_0 :: Q
+  d = Q_1 :: Q
 This is the only solution.
 DONE!

sbv.cabal

@@ -159,6 +159,7 @@ Library
                   , Documentation.SBV.Examples.KnuckleDragger.CaseSplit
                   , Documentation.SBV.Examples.KnuckleDragger.Kleene
                   , Documentation.SBV.Examples.KnuckleDragger.Induction
+                  , Documentation.SBV.Examples.KnuckleDragger.InsertionSort
                   , Documentation.SBV.Examples.KnuckleDragger.ListLen
                   , Documentation.SBV.Examples.KnuckleDragger.RevLen
                   , Documentation.SBV.Examples.KnuckleDragger.Sqrt2IsIrrational