Adding JavaSMT support

.github/actions/cache-build/action.yml

@@ -16,5 +16,5 @@ runs:
     - name: build gradle
       uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1
       with:
-        arguments: ${{ inputs.arguments }} --info --stacktrace
+        arguments: ${{ inputs.arguments }} --info --stacktrace --max-workers 2 --no-daemon
 

.github/workflows/sonar.yml

@@ -33,7 +33,7 @@ jobs:
         if: env.SONAR_TOKEN != '' && github.event_name == 'push'
         uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1
         with:
-          arguments: build jacocoTestReport sonar --info -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m
+          arguments: build jacocoTestReport sonar --stacktrace --info --max-workers 2 --no-daemon -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m
       - name: Checkout source branch
         if: github.event_name == 'pull_request_target'
         uses: actions/checkout@c85c95e3d7251135ab7dc9ce3241c5835cc595a9 # v3.5.3
@@ -48,4 +48,4 @@ jobs:
         if: env.SONAR_TOKEN != '' && github.event_name == 'pull_request_target' && contains(github.event.pull_request.labels.*.name, 'Ready to test')
         uses: gradle/gradle-build-action@40b6781dcdec2762ad36556682ac74e31030cfe2 # v2.5.1
         with:
-          arguments: build jacocoTestReport sonar --info -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m  -Dsonar.pullrequest.key=${{ github.event.pull_request.number }}
+          arguments: build jacocoTestReport sonar --info --max-workers 2 --no-daemon -Dorg.gradle.jvmargs=-XX:MaxMetaspaceSize=512m  -Dsonar.pullrequest.key=${{ github.event.pull_request.number }}

build.gradle.kts

