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  de‐
50       sign  and  internals of CVC4.  It is maintained at http://cvc4.cs.stan‐
51       ford.edu/wiki/.
52
53
54
55CVC4 release CVC4_RELEASE_STRING  2021-06-02                        LIBCVC4(3)