add missing cases

LeventErkok · Sep 16, 2024 · 8eb1c1f · 8eb1c1f
1 parent 2e0c3eb
commit 8eb1c1f
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/Data/SBV/Core/Symbolic.hs b/Data/SBV/Core/Symbolic.hs
@@ -639,10 +639,13 @@ instance Show Op where
   show (MaybeIs          k False)       = "(_ is (nothing_SBVMaybe () "              ++ show (KMaybe k) ++ "))"
   show (MaybeIs          k True )       = "(_ is (just_SBVMaybe (" ++ show k ++ ") " ++ show (KMaybe k) ++ "))"
   show MaybeAccess                      = "get_just_SBVMaybe"
+  show (ArrayLambda s)                  = s
+  show ReadArray                        = "select"
+  show WriteArray                       = "store"
 
   show op
     | Just s <- op `lookup` syms = s
-    | True                       = error "impossible happened; can't find op!"
+    | True                       = error "impossible happened; can't find op!" -- NB. Can't display the OP here! it's the show instance after all.
     where syms = [ (Plus, "+"), (Times, "*"), (Minus, "-"), (UNeg, "-"), (Abs, "abs")
                  , (Quot, "quot")
                  , (Rem,  "rem")

diff --git a/Data/SBV/SMT/SMTLib2.hs b/Data/SBV/SMT/SMTLib2.hs
@@ -884,8 +884,9 @@ cvtExp curProgInfo caps rm tableMap expr@(SBVApp _ arguments) = sh expr
 
         sh (SBVApp (KindCast f t) [a]) = handleKindCast hasInt2bv f t (cvtSV a)
 
-        sh (SBVApp ReadArray  [a, i])    = "(select " ++ cvtSV a ++ " " ++ cvtSV i ++ ")"
-        sh (SBVApp WriteArray [a, i, v]) = "(store "  ++ cvtSV a ++ " " ++ cvtSV i ++ " " ++ cvtSV v ++ ")"
+        sh (SBVApp (ArrayLambda s) [])        = s
+        sh (SBVApp ReadArray       [a, i])    = "(select " ++ cvtSV a ++ " " ++ cvtSV i ++ ")"
+        sh (SBVApp WriteArray      [a, i, e]) = "(store "  ++ cvtSV a ++ " " ++ cvtSV i ++ " " ++ cvtSV e ++ ")"
 
         sh (SBVApp (Uninterpreted nm) [])   = nm
         sh (SBVApp (Uninterpreted nm) args) = "(" ++ nm ++ " " ++ unwords (map cvtSV args) ++ ")"