libcvc4 man page

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

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

Referenced By

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

July 2014 CVC4 release 1.4 CVC4 Library Interfaces