1LIBCVC4(3)                  CVC4 Library Interfaces                 LIBCVC4(3)
2
3
4

NAME

6       libcvc4 - a library interface for the CVC4 theorem prover
7

SYNOPSIS

9       A small program like:
10
11              #include <iostream>
12              #include "expr/expr_manager.h"
13              #include "smt/smt_engine.h"
14
15              using namespace CVC4;
16
17              int main() {
18                ExprManager em;
19                SmtEngine smt(&em);
20                Expr onePlusTwo = em.mkExpr(kind::PLUS,
21                                            em.mkConst(Rational(1)),
22                                            em.mkConst(Rational(2)));
23                std::cout << language::SetLanguage(language::output::LANG_CVC4)
24                          << smt.getInfo("name")
25                          << " says that 1 + 2 = "
26                          << smt.simplify(onePlusTwo)
27                          << std::endl;
28
29                return 0;
30              }
31
32       gives the output:
33
34              "cvc4" says that 1 + 2 = 3
35
36

DESCRIPTION

38       The  main classes of interest in CVC4's API are ExprManager, SmtEngine,
39       and a few related ones like Expr and Type.
40
41       The ExprManager is used to build up  expressions  and  types,  and  the
42       SmtEngine  is  used  primarily  to  make assertions, check satisfiabil‐
43       ity/validity, and extract models and proofs.
44
45

SEE ALSO

47       cvc4(1), libcvc4parser(3)
48
49       Additionally, the CVC4  wiki  contains  useful  information  about  the
50       design and internals of CVC4.  It is maintained at http://cvc4.cs.stan‐
51       ford.edu/wiki/.
52
53
54
55CVC4 release CVC4_RELEASE_STRING  2020-01-28                        LIBCVC4(3)