The yices-painless package

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 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.

More information about Yices:

http://yices.csl.sri.com/

Low and medium-level bindings to the Yices C API are also provided. The medium-level bindings add significant type and resource safety to that which the C API provides.

Properties

Versions	0.1, 0.1.1, 0.1.2
Dependencies	base (>3 & <5), containers (≥0.2), pretty, strict-concurrency, vector (≥0.7)
License	BSD3
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
Upload date	Sat Jan 15 21:48:10 UTC 2011
Uploaded by	DonaldStewart
Build failure	ghc-7.0 (log)

Modules

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

Downloads

yices-painless-0.1.tar.gz (Cabal source package)
package description (included in the package)