Merge remote-tracking branch 'origin/master' into 412-inconsistent-handling-of-unicode-characters-in-string-theory

Author: daniel-raffler

.appveyor.yml

@@ -10,7 +10,7 @@ version: build {build} {branch}
 
 os: Visual Studio 2019
 
-clone_depth: 1
+clone_depth: 5
 
 install:
   - ps: |
@@ -44,6 +44,7 @@ build_script:
       Copy-Item -Path "lib\java\runtime-z3\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
       Copy-Item -Path "lib\java\runtime-mathsat\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
       Copy-Item -Path "lib\java\runtime-bitwuzla\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
+      Copy-Item -Path "lib\java\runtime-cvc5\x64\*.dll" -Destination "lib\native\x86_64-windows\" -Force
 
 test_script:
   - ant unit-tests

.gitignore

@@ -71,5 +71,6 @@ build.properties
 /.apt-generated/
 /repository
 /dist
+/downloads
 
 pom.xml

CHANGELOG.md

@@ -158,7 +158,7 @@ The visitation of quantified formulas was improved.
 ## JavaSMT 3.9.0
 
 This release contains a larger update of Princess and more JUnit tests.
-The PrettyPrinter is switched from a boolean parameter to a options enum.
+The PrettyPrinter is switched from a boolean parameter to an options enum.
 The example projects for Maven are updated with newer solver versions.
 
 ### Updated solvers:
@@ -181,7 +181,7 @@ if disk space is a critical point.
 
 ### Updated solvers:
  - MathSAT5 5.6.5 (inculding binary for Windows)
- - Z3 4.8.9 (including binaries for Windows and MacOS)
+ - Z3 4.8.9 (including binaries for Windows and macOS)
 
 ## JavaSMT 3.6.1
 

README.md

