Skip to content

Commit

Permalink
compress spaces before computing the hash
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Dec 25, 2024
1 parent 1bb3738 commit ba6cfba
Showing 1 changed file with 4 additions and 1 deletion.
5 changes: 4 additions & 1 deletion Data/SBV/SMT/SMTLib2.hs
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ import qualified Data.Graph as DG
-- | For higher-order functions, we firstify them. This requires a uniqu name creation. Here,
-- we create a firstified name based on the operation. The suffix appended will have at most uniqLen length.
firstify :: Int -> Op -> String
firstify uniqLen o = prefix o ++ "_" ++ take uniqLen (BC.unpack (B.encode (hash (BC.pack (show o)))))
firstify uniqLen o = prefix o ++ "_" ++ take uniqLen (BC.unpack (B.encode (hash (BC.pack (compress (show o))))))
where prefix (SeqOp SBVReverse {}) = "sbv.reverse"
prefix (SeqOp SBVZip {}) = "sbv.zip"
prefix (SeqOp SBVZipWith {}) = "sbv.zipWith"
Expand All @@ -68,6 +68,9 @@ firstify uniqLen o = prefix o ++ "_" ++ take uniqLen (BC.unpack (B.encode (hash
, "*** Please report this as a bug."
]

-- compress and make spaces uniform; get words, and then unwords
compress = unwords . words

-- | Translate a problem into an SMTLib2 script
cvt :: SMTLibConverter ([String], [String])
cvt ctx curProgInfo kindInfo isSat comments allInputs (_, consts) tbls uis defs (SBVPgm asgnsSeq) cstrs out cfg = (pgm, exportedDefs)
Expand Down

0 comments on commit ba6cfba

Please sign in to comment.