Merge remote-tracking branch 'origin/master' into cvc5

Author: kfriedberger

.gitignore

@@ -25,8 +25,14 @@ lib/native/*/*.asc
 doc/Example-Maven-Project/target*
 doc/Example-Maven-Web-Project/target*
 doc/Example-Gradle-Project/.gradle
+doc/Example-Gradle-Project/.settings
+doc/Example-Gradle-Project/.project
 doc/Example-Gradle-Project/dependencies
 doc/Example-Gradle-Project/build
+doc/Example-Gradle-Project-Kotlin/.gradle
+doc/Example-Gradle-Project-Kotlin/.settings
+doc/Example-Gradle-Project-Kotlin/.project
+doc/Example-Gradle-Project-Kotlin/build
 
 solvers_maven_conf/*.asc
 

.gitlab-ci.yml

@@ -14,9 +14,9 @@ variables:
   # Version of https://gitlab.com/sosy-lab/software/refaster/ to use
   REFASTER_REPO_REVISION: 8b7f38e2afedf64b3cfa9592bbb8790b88f58352
   # Needs to be synchronized with Error Prone version in lib/ivy.xml
-  REFASTER_VERSION: 2.11.0
+  REFASTER_VERSION: 2.14.0
 
-build:jdk-14:
+build:jdk-17:
   variables:
     # https://github.com/google/error-prone/issues/1106
     ANT_PROPS_BUILD: "-Divy.disable=true -Derrorprone.disable=true"

CHANGELOG.md

@@ -3,13 +3,43 @@ This file is part of JavaSMT,
 an API wrapper for a collection of SMT solvers:
 https://github.com/sosy-lab/java-smt
 
-SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
 
 SPDX-License-Identifier: Apache-2.0
 -->
 
 # JavaSMT ChangeLog
 
+## JavaSMT 3.13.3
+
+This patch release comes with a smaller bugfix for String-theory formulas in Z3.
+
+## JavaSMT 3.13.2
+
+This patch release comes with some updated solvers and some smaller bugfixes.
+
+### Updated solvers:
+ - JavaSMT 2.5-1147-g108647d8
+ - Z3 4.10.1
+
+## JavaSMT 3.13.1
+
+This patch release contains with several smaller fixes for the integration of SMTInterpol and Princess.
+
+## JavaSMT 3.13.0
+
+This release comes with several bugfixes, e.g.,
+we improved DIV and MOD operations in Integer theory.
+
+### Updated solvers:
+ - MathSAT 5.6.8
+ - Princess 2022-07-01
+ - Z3 4.8.17
+
+### Breaking change:
+The public API for FloatingPointManager was changed to support conversion
+of FloatingPoint to signed and unsigned Bitvectors.
+
 ## JavaSMT 3.12.0
 
 This release comes with an initial support for String theory for SMT solvers like Z3 and CVC4.

README.md

@@ -83,12 +83,23 @@ We aim for supporting more important features, more SMT solvers, and more system
 If something specific is missing, please [look for or file an issue](https://github.com/sosy-lab/java-smt/issues).
 
 #### Multithreading Support
-The solvers Z3 (w and w/o Optimization), SMTInterpol, Princess, MathSAT5, Boolector and CVC4 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
-a solver from any thread.
-CVC4 supports multithreading on a single context with multiple stacks(=provers).
+| SMT Solver | Concurrent context usage¹ | Concurrent prover usage² |
+| --- |:---:|:---:|
+| [Boolector](https://boolector.github.io/) | :heavy_check_mark: |  |
+| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | :heavy_check_mark: |
+| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: |  |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: |  |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: |  |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: |  |
+| [Yices2](https://yices.csl.sri.com/) |  |  |
+| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: |  |
+
+Interruption using a [ShutdownNotifier][] may be used to interrupt a
+a solver from any thread.  
+Formulas are translatable in between contexts/provers/threads using _FormulaManager.translateFrom()_.
+
+¹ Multiple contexts, but all operations on each context only from a single thread.  
+² Multiple provers on one or more contexts, with each prover using its own thread.
 
 #### Garbage Collection in Native Solvers
 JavaSMT exposes an API for performing garbage collection on solvers

build/build-compile.xml

@@ -32,19 +32,32 @@ SPDX-License-Identifier: Apache-2.0
         <fileset dir="${ivy.lib.dir}" includes="build/*.jar"/>
     </path>
 
+    <patternset id="source.additional">
+        <exclude name="**/*.java" />
+    </patternset>
+
+    <!-- error-prone config from https://errorprone.info/docs/installation#jdk-16 -->
+    <property name="errorprone.options.required" value="
+        -XDcompilePolicy=simple
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.api=ALL-UNNAMED
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.file=ALL-UNNAMED
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.main=ALL-UNNAMED
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.model=ALL-UNNAMED
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.parser=ALL-UNNAMED
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.processing=ALL-UNNAMED
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.tree=ALL-UNNAMED
+        -J--add-exports=jdk.compiler/com.sun.tools.javac.util=ALL-UNNAMED
+        -J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED
+        -J--add-opens=jdk.compiler/com.sun.tools.javac.comp=ALL-UNNAMED
+        "/>
+
     <!-- We use error-prone as the compiler, cf. http://errorprone.info/ -->
     <target name="build-project" unless="skipBuild" depends="build-dependencies">
         <depend srcdir="${source.dir}" destdir="${class.dir}"/>
         <mkdir dir="${source.generated.dir}"/>
         <copy todir="${class.dir}">
           <fileset dir="${source.dir}">
