Hackage :: [Package]

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 https://github.com/crvdgc/smt2-parser#readme

[Skip to Readme]

Properties

Versions 0.1.0.0, 0.1.0.0, 0.1.0.1
Change log ChangeLog.md
Dependencies base (>=4.13.0 && <4.14), parsec (>=3.1.14 && <3.2), text (>=1.2.4 && <1.3) [details]
License BSD-3-Clause
Copyright 2020 crvdgc
Author crvdgc
Maintainer 2502project@gmail.com
Category SMT, Formal Languages, Language
Home page https://github.com/crvdgc/smt2-parser#readme
Bug tracker https://github.com/crvdgc/smt2-parser/issues
Source repo head: git clone https://github.com/crvdgc/smt2-parser
Uploaded by liuyuxi at 2020-12-02T13:24:06Z

Modules

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Readme for smt2-parser-0.1.0.0

[back to package description]

smt2-parser

A Haskell parser for SMT-LIB version 2.6 1. 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.

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