diff options
author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-04-21 10:21:34 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-21 10:21:34 -0700 |
commit | ae5ee4b07dc3d3c792e7fe7f382ff490dd28aca4 (patch) | |
tree | a7c2ab8013f46dbea75fcd6e7da3fb83e2012b2f /doc | |
parent | 86aa9bc35ba9dc9a57913a2ffc71619c7657cc35 (diff) |
Goodbye CVC4, hello cvc5! (#6371)
This commits changes the build system to cvc5 and removes the remaining
occurrences of CVC4. It further cleans up outdated/unused scripts in contrib/.
Diffstat (limited to 'doc')
-rw-r--r-- | doc/CMakeLists.txt | 26 | ||||
-rw-r--r-- | doc/cvc5.1_template.in (renamed from doc/cvc4.1_template.in) | 0 | ||||
-rw-r--r-- | doc/cvc5.5.in (renamed from doc/cvc4.5.in) | 0 | ||||
-rw-r--r-- | doc/libcvc5.3.in (renamed from doc/libcvc4.3.in) | 0 | ||||
-rw-r--r-- | doc/libcvc5parser.3.in (renamed from doc/libcvc4parser.3.in) | 0 | ||||
-rw-r--r-- | doc/mainpage.md | 43 |
6 files changed, 13 insertions, 56 deletions
diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt index 002a94cb7..a58303520 100644 --- a/doc/CMakeLists.txt +++ b/doc/CMakeLists.txt @@ -17,7 +17,7 @@ # Set variables required for the documentation *.in files string(TIMESTAMP MAN_DATE "%Y-%m-%d") -set(VERSION CVC4_RELEASE_STRING) +set(VERSION CVC5_RELEASE_STRING) #-----------------------------------------------------------------------------# # Generate files @@ -27,20 +27,20 @@ configure_file( ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc_template) configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/cvc4.1_template.in - ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1_template) + ${CMAKE_CURRENT_SOURCE_DIR}/cvc5.1_template.in + ${CMAKE_CURRENT_BINARY_DIR}/cvc5.1_template) configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/cvc4.5.in - ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5) + ${CMAKE_CURRENT_SOURCE_DIR}/cvc5.5.in + ${CMAKE_CURRENT_BINARY_DIR}/cvc5.5) configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4.3.in - ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3) + ${CMAKE_CURRENT_SOURCE_DIR}/libcvc5.3.in + ${CMAKE_CURRENT_BINARY_DIR}/libcvc5.3) configure_file( - ${CMAKE_CURRENT_SOURCE_DIR}/libcvc4parser.3.in - ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3) + ${CMAKE_CURRENT_SOURCE_DIR}/libcvc5parser.3.in + ${CMAKE_CURRENT_BINARY_DIR}/libcvc5parser.3) configure_file( ${CMAKE_CURRENT_SOURCE_DIR}/options.3cvc_template.in @@ -49,11 +49,11 @@ configure_file( #-----------------------------------------------------------------------------# # Install man pages -install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.1 DESTINATION share/man/man1) -install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc4.5 DESTINATION share/man/man5) +install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc5.1 DESTINATION share/man/man1) +install(FILES ${CMAKE_CURRENT_BINARY_DIR}/cvc5.5 DESTINATION share/man/man5) install(FILES - ${CMAKE_CURRENT_BINARY_DIR}/libcvc4.3 - ${CMAKE_CURRENT_BINARY_DIR}/libcvc4parser.3 + ${CMAKE_CURRENT_BINARY_DIR}/libcvc5.3 + ${CMAKE_CURRENT_BINARY_DIR}/libcvc5parser.3 ${CMAKE_CURRENT_BINARY_DIR}/options.3cvc ${CMAKE_CURRENT_BINARY_DIR}/SmtEngine.3cvc DESTINATION share/man/man3) diff --git a/doc/cvc4.1_template.in b/doc/cvc5.1_template.in index 042d6cfc1..042d6cfc1 100644 --- a/doc/cvc4.1_template.in +++ b/doc/cvc5.1_template.in diff --git a/doc/cvc4.5.in b/doc/cvc5.5.in index d66110f63..d66110f63 100644 --- a/doc/cvc4.5.in +++ b/doc/cvc5.5.in diff --git a/doc/libcvc4.3.in b/doc/libcvc5.3.in index 1db5b3c2d..1db5b3c2d 100644 --- a/doc/libcvc4.3.in +++ b/doc/libcvc5.3.in diff --git a/doc/libcvc4parser.3.in b/doc/libcvc5parser.3.in index f288daf83..f288daf83 100644 --- a/doc/libcvc4parser.3.in +++ b/doc/libcvc5parser.3.in diff --git a/doc/mainpage.md b/doc/mainpage.md deleted file mode 100644 index 13005e023..000000000 --- a/doc/mainpage.md +++ /dev/null @@ -1,43 +0,0 @@ -/** -\mainpage 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.stanford.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, https://github.com/CVC4/CVC4/issues. - -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 - -\page authors AUTHORS -\verbinclude AUTHORS -\page copying COPYING -\verbinclude COPYING -\page install INSTALL -\verbinclude INSTALL -\page news NEWS -\verbinclude NEWS -\page release-notes RELEASE-NOTES -\verbinclude RELEASE-NOTES -\page readme README -\verbinclude README -\page thanks THANKS -\verbinclude THANKS -*/ |