@@ -65,7 +65,7 @@ JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.
 | [Bitwuzla](https://bitwuzla.github.io/) |  :heavy_check_mark:²  | :heavy_check_mark:² | :heavy_check_mark: |  |                                                        |  | a fast solver for bitvector logic |
 | [Boolector](https://boolector.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | a fast solver for bitvector logic, misses formula introspection, deprecated |
 | [CVC4](https://cvc4.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  |  |
-| [CVC5](https://cvc5.github.io/) |  :heavy_check_mark:   |                     |  |  |                                                        |  |  |
+| [CVC5](https://cvc5.github.io/) |  :heavy_check_mark:  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |  :heavy_check_mark:  |  :heavy_check_mark:  |  |
 | [MathSAT5](http://mathsat.fbk.eu/) |  :heavy_check_mark:   | :heavy_check_mark:  | :heavy_check_mark: |  | [maybe](https://github.com/sosy-lab/java-smt/pull/430)³ |  |  |
 | [OpenSMT](https://verify.inf.usi.ch/opensmt) |  :heavy_check_mark:²  | :heavy_check_mark:² |  |  |                                                        |  |  |
 | [OptiMathSAT](http://optimathsat.disi.unitn.it/) |  :heavy_check_mark:   |                     |  |  |                                                        |  | based on MathSAT5, with support for optimization queries |
@@ -76,7 +76,7 @@ JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.
 
 We support a reasonable list of operating systems and versions.
 - Our main target is Linux (mainly Ubuntu or comparable Linux distributions).
-  Windows 10/11 and MacOS are supported for several SMT solvers.
+  Windows 10/11 and macOS are supported for several SMT solvers.
 - Our main development architecture is x64 (x86-64).
   We also provide some solvers for ARM64 (AArch64 for ARMv8-A), e.g., Java-based SMT solvers, Z3, and MathSAT.
   If a specific operating system or architecture is missing and required,
@@ -88,7 +88,7 @@ available with Ubuntu 18.04 or later.
 
 ² Solver requires at least `GLIBC_2.29`/`GLIBCXX_3.4.26` or `GLIBC_2.34`/`GLIBCXX_3.4.29`,
 available with Ubuntu 22.04 or later.  
-³ We do not provide a signed solver library for MacOS. The user needs to compile and sign it.
+³ We do not provide a signed solver library for macOS. The user needs to compile and sign it.
 
 #### Solver Features
 
@@ -181,10 +181,11 @@ try (SolverContext context = SolverContextFactory.createSolverContext(
 
 ## Authors
 
- - Project maintainers: [Karlheinz Friedberger][] and [Philipp Wendler][]
+ - Project maintainers: [Karlheinz Friedberger][] and [Daniel Baier][]
  - Former project maintainer: [George Karpenkov][]
  - Initial codebase, many design decisions: [Philipp Wendler][]
- - Contributions: [Daniel Baier][], [Thomas Stieglmaier][] and several others.
+ - Contributions: [Bajczi Levente][], Daniel Raffler, [Martin Spiessl][], [Thomas Stieglmaier][],
+   and many others. For a full list, see the [contributors overview][].
 
 [ConfigurationOptions]: https://sosy-lab.github.io/java-smt/ConfigurationOptions.txt
 [Manual Installation]: doc/Getting-started.md#manual-installation
@@ -195,5 +196,8 @@ try (SolverContext context = SolverContextFactory.createSolverContext(
 [Thomas Stieglmaier]: https://stieglmaier.me/
 [Karlheinz Friedberger]: https://www.sosy-lab.org/people/friedberger
 [Daniel Baier]: https://www.sosy-lab.org/people/baier
+[Martin Spiessl]: https://www.sosy-lab.org/people/spiessl/
+[Bajczi Levente]: leventebajczi.github.io
 [Ivy repository]: https://www.sosy-lab.org/ivy
 [Maven repository]: https://mvnrepository.com/artifact/org.sosy-lab/java-smt
+[contributors overview]: https://github.com/sosy-lab/java-smt/graphs/contributors

build.xml

@@ -87,7 +87,7 @@ SPDX-License-Identifier: Apache-2.0
             <fileset dir="." includes="${libraryFiles} ${jarFiles} Javadoc-z3/"/>
             <fileset dir="lib/native/source/libmathsat5j" includes="*.so *.dll *.o"/>
             <fileset dir="lib/native/source/libbitwuzla" includes="install-linux/ install-linux-x64/ install-linux-arm64/ install-windows/ install-windows-x64/ build/ doc/ *.so *.dll bitwuzla_wrap.o"/>
-            <fileset dir="lib/native/source/opensmt" includes="install-linux-x64/ install-linux-arm64/ *.so"/>
+            <fileset dir="lib/native/source/opensmt" includes="build/ doc/ install-linux-x64/ install-linux-arm64/ *.o *.so version.h"/>
         </delete>
     </target>
 

build/build-compile.xml

@@ -74,7 +74,7 @@ SPDX-License-Identifier: Apache-2.0
             <src path="${source.dir}"/>
             <classpath refid="classpath"/>
             <compilerarg value="-Xlint"/>
-            <compilerarg value="-Xlint:-fallthrough"/> <!-- checked by error-prone, too, and javac does not recognized $FALL-THROUGH$ -->
+            <compilerarg value="-Xlint:-fallthrough"/> <!-- checked by error-prone, too, and javac does not recognize $FALL-THROUGH$ -->
             <compilerarg value="-Xlint:-processing"/>
             <compilerarg value="-Xlint:-options"/> <!-- suppress warning about bootclasspath on newer JDK -->
             <compilerarg value="-Xlint:-this-escape" if:set="java21"/> <!-- false alarm for every use of configuration injection -->

build/build-documentation.xml

@@ -37,7 +37,7 @@ SPDX-License-Identifier: Apache-2.0
 
             <classpath refid="classpath"/>
 
-            <!-- "-v" is a optional param for verbose output of OptionCollector -->
+            <!-- "-v" is an optional param for verbose output of OptionCollector -->
             <!-- <arg value="-v"/> -->
         </java>
         <echo message="Options collected." level="info"/>

build/build-ivy.xml

@@ -46,7 +46,7 @@ SPDX-License-Identifier: Apache-2.0
     </condition>
     <property name="ivy.cache.dir" location="${tmp.ivy.cache.dir}" />
 
-    <!-- If necessary, download Ivy from web site so that it does not need to be installed. -->
+    <!-- If necessary, download Ivy from website so that it does not need to be installed. -->
     <target name="bootstrap-ivy" unless="ivy.jar.present">
         <mkdir dir="${ivy.jar.dir}"/>
         <echo message="Downloading ivy..."/>

build/build-junit.xml

@@ -46,21 +46,21 @@ SPDX-License-Identifier: Apache-2.0
             <path refid="classpath"/>
         </path>
 
+        <delete dir="${junit.dir}"/>
         <mkdir dir="${junit.dir}"/>
     </target>
 
-    <target name="unit-tests" depends="build, load-junit, init-unit-tests" description="Run all JUnit tests">
-        <delete dir="{junit.dir}"/>
+    <macrodef name="run-junit-tests">
+      <sequential>
         <junit fork="true" printSummary="true" showOutput="false" failureproperty="junit.failed" timeout="600000">
             <assertions><enable/></assertions>
             <formatter type="xml"/>
             <classpath refid="classpath.junit"/>
             <sysproperty key="java.awt.headless" value="true" />
             <batchtest fork="true" todir="${junit.dir}">
-                <fileset dir="${class.dir}">
-                    <include name="**/*Test.*"/>
-                    <exclude name="**/*$*Test.*"/>
-                </fileset>
+              <fileset dir="${class.dir}">
+                <patternset refid="test.sources"/>
+              </fileset>
             </batchtest>
         </junit>
         <junitreport todir="${junit.dir}">
@@ -69,6 +69,41 @@ SPDX-License-Identifier: Apache-2.0
         </junitreport>
         <move file="junit-noframes.html" tofile="JUnit.html"/>
         <fail if="junit.failed" message="JUnit tests failed, look at JUnit.html"/>
+      </sequential>
+    </macrodef>
+
+    <target name="unit-tests-quick" depends="build, load-junit, init-unit-tests"
+            description="Run a minimal set of JUnit tests that are considered quick">
+        <!-- A simpler way for specifying quick tests would be an annotation on class or method level.
+             JUnit 5 might bring such features. However, we still depend on JUnit 4. -->
+        <patternset id="test.sources">
+            <include name="**/solvers/bitwuzla/BitwuzlaNativeApiTest.*"/>
+            <include name="**/solvers/boolector/BoolectorNativeApiTest.*"/>
+            <include name="**/solvers/cvc4/CVC4NativeAPITest.*"/>
+            <include name="**/solvers/cvc5/CVC5NativeAPITest.*"/>
+            <include name="**/solvers/mathsat5/Mathsat5AbstractNativeApiTest.*"/>
+            <include name="**/solvers/mathsat5/Mathsat5NativeApiTest.*"/>
+            <include name="**/solvers/mathsat5/Mathsat5OptimizationNativeApiTest.*"/>
+            <include name="**/solvers/opensmt/OpenSmtNativeAPITest.*"/>
+            <include name="**/solvers/yices2/Yices2NativeApiTest.*"/>
+            <include name="**/test/FloatingPointNumberTest.*"/>
+            <include name="**/test/FormulaManagerTest.*"/>
+            <include name="**/test/NumeralFormulaManagerTest.*"/>
+            <include name="**/test/ProverEnvironmentTest.*"/>
+            <include name="**/test/RationalFormulaManagerTest.*"/>
+            <include name="**/test/SolverContextFactoryTest.*"/>
+            <include name="**/test/SolverContextTest.*"/>
+        </patternset>
+        <run-junit-tests/>
+    </target>
+
+    <target name="unit-tests" depends="build, load-junit, init-unit-tests"
+            description="Run all JUnit tests">
+        <patternset id="test.sources">
+            <include name="**/*Test.*"/>
+            <exclude name="**/*$*Test.*"/>
+        </patternset>
+        <run-junit-tests/>
     </target>
 
     <target name="load-jacoco" depends="resolve-dependencies">
@@ -78,7 +113,6 @@ SPDX-License-Identifier: Apache-2.0
     </target>
 
     <target name="unit-tests-coverage" depends="build, load-junit, load-jacoco, init-unit-tests" description="Run all JUnit tests with coverage report">
-        <delete dir="{junit.dir}"/>
         <jacoco:coverage destfile="${junit.dir}/jacoco.exec" excludes="**/*Test*:**/Dummy*">
             <junit fork="true" printSummary="true" showOutput="false" failureproperty="junit.failed" timeout="600000">
                 <assertions><enable/></assertions>

build/build-maven-publish.xml

@@ -48,7 +48,7 @@ SPDX-License-Identifier: Apache-2.0
     </target>
 
     <!-- macro for pushing a JavaSMT file into a Maven repository
-         (push into the staging area, from there manual publication is required afterwards) -->
+         (push into the staging area, from there manual publication is required afterward) -->
     <macrodef name="stage-javasmt-file">
       <attribute name="filename"/>
       <attribute name="fileending"/>
@@ -82,7 +82,7 @@ SPDX-License-Identifier: Apache-2.0
     </macrodef>
 
     <!-- macro for pushing solvers into a Maven repository
-         (push into the staging area, from there manual publication is required afterwards) -->
+         (push into the staging area, from there manual publication is required afterward) -->
     <macrodef name="stage-solver-file">
       <!-- 'filename' is only used for reading file from file-system, not used "in" Maven -->
       <attribute name="filename"/>
@@ -229,15 +229,17 @@ SPDX-License-Identifier: Apache-2.0
         <ivy:artifactproperty name="[artifact].revision" value="[revision]"/>
         <property name="stage.solver" value="cvc5"/>
         <property name="stage.revision" value="${cvc5.revision}"/>
+        <property name="libDir.x64" value="lib/java/runtime-cvc5/x64"/>
+        <property name="libDir.arm64" value="lib/java/runtime-cvc5/arm64"/>
         <!-- prepare the pom-file -->
         <generate-solver-pom-file/>
         <!-- then publish the files -->
         <stage-solver-file filename="cvc5" fileending="jar"/>
-        <stage-solver-file filename="libcvc5" classifier="libcvc5" fileending="so"/>
-        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni" fileending="so"/>
-        <stage-solver-file filename="libcvc5parser" classifier="libcvc5parser" fileending="so"/>
-        <stage-solver-file filename="libpoly" classifier="libpoly" fileending="so"/>
-        <stage-solver-file filename="libpolyxx" classifier="libpolyxx" fileending="so"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-x64" filedirectory="${libDir.x64}" fileending="so"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-arm64" filedirectory="${libDir.arm64}" fileending="so"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-x64" filedirectory="${libDir.x64}" fileending="dll"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-x64" filedirectory="${libDir.x64}" fileending="dylib"/>
+        <stage-solver-file filename="libcvc5jni" classifier="libcvc5jni-arm64" filedirectory="${libDir.arm64}" fileending="dylib"/>
     </target>
 
     <!--