1 .\" Process this file with
2 .\" groff -man -Tascii libcvc4.3
4 .TH LIBCVC4 3 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces"
6 libcvc4 \- a library interface for the CVC4 theorem prover
14 #include "expr/expr_manager.h"
15 #include "smt/smt_engine.h"
22 Expr onePlusTwo = em.mkExpr(kind::PLUS,
23 em.mkConst(Rational(1)),
24 em.mkConst(Rational(2)));
25 std::cout << language::SetLanguage(language::output::LANG_CVC4)
26 << smt.getInfo("name")
27 << " says that 1 + 2 = "
28 << smt.simplify(onePlusTwo)
39 "cvc4" says that 1 + 2 = 3
44 The main classes of interest in CVC4's API are
47 and a few related ones like
54 is used to build up expressions and types, and the
56 is used primarily to make assertions, check satisfiability/validity, and extract models and proofs.
62 Additionally, the CVC4 wiki contains useful information about the
63 design and internals of CVC4. It is maintained at
64 .BR http://cvc4.cs.stanford.edu/wiki/ .