blob: 99b0451f67a6ad79b8f062293daccda17a43ed36 (
plain)
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
|
.\" Process this file with
.\" groff -man -Tascii SmtEngine.3cvc4
.\"
.TH SMTENGINE 3cvc4 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces"
.SH NAME
SmtEngine \- the primary interface to CVC4's theorem-proving capabilities
.SH DESCRIPTION
.B SmtEngine
is the main entry point into the CVC4 theorem prover API.
.SH SMTENGINE OPTIONS
The SmtEngine is in charge of setting and getting information and options.
Numerous options are available via the
.I SmtEngine::setOption()
call.
.I SmtEngine::setOption()
and
.I SmtEngine::getOption()
use the following option keys.
.RS
.TP 10
.I "COMMON OPTIONS"
${common_manpage_smt_documentation}
${remaining_manpage_smt_documentation}
.PD
.RE
.SH VERSION
This manual page refers to
.B CVC4
version @VERSION@.
.SH BUGS
A Bugzilla for the CVC4 project is maintained at
.BR http://church.cims.nyu.edu/bugzilla3/ .
.SH AUTHORS
.B CVC4
is developed by a team of researchers at New York University
and the University of Iowa.
See the AUTHORS file in the distribution for a full list of
contributors.
.SH "SEE ALSO"
.BR libcvc4 (3),
.BR libcvc4parser (3),
.BR libcvc4compat (3)
Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4. It is maintained at
.BR http://church.cims.nyu.edu/wiki/ .
|
