diff --git a/.github/actions/cache-build/action.yml b/.github/actions/cache-build/action.yml index 664f9ffb30..217f326f44 100644 --- a/.github/actions/cache-build/action.yml +++ b/.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 diff --git a/.github/workflows/sonar.yml b/.github/workflows/sonar.yml index d6078ecf79..c291bdc97c 100644 --- a/.github/workflows/sonar.yml +++ b/.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 }} diff --git a/build.gradle.kts b/build.gradle.kts index f11d9124c4..479f4b71a0 100644 --- a/build.gradle.kts +++ b/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")) } diff --git a/buildSrc/gradle.properties b/buildSrc/gradle.properties index 781f22cb07..68276da2bc 100644 --- a/buildSrc/gradle.properties +++ b/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 \ No newline at end of file +gsonVersion=2.9.1 +javasmtVersion=4.1.1 +sosylabVersion=0.3000-569-g89796f98 \ No newline at end of file diff --git a/buildSrc/src/main/kotlin/Deps.kt b/buildSrc/src/main/kotlin/Deps.kt index 81fbfeefbb..86c5f2cd09 100644 --- a/buildSrc/src/main/kotlin/Deps.kt +++ b/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}" diff --git a/buildSrc/src/main/kotlin/java-common.gradle.kts b/buildSrc/src/main/kotlin/java-common.gradle.kts index 2b5fb8aa5a..dbc37729e0 100644 --- a/buildSrc/src/main/kotlin/java-common.gradle.kts +++ b/buildSrc/src/main/kotlin/java-common.gradle.kts @@ -56,4 +56,8 @@ tasks { withType { useJUnitPlatform() } + + withType { + jvmArgs("-Xss5m", "-Xms512m", "-Xmx1g") + } } diff --git a/lib/README.md b/lib/README.md index dcc52419c5..f03f5d333e 100644 --- a/lib/README.md +++ b/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. + 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. ``` \ No newline at end of file diff --git a/lib/cvc5.jar b/lib/cvc5.jar new file mode 100644 index 0000000000..42ccb9e8e7 Binary files /dev/null and b/lib/cvc5.jar differ diff --git a/lib/javasmt.jar b/lib/javasmt.jar new file mode 100644 index 0000000000..5f806c43c0 Binary files /dev/null and b/lib/javasmt.jar differ diff --git a/lib/libcvc5.so.1 b/lib/libcvc5.so.1 new file mode 100644 index 0000000000..c79bc0de81 Binary files /dev/null and b/lib/libcvc5.so.1 differ diff --git a/lib/libcvc5jni.so b/lib/libcvc5jni.so new file mode 100644 index 0000000000..903602a4cf Binary files /dev/null and b/lib/libcvc5jni.so differ diff --git a/lib/libcvc5parser.so b/lib/libcvc5parser.so new file mode 100644 index 0000000000..1047266a12 Binary files /dev/null and b/lib/libcvc5parser.so differ diff --git a/lib/libcvc5parser.so.1 b/lib/libcvc5parser.so.1 new file mode 100644 index 0000000000..1047266a12 Binary files /dev/null and b/lib/libcvc5parser.so.1 differ diff --git a/lib/libpoly.so.0 b/lib/libpoly.so.0 new file mode 100644 index 0000000000..6173feaa22 Binary files /dev/null and b/lib/libpoly.so.0 differ diff --git a/lib/libpolyxx.so.0 b/lib/libpolyxx.so.0 new file mode 100644 index 0000000000..cc30d0cc7f Binary files /dev/null and b/lib/libpolyxx.so.0 differ diff --git a/settings.gradle.kts b/settings.gradle.kts index 19874e5760..e13aec1d4a 100644 --- a/settings.gradle.kts +++ b/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", diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpAssignExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpAssignExpr.java index 61ce8e576f..8b797fcb2f 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpAssignExpr.java +++ b/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 diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java index 6a019cb365..062f457a9e 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java @@ -23,6 +23,8 @@ import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; +import java.util.Arrays; + import static com.google.common.base.Preconditions.checkArgument; import static com.google.common.base.Preconditions.checkNotNull; import static hu.bme.mit.theta.core.utils.FpUtils.bigFloatToFpLitExpr; @@ -49,6 +51,23 @@ public static FpLitExpr of(final boolean hidden, final BvLitExpr exponent, final return new FpLitExpr(hidden, exponent, significand); } + public static FpLitExpr of(final BvLitExpr value, final FpType fpType) { + boolean[] literal = value.getValue(); + checkArgument(fpType.getExponent() + fpType.getSignificand() + 1 == literal.length); + return new FpLitExpr( + literal[0], + BvLitExpr.of(Arrays.copyOfRange(literal, 1, fpType.getExponent() + 1)), + BvLitExpr.of(Arrays.copyOfRange(literal, fpType.getExponent() + 1, fpType.getExponent() + fpType.getSignificand() + 1))); + } + + public static FpLitExpr of(final BvLitExpr hidden, final BvLitExpr exponent, final BvLitExpr significand) { + boolean[] hiddenLit = hidden.getValue(); + return new FpLitExpr( + hiddenLit[0], + exponent, + significand); + } + public boolean getHidden() { return hidden; } @@ -160,6 +179,13 @@ public BoolLitExpr eq(final FpLitExpr that) { return BoolExprs.Bool(this.hidden == that.hidden && this.exponent.equals(that.exponent) && this.significand.equals(that.significand)); } + public BoolLitExpr assign(final FpLitExpr that) { + checkArgument(this.getType().equals(that.getType())); + var left = fpLitExprToBigFloat(FpRoundingMode.getDefaultRoundingMode(), this); + var right = fpLitExprToBigFloat(FpRoundingMode.getDefaultRoundingMode(), that); + return BoolExprs.Bool(this.hidden == that.hidden && this.exponent.equals(that.exponent) && this.significand.equals(that.significand)); + } + public BoolLitExpr gt(final FpLitExpr that) { checkArgument(this.getType().equals(that.getType())); var left = fpLitExprToBigFloat(FpRoundingMode.getDefaultRoundingMode(), this); @@ -252,7 +278,9 @@ public int hashCode() { @Override public boolean equals(final Object obj) { if (obj != null && this.getClass() == obj.getClass() && getType().equals(((FpLitExpr) obj).getType())) { - return eq((FpLitExpr) obj).equals(BoolExprs.True()); + return this.exponent.equals(((FpLitExpr) obj).exponent) && + this.hidden == ((FpLitExpr) obj).hidden && + this.significand.equals(((FpLitExpr) obj).significand); } else { return false; } diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java index 9914300c06..17e46be03d 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpType.java @@ -68,7 +68,7 @@ public int getSignificand() { @Override public EqExpr Eq(Expr leftOp, Expr rightOp) { - return FpEqExpr.of(leftOp, rightOp); + return FpAssignExpr.of(leftOp, rightOp); } @Override diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncExprs.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncExprs.java index 65597da9ca..ceba2b56eb 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncExprs.java +++ b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/functype/FuncExprs.java @@ -19,6 +19,10 @@ import hu.bme.mit.theta.core.type.Expr; import hu.bme.mit.theta.core.type.Type; +import java.util.List; + +import static com.google.common.base.Preconditions.checkArgument; + public final class FuncExprs { private FuncExprs() { @@ -39,4 +43,23 @@ public static FuncAppExpr FuncAppExpr App( + final Expr> func, final Expr paramHead, final List paramTail) { + if (!paramTail.isEmpty()) { + final var newParamHead = paramTail.get(paramTail.size() - 1); + final var newParamTail = paramTail.subList(0, paramTail.size() - 1); + return App(App(func, newParamHead, newParamTail), paramHead); + } else { + return App(func, paramHead); + } + } + + public static FuncAppExpr App( + final Expr> func, final List params) { + checkArgument(!params.isEmpty()); + final var paramHead = params.get(params.size() - 1); + final var paramTail = params.subList(0, params.size() - 1); + return App(func, paramHead, paramTail); + } + } diff --git a/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/IdentityTest.java b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/IdentityTest.java new file mode 100644 index 0000000000..277bec50ef --- /dev/null +++ b/subprojects/common/core/src/test/java/hu/bme/mit/theta/core/expr/IdentityTest.java @@ -0,0 +1,48 @@ +/* + * 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. + */ + +package hu.bme.mit.theta.core.expr; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.utils.ExpressionUtils; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; + +import java.util.Collection; + +@RunWith(Parameterized.class) +public class IdentityTest { + @Parameter(value = 0) + public String className; + + @Parameter(value = 1) + public Expr expr; + + + @Parameters(name = "Expression {0}: {1}") + public static Collection data() { + return ExpressionUtils.AllExpressions().entrySet().stream().map(e -> new Object[]{e.getKey(), e.getValue()}).toList(); + } + + @Test + public void testRoundtrip() { + Assert.assertEquals(expr.withOps(expr.getOps()), expr); + } +} diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/ArrayTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/ArrayTestUtils.java new file mode 100644 index 0000000000..39eb1e84b9 --- /dev/null +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/ArrayTestUtils.java @@ -0,0 +1,59 @@ +/* + * 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. + */ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayType; +import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; + +import java.util.Arrays; +import java.util.Collection; +import java.util.List; + +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; + +public class ArrayTestUtils { + + private ArrayTestUtils() { + } + + public static Collection BasicOperations() { + + final var c1 = Const("arr", ArrayType.of(Int(), Int())); + + return Arrays.asList(new Object[][]{ + + {ArrayReadExpr.class, Int(5), ArrayReadExpr.of(ArrayWriteExpr.of(c1.getRef(), Int(0), Int(5)), Int(0))}, + {ArrayEqExpr.class, True(), ArrayEqExpr.of(c1.getRef(), c1.getRef())}, + {ArrayNeqExpr.class, False(), ArrayNeqExpr.of(c1.getRef(), c1.getRef())}, + + {ArrayReadExpr.class, Int(5), ArrayReadExpr.of(ArrayLitExpr.of(List.of(), Int(5), ArrayType.of(Int(), Int())), Int(42))}, + {ArrayReadExpr.class, Int(5), ArrayReadExpr.of(ArrayInitExpr.of(List.of(), Int(5), ArrayType.of(Int(), Int())), Int(42))}, + + {ArrayReadExpr.class, Int(3), ArrayReadExpr.of(ArrayLitExpr.of(List.of(Tuple2.of(Int(42), Int(3))), Int(5), ArrayType.of(Int(), Int())), Int(42))}, + {ArrayReadExpr.class, Int(3), ArrayReadExpr.of(ArrayInitExpr.of(List.of(Tuple2.of(Int(42), Int(3))), Int(5), ArrayType.of(Int(), Int())), Int(42))}, + }); + } + +} diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BoolTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BoolTestUtils.java new file mode 100644 index 0000000000..4d11a5ded7 --- /dev/null +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BoolTestUtils.java @@ -0,0 +1,78 @@ +/* + * 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. + */ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.core.type.anytype.IteExpr; +import hu.bme.mit.theta.core.type.booltype.ExistsExpr; +import hu.bme.mit.theta.core.type.booltype.ForallExpr; +import hu.bme.mit.theta.core.type.booltype.ImplyExpr; +import hu.bme.mit.theta.core.type.booltype.OrExpr; +import hu.bme.mit.theta.core.type.booltype.XorExpr; + +import java.util.Arrays; +import java.util.Collection; +import java.util.List; + +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.decl.Decls.Param; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Geq; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Ite; +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Lt; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.And; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Xor; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; + +public class BoolTestUtils { + + private BoolTestUtils() { + } + + public static Collection BasicOperations() { + final var p1 = Param("x", Int()); + final var p2 = Param("y", Int()); + final var p3 = Param("z", Int()); + final var c1 = Const("c", Int()); + + return Arrays.asList(new Object[][]{ + + {IteExpr.class, Ite(Geq(c1.getRef(), Int(0)), Int(1), Int(2)), Ite(Lt(c1.getRef(), Int(0)), Int(2), Int(1))}, + {ImplyExpr.class, False(), Imply(True(), False())}, + {ImplyExpr.class, False(), Imply(True(), False())}, + {XorExpr.class, False(), Xor(True(), True())}, + {OrExpr.class, True(), Or(True(), True())}, + {ExistsExpr.class, True(), Exists(List.of(p1), Eq(p1.getRef(), Int(0)))}, + {ForallExpr.class, False(), Forall(List.of(p1), Eq(p1.getRef(), Int(0)))}, + + {ExistsExpr.class, True(), Exists(List.of(p1), Exists(List.of(p2), Eq(p1.getRef(), p2.getRef())))}, + {ForallExpr.class, False(), Forall(List.of(p1), Forall(List.of(p2), Eq(p1.getRef(), p2.getRef())))}, + + {ExistsExpr.class, False(), Exists(List.of(p1, p2), Exists(List.of(p3), And(List.of( + Lt(p1.getRef(), p2.getRef()), + Lt(p2.getRef(), p3.getRef()), + Lt(p3.getRef(), p1.getRef()) + ))))}, + + }); + } + +} diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/BvTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BvTestUtils.java similarity index 98% rename from subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/BvTestUtils.java rename to subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BvTestUtils.java index a0f35d8cc2..cfb2e00e37 100644 --- a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/utils/BvTestUtils.java +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BvTestUtils.java @@ -28,6 +28,7 @@ import hu.bme.mit.theta.core.type.bvtype.BvNeqExpr; import hu.bme.mit.theta.core.type.bvtype.BvNotExpr; import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; +import hu.bme.mit.theta.core.type.bvtype.BvPosExpr; import hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr; import hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr; import hu.bme.mit.theta.core.type.bvtype.BvSDivExpr; @@ -70,6 +71,7 @@ import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Neq; import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Not; import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Or; +import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Pos; import static hu.bme.mit.theta.core.type.bvtype.BvExprs.RotateLeft; import static hu.bme.mit.theta.core.type.bvtype.BvExprs.RotateRight; import static hu.bme.mit.theta.core.type.bvtype.BvExprs.SDiv; @@ -132,6 +134,9 @@ public static Collection BasicOperations() { {BvAddExpr.class, SBv16(-32768), Add(List.of(SBv16(32767), SBv16(1)))}, {BvSubExpr.class, SBv16(32767), Sub(SBv16(-32768), SBv16(1))}, {BvMulExpr.class, SBv16(-32768), Mul(List.of(SBv16(16384), SBv16(2)))}, + + {BvPosExpr.class, SBv16(-5), Pos(SBv16(-5))}, + {BvNegExpr.class, SBv16(5), Neg(SBv16(-5))}, }); } diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/ExpressionUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/ExpressionUtils.java new file mode 100644 index 0000000000..47efd30c40 --- /dev/null +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/ExpressionUtils.java @@ -0,0 +1,64 @@ +/* + * 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. + */ + +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.QuantifiedExpr; +import hu.bme.mit.theta.core.type.functype.FuncAppExpr; + +import java.util.Map; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +public class ExpressionUtils { + + private static Stream> getWithAllOps(Expr e) { + if (e instanceof QuantifiedExpr || e instanceof FuncAppExpr) { + return Stream.of(e); // we don't want their body to be unwrapped, as they contain ParamDecls + } + return Stream.concat(Stream.of(e), e.getOps().stream()); + } + + public static Map> AllExpressions() { + return Stream.of( + BvTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[2]), + BvTestUtils.BitvectorOperations().stream().map(o -> ((Object[]) o)[2]), + BvTestUtils.RelationalOperations().stream().map(o -> ((Object[]) o)[2]), + FpTestUtils.GetOperations().map(o -> ((Object[]) o)[2]), + IntTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[2]), + RatTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[2]), + BoolTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[2]), + ArrayTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[2]), + FuncTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[2]), + + + BvTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[1]), + BvTestUtils.BitvectorOperations().stream().map(o -> ((Object[]) o)[1]), + BvTestUtils.RelationalOperations().stream().map(o -> ((Object[]) o)[1]), + FpTestUtils.GetOperations().map(o -> ((Object[]) o)[1]), + IntTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[1]), + RatTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[1]), + BoolTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[1]), + ArrayTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[1]), + FuncTestUtils.BasicOperations().stream().map(o -> ((Object[]) o)[1])) + + .reduce(Stream::concat).get() + .map(o -> (Expr) o) + .flatMap(ExpressionUtils::getWithAllOps) + .collect(Collectors.toMap(o -> o.getClass().getSimpleName(), o -> o, (expr, expr2) -> expr2)); + } +} diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/FpTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/FpTestUtils.java index 941714a40b..1ac7aa2d51 100644 --- a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/FpTestUtils.java +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/FpTestUtils.java @@ -19,11 +19,13 @@ import hu.bme.mit.theta.common.OsHelper; import hu.bme.mit.theta.core.type.fptype.FpAbsExpr; import hu.bme.mit.theta.core.type.fptype.FpAddExpr; +import hu.bme.mit.theta.core.type.fptype.FpAssignExpr; import hu.bme.mit.theta.core.type.fptype.FpDivExpr; import hu.bme.mit.theta.core.type.fptype.FpEqExpr; import hu.bme.mit.theta.core.type.fptype.FpFromBvExpr; import hu.bme.mit.theta.core.type.fptype.FpGeqExpr; import hu.bme.mit.theta.core.type.fptype.FpGtExpr; +import hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr; import hu.bme.mit.theta.core.type.fptype.FpIsNanExpr; import hu.bme.mit.theta.core.type.fptype.FpLeqExpr; import hu.bme.mit.theta.core.type.fptype.FpLitExpr; @@ -54,10 +56,12 @@ import static hu.bme.mit.theta.core.type.fptype.FpExprs.Add; import static hu.bme.mit.theta.core.type.fptype.FpExprs.Div; import static hu.bme.mit.theta.core.type.fptype.FpExprs.Eq; +import static hu.bme.mit.theta.core.type.fptype.FpExprs.FpAssign; import static hu.bme.mit.theta.core.type.fptype.FpExprs.FpType; import static hu.bme.mit.theta.core.type.fptype.FpExprs.FromBv; import static hu.bme.mit.theta.core.type.fptype.FpExprs.Geq; import static hu.bme.mit.theta.core.type.fptype.FpExprs.Gt; +import static hu.bme.mit.theta.core.type.fptype.FpExprs.IsInfinite; import static hu.bme.mit.theta.core.type.fptype.FpExprs.IsNan; import static hu.bme.mit.theta.core.type.fptype.FpExprs.Leq; import static hu.bme.mit.theta.core.type.fptype.FpExprs.Lt; @@ -112,6 +116,8 @@ private static Collection BasicOperations() { {FpDivExpr.class, Fp16("2.1"), Div(RNE, Fp16("7.14"), Fp16("3.4"))}, {FpEqExpr.class, Bool(true), Eq(Fp16("7.14"), Fp16("7.14"))}, {FpEqExpr.class, Bool(false), Eq(Fp16("7.14"), Fp16("7.15"))}, + {FpEqExpr.class, Bool(false), Eq(Fp16NaN(), Fp16NaN())}, + {FpAssignExpr.class, Bool(true), FpAssign(Fp16NaN(), Fp16NaN())}, {FpNeqExpr.class, Bool(true), Neq(Fp16("-7.14"), Fp16("7.14"))}, {FpNeqExpr.class, Bool(false), Neq(Fp16("-7.14"), Fp16("-7.14"))}, {FpAbsExpr.class, Fp16("2.1"), Abs(Fp16("2.1"))}, @@ -126,6 +132,9 @@ private static Collection BasicOperations() { {FpIsNanExpr.class, Bool(false), IsNan(Fp16PInf())}, {FpIsNanExpr.class, Bool(false), IsNan(Fp16NInf())}, {FpIsNanExpr.class, Bool(false), IsNan(Fp16("0.0"))}, + {FpIsInfiniteExpr.class, Bool(false), IsInfinite(Fp16("0.0"))}, + {FpIsInfiniteExpr.class, Bool(true), IsInfinite(FpTestUtils.Fp16PInf())}, + {FpIsInfiniteExpr.class, Bool(true), IsInfinite(FpTestUtils.Fp16NInf())}, {FpLeqExpr.class, Bool(true), Leq(Fp16("7.14"), Fp16("7.15"))}, {FpLeqExpr.class, Bool(true), Leq(Fp16("7.14"), Fp16("7.14"))}, {FpLeqExpr.class, Bool(false), Leq(Fp16("-7.14"), Fp16("-7.15"))}, diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/FuncTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/FuncTestUtils.java new file mode 100644 index 0000000000..bc0c90b86d --- /dev/null +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/FuncTestUtils.java @@ -0,0 +1,47 @@ +/* + * 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. + */ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.core.type.functype.FuncAppExpr; +import hu.bme.mit.theta.core.type.functype.FuncType; + +import java.util.Arrays; +import java.util.Collection; + +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.functype.FuncExprs.App; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; + +public class FuncTestUtils { + + private FuncTestUtils() { + } + + public static Collection BasicOperations() { + final var sortFuncType = FuncType.of(Int(), FuncType.of(Int(), Bool())); + final var sortFunc = Const("sort", sortFuncType); + + return Arrays.asList(new Object[][]{ + + {FuncAppExpr.class, + App(App(sortFunc.getRef(), Int(0)), Int(1)), + App(App(sortFunc.getRef(), Int(0)), Int(1))}, + + }); + } + +} diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/IntTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/IntTestUtils.java new file mode 100644 index 0000000000..a52ce7613a --- /dev/null +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/IntTestUtils.java @@ -0,0 +1,102 @@ +/* + * 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. + */ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.core.type.inttype.IntAddExpr; +import hu.bme.mit.theta.core.type.inttype.IntDivExpr; +import hu.bme.mit.theta.core.type.inttype.IntEqExpr; +import hu.bme.mit.theta.core.type.inttype.IntGeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntGtExpr; +import hu.bme.mit.theta.core.type.inttype.IntLeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntLtExpr; +import hu.bme.mit.theta.core.type.inttype.IntModExpr; +import hu.bme.mit.theta.core.type.inttype.IntMulExpr; +import hu.bme.mit.theta.core.type.inttype.IntNegExpr; +import hu.bme.mit.theta.core.type.inttype.IntNeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntPosExpr; +import hu.bme.mit.theta.core.type.inttype.IntRemExpr; +import hu.bme.mit.theta.core.type.inttype.IntSubExpr; + +import java.util.Arrays; +import java.util.Collection; +import java.util.List; + +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Div; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Geq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Gt; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Leq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Lt; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Mod; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Mul; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Neg; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Neq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Pos; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Rem; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Sub; + +public class IntTestUtils { + + private IntTestUtils() { + } + + public static Collection BasicOperations() { + final var c1 = Const("x", Int()); + + return Arrays.asList(new Object[][]{ + + {IntAddExpr.class, Int(4), Add(List.of(Int(1), Int(3)))}, + {IntSubExpr.class, Int(1), Sub(Int(4), Int(3))}, + {IntMulExpr.class, Int(12), Mul(List.of(Int(4), Int(3)))}, + {IntDivExpr.class, Int(4), Div(Int(12), Int(3))}, + {IntModExpr.class, Int(1), Mod(Int(13), Int(3))}, + {IntRemExpr.class, Int(1), Rem(Int(13), Int(3))}, + + {IntAddExpr.class, Int(4), Add(List.of(Int(-1), Int(5)))}, + {IntSubExpr.class, Int(-2), Sub(Int(4), Int(6))}, + {IntMulExpr.class, Int(-12), Mul(List.of(Int(-4), Int(3)))}, + {IntDivExpr.class, Int(-4), Div(Int(12), Int(-3))}, + {IntModExpr.class, Int(2), Mod(Int(-13), Int(3))}, + {IntRemExpr.class, Int(1), Rem(Int(13), Int(3))}, + {IntRemExpr.class, Int(-1), Rem(Int(13), Int(-3))}, + {IntRemExpr.class, Int(2), Rem(Int(-13), Int(3))}, + {IntRemExpr.class, Int(-2), Rem(Int(-13), Int(-3))}, + {IntNegExpr.class, Int(-13), Neg(Int(13))}, + + + {IntEqExpr.class, False(), Eq(Int(1), Int(3))}, + {IntEqExpr.class, True(), Eq(Int(3), Int(3))}, + {IntNeqExpr.class, True(), Neq(Int(1), Int(3))}, + {IntNeqExpr.class, False(), Neq(Int(3), Int(3))}, + {IntGeqExpr.class, False(), Geq(Int(1), Int(3))}, + {IntGeqExpr.class, True(), Geq(Int(3), Int(3))}, + {IntGtExpr.class, False(), Gt(Int(1), Int(3))}, + {IntGtExpr.class, False(), Gt(Int(3), Int(3))}, + {IntLeqExpr.class, True(), Leq(Int(1), Int(3))}, + {IntLeqExpr.class, True(), Leq(Int(3), Int(3))}, + {IntLtExpr.class, True(), Lt(Int(1), Int(3))}, + {IntLtExpr.class, False(), Lt(Int(3), Int(3))}, + + {IntPosExpr.class, c1.getRef(), Pos(c1.getRef())}, + }); + } + +} diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/RatTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/RatTestUtils.java new file mode 100644 index 0000000000..88f2fa73e5 --- /dev/null +++ b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/RatTestUtils.java @@ -0,0 +1,93 @@ +/* + * 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. + */ +package hu.bme.mit.theta.core.utils; + +import hu.bme.mit.theta.core.type.inttype.IntToRatExpr; +import hu.bme.mit.theta.core.type.rattype.RatAddExpr; +import hu.bme.mit.theta.core.type.rattype.RatDivExpr; +import hu.bme.mit.theta.core.type.rattype.RatEqExpr; +import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatGtExpr; +import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatLtExpr; +import hu.bme.mit.theta.core.type.rattype.RatMulExpr; +import hu.bme.mit.theta.core.type.rattype.RatNegExpr; +import hu.bme.mit.theta.core.type.rattype.RatNeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatSubExpr; +import hu.bme.mit.theta.core.type.rattype.RatToIntExpr; + +import java.util.Arrays; +import java.util.Collection; +import java.util.List; + +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.ToRat; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Add; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Div; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Eq; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Geq; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Gt; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Leq; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Lt; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Mul; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Neg; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Neq; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Sub; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.ToInt; + +public class RatTestUtils { + + private RatTestUtils() { + } + + public static Collection BasicOperations() { + return Arrays.asList(new Object[][]{ + + {RatAddExpr.class, Rat(4, 1), Add(List.of(Rat(1, 1), Rat(3, 1)))}, + {RatSubExpr.class, Rat(1, 1), Sub(Rat(4, 1), Rat(3, 1))}, + {RatMulExpr.class, Rat(12, 1), Mul(List.of(Rat(4, 1), Rat(3, 1)))}, + {RatDivExpr.class, Rat(4, 1), Div(Rat(12, 1), Rat(3, 1))}, + + {RatAddExpr.class, Rat(4, 1), Add(List.of(Rat(-1, 1), Rat(5, 1)))}, + {RatSubExpr.class, Rat(-2, 1), Sub(Rat(4, 1), Rat(6, 1))}, + {RatMulExpr.class, Rat(-12, 1), Mul(List.of(Rat(-4, 1), Rat(3, 1)))}, + {RatDivExpr.class, Rat(-4, 1), Div(Rat(12, 1), Rat(-3, 1))}, + {RatNegExpr.class, Rat(-13, 1), Neg(Rat(13, 1))}, + + + {RatEqExpr.class, False(), Eq(Rat(1, 1), Rat(3, 1))}, + {RatEqExpr.class, True(), Eq(Rat(3, 1), Rat(3, 1))}, + {RatNeqExpr.class, True(), Neq(Rat(1, 1), Rat(3, 1))}, + {RatNeqExpr.class, False(), Neq(Rat(3, 1), Rat(3, 1))}, + {RatGeqExpr.class, False(), Geq(Rat(1, 1), Rat(3, 1))}, + {RatGeqExpr.class, True(), Geq(Rat(3, 1), Rat(3, 1))}, + {RatGtExpr.class, False(), Gt(Rat(1, 1), Rat(3, 1))}, + {RatGtExpr.class, False(), Gt(Rat(3, 1), Rat(3, 1))}, + {RatLeqExpr.class, True(), Leq(Rat(1, 1), Rat(3, 1))}, + {RatLeqExpr.class, True(), Leq(Rat(3, 1), Rat(3, 1))}, + {RatLtExpr.class, True(), Lt(Rat(1, 1), Rat(3, 1))}, + {RatLtExpr.class, False(), Lt(Rat(3, 1), Rat(3, 1))}, + + {RatToIntExpr.class, Int(5), ToInt(Rat(11, 2))}, + {IntToRatExpr.class, Rat(5, 1), ToRat(Int(5))}, + + }); + } + +} diff --git a/subprojects/solver/solver-javasmt/README.md b/subprojects/solver/solver-javasmt/README.md new file mode 100644 index 0000000000..8f033d7c0f --- /dev/null +++ b/subprojects/solver/solver-javasmt/README.md @@ -0,0 +1,2 @@ +This project wraps the [JavaSMT solver wrapper](https://github.com/sosy-lab/java-smt) into our common interfaces for solvers (located in the [solver](../solver) project). +Normally, only the factory class should be used from this project to instantiate a new solver and then the common interfaces should be preferred. The [factory](./src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java) needs a [Solvers](https://github.com/sosy-lab/java-smt/blob/12ceedfa6a8412268f77b8a7af7fb7a1b97bbd29/src/org/sosy_lab/java_smt/SolverContextFactory.java#L51-L61) enum value, or the [manager](./src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java) needs a string with the same values after the `JavaSMT:` prefix. diff --git a/subprojects/solver/solver-javasmt/bin/.gitignore b/subprojects/solver/solver-javasmt/bin/.gitignore new file mode 100644 index 0000000000..7eed456bec --- /dev/null +++ b/subprojects/solver/solver-javasmt/bin/.gitignore @@ -0,0 +1,2 @@ +/main/ +/test/ diff --git a/subprojects/solver/solver-javasmt/build.gradle.kts b/subprojects/solver/solver-javasmt/build.gradle.kts new file mode 100644 index 0000000000..babcca831b --- /dev/null +++ b/subprojects/solver/solver-javasmt/build.gradle.kts @@ -0,0 +1,28 @@ +/* + * 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. + */ +plugins { + id("java-common") +} + +dependencies { + implementation(project(":theta-common")) + implementation(project(":theta-core")) + implementation(project(":theta-solver")) + implementation(files(rootDir.resolve(Deps.javasmtLocal))) + implementation(Deps.javasmt) + implementation(files(rootDir.resolve(Deps.cvc5))) + testImplementation(testFixtures(project(":theta-core"))) +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTDeclTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTDeclTransformer.java new file mode 100644 index 0000000000..27e53ea8ac --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTDeclTransformer.java @@ -0,0 +1,109 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.functype.FuncType; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.SolverContext; + +import java.util.List; + +import static com.google.common.base.Preconditions.checkArgument; + +final class JavaSMTDeclTransformer { + + private final JavaSMTTransformationManager transformer; + private final JavaSMTSymbolTable symbolTable; + private final SolverContext context; + + private int symbolCount; + + JavaSMTDeclTransformer(final JavaSMTTransformationManager transformer, final JavaSMTSymbolTable symbolTable, + final SolverContext context) { + this.transformer = transformer; + this.symbolTable = symbolTable; + this.context = context; + this.symbolCount = 0; + } + + public Formula toSymbol(final Decl decl) { + if (decl instanceof ConstDecl) { + return transformConst((ConstDecl) decl); + } else { + throw new UnsupportedOperationException("Cannot transform declaration: " + decl); + } + } + + private Formula transformConst(final ConstDecl decl) { + final Formula symbol; + + if (symbolTable.definesConstAsFormula(decl)) { + symbol = symbolTable.getSymbolAsFormula(decl); + } else { + final Type type = decl.getType(); + + final Tuple2, Type> extractedTypes = extractTypes(type); + final List paramTypes = extractedTypes.get1(); + final Type returnType = extractedTypes.get2(); + + final FormulaType returnSort = transformer.toSort(returnType); + final List> paramSorts = paramTypes.stream() + .map(transformer::toSort) + .toList(); + + + if (paramSorts.isEmpty()) { + symbol = context.getFormulaManager().makeVariable(returnSort, symbolNameFor(decl)); + } else { + throw new JavaSMTSolverException("Function consts not yet supported."); + } + + symbolTable.put(decl, symbol); + } + + return symbol; + } + + private Tuple2, Type> extractTypes(final Type type) { + if (type instanceof FuncType funcType) { + + final Type paramType = funcType.getParamType(); + final Type resultType = funcType.getResultType(); + + checkArgument(!(paramType instanceof FuncType), "Parameter type most not be function"); + + final Tuple2, Type> subResult = extractTypes(resultType); + final List paramTypes = subResult.get1(); + final Type newResultType = subResult.get2(); + final List newParamTypes = ImmutableList.builder().add(paramType) + .addAll(paramTypes).build(); + return Tuple2.of(newParamTypes, newResultType); + } else { + return Tuple2.of(ImmutableList.of(), type); + } + } + + private String symbolNameFor(final Decl decl) { + return String.format("%s_%d", decl.getName(), symbolCount++); + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java new file mode 100644 index 0000000000..87dc5f2927 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java @@ -0,0 +1,1335 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.cache.Cache; +import com.google.common.cache.CacheBuilder; +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.common.DispatchTable; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.common.dsl.Env; +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.decl.ParamDecl; +import hu.bme.mit.theta.core.dsl.DeclSymbol; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.anytype.IteExpr; +import hu.bme.mit.theta.core.type.anytype.RefExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayEqExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayNeqExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr; +import hu.bme.mit.theta.core.type.booltype.AndExpr; +import hu.bme.mit.theta.core.type.booltype.ExistsExpr; +import hu.bme.mit.theta.core.type.booltype.FalseExpr; +import hu.bme.mit.theta.core.type.booltype.ForallExpr; +import hu.bme.mit.theta.core.type.booltype.IffExpr; +import hu.bme.mit.theta.core.type.booltype.ImplyExpr; +import hu.bme.mit.theta.core.type.booltype.NotExpr; +import hu.bme.mit.theta.core.type.booltype.OrExpr; +import hu.bme.mit.theta.core.type.booltype.TrueExpr; +import hu.bme.mit.theta.core.type.booltype.XorExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAddExpr; +import hu.bme.mit.theta.core.type.bvtype.BvAndExpr; +import hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvConcatExpr; +import hu.bme.mit.theta.core.type.bvtype.BvEqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvExtractExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvMulExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNegExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvNotExpr; +import hu.bme.mit.theta.core.type.bvtype.BvOrExpr; +import hu.bme.mit.theta.core.type.bvtype.BvPosExpr; +import hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSDivExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSExtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSGtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSLtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSModExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr; +import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSubExpr; +import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr; +import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvUGtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvULeqExpr; +import hu.bme.mit.theta.core.type.bvtype.BvULtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvURemExpr; +import hu.bme.mit.theta.core.type.bvtype.BvXorExpr; +import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; +import hu.bme.mit.theta.core.type.fptype.FpAbsExpr; +import hu.bme.mit.theta.core.type.fptype.FpAddExpr; +import hu.bme.mit.theta.core.type.fptype.FpAssignExpr; +import hu.bme.mit.theta.core.type.fptype.FpDivExpr; +import hu.bme.mit.theta.core.type.fptype.FpEqExpr; +import hu.bme.mit.theta.core.type.fptype.FpFromBvExpr; +import hu.bme.mit.theta.core.type.fptype.FpGeqExpr; +import hu.bme.mit.theta.core.type.fptype.FpGtExpr; +import hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr; +import hu.bme.mit.theta.core.type.fptype.FpIsNanExpr; +import hu.bme.mit.theta.core.type.fptype.FpLeqExpr; +import hu.bme.mit.theta.core.type.fptype.FpLitExpr; +import hu.bme.mit.theta.core.type.fptype.FpLtExpr; +import hu.bme.mit.theta.core.type.fptype.FpMaxExpr; +import hu.bme.mit.theta.core.type.fptype.FpMinExpr; +import hu.bme.mit.theta.core.type.fptype.FpMulExpr; +import hu.bme.mit.theta.core.type.fptype.FpNegExpr; +import hu.bme.mit.theta.core.type.fptype.FpNeqExpr; +import hu.bme.mit.theta.core.type.fptype.FpPosExpr; +import hu.bme.mit.theta.core.type.fptype.FpRemExpr; +import hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr; +import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; +import hu.bme.mit.theta.core.type.fptype.FpSqrtExpr; +import hu.bme.mit.theta.core.type.fptype.FpSubExpr; +import hu.bme.mit.theta.core.type.fptype.FpToBvExpr; +import hu.bme.mit.theta.core.type.fptype.FpToFpExpr; +import hu.bme.mit.theta.core.type.functype.FuncAppExpr; +import hu.bme.mit.theta.core.type.functype.FuncType; +import hu.bme.mit.theta.core.type.inttype.IntAddExpr; +import hu.bme.mit.theta.core.type.inttype.IntDivExpr; +import hu.bme.mit.theta.core.type.inttype.IntEqExpr; +import hu.bme.mit.theta.core.type.inttype.IntGeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntGtExpr; +import hu.bme.mit.theta.core.type.inttype.IntLeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntLitExpr; +import hu.bme.mit.theta.core.type.inttype.IntLtExpr; +import hu.bme.mit.theta.core.type.inttype.IntModExpr; +import hu.bme.mit.theta.core.type.inttype.IntMulExpr; +import hu.bme.mit.theta.core.type.inttype.IntNegExpr; +import hu.bme.mit.theta.core.type.inttype.IntNeqExpr; +import hu.bme.mit.theta.core.type.inttype.IntPosExpr; +import hu.bme.mit.theta.core.type.inttype.IntRemExpr; +import hu.bme.mit.theta.core.type.inttype.IntSubExpr; +import hu.bme.mit.theta.core.type.inttype.IntToRatExpr; +import hu.bme.mit.theta.core.type.rattype.RatAddExpr; +import hu.bme.mit.theta.core.type.rattype.RatDivExpr; +import hu.bme.mit.theta.core.type.rattype.RatEqExpr; +import hu.bme.mit.theta.core.type.rattype.RatGeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatGtExpr; +import hu.bme.mit.theta.core.type.rattype.RatLeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatLitExpr; +import hu.bme.mit.theta.core.type.rattype.RatLtExpr; +import hu.bme.mit.theta.core.type.rattype.RatMulExpr; +import hu.bme.mit.theta.core.type.rattype.RatNegExpr; +import hu.bme.mit.theta.core.type.rattype.RatNeqExpr; +import hu.bme.mit.theta.core.type.rattype.RatPosExpr; +import hu.bme.mit.theta.core.type.rattype.RatSubExpr; +import hu.bme.mit.theta.core.type.rattype.RatToIntExpr; +import hu.bme.mit.theta.core.utils.BvUtils; +import org.sosy_lab.java_smt.api.ArrayFormula; +import org.sosy_lab.java_smt.api.ArrayFormulaManager; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BitvectorFormulaManager; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.BooleanFormulaManager; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormulaManager; +import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.IntegerFormulaManager; +import org.sosy_lab.java_smt.api.NumeralFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager; +import org.sosy_lab.java_smt.api.RationalFormulaManager; +import org.sosy_lab.java_smt.api.SolverContext; + +import java.util.ArrayList; +import java.util.List; +import java.util.concurrent.ExecutionException; +import java.util.function.Supplier; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +final class JavaSMTExprTransformer { + + private static final int CACHE_SIZE = 1000; + private final BooleanFormulaManager booleanFormulaManager; + private final IntegerFormulaManager integerFormulaManager; + private final RationalFormulaManager rationalFormulaManager; + private final BitvectorFormulaManager bitvectorFormulaManager; + private final FloatingPointFormulaManager floatingPointFormulaManager; + private final QuantifiedFormulaManager quantifiedFormulaManager; + private final ArrayFormulaManager arrayFormulaManager; + + private final JavaSMTTransformationManager transformer; + private final JavaSMTSymbolTable symbolTable; + private final SolverContext context; + + private final Cache, Formula> exprToTerm; + private final DispatchTable table; + private final Env env; + + public JavaSMTExprTransformer(final JavaSMTTransformationManager transformer, final JavaSMTSymbolTable symbolTable, final SolverContext context) { + this.symbolTable = symbolTable; + this.context = context; + this.transformer = transformer; + this.env = new Env(); + + booleanFormulaManager = orElseNull(() -> context.getFormulaManager().getBooleanFormulaManager()); + integerFormulaManager = orElseNull(() -> context.getFormulaManager().getIntegerFormulaManager()); + rationalFormulaManager = orElseNull(() -> context.getFormulaManager().getRationalFormulaManager()); + bitvectorFormulaManager = orElseNull(() -> context.getFormulaManager().getBitvectorFormulaManager()); + floatingPointFormulaManager = orElseNull(() -> context.getFormulaManager().getFloatingPointFormulaManager()); + quantifiedFormulaManager = orElseNull(() -> context.getFormulaManager().getQuantifiedFormulaManager()); + arrayFormulaManager = orElseNull(() -> context.getFormulaManager().getArrayFormulaManager()); + + exprToTerm = CacheBuilder.newBuilder().maximumSize(CACHE_SIZE).build(); + + table = DispatchTable.builder() + + // General + + .addCase(RefExpr.class, this::transformRef) + + .addCase(IteExpr.class, this::transformIte) + + // Boolean + + .addCase(FalseExpr.class, this::transformFalse) + + .addCase(TrueExpr.class, this::transformTrue) + + .addCase(NotExpr.class, this::transformNot) + + .addCase(ImplyExpr.class, this::transformImply) + + .addCase(IffExpr.class, this::transformIff) + + .addCase(XorExpr.class, this::transformXor) + + .addCase(AndExpr.class, this::transformAnd) + + .addCase(OrExpr.class, this::transformOr) + + .addCase(ExistsExpr.class, this::transformExists) + + .addCase(ForallExpr.class, this::transformForall) + + // Rationals + + .addCase(RatLitExpr.class, this::transformRatLit) + + .addCase(RatAddExpr.class, this::transformRatAdd) + + .addCase(RatSubExpr.class, this::transformRatSub) + + .addCase(RatPosExpr.class, this::transformRatPos) + + .addCase(RatNegExpr.class, this::transformRatNeg) + + .addCase(RatMulExpr.class, this::transformRatMul) + + .addCase(RatDivExpr.class, this::transformRatDiv) + + .addCase(RatEqExpr.class, this::transformRatEq) + + .addCase(RatNeqExpr.class, this::transformRatNeq) + + .addCase(RatGeqExpr.class, this::transformRatGeq) + + .addCase(RatGtExpr.class, this::transformRatGt) + + .addCase(RatLeqExpr.class, this::transformRatLeq) + + .addCase(RatLtExpr.class, this::transformRatLt) + + .addCase(RatToIntExpr.class, this::transformRatToInt) + + // Integers + + .addCase(IntLitExpr.class, this::transformIntLit) + + .addCase(IntAddExpr.class, this::transformIntAdd) + + .addCase(IntSubExpr.class, this::transformIntSub) + + .addCase(IntPosExpr.class, this::transformIntPos) + + .addCase(IntNegExpr.class, this::transformIntNeg) + + .addCase(IntMulExpr.class, this::transformIntMul) + + .addCase(IntDivExpr.class, this::transformIntDiv) + + .addCase(IntModExpr.class, this::transformIntMod) + + .addCase(IntRemExpr.class, this::transformIntRem) + + .addCase(IntEqExpr.class, this::transformIntEq) + + .addCase(IntNeqExpr.class, this::transformIntNeq) + + .addCase(IntGeqExpr.class, this::transformIntGeq) + + .addCase(IntGtExpr.class, this::transformIntGt) + + .addCase(IntLeqExpr.class, this::transformIntLeq) + + .addCase(IntLtExpr.class, this::transformIntLt) + + .addCase(IntToRatExpr.class, this::transformIntToRat) + + // Bitvectors + + .addCase(BvLitExpr.class, this::transformBvLit) + + .addCase(BvConcatExpr.class, this::transformBvConcat) + + .addCase(BvExtractExpr.class, this::transformBvExtract) + + .addCase(BvZExtExpr.class, this::transformBvZExt) + + .addCase(BvSExtExpr.class, this::transformBvSExt) + + .addCase(BvAddExpr.class, this::transformBvAdd) + + .addCase(BvSubExpr.class, this::transformBvSub) + + .addCase(BvPosExpr.class, this::transformBvPos) + + .addCase(BvSignChangeExpr.class, this::transformBvSignChange) + + .addCase(BvNegExpr.class, this::transformBvNeg) + + .addCase(BvMulExpr.class, this::transformBvMul) + + .addCase(BvUDivExpr.class, this::transformBvUDiv) + + .addCase(BvSDivExpr.class, this::transformBvSDiv) + + .addCase(BvSModExpr.class, this::transformBvSMod) + + .addCase(BvURemExpr.class, this::transformBvURem) + + .addCase(BvSRemExpr.class, this::transformBvSRem) + + .addCase(BvAndExpr.class, this::transformBvAnd) + + .addCase(BvOrExpr.class, this::transformBvOr) + + .addCase(BvXorExpr.class, this::transformBvXor) + + .addCase(BvNotExpr.class, this::transformBvNot) + + .addCase(BvShiftLeftExpr.class, this::transformBvShiftLeft) + + .addCase(BvArithShiftRightExpr.class, this::transformBvArithShiftRight) + + .addCase(BvLogicShiftRightExpr.class, this::transformBvLogicShiftRight) + + .addCase(BvRotateLeftExpr.class, this::transformBvRotateLeft) + + .addCase(BvRotateRightExpr.class, this::transformBvRotateRight) + + .addCase(BvEqExpr.class, this::transformBvEq) + + .addCase(BvNeqExpr.class, this::transformBvNeq) + + .addCase(BvUGeqExpr.class, this::transformBvUGeq) + + .addCase(BvUGtExpr.class, this::transformBvUGt) + + .addCase(BvULeqExpr.class, this::transformBvULeq) + + .addCase(BvULtExpr.class, this::transformBvULt) + + .addCase(BvSGeqExpr.class, this::transformBvSGeq) + + .addCase(BvSGtExpr.class, this::transformBvSGt) + + .addCase(BvSLeqExpr.class, this::transformBvSLeq) + + .addCase(BvSLtExpr.class, this::transformBvSLt) + + // Floating points + + .addCase(FpLitExpr.class, this::transformFpLit) + + .addCase(FpAddExpr.class, this::transformFpAdd) + + .addCase(FpSubExpr.class, this::transformFpSub) + + .addCase(FpPosExpr.class, this::transformFpPos) + + .addCase(FpNegExpr.class, this::transformFpNeg) + + .addCase(FpMulExpr.class, this::transformFpMul) + + .addCase(FpDivExpr.class, this::transformFpDiv) + + .addCase(FpEqExpr.class, this::transformFpEq) + + .addCase(FpAssignExpr.class, this::transformFpAssign) + + .addCase(FpGeqExpr.class, this::transformFpGeq) + + .addCase(FpLeqExpr.class, this::transformFpLeq) + + .addCase(FpGtExpr.class, this::transformFpGt) + + .addCase(FpLtExpr.class, this::transformFpLt) + + .addCase(FpNeqExpr.class, this::transformFpNeq) + + .addCase(FpAbsExpr.class, this::transformFpAbs) + + .addCase(FpRoundToIntegralExpr.class, this::transformFpRoundToIntegral) + + .addCase(FpMaxExpr.class, this::transformFpMax) + + .addCase(FpMinExpr.class, this::transformFpMin) + + .addCase(FpSqrtExpr.class, this::transformFpSqrt) + + .addCase(FpRemExpr.class, this::transformFpRem) + + .addCase(FpIsNanExpr.class, this::transformFpIsNan) + + .addCase(FpIsInfiniteExpr.class, this::transformFpIsInfinite) + + .addCase(FpFromBvExpr.class, this::transformFpFromBv) + + .addCase(FpToBvExpr.class, this::transformFpToBv) + + .addCase(FpToFpExpr.class, this::transformFpToFp) + + // Functions + + .addCase(FuncAppExpr.class, this::transformFuncApp) + + // Arrays + + .addCase(ArrayReadExpr.class, this::transformArrayRead) + + .addCase(ArrayWriteExpr.class, this::transformArrayWrite) + + .addCase(ArrayEqExpr.class, this::transformArrayEq) + + .addCase(ArrayNeqExpr.class, this::transformArrayNeq) + + .addCase(ArrayLitExpr.class, this::transformArrayLit) + + .addCase(ArrayInitExpr.class, this::transformArrayInit) + + .build(); + } + + private static T orElseNull(Supplier supplier) { + try { + return supplier.get(); + } catch (UnsupportedOperationException uoe) { + return null; + } + } + + //// + + /* + * General + */ + + public Formula toTerm(final Expr expr) { + try { + return exprToTerm.get(expr, () -> table.dispatch(expr)); + } catch (final ExecutionException e) { + throw new AssertionError("Unhandled case: " + expr, e); + } + } + + private Formula transformRef(final RefExpr expr) { + final Decl decl = expr.getDecl(); + if (decl instanceof ConstDecl) { + return transformer.toSymbol(decl); + } else if (decl instanceof ParamDecl) { + return (Formula) env.eval(DeclSymbol.of(decl)); + } else { + throw new UnsupportedOperationException( + "Cannot transform reference for declaration: " + decl); + } + } + + /* + * Booleans + */ + + private Formula transformIte(final IteExpr expr) { + final BooleanFormula condTerm = (BooleanFormula) toTerm(expr.getCond()); + final Formula thenTerm = toTerm(expr.getThen()); + final Formula elzeTerm = toTerm(expr.getElse()); + return booleanFormulaManager.ifThenElse(condTerm, thenTerm, elzeTerm); + } + + private Formula transformFalse(final FalseExpr expr) { + return booleanFormulaManager.makeFalse(); + + } + + private Formula transformTrue(final TrueExpr expr) { + return booleanFormulaManager.makeTrue(); + } + + private Formula transformNot(final NotExpr expr) { + final BooleanFormula opTerm = (BooleanFormula) toTerm(expr.getOp()); + return booleanFormulaManager.not(opTerm); + } + + private Formula transformImply(final ImplyExpr expr) { + final BooleanFormula leftOpTerm = (BooleanFormula) toTerm(expr.getLeftOp()); + final BooleanFormula rightOpTerm = (BooleanFormula) toTerm(expr.getRightOp()); + return booleanFormulaManager.implication(leftOpTerm, rightOpTerm); + } + + private Formula transformIff(final IffExpr expr) { + final BooleanFormula leftOpTerm = (BooleanFormula) toTerm(expr.getLeftOp()); + final BooleanFormula rightOpTerm = (BooleanFormula) toTerm(expr.getRightOp()); + return booleanFormulaManager.equivalence(leftOpTerm, rightOpTerm); + } + + private Formula transformXor(final XorExpr expr) { + final BooleanFormula leftOpTerm = (BooleanFormula) toTerm(expr.getLeftOp()); + final BooleanFormula rightOpTerm = (BooleanFormula) toTerm(expr.getRightOp()); + return booleanFormulaManager.xor(leftOpTerm, rightOpTerm); + } + + private Formula transformAnd(final AndExpr expr) { + final List opTerms = expr.getOps().stream() + .map(e -> (BooleanFormula) toTerm(e)) + .toList(); + return booleanFormulaManager.and(opTerms); + } + + private Formula transformOr(final OrExpr expr) { + final List opTerms = expr.getOps().stream() + .map(e -> (BooleanFormula) toTerm(e)) + .toList(); + return booleanFormulaManager.or(opTerms); + } + + private Formula transformExists(final ExistsExpr expr) { + env.push(); + final List paramTerms = transformParamDecls(expr.getParamDecls()); + final BooleanFormula opTerm = (BooleanFormula) toTerm(expr.getOp()); + final BooleanFormula result = quantifiedFormulaManager.exists(paramTerms, opTerm); + env.pop(); + return result; + } + + private Formula transformForall(final ForallExpr expr) { + env.push(); + final List paramTerms = transformParamDecls(expr.getParamDecls()); + final BooleanFormula opTerm = (BooleanFormula) toTerm(expr.getOp()); + final BooleanFormula result = quantifiedFormulaManager.forall(paramTerms, opTerm); + env.pop(); + return result; + } + + private List transformParamDecls(final List> paramDecls) { + final List paramTerms = new ArrayList<>(paramDecls.size()); + for (final ParamDecl paramDecl : paramDecls) { + final Formula paramSymbol = transformParamDecl(paramDecl); + paramTerms.add(paramSymbol); + env.define(DeclSymbol.of(paramDecl), paramSymbol); + } + return paramTerms; + } + + private Formula transformParamDecl(final ParamDecl paramDecl) { + final Type type = paramDecl.getType(); + if (type instanceof FuncType) { + throw new UnsupportedOperationException("Only simple types are supported"); + } else { + final FormulaType sort = transformer.toSort(type); + return context.getFormulaManager().makeVariable(sort, paramDecl.getName()); + } + } + + /* + * Rationals + */ + + private Formula transformRatLit(final RatLitExpr expr) { + var num = rationalFormulaManager.makeNumber(expr.getNum().toString()); + var denom = rationalFormulaManager.makeNumber(expr.getDenom().toString()); + return rationalFormulaManager.divide(num, denom); + } + + private Formula transformRatAdd(final RatAddExpr expr) { + final List opTerms = expr.getOps().stream() + .map(e -> (RationalFormula) toTerm(e)) + .toList(); + return opTerms.stream().reduce(rationalFormulaManager::add).get(); + } + + private Formula transformRatSub(final RatSubExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm( + expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm( + expr.getRightOp()); + return rationalFormulaManager.subtract(leftOpTerm, rightOpTerm); + } + + private Formula transformRatPos(final RatPosExpr expr) { + return toTerm(expr.getOp()); + } + + private Formula transformRatNeg(final RatNegExpr expr) { + final RationalFormula opTerm = (RationalFormula) toTerm(expr.getOp()); + return rationalFormulaManager.negate(opTerm); + } + + private Formula transformRatMul(final RatMulExpr expr) { + final List opTerms = expr.getOps().stream() + .map(e -> (RationalFormula) toTerm(e)) + .toList(); + return opTerms.stream().reduce(rationalFormulaManager::multiply).get(); + } + + private Formula transformRatDiv(final RatDivExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm( + expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm( + expr.getRightOp()); + return rationalFormulaManager.divide(leftOpTerm, rightOpTerm); + } + + private Formula transformRatEq(final RatEqExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm(expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm(expr.getRightOp()); + return rationalFormulaManager.equal(leftOpTerm, rightOpTerm); + } + + private Formula transformRatNeq(final RatNeqExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm(expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm(expr.getRightOp()); + return booleanFormulaManager.not(rationalFormulaManager.equal(leftOpTerm, rightOpTerm)); + } + + private Formula transformRatGeq(final RatGeqExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm( + expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm( + expr.getRightOp()); + return rationalFormulaManager.greaterOrEquals(leftOpTerm, rightOpTerm); + } + + private Formula transformRatGt(final RatGtExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm( + expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm( + expr.getRightOp()); + return rationalFormulaManager.greaterThan(leftOpTerm, rightOpTerm); + } + + private Formula transformRatLeq(final RatLeqExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm( + expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm( + expr.getRightOp()); + return rationalFormulaManager.lessOrEquals(leftOpTerm, rightOpTerm); + } + + private Formula transformRatLt(final RatLtExpr expr) { + final RationalFormula leftOpTerm = (RationalFormula) toTerm( + expr.getLeftOp()); + final RationalFormula rightOpTerm = (RationalFormula) toTerm( + expr.getRightOp()); + return rationalFormulaManager.lessThan(leftOpTerm, rightOpTerm); + } + + /* + * Integers + */ + + private Formula transformRatToInt(final RatToIntExpr expr) { + return rationalFormulaManager.floor((NumeralFormula) toTerm(expr.getOp())); + } + + private Formula transformIntLit(final IntLitExpr expr) { + return integerFormulaManager.makeNumber(expr.getValue().toString()); + } + + private Formula transformIntAdd(final IntAddExpr expr) { + final List opTerms = expr.getOps().stream() + .map(e -> (IntegerFormula) toTerm(e)) + .toList(); + return opTerms.stream().reduce(integerFormulaManager::add).get(); + } + + private Formula transformIntSub(final IntSubExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return integerFormulaManager.subtract(leftOpTerm, rightOpTerm); + } + + private Formula transformIntPos(final IntPosExpr expr) { + return toTerm(expr.getOp()); + } + + private Formula transformIntNeg(final IntNegExpr expr) { + final IntegerFormula opTerm = (IntegerFormula) toTerm(expr.getOp()); + return integerFormulaManager.negate(opTerm); + } + + private Formula transformIntMul(final IntMulExpr expr) { + final List opTerms = expr.getOps().stream() + .map(e -> (IntegerFormula) toTerm(e)) + .toList(); + return opTerms.stream().reduce(integerFormulaManager::multiply).get(); + } + + private Formula transformIntDiv(final IntDivExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return integerFormulaManager.divide(leftOpTerm, rightOpTerm); + } + + private Formula transformIntMod(final IntModExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return integerFormulaManager.modulo(leftOpTerm, rightOpTerm); + } + + private Formula transformIntRem(final IntRemExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return booleanFormulaManager.ifThenElse( + integerFormulaManager.greaterOrEquals(rightOpTerm, integerFormulaManager.makeNumber(0)), + integerFormulaManager.modulo(leftOpTerm, rightOpTerm), + integerFormulaManager.negate(integerFormulaManager.modulo(leftOpTerm, rightOpTerm)) + ); + } + + private Formula transformIntEq(final IntEqExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm(expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm(expr.getRightOp()); + return integerFormulaManager.equal(leftOpTerm, rightOpTerm); + } + + private Formula transformIntNeq(final IntNeqExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm(expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm(expr.getRightOp()); + return booleanFormulaManager.not(integerFormulaManager.equal(leftOpTerm, rightOpTerm)); + } + + private Formula transformIntGeq(final IntGeqExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return integerFormulaManager.greaterOrEquals(leftOpTerm, rightOpTerm); + } + + private Formula transformIntGt(final IntGtExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return integerFormulaManager.greaterThan(leftOpTerm, rightOpTerm); + } + + private Formula transformIntLeq(final IntLeqExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return integerFormulaManager.lessOrEquals(leftOpTerm, rightOpTerm); + } + + private Formula transformIntLt(final IntLtExpr expr) { + final IntegerFormula leftOpTerm = (IntegerFormula) toTerm( + expr.getLeftOp()); + final IntegerFormula rightOpTerm = (IntegerFormula) toTerm( + expr.getRightOp()); + return integerFormulaManager.lessThan(leftOpTerm, rightOpTerm); + } + + private Formula transformIntToRat(final IntToRatExpr expr) { + return rationalFormulaManager.sum(List.of((IntegerFormula) toTerm(expr.getOp()))); + } + + /* + * Bitvectors + */ + + private Formula transformBvLit(final BvLitExpr expr) { + return bitvectorFormulaManager.makeBitvector( + expr.getType().getSize(), + BvUtils.neutralBvLitExprToBigInteger(expr)); + } + + private Formula transformBvEq(final BvEqExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + return bitvectorFormulaManager.equal(leftOpTerm, rightOpTerm); + } + + private Formula transformBvNeq(final BvNeqExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + return booleanFormulaManager.not(bitvectorFormulaManager.equal(leftOpTerm, rightOpTerm)); + } + + private Formula transformBvConcat(final BvConcatExpr expr) { + final BitvectorFormula[] opTerms = expr.getOps().stream() + .map(e -> (BitvectorFormula) toTerm(e)) + .toArray(BitvectorFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], bitvectorFormulaManager::concat); + } + + private Formula transformBvExtract(final BvExtractExpr expr) { + final BitvectorFormula bitvecTerm = (BitvectorFormula) toTerm(expr.getBitvec()); + final int from = expr.getFrom().getValue().intValue(); + final int until = expr.getUntil().getValue().intValue(); + + return bitvectorFormulaManager.extract(bitvecTerm, until - 1, from); + } + + private Formula transformBvZExt(final BvZExtExpr expr) { + final BitvectorFormula bitvecTerm = (BitvectorFormula) toTerm(expr.getOp()); + final int extendWith = expr.getExtendType().getSize() - expr.getOp().getType().getSize(); + + return bitvectorFormulaManager.extend(bitvecTerm, extendWith, false); + } + + private Formula transformBvSExt(final BvSExtExpr expr) { + final BitvectorFormula bitvecTerm = (BitvectorFormula) toTerm(expr.getOp()); + final int extendWith = expr.getExtendType().getSize() - expr.getOp().getType().getSize(); + + return bitvectorFormulaManager.extend(bitvecTerm, extendWith, true); + } + + private Formula transformBvAdd(final BvAddExpr expr) { + final BitvectorFormula[] opTerms = expr.getOps().stream() + .map(e -> (BitvectorFormula) toTerm(e)) + .toArray(BitvectorFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], bitvectorFormulaManager::add); + } + + private Formula transformBvSub(final BvSubExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + return bitvectorFormulaManager.subtract(leftOpTerm, rightOpTerm); + } + + private Formula transformBvPos(final BvPosExpr expr) { + return toTerm(expr.getOp()); + } + + private Formula transformBvSignChange(final BvSignChangeExpr expr) { + return (BitvectorFormula) toTerm(expr.getOp()); + } + + private Formula transformBvNeg(final BvNegExpr expr) { + final BitvectorFormula opTerm = (BitvectorFormula) toTerm(expr.getOp()); + return bitvectorFormulaManager.negate(opTerm); + } + + private Formula transformBvMul(final BvMulExpr expr) { + final BitvectorFormula[] opTerms = expr.getOps().stream() + .map(e -> (BitvectorFormula) toTerm(e)) + .toArray(BitvectorFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], bitvectorFormulaManager::multiply); + } + + private Formula transformBvUDiv(final BvUDivExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.divide(leftOpTerm, rightOpTerm, false); + } + + private Formula transformBvSDiv(final BvSDivExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.divide(leftOpTerm, rightOpTerm, true); + } + + private Formula transformBvSMod(final BvSModExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.smod(leftOpTerm, rightOpTerm); + } + + private Formula transformBvURem(final BvURemExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.rem(leftOpTerm, rightOpTerm, false); + } + + private Formula transformBvSRem(final BvSRemExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.rem(leftOpTerm, rightOpTerm, true); + } + + private Formula transformBvAnd(final BvAndExpr expr) { + final BitvectorFormula[] opTerms = expr.getOps().stream() + .map(e -> (BitvectorFormula) toTerm(e)) + .toArray(BitvectorFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], bitvectorFormulaManager::and); + } + + private Formula transformBvOr(final BvOrExpr expr) { + final BitvectorFormula[] opTerms = expr.getOps().stream() + .map(e -> (BitvectorFormula) toTerm(e)) + .toArray(BitvectorFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], bitvectorFormulaManager::or); + } + + private Formula transformBvXor(final BvXorExpr expr) { + final BitvectorFormula[] opTerms = expr.getOps().stream() + .map(e -> (BitvectorFormula) toTerm(e)) + .toArray(BitvectorFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], bitvectorFormulaManager::xor); + } + + private Formula transformBvNot(final BvNotExpr expr) { + final BitvectorFormula opTerm = (BitvectorFormula) toTerm(expr.getOp()); + + return bitvectorFormulaManager.not(opTerm); + } + + private Formula transformBvShiftLeft(final BvShiftLeftExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.shiftLeft(leftOpTerm, rightOpTerm); + } + + private Formula transformBvArithShiftRight(final BvArithShiftRightExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.shiftRight(leftOpTerm, rightOpTerm, true); + } + + private Formula transformBvLogicShiftRight(final BvLogicShiftRightExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.shiftRight(leftOpTerm, rightOpTerm, false); + } + + private Formula transformBvRotateLeft(final BvRotateLeftExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.rotateLeft(leftOpTerm, rightOpTerm); + } + + private Formula transformBvRotateRight(final BvRotateRightExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.rotateRight(leftOpTerm, rightOpTerm); + } + + private Formula transformBvUGeq(final BvUGeqExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.greaterOrEquals(leftOpTerm, rightOpTerm, false); + } + + private Formula transformBvUGt(final BvUGtExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.greaterThan(leftOpTerm, rightOpTerm, false); + } + + private Formula transformBvULeq(final BvULeqExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.lessOrEquals(leftOpTerm, rightOpTerm, false); + } + + private Formula transformBvULt(final BvULtExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.lessThan(leftOpTerm, rightOpTerm, false); + } + + private Formula transformBvSGeq(final BvSGeqExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.greaterOrEquals(leftOpTerm, rightOpTerm, true); + } + + private Formula transformBvSGt(final BvSGtExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.greaterThan(leftOpTerm, rightOpTerm, true); + } + + private Formula transformBvSLeq(final BvSLeqExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.lessOrEquals(leftOpTerm, rightOpTerm, true); + } + + private Formula transformBvSLt(final BvSLtExpr expr) { + final BitvectorFormula leftOpTerm = (BitvectorFormula) toTerm(expr.getLeftOp()); + final BitvectorFormula rightOpTerm = (BitvectorFormula) toTerm(expr.getRightOp()); + + return bitvectorFormulaManager.lessThan(leftOpTerm, rightOpTerm, true); + } + + /* + * Floating points + */ + + + private Formula transformFpLit(final FpLitExpr expr) { + return floatingPointFormulaManager.makeNumber( + BvUtils.neutralBvLitExprToBigInteger(expr.getExponent()), + BvUtils.neutralBvLitExprToBigInteger(expr.getSignificand()), + expr.getHidden(), + FloatingPointType.getFloatingPointType(expr.getType().getExponent(), expr.getType().getSignificand() - 1) + ); + } + + private Formula transformFpAdd(final FpAddExpr expr) { + final FloatingPointFormula[] opTerms = expr.getOps().stream() + .map(e -> (FloatingPointFormula) toTerm(e)) + .toArray(FloatingPointFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], + (op1, op2) -> floatingPointFormulaManager.add(op1, op2, + transformFpRoundingMode(expr.getRoundingMode()) + )); + } + + private Formula transformFpSub(final FpSubExpr expr) { + final FloatingPointFormula leftOpTerm = (FloatingPointFormula) toTerm(expr.getLeftOp()); + final FloatingPointFormula rightOpTerm = (FloatingPointFormula) toTerm(expr.getRightOp()); + return floatingPointFormulaManager.subtract(leftOpTerm, rightOpTerm, transformFpRoundingMode(expr.getRoundingMode())); + } + + private Formula transformFpPos(final FpPosExpr expr) { + return toTerm(expr.getOp()); + } + + private Formula transformFpNeg(final FpNegExpr expr) { + final FloatingPointFormula opTerm = (FloatingPointFormula) toTerm(expr.getOp()); + return floatingPointFormulaManager.negate(opTerm); + } + + private Formula transformFpAbs(final FpAbsExpr expr) { + final FloatingPointFormula opTerm = (FloatingPointFormula) toTerm(expr.getOp()); + return floatingPointFormulaManager.abs(opTerm); + } + + private Formula transformFpIsNan(final FpIsNanExpr expr) { + final FloatingPointFormula opTerm = (FloatingPointFormula) toTerm(expr.getOp()); + return floatingPointFormulaManager.isNaN(opTerm); + } + + private Formula transformFpIsInfinite(final FpIsInfiniteExpr expr) { + final FloatingPointFormula opTerm = (FloatingPointFormula) toTerm(expr.getOp()); + return floatingPointFormulaManager.isInfinity(opTerm); + } + + private Formula transformFpSqrt(final FpSqrtExpr expr) { + final FloatingPointFormula opTerm = (FloatingPointFormula) toTerm(expr.getOp()); + return floatingPointFormulaManager.sqrt(opTerm, transformFpRoundingMode(expr.getRoundingMode())); + } + + private Formula transformFpRoundToIntegral(final FpRoundToIntegralExpr expr) { + final FloatingPointFormula opTerm = (FloatingPointFormula) toTerm(expr.getOp()); + return floatingPointFormulaManager.round(opTerm, transformFpRoundingMode(expr.getRoundingMode())); + } + + private Formula transformFpMul(final FpMulExpr expr) { + final FloatingPointFormula[] opTerms = expr.getOps().stream() + .map(e -> (FloatingPointFormula) toTerm(e)) + .toArray(FloatingPointFormula[]::new); + + return Stream.of(opTerms).skip(1).reduce(opTerms[0], + (op1, op2) -> floatingPointFormulaManager.multiply(op1, op2, transformFpRoundingMode(expr.getRoundingMode()))); + } + + private Formula transformFpDiv(final FpDivExpr expr) { + final FloatingPointFormula leftOpTerm = (FloatingPointFormula) toTerm(expr.getLeftOp()); + final FloatingPointFormula rightOpTerm = (FloatingPointFormula) toTerm(expr.getRightOp()); + + return floatingPointFormulaManager.divide(leftOpTerm, rightOpTerm, transformFpRoundingMode(expr.getRoundingMode())); + } + + private Formula transformFpRem(final FpRemExpr expr) { + final FloatingPointFormula leftOpTerm = (FloatingPointFormula) toTerm(expr.getLeftOp()); + final FloatingPointFormula rightOpTerm = (FloatingPointFormula) toTerm(expr.getRightOp()); + return floatingPointFormulaManager.remainder(leftOpTerm, rightOpTerm); + } + + private Formula transformFpEq(final FpEqExpr expr) { + final Formula leftOpTerm = toTerm(expr.getLeftOp()); + final Formula rightOpTerm = toTerm(expr.getRightOp()); + return floatingPointFormulaManager.equalWithFPSemantics((FloatingPointFormula) leftOpTerm, (FloatingPointFormula) rightOpTerm); + } + + private Formula transformFpAssign(final FpAssignExpr expr) { + final Formula leftOpTerm = toTerm(expr.getLeftOp()); + final Formula rightOpTerm = toTerm(expr.getRightOp()); + return floatingPointFormulaManager.assignment((FloatingPointFormula) leftOpTerm, (FloatingPointFormula) rightOpTerm); + } + + private Formula transformFpNeq(final FpNeqExpr expr) { + final Formula leftOpTerm = toTerm(expr.getLeftOp()); + final Formula rightOpTerm = toTerm(expr.getRightOp()); + return booleanFormulaManager.not(floatingPointFormulaManager.equalWithFPSemantics((FloatingPointFormula) leftOpTerm, (FloatingPointFormula) rightOpTerm)); + } + + private Formula transformFpGeq(final FpGeqExpr expr) { + final Formula leftOpTerm = toTerm(expr.getLeftOp()); + final Formula rightOpTerm = toTerm(expr.getRightOp()); + return floatingPointFormulaManager.greaterOrEquals((FloatingPointFormula) leftOpTerm, (FloatingPointFormula) rightOpTerm); + } + + private Formula transformFpLeq(final FpLeqExpr expr) { + final Formula leftOpTerm = toTerm(expr.getLeftOp()); + final Formula rightOpTerm = toTerm(expr.getRightOp()); + return floatingPointFormulaManager.lessOrEquals((FloatingPointFormula) leftOpTerm, (FloatingPointFormula) rightOpTerm); + } + + private Formula transformFpGt(final FpGtExpr expr) { + final Formula leftOpTerm = toTerm(expr.getLeftOp()); + final Formula rightOpTerm = toTerm(expr.getRightOp()); + return floatingPointFormulaManager.greaterThan((FloatingPointFormula) leftOpTerm, (FloatingPointFormula) rightOpTerm); + } + + private Formula transformFpLt(final FpLtExpr expr) { + final Formula leftOpTerm = toTerm(expr.getLeftOp()); + final Formula rightOpTerm = toTerm(expr.getRightOp()); + return floatingPointFormulaManager.lessThan((FloatingPointFormula) leftOpTerm, (FloatingPointFormula) rightOpTerm); + } + + private FloatingPointRoundingMode transformFpRoundingMode(final FpRoundingMode roundingMode) { + return switch (roundingMode) { + case RNE -> FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + case RNA -> FloatingPointRoundingMode.NEAREST_TIES_AWAY; + case RTP -> FloatingPointRoundingMode.TOWARD_POSITIVE; + case RTN -> FloatingPointRoundingMode.TOWARD_NEGATIVE; + case RTZ -> FloatingPointRoundingMode.TOWARD_ZERO; + }; + } + + private Formula transformFpMax(final FpMaxExpr expr) { + final FloatingPointFormula leftOpTerm = (FloatingPointFormula) toTerm(expr.getLeftOp()); + final FloatingPointFormula rightOpTerm = (FloatingPointFormula) toTerm(expr.getRightOp()); + return floatingPointFormulaManager.max(leftOpTerm, rightOpTerm); + } + + private Formula transformFpMin(final FpMinExpr expr) { + final FloatingPointFormula leftOpTerm = (FloatingPointFormula) toTerm(expr.getLeftOp()); + final FloatingPointFormula rightOpTerm = (FloatingPointFormula) toTerm(expr.getRightOp()); + return floatingPointFormulaManager.min(leftOpTerm, rightOpTerm); + } + + private Formula transformFpFromBv(final FpFromBvExpr expr) { + final BitvectorFormula val = (BitvectorFormula) toTerm(expr.getOp()); + final FloatingPointType fpSort = FloatingPointType.getFloatingPointType( + expr.getFpType().getExponent(), + expr.getFpType().getSignificand() - 1); + return floatingPointFormulaManager.castFrom(val, expr.isSigned(), fpSort); + } + + private Formula transformFpToBv(final FpToBvExpr expr) { + final FloatingPointFormula op = (FloatingPointFormula) toTerm(expr.getOp()); + final FloatingPointRoundingMode roundingMode = transformRoundingMode(expr.getRoundingMode()); + + return floatingPointFormulaManager.castTo(op, expr.getSgn(), FormulaType.getBitvectorTypeWithSize(expr.getSize()), roundingMode); + } + + private static FloatingPointRoundingMode transformRoundingMode(final FpRoundingMode fpRoundingMode) { + return switch (fpRoundingMode) { + case RNE -> FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN; + case RNA -> FloatingPointRoundingMode.NEAREST_TIES_AWAY; + case RTP -> FloatingPointRoundingMode.TOWARD_POSITIVE; + case RTN -> FloatingPointRoundingMode.TOWARD_NEGATIVE; + case RTZ -> FloatingPointRoundingMode.TOWARD_ZERO; + }; + } + /* + * Arrays + */ + + private Formula transformFpToFp(final FpToFpExpr expr) { + final FloatingPointFormula op = (FloatingPointFormula) toTerm(expr.getOp()); + + return floatingPointFormulaManager.castTo( + op, + true, // ignored + FloatingPointType.getFloatingPointType(expr.getExpBits(), expr.getSignBits() - 1), + transformFpRoundingMode(expr.getRoundingMode())); + } + + private Formula transformArrayRead(final ArrayReadExpr expr) { + final ArrayFormula arrayTerm = (ArrayFormula) toTerm( + expr.getArray()); + final Formula indexTerm = toTerm(expr.getIndex()); + return arrayFormulaManager.select(arrayTerm, indexTerm); + } + + private Formula transformArrayWrite(final ArrayWriteExpr expr) { + final ArrayFormula arrayTerm = (ArrayFormula) toTerm( + expr.getArray()); + final Formula indexTerm = toTerm(expr.getIndex()); + final Formula elemTerm = toTerm(expr.getElem()); + return arrayFormulaManager.store(arrayTerm, indexTerm, elemTerm); + } + + private Formula transformArrayEq(final ArrayEqExpr expr) { + final ArrayFormula leftOpTerm = (ArrayFormula) toTerm(expr.getLeftOp()); + final ArrayFormula rightOpTerm = (ArrayFormula) toTerm(expr.getRightOp()); + return arrayFormulaManager.equivalence(leftOpTerm, rightOpTerm); + } + + private Formula transformArrayNeq(final ArrayNeqExpr expr) { + return booleanFormulaManager.not( + (BooleanFormula) transformArrayEq(ArrayEqExpr.create(expr.getLeftOp(), expr.getRightOp())) + ); + } + + private Formula transformArrayLit(final ArrayLitExpr expr) { + final TE elseElem = (TE) toTerm(expr.getElseElem()); + final FormulaType elemType = (FormulaType) transformer.toSort(expr.getType().getElemType()); + final FormulaType indexType = (FormulaType) transformer.toSort(expr.getType().getIndexType()); + var arr = arrayFormulaManager.makeArray( + elseElem, + indexType, + elemType); + for (Tuple2, ? extends LitExpr> element : expr.getElements()) { + final TI index = (TI) toTerm(element.get1()); + final TE elem = (TE) toTerm(element.get2()); + arr = arrayFormulaManager.store(arr, index, elem); + } + return arr; + } + + private Formula transformArrayInit(final ArrayInitExpr expr) { + final TE elseElem = (TE) toTerm(expr.getElseElem()); + final FormulaType elemType = (FormulaType) transformer.toSort(expr.getType().getElemType()); + final FormulaType indexType = (FormulaType) transformer.toSort(expr.getType().getIndexType()); + var arr = arrayFormulaManager.makeArray( + elseElem, + indexType, + elemType); + for (Tuple2, ? extends Expr> element : expr.getElements()) { + final TI index = (TI) toTerm(element.get1()); + final TE elem = (TE) toTerm(element.get2()); + arr = arrayFormulaManager.store(arr, index, elem); + } + return arr; + } + + + /* + * Functions + */ + + private Formula transformFuncApp(final FuncAppExpr expr) { + final Tuple2, List>> funcAndArgs = extractFuncAndArgs(expr); + final Expr func = funcAndArgs.get1(); + if (func instanceof RefExpr) { + final RefExpr ref = (RefExpr) func; + final ConstDecl decl = (ConstDecl) ref.getDecl(); + final String name = decl.getName(); + + final List> args = funcAndArgs.get2(); + final List argTerms = args.stream() + .map(this::toTerm) + .toList(); + + + final FunctionDeclaration funcDecl; + if (symbolTable.definesConstAsFunction(decl)) { + funcDecl = symbolTable.getSymbolAsFunction(decl); + } else { + funcDecl = context.getFormulaManager().getUFManager().declareUF( + name, + transformer.toSort(expr.getType()), + argTerms.stream().map(context.getFormulaManager()::getFormulaType).collect(Collectors.toList())); + + symbolTable.put(decl, funcDecl); + } + + return context.getFormulaManager().getUFManager().callUF(funcDecl, argTerms); + } else { + throw new UnsupportedOperationException( + "Higher order functions are not supported: " + func); + } + } + + private static Tuple2, List>> extractFuncAndArgs(final FuncAppExpr expr) { + final Expr func = expr.getFunc(); + final Expr arg = expr.getParam(); + if (func instanceof FuncAppExpr) { + final FuncAppExpr funcApp = (FuncAppExpr) func; + final Tuple2, List>> funcAndArgs = extractFuncAndArgs(funcApp); + final Expr resFunc = funcAndArgs.get1(); + final List> args = funcAndArgs.get2(); + final List> resArgs = ImmutableList.>builder().addAll(args).add(arg) + .build(); + return Tuple2.of(resFunc, resArgs); + } else { + return Tuple2.of(func, ImmutableList.of(arg)); + } + } + + public void reset() { + exprToTerm.invalidateAll(); + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTInterpolant.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTInterpolant.java new file mode 100644 index 0000000000..8c8f3b6682 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTInterpolant.java @@ -0,0 +1,43 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.solver.Interpolant; +import hu.bme.mit.theta.solver.ItpMarker; + +import java.util.Map; + +import static com.google.common.base.Preconditions.checkNotNull; + +final class JavaSMTInterpolant implements Interpolant { + + private final Map> itpMap; + + JavaSMTInterpolant(final Map> itpMap) { + this.itpMap = itpMap; + } + + @Override + public Expr eval(final ItpMarker marker) { + checkNotNull(marker); + final Expr itpExpr = itpMap.get(marker); + checkNotNull(itpExpr); + return itpExpr; + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpMarker.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpMarker.java new file mode 100644 index 0000000000..ca5e6abe20 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpMarker.java @@ -0,0 +1,50 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.solver.ItpMarker; +import hu.bme.mit.theta.solver.Stack; +import hu.bme.mit.theta.solver.impl.StackImpl; + +import java.util.Collection; + +import static com.google.common.base.Preconditions.checkNotNull; + +final class JavaSMTItpMarker implements ItpMarker { + + private final Stack terms; + + public JavaSMTItpMarker() { + terms = new StackImpl<>(); + } + + public void add(final T term) { + terms.add(checkNotNull(term)); + } + + public void push() { + terms.push(); + } + + public void pop(final int n) { + terms.pop(n); + } + + public Collection getTerms() { + return terms.toCollection(); + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpPattern.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpPattern.java new file mode 100644 index 0000000000..29ab0c5bbd --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpPattern.java @@ -0,0 +1,110 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.collect.Lists; +import hu.bme.mit.theta.solver.ItpMarker; +import hu.bme.mit.theta.solver.ItpMarkerTree; +import hu.bme.mit.theta.solver.ItpPattern; + +import java.util.ArrayList; +import java.util.List; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkState; + +public class JavaSMTItpPattern implements ItpPattern.Binary, + ItpPattern.Sequence, ItpPattern.Tree { + + final ItpMarkerTree markerTree; + + JavaSMTItpPattern(final ItpMarkerTree markerTree) { + this.markerTree = markerTree; + } + + @SuppressWarnings("unchecked") + static JavaSMTItpPattern of(final ItpMarkerTree markerTree) { + final var list = new ArrayList>(); + list.add(markerTree); + while (!list.isEmpty()) { + final var node = list.get(0); + list.remove(0); + + checkArgument(node.getMarker() instanceof JavaSMTItpMarker); + + list.addAll(node.getChildren()); + } + + return new JavaSMTItpPattern((ItpMarkerTree) markerTree); + } + + @Override + public JavaSMTItpMarker getA() { + checkState(isBinary()); + return markerTree.getChild(0).getMarker(); + } + + @Override + public JavaSMTItpMarker getB() { + checkState(isBinary()); + return markerTree.getMarker(); + } + + @Override + public List getSequence() { + checkState(isSequence()); + final var markerList = new ArrayList(); + + var current = markerTree; + while (current.getChildrenNumber() > 0) { + markerList.add(current.getMarker()); + current = current.getChild(0); + } + markerList.add(current.getMarker()); + + return Lists.reverse(markerList); + } + + @Override + public ItpMarkerTree getRoot() { + return markerTree; + } + + @Override + public E visit(ItpPatternVisitor visitor) { + return visitor.visitTreePattern(this); + } + + private boolean isBinary() { + return + markerTree != null && + markerTree.getChildrenNumber() == 1 && + markerTree.getChild(0) != null && + markerTree.getChild(0).getChildrenNumber() == 0; + } + + private boolean isSequence() { + var current = markerTree; + while (current.getChildrenNumber() > 0) { + if (current.getChildrenNumber() > 1) { + return false; + } else { + current = current.getChild(0); + } + } + return true; + } +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java new file mode 100644 index 0000000000..516021bc5e --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolver.java @@ -0,0 +1,211 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.common.container.Containers; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.solver.Interpolant; +import hu.bme.mit.theta.solver.ItpMarker; +import hu.bme.mit.theta.solver.ItpMarkerTree; +import hu.bme.mit.theta.solver.ItpPattern; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import hu.bme.mit.theta.solver.Stack; +import hu.bme.mit.theta.solver.impl.StackImpl; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; + +import java.util.Collection; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; + +final class JavaSMTItpSolver implements ItpSolver, Solver { + + private final JavaSMTTransformationManager transformationManager; + + private final JavaSMTSolver solver; + private final InterpolatingProverEnvironment interpolatingProverEnvironment; + + private final Stack markers; + + private final JavaSMTTermTransformer termTransformer; + private final SolverContext context; + + public JavaSMTItpSolver(final JavaSMTSymbolTable symbolTable, + final JavaSMTTransformationManager transformationManager, + final JavaSMTTermTransformer termTransformer, + final SolverContext context, + final InterpolatingProverEnvironment interpolatingProverEnvironment) { + this.transformationManager = transformationManager; + this.termTransformer = termTransformer; + this.context = context; + + this.solver = new JavaSMTSolver(symbolTable, transformationManager, termTransformer, context, interpolatingProverEnvironment); + this.interpolatingProverEnvironment = interpolatingProverEnvironment; + + markers = new StackImpl<>(); + } + + @Override + public ItpPattern createTreePattern(final ItpMarkerTree root) { + checkNotNull(root); + return JavaSMTItpPattern.of(root); + } + + @Override + public JavaSMTItpMarker createMarker() { + final JavaSMTItpMarker marker = new JavaSMTItpMarker(); + markers.add(marker); + return marker; + } + + @Override + public void add(final ItpMarker marker, final Expr assertion) { + checkNotNull(marker); + checkNotNull(assertion); + checkArgument(markers.toCollection().contains(marker), "Marker not found in solver"); + final JavaSMTItpMarker z3Marker = (JavaSMTItpMarker) marker; + BooleanFormula term = (BooleanFormula) transformationManager.toTerm(assertion); + Object c = solver.add(assertion, term); + z3Marker.add(c); + } + + @Override + public Interpolant getInterpolant(final ItpPattern pattern) { + checkState(solver.getStatus() == SolverStatus.UNSAT, + "Cannot get interpolant if status is not UNSAT."); + checkArgument(pattern instanceof JavaSMTItpPattern); + + checkArgument(pattern instanceof JavaSMTItpPattern); + final JavaSMTItpPattern javaSMTItpPattern = (JavaSMTItpPattern) pattern; + + final List markerList = new LinkedList<>(); + final List> termList = new LinkedList<>(); + final List indexList = new LinkedList<>(); + + getInterpolantParams(javaSMTItpPattern.getRoot(), markerList, termList, indexList); + + try { + final List interpolants; + if (indexList.stream().allMatch(i -> i == 0)) { + interpolants = interpolatingProverEnvironment.getSeqInterpolants(termList); + } else { + interpolants = interpolatingProverEnvironment.getTreeInterpolants(termList, indexList.stream().mapToInt(i -> i).toArray()); + } + + Map> itpMap = Containers.createMap(); + for (int i = 0; i < interpolants.size(); i++) { + BooleanFormula term = interpolants.get(i); + Expr expr = (Expr) termTransformer.toExpr(term); + itpMap.put(markerList.get(i), expr); + } + itpMap.put(markerList.get(interpolants.size()), False()); + return new JavaSMTInterpolant(itpMap); + } catch (SolverException | InterruptedException e) { + throw new JavaSMTSolverException(e); + } + } + + private int getInterpolantParams(final ItpMarkerTree root, List markerList, final List> terms, final List indices) { + int leftmostIndex = -1; + for (ItpMarkerTree child : root.getChildren()) { + final int index = getInterpolantParams(child, markerList, terms, indices); + if (leftmostIndex == -1) { + leftmostIndex = index; + } + } + if (leftmostIndex == -1) { + leftmostIndex = indices.size(); + } + markerList.add(root.getMarker()); + terms.add(root.getMarker().getTerms()); + indices.add(leftmostIndex); + return leftmostIndex; + } + + + @Override + public Collection getMarkers() { + return markers.toCollection(); + } + + // delegate + + @Override + public void add(final Expr assertion) { + checkNotNull(assertion); + solver.add(assertion); + } + + @Override + public SolverStatus check() { + return solver.check(); + } + + @Override + public void push() { + markers.push(); + for (final JavaSMTItpMarker marker : markers) { + marker.push(); + } + solver.push(); + } + + @Override + public void pop(final int n) { + markers.pop(n); + for (final JavaSMTItpMarker marker : markers) { + marker.pop(n); + } + solver.pop(n); + } + + @Override + public void reset() { + solver.reset(); + } + + @Override + public SolverStatus getStatus() { + return solver.getStatus(); + } + + @Override + public Valuation getModel() { + return solver.getModel(); + } + + @Override + public Collection> getAssertions() { + return solver.getAssertions(); + } + + @Override + public void close() { + solver.close(); + } +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java new file mode 100644 index 0000000000..cf4a63fab7 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolver.java @@ -0,0 +1,335 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.common.container.Containers; +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.arraytype.ArrayType; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.functype.FuncType; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import hu.bme.mit.theta.solver.Stack; +import hu.bme.mit.theta.solver.UCSolver; +import hu.bme.mit.theta.solver.impl.StackImpl; +import org.sosy_lab.java_smt.api.BasicProverEnvironment; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.Model.ValueAssignment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverException; + +import java.util.Collection; +import java.util.Collections; +import java.util.LinkedList; +import java.util.List; +import java.util.Map; +import java.util.Optional; + +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; + +final class JavaSMTSolver implements UCSolver, Solver { + + private final JavaSMTSymbolTable symbolTable; + private final JavaSMTTransformationManager transformationManager; + private final JavaSMTTermTransformer termTransformer; + + private final SolverContext context; + private final BasicProverEnvironment solver; + + private final Stack> assertions; + + private Valuation model; + private Collection> unsatCore; + + + private final Map> assumptions; + private SolverStatus status; + + public JavaSMTSolver(final JavaSMTSymbolTable symbolTable, + final JavaSMTTransformationManager transformationManager, + final JavaSMTTermTransformer termTransformer, + final SolverContext context, + final BasicProverEnvironment solver) { + this.symbolTable = symbolTable; + this.transformationManager = transformationManager; + this.termTransformer = termTransformer; + this.context = context; + this.solver = solver; + + assertions = new StackImpl<>(); + assumptions = Containers.createMap(); + } + + //// + + @Override + public void add(final Expr assertion) { + checkNotNull(assertion); + final BooleanFormula term = (BooleanFormula) transformationManager.toTerm( + assertion); + add(assertion, term); + } + + Object add(final Expr assertion, final BooleanFormula term) { + assertions.add(assertion); + Object ret; + try { + ret = solver.addConstraint(term); + } catch (InterruptedException e) { + throw new JavaSMTSolverException(e); + } + clearState(); + return ret; + } + + + @Override + public void track(final Expr assertion) { + add(assertion); + } + + @Override + public Collection> getUnsatCore() { + checkState(status == SolverStatus.UNSAT, "Cannot get unsat core if status is not UNSAT"); + + if (unsatCore == null) { + unsatCore = extractUnsatCore(); + } + + assert unsatCore != null; + return Collections.unmodifiableCollection(unsatCore); + } + + + private Collection> extractUnsatCore() { + assert status == SolverStatus.UNSAT; + assert unsatCore == null; + + final Collection> unsatCore = new LinkedList<>(); + + final List jsmtUnsatCore = solver.getUnsatCore(); + + for (final Formula term : jsmtUnsatCore) { + final Expr assumption = (Expr) termTransformer.toExpr(term); + + assert assumption != null; + unsatCore.add(assumption); + } + + return unsatCore; + } + + + @Override + public SolverStatus check() { + try { + final boolean unsat = solver.isUnsat(); + status = unsat ? SolverStatus.UNSAT : SolverStatus.SAT; + return status; + } catch (SolverException | InterruptedException e) { + throw new JavaSMTSolverException(e); + } + } + + @Override + public void push() { + assertions.push(); + try { + solver.push(); + } catch (InterruptedException e) { + throw new JavaSMTSolverException(e); + } + } + + @Override + public void pop(final int n) { + assertions.pop(n); + for (int i = 0; i < n; i++) { + solver.pop(); + } + clearState(); + } + + @Override + public void reset() { + throw new JavaSMTSolverException("Cannot reset JavaSMT right now."); + } + + @Override + public SolverStatus getStatus() { + checkState(status != null, "Solver status is unknown."); + return status; + } + + @Override + public Valuation getModel() { + checkState(status == SolverStatus.SAT, "Cannot get model if status is not SAT."); + + if (model == null) { + model = extractModel(); + } + + return model; + } + + private Valuation extractModel() { + assert status == SolverStatus.SAT; + assert model == null; + + final Model model; + try { + model = solver.getModel(); + return new JavaSMTModel(model); + } catch (SolverException e) { + throw new JavaSMTSolverException(e); + } + } + + @Override + public Collection> getAssertions() { + return assertions.toCollection(); + } + + private void clearState() { + status = null; + model = null; + unsatCore = null; + } + + @Override + public void close() { + context.close(); + } + + //// + + private final class JavaSMTModel extends Valuation { + + private final Model model; + private final Map, LitExpr> constToExpr; + private volatile Collection> constDecls = null; + + public JavaSMTModel(final Model model) { + this.model = model; + constToExpr = Containers.createMap(); + } + + @Override + public Collection> getDecls() { + Collection> result = constDecls; + if (result == null) { + result = constDeclsOf(model); + constDecls = result; + } + return result; + } + + @Override + public Optional> eval(final Decl decl) { + checkNotNull(decl); + + if (!(decl instanceof ConstDecl)) { + return Optional.empty(); + } + + final ConstDecl constDecl = (ConstDecl) decl; + + LitExpr val = constToExpr.get(constDecl); + if (val == null) { + val = extractLiteral(constDecl); + if (val != null) { + constToExpr.put(constDecl, val); + } + } + + @SuppressWarnings("unchecked") final LitExpr tVal = (LitExpr) val; + return Optional.ofNullable(tVal); + } + + private LitExpr extractLiteral(final ConstDecl decl) { + final Formula formula = transformationManager.toSymbol(decl); + final Type type = decl.getType(); + if (type instanceof FuncType) { + return extractFuncLiteral(formula); + } else if (type instanceof ArrayType) { + return extractArrayLiteral(formula); + } else if (type instanceof BvType) { + return extractBvConstLiteral(formula); + } else { + return extractConstLiteral(formula); + } + } + + private LitExpr extractFuncLiteral(final Formula formula) { + final Expr expr = termTransformer.toExpr(formula); + return (LitExpr) expr; + } + + private LitExpr extractArrayLiteral(final Formula formula) { + final Expr expr = termTransformer.toExpr(formula); + return (LitExpr) expr; + } + + private LitExpr extractBvConstLiteral(final Formula formula) { + final Formula term = model.eval(formula); + if (term == null) { + return null; + } else { + return (BvLitExpr) termTransformer.toExpr(term); + } + } + + private LitExpr extractConstLiteral(final Formula formula) { + final Formula term = model.eval(formula); + if (term == null) { + return null; + } else { + return (LitExpr) termTransformer.toExpr(term); + } + } + + @Override + public Map, LitExpr> toMap() { + getDecls().forEach(this::eval); + return Collections.unmodifiableMap(constToExpr); + } + + //// + + private Collection> constDeclsOf(final Model model) { + final ImmutableList.Builder> builder = ImmutableList.builder(); + for (final Formula symbol : model.asList().stream().map(ValueAssignment::getKey).toList()) { + if (symbolTable.definesSymbol(symbol)) { + final ConstDecl constDecl = symbolTable.getConst(symbol); + builder.add(constDecl); + } + } + return builder.build(); + } + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverException.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverException.java new file mode 100644 index 0000000000..06ead8f05b --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverException.java @@ -0,0 +1,33 @@ +/* + * 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. + */ + +package hu.bme.mit.theta.solver.javasmt; + +public class JavaSMTSolverException extends RuntimeException { + + public JavaSMTSolverException(String message) { + super(message); + } + + public JavaSMTSolverException(String message, Throwable cause) { + super(message, cause); + } + + public JavaSMTSolverException(Throwable cause) { + super(cause); + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java new file mode 100644 index 0000000000..ed3c2a2008 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFactory.java @@ -0,0 +1,194 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.UCSolver; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.log.BasicLogManager; +import org.sosy_lab.common.log.LogManager; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.InterpolatingProverEnvironment; +import org.sosy_lab.java_smt.api.ProverEnvironment; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.SolverContext.ProverOptions; + +import java.util.List; +import java.util.Map; +import java.util.stream.Stream; + +public final class JavaSMTSolverFactory implements SolverFactory { + private final Solvers solver; + + private final Configuration config; + private final LogManager logger; + private final ShutdownManager shutdownManager; + + /** + * Available options (mined from javasmt sources): + * Prefix: solver + * Options: + * * private boolean logAllQueries Export solver queries in SmtLib format into a file. + * * @FileOption(FileOption.Type.OUTPUT_FILE) private @Nullable PathCounterTemplate logfile Export solver queries in SmtLib format into a file. + * * private boolean renameLogfileToAvoidConflicts If logging from the same application, avoid conflicting logfile names. + * * private long randomSeed Random seed for SMT solver. + * * private Solvers solver Which SMT solver to use. + * * private boolean useLogger Log solver actions, this may be slow! + * * private boolean synchronize Sequentialize all solver actions to allow concurrent access! + * * private boolean collectStatistics Counts all operations and interactions towards the SMT solver. + * * private FloatingPointRoundingMode floatingPointRoundingMode Default rounding mode for floating point operations. + * * private NonLinearArithmetic nonLinearArithmetic Use non-linear arithmetic of the solver if supported and throw exception otherwise, + * Prefix: solver.synchronized + * Options: + * * private boolean useSeperateProvers Use provers from a seperate context to solve queries. + * Prefix: solver.boolector + * Options: + * * private SatSolver satSolver The SAT solver used by Boolector. + * * private String furtherOptions Further options for Boolector in addition to the default options. + * Prefix: solver.cvc5 + * Options: + * * private boolean validateInterpolants apply additional validation checks for interpolation results + * Prefix: solver.mathsat5 + * Options: + * * private String furtherOptions Further options that will be passed to Mathsat in addition to the default options. + * * boolean loadOptimathsat5 Load less stable optimizing version of mathsat5 solver. + * Prefix: solver.opensmt + * Options: + * * Logics logic SMT-LIB2 name of the logic to be used by the solver. + * * int algBool Algorithm for boolean interpolation + * * int algUf Algorithm for UF interpolation + * * int algLra Algorithm for LRA interpolation + * Prefix: solver.princess + * Options: + * * private int minAtomsForAbbreviation The number of atoms a term has to have before + * * private boolean enableAssertions Enable additional assertion checks within Princess. + * * private boolean logAllQueriesAsScala log all queries as Princess-specific Scala code + * * @FileOption(FileOption.Type.OUTPUT_FILE) private PathCounterTemplate logAllQueriesAsScalaFile file for Princess-specific dump of queries as Scala code + * Prefix: solver.smtinterpol + * Options: + * * private boolean checkResults Double check generated results like interpolants and models whether they are correct + * * private List furtherOptions Further options that will be set to true for SMTInterpol + * Prefix: solver.z3 + * Options: + * * private boolean usePhantomReferences Whether to use PhantomReferences for discarding Z3 AST + * Prefix: solver.z3 + * Options: + * * boolean requireProofs Require proofs from SMT solver + * * @FileOption(FileOption.Type.OUTPUT_FILE) @Nullable Path log Activate replayable logging in Z3. + * * String optimizationEngine Engine to use for the optimization + * * String objectivePrioritizationMode Ordering for objectives in the optimization context + */ + + private JavaSMTSolverFactory(Solvers solver, String[] args) { + try { + this.solver = solver; + config = Configuration.fromCmdLineArguments(args); + logger = BasicLogManager.create(config); + shutdownManager = ShutdownManager.create(); + } catch (InvalidConfigurationException e) { + throw new JavaSMTSolverException(e); + } + } + + public static JavaSMTSolverFactory create(Solvers solver, Map args) { + return create(solver, args.entrySet().stream().flatMap(e -> Stream.of(e.getKey(), e.getValue())).toList()); + } + + public static JavaSMTSolverFactory create(Solvers solver, List args) { + return create(solver, args.toArray(new String[]{})); + } + + public static JavaSMTSolverFactory create(Solvers solver, String[] args) { + return new JavaSMTSolverFactory(solver, args); + } + + @Override + public Solver createSolver() { + try { + final SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdownManager.getNotifier(), solver); + final JavaSMTSymbolTable symbolTable = new JavaSMTSymbolTable(); + final JavaSMTTransformationManager transformationManager = new JavaSMTTransformationManager(symbolTable, context); + final JavaSMTTermTransformer termTransformer = new JavaSMTTermTransformer(symbolTable, context); + + final ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS); + + return new JavaSMTSolver(symbolTable, transformationManager, termTransformer, context, prover); + } catch (InvalidConfigurationException e) { + throw new JavaSMTSolverException(e); + } + } + + + public Solver createSolverWithPropagators(JavaSMTUserPropagator... propagators) { + try { + final SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdownManager.getNotifier(), solver); + final JavaSMTSymbolTable symbolTable = new JavaSMTSymbolTable(); + final JavaSMTTransformationManager transformationManager = new JavaSMTTransformationManager(symbolTable, context); + final JavaSMTTermTransformer termTransformer = new JavaSMTTermTransformer(symbolTable, context); + + final ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS); + for (JavaSMTUserPropagator propagator : propagators) { + if (!prover.registerUserPropagator(propagator)) { + throw new JavaSMTSolverException("Could not register user propagator " + propagator); + } + propagator.setToExpr(termTransformer::toExpr); + propagator.setToTerm(transformationManager::toTerm); + } + + return new JavaSMTSolver(symbolTable, transformationManager, termTransformer, context, prover); + } catch (InvalidConfigurationException e) { + throw new JavaSMTSolverException(e); + } + } + + @Override + public UCSolver createUCSolver() { + try { + final SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdownManager.getNotifier(), solver); + final JavaSMTSymbolTable symbolTable = new JavaSMTSymbolTable(); + final JavaSMTTransformationManager transformationManager = new JavaSMTTransformationManager(symbolTable, context); + final JavaSMTTermTransformer termTransformer = new JavaSMTTermTransformer(symbolTable, context); + + final ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS, ProverOptions.GENERATE_UNSAT_CORE); + + return new JavaSMTSolver(symbolTable, transformationManager, termTransformer, context, prover); + } catch (InvalidConfigurationException e) { + throw new JavaSMTSolverException(e); + } + } + + @Override + public ItpSolver createItpSolver() { + try { + final SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdownManager.getNotifier(), solver); + final JavaSMTSymbolTable symbolTable = new JavaSMTSymbolTable(); + final JavaSMTTransformationManager transformationManager = new JavaSMTTransformationManager(symbolTable, context); + final JavaSMTTermTransformer termTransformer = new JavaSMTTermTransformer(symbolTable, context); + + final InterpolatingProverEnvironment prover = context.newProverEnvironmentWithInterpolation(ProverOptions.GENERATE_MODELS); + + return new JavaSMTItpSolver(symbolTable, transformationManager, termTransformer, context, prover); + } catch (InvalidConfigurationException e) { + throw new JavaSMTSolverException(e); + } + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java new file mode 100644 index 0000000000..e34221f7fa --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverManager.java @@ -0,0 +1,103 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverBase; +import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.SolverManager; +import hu.bme.mit.theta.solver.UCSolver; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.HashSet; +import java.util.Set; +import java.util.regex.Pattern; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkState; + +public final class JavaSMTSolverManager extends SolverManager { + + private static final Pattern NAME_PATTERN = Pattern.compile("JavaSMT:(.*)"); + + private boolean closed = false; + private final Set instantiatedSolvers = new HashSet<>(); + + private JavaSMTSolverManager() { + } + + public static JavaSMTSolverManager create() { + return new JavaSMTSolverManager(); + } + + @Override + public boolean managesSolver(final String name) { + return NAME_PATTERN.matcher(name).matches(); + } + + @Override + public SolverFactory getSolverFactory(final String name) throws InvalidConfigurationException { + final var matcher = NAME_PATTERN.matcher(name); + checkArgument(matcher.matches()); + final var solverName = matcher.group(1); + final var solver = Solvers.valueOf(solverName); + + return new ManagedFactory(JavaSMTSolverFactory.create(solver, new String[]{})); + } + + @Override + public synchronized void close() throws Exception { + for (final var solver : instantiatedSolvers) { + solver.close(); + } + closed = true; + } + + private final class ManagedFactory implements SolverFactory { + + private final SolverFactory solverFactory; + + private ManagedFactory(final SolverFactory solverFactory) { + this.solverFactory = solverFactory; + } + + @Override + public Solver createSolver() { + checkState(!closed, "Solver manager was closed"); + final var solver = solverFactory.createSolver(); + instantiatedSolvers.add(solver); + return solver; + } + + @Override + public UCSolver createUCSolver() { + checkState(!closed, "Solver manager was closed"); + final var solver = solverFactory.createUCSolver(); + instantiatedSolvers.add(solver); + return solver; + } + + @Override + public ItpSolver createItpSolver() { + checkState(!closed, "Solver manager was closed"); + final var solver = solverFactory.createItpSolver(); + instantiatedSolvers.add(solver); + return solver; + } + } +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSymbolTable.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSymbolTable.java new file mode 100644 index 0000000000..e081b5b8ef --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSymbolTable.java @@ -0,0 +1,96 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.collect.BiMap; +import com.google.common.collect.HashBiMap; +import com.google.common.collect.Maps; +import hu.bme.mit.theta.core.decl.ConstDecl; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FunctionDeclaration; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; + +final class JavaSMTSymbolTable { + + private final BiMap, Formula> constToSymbol; + private final BiMap, FunctionDeclaration> constToFuncDecl; + + public JavaSMTSymbolTable() { + constToSymbol = Maps.synchronizedBiMap(HashBiMap.create()); + constToFuncDecl = Maps.synchronizedBiMap(HashBiMap.create()); + } + + public boolean definesConstAsFormula(final ConstDecl constDecl) { + return constToSymbol.containsKey(constDecl); + } + + public boolean definesConstAsFunction(final ConstDecl constDecl) { + return constToFuncDecl.containsKey(constDecl); + } + + public boolean definesSymbol(final Formula symbol) { + return constToSymbol.inverse().containsKey(symbol); + } + + public boolean definesSymbol(final FunctionDeclaration symbol) { + return constToFuncDecl.inverse().containsKey(symbol); + } + + public Formula getSymbolAsFormula(final ConstDecl constDecl) { + checkArgument(definesConstAsFormula(constDecl), "Declaration %s not found in symbol table", + constDecl); + return constToSymbol.get(constDecl); + } + + public FunctionDeclaration getSymbolAsFunction(final ConstDecl constDecl) { + checkArgument(definesConstAsFunction(constDecl), "Declaration %s not found in symbol table", + constDecl); + return constToFuncDecl.get(constDecl); + } + + public ConstDecl getConst(final Formula symbol) { + checkArgument(definesSymbol(symbol), "Symbol %s not found in symbol table", symbol); + return constToSymbol.inverse().get(symbol); + } + + public ConstDecl getConst(final FunctionDeclaration symbol) { + checkArgument(definesSymbol(symbol), "Symbol %s not found in symbol table", symbol); + return constToFuncDecl.inverse().get(symbol); + } + + public void put(final ConstDecl constDecl, final Formula symbol) { + checkNotNull(constDecl); + checkNotNull(symbol); + checkState(!constToSymbol.containsKey(constDecl), "Constant %s not found.", constDecl); + constToSymbol.put(constDecl, symbol); + } + + public void put(final ConstDecl constDecl, final FunctionDeclaration symbol) { + checkNotNull(constDecl); + checkNotNull(symbol); + checkState(!constToFuncDecl.containsKey(constDecl), "Constant %s not found.", constDecl); + constToFuncDecl.put(constDecl, symbol); + } + + public void clear() { + constToSymbol.clear(); + constToFuncDecl.clear(); + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java new file mode 100644 index 0000000000..387d31fd76 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTermTransformer.java @@ -0,0 +1,585 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.collect.Lists; +import hu.bme.mit.theta.common.QuadFunction; +import hu.bme.mit.theta.common.TernaryOperator; +import hu.bme.mit.theta.common.TriFunction; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.common.container.Containers; +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.decl.ParamDecl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.abstracttype.AbstractExprs; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayType; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.bvtype.BvExtractExpr; +import hu.bme.mit.theta.core.type.bvtype.BvLitExpr; +import hu.bme.mit.theta.core.type.bvtype.BvSExtExpr; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.bvtype.BvZExtExpr; +import hu.bme.mit.theta.core.type.fptype.FpFromBvExpr; +import hu.bme.mit.theta.core.type.fptype.FpLitExpr; +import hu.bme.mit.theta.core.type.fptype.FpRoundingMode; +import hu.bme.mit.theta.core.type.fptype.FpToBvExpr; +import hu.bme.mit.theta.core.type.fptype.FpToFpExpr; +import hu.bme.mit.theta.core.type.fptype.FpType; +import hu.bme.mit.theta.core.type.functype.FuncExprs; +import hu.bme.mit.theta.core.type.functype.FuncType; +import hu.bme.mit.theta.core.type.inttype.IntLitExpr; +import hu.bme.mit.theta.core.utils.BvUtils; +import hu.bme.mit.theta.core.utils.TypeUtils; +import org.sosy_lab.common.rationals.Rational; +import org.sosy_lab.java_smt.api.BitvectorFormula; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; +import org.sosy_lab.java_smt.api.FormulaType.BitvectorType; +import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; +import org.sosy_lab.java_smt.api.FunctionDeclaration; +import org.sosy_lab.java_smt.api.Model; +import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.visitors.FormulaVisitor; + +import java.math.BigInteger; +import java.util.ArrayList; +import java.util.List; +import java.util.Map; +import java.util.function.BiFunction; +import java.util.function.BinaryOperator; +import java.util.function.Function; +import java.util.function.Supplier; +import java.util.function.UnaryOperator; +import java.util.regex.Matcher; +import java.util.regex.Pattern; +import java.util.stream.Collectors; + +import static com.google.common.base.Preconditions.checkArgument; +import static com.google.common.base.Preconditions.checkNotNull; +import static com.google.common.base.Preconditions.checkState; +import static com.google.common.collect.ImmutableList.toImmutableList; +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.decl.Decls.Param; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Exists; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.False; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.rattype.RatExprs.Rat; + +final class JavaSMTTermTransformer { + + private static final String PARAM_NAME_FORMAT = "_p%d"; + + private final JavaSMTSymbolTable symbolTable; + private final SolverContext context; + private final Map, QuadFunction, Model, List>, Expr>> environment; + + public JavaSMTTermTransformer(final JavaSMTSymbolTable symbolTable, SolverContext context) { + this.symbolTable = symbolTable; + this.context = context; + + environment = Containers.createMap(); + addFunc("and", exprMultiaryOperator(hu.bme.mit.theta.core.type.booltype.AndExpr::create)); + addFunc("false", exprNullaryOperator(hu.bme.mit.theta.core.type.booltype.FalseExpr::getInstance)); + addFunc("true", exprNullaryOperator(hu.bme.mit.theta.core.type.booltype.TrueExpr::getInstance)); + addFunc("iff", exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.IffExpr::create)); + addFunc("not", exprUnaryOperator(hu.bme.mit.theta.core.type.booltype.NotExpr::create)); + addFunc("=>", exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.ImplyExpr::create)); + addFunc("xor", exprBinaryOperator(hu.bme.mit.theta.core.type.booltype.XorExpr::create)); + addFunc("or", exprMultiaryOperator(hu.bme.mit.theta.core.type.booltype.OrExpr::create)); + addFunc("ite", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create)); + addFunc("if", exprTernaryOperator(hu.bme.mit.theta.core.type.anytype.IteExpr::create)); + addFunc("prime", exprUnaryOperator(hu.bme.mit.theta.core.type.anytype.PrimeExpr::of)); + addFunc("=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Eq)); + addFunc(">=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Geq)); + addFunc(">", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Gt)); + addFunc("<=", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Leq)); + addFunc("<", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Lt)); + addFunc("+", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Add)); + addFunc("-", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Sub)); + addFunc("+", exprUnaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Pos)); + addFunc("-", exprUnaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Neg)); + addFunc("*", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Mul)); + addFunc("/", exprBinaryOperator(hu.bme.mit.theta.core.type.abstracttype.AbstractExprs::Div)); + addFunc("to_int", exprUnaryOperator(hu.bme.mit.theta.core.type.rattype.RatToIntExpr::create)); + addFunc("div", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntDivExpr::create)); + addFunc("to_rat", exprUnaryOperator(hu.bme.mit.theta.core.type.inttype.IntToRatExpr::create)); + addFunc("mod", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntModExpr::create)); + addFunc("rem", exprBinaryOperator(hu.bme.mit.theta.core.type.inttype.IntRemExpr::create)); + addFunc("fp.add", exprFpMultiaryOperator(hu.bme.mit.theta.core.type.fptype.FpAddExpr::create)); + addFunc("fp.sub", exprFpBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpSubExpr::create)); + addFunc("fp.pos", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpPosExpr::create)); + addFunc("fp.neg", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpNegExpr::create)); + addFunc("fp.mul", exprFpMultiaryOperator(hu.bme.mit.theta.core.type.fptype.FpMulExpr::create)); + addFunc("fp.div", exprFpBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpDivExpr::create)); + addFunc("fp.rem", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpRemExpr::create)); + addFunc("fprem", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpRemExpr::create)); + addFunc("fp.abs", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpAbsExpr::create)); + addFunc("fp.leq", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpLeqExpr::create)); + addFunc("fp.lt", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpLtExpr::create)); + addFunc("fp.geq", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpGeqExpr::create)); + addFunc("fp.gt", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpGtExpr::create)); + addFunc("fp.eq", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpEqExpr::create)); + addFunc("fp.isnan", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsNanExpr::create)); + addFunc("fp.isNaN", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsNanExpr::create)); + addFunc("isinfinite", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr::create)); + addFunc("fp.isInfinite", exprUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpIsInfiniteExpr::create)); + addFunc("fp.roundtoint", exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr::create)); + addFunc("fp.roundToIntegral", exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpRoundToIntegralExpr::create)); + addFunc("fp.sqrt", exprFpUnaryOperator(hu.bme.mit.theta.core.type.fptype.FpSqrtExpr::create)); + addFunc("fp.max", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpMaxExpr::create)); + addFunc("fp.min", exprBinaryOperator(hu.bme.mit.theta.core.type.fptype.FpMinExpr::create)); + addFunc("++", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvConcatExpr::create)); + addFunc("concat", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvConcatExpr::create)); + addFunc("bvadd", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvAddExpr::create)); + addFunc("bvsub", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSubExpr::create)); + addFunc("bvpos", exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvPosExpr::create)); + addFunc("bvneg", exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvNegExpr::create)); + addFunc("bvmul", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvMulExpr::create)); + addFunc("bvudiv", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUDivExpr::create)); + addFunc("bvsdiv", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSDivExpr::create)); + addFunc("bvsmod", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSModExpr::create)); + addFunc("bvurem", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvURemExpr::create)); + addFunc("bvsrem", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSRemExpr::create)); + addFunc("bvor", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvOrExpr::create)); + addFunc("bvand", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvAndExpr::create)); + addFunc("bvxor", exprMultiaryOperator(hu.bme.mit.theta.core.type.bvtype.BvXorExpr::create)); + addFunc("bvnot", exprUnaryOperator(hu.bme.mit.theta.core.type.bvtype.BvNotExpr::create)); + addFunc("bvshl", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr::create)); + addFunc("bvashr", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvArithShiftRightExpr::create)); + addFunc("bvlshr", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvLogicShiftRightExpr::create)); + addFunc("bvrol", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create)); + addFunc("ext_rotate_left", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateLeftExpr::create)); + addFunc("bvror", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create)); + addFunc("ext_rotate_right", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvRotateRightExpr::create)); + addFunc("bvult", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULtExpr::create)); + addFunc("bvule", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvULeqExpr::create)); + addFunc("bvugt", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUGtExpr::create)); + addFunc("bvuge", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr::create)); + addFunc("bvslt", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSLtExpr::create)); + addFunc("bvsle", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSLeqExpr::create)); + addFunc("bvsgt", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSGtExpr::create)); + addFunc("bvsge", exprBinaryOperator(hu.bme.mit.theta.core.type.bvtype.BvSGeqExpr::create)); + addFunc("read", exprBinaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr::create)); + addFunc("write", exprTernaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr::create)); + addFunc("select", exprBinaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayReadExpr::create)); + addFunc("store", exprTernaryOperator(hu.bme.mit.theta.core.type.arraytype.ArrayWriteExpr::create)); + + environment.put(Tuple2.of("fp.frombv", 1), (term, args, model, vars) -> { + FloatingPointType type = (FloatingPointType) context.getFormulaManager().getFormulaType((FloatingPointFormula) term); + final var roundingmode = getRoundingMode(args.get(0).toString()); + final Expr op = (Expr) transform(args.get(1), model, vars); + return FpFromBvExpr.of(roundingmode, op, FpType.of(type.getExponentSize(), type.getMantissaSize() + 1), true); + }); + environment.put(Tuple2.of("fp.to_sbv", 2), (term, args, model, vars) -> { + BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); + final var roundingmode = getRoundingMode(args.get(0).toString()); + final Expr op = (Expr) transform(args.get(1), model, vars); + return FpToBvExpr.of(roundingmode, op, type.getSize(), true); + }); + environment.put(Tuple2.of("fp.to_ubv", 2), (term, args, model, vars) -> { + BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); + final var roundingmode = getRoundingMode(args.get(0).toString()); + final Expr op = (Expr) transform(args.get(1), model, vars); + return FpToBvExpr.of(roundingmode, op, type.getSize(), false); + }); + environment.put(Tuple2.of("to_fp", 2), (term, args, model, vars) -> { + FloatingPointType type = (FloatingPointType) context.getFormulaManager().getFormulaType((FloatingPointFormula) term); + final var roundingmode = getRoundingMode(args.get(0).toString()); + final Expr op = transform(args.get(1), model, vars); + if (op.getType() instanceof FpType) { + return FpToFpExpr.of(roundingmode, (Expr) op, type.getExponentSize(), type.getMantissaSize() + 1); + } else if (op.getType() instanceof BvType) { + return FpFromBvExpr.of(roundingmode, (Expr) op, FpType.of(type.getExponentSize(), type.getMantissaSize() + 1), false); + } else { + throw new JavaSMTSolverException("Unsupported:" + op.getType()); + } + }); + environment.put(Tuple2.of("to_fp", 1), (term, args, model, vars) -> { + FloatingPointType type = (FloatingPointType) context.getFormulaManager().getFormulaType((FloatingPointFormula) term); + final Expr op = (Expr) transform(args.get(0), model, vars); + return FpFromBvExpr.of(FpRoundingMode.getDefaultRoundingMode(), op, FpType.of(type.getExponentSize(), type.getMantissaSize() + 1), true); + }); + + environment.put(Tuple2.of("extract", 1), (term, args, model, vars) -> { + final Pattern pattern = Pattern.compile("extract ([0-9]+) ([0-9]+)"); + final String termStr = term.toString(); + final Matcher match = pattern.matcher(termStr); + if (match.find()) { + final int to = Integer.parseInt(match.group(1)) + 1; + final int from = Integer.parseInt(match.group(2)); + final Expr op = (Expr) transform(args.get(0), model, vars); + return BvExtractExpr.of(op, Int(from), Int(to)); + } + throw new JavaSMTSolverException("Not supported: " + term); + }); + environment.put(Tuple2.of("zero_extend", 1), (term, args, model, vars) -> { + BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); + final Expr op = (Expr) transform(args.get(0), model, vars); + return BvZExtExpr.of(op, BvType.of(type.getSize())); + }); + environment.put(Tuple2.of("sign_extend", 1), (term, args, model, vars) -> { + BitvectorType type = (BitvectorType) context.getFormulaManager().getFormulaType((BitvectorFormula) term); + final Expr op = (Expr) transform(args.get(0), model, vars); + return BvSExtExpr.of(op, BvType.of(type.getSize())); + }); + environment.put(Tuple2.of("EqZero", 1), (term, args, model, vars) -> { + final Expr op = transform(args.get(0), model, vars); + return AbstractExprs.Eq(op, TypeUtils.getDefaultValue(op.getType())); + }); + environment.put(Tuple2.of("fp", 3), (term, args, model, vars) -> { + final Expr op1 = (Expr) transform(args.get(0), model, vars); + final Expr op2 = (Expr) transform(args.get(1), model, vars); + final Expr op3 = (Expr) transform(args.get(2), model, vars); + return FpLitExpr.of((BvLitExpr) op1, (BvLitExpr) op2, (BvLitExpr) op3); + }); + environment.put(Tuple2.of("const", 1), (term, args, model, vars) -> { + return transformLit(term, transform(args.get(0), model, vars)); + }); + } + + private void addFunc(String name, Tuple2, Model, List>, Expr>> func) { + checkArgument(!environment.containsKey(Tuple2.of(name, func.get1())), "Duplicate key: " + Tuple2.of(name, func.get1())); + environment.put(Tuple2.of(name, func.get1()), func.get2()); + } + + public Expr toExpr(final Formula term) { + return transform(term, null, new ArrayList<>()); + } + + //////// + + private Expr transform(final Formula term, final Model model, + final List> vars) { + + try { + return context.getFormulaManager().visit(term, new FormulaVisitor>() { + @Override + public Expr visitFreeVariable(Formula f, String name) { + return transformVar(f, name, vars); + } + + @Override + public Expr visitBoundVariable(Formula f, int deBruijnIdx) { + return Lists.reverse(vars).get(deBruijnIdx).getRef(); // I think the reverse list is necessary here. + } + + @Override + public Expr visitConstant(Formula f, Object value) { + return transformLit(f, value); + } + + @Override + public Expr visitFunction(Formula f, List args, FunctionDeclaration functionDeclaration) { + return transformApp(f, functionDeclaration, args, model, vars); + } + + @Override + public Expr visitQuantifier(BooleanFormula f, Quantifier quantifier, List boundVariables, BooleanFormula body) { + return transformQuantifier(quantifier, boundVariables, model, body, vars); + } + }); + } catch (JavaSMTSolverException e) { + throw new JavaSMTSolverException("Not supported: " + term, e); + } + } + + private Expr transformLit(Formula f, Object value) { + FormulaType type = context.getFormulaManager().getFormulaType(f); + if (type.isIntegerType()) { + checkArgument(value instanceof BigInteger, "Type mismatch (Expected BigInteger): " + value + " (" + value.getClass().getSimpleName() + ")"); + return transformIntLit(f, (BigInteger) value); + } else if (type.isRationalType()) { + checkArgument(value instanceof Rational || value instanceof BigInteger, "Type mismatch (Expected Rational or BigInteger): " + value + " (" + value.getClass().getSimpleName() + ")"); + if (value instanceof Rational) { + return transformRatLit(f, (Rational) value); + } else if (value instanceof BigInteger) { + return transformRatLit(f, (BigInteger) value); + } + } else if (type.isBitvectorType()) { + checkArgument(value instanceof BigInteger, "Type mismatch (Expected BigInteger): " + value + " (" + value.getClass().getSimpleName() + ")"); + return transformBvLit(f, (BigInteger) value); + } else if (type.isFloatingPointType()) { + checkArgument(value instanceof FloatingPointNumber, "Type mismatch (Expected FloatingPointNumber): " + value + " (" + value.getClass().getSimpleName() + ")"); + return transformFpLit((FloatingPointNumber) value); + } else if (type.isArrayType()) { + checkArgument(value instanceof Expr, "Typ mismatch (Expected Expr): " + value + " (" + value.getClass().getSimpleName() + ")"); + return transformArrLit(f, (Expr) value); + } else if (type.isBooleanType()) { + if (Boolean.TRUE.equals(value)) { + return True(); + } else if (Boolean.FALSE.equals(value)) { + return False(); + } + } + throw new JavaSMTSolverException("Not supported: " + f); + } + + //// + + private Expr transformIntLit(final Formula term, final BigInteger value) { + return Int(value); + } + + private Expr transformRatLit(final Formula term, BigInteger value) { + return Rat(value, BigInteger.ONE); + } + + private Expr transformRatLit(final Formula term, Rational value) { + return Rat(value.getNum(), value.getDen()); + } + + private Expr transformArrLit(final Formula term, Expr value) { + final ArrayType type = (ArrayType) transformType(context.getFormulaManager().getFormulaType(term)); + if (value instanceof LitExpr) { + return ArrayLitExpr.of(List.of(), value, type); + } else { + return ArrayInitExpr.of(List.of(), value, type); + } + } + + private Expr transformBvLit(final Formula term, BigInteger value) { + final var bvNum = (BitvectorFormula) term; + BitvectorType formulaType = (BitvectorType) context.getFormulaManager().getFormulaType(bvNum); + + return BvUtils.bigIntegerToNeutralBvLitExpr(value, formulaType.getSize()); + } + + private Expr transformFpLit(FloatingPointNumber value) { + return FpLitExpr.of( + value.getSign(), + BvUtils.bigIntegerToNeutralBvLitExpr(value.getExponent(), value.getExponentSize()), + BvUtils.bigIntegerToNeutralBvLitExpr(value.getMantissa(), value.getMantissaSize())); + } + + private Expr transformApp(Formula f, final FunctionDeclaration funcDecl, + final List args, + final Model model, + final List> vars) { + + final var key1 = Tuple2.of(funcDecl.getName(), args.size()); + final var key2 = Tuple2.of(funcDecl.getName(), -1); + if (environment.containsKey(key1)) { + return environment.get(key1).apply(f, args, model, vars); + } else if (environment.containsKey(key2)) { + return environment.get(key2).apply(f, args, model, vars); + } else { + final var paramExprs = args.stream().map((Formula term) -> (Expr) toExpr(term)).toList(); + + final Expr> funcExpr; + if (symbolTable.definesSymbol(funcDecl)) { + funcExpr = (Expr>) checkNotNull(symbolTable.getConst(funcDecl).getRef()); + } else { + funcExpr = Const(funcDecl.getName(), getFuncType( + transformType(context.getFormulaManager().getFormulaType(f)), + args.stream().map(context.getFormulaManager()::getFormulaType).map(this::transformType).toList() + )).getRef(); + } + + return FuncExprs.App(funcExpr, paramExprs); + } + } + + private

FuncType getFuncType(final R resultType, final List

paramTypes) { + if (paramTypes.size() == 1) { + return FuncType.of(paramTypes.get(0), resultType); + } else { + return (FuncType) FuncType.of(paramTypes.get(0), getFuncType(resultType, paramTypes.subList(1, paramTypes.size()))); + } + } + + private ParamDecl transformParam(Formula term) { + final var type = context.getFormulaManager().getFormulaType(term); + final var thetaType = transformType(type); + return Param(term.toString(), thetaType); + } + + private Expr transformQuantifier(final Quantifier term, final List boundVars, + final Model model, final BooleanFormula body, final List> vars) { + + final List> params = boundVars + .stream() + .map(this::transformParam) + .collect(Collectors.toList()); + final Expr ret; + + pushParams(vars, params); + final Expr expr = (Expr) transform(body, model, vars); + popParams(vars, params); + + if (term == Quantifier.EXISTS) { + ret = Exists(params, expr); + } else { + ret = Forall(params, expr); + } + + return ret; + } + + private void pushParams(final List> vars, final List> paramDecls) { + vars.addAll(paramDecls); + } + + private void popParams(final List> vars, final List> paramDecls) { + for (int i = 0; i < paramDecls.size(); i++) { + vars.remove(vars.size() - 1); + } + } + + private Expr transformVar(final Formula term, String name, final List> vars) { + FormulaType type = context.getFormulaManager().getFormulaType(term); + Type thetaType = transformType(type); + final var c = symbolTable.getConst(term); + checkState(thetaType == null || c.getType().equals(thetaType)); + return c.getRef(); + } + + private Type transformType(FormulaType type) { + if (type.isIntegerType()) { + return Int(); + } else if (type.isRationalType()) { + return Rat(); + } else if (type.isBitvectorType()) { + BitvectorType bvType = (BitvectorType) type; + return BvType.of(bvType.getSize()); + } else if (type.isFloatingPointType()) { + FloatingPointType fpType = (FloatingPointType) type; + return FpType.of(fpType.getExponentSize(), fpType.getMantissaSize() + 1); + } else if (type.isArrayType()) { + ArrayFormulaType arrayFormulaType = (ArrayFormulaType) type; + final var indexType = arrayFormulaType.getIndexType(); + final var elemType = arrayFormulaType.getElementType(); + return ArrayType.of(transformType(indexType), transformType(elemType)); + } else if (type.isBooleanType()) { + return Bool(); + } + throw new JavaSMTSolverException("Type not supported: " + type); + } + + //// + + private Tuple2, Model, List>, Expr>> exprNullaryOperator( + final Supplier> function) { + return Tuple2.of(0, (term, args, model, vars) -> { + checkArgument(args.isEmpty(), "Number of arguments must be zero"); + return function.get(); + }); + } + + private Tuple2, Model, List>, Expr>> exprUnaryOperator( + final UnaryOperator> function) { + return Tuple2.of(1, (term, args, model, vars) -> { + checkArgument(args.size() == 1, "Number of arguments must be one"); + final Expr op = transform(args.get(0), model, vars); + return function.apply(op); + }); + } + + private Tuple2, Model, List>, Expr>> exprBinaryOperator( + final BinaryOperator> function) { + return Tuple2.of(2, (term, args, model, vars) -> { + checkArgument(args.size() == 2, "Number of arguments must be two"); + final Expr op1 = transform(args.get(0), model, vars); + final Expr op2 = transform(args.get(1), model, vars); + return function.apply(op1, op2); + }); + } + + private Tuple2, Model, List>, Expr>> exprTernaryOperator( + final TernaryOperator> function) { + return Tuple2.of(3, (term, args, model, vars) -> { + checkArgument(args.size() == 3, "Number of arguments must be three"); + final Expr op1 = transform(args.get(0), model, vars); + final Expr op2 = transform(args.get(1), model, vars); + final Expr op3 = transform(args.get(2), model, vars); + return function.apply(op1, op2, op3); + }); + } + + private Tuple2, Model, List>, Expr>> exprMultiaryOperator( + final Function>, Expr> function) { + return Tuple2.of(-1, (term, args, model, vars) -> { + final List> ops = args.stream().map(arg -> transform(arg, model, vars)) + .collect(toImmutableList()); + return function.apply(ops); + }); + } + + + private Tuple2, Model, List>, Expr>> exprFpUnaryOperator( + final BiFunction, Expr> function) { + return Tuple2.of(2, (term, args, model, vars) -> { + checkArgument(args.size() == 2, "Number of arguments must be two"); + final var roundingmode = getRoundingMode(args.get(0).toString()); + final Expr op2 = transform(args.get(1), model, vars); + return function.apply(roundingmode, op2); + }); + } + + private Tuple2, Model, List>, Expr>> exprFpBinaryOperator( + final TriFunction, Expr, Expr> function) { + return Tuple2.of(3, (term, args, model, vars) -> { + checkArgument(args.size() == 3, "Number of arguments must be three"); + final var roundingmode = getRoundingMode(args.get(0).toString()); + final Expr op1 = transform(args.get(1), model, vars); + final Expr op2 = transform(args.get(2), model, vars); + return function.apply(roundingmode, op1, op2); + }); + } + + private Tuple2, Model, List>, Expr>> exprFpMultiaryOperator( + final BiFunction>, Expr> function) { + return Tuple2.of(-1, (term, args, model, vars) -> { + final var roundingmode = getRoundingMode(args.get(0).toString()); + final List> ops = args.stream().skip(1).map(arg -> transform(arg, model, vars)) + .collect(toImmutableList()); + return function.apply(roundingmode, ops); + }); + } + + private Tuple2, Model, List>, Expr>> exprFpLitUnaryOperator( + final BiFunction> function) { + return Tuple2.of(3, (term, args, model, vars) -> { + final BvLitExpr op1 = (BvLitExpr) transform(args.get(0), model, vars); + final IntLitExpr op2 = (IntLitExpr) transform(args.get(1), model, vars); + final IntLitExpr op3 = (IntLitExpr) transform(args.get(2), model, vars); + return function.apply(op1, FpType.of(op2.getValue().intValue(), op3.getValue().intValue() + 1)); + }); + } + + private FpRoundingMode getRoundingMode(String s) { + return switch (s) { + case "roundNearestTiesToAway" -> FpRoundingMode.RNA; + case "roundNearestTiesToEven" -> FpRoundingMode.RNE; + case "roundTowardZero" -> FpRoundingMode.RTZ; + default -> throw new JavaSMTSolverException("Unexpected value: " + s); + }; + } + + +} + diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformationManager.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformationManager.java new file mode 100644 index 0000000000..4ea1d6dda3 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformationManager.java @@ -0,0 +1,53 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.decl.Decl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.SolverContext; + +final class JavaSMTTransformationManager { + + private final JavaSMTTypeTransformer typeTransformer; + private final JavaSMTDeclTransformer declTransformer; + private final JavaSMTExprTransformer exprTransformer; + + public JavaSMTTransformationManager(final JavaSMTSymbolTable symbolTable, final SolverContext context) { + this.typeTransformer = new JavaSMTTypeTransformer(); + this.declTransformer = new JavaSMTDeclTransformer(this, symbolTable, context); + this.exprTransformer = new JavaSMTExprTransformer(this, symbolTable, context); + } + + public FormulaType toSort(final Type type) { + return typeTransformer.toSort(type); + } + + public Formula toSymbol(final Decl decl) { + return declTransformer.toSymbol(decl); + } + + public Formula toTerm(final Expr expr) { + return exprTransformer.toTerm(expr); + } + + public void reset() { + // declTransformer does not have to be reset + exprTransformer.reset(); + } +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java new file mode 100644 index 0000000000..cf6d051354 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTypeTransformer.java @@ -0,0 +1,64 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.arraytype.ArrayType; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.fptype.FpType; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.core.type.rattype.RatType; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; +import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; + +final class JavaSMTTypeTransformer { + + private final FormulaType boolSort; + private final FormulaType intSort; + private final FormulaType realSort; + + JavaSMTTypeTransformer() { + boolSort = FormulaType.BooleanType; + intSort = FormulaType.IntegerType; + realSort = FormulaType.RationalType; + } + + public FormulaType toSort(final Type type) { + if (type instanceof BoolType) { + return boolSort; + } else if (type instanceof IntType) { + return intSort; + } else if (type instanceof RatType) { + return realSort; + } else if (type instanceof BvType bvType) { + return FormulaType.getBitvectorTypeWithSize(bvType.getSize()); + } else if (type instanceof FpType fpType) { + return FormulaType.getFloatingPointType(fpType.getExponent(), + fpType.getSignificand()); + } else if (type instanceof ArrayType arrayType) { + final FormulaType indexSort = toSort(arrayType.getIndexType()); + final FormulaType elemSort = toSort(arrayType.getElemType()); + return FormulaType.getArrayType(indexSort, elemSort); + } else { + throw new UnsupportedOperationException( + "Unsupported type: " + type.getClass().getSimpleName()); + } + } + +} diff --git a/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTUserPropagator.java b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTUserPropagator.java new file mode 100644 index 0000000000..0bc2bcb02e --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTUserPropagator.java @@ -0,0 +1,137 @@ +/* + * 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. + */ + +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import org.sosy_lab.java_smt.api.BooleanFormula; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.PropagatorBackend; +import org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator; + +import java.util.Arrays; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; +import java.util.Objects; +import java.util.Optional; +import java.util.function.Function; + +import static com.google.common.base.Preconditions.checkState; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.utils.TypeUtils.cast; + +public abstract class JavaSMTUserPropagator extends AbstractUserPropagator { + private Function, Formula> toTerm; + private Function> toExpr; + private final Map, BooleanFormula> registeredTerms; + + protected JavaSMTUserPropagator() { + super(); + registeredTerms = new LinkedHashMap<>(); + } + + final void setToTerm(final Function, Formula> toTerm) { + this.toTerm = toTerm; + } + + final void setToExpr(final Function> toExpr) { + this.toExpr = toExpr; + } + + @Override + protected final PropagatorBackend getBackend() { + return super.getBackend(); + } + + /** + * Gets called when the solver decides on the value for a bool expression. + * Can call propagate* calls from here. + * When overriding, no need to call super. + * + * @param expr The expression for which a value became available + * @param value The value of the expression + */ + public void onKnownValue(final Expr expr, final boolean value) { + } + + @Override + public final void onKnownValue(final BooleanFormula expr, final boolean value) { + super.onKnownValue(expr, value); + final var tExpr = cast(toExpr.apply(expr), Bool()); + onKnownValue(tExpr, value); + } + + /** + * Gets called when a branching is done on a registered expression. + * Change the decision by calling propagateNextDecision. + * + * @param expr + * @param value + */ + public void onDecision(final Expr expr, final boolean value) { + } + + @Override + public final void onDecision(final BooleanFormula expr, final boolean value) { + super.onDecision(expr, value); + final var tExpr = cast(toExpr.apply(expr), Bool()); + onDecision(tExpr, value); + } + + @Override + public final void initializeWithBackend(final PropagatorBackend pBackend) { + super.initializeWithBackend(pBackend); + getBackend().notifyOnFinalCheck(); + getBackend().notifyOnKnownValue(); + getBackend().notifyOnDecision(); + } + + /** + * Register an expression with the propagator. Does NOT add it to the solver. + * + * @param expr The expression to register + */ + public void registerExpression(final Expr expr) { + final BooleanFormula booleanFormula = (BooleanFormula) toTerm.apply(expr); + registeredTerms.put(expr, booleanFormula); + registerExpression(booleanFormula); + } + + @Override + public final void registerExpression(final BooleanFormula theoryExpr) { + super.registerExpression(theoryExpr); + } + + public final void propagateConflict(final List> exprs) { + final var terms = exprs.stream().map(registeredTerms::get).toArray(BooleanFormula[]::new); + checkState(Arrays.stream(terms).noneMatch(Objects::isNull)); + getBackend().propagateConflict(terms); + } + + public final void propagateConsequence(final List> exprs, final Expr consequence) { + final var terms = exprs.stream().map(registeredTerms::get).toArray(BooleanFormula[]::new); + checkState(Arrays.stream(terms).noneMatch(Objects::isNull), "Registered terms failed to look up one or more expressions from %s. Registered terms: %s", exprs, registeredTerms.keySet()); + final BooleanFormula consequenceTerm = (BooleanFormula) toTerm.apply(consequence); + getBackend().propagateConsequence(terms, consequenceTerm); + } + + public final boolean propagateNextDecision(final Expr formula, Optional optional) { + final BooleanFormula term = (BooleanFormula) toTerm.apply(formula); + return getBackend().propagateNextDecision(term, optional); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolverTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolverTest.java new file mode 100644 index 0000000000..b36c03622d --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTItpSolverTest.java @@ -0,0 +1,269 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.collect.ImmutableList; +import hu.bme.mit.theta.common.OsHelper; +import hu.bme.mit.theta.common.OsHelper.OperatingSystem; +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.ParamDecl; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.functype.FuncType; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.core.utils.ExprUtils; +import hu.bme.mit.theta.solver.Interpolant; +import hu.bme.mit.theta.solver.ItpMarker; +import hu.bme.mit.theta.solver.ItpPattern; +import hu.bme.mit.theta.solver.ItpSolver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Assert; +import org.junit.Before; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.junit.runners.Parameterized.Parameters; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.Collection; +import java.util.List; + +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.decl.Decls.Param; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Forall; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Imply; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; +import static hu.bme.mit.theta.core.type.functype.FuncExprs.App; +import static hu.bme.mit.theta.core.type.functype.FuncExprs.Func; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Mul; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Neq; +import static hu.bme.mit.theta.solver.ItpMarkerTree.Leaf; +import static hu.bme.mit.theta.solver.ItpMarkerTree.Subtree; +import static hu.bme.mit.theta.solver.ItpMarkerTree.Tree; +import static org.junit.Assume.assumeFalse; + +@RunWith(Parameterized.class) +public final class JavaSMTItpSolverTest { + @Parameter(0) + public Solvers solver; + @Parameter(1) + public ItpSolver itpSolver; + + Expr a; + Expr b; + Expr c; + Expr d; + Expr e; + Expr> f; + Expr> g; + + + @Parameters(name = "solver: {0}") + public static Collection operations() { + if (OsHelper.getOs().equals(OperatingSystem.LINUX)) { + return List.of( + new Object[]{Solvers.SMTINTERPOL, JavaSMTSolverFactory.create(Solvers.SMTINTERPOL, new String[]{}).createItpSolver()}, + new Object[]{Solvers.PRINCESS, JavaSMTSolverFactory.create(Solvers.PRINCESS, new String[]{}).createItpSolver()}, + new Object[]{Solvers.CVC5, JavaSMTSolverFactory.create(Solvers.CVC5, new String[]{}).createItpSolver()} + ); + } else { + return List.of( + new Object[]{Solvers.SMTINTERPOL, JavaSMTSolverFactory.create(Solvers.SMTINTERPOL, new String[]{}).createItpSolver()}, + new Object[]{Solvers.PRINCESS, JavaSMTSolverFactory.create(Solvers.PRINCESS, new String[]{}).createItpSolver()} + ); + } + } + + @Before + public void initialize() { + final ConstDecl ad = Const("a", Int()); + final ConstDecl bd = Const("b", Int()); + final ConstDecl cd = Const("c", Int()); + final ConstDecl dd = Const("d", Int()); + final ConstDecl ed = Const("e", Int()); + final ConstDecl> fd = Const("f", Func(Int(), Int())); + final ConstDecl> gd = Const("g", Func(Int(), Int())); + + a = ad.getRef(); + b = bd.getRef(); + c = cd.getRef(); + d = dd.getRef(); + e = ed.getRef(); + f = fd.getRef(); + g = gd.getRef(); + } + + @Test + public void testBinaryInterpolation() { + final ItpMarker A = itpSolver.createMarker(); + final ItpMarker B = itpSolver.createMarker(); + final ItpPattern pattern = itpSolver.createBinPattern(A, B); + + itpSolver.add(A, Eq(a, b)); + itpSolver.add(A, Eq(a, c)); + itpSolver.add(B, Eq(b, d)); + itpSolver.add(B, Neq(c, d)); + + itpSolver.check(); + Assert.assertEquals(SolverStatus.UNSAT, itpSolver.getStatus()); + final Interpolant itp = itpSolver.getInterpolant(pattern); + + System.out.println(itp.eval(A)); + System.out.println("----------"); + Assert.assertTrue(ExprUtils.getVars(itp.eval(A)).size() <= 3); + } + + @Test + public void testSequenceInterpolation() { + final ItpMarker I1 = itpSolver.createMarker(); + final ItpMarker I2 = itpSolver.createMarker(); + final ItpMarker I3 = itpSolver.createMarker(); + final ItpMarker I4 = itpSolver.createMarker(); + final ItpMarker I5 = itpSolver.createMarker(); + final ItpPattern pattern = itpSolver.createSeqPattern(ImmutableList.of(I1, I2, I3, I4, I5)); + + itpSolver.add(I1, Eq(a, Int(0))); + itpSolver.add(I2, Eq(a, b)); + itpSolver.add(I3, Eq(c, d)); + itpSolver.add(I4, Eq(d, Int(1))); + itpSolver.add(I5, Eq(b, c)); + + itpSolver.check(); + Assert.assertEquals(SolverStatus.UNSAT, itpSolver.getStatus()); + final Interpolant itp = itpSolver.getInterpolant(pattern); + + System.out.println(itp.eval(I1)); + System.out.println(itp.eval(I2)); + System.out.println(itp.eval(I3)); + System.out.println(itp.eval(I4)); + System.out.println(itp.eval(I5)); + System.out.println("----------"); + } + + @Test + public void testTreeInterpolation() { + assumeFalse(solver == Solvers.CVC5); + + final ItpMarker I1 = itpSolver.createMarker(); + final ItpMarker I2 = itpSolver.createMarker(); + final ItpMarker I3 = itpSolver.createMarker(); + final ItpMarker I4 = itpSolver.createMarker(); + final ItpMarker I5 = itpSolver.createMarker(); + final ItpPattern pattern = itpSolver.createTreePattern( + Tree(I3, Subtree(I1, Leaf(I4), Leaf(I5)), Leaf(I2))); + + itpSolver.add(I1, Eq(a, Int(0))); + itpSolver.add(I2, Eq(a, b)); + itpSolver.add(I3, Eq(c, d)); + itpSolver.add(I4, Eq(d, Int(1))); + itpSolver.add(I5, Eq(b, c)); + + itpSolver.check(); + Assert.assertEquals(SolverStatus.UNSAT, itpSolver.getStatus()); + final Interpolant itp = itpSolver.getInterpolant(pattern); + + System.out.println(itp.eval(I1)); + System.out.println(itp.eval(I2)); + System.out.println(itp.eval(I3)); + System.out.println(itp.eval(I4)); + System.out.println(itp.eval(I5)); + System.out.println("----------"); + } + + @Test + public void testLIA() { + assumeFalse(solver == Solvers.CVC5); + + final ItpMarker A = itpSolver.createMarker(); + final ItpMarker B = itpSolver.createMarker(); + final ItpPattern pattern = itpSolver.createBinPattern(A, B); + + itpSolver.add(A, Eq(b, Mul(ImmutableList.of(Int(2), a)))); + itpSolver.add(B, Eq(b, Add(ImmutableList.of(Mul(ImmutableList.of(Int(2), c)), Int(1))))); + + itpSolver.check(); + Assert.assertEquals(SolverStatus.UNSAT, itpSolver.getStatus()); + final Interpolant itp = itpSolver.getInterpolant(pattern); + + System.out.println(itp.eval(A)); + System.out.println("----------"); + } + + @Test + public void testQuantifiers() { + assumeFalse(solver == Solvers.SMTINTERPOL); + assumeFalse(solver == Solvers.CVC5); + + final ItpMarker A = itpSolver.createMarker(); + final ItpMarker B = itpSolver.createMarker(); + final ItpPattern pattern = itpSolver.createBinPattern(A, B); + + final ConstDecl id = Const("i", Int()); + final ConstDecl> pd = Const("p", Func(Int(), Bool())); + final ConstDecl> qd = Const("q", Func(Int(), Bool())); + final ParamDecl x1d = Param("x", Int()); + final ParamDecl x2d = Param("x", Int()); + + final Expr i = id.getRef(); + final Expr> p = pd.getRef(); + final Expr> q = qd.getRef(); + final Expr x1 = x1d.getRef(); + final Expr x2 = x2d.getRef(); + + itpSolver.add(A, Forall(ImmutableList.of(x1d), Imply(App(q, x1), App(p, x1)))); + itpSolver.add(A, Forall(ImmutableList.of(x2d), Not(App(p, x2)))); + itpSolver.add(B, App(q, i)); + + itpSolver.check(); + Assert.assertEquals(SolverStatus.UNSAT, itpSolver.getStatus()); + final Interpolant itp = itpSolver.getInterpolant(pattern); + + System.out.println(itp.eval(A)); + System.out.println("----------"); + } + + @Test + public void testPushPop() { + final ItpMarker A = itpSolver.createMarker(); + final ItpMarker B = itpSolver.createMarker(); + final ItpPattern pattern = itpSolver.createBinPattern(A, B); + + itpSolver.add(A, Eq(a, b)); + itpSolver.add(B, Eq(b, c)); + + itpSolver.push(); + + itpSolver.add(A, Neq(a, c)); + itpSolver.check(); + Assert.assertEquals(SolverStatus.UNSAT, itpSolver.getStatus()); + + itpSolver.pop(); + + itpSolver.add(B, Neq(a, c)); + itpSolver.check(); + Assert.assertEquals(SolverStatus.UNSAT, itpSolver.getStatus()); + final Interpolant itp = itpSolver.getInterpolant(pattern); + + System.out.println(itp.eval(A)); + System.out.println("----------"); + } + +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverArrayTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverArrayTest.java new file mode 100644 index 0000000000..4d7c433e92 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverArrayTest.java @@ -0,0 +1,81 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.utils.ArrayTestUtils; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.Collection; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertTrue; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class JavaSMTSolverArrayTest { + + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameters(name = "expected: {1}, actual: {2}") + public static Collection operations() { + return ArrayTestUtils.BasicOperations(); + } + + @Test + public void testOperationEquals() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + final Solver solver = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver(); + solver.push(); + + solver.add(EqExpr.create2(expected, actual)); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverBVTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverBVTest.java new file mode 100644 index 0000000000..936a5943d1 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverBVTest.java @@ -0,0 +1,90 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.utils.BvTestUtils; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.Collection; +import java.util.stream.Collectors; +import java.util.stream.Stream; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertTrue; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class JavaSMTSolverBVTest { + + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameters(name = "expected: {1}, actual: {2}") + public static Collection operations() { + return Stream.concat( + BvTestUtils.BasicOperations().stream(), + Stream.concat( + BvTestUtils.BitvectorOperations().stream(), + BvTestUtils.RelationalOperations().stream() + ) + ) + .collect(Collectors.toUnmodifiableList()); + } + + @Test + public void testOperationEquals() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + final Solver solver = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver(); + solver.push(); + + solver.add(EqExpr.create2(expected, actual)); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverBooleanTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverBooleanTest.java new file mode 100644 index 0000000000..014792fc3c --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverBooleanTest.java @@ -0,0 +1,81 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.utils.BoolTestUtils; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.Collection; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertTrue; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class JavaSMTSolverBooleanTest { + + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameters(name = "expected: {1}, actual: {2}") + public static Collection operations() { + return BoolTestUtils.BasicOperations(); + } + + @Test + public void testOperationEquals() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + final Solver solver = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver(); + solver.push(); + + solver.add(EqExpr.create2(expected, actual)); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFPTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFPTest.java new file mode 100644 index 0000000000..a64cefbd2c --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverFPTest.java @@ -0,0 +1,110 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.type.fptype.FpLeqExpr; +import hu.bme.mit.theta.core.type.fptype.FpLitExpr; +import hu.bme.mit.theta.core.type.fptype.FpType; +import hu.bme.mit.theta.core.utils.FpTestUtils; +import hu.bme.mit.theta.core.utils.FpUtils; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.kframework.mpfr.BigFloat; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.Collection; +import java.util.stream.Collectors; + +import static hu.bme.mit.theta.core.type.fptype.FpExprs.Abs; +import static hu.bme.mit.theta.core.type.fptype.FpExprs.IsNan; +import static hu.bme.mit.theta.core.type.fptype.FpExprs.Leq; +import static hu.bme.mit.theta.core.type.fptype.FpExprs.Sub; +import static hu.bme.mit.theta.core.type.fptype.FpRoundingMode.RNE; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertTrue; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class JavaSMTSolverFPTest { + + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameters(name = "expected: {1}, actual: {2}") + public static Collection operations() { + return FpTestUtils.GetOperations() + .collect(Collectors.toUnmodifiableList()); + } + + @Test + public void testOperationEquals() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + final Solver solver = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver(); + solver.push(); + + if (expected instanceof FpLitExpr && actual.getType() instanceof FpType) { + if (((FpLitExpr) expected).isNaN()) { + //noinspection unchecked + solver.add(IsNan((Expr) actual)); + } else if (((FpLitExpr) expected).isNegativeInfinity()) { + solver.add(EqExpr.create2(expected, actual)); + } else if (((FpLitExpr) expected).isPositiveInfinity()) { + solver.add(EqExpr.create2(expected, actual)); + } else { + //noinspection unchecked + FpLeqExpr leq = Leq(Abs(Sub(RNE, (FpLitExpr) expected, (Expr) actual)), + FpUtils.bigFloatToFpLitExpr(new BigFloat("1e-2", + FpUtils.getMathContext((FpType) actual.getType(), RNE)), + (FpType) actual.getType())); + solver.add(leq); + } + } else { + solver.add(EqExpr.create2(expected, actual)); + } + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverIntTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverIntTest.java new file mode 100644 index 0000000000..4a79168fce --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverIntTest.java @@ -0,0 +1,81 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.utils.IntTestUtils; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.Collection; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertTrue; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class JavaSMTSolverIntTest { + + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameters(name = "expected: {1}, actual: {2}") + public static Collection operations() { + return IntTestUtils.BasicOperations(); + } + + @Test + public void testOperationEquals() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + final Solver solver = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver(); + solver.push(); + + solver.add(EqExpr.create2(expected, actual)); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverRatTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverRatTest.java new file mode 100644 index 0000000000..1566a81a34 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverRatTest.java @@ -0,0 +1,81 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.abstracttype.EqExpr; +import hu.bme.mit.theta.core.utils.RatTestUtils; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.Collection; + +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertTrue; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class JavaSMTSolverRatTest { + + @Parameterized.Parameter(0) + public Class exprType; + + @Parameterized.Parameter(1) + public Expr expected; + + @Parameterized.Parameter(2) + public Expr actual; + + @Parameters(name = "expected: {1}, actual: {2}") + public static Collection operations() { + return RatTestUtils.BasicOperations(); + } + + @Test + public void testOperationEquals() { + // Sanity check + assertNotNull(exprType); + assertNotNull(expected); + assertNotNull(actual); + + // Type checks + assertTrue( + "The type of actual is " + actual.getClass().getName() + " instead of " + + exprType.getName(), + exprType.isInstance(actual) + ); + assertEquals( + "The type of expected (" + expected.getType() + ") must match the type of actual (" + + actual.getType() + ")", + expected.getType(), + actual.getType() + ); + + // Equality check + final Solver solver = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver(); + solver.push(); + + solver.add(EqExpr.create2(expected, actual)); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverTest.java new file mode 100644 index 0000000000..1ffd955015 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTSolverTest.java @@ -0,0 +1,491 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.common.OsHelper; +import hu.bme.mit.theta.common.OsHelper.OperatingSystem; +import hu.bme.mit.theta.common.Tuple2; +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.decl.ParamDecl; +import hu.bme.mit.theta.core.model.ImmutableValuation; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.LitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayExprs; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayType; +import hu.bme.mit.theta.core.type.booltype.BoolExprs; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.bvtype.BvExprs; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.functype.FuncType; +import hu.bme.mit.theta.core.type.inttype.IntEqExpr; +import hu.bme.mit.theta.core.type.inttype.IntExprs; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.solver.Solver; +import hu.bme.mit.theta.solver.SolverStatus; +import hu.bme.mit.theta.solver.UCSolver; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameters; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; + +import java.util.ArrayList; +import java.util.Arrays; +import java.util.Collection; +import java.util.List; +import java.util.Optional; + +import static com.google.common.collect.ImmutableList.of; +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.decl.Decls.Param; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Array; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.ArrayInit; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Read; +import static hu.bme.mit.theta.core.type.arraytype.ArrayExprs.Write; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.True; +import static hu.bme.mit.theta.core.type.bvtype.BvExprs.Bv; +import static hu.bme.mit.theta.core.type.bvtype.BvExprs.BvType; +import static hu.bme.mit.theta.core.type.functype.FuncExprs.App; +import static hu.bme.mit.theta.core.type.functype.FuncExprs.Func; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Add; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assert.assertTrue; + +@RunWith(Parameterized.class) +public final class JavaSMTSolverTest { + + + @Parameterized.Parameter(0) + public Solvers solvers; + + @Parameterized.Parameter(1) + public Solver solver; + + @Parameters(name = "solver: {0}") + public static Collection operations() { + if (OsHelper.getOs().equals(OperatingSystem.LINUX)) { + return Arrays.asList(new Object[][]{ + {Solvers.Z3, JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver()}, + {Solvers.CVC5, JavaSMTSolverFactory.create(Solvers.CVC5, new String[]{}).createSolver()}, + {Solvers.PRINCESS, JavaSMTSolverFactory.create(Solvers.PRINCESS, new String[]{}).createSolver()}, + }); + } else { + return Arrays.asList(new Object[][]{ + {Solvers.Z3, JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createSolver()}, + {Solvers.PRINCESS, JavaSMTSolverFactory.create(Solvers.PRINCESS, new String[]{}).createSolver()}, + }); + } + } + + @Test + public void testSimple() { + // Create two integer constants x and y + final ConstDecl cx = Const("x", Int()); + final ConstDecl cy = Const("y", Int()); + + // Add x == y + 1 to the solver + solver.add(Eq(cx.getRef(), Add(cy.getRef(), Int(1)))); + + // Check, the expression should be satisfiable + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + // Add x < y to the solver + solver.add(IntExprs.Lt(cx.getRef(), cy.getRef())); + + // Check, the expression should be unsatisfiable + status = solver.check(); + assertTrue(status.isUnsat()); + } + + @Test + public void testTrack() { + final UCSolver solver = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}).createUCSolver(); + final ConstDecl ca = Const("a", BoolExprs.Bool()); + final Expr expr = BoolExprs.And(ca.getRef(), True()); + + solver.push(); + solver.track(expr); + + final SolverStatus status = solver.check(); + + assertTrue(status.isSat()); + + final Valuation model = solver.getModel(); + + assertNotNull(model); + + solver.pop(); + } + + // @Test + public void testFunc() { + // Arrange + final ConstDecl> ca = Const("a", Func(Int(), Int())); + final Expr> a = ca.getRef(); + final ParamDecl px = Param("x", Int()); + final Expr x = px.getRef(); + + solver.add(BoolExprs.Forall(of(px), + BoolExprs.Imply(IntExprs.Leq(x, Int(0)), Eq(App(a, x), Int(0))))); + solver.add(BoolExprs.Forall(of(px), + BoolExprs.Imply(IntExprs.Geq(x, Int(1)), Eq(App(a, x), Int(1))))); + + // Act + final SolverStatus status = solver.check(); + assertTrue(status.isSat()); + final Valuation model = solver.getModel(); + final Optional>> optVal = model.eval(ca); + final Expr> val = optVal.get(); + + // Assert + assertEquals(ca.getType(), val.getType()); + } + + //@Test + public void testArray() { + final ConstDecl> arr = Const("arr", Array(Int(), Int())); + + solver.add(ArrayExprs.Eq(Write(arr.getRef(), Int(0), Int(1)), arr.getRef())); + solver.add(ArrayExprs.Eq(Write(arr.getRef(), Int(1), Int(2)), arr.getRef())); + + // Check, the expression should be satisfiable + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation valuation = solver.getModel(); + final Optional>> optVal = valuation.eval(arr); + final Expr> val = optVal.get(); + assertTrue(val instanceof ArrayLitExpr); + var valLit = (ArrayLitExpr) val; + assertEquals(2, valLit.getElements().size()); + assertEquals(Int(1), Read(valLit, Int(0)).eval(ImmutableValuation.empty())); + assertEquals(Int(2), Read(valLit, Int(1)).eval(ImmutableValuation.empty())); + } + + //@Test + public void testArrayInit() { + final ConstDecl> arr = Const("arr", Array(Int(), Int())); + var elems = new ArrayList, Expr>>(); + ConstDecl noname = Const("noname", Int()); + elems.add(Tuple2.of(Int(0), Int(1))); + elems.add(Tuple2.of(Int(1), Int(2))); + elems.add(Tuple2.of(Int(2), Add(noname.getRef(), Int(3)))); + var initarr = ArrayInit(elems, Int(100), Array(Int(), Int())); + + solver.add(ArrayExprs.Eq(arr.getRef(), initarr)); + + // Check, the expression should be satisfiable + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + solver.add(Eq(noname.getRef(), Int(1))); + status = solver.check(); + assertTrue(status.isSat()); + + Valuation valuation = solver.getModel(); + final Optional>> optVal = valuation.eval(arr); + assertTrue(optVal.isPresent()); + final Expr> val = optVal.get(); + assertTrue(val instanceof ArrayLitExpr); + var valLit = (ArrayLitExpr) val; + assertEquals(Int(1), Read(valLit, Int(0)).eval(ImmutableValuation.empty())); + assertEquals(Int(2), Read(valLit, Int(1)).eval(ImmutableValuation.empty())); + assertEquals(Int(4), Read(valLit, Int(2)).eval(ImmutableValuation.empty())); + } + + // @Test + public void testReset() { + final ConstDecl cx = Const("x", Int()); + final ConstDecl cy = Const("y", Int()); + + IntEqExpr eqExpr = Eq(cx.getRef(), Add(cy.getRef(), Int(1))); + solver.add(eqExpr); + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + solver.add(IntExprs.Lt(cx.getRef(), cy.getRef())); + status = solver.check(); + assertTrue(status.isUnsat()); + + solver.reset(); + assertEquals(0, solver.getAssertions().size()); + + solver.add(eqExpr); + status = solver.check(); + assertTrue(status.isSat()); + } + + // @Test(expected = IllegalArgumentException.class) + public void testResetStack() { + solver.push(); + solver.push(); + solver.pop(); + solver.reset(); + solver.pop(); + } + + @Test + public void testBV1() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cx.getRef(), Bv(new boolean[]{false, false, true, false}))); + solver.add(BvExprs.Eq(cy.getRef(), Bv(new boolean[]{false, false, true, false}))); + solver.add(BvExprs.Eq(cx.getRef(), cy.getRef())); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + solver.pop(); + } + + @Test + public void testBV2() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cz = Const("z", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cx.getRef(), Bv(new boolean[]{false, false, false, false}))); + solver.add(BvExprs.Neq(cx.getRef(), cz.getRef())); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV3() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cx.getRef(), Bv(new boolean[]{false, false, false, false}))); + solver.add(BvExprs.Eq(cy.getRef(), + BvExprs.Add(List.of(cx.getRef(), Bv(new boolean[]{false, false, false, true}))))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV4() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cx.getRef(), Bv(new boolean[]{false, false, true, false}))); + solver.add(BvExprs.Eq(cy.getRef(), + BvExprs.Sub(cx.getRef(), Bv(new boolean[]{false, false, false, true})))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV5() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cx.getRef(), Bv(new boolean[]{false, false, true, false}))); + solver.add(BvExprs.Eq(cy.getRef(), BvExprs.Neg(cx.getRef()))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV6() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cx.getRef(), Bv(new boolean[]{false, false, true, false}))); + solver.add(BvExprs.Eq(cy.getRef(), + BvExprs.Mul(List.of(cx.getRef(), Bv(new boolean[]{false, false, true, false}))))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV7() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.ULt(cx.getRef(), Bv(new boolean[]{true, true, true, true}))); + solver.add(BvExprs.ULt(cy.getRef(), Bv(new boolean[]{true, true, true, true}))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV8() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cx.getRef(), Bv(new boolean[]{true, false, true, false}))); + solver.add(BvExprs.Eq(cy.getRef(), + BvExprs.SMod(cx.getRef(), Bv(new boolean[]{false, true, false, false})))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV9() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cy.getRef(), Bv(new boolean[]{false, true, false, false}))); + solver.add(BvExprs.Eq(BvExprs.Or(List.of(cx.getRef(), cy.getRef())), + Bv(new boolean[]{true, true, false, false}))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV10() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cy.getRef(), Bv(new boolean[]{false, true, false, false}))); + solver.add(BvExprs.Eq(BvExprs.And(List.of(cx.getRef(), cy.getRef())), + Bv(new boolean[]{false, true, false, false}))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV11() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cy.getRef(), Bv(new boolean[]{false, true, false, false}))); + solver.add(BvExprs.Eq(BvExprs.Xor(List.of(cx.getRef(), cy.getRef())), + Bv(new boolean[]{false, true, false, false}))); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } + + @Test + public void testBV12() { + final ConstDecl cx = Const("x", BvType(4)); + final ConstDecl cy = Const("y", BvType(4)); + + solver.push(); + + solver.add(BvExprs.Eq(cy.getRef(), Bv(new boolean[]{false, true, false, false}))); + solver.add(BvExprs.Eq( + BvExprs.ArithShiftRight(cy.getRef(), Bv(new boolean[]{false, false, false, true})), + cx.getRef())); + + SolverStatus status = solver.check(); + assertTrue(status.isSat()); + + Valuation model = solver.getModel(); + assertNotNull(model); + assertNotNull(model.toMap()); + + solver.pop(); + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformerTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformerTest.java new file mode 100644 index 0000000000..74a46f5b8f --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTTransformerTest.java @@ -0,0 +1,131 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import com.google.common.collect.Sets; +import hu.bme.mit.theta.common.OsHelper; +import hu.bme.mit.theta.common.OsHelper.OperatingSystem; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.Type; +import hu.bme.mit.theta.core.type.arraytype.ArrayInitExpr; +import hu.bme.mit.theta.core.type.arraytype.ArrayLitExpr; +import hu.bme.mit.theta.core.type.booltype.QuantifiedExpr; +import hu.bme.mit.theta.core.type.bvtype.BvType; +import hu.bme.mit.theta.core.type.fptype.FpType; +import hu.bme.mit.theta.core.type.functype.FuncType; +import hu.bme.mit.theta.core.type.rattype.RatType; +import hu.bme.mit.theta.core.utils.ExpressionUtils; +import org.junit.Assert; +import org.junit.Test; +import org.junit.runner.RunWith; +import org.junit.runners.Parameterized; +import org.junit.runners.Parameterized.Parameter; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.log.BasicLogManager; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.SolverContext; + +import java.util.Collection; +import java.util.Set; +import java.util.function.Predicate; +import java.util.stream.Collectors; + +import static hu.bme.mit.theta.core.type.abstracttype.AbstractExprs.Eq; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; +import static org.junit.Assert.assertNotNull; +import static org.junit.Assume.assumeFalse; +import static org.junit.runners.Parameterized.Parameters; + +@RunWith(Parameterized.class) +public class JavaSMTTransformerTest { + + @Parameter(0) + public Expr expr; + + @Parameter(1) + public Solvers solver; + + @Parameters(name = "expr: {0}, solver: {1}") + public static Collection operations() { + final Set solvers; + if (OsHelper.getOs().equals(OperatingSystem.LINUX)) { + solvers = Set.of(Solvers.Z3, Solvers.SMTINTERPOL, Solvers.CVC5, Solvers.PRINCESS); + } else { + solvers = Set.of(Solvers.Z3, Solvers.SMTINTERPOL, Solvers.PRINCESS); + } + + return Sets.cartesianProduct( + ExpressionUtils.AllExpressions().values().stream() + .collect(Collectors.toSet()), + solvers).stream() + .map(objects -> new Object[]{objects.get(0), objects.get(1)}).toList(); + } + + + private static boolean hasType(Expr expr, Predicate pred) { + if (pred.test(expr.getType())) return true; + return expr.getOps().stream().anyMatch((op) -> hasType(op, pred)); + } + + private static boolean hasExpr(Expr expr, Predicate> pred) { + if (pred.test(expr)) return true; + return expr.getOps().stream().anyMatch((op) -> hasExpr(op, pred)); + } + + @Test + public void testRoundtripTransformer() throws Exception { + // Sanity check + assertNotNull(expr); + assumeFalse(solver == Solvers.CVC5 && hasType(expr, type -> type instanceof FpType && !Set.of(32, 64).contains(((FpType) type).getSignificand() + ((FpType) type).getExponent()))); + assumeFalse(solver == Solvers.PRINCESS && hasType(expr, type -> type instanceof FpType || type instanceof RatType)); + assumeFalse(solver == Solvers.SMTINTERPOL && (hasType(expr, type -> type instanceof BvType || type instanceof FpType) || expr instanceof QuantifiedExpr)); + assumeFalse(solver == Solvers.SMTINTERPOL && (hasType(expr, type -> type instanceof BvType || type instanceof FpType) || expr instanceof QuantifiedExpr)); + assumeFalse((solver == Solvers.SMTINTERPOL || solver == Solvers.PRINCESS) && hasExpr(expr, e -> e instanceof ArrayInitExpr || e instanceof ArrayLitExpr)); + + final JavaSMTSymbolTable javaSMTSymbolTable = new JavaSMTSymbolTable(); + final var config = Configuration.fromCmdLineArguments(new String[]{}); + final var logger = BasicLogManager.create(config); + final var shutdownManager = ShutdownManager.create(); + try (final SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdownManager.getNotifier(), Solvers.Z3)) { + final JavaSMTTransformationManager javaSMTExprTransformer = new JavaSMTTransformationManager(javaSMTSymbolTable, context); + final JavaSMTTermTransformer javaSMTTermTransformer = new JavaSMTTermTransformer(javaSMTSymbolTable, context); + + final var expTerm = javaSMTExprTransformer.toTerm(expr); + final var expExpr = javaSMTTermTransformer.toExpr(expTerm); + + try { + Assert.assertEquals(expr, expExpr); + } catch (AssertionError e) { + if (hasType(expr, type -> type instanceof FuncType)) { + throw e; // for functions, we don't want the solver to step in + } + try (final var solver = JavaSMTSolverFactory.create(this.solver, new String[]{}).createSolver()) { + solver.push(); + solver.add(Eq(expr, expExpr)); + Assert.assertTrue("(= %s %s) is unsat\n".formatted(expr, expExpr), solver.check().isSat()); + solver.pop(); + solver.push(); + solver.add(Not(Eq(expr, expExpr))); + Assert.assertTrue("(not (= %s %s)) is sat with model %s\n".formatted(expr, expExpr, solver.check().isSat() ? solver.getModel() : ""), solver.check().isUnsat()); + solver.pop(); + } + } + } + + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTUserPropagatorTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTUserPropagatorTest.java new file mode 100644 index 0000000000..6caab7dae6 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/JavaSMTUserPropagatorTest.java @@ -0,0 +1,140 @@ +/* + * 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. + */ + +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.functype.FuncAppExpr; +import hu.bme.mit.theta.core.type.functype.FuncType; +import hu.bme.mit.theta.core.type.inttype.IntLitExpr; +import hu.bme.mit.theta.core.type.inttype.IntType; +import org.junit.Test; + +import java.math.BigInteger; +import java.util.LinkedHashMap; +import java.util.List; +import java.util.Map; + +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Bool; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Not; +import static hu.bme.mit.theta.core.type.booltype.BoolExprs.Or; +import static hu.bme.mit.theta.core.type.functype.FuncExprs.App; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Eq; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Lt; +import static org.junit.Assert.assertEquals; +import static org.junit.Assert.assertTrue; +import static org.sosy_lab.java_smt.SolverContextFactory.Solvers.Z3; + +public class JavaSMTUserPropagatorTest { + + @Test + public void testUserPropagatorBool() throws Exception { + TestKnownValuePropagator testPropagator = new TestKnownValuePropagator(); + + try (final var solver = JavaSMTSolverFactory.create(Z3, new String[]{}).createSolverWithPropagators(testPropagator)) { + final var c1 = Const("x", Bool()); + final var c2 = Const("y", Bool()); + final var c3 = Const("z", Bool()); + final var expr1 = Or(c1.getRef(), c2.getRef(), c3.getRef()); + + testPropagator.registerExpression(c1.getRef(), false); + testPropagator.registerExpression(c2.getRef(), false); + + solver.add(expr1); + + solver.check(); + assertTrue("Should be SAT", solver.getStatus().isSat()); + } + } + + + @Test + public void testUserPropagatorFunc() throws Exception { + TestConsequencePropagator testPropagator = new TestConsequencePropagator(); + + try (final var solver = JavaSMTSolverFactory.create(Z3, new String[]{}).createSolverWithPropagators(testPropagator)) { + final var c1 = Const("x", Int()); + final var c2 = Const("y", Int()); + final var c3 = Const("z", Int()); + + final var sortFuncType = FuncType.of(Int(), FuncType.of(Int(), Bool())); + final var sortFunc = Const("sort", sortFuncType); + + final var expr1 = App(App(sortFunc.getRef(), c1.getRef()), c2.getRef()); + final var expr2 = App(App(sortFunc.getRef(), c2.getRef()), c3.getRef()); + + solver.add(expr1); + solver.add(expr2); + solver.add(Eq(c1.getRef(), Int(0))); + solver.add(Eq(c3.getRef(), Int(2))); + + testPropagator.registerExpression(expr1); + testPropagator.registerExpression(expr2); + + solver.check(); + assertTrue("Should be SAT", solver.getStatus().isSat()); + + final var model = solver.getModel(); + assertEquals("Should only be one.", BigInteger.ONE, ((IntLitExpr) model.eval(c2).get()).getValue()); + + solver.add(Not(Eq(c2.getRef(), Int(1)))); + solver.check(); + assertTrue("Should be UNSAT", solver.getStatus().isUnsat()); + } + } + + + private static class TestConsequencePropagator extends JavaSMTUserPropagator { + @Override + public void onKnownValue(Expr expr, boolean value) { + System.err.printf("%s := %s\n", expr, value); + FuncAppExpr appOuter = (FuncAppExpr) expr; + FuncAppExpr appInner = (FuncAppExpr) appOuter.getFunc(); + + final var consequence = Lt((Expr) appInner.getParam(), (Expr) appOuter.getParam()); + + if (value) { + System.err.printf("Consequence: %s\n", consequence); + propagateConsequence(List.of(expr), consequence); + } else { + System.err.printf("Consequence: %s\n", Not(consequence)); + propagateConsequence(List.of(expr), Not(consequence)); + } + } + } + + + private static class TestKnownValuePropagator extends JavaSMTUserPropagator { + + private final Map, Boolean> setExpressions = new LinkedHashMap<>(); + + @Override + public void onKnownValue(Expr expr, boolean value) { + System.err.printf("%s := %s\n", expr, value); + if (setExpressions.containsKey(expr) && value != setExpressions.get(expr)) { + propagateConflict(List.of(expr)); + } + } + + public void registerExpression(Expr expr, boolean value) { + setExpressions.put(expr, value); + this.registerExpression(expr); + } + } +} diff --git a/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/SolverUtilsTest.java b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/SolverUtilsTest.java new file mode 100644 index 0000000000..30dcbbd179 --- /dev/null +++ b/subprojects/solver/solver-javasmt/src/test/java/hu/bme/mit/theta/solver/javasmt/SolverUtilsTest.java @@ -0,0 +1,88 @@ +/* + * 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. + */ +package hu.bme.mit.theta.solver.javasmt; + +import hu.bme.mit.theta.core.decl.ConstDecl; +import hu.bme.mit.theta.core.model.Valuation; +import hu.bme.mit.theta.core.type.Expr; +import hu.bme.mit.theta.core.type.booltype.BoolLitExpr; +import hu.bme.mit.theta.core.type.booltype.BoolType; +import hu.bme.mit.theta.core.type.inttype.IntType; +import hu.bme.mit.theta.solver.SolverFactory; +import hu.bme.mit.theta.solver.utils.SolverUtils; +import org.junit.Assert; +import org.junit.Test; +import org.sosy_lab.common.ShutdownManager; +import org.sosy_lab.common.configuration.Configuration; +import org.sosy_lab.common.configuration.InvalidConfigurationException; +import org.sosy_lab.common.log.BasicLogManager; +import org.sosy_lab.common.log.LogManager; +import org.sosy_lab.java_smt.SolverContextFactory; +import org.sosy_lab.java_smt.SolverContextFactory.Solvers; +import org.sosy_lab.java_smt.api.Formula; +import org.sosy_lab.java_smt.api.FormulaType; +import org.sosy_lab.java_smt.api.SolverContext; +import org.sosy_lab.java_smt.api.visitors.DefaultFormulaVisitor; + +import java.math.BigInteger; +import java.util.stream.Stream; + +import static hu.bme.mit.theta.core.decl.Decls.Const; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Gt; +import static hu.bme.mit.theta.core.type.inttype.IntExprs.Int; + +public class SolverUtilsTest { + + @Test + public void testModels() { + // Arrange + final SolverFactory factory = JavaSMTSolverFactory.create(Solvers.Z3, new String[]{}); + + final ConstDecl cx = Const("x", Int()); + final ConstDecl cy = Const("y", Int()); + final Expr x = cx.getRef(); + final Expr y = cy.getRef(); + final Expr expr = Gt(x, y); + final Stream models = SolverUtils.models(factory, expr); + + // Act + models.limit(5).forEach(m -> Assert.assertTrue(((BoolLitExpr) (expr.eval(m))).getValue())); + } + + // https://github.com/sosy-lab/java-smt/issues/359 + // if this no longer fails, clean up the FpToFp mitigations in ExprTransformer + @Test + public void testBugreport() throws InvalidConfigurationException { + final Configuration config = Configuration.fromCmdLineArguments(new String[]{}); + final LogManager logger = BasicLogManager.create(config); + final ShutdownManager shutdownManager = ShutdownManager.create(); + final SolverContext context = SolverContextFactory.createSolverContext(config, logger, shutdownManager.getNotifier(), Solvers.Z3); + + final Formula term = context.getFormulaManager().getFloatingPointFormulaManager().fromIeeeBitvector( + context.getFormulaManager().getBitvectorFormulaManager().makeBitvector(16, BigInteger.ZERO), + FormulaType.getFloatingPointType(5, 10) + ); + + context.getFormulaManager().visit(term, new DefaultFormulaVisitor() { + @Override + protected Void visitDefault(Formula f) { + return null; + } + }); + + } + +} diff --git a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ExprTransformer.java b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ExprTransformer.java index 77ecf49394..45d1f60388 100644 --- a/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ExprTransformer.java +++ b/subprojects/solver/solver-z3-legacy/src/main/java/hu/bme/mit/theta/solver/z3legacy/Z3ExprTransformer.java @@ -1160,7 +1160,7 @@ private com.microsoft.z3legacy.Expr transformFpFromBv(final FpFromBvExpr expr) { final FPSort fpSort = context.mkFPSort(expr.getFpType().getExponent(), expr.getFpType().getSignificand()); return context.mkFPToFP(transformFpRoundingMode(expr.getRoundingMode()), val, fpSort, - expr.isSigned()); + expr.isSigned()); // TODO: is this OK? FP2FP when BV2FP is used? } private com.microsoft.z3legacy.Expr transformFpToBv(final FpToBvExpr expr) { diff --git a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java index 603ebca545..9893b19ff2 100644 --- a/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java +++ b/subprojects/solver/solver-z3/src/main/java/hu/bme/mit/theta/solver/z3/Z3ExprTransformer.java @@ -1160,7 +1160,7 @@ private com.microsoft.z3.Expr transformFpFromBv(final FpFromBvExpr expr) { final FPSort fpSort = context.mkFPSort(expr.getFpType().getExponent(), expr.getFpType().getSignificand()); return context.mkFPToFP(transformFpRoundingMode(expr.getRoundingMode()), val, fpSort, - expr.isSigned()); + expr.isSigned()); // TODO: is this OK? FP2FP when BV2FP is used? } private com.microsoft.z3.Expr transformFpToBv(final FpToBvExpr expr) { diff --git a/subprojects/xcfa/xcfa-cli/build.gradle.kts b/subprojects/xcfa/xcfa-cli/build.gradle.kts index a4a2e6db13..5e1c150d4c 100644 --- a/subprojects/xcfa/xcfa-cli/build.gradle.kts +++ b/subprojects/xcfa/xcfa-cli/build.gradle.kts @@ -29,8 +29,10 @@ dependencies { implementation(project(":theta-xcfa")) implementation(project(":theta-xcfa-analysis")) implementation(project(":theta-c2xcfa")) + implementation(project(":theta-solver-z3")) implementation(project(":theta-solver-z3-legacy")) implementation(project(":theta-solver-smtlib")) + implementation(project(":theta-solver-javasmt")) implementation(project(":theta-solver")) implementation(project(":theta-c-frontend")) implementation(project(":theta-grammar")) diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt index aca4d46ef1..1cb4db021c 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/params/ExitCodes.kt @@ -19,6 +19,7 @@ package hu.bme.mit.theta.xcfa.cli.params import com.microsoft.z3.Z3Exception import hu.bme.mit.theta.common.exception.NotSolvableException import hu.bme.mit.theta.solver.UnknownSolverStatusException +import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverException import hu.bme.mit.theta.solver.smtlib.solver.SmtLibSolverException import hu.bme.mit.theta.solver.validator.SolverValidationException import kotlin.system.exitProcess @@ -58,6 +59,9 @@ fun exitOnError(stacktrace: Boolean, debug: Boolean, body: () -> T): T { } catch (e: SmtLibSolverException) { e.printCauseAndTrace(stacktrace) exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code) + } catch (e: JavaSMTSolverException) { + e.printCauseAndTrace(stacktrace) + exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code) } catch (e: SolverValidationException) { e.printCauseAndTrace(stacktrace) exitProcess(debug, e, ExitCodes.SOLVER_ERROR.code); diff --git a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt index 63ab05a002..ed9ea1f99f 100644 --- a/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt +++ b/subprojects/xcfa/xcfa-cli/src/main/java/hu/bme/mit/theta/xcfa/cli/utils/SolverRegistration.kt @@ -20,6 +20,7 @@ import hu.bme.mit.theta.common.OsHelper import hu.bme.mit.theta.common.logging.Logger import hu.bme.mit.theta.solver.SolverFactory import hu.bme.mit.theta.solver.SolverManager +import hu.bme.mit.theta.solver.javasmt.JavaSMTSolverManager import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager import hu.bme.mit.theta.solver.validator.SolverValidatorWrapperFactory import hu.bme.mit.theta.solver.z3legacy.Z3SolverManager @@ -35,7 +36,11 @@ fun registerAllSolverManagers(home: String, logger: Logger) { SolverManager.closeAll() // register solver managers SolverManager.registerSolverManager(Z3SolverManager.create()) + logger.write(Logger.Level.INFO, "Registered Legacy-Z3 SolverManager\n") + SolverManager.registerSolverManager(hu.bme.mit.theta.solver.z3.Z3SolverManager.create()) logger.write(Logger.Level.INFO, "Registered Z3 SolverManager\n") + SolverManager.registerSolverManager(JavaSMTSolverManager.create()) + logger.write(Logger.Level.INFO, "Registered JavaSMT SolverManager\n") if (OsHelper.getOs() == OsHelper.OperatingSystem.LINUX) { val homePath = Path.of(home) val smtLibSolverManager: SmtLibSolverManager = SmtLibSolverManager.create(homePath, logger)