smtlib-tools

Programs for working with SMT-LIB files

git clone https://git.8pit.net/smtlib-tools.git

  1module Main where
  2
  3import Data.Map.Strict qualified as Map
  4import Control.Monad (forM_)
  5import Control.Monad.State.Strict (State, modify, runState)
  6import SimpleSMT qualified as SMT
  7import System.IO (stdin, hGetContents)
  8
  9type Stats = Map.Map String Int
 10
 11mkStats :: Stats
 12mkStats = Map.empty
 13
 14toCSV :: Stats -> String
 15toCSV e =
 16  unlines $ header : map go (Map.toList e)
 17  where
 18    seperator :: String
 19    seperator = ";"
 20
 21    header :: String
 22    header = "name" ++ seperator ++ "occurrence"
 23
 24    go :: (String, Int) -> String
 25    go (n, c) = "\"" ++ n ++ "\"" ++ seperator ++ show c
 26
 27------------------------------------------------------------------------
 28
 29collectName :: String -> State Stats ()
 30collectName name =
 31  modify $ Map.insertWith (+) name 1
 32
 33collectBinary :: String -> SMT.SExpr -> SMT.SExpr -> State Stats ()
 34collectBinary name lhs rhs = do
 35  collectName name
 36  collectExpr lhs >> collectExpr rhs
 37
 38collectExpr :: SMT.SExpr -> State Stats ()
 39collectExpr (SMT.List (SMT.Atom "=" : values))
 40  = forM_ values collectExpr
 41collectExpr (SMT.List [SMT.Atom "or", lhs, rhs]) = collectBinary "or" lhs rhs
 42collectExpr (SMT.List [SMT.Atom "not", p]) = collectName "not" >> collectExpr p
 43collectExpr (SMT.List [SMT.Atom "bvneg", p]) = collectName "bvneg" >> collectExpr p
 44collectExpr (SMT.List [SMT.List [SMT.Atom "_", SMT.Atom "extract", _, _], expr])
 45  = collectName "extract" >> collectExpr expr
 46collectExpr (SMT.List [SMT.List [SMT.Atom "_", SMT.Atom "zero_extend", _], expr])
 47  = collectName "zero_extend" >> collectExpr expr
 48collectExpr (SMT.List [SMT.List [SMT.Atom "_", SMT.Atom "sign_extend", _], expr])
 49  = collectName "sign_extend" >> collectExpr expr
 50collectExpr (SMT.List [SMT.Atom "ite", cond, ifT, ifF]) = do
 51  collectName "ite"
 52  collectExpr cond >> collectExpr ifT >> collectExpr ifF
 53collectExpr (SMT.List [SMT.Atom "select", lhs, rhs]) = collectBinary "select" lhs rhs
 54collectExpr (SMT.List [SMT.Atom "and", lhs, rhs]) = collectBinary "and" lhs rhs
 55collectExpr (SMT.List [SMT.Atom "concat", lhs, rhs]) = collectBinary "concat" lhs rhs
 56collectExpr (SMT.List [SMT.Atom "bvadd", lhs, rhs]) = collectBinary "bvadd" lhs rhs
 57collectExpr (SMT.List [SMT.Atom "bvsub", lhs, rhs]) = collectBinary "bvsub" lhs rhs
 58collectExpr (SMT.List [SMT.Atom "bvmul", lhs, rhs]) = collectBinary "bvmul" lhs rhs
 59collectExpr (SMT.List [SMT.Atom "bvsdiv", lhs, rhs]) = collectBinary "bvsdiv" lhs rhs
 60collectExpr (SMT.List [SMT.Atom "bvudiv", lhs, rhs]) = collectBinary "bvudiv" lhs rhs
 61collectExpr (SMT.List [SMT.Atom "bvxor", lhs, rhs]) = collectBinary "bvxor" lhs rhs
 62collectExpr (SMT.List [SMT.Atom "bvand", lhs, rhs]) = collectBinary "bvand" lhs rhs
 63collectExpr (SMT.List [SMT.Atom "bvor", lhs, rhs]) = collectBinary "bvor" lhs rhs
 64collectExpr (SMT.List [SMT.Atom "bvurem", lhs, rhs]) = collectBinary "bvurem" lhs rhs
 65collectExpr (SMT.List [SMT.Atom "bvsrem", lhs, rhs]) = collectBinary "bvsrem" lhs rhs
 66collectExpr (SMT.List [SMT.Atom "bvashr", lhs, rhs]) = collectBinary "bvashr" lhs rhs
 67collectExpr (SMT.List [SMT.Atom "bvlshr", lhs, rhs]) = collectBinary "bvlshr" lhs rhs
 68collectExpr (SMT.List [SMT.Atom "bvshl", lhs, rhs]) = collectBinary "bvshl" lhs rhs
 69collectExpr (SMT.List [SMT.Atom "bvsle", lhs, rhs]) = collectBinary "bvsle" lhs rhs
 70collectExpr (SMT.List [SMT.Atom "bvslt", lhs, rhs]) = collectBinary "bvslt" lhs rhs
 71collectExpr (SMT.List [SMT.Atom "bvsge", lhs, rhs]) = collectBinary "bvsge" lhs rhs
 72collectExpr (SMT.List [SMT.Atom "bvsgt", lhs, rhs]) = collectBinary "bvsgt" lhs rhs
 73collectExpr (SMT.List [SMT.Atom "bvule", lhs, rhs]) = collectBinary "bvule" lhs rhs
 74collectExpr (SMT.List [SMT.Atom "bvult", lhs, rhs]) = collectBinary "bvult" lhs rhs
 75collectExpr (SMT.List [SMT.Atom "bvuge", lhs, rhs]) = collectBinary "bvuge" lhs rhs
 76collectExpr (SMT.List [SMT.Atom "bvugt", lhs, rhs]) = collectBinary "bvugt" lhs rhs
 77collectExpr (SMT.Atom _) = pure ()
 78collectExpr (SMT.List [SMT.Atom "_", SMT.Atom _, SMT.Atom _]) = pure ()
 79collectExpr e = error $ "collectExpr: Unknown expression '" ++ show e ++ "'"
 80
 81collectCmd :: SMT.SExpr -> State Stats ()
 82collectCmd (SMT.List [SMT.Atom "check-sat-assuming", SMT.List assumptions])
 83  = collectName "check-sat-assuming" >> forM_ assumptions collectExpr
 84collectCmd (SMT.List ((SMT.Atom "set-logic") : _)) = pure ()
 85collectCmd (SMT.List ((SMT.Atom "declare-fun") : _)) = pure ()
 86collectCmd (SMT.List (SMT.Atom "check-sat":_)) = collectName "check-sat" >> pure ()
 87collectCmd (SMT.List (SMT.Atom "pop":_)) = pure ()
 88collectCmd (SMT.List (SMT.Atom "push":_)) = pure ()
 89collectCmd (SMT.List [SMT.Atom "assert", expr]) = collectExpr expr
 90collectCmd cmd = error $ "collectCmd: Unknown command '" ++ show cmd ++ "'"
 91
 92collect :: [SMT.SExpr] -> State Stats ()
 93collect sexprs = forM_ sexprs collectCmd
 94
 95------------------------------------------------------------------------
 96
 97readSExprs :: String -> [SMT.SExpr]
 98readSExprs str = go (SMT.readSExpr str)
 99  where
100    go :: Maybe (SMT.SExpr, String) -> [SMT.SExpr]
101    go Nothing = []
102    go (Just (acc, rest)) = acc : go (SMT.readSExpr rest)
103
104getStats :: [SMT.SExpr] -> Stats
105getStats exprs = snd $ collectStats exprs
106  where
107    collectStats e = runState (collect e) mkStats
108
109------------------------------------------------------------------------
110
111main :: IO ()
112main = do
113  exprs <- readSExprs <$> hGetContents stdin
114  putStr (toCSV $! getStats exprs)