doc/mainpage.md

   1 /**
   2 \mainpage Getting started with the CVC4 API
   3
   4 The main classes of the CVC4 API are:
   5 - CVC4::Expr - an expression (a formula, term, variable, constant, etc.)
   6 - CVC4::Type - a type (every Expr has a Type)
   7 - CVC4::ExprManager - a factory class for Exprs and Types (create one of these for your application)
   8 - CVC4::SmtEngine - the SMT interface, permits making assertions and checking satisfiability (create one of these for your application)
   9
  10 There are numerous examples of the use of the C++ API in the examples/api directory of the CVC4 source distribution.  There is also a discussion on our CVC4 Wiki at
  11 http://cvc4.cs.stanford.edu/wiki/Tutorials#C.2B.2B_API
  12
  13 Using the CVC4 API from Java
  14
  15 While these API documentation resources explicitly refer to the C++ interface, the Java interface is generated automatically from the C++ sources by SWIG, and thus the interface is almost line-by-line identical in Java.  It is possible, then, to use these C++ resources to help with the Java API.  There are three main ways in which the Java API differs from the C++ API.  First, the CVC4 API makes moderate use of C++ operator overloading, which is not possible in Java.  We have provided standard renamings for the Java methods associated to these C++ overloaded operators---for instance, "plus" replaces operator+, "equals" replaces operator==, etc.
  16
  17 Secondly, C++ iterators are replaced by Java iterators.  Instead of begin() and end() on classes like CVC4::Expr, you'll notice in the Java interface that there is an iterator() method that returns a java.util.Iterator<Expr>.  This allows Java developers to more naturally work with our (ultimately C++) objects through a more Java-like interface.
  18
  19 Third, I/O streams are wrapped so that some functions requiring C++ input and output streams will accept Java InputStreams and OutputStreams.
  20
  21 Our intent is to make the C++ API as useful and functional for Java developers as possible, while still retaining the flexibility of our original C++ design.  If we can make your life as a Java user of our libraries easier, please let us know by requesting an enhancement or reporting a bug at our bug-tracking service, https://github.com/CVC4/CVC4/issues.
  22
  23 For examples of Java programs using the CVC4 API, look in the directory examples/api/java in the CVC4 source distribution.
  24
  25 Thank you for your interest in CVC4!
  26
  27 The CVC4 Development team
  28
  29 \page authors AUTHORS
  30 \verbinclude AUTHORS
  31 \page copying COPYING
  32 \verbinclude COPYING
  33 \page install INSTALL
  34 \verbinclude INSTALL
  35 \page news NEWS
  36 \verbinclude NEWS
  37 \page release-notes RELEASE-NOTES
  38 \verbinclude RELEASE-NOTES
  39 \page readme README
  40 \verbinclude README
  41 \page thanks THANKS
  42 \verbinclude THANKS
  43 */