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:

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