yices-painless: An embedded language for programming the Yices SMT solver

[ bsd3, formal-methods, library, math, theorem-provers ] [ Propose Tags ]

This library defines an embedded language in Haskell for programming the Yices SMT solver.

Yices is an efficient SMT solver that decides the satisfiability of arbitrary formulas containing uninterpreted function symbols with equality, linear real and integer arithmetic, scalar types, recursive datatypes, tuples, records, extensional arrays, fixed-size bit-vectors, quantifiers, and lambda expressions. Yices also does MaxSMT (and, dually, unsat cores) and is competitive as an ordinary SAT and MaxSAT solver.

The embedded language embeds both terms, functions and types into Haskell, via a typed higher-order abstract syntax representation. Propositions in the embedding are represented as (typed) pure expressions.

Solution variables in the proposition (notionally, free variables) are bound an the outermost lambda term. Propositions constructed from logical primitives can then be executed by the solver to yield a satisfying assignment to those free variables in the proposition. Uninterpreted functions may be introduced via variables as well.

More information about Yices:

The primary interface is via the EDSL, Yices.Painless.Language, however, low and medium-level bindings to the Yices C API are also provided (Yices.Painless.Base.C and Yices.Painless.Base). The medium-level bindings add significant type and resource safety to that which the C API provides.

Documentation for this package is available:


  • Yices
    • Painless
      • Yices.Painless.Base
        • Yices.Painless.Base.C
      • Yices.Painless.Language
      • Yices.Painless.Tuple
      • Yices.Painless.Type


Automatic Flags

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


Maintainer's Corner

Package maintainers

For package maintainers and hackage trustees


  • No Candidates
Versions [RSS] 0.1, 0.1.1, 0.1.2
Dependencies base (>3 && <5), containers (>=0.2), pretty, strict-concurrency, vector (>=0.7) [details]
License BSD-3-Clause
Copyright Don Stewart 2010.
Author Don Stewart
Maintainer dons@galois.com
Category Math, Theorem Provers, Formal Methods
Home page http://code.haskell.org/~dons/code/yices-painless
Uploaded by DonaldStewart at 2011-01-17T22:46:47Z
Reverse Dependencies 1 direct, 0 indirect [details]
Downloads 2463 total (11 in the last 30 days)
Rating (no votes yet) [estimated by Bayesian average]
Your Rating
  • λ
  • λ
  • λ
Status Docs not available [build log]
All reported builds failed as of 2016-12-28 [all 12 reports]