updating documentation.

sosy-lab · Nov 30, 2019 · d903500 · d903500
1 parent d5879be
commit d903500
Show file tree

Hide file tree

Showing 3 changed files with 88 additions and 9 deletions.
diff --git a/CHANGELOG.md b/CHANGELOG.md
@@ -1,5 +1,33 @@
 # JavaSMT ChangeLog
 
+## JavaSMT 3.3.0
+
+### Changes in the API:
+ - FloatingPointManager supports more arithmetic methods, such as `min`, `max`, `abs`, `sqrt`.
+
+### Improvements and Fixes:
+ - More consistency checks on bitvector constants
+ - The Maven release contains the bindings for Princess
+ - New or updated solver versions:
+    - Boolector 3.0.0-2019-11-11-g9d06cc0 was added (#174).
+    - CVC4: 1.8-prerelease-2019-11-30-gae93e65
+    - Princess: 2.12-2019-11-20
+    - SMTInterpol: 2.5-533-ga4ba1513
+    - other solvers were not updated since the last release
+
+## JavaSMT 3.2.0
+
+The biggest change is the integration of the CVC4 SMT solver (CVC4 1.8-prerelease).
+
+## JavaSMT 3.1.0
+
+This is mostly a cleanup release that contains several smaller changes and optimizations.
+
+We included new solver versions:
+
+- OptiMathSAT: 1.6.3
+- SMTInterpol: 2.5-515-g2765bdd
+
 ## JavaSMT 3.0.0
 
 ### Changes in the API

diff --git a/README.md b/README.md
@@ -37,21 +37,23 @@ Currently JavaSMT support several SMT solvers (see [Getting Started](doc/Getting
  - [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/)
  - [Princess](http://www.philipp.ruemmer.org/princess.shtml)
  - [Z3](https://github.com/Z3Prover/z3)
+ - [CVC4](https://cvc4.github.io/)
+ - [Boolector](https://boolector.github.io/)
 
-The following features are supported:
+The following features are supported (depending on the used SMT solver):
 
  - Satisfiability checking
  - Quantifiers and quantifier elimination
  - Incremental solving with assumptions
  - Incremental solving with push/pop
  - Multiple independent contexts
  - Model generation
- - Interpolation, including tree and sequential
+ - Interpolation, including tree and sequential structure
  - Formula transformation using built-in tactics
  - Formula introspection using visitors
 
 #### Multithreading Support
-All solvers support multithreading (MathSAT only since JavaSMT 1.0.1-164-gd14ed28),
+Most solvers support multithreading,
 provided that different threads use different contexts,
 and _all_ operations on a single context are performed from a single thread.
 Interruption using [ShutdownNotifier][] may be used to interrupt a
@@ -79,7 +81,9 @@ Currently we do not support performing garbage collection for MathSAT5.
 
 
 ## Getting started
-Installation is possible via [Maven][Maven repository], [Ivy][Ivy repository], or [manually][Manual Installation].  Please see our [Getting Started Guide](doc/Getting-started.md)
+Installation is possible via [Maven][Maven repository],
+[Ivy][Ivy repository], or [manually][Manual Installation].
+Please see our [Getting Started Guide](doc/Getting-started.md).
 
 #### Usage
 ``` java
@@ -110,8 +114,8 @@ try (SolverContext context = SolverContextFactory.createSolverContext(
  - Project maintainers: [Karlheinz Friedberger][] and [Philipp Wendler][]
  - Former project maintainer: [George Karpenkov][]
  - Initial codebase, many design decisions: [Philipp Wendler][]
- - Contributions: [Thomas Stieglmaier][] and others.
- 
+ - Contributions: Daniel Baier, [Thomas Stieglmaier][] and several others.
+
 [ConfigurationOptions]: https://sosy-lab.github.io/java-smt/ConfigurationOptions.txt
 [Manual Installation]: doc/Getting-started.md#manual-installation
 [ShutdownNotifier]: https://sosy-lab.github.io/java-common-lib/api/org/sosy_lab/common/ShutdownNotifier.html

diff --git a/doc/Developers.md b/doc/Developers.md
@@ -16,7 +16,7 @@ for more information.
 ## Continuous Integration
 
 We rely on [GitLab-CI][] for continuous integration, which picks up code style violations,
-compile warnings for both ECJ and javac (for several versions of Java), 
+compile warnings for both ECJ and javac (for several versions of Java),
 [SpotBugs](https://github.com/spotbugs/spotbugs) errors,...
 
 ## Releasing JavaSMT
@@ -57,6 +57,10 @@ For publishing to Maven Central, we use the [Nexus Repository Manager](https://o
 
 #### Requirements
 
+Please make sure that all necessary libraries are already released on Maven Central,
+before (or at least while) publishing a new version of JavaSMT.
+Maven does not check for existing dependencies automatically.
+
 Please make sure that you have a valid user account and configured your local settings accordingly.
 For example, insert the following content into `~/.m2/settings.xml`:
 ```xml
@@ -87,16 +91,21 @@ The following steps are required:
  - Run the `stage` ANT target.
    (There is currently no need to change any label from `SNAPSHOT` to `RELEASE` or vice versa,
    as written somewhere in the documentation, because we only produce `RELEASE` versions.)
- - Login to [Nexus Repository Manager](https://oss.sonatype.org/) 
+ - Login to [Nexus Repository Manager](https://oss.sonatype.org/)
    and open the [list of staging repositories](https://oss.sonatype.org/#stagingRepositories).
- - Run `close` and `release` tasks on your pushed bundle 
+ - Run `close` and `release` tasks on your pushed bundle
    (see [documentation](http://central.sonatype.org/pages/releasing-the-deployment.html) for details).
  - After some delay (a few hours or days) the release is automatically synced to Maven Central.
 
 Additional instructions are available at the official [OSSRH][] page.
 
 ## Releasing Solvers
 
+Before actually releasing a new version of a solver into the public world,
+make sure, it is tested sufficiently.
+This is one of the most critical steps in JavaSMT development.
+
+
 ### Publishing Z3
 
 We prefer to use the official Z3 binaries,
@@ -131,6 +140,43 @@ ant publish-z3 -Dz3.path=$Z3_DIR/build
 ```
 Finally follow the instructions shown in the message at the end.
 
+
+### Publishing CVC4
+
+We prefer to use our own CVC4 binaries and Java bindings.
+
+To publish CVC4, checkout the [CVC4 repository](https://github.com/kfriedberger/CVC4).
+Then execute the following command in the JavaSMT directory,
+where `$CVC4_DIR` is the path to the CVC4 directory
+and `$CVC4_VERSION` is the version number:
+```
+ant publish-cvc4 -Dcvc4.path=$CVC4_DIR -Dcvc4.customRev=$CVC4_VERSION
+```
+Example:
+```
+ant publish-cvc4 -Dcvc4.path=../CVC4 -Dcvc4.customRev=1.8-prerelease-2019-10-05
+```
+Finally follow the instructions shown in the message at the end.
+
+
+### Publishing Boolector
+
+We prefer to use our own Boolector binaries and Java bindings.
+
+To publish Boolector, checkout the [CVC4 repository](https://github.com/kfriedberger/CVC4).
+Then execute the following command in the JavaSMT directory,
+where `$BTOR_DIR` is the path to the CVC4 directory
+and `$BTOR_VERSION` is the version number:
+```
+ant publish-boolector -Dboolector.path=$BTOR_DIR -Dboolector.customRev=$BTOR_VERSION
+```
+Example:
+```
+ant publish-boolector -Dboolector.path=../boolector -Dboolector.customRev=3.0.0-2019-11-29
+```
+Finally follow the instructions shown in the message at the end.
+
+
 ### Publishing (Opti)-MathSAT5
 
 For publishing MathSAT5, you need to use a machine with at least GCC 4.9.
@@ -154,6 +200,7 @@ ant publish-optimathsat -Dmathsat.path=$OPTIMATHSAT_PATH -Dgmp.path=$GMP_PATH -D
 The scripts for publishing Princess and SMTInterpol are available
 at the root of the [Ivy Repository](https://svn.sosy-lab.org/software/ivy).
 
+
 ## Writing Solver Backends
 
 In order to write a solver backend it is sufficient to provide the