1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80

Name: yicespainless
Version: 0.1.2
Synopsis: An embedded language for programming the Yices SMT solver
Description:
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, fixedsize
bitvectors, 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 higherorder 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:
.
* <http://yices.csl.sri.com/>
.
The primary interface is via the EDSL, "Yices.Painless.Language",
however, low and mediumlevel bindings to the Yices C API are also provided
("Yices.Painless.Base.C" and "Yices.Painless.Base"). The
mediumlevel bindings add significant type and resource safety to
that which the C API provides.
.
Documentation for this package is available:
.
* <http://www.galois.com/~dons/yicespainless/>
.
Homepage: http://code.haskell.org/~dons/code/yicespainless
License: BSD3
Licensefile: LICENSE
Author: Don Stewart
Maintainer: dons@galois.com
Copyright: Don Stewart 2010.
Category: Math, Theorem Provers, Formal Methods
Buildtype: Simple
Cabalversion: >=1.2
Flag yicesdynamic
default: True
Library
Exposedmodules:
Yices.Painless.Language
Yices.Painless.Base
Yices.Painless.Base.C
Yices.Painless.Type
Yices.Painless.Tuple
ghcoptions: Wall
Builddepends: base > 3 && < 5,
pretty,
strictconcurrency,
containers >= 0.2,
vector >= 0.7
Buildtools: hsc2hs
Extensions: ForeignFunctionInterface
includes: yices_c.h
extralibraries: yices
if flag(yicesdynamic)
extralibraries: gmp
