API documentation improvements.

diff --git a/.gitignore b/.gitignore
index b3cce03ed95cb408252370ec0ea79c39803cbd28..b63d4c851efda56776a4884cc51a7a511e8a0190 100644 (file)
--- a/.gitignore
+++ b/.gitignore
@@ -10,7 +10,7 @@
 /cvc4-*.tar.gz
 /cvc4-*.tar.bz2
 /builds/
-/doc/
+/doc/doxygen
 .dep
 Makefile.in
 /configure

diff --git a/config/doxygen.cfg b/config/doxygen.cfg
index f0548554230f3a90ce2f2f52d25f0c0da3d77c2c..9f7205f8b38680d9d82e6eed0fa7cd6fe7281203 100644 (file)
--- a/config/doxygen.cfg
+++ b/config/doxygen.cfg
@@ -575,8 +575,11 @@ INPUT                  = $(SRCDIR)/AUTHORS \
                          $(SRCDIR)/README \
                          $(SRCDIR)/RELEASE-NOTES \
                          $(SRCDIR)/THANKS \
+                         $(SRCDIR)/doc/mainpage.md \
                          $(CVC4_DOXYGEN_INPUT)
 
+USE_MDFILE_AS_MAINPAGE = $(SRCDIR)/doc/mainpage.md
+
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding, which is
 # also the default input encoding. Doxygen uses libiconv (or the iconv built

diff --git a/doc/mainpage.md b/doc/mainpage.md
new file mode 100644 (file)
index 0000000..1fc04ab
--- /dev/null
+++ b/doc/mainpage.md
@@ -0,0 +1,26 @@
+Getting started with the CVC4 API
+
+The main classes of the CVC4 API are:
+- CVC4::Expr - an expression (a formula, term, variable, constant, etc.)
+- CVC4::Type - a type (every Expr has a Type)
+- CVC4::ExprManager - a factory class for Exprs and Types (create one of these for your application)
+- CVC4::SmtEngine - the SMT interface, permits making assertions and checking satisfiability (create one of these for your application)
+
+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
+http://cvc4.cs.nyu.edu/wiki/Tutorials#C.2B.2B_API
+
+Using the CVC4 API from Java
+
+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.
+
+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.
+
+Third, I/O streams are wrapped so that some functions requiring C++ input and output streams will accept Java InputStreams and OutputStreams.
+
+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, http://cvc4.cs.nyu.edu/bugs.
+
+For examples of Java programs using the CVC4 API, look in the directory examples/api/java in the CVC4 source distribution.
+
+Thank you for your interest in CVC4!
+
+The CVC4 Development team

diff --git a/src/parser/parser.h b/src/parser/parser.h
index 2f30460d2aa2bec23b647ef15fec94750c6b670f..94636dd796c217baf3727a9471cb864d39a63859 100644 (file)
--- a/src/parser/parser.h
+++ b/src/parser/parser.h
@@ -327,6 +327,7 @@ public:
    * @param name the symbol to check
    * @param check the kind of check to perform
    * @param type the type of the symbol
+   * @param notes notes to add to a parse error (if one is generated)
    * @throws ParserException if checks are enabled and the check fails
    */
   void checkDeclaration(const std::string& name, DeclarationCheck check,