Hackage :: [Package]

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

[ bsd3, formal-languages, language, library, smt ] [ Propose Tags ] [ Report a vulnerability ]

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 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 [email protected]
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:59Z
Distributions NixOS:0.1.0.1
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 1061 total (2 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs uploaded by user [build log]
All reported builds failed as of 2020-12-02 [all 2 reports]

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

OSZAR »