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/.

CVC4 release CVC4_RELEASE_STRING                   2024-03-31                                         LIBCVC4(3)