forked from clconway/cvc3-debian
-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathcontrol
203 lines (197 loc) · 8.63 KB
/
control
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
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
Source: cvc3
Section: math
Priority: extra
Maintainer: Morgan Deters <[email protected]>
Build-Depends: cdbs, debhelper (>= 7), autoconf, autotools-dev, bison, default-jdk, flex, libgmp-dev | libgmp3-dev, patchutils, python
Standards-Version: 3.9.5
Homepage: http://www.cs.nyu.edu/acsys/cvc3/
Package: cvc3
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}
Description: Automatic theorem prover for SMT problems
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories
(SMT) problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in
logical theories and their combination.
.
CVC3 is the last offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular,
it builds on the code base of CVC Lite, its most recent
predecessor. Its high level design follows that of the Sammy prover.
.
CVC3 works with a version of first-order logic with polymorphic types
and has a wide variety of features including:
.
* several built-in base theories: rational and integer linear
arithmetic, arrays, tuples, records, inductive data types, bit
vectors, and equality over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* rich C, C++, and Java APIs for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial
purposes (see license).
.
This package contains the CVC3 command line program.
Package: libcvc3-5
Section: libs
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}
Description: Automatic theorem prover library for SMT problems
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories
(SMT) problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in
logical theories and their combination.
.
CVC3 is the last offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular,
it builds on the code base of CVC Lite, its most recent
predecessor. Its high level design follows that of the Sammy prover.
.
CVC3 works with a version of first-order logic with polymorphic types
and has a wide variety of features including:
.
* several built-in base theories: rational and integer linear
arithmetic, arrays, tuples, records, inductive data types, bit
vectors, and equality over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* rich C, C++, and Java APIs for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial
purposes (see license).
.
This package contains the files necessary for running applications
that use the CVC3 library.
Package: libcvc3-dev
Section: libdevel
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}, libcvc3-5 (= ${binary:Version})
Replaces: libcvc3-5-dev, libcvc3-2-dev
Breaks: libcvc3-5-dev, libcvc3-2-dev
Description: Automatic theorem prover library for SMT problems (development files)
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories
(SMT) problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in
logical theories and their combination.
.
CVC3 is the last offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular,
it builds on the code base of CVC Lite, its most recent
predecessor. Its high level design follows that of the Sammy prover.
.
CVC3 works with a version of first-order logic with polymorphic types
and has a wide variety of features including:
.
* several built-in base theories: rational and integer linear
arithmetic, arrays, tuples, records, inductive data types, bit
vectors, and equality over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* rich C, C++, and Java APIs for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial
purposes (see license).
.
This package contains the files necessary for building applications
that use the CVC3 library.
Package: libcvc3-5-java
Section: java
Architecture: all
Depends: ${shlibs:Depends}, ${misc:Depends}, libcvc3-5-jni (>= ${source:Version})
Description: Java bindings for CVC3 (bytecode library)
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories
(SMT) problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in
logical theories and their combination.
.
CVC3 is the last offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular,
it builds on the code base of CVC Lite, its most recent
predecessor. Its high level design follows that of the Sammy prover.
.
CVC3 works with a version of first-order logic with polymorphic types
and has a wide variety of features including:
.
* several built-in base theories: rational and integer linear
arithmetic, arrays, tuples, records, inductive data types, bit
vectors, and equality over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* rich C, C++, and Java APIs for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial
purposes (see license).
.
This package provides architecture-independent files of the Java
bindings for CVC3
Package: libcvc3-5-jni
Section: java
Architecture: any
Depends: ${shlibs:Depends}, ${misc:Depends}
Replaces: libcvc3-2-jni
Breaks: libcvc3-2-jni
Description: Java bindings for CVC3 (native library)
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories
(SMT) problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in
logical theories and their combination.
.
CVC3 is the last offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular,
it builds on the code base of CVC Lite, its most recent
predecessor. Its high level design follows that of the Sammy prover.
.
CVC3 works with a version of first-order logic with polymorphic types
and has a wide variety of features including:
.
* several built-in base theories: rational and integer linear
arithmetic, arrays, tuples, records, inductive data types, bit
vectors, and equality over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* rich C, C++, and Java APIs for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial
purposes (see license).
.
This package provides the native library needed for the Java bindings
for CVC3
Package: cvc3-el
Architecture: all
Depends: emacs | emacsen, ${misc:Depends}
Recommends: cvc3
Enhances: cvc3
Description: Emacs mode for CVC3
CVC3 is an automatic theorem prover for Satisfiability Modulo Theories
(SMT) problems. It can be used to prove the validity (or, dually, the
satisfiability) of first-order formulas in a large number of built-in
logical theories and their combination.
.
CVC3 is the last offspring of a series of popular SMT provers, which
originated at Stanford University with the SVC system. In particular,
it builds on the code base of CVC Lite, its most recent
predecessor. Its high level design follows that of the Sammy prover.
.
CVC3 works with a version of first-order logic with polymorphic types
and has a wide variety of features including:
.
* several built-in base theories: rational and integer linear
arithmetic, arrays, tuples, records, inductive data types, bit
vectors, and equality over uninterpreted function symbols;
* support for quantifiers;
* an interactive text-based interface;
* rich C, C++, and Java APIs for embedding in other systems;
* proof and model generation abilities;
* predicate subtyping;
* essentially no limit on its use for research or commercial
purposes (see license).
.
The package provides an Emacs major mode "cvc3-mode" with syntax
highlighting for the CVC3 input language and running CVC3 as an
inferior process.