-            <exclude name="**/*.java" />
-            <exclude name="**/*.cup" />
-            <exclude name="**/*.jflex" />
-            <exclude name="**/*.nested" />
-            <exclude name="**/*.xml" />
-            <exclude name="**/*.dia" />
-            <exclude name="**/*.pdf" />
+            <patternset refid="source.additional" />
           </fileset>
         </copy>
         <javac debug="true"
@@ -61,9 +74,8 @@ SPDX-License-Identifier: Apache-2.0
             <compilerarg value="-Xlint:-processing"/>
             <compilerarg value="-Xlint:-options"/> <!-- suppress warning about bootclasspath on newer JDK -->
             <compilerarg value="-Werror" unless:set="compile.warn"/>
-            <compilerarg value="-XDcompilePolicy=simple"/> <!-- necessary for error-prone -->
+            <compilerarg line="${errorprone.options.required}" unless:set="errorprone.disable"/>
             <compilerarg value="-Xplugin:ErrorProne -XepDisableWarningsInGeneratedCode ${errorprone.options}" unless:set="errorprone.disable"/>
-            <compilerarg value="-J--add-opens=jdk.compiler/com.sun.tools.javac.code=ALL-UNNAMED" unless:set="errorprone.disable"/>
             <compilerarg value="-s"/><compilerarg value="${source.generated.dir}"/>
             <compilerarg value="-processorpath"/><compilerarg pathref="processorpath"/>
         </javac>
@@ -88,7 +100,7 @@ SPDX-License-Identifier: Apache-2.0
                encoding="UTF-8">
             <src path="${source.dir}"/>
             <classpath refid="classpath"/>
-            <compilerarg value="-XDcompilePolicy=simple"/> <!-- necessary for error-prone -->
+            <compilerarg line="${errorprone.options.required}" unless:set="errorprone.disable"/>
             <compilerarg value="-Xplugin:ErrorProne -XepPatchChecks:refaster:${refaster.rule.file} -XepPatchLocation:${basedir}" unless:set="errorprone.disable"/>
             <compilerarg value="-s"/><compilerarg value="${source.generated.dir}"/>
             <compilerarg value="-processorpath"/><compilerarg pathref="processorpath"/>

build/build-publish-solvers.xml

