smtlib2: A type-safe interface to communicate with an SMT solver.

[ formal-methods, gpl, library, smt, symbolic-computation, theorem-provers ] [ Propose Tags ]

Modules

[Last Documentation]

  • Data
    • Data.Unit
  • Language
    • Language.SMTLib2
      • Language.SMTLib2.Connection
      • Language.SMTLib2.Internals
        • Language.SMTLib2.Internals.Instances
        • Language.SMTLib2.Internals.Interface
        • Language.SMTLib2.Internals.Operators
        • Language.SMTLib2.Internals.Optimize
      • Language.SMTLib2.Pipe
      • Language.SMTLib2.Solver
      • Language.SMTLib2.Strategy

Flags

Automatic Flags
NameDescriptionDefault
withconstraints

Enables the use of the constraint-kind extension which is needed to parse map-expressions.

Enabled
withdatakinds

Enables the use of the data-kinds extension which is needed for typed bitvectors.

Disabled

Use -f <flag> to enable a flag, or -f -<flag> to disable that flag. More info

Downloads

Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees

Candidates

Versions [RSS] 0.1, 0.2, 0.3, 0.3.1, 1.0
Dependencies array, atto-lisp (>=0.2), attoparsec, base (>=4 && <5), blaze-builder, bytestring, constraints, containers, data-fix, mtl, process, tagged, text, transformers [details]
License GPL-3.0-only
Author Henning Günther <guenther@forsyte.at>
Maintainer guenther@forsyte.at
Category SMT, Formal Methods, Theorem Provers, Symbolic Computation
Source repo head: git clone https://github.com/hguenther/smtlib2.git
Uploaded by HenningGuenther at 2014-12-07T15:05:12Z
Distributions
Reverse Dependencies 6 direct, 8 indirect [details]
Downloads 4307 total (13 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-12 [all 6 reports]