diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | config/doxygen.cfg | 3 | ||||
| -rw-r--r-- | doc/mainpage.md | 26 | ||||
| -rw-r--r-- | src/parser/parser.h | 1 |
4 files changed, 31 insertions, 1 deletions
diff --git a/.gitignore b/.gitignore index b3cce03ed..b63d4c851 100644 --- 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 f05485542..9f7205f8b 100644 --- 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 index 000000000..1fc04ab3c --- /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 2f30460d2..94636dd79 100644 --- 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, |