@@ -67,6 +67,10 @@ SPDX-License-Identifier: Apache-2.0
             Please provide all releases (Linux64, MacOS, and Windows64) together in the same root directory,
             e.g., copy the releases (especially the content of their `bin` directories) together into one directory.
             The only overlap between those releases is the JAR file, which should be equal anyway.
+            Additionally, make the Java sources available in this directory.
+            This can be done by:
+            - copying the content of sources-zip into the current directory (or vice versa)
+            - executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required.
         </fail>
         <echo>Option -Dz3.version=... not specified. Trying to determine z3.version from git repository. This will fail if git repository is not available.</echo>
         <exec executable="git" dir="${z3.path}" outputproperty="z3.version" failonerror="true">

build/deploy-gh-pages.sh

@@ -32,8 +32,8 @@ git init
 git add .
 git commit -m "Deploy to GitHub Pages"
 
-# Force push from the current repo's master branch to the remote
+# Force push from the current repo's HEAD to the remote
 # repo's gh-pages branch. (All previous history on the gh-pages branch
 # will be lost, since we are overwriting it.) We redirect any output to
 # /dev/null to hide any sensitive credential data that might otherwise be exposed.
-git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" master:gh-pages > /dev/null 2>&1
+git push --force --quiet "https://${GH_TOKEN}@${GH_REF}" HEAD:gh-pages > /dev/null 2>&1

build/gitlab-ci.Dockerfile.jdk-14 renamed to build/gitlab-ci.Dockerfile.jdk-17

@@ -2,7 +2,7 @@
 # an API wrapper for a collection of SMT solvers:
 # https://github.com/sosy-lab/java-smt
 #
-# SPDX-FileCopyrightText: 2020 Dirk Beyer <https://www.sosy-lab.org>
+# SPDX-FileCopyrightText: 2022 Dirk Beyer <https://www.sosy-lab.org>
 #
 # SPDX-License-Identifier: Apache-2.0
 
@@ -11,9 +11,9 @@
 # and will be used by CI as declared in .gitlab-ci.yml.
 #
 # Commands for updating the image:
-# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-14 - < build/gitlab-ci.Dockerfile.jdk-14
+# docker build --pull -t registry.gitlab.com/sosy-lab/software/java-smt/test:jdk-17 - < build/gitlab-ci.Dockerfile.jdk-17
 # docker push registry.gitlab.com/sosy-lab/software/java-smt/test
 
-FROM registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-14
+FROM registry.gitlab.com/sosy-lab/software/java-project-template/test:jdk-17
 RUN apt-get update && apt-get install -y \
   libgomp1

build/gitlab-ci.Dockerfile.jdk-8

@@ -56,9 +56,9 @@ build:jdk-11:
   <<: *build
   image: ${CI_REGISTRY_IMAGE}/test:jdk-11
 
-build:jdk-14:
+build:jdk-17:
   <<: *build
-  image: ${CI_REGISTRY_IMAGE}/test:jdk-14
+  image: ${CI_REGISTRY_IMAGE}/test:jdk-17
 
 
 # For checks that need the binaries
@@ -84,9 +84,9 @@ build-project-ecj:jdk-11:
   <<: *build-project-ecj
   image: ${CI_REGISTRY_IMAGE}/test:jdk-11
 
-build-project-ecj:jdk-14:
+build-project-ecj:jdk-17:
   <<: *build-project-ecj
-  image: ${CI_REGISTRY_IMAGE}/test:jdk-14
+  image: ${CI_REGISTRY_IMAGE}/test:jdk-17
 
 
 check-format:
@@ -154,20 +154,20 @@ unit-tests:jdk-11:
     - build:jdk-11
   image: ${CI_REGISTRY_IMAGE}/test:jdk-11
 
-unit-tests:jdk-14:
+unit-tests:jdk-17:
   <<: *unit-tests
   dependencies:
     - build-dependencies
-    - build:jdk-14
+    - build:jdk-17
   needs:
     - build-dependencies
-    - build:jdk-14
-  image: ${CI_REGISTRY_IMAGE}/test:jdk-14
+    - build:jdk-17
+  image: ${CI_REGISTRY_IMAGE}/test:jdk-17
 
 
 refaster:
   <<: *source_check
-  image: ${CI_REGISTRY_IMAGE}/test:jdk-14
+  image: ${CI_REGISTRY_IMAGE}/test:jdk-11
   before_script:
     - 'test -d refaster || git clone https://gitlab.com/sosy-lab/software/refaster.git'
     - 'cd refaster'
@@ -206,26 +206,6 @@ reuse:
     - reuse lint
 
 
-deploy-coverage:
-  stage: deploy
-  script: "build/deploy-coverage.sh"
-  dependencies:
-    - unit-tests:jdk-11
-  needs:
-    - unit-tests:jdk-11
-  only:
-    refs:
-      - master
-    variables:
-      - $CI_PROJECT_PATH == $PROJECT_PATH # not on forks
-  except:
-    variables:
-      - $CODACY_PROJECT_TOKEN == null # required for job
-      - $GH_TOKEN == null # required for job
-  cache:
-    paths:
-      - "codacy-coverage-reporter-assembly*.jar"
-
 deploy-gh-pages:
   stage: deploy
   script: "build/deploy-gh-pages.sh"
@@ -236,9 +216,8 @@ deploy-gh-pages:
     - build:jdk-11
     - javadoc
   only:
-    refs:
-      - master
     variables:
+      - $CI_COMMIT_BRANCH == $CI_DEFAULT_BRANCH # only on default branch
       - $CI_PROJECT_PATH == $PROJECT_PATH # not on forks
   except:
     variables:
@@ -268,8 +247,8 @@ build-docker:test:jdk-11:
     DOCKERFILE: build/gitlab-ci.Dockerfile.jdk-11
     IMAGE: /test:jdk-11
 
-build-docker:test:jdk-14:
+build-docker:test:jdk-17:
   extends: .build-docker
   variables:
-    DOCKERFILE: build/gitlab-ci.Dockerfile.jdk-14
-    IMAGE: /test:jdk-14
+    DOCKERFILE: build/gitlab-ci.Dockerfile.jdk-17
+    IMAGE: /test:jdk-17

build/gitlab-ci.yml

@@ -46,7 +46,7 @@ there are scripts for publishing available at the root of the [Ivy Repository](h
 We prefer to use the official Z3 binaries,
 please build from source only if necessary (e.g., in case of an important bugfix).
 
-To publish Z3, download the **Ubuntu 16.04**, **Windows**, and **OSX** binary
+To publish Z3, download the **Ubuntu**, **Windows**, and **OSX** binary
 and the sources (for JavaDoc) for the [latest release](https://github.com/Z3Prover/z3/releases) and unzip them.
 In the unpacked sources directory, prepare Java sources via `python scripts/mk_make.py --java`.
 For simpler handling, we then copy the files from the three `bin` directories together into one directory,
@@ -145,12 +145,12 @@ and `$MATHSAT_VERSION` is the version number of MathSAT (all-in-one, runtime: le
 Concrete example (`$WD` is a working directory where all dependencies are located):
 ```
   ant publish-mathsat \
-      -Dmathsat.path=$WD/mathsat-5.6.4-linux-x86_64-reentrant \
+      -Dmathsat.path=$WD/mathsat-5.6.7-linux-x86_64-reentrant \
       -Dgmp.path=$WD/gmp-6.1.2 \
-      -Dmathsat-windows.path=$WD/mathsat-5.6.4-win64-msvc \
+      -Dmathsat-windows.path=$WD/mathsat-5.6.7-win64-msvc \
       -Dmpir-windows.path=$WD/mpir-2.7.2-win \
       -Djdk-windows.path=$WD/jdk-11 \
-      -Dmathsat.version=5.6.4-debug
+      -Dmathsat.version=5.6.7
 ```
 Finally follow the instructions shown in the message at the end.