NAME

       libcvc4 - a library interface for the CVC4 theorem prover

SYNOPSIS

       A small program like:

              #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;
              }

       gives the output:

              "cvc4" says that 1 + 2 = 3

DESCRIPTION

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

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

SEE ALSO

       cvc4(1), libcvc4parser(3)

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