@@ -28,7 +28,7 @@ buildscript {
 
 allprojects {
     group = "hu.bme.mit.theta"
-    version = "5.0.6"
+    version = "5.1.0"
 
     apply(from = rootDir.resolve("gradle/shared-with-buildSrc/mirrors.gradle.kts"))
 }

buildSrc/gradle.properties

@@ -1,3 +1,19 @@
+#
+#  Copyright 2024 Budapest University of Technology and Economics
+#
+#  Licensed under the Apache License, Version 2.0 (the "License");
+#  you may not use this file except in compliance with the License.
+#  You may obtain a copy of the License at
+#
+#      http://www.apache.org/licenses/LICENSE-2.0
+#
+#  Unless required by applicable law or agreed to in writing, software
+#  distributed under the License is distributed on an "AS IS" BASIS,
+#  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+#  See the License for the specific language governing permissions and
+#  limitations under the License.
+#
+
 javaVersion=17
 kotlinVersion=1.7.10
 shadowVersion=7.1.2
@@ -9,4 +25,6 @@ junitVersion=5.9.3
 junit4Version=4.12
 jacocoVersion=0.8.8
 mockitoVersion=2.2.11
-gsonVersion=2.9.1
+gsonVersion=2.9.1
+javasmtVersion=4.1.1
+sosylabVersion=0.3000-569-g89796f98

buildSrc/src/main/kotlin/Deps.kt

@@ -28,6 +28,12 @@ object Deps {
     val z3 = "lib/com.microsoft.z3.jar"
     val z3legacy = "lib/com.microsoft.z3legacy.jar"
 
+    val cvc5 = "lib/cvc5.jar"
+
+    val javasmt = "org.sosy-lab:java-smt:${Versions.javasmt}"
+    val javasmtLocal = "lib/javasmt.jar"
+    val sosylabCommon = "org.sosy-lab:common:${Versions.sosylab}"
+
     val jcommander = "com.beust:jcommander:${Versions.jcommander}"
 
     val junit4 = "junit:junit:${Versions.junit4}"

buildSrc/src/main/kotlin/java-common.gradle.kts

@@ -56,4 +56,8 @@ tasks {
     withType<Test> {
         useJUnitPlatform()
     }
+
+    withType<Test> {
+        jvmArgs("-Xss5m", "-Xms512m", "-Xmx1g")
+    }
 }

lib/README.md

@@ -71,4 +71,288 @@ The GNU MP Library is free software; you can redistribute it and/or modify it un
 The GNU MP Library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU Lesser General Public License for more details.
 
 You should have received a copy of the GNU Lesser General Public License along with the GNU MP Library; see the file COPYING.LIB.  If not, write to the Free Software Foundation, Inc., 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301, USA. 
+```
+
+JavaSMT is licensed under the following license: [Apache License Version 2.0](https://github.com/sosy-lab/java-smt/blob/fix-modulo/LICENSE)
+
+CVC5 is licensed under the following license:
+```
+cvc5 is copyright (C) 2009-2023 by its authors and contributors (see the file
+AUTHORS) and their institutional affiliations.  All rights reserved.
+
+The source code of cvc5 is open and available to students, researchers,
+software companies, and everyone else to study, to modify, and to redistribute
+original or modified versions; distribution is under the terms of the modified
+BSD license (reproduced below).  Please note that cvc5 can be configured
+(however, by default it is not) to link against some GPLed libraries, and
+therefore the use of these builds may be restricted in non-GPL-compatible
+projects.  See below for a discussion of CLN and GLPK (the two GPLed optional
+library dependences for cvc5), and how to ensure you have a build that doesn't
+link against GPLed libraries.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are
+met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. Redistributions in binary form must reproduce the above copyright
+   notice, this list of conditions and the following disclaimer in the
+   documentation and/or other materials provided with the distribution.
+
+3. Neither the name of the copyright holder nor the names of its
+   contributors may be used to endorse or promote products derived from
+   this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT OWNERS AND CONTRIBUTORS
+''AS IS'' AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+
+
+-------------------------------------------------------------------------------
+ Third-Party Software
+-------------------------------------------------------------------------------
+
+The cvc5 source code includes third-party software which has its own copyright
+and licensing terms, as described below.
+
+The following file contains third-party software.
+
+  cmake/CodeCoverage.cmake
+
+The copyright and licensing information of this file is in its header.
+
+cvc5 incorporates MiniSat code (see src/prop/minisat),
+excluded from the above copyright. See licenses/minisat-LICENSE
+for copyright and licensing information.
+
+cvc5 by default links against The GNU Multiple Precision (GMP) Arithmetic
+Library, which is licensed under GNU LGPL v3.  See the file
+licenses/lgpl-3.0.txt for a copy of that license.  Note that according to the
+terms of the LGPL, both cvc5's source, and the combined work (cvc5 linked with
+GMP) may (and do) remain under the more permissive modified BSD license.
+
+cvc5 also links against the CaDiCaL library
+(https://github.com/arminbiere/cadical), which is licensed under
+the MIT license.
+See https://raw.githubusercontent.com/arminbiere/cadical/master/LICENSE
+for copyright and licensing information.  Linking cvc5 against
+this library does not affect the license terms of the cvc5 code.
+
+The implementation of the floating point solver in cvc5 depends on symfpu
+(https://github.com/martin-cs/symfpu) written by Martin Brain.
+See https://raw.githubusercontent.com/martin-cs/symfpu/CVC4/LICENSE for
+copyright and licensing information.
+
+cvc5 optionally links against the following libraries:
+
+  ABC                (https://bitbucket.org/alanmi/abc)
+  CryptoMiniSat      (https://github.com/msoos/cryptominisat)
+  LibPoly            (https://github.com/SRI-CSL/libpoly)
+  libedit            (https://thrysoee.dk/editline)
+
+Linking cvc5 against these libraries does not affect the license terms of the
+cvc5 code.  See the respective projects for copyright and licensing
+information.
+
+
+-------------------------------------------------------------------------------
+ OPTIONAL GPLv3 libraries
+-------------------------------------------------------------------------------
+
+Please be advised that the following libraries are covered under the GPLv3
+license.  If you choose to link cvc5 against one of these libraries, the
+resulting combined work is also covered under the GPLv3. If you want to make
+sure you build a version of cvc5 that uses no GPLed libraries, configure cvc5
+with the "--no-gpl" option before building (which is the default).  cvc5 can
+then be used in contexts where you want to use cvc5 under the terms of the
+(modified) BSD license.  See licenses/gpl-3.0.txt for more information.
+
+cvc5 can be optionally configured to link against CLN, the Class Library for
+Numbers, available here:
+
+  http://www.ginac.de/CLN/
+
+cvc5 can be optionally configured to link against glpk-cut-log, a modified
+version of GLPK, the GNU Linear Programming Kit, available here:
+
+  https://github.com/timothy-king/glpk-cut-log
+```
+
+libpoly is licensed under the following license:
+```
+ GNU LESSER GENERAL PUBLIC LICENSE
+                       Version 3, 29 June 2007
+
+ Copyright (C) 2007 Free Software Foundation, Inc. <http://fsf.org/>
+ Everyone is permitted to copy and distribute verbatim copies
+ of this license document, but changing it is not allowed.
+
+
+  This version of the GNU Lesser General Public License incorporates
+the terms and conditions of version 3 of the GNU General Public
+License, supplemented by the additional permissions listed below.
+
+  0. Additional Definitions.
+
+  As used herein, "this License" refers to version 3 of the GNU Lesser
+General Public License, and the "GNU GPL" refers to version 3 of the GNU
+General Public License.
+
+  "The Library" refers to a covered work governed by this License,
+other than an Application or a Combined Work as defined below.
+
+  An "Application" is any work that makes use of an interface provided
+by the Library, but which is not otherwise based on the Library.
+Defining a subclass of a class defined by the Library is deemed a mode
+of using an interface provided by the Library.
+
+  A "Combined Work" is a work produced by combining or linking an
+Application with the Library.  The particular version of the Library
+with which the Combined Work was made is also called the "Linked
+Version".
+
+  The "Minimal Corresponding Source" for a Combined Work means the
+Corresponding Source for the Combined Work, excluding any source code
+for portions of the Combined Work that, considered in isolation, are
+based on the Application, and not on the Linked Version.
+
+  The "Corresponding Application Code" for a Combined Work means the
+object code and/or source code for the Application, including any data
+and utility programs needed for reproducing the Combined Work from the
+Application, but excluding the System Libraries of the Combined Work.
+
+  1. Exception to Section 3 of the GNU GPL.
+
+  You may convey a covered work under sections 3 and 4 of this License
+without being bound by section 3 of the GNU GPL.
+
+  2. Conveying Modified Versions.
+
+  If you modify a copy of the Library, and, in your modifications, a
+facility refers to a function or data to be supplied by an Application
+that uses the facility (other than as an argument passed when the
+facility is invoked), then you may convey a copy of the modified
+version:
+
+   a) under this License, provided that you make a good faith effort to
+   ensure that, in the event an Application does not supply the
+   function or data, the facility still operates, and performs
+   whatever part of its purpose remains meaningful, or
+
+   b) under the GNU GPL, with none of the additional permissions of
+   this License applicable to that copy.
+
+  3. Object Code Incorporating Material from Library Header Files.
+
+  The object code form of an Application may incorporate material from
+a header file that is part of the Library.  You may convey such object
+code under terms of your choice, provided that, if the incorporated
+material is not limited to numerical parameters, data structure
+layouts and accessors, or small macros, inline functions and templates
+(ten or fewer lines in length), you do both of the following:
+
+   a) Give prominent notice with each copy of the object code that the
+   Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the object code with a copy of the GNU GPL and this license
+   document.
+
+  4. Combined Works.
+
+  You may convey a Combined Work under terms of your choice that,
+taken together, effectively do not restrict modification of the
+portions of the Library contained in the Combined Work and reverse
+engineering for debugging such modifications, if you also do each of
+the following:
+
+   a) Give prominent notice with each copy of the Combined Work that
+   the Library is used in it and that the Library and its use are
+   covered by this License.
+
+   b) Accompany the Combined Work with a copy of the GNU GPL and this license
+   document.
+
+   c) For a Combined Work that displays copyright notices during
+   execution, include the copyright notice for the Library among
+   these notices, as well as a reference directing the user to the
+   copies of the GNU GPL and this license document.
+
+   d) Do one of the following:
+
+       0) Convey the Minimal Corresponding Source under the terms of this
+       License, and the Corresponding Application Code in a form
+       suitable for, and under terms that permit, the user to
+       recombine or relink the Application with a modified version of
+       the Linked Version to produce a modified Combined Work, in the
+       manner specified by section 6 of the GNU GPL for conveying
+       Corresponding Source.
+
+       1) Use a suitable shared library mechanism for linking with the
+       Library.  A suitable mechanism is one that (a) uses at run time
+       a copy of the Library already present on the user's computer
+       system, and (b) will operate properly with a modified version
+       of the Library that is interface-compatible with the Linked
+       Version.
+
+   e) Provide Installation Information, but only if you would otherwise
+   be required to provide such information under section 6 of the
+   GNU GPL, and only to the extent that such information is
+   necessary to install and execute a modified version of the
+   Combined Work produced by recombining or relinking the
+   Application with a modified version of the Linked Version. (If
+   you use option 4d0, the Installation Information must accompany
+   the Minimal Corresponding Source and Corresponding Application
+   Code. If you use option 4d1, you must provide the Installation
+   Information in the manner specified by section 6 of the GNU GPL
+   for conveying Corresponding Source.)
+
+  5. Combined Libraries.
+
+  You may place library facilities that are a work based on the
+Library side by side in a single library together with other library
+facilities that are not Applications and are not covered by this
+License, and convey such a combined library under terms of your
+choice, if you do both of the following:
+
+   a) Accompany the combined library with a copy of the same work based
+   on the Library, uncombined with any other library facilities,
+   conveyed under the terms of this License.
+
+   b) Give prominent notice with the combined library that part of it
+   is a work based on the Library, and explaining where to find the
+   accompanying uncombined form of the same work.
+
+  6. Revised Versions of the GNU Lesser General Public License.
+
+  The Free Software Foundation may publish revised and/or new versions
+of the GNU Lesser General Public License from time to time. Such new
+versions will be similar in spirit to the present version, but may
+differ in detail to address new problems or concerns.
+
+  Each version is given a distinguishing version number. If the
+Library as you received it specifies that a certain numbered version
+of the GNU Lesser General Public License "or any later version"
+applies to it, you have the option of following the terms and
+conditions either of that published version or of any later version
+published by the Free Software Foundation. If the Library as you
+received it does not specify a version number of the GNU Lesser
+General Public License, you may choose any version of the GNU Lesser
+General Public License ever published by the Free Software Foundation.
+
+  If the Library as you received it specifies that a proxy can decide
+whether future versions of the GNU Lesser General Public License shall
+apply, that proxy's public statement of acceptance of any version is
+permanent authorization for you to choose that version for the
+Library.
 ```

settings.gradle.kts

@@ -52,6 +52,7 @@ include(
     "solver/solver",
     "solver/solver-z3",
     "solver/solver-z3-legacy",
+    "solver/solver-javasmt",
     "solver/solver-smtlib",
     "solver/solver-smtlib-cli",
     "solver/graph-solver",

subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpAssignExpr.java

@@ -56,7 +56,7 @@ public BoolLitExpr eval(final Valuation val) {
         final FpLitExpr leftOpVal = (FpLitExpr) getLeftOp().eval(val);
         final FpLitExpr rightOpVal = (FpLitExpr) getRightOp().eval(val);
 
-        return leftOpVal.eq(rightOpVal);
+        return leftOpVal.assign(rightOpVal);
     }
 
     @Override