LIBCVC4(3)                  CVC4 Library Interfaces                 LIBCVC4(3)

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  2023-09-01                        LIBCVC4(3)