smt2-parser

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

Usage

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.

Footnotes

1. 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 www.SMT-LIB.org ↩