smt2-parser: A Haskell parser for SMT-LIB version 2.6

This is a package candidate release! Here you can preview how this package release will appear once published to the main package index (which can be accomplished via the 'maintain' link below). Please note that once a package has been published to the main package index it cannot be undone! Please consult the package uploading documentation for more information.

[maintain] [Publish]

Please see the README on GitHub at

[Skip to Readme]


Change log
Dependencies base (>=4.13.0 && <5), parsec (>=3.1.14), text (>=1.2.4) [details]
License BSD-3-Clause
Copyright 2020 crvdgc
Author crvdgc
Category SMT, Formal Languages, Language
Home page
Bug tracker
Source repo head: git clone
Uploaded by liuyuxi at 2022-10-08T09:29:56Z


[Index] [Quick Jump]


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for smt2-parser-

[back to package description]


A Haskell parser for SMT-LIB version 2.6 1. The language reference is available in pdf.


Run a parser with an input string:

-- parseStringEof :: Parser a -> T.Text -> Either ParseError a

parseStringEof numeral "0" === Right ("0" :: Numeral)
parseStringEof identifier "(_ BitVec 32)" === Right (IdIndexed ("BitVec" :: Symbol) (fromList [IxNumeral "32"]))

Run a parser from a file string, possibly leading and trailing by spaces and having comments

-- parseFileMsg :: Parser a -> T.Text -> Either T.Text a
>>> parseFileMsg script (T.pack "(set-logic HORN)\n\n(declare-fun |sum$unknown:2|\n  ( Int Int ) Bool\n)\n(assert\n  (forall ( (|$V-reftype:10| Int) (|$alpha-1:n| Int) (|$knormal:1| Int) (|$knormal:2| Int) (|$knormal:3| Int) )\n    (=>\n      ( and (= |$knormal:2| (- |$alpha-1:n| 1)) (= (not (= 0 |$knormal:1|)) (<= |$alpha-1:n| 0)) (= |$V-reftype:10| (+ |$alpha-1:n| |$knormal:3|)) (not (not (= 0 |$knormal:1|))) (|sum$unknown:2| |$knormal:3| |$knormal:2|) true )\n      (|sum$unknown:2| |$V-reftype:10| |$alpha-1:n|)\n    )\n  )\n)(check-sat)")

Right [ SetLogic "HORN"
      , DeclareFun "sum$unknown:2" [SortSymbol (IdSymbol "Int"),...] (SortSymbol (IdSymbol "Bool"))
      , Assert (TermForall ...)
      , CheckSat

Known Issue

removeComment may cause performance issue. Use parseCommentFreeFileMsg on a preprocessed comment-free file instead.


Barrett, Clarke, Pascal Fontaine and Cesare Tinelli. The SMT-LIB Standard: Version 2.6. Technical Report BarFT-RR-17, Department of Computer Science, The University of Iowa, 2017. Available at