---
name: "libcvc4"
section: "3"
platform: "linux"
package: "cvc4"
version: "1.8-3"
release: "Arch Linux 2026-11-01"
platforms: ["linux"]
url: "https://new.carta.tech/libcvc4"
---

# libcvc4(3)

a library interface for the CVC4 theorem prover

## 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)](/cvc4/1.md), [**libcvc4parser**(3)](/libcvc4parser/3.md)

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