libcvc4 man page

libcvc4 — a library interface for the CVC4 theorem prover


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,
  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


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), libcvc4compat(3)

Additionally, the CVC4 wiki contains useful information about the design and internals of CVC4.  It is maintained at

Referenced By

cvc4(1), cvc4(5), libcvc4compat(3), libcvc4parser(3), options.3cvc(3), SmtEngine.3cvc(3).

August 2017 CVC4 release 1.5 CVC4 Library Interfaces