.\" Process this file with
.\" groff -man -Tascii libcvc4.3
.\"
.TH LIBCVC4 3 "2020-10-25" "CVC4 release CVC4_RELEASE_STRING" "CVC4 Library Interfaces"
.SH NAME
libcvc4 \- a library interface for the CVC4 theorem prover
.SH SYNOPSIS

A small program like:

.RS
.nf
#include <iostream>
#include "expr/expr_manager.h"
#include "smt/smt_engine.h"

using namespace CVC4;

int main() {
  ExprManager em;
  SmtEngine smt(&em);
  Expr onePlusTwo = em.mkExpr(kind::PLUS,
                              em.mkConst(Rational(1)),
                              em.mkConst(Rational(2)));
  std::cout << language::SetLanguage(language::output::LANG_CVC4)
            << smt.getInfo("name")
            << " says that 1 + 2 = "
            << smt.simplify(onePlusTwo)
            << std::endl;

  return 0;
}
.fi
.RE

gives the output:

.RS
"cvc4" says that 1 + 2 = 3
.RE

.SH DESCRIPTION

The main classes of interest in CVC4's API are
.I ExprManager,
.I SmtEngine,
and a few related ones like
.I Expr
and
.I Type.

The
.I ExprManager
is used to build up expressions and types, and the
.I SmtEngine
is used primarily to make assertions, check satisfiability/validity, and extract models and proofs.

.SH "SEE ALSO"
.BR cvc4 (1),
.BR libcvc4parser (3)

Additionally, the CVC4 wiki contains useful information about the
design and internals of CVC4.  It is maintained at
.BR http://cvc4.cs.stanford.edu/wiki/ .