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

[ formal-methods, gpl, library, smt, symbolic-computation, theorem-provers ] [ Propose Tags ]
Versions [faq] 0.1, 0.2, 0.3, 0.3.1, 1.0
Dependencies array, atto-lisp (>=0.2), attoparsec, base (==4.*), 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 NixOS:1.0
Downloads 3586 total (3 in the last 30 days)
Rating 2.0 (votes: 1) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Hackage Matrix CI
Docs not available [build log]
All reported builds failed as of 2016-12-12 [all 6 reports]

Modules

  • 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

NameDescriptionDefaultType
withconstraints

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

EnabledAutomatic
withdatakinds

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

DisabledAutomatic

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

Downloads

Maintainer's Corner

For package maintainers and hackage trustees