doc/libcvc4.3.in

   1 .\" Process this file with
   2 .\" groff -man -Tascii libcvc4.3
   3 .\"
   4 .TH LIBCVC4 3 "@MAN_DATE@" "CVC4 release @VERSION@" "CVC4 Library Interfaces"
   5 .SH NAME
   6 libcvc4 \- a library interface for the CVC4 theorem prover
   7 .SH SYNOPSIS
   8
   9 A small program like:
  10
  11 .RS
  12 .nf
  13 #include <iostream>
  14 #include "expr/expr_manager.h"
  15 #include "smt/smt_engine.h"
  16
  17 using namespace CVC4;
  18
  19 int main() {
  20   ExprManager em;
  21   SmtEngine smt(&em);
  22   Expr onePlusTwo = em.mkExpr(kind::PLUS,
  23                               em.mkConst(Rational(1)),
  24                               em.mkConst(Rational(2)));
  25   std::cout << language::SetLanguage(language::output::LANG_CVC4)
  26             << smt.getInfo("name")
  27             << " says that 1 + 2 = "
  28             << smt.simplify(onePlusTwo)
  29             << std::endl;
  30
  31   return 0;
  32 }
  33 .fi
  34 .RE
  35
  36 gives the output:
  37
  38 .RS
  39 "cvc4" says that 1 + 2 = 3
  40 .RE
  41
  42 .SH DESCRIPTION
  43
  44 The main classes of interest in CVC4's API are
  45 .I ExprManager,
  46 .I SmtEngine,
  47 and a few related ones like
  48 .I Expr
  49 and
  50 .I Type.
  51
  52 The
  53 .I ExprManager
  54 is used to build up expressions and types, and the
  55 .I SmtEngine
  56 is used primarily to make assertions, check satisfiability/validity, and extract models and proofs.
  57
  58 .SH "SEE ALSO"
  59 .BR cvc4 (1),
  60 .BR libcvc4parser (3)
  61
  62 Additionally, the CVC4 wiki contains useful information about the
  63 design and internals of CVC4.  It is maintained at
  64 .BR http://cvc4.cs.stanford.edu/wiki/ .