diff --git a/README.md b/README.md
index 0ed6cb8148..897dc66eaf 100644
--- a/README.md
+++ b/README.md
@@ -56,18 +56,19 @@ Only a few SMT solvers provide support for theories like Arrays, Floating Point,
Currently JavaSMT supports several SMT solvers (see [Getting Started](doc/Getting-started.md) for installation):
-| SMT Solver | Linux64 | Windows64 | MacOS | Description |
-| --- |:---:|:---:|:---:|:--- |
-| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | a fast solver for bitvector logic, misses formula introspection |
-| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | |
-| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | new! |
-| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | | |
-| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | | | new! |
-| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | based on MathSAT5, with support for optimization |
-| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
-| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
-| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | [soon](https://github.com/sosy-lab/java-smt/pull/215) | | |
-| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
+| SMT Solver | Linux64 | Windows64 | MacOS | Description |
+|-------------------------------------------------------------------------|:---:|:---:|:---:|:-----------------------------------------------------------------------------|
+| [Bitwuzla](https://boolector.github.io/) | :heavy_check_mark: | | | a fast solver for bitvector and floating-point logic, successor of Boolector |
+| [Boolector](https://boolector.github.io/) | :heavy_check_mark: | | | a fast solver for bitvector logic, misses formula introspection |
+| [CVC4](https://cvc4.github.io/) | :heavy_check_mark: | | | |
+| [CVC5](https://cvc5.github.io/) | :heavy_check_mark: | | | new! |
+| [MathSAT5](http://mathsat.fbk.eu/) | :heavy_check_mark: | :heavy_check_mark: | | |
+| [OpenSMT](https://verify.inf.usi.ch/opensmt) | :heavy_check_mark: | | | new! |
+| [OptiMathSAT](http://optimathsat.disi.unitn.it/) | :heavy_check_mark: | | | based on MathSAT5, with support for optimization |
+| [Princess](http://www.philipp.ruemmer.org/princess.shtml) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [SMTInterpol](https://ultimate.informatik.uni-freiburg.de/smtinterpol/) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | Java-based SMT solver |
+| [Yices2](https://yices.csl.sri.com/) | :heavy_check_mark: | [soon](https://github.com/sosy-lab/java-smt/pull/215) | | |
+| [Z3](https://github.com/Z3Prover/z3) | :heavy_check_mark: | :heavy_check_mark: | :heavy_check_mark: | mature and well-known solver |
The following features are supported (depending on the used SMT solver):
diff --git a/build.xml b/build.xml
index 2cb4a302ae..3a2d66ff2c 100644
--- a/build.xml
+++ b/build.xml
@@ -22,6 +22,7 @@ SPDX-License-Identifier: Apache-2.0
-
+
diff --git a/build/build-publish-solvers.xml b/build/build-publish-solvers.xml
index b88aea311f..994a64a8d9 100644
--- a/build/build-publish-solvers.xml
+++ b/build/build-publish-solvers.xml
@@ -11,8 +11,9 @@ SPDX-License-Identifier: Apache-2.0
-->
-
+
+
diff --git a/build/build-publish-solvers/build-jar-yices2.xml b/build/build-publish-solvers/build-jar-yices2.xml
index 1f9eaec4d2..9889600c47 100644
--- a/build/build-publish-solvers/build-jar-yices2.xml
+++ b/build/build-publish-solvers/build-jar-yices2.xml
@@ -25,7 +25,9 @@ SPDX-License-Identifier: Apache-2.0
-
+
+
+
diff --git a/build/build-publish-solvers/macros.xml b/build/build-publish-solvers/macros.xml
index f7145604d8..e21696ab47 100644
--- a/build/build-publish-solvers/macros.xml
+++ b/build/build-publish-solvers/macros.xml
@@ -32,9 +32,10 @@ SPDX-License-Identifier: Apache-2.0
-
+
+ message="Cannot publish without 'repository' dir, please run 'svn co https://svn.sosy-lab.org/software/ivy/repository/${ivy.organisation}/${ivy.module} repository/${ivy.organisation}/${ivy.module}'."/>
You now want to run
svn add repository/${ivy.organisation}/${ivy.module}/*-@{solverVersion}*
- svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version @{solverVersion} of @{solverName} Solver"
- to make the new version publicly available.
+ svn ci repository/${ivy.organisation}/${ivy.module} -m"publish version
+ @{solverVersion} of @{solverName} Solver"
+ to make the new version publicly available.
+
diff --git a/build/build-publish-solvers/solver-bitwuzla.xml b/build/build-publish-solvers/solver-bitwuzla.xml
new file mode 100644
index 0000000000..8673972f39
--- /dev/null
+++ b/build/build-publish-solvers/solver-bitwuzla.xml
@@ -0,0 +1,136 @@
+
+
+
+
+
+
+
+
+
+
+
+
+ Please specify the path to Bitwuzla with the flag -Dbitwuzla.path=/path/to/bitwuzla.
+ The path has to point to the root Bitwuzla folder, i.e.,
+ a checkout of the official git repositoy from 'https://github.com/bitwuzla/bitwuzla'.
+ Note that shell substitutions do not work and a full absolute path has to be specified.
+
+
+ The path is ${bitwuzla.path}
+
+
+
+ Please specify a custom revision with the flag -Dbitwuzla.customRev=XXX.
+ The custom revision has to be unique amongst the already known version
+ numbers from the ivy repository. The script will append the git revision.
+
+
+
+ Please specify the path to GMP with the flag -Dgmp.path=/path/to/gmp.
+ The path has to point to the root GMP folder with version equal to or larger than 6.1.
+ Note that shell substitutions do not work and a full absolute path has to be specified.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/build/build-publish-solvers/solver-boolector.xml b/build/build-publish-solvers/solver-boolector.xml
index 7238058e43..97652d1319 100644
--- a/build/build-publish-solvers/solver-boolector.xml
+++ b/build/build-publish-solvers/solver-boolector.xml
@@ -30,7 +30,8 @@ SPDX-License-Identifier: Apache-2.0
-
+
@@ -39,56 +40,65 @@ SPDX-License-Identifier: Apache-2.0
-
-
+
+
-
-
-
-
-
-
+
+
+
+
+
+
-
+
-
+
-
+
-
+
-
-
+
+
+
+
+
-
-
-
+
+
+
-
+ description="Publish Boolector binaries to Ivy repository.">
+
diff --git a/build/build-publish-solvers/solver-cvc4.xml b/build/build-publish-solvers/solver-cvc4.xml
index 29a671396c..95c3ca349b 100644
--- a/build/build-publish-solvers/solver-cvc4.xml
+++ b/build/build-publish-solvers/solver-cvc4.xml
@@ -49,43 +49,54 @@ SPDX-License-Identifier: Apache-2.0
-
+
-
+
-
+
-
+
-
-
+
+
+
+
+
-
-
-
+
+
+
+
+
+
+
+
-
-
-
+
+
+
-
+ description="Publish CVC4 binaries to Ivy repository.">
+
diff --git a/build/build-publish-solvers/solver-cvc5.xml b/build/build-publish-solvers/solver-cvc5.xml
index 430d78747f..bb1fe693cd 100644
--- a/build/build-publish-solvers/solver-cvc5.xml
+++ b/build/build-publish-solvers/solver-cvc5.xml
@@ -68,11 +68,12 @@ SPDX-License-Identifier: Apache-2.0
-
+
-
+
@@ -80,10 +81,13 @@ SPDX-License-Identifier: Apache-2.0
-
-
+
+
-
+
@@ -107,40 +111,57 @@ SPDX-License-Identifier: Apache-2.0
-
-
-
+
+
+
+
+
+
+
+
-
-
+
+
+
+
+
-
-
+
+
+
+
+
-
-
+
+
+
+
+
-
+
+
+
-
+
+
-
+ description="Publish CVC5 binaries to Ivy repository.">
+
diff --git a/build/build-publish-solvers/solver-mathsat.xml b/build/build-publish-solvers/solver-mathsat.xml
index cfabeb1b62..669925545d 100644
--- a/build/build-publish-solvers/solver-mathsat.xml
+++ b/build/build-publish-solvers/solver-mathsat.xml
@@ -30,54 +30,66 @@ SPDX-License-Identifier: Apache-2.0
-
-
+
+
-
-
-
+
+
+
-
+
-
-
-
-
-
-
-
+
+
+
+
+
+
+
-
+
Please specify the MathSAT5 version with the flag -Dmathsat.version=... .
-
-
-
+
+
+
-
+
+ description="Publish OptiMathSAT binaries to Ivy repo.">
Please specify the @{flag} version with the flag -Dmathsat.version=... .
-
+
-
+
diff --git a/build/build-publish-solvers/solver-opensmt.xml b/build/build-publish-solvers/solver-opensmt.xml
index 2b73ffa905..cb950ffeae 100644
--- a/build/build-publish-solvers/solver-opensmt.xml
+++ b/build/build-publish-solvers/solver-opensmt.xml
@@ -30,7 +30,8 @@ SPDX-License-Identifier: Apache-2.0
-
+
@@ -39,9 +40,9 @@ SPDX-License-Identifier: Apache-2.0
-
+
-
+
@@ -71,8 +72,8 @@ SPDX-License-Identifier: Apache-2.0
-
-
+
+
@@ -175,8 +176,8 @@ SPDX-License-Identifier: Apache-2.0
-
+ description="Publish OpenSMT binaries to Ivy repository.">
+
diff --git a/build/build-publish-solvers/solver-z3.xml b/build/build-publish-solvers/solver-z3.xml
index 1b5045aa81..15f991af2a 100644
--- a/build/build-publish-solvers/solver-z3.xml
+++ b/build/build-publish-solvers/solver-z3.xml
@@ -22,24 +22,32 @@ SPDX-License-Identifier: Apache-2.0
- Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin` directory).
- The path has to point to the root Z3 folder (i.e., the path is ending with '/bin') and can be relative or absolute.
+ Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin`
+ directory).
+ The path has to point to the root Z3 folder (i.e., the path is ending with '/bin') and
+ can be relative or absolute.
Note that shell substitutions do not work.
- Please provide all releases (Linux64, MacOS, and Windows64) together in the same root directory,
- e.g., copy the releases (especially the content of their `bin` directories) together into one directory.
+ Please provide all releases (Linux64, MacOS, and Windows64) together in the same root
+ directory,
+ e.g., copy the releases (especially the content of their `bin` directories) together
+ into one directory.
The only overlap between those releases is the JAR file, which should be equal anyway.
Additionally, make the Java sources available in this directory.
This can be done by:
- copying the content of sources-zip into the current directory (or vice versa)
- - executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required.
+ - executing `python scripts/mk_make.py --java` to generate all Java related files.
+ Executing `make` is not required.
-
+
-
+
+
+
libz3.so has missing SONAME property.
Please run 'patchelf --set-soname libz3.so ${z3.path}/libz3.so'.
@@ -59,40 +67,50 @@ SPDX-License-Identifier: Apache-2.0
- Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin` directory).
+ Please specify the path to Z3 with the flag -Dz3.path=/path/to/z3 (e.g. `bin`
+ directory).
The path has to point to the root Z3 folder and can be relative or absolute.
Note that shell substitutions do not work.
- Please provide all releases (Linux64, MacOS, and Windows64) together in the same root directory,
- e.g., copy the releases (especially the content of their `bin` directories) together into one directory.
+ Please provide all releases (Linux64, MacOS, and Windows64) together in the same root
+ directory,
+ e.g., copy the releases (especially the content of their `bin` directories) together
+ into one directory.
The only overlap between those releases is the JAR file, which should be equal anyway.
Additionally, make the Java sources available in this directory.
This can be done by:
- copying the content of sources-zip into the current directory (or vice versa)
- - executing `python scripts/mk_make.py --java` to generate all Java related files. Executing `make` is not required.
+ - executing `python scripts/mk_make.py --java` to generate all Java related files.
+ Executing `make` is not required.
- Option -Dz3.version=... not specified. Trying to determine z3.version from git repository. This will fail if git repository is not available.
+ Option -Dz3.version=... not specified. Trying to determine z3.version from git
+ repository. This will fail if git repository is not available.
+
-
+
-
+ description="Publish Z3 binaries to Ivy repo.">
+
-
-
-
-
+
+
+
+
-
+
@@ -107,15 +125,15 @@ SPDX-License-Identifier: Apache-2.0
+ destdir="${z3.javadoc.dir}"
+ classpathref="classpath"
+ locale="en_US"
+ encoding="utf-8"
+ windowtitle="${z3.project.name}"
+ failonerror="false"
+ failonwarning="false"
+ overview="doc/javadoc_overview.html"
+ >
@@ -131,7 +149,7 @@ SPDX-License-Identifier: Apache-2.0
-
+
diff --git a/build/build-publish-solvers/solvers-yices.xml b/build/build-publish-solvers/solvers-yices.xml
index 998d7ea78c..7131d32bbb 100644
--- a/build/build-publish-solvers/solvers-yices.xml
+++ b/build/build-publish-solvers/solvers-yices.xml
@@ -16,42 +16,47 @@ SPDX-License-Identifier: Apache-2.0
+ description="Compile Yices2 bindings">
-
-
-
-
-
-
-
-
-
+
+
+
+
+
+
+
+
+
+ description="Publish Yices2 binaries to Ivy repo.">
Please specify the Yices2 version with the flag -Dyices2.version=... .
-
+
-
+
-
+
+ description="Publish Java bindings for Yices2 to Ivy repo.">
-
+ message="Cannot publish version ${version}, only unmodified working copies may be published."/>
+
diff --git a/build/build-publish.xml b/build/build-publish.xml
index d71871ee2d..78799fd96b 100644
--- a/build/build-publish.xml
+++ b/build/build-publish.xml
@@ -25,8 +25,10 @@ SPDX-License-Identifier: Apache-2.0
+
- Java wrapper for SMT solvers like Z3, MathSAT5, SMTInterpol, Princess, CVC4, CVC5, Boolector, and Yices2.
+ Java wrapper for SMT solvers like Z3, MathSAT5, SMTInterpol, Princess, CVC4, CVC5,
+ Boolector, Yices2, and Bitwuzla.
@@ -41,6 +42,7 @@ SPDX-License-Identifier: Apache-2.0
+
@@ -159,15 +161,18 @@ SPDX-License-Identifier: Apache-2.0
-
+
+
-
+
+
+
+
+
+
+ Bitwuzla solver and JavaSMT JNI wrapper.
+ Bitwuzla is provided under the MIT License.
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
+
diff --git a/solvers_ivy_conf/ivy_javasmt_yices2.xml b/solvers_ivy_conf/ivy_javasmt_yices2.xml
index f338b3a2c3..351bbcd4ee 100644
--- a/solvers_ivy_conf/ivy_javasmt_yices2.xml
+++ b/solvers_ivy_conf/ivy_javasmt_yices2.xml
@@ -33,19 +33,23 @@ SPDX-License-Identifier: Apache-2.0
-
+
-
+
-
+
-
+
diff --git a/src/org/sosy_lab/java_smt/SolverContextFactory.java b/src/org/sosy_lab/java_smt/SolverContextFactory.java
index f5754b32ad..1f9e1387b6 100644
--- a/src/org/sosy_lab/java_smt/SolverContextFactory.java
+++ b/src/org/sosy_lab/java_smt/SolverContextFactory.java
@@ -29,6 +29,7 @@
import org.sosy_lab.java_smt.delegate.logging.LoggingSolverContext;
import org.sosy_lab.java_smt.delegate.statistics.StatisticsSolverContext;
import org.sosy_lab.java_smt.delegate.synchronize.SynchronizedSolverContext;
+import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaSolverContext;
import org.sosy_lab.java_smt.solvers.boolector.BoolectorSolverContext;
import org.sosy_lab.java_smt.solvers.cvc4.CVC4SolverContext;
import org.sosy_lab.java_smt.solvers.cvc5.CVC5SolverContext;
@@ -57,7 +58,8 @@ public enum Solvers {
BOOLECTOR,
CVC4,
CVC5,
- YICES2
+ YICES2,
+ BITWUZLA
}
@Option(secure = true, description = "Export solver queries in SmtLib format into a file.")
@@ -290,6 +292,10 @@ private SolverContext generateContext0(Solvers solverToCreate)
case BOOLECTOR:
return BoolectorSolverContext.create(config, shutdownNotifier, logfile, randomSeed, loader);
+ case BITWUZLA:
+ return BitwuzlaSolverContext.create(
+ config, shutdownNotifier, logfile, randomSeed, floatingPointRoundingMode, loader);
+
default:
throw new AssertionError("no solver selected");
}
diff --git a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
index b5ac3b1455..75f56bdb12 100644
--- a/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
+++ b/src/org/sosy_lab/java_smt/api/BasicProverEnvironment.java
@@ -197,7 +197,7 @@ interface AllSatCallback {
*
* @param propagator The (fresh) user propagator to register.
* @return {@code true}, if the user propagator was successfully registered. Most SMT solvers do
- * not support user propagators and hence return {@code false}.
+ * not support user propagators and hence return {@code false}.
*/
default boolean registerUserPropagator(UserPropagator propagator) {
return false;
diff --git a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java
index 48a3028de7..43d06203f9 100644
--- a/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java
+++ b/src/org/sosy_lab/java_smt/api/BitvectorFormulaManager.java
@@ -145,7 +145,7 @@ public interface BitvectorFormulaManager {
* the numerator itself. We refer to the SMTLIB standard for the division and modulo operators in
* BV theory.
*
- * @param numerator dividend
+ * @param numerator dividend
* @param denumerator divisor
*/
BitvectorFormula smodulo(BitvectorFormula numerator, BitvectorFormula denumerator);
diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java
index a04f835590..3f5a9c3946 100644
--- a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java
+++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java
@@ -27,13 +27,19 @@ public abstract class FloatingPointNumber {
public static final int DOUBLE_PRECISION_EXPONENT_SIZE = 11;
public static final int DOUBLE_PRECISION_MANTISSA_SIZE = 52;
- /** Whether the number is positive (TRUE) or negative (FALSE). */
+ /**
+ * Whether the number is positive (TRUE) or negative (FALSE).
+ */
public abstract boolean getSign();
- /** The exponent of the floating-point number, given as numeric value. */
+ /**
+ * The exponent of the floating-point number, given as numeric value.
+ */
public abstract BigInteger getExponent();
- /** The mantissa (aka significand) of the floating-point number, given as numeric value. */
+ /**
+ * The mantissa (aka significand) of the floating-point number, given as numeric value.
+ */
public abstract BigInteger getMantissa();
public abstract int getExponentSize();
@@ -78,7 +84,9 @@ private boolean isDoublePrecision() {
&& getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE;
}
- /** compute a representation as Java-based float value, if possible. */
+ /**
+ * compute a representation as Java-based float value, if possible.
+ */
public float floatValue() {
Preconditions.checkArgument(
isSinglePrecision(),
@@ -88,7 +96,9 @@ public float floatValue() {
return Float.intBitsToFloat(bits.length() == 0 ? 0 : (int) bits.toLongArray()[0]);
}
- /** compute a representation as Java-based double value, if possible. */
+ /**
+ * compute a representation as Java-based double value, if possible.
+ */
public double doubleValue() {
Preconditions.checkArgument(
isSinglePrecision() || isDoublePrecision(),
diff --git a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java
index c5932cd2eb..b69541dc81 100644
--- a/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java
+++ b/src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java
@@ -138,7 +138,9 @@ public enum FunctionDeclarationKind {
/** Unsigned remainder over bitvectors. */
BV_UREM,
- /** Signed modulo over bitvectors. */
+ /**
+ * Signed modulo over bitvectors.
+ */
BV_SMOD,
/** Multiplication over bitvectors. */
diff --git a/src/org/sosy_lab/java_smt/api/PropagatorBackend.java b/src/org/sosy_lab/java_smt/api/PropagatorBackend.java
index bbfa8f5d2c..7838d6ab09 100644
--- a/src/org/sosy_lab/java_smt/api/PropagatorBackend.java
+++ b/src/org/sosy_lab/java_smt/api/PropagatorBackend.java
@@ -47,7 +47,7 @@ public interface PropagatorBackend {
* generate a theory lemma.
*
* @param assignedExpressions A set of assigned expressions.
- * @param consequence The consequence implied by the assigned expressions.
+ * @param consequence The consequence implied by the assigned expressions.
*/
void propagateConsequence(BooleanFormula[] assignedExpressions, BooleanFormula consequence);
@@ -56,11 +56,11 @@ public interface PropagatorBackend {
* UserPropagator#onKnownValue}, will set the next decision to be made. If called during {@link
* UserPropagator#onDecision}, will overwrite the current decision to be made.
*
- * @param expr The expression to assign to next.
+ * @param expr The expression to assign to next.
* @param value The value to be assigned. If not given, the solver will decide.
* @return False, if the value of {@code expr} is already assigned. True, otherwise. Note that the
- * value of {@code expr} may already be decided before being reported via {@link
- * UserPropagator#onKnownValue}.
+ * value of {@code expr} may already be decided before being reported via {@link
+ * UserPropagator#onKnownValue}.
*/
boolean propagateNextDecision(BooleanFormula expr, Optional value);
diff --git a/src/org/sosy_lab/java_smt/api/UserPropagator.java b/src/org/sosy_lab/java_smt/api/UserPropagator.java
index 9765658d7d..eb7f71e54e 100644
--- a/src/org/sosy_lab/java_smt/api/UserPropagator.java
+++ b/src/org/sosy_lab/java_smt/api/UserPropagator.java
@@ -65,7 +65,7 @@ public interface UserPropagator {
*
Note: This callback is only invoked if the user propagator enabled it via {@link
* PropagatorBackend#notifyOnKnownValue()}.
*
- * @param expr The expressions whose value is known.
+ * @param expr The expressions whose value is known.
* @param value The value of the expression.
*/
void onKnownValue(BooleanFormula expr, boolean value);
@@ -78,7 +78,7 @@ public interface UserPropagator {
*
Note: This callback is only invoked if the user propagator enabled it via {@link
* PropagatorBackend#notifyOnDecision()}.
*
- * @param expr The expressions whose value gets decided (usually a literal).
+ * @param expr The expressions whose value gets decided (usually a literal).
* @param value The decision value.
*/
void onDecision(BooleanFormula expr, boolean value);
diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractUserPropagator.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractUserPropagator.java
index 84afa318f7..5a6941a2cd 100644
--- a/src/org/sosy_lab/java_smt/basicimpl/AbstractUserPropagator.java
+++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractUserPropagator.java
@@ -24,19 +24,24 @@ protected PropagatorBackend getBackend() {
}
@Override
- public void onPush() {}
+ public void onPush() {
+ }
@Override
- public void onPop(int numPoppedLevels) {}
+ public void onPop(int numPoppedLevels) {
+ }
@Override
- public void onFinalCheck() {}
+ public void onFinalCheck() {
+ }
@Override
- public void onKnownValue(BooleanFormula expr, boolean value) {}
+ public void onKnownValue(BooleanFormula expr, boolean value) {
+ }
@Override
- public void onDecision(BooleanFormula expr, boolean value) {}
+ public void onDecision(BooleanFormula expr, boolean value) {
+ }
@Override
public void initializeWithBackend(PropagatorBackend pBackend) {
diff --git a/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java b/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java
index 213f442065..bbd17b7cdc 100644
--- a/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java
+++ b/src/org/sosy_lab/java_smt/example/SimpleUserPropagator.java
@@ -29,10 +29,13 @@
import org.sosy_lab.java_smt.api.SolverException;
import org.sosy_lab.java_smt.basicimpl.AbstractUserPropagator;
-/** Example of a simple user propagator that prohibits variables/expressions to be set to true. */
+/**
+ * Example of a simple user propagator that prohibits variables/expressions to be set to true.
+ */
public class SimpleUserPropagator {
- private SimpleUserPropagator() {}
+ private SimpleUserPropagator() {
+ }
public static void main(String[] args)
throws InvalidConfigurationException, InterruptedException, SolverException {
@@ -41,7 +44,7 @@ public static void main(String[] args)
ShutdownNotifier notifier = ShutdownNotifier.createDummy();
try (SolverContext context =
- SolverContextFactory.createSolverContext(config, logger, notifier, Solvers.Z3)) {
+ SolverContextFactory.createSolverContext(config, logger, notifier, Solvers.Z3)) {
final BooleanFormulaManager bmgr = context.getFormulaManager().getBooleanFormulaManager();
testWithBlockedLiterals(context, bmgr, logger);
@@ -153,7 +156,9 @@ private static void testWithBlockedSubclauses(
}
}
- /** This user propagator will raise a conflict whenever a registered expression is set to true. */
+ /**
+ * This user propagator will raise a conflict whenever a registered expression is set to true.
+ */
private static class MyUserPropagator extends AbstractUserPropagator {
private final List disabledExpressions = new ArrayList<>();
@@ -178,7 +183,7 @@ public void onKnownValue(BooleanFormula expr, boolean value) {
logger.log(Level.INFO, "Solver assigned", expr, "to", value);
if (value && disabledExpressions.contains(expr)) {
logger.log(Level.INFO, "User propagator raised conflict on", expr);
- getBackend().propagateConflict(new BooleanFormula[] {expr});
+ getBackend().propagateConflict(new BooleanFormula[]{expr});
}
}
diff --git a/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueens.java b/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueens.java
index 93e5d0ed8c..4f2fc21f18 100644
--- a/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueens.java
+++ b/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueens.java
@@ -89,10 +89,10 @@ public static void main(String... args)
// this example uses Z3, because it is currently the only solver providing user propagation.
try (SolverContext context =
- SolverContextFactory.createSolverContext(config, logger, notifier, Solvers.Z3);
- ProverEnvironment prover =
- context.newProverEnvironment(
- ProverOptions.GENERATE_MODELS, ProverOptions.GENERATE_ALL_SAT)) {
+ SolverContextFactory.createSolverContext(config, logger, notifier, Solvers.Z3);
+ ProverEnvironment prover =
+ context.newProverEnvironment(
+ ProverOptions.GENERATE_MODELS, ProverOptions.GENERATE_ALL_SAT)) {
// parse input parameters
if (args == null || args.length != 2) {
@@ -150,7 +150,7 @@ public static void main(String... args)
* of size N x N.
*
* @return a 2D array of BooleanFormula objects, where each BooleanFormula object represents a
- * variable for a cell in the grid.
+ * variable for a cell in the grid.
*/
private BooleanFormula[][] getSymbols() {
final BooleanFormula[][] symbols = new BooleanFormula[n][n];
@@ -167,7 +167,7 @@ private BooleanFormula[][] getSymbols() {
* board.
*
* @param symbols a 2D Boolean array representing the board. Each element is true if there is a
- * queen in that cell, false otherwise.
+ * queen in that cell, false otherwise.
* @return a List of BooleanFormulas representing the rules for this constraint.
*/
private List rowRule1(BooleanFormula[][] symbols) {
@@ -196,7 +196,7 @@ private List rowRule1(BooleanFormula[][] symbols) {
*
We add a negation of the conjunction of all possible pairs of variables in each row.
*
* @param symbols a 2D array of BooleanFormula objects representing the variables for each cell on
- * the board.
+ * the board.
* @return a list of BooleanFormula objects representing the constraints added by this rule.
*/
private List rowRule2(BooleanFormula[][] symbols) {
@@ -225,7 +225,7 @@ private List rowRule2(BooleanFormula[][] symbols) {
*
We add a negation of the conjunction of all possible pairs of variables in each column.
*
* @param symbols a 2D array of BooleanFormula representing the placement of queens on the
- * chessboard
+ * chessboard
* @return a list of BooleanFormula objects representing the constraints added by this rule.
*/
private List columnRule(BooleanFormula[][] symbols) {
@@ -267,7 +267,7 @@ private List columnRule(BooleanFormula[][] symbols) {
*
*
* @param symbols a two-dimensional array of Boolean formulas representing the chessboard
- * configuration
+ * configuration
* @return a list of BooleanFormula objects representing the constraints added by this rule.
*/
private List diagonalRule(BooleanFormula[][] symbols) {
diff --git a/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueensConstraintPropagator.java b/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueensConstraintPropagator.java
index 329cdd9a17..2fc238aa7c 100644
--- a/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueensConstraintPropagator.java
+++ b/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/NQueensConstraintPropagator.java
@@ -61,7 +61,7 @@ public void onKnownValue(BooleanFormula var, boolean value) {
if (x1 == x2 || y1 == y2 || Math.abs(x1 - x2) == Math.abs(y1 - y2)) {
// We have two queens on the same row, same column, or same diagonal.
// This is not allowed, so we raise a conflict.
- getBackend().propagateConflict(new BooleanFormula[] {var, other});
+ getBackend().propagateConflict(new BooleanFormula[]{var, other});
}
}
}
diff --git a/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/package-info.java b/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/package-info.java
index e251ddf3a4..44a6aa4093 100644
--- a/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/package-info.java
+++ b/src/org/sosy_lab/java_smt/example/nqueens_user_propagator/package-info.java
@@ -6,5 +6,7 @@
//
// SPDX-License-Identifier: Unlicense OR Apache-2.0 OR MIT
-/** Some basic examples for using Java-SMT. */
+/**
+ * Some basic examples for using Java-SMT.
+ */
package org.sosy_lab.java_smt.example.nqueens_user_propagator;
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaArrayFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaArrayFormulaManager.java
new file mode 100644
index 0000000000..4e853ba93f
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaArrayFormulaManager.java
@@ -0,0 +1,52 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_EQUAL;
+
+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.basicimpl.AbstractArrayFormulaManager;
+
+public class BitwuzlaArrayFormulaManager
+ extends AbstractArrayFormulaManager {
+
+ protected BitwuzlaArrayFormulaManager(BitwuzlaFormulaCreator pCreator) {
+ super(pCreator);
+ }
+
+ @Override
+ protected Long select(Long pArray, Long pIndex) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_ARRAY_SELECT.swigValue(), pArray, pIndex);
+ }
+
+ @Override
+ protected Long store(Long pArray, Long pIndex, Long pValue) {
+ return BitwuzlaJNI.bitwuzla_mk_term3(
+ BitwuzlaKind.BITWUZLA_KIND_ARRAY_STORE.swigValue(), pArray, pIndex, pValue);
+ }
+
+ @Override
+ @SuppressWarnings("MethodTypeParameterName")
+ protected Long internalMakeArray(
+ String pName, FormulaType pIndexType, FormulaType pElementType) {
+ final ArrayFormulaType arrayFormulaType =
+ FormulaType.getArrayType(pIndexType, pElementType);
+ final long bitwuzlaArrayType = toSolverType(arrayFormulaType);
+ long newVar = getFormulaCreator().makeVariable(bitwuzlaArrayType, pName);
+ return newVar;
+ }
+
+ @Override
+ protected Long equivalence(Long pArray1, Long pArray2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_EQUAL.swigValue(), pArray1, pArray2);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java
new file mode 100644
index 0000000000..307157b2cb
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBitvectorFormulaManager.java
@@ -0,0 +1,207 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import java.math.BigInteger;
+import org.sosy_lab.java_smt.basicimpl.AbstractBitvectorFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class BitwuzlaBitvectorFormulaManager
+ extends AbstractBitvectorFormulaManager {
+
+ protected BitwuzlaBitvectorFormulaManager(
+ FormulaCreator pCreator,
+ AbstractBooleanFormulaManager pBmgr) {
+ super(pCreator, pBmgr);
+ }
+
+ @Override
+ protected Long makeBitvectorImpl(int length, Long pParam1) {
+ throw new UnsupportedOperationException("Bitwuzla does not support INT theory");
+ }
+
+ @Override
+ protected Long makeBitvectorImpl(int length, BigInteger pI) {
+ pI = transformValueToRange(length, pI);
+ long sort = BitwuzlaJNI.bitwuzla_mk_bv_sort(length);
+ return BitwuzlaJNI.bitwuzla_mk_bv_value(sort, pI.toString(), 10);
+ }
+
+ @Override
+ protected Long toIntegerFormulaImpl(Long pI, boolean signed) {
+ throw new UnsupportedOperationException("BV to INT conversion is not supported.");
+ }
+
+ @Override
+ protected Long negate(Long pParam1) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BitwuzlaKind.BITWUZLA_KIND_BV_NOT.swigValue(), pParam1);
+ }
+
+ @Override
+ protected Long add(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_ADD.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long subtract(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SUB.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long divide(Long pParam1, Long pParam2, boolean signed) {
+ if (signed) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SDIV.swigValue(), pParam1, pParam2);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_UDIV.swigValue(), pParam1, pParam2);
+ }
+ }
+
+ @Override
+ protected Long remainder(Long pParam1, Long pParam2, boolean signed) {
+ BitwuzlaKind kind =
+ signed ? BitwuzlaKind.BITWUZLA_KIND_BV_SREM : BitwuzlaKind.BITWUZLA_KIND_BV_UREM;
+ return BitwuzlaJNI.bitwuzla_mk_term2(kind.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long smodulo(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SMOD.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long multiply(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_MUL.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long equal(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_EQUAL.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long greaterThan(Long pParam1, Long pParam2, boolean signed) {
+ if (signed) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SGT.swigValue(), pParam1, pParam2);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_UGT.swigValue(), pParam1, pParam2);
+ }
+ }
+
+ @Override
+ protected Long greaterOrEquals(Long pParam1, Long pParam2, boolean signed) {
+ if (signed) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SGE.swigValue(), pParam1, pParam2);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_UGE.swigValue(), pParam1, pParam2);
+ }
+ }
+
+ @Override
+ protected Long lessThan(Long pParam1, Long pParam2, boolean signed) {
+ if (signed) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SLT.swigValue(), pParam1, pParam2);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_ULT.swigValue(), pParam1, pParam2);
+ }
+ }
+
+ @Override
+ protected Long lessOrEquals(Long pParam1, Long pParam2, boolean signed) {
+ if (signed) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SLE.swigValue(), pParam1, pParam2);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_ULE.swigValue(), pParam1, pParam2);
+ }
+ }
+
+ @Override
+ protected Long not(Long pParam1) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BitwuzlaKind.BITWUZLA_KIND_BV_NOT.swigValue(), pParam1);
+ }
+
+ @Override
+ protected Long and(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_AND.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long or(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_OR.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long xor(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_XOR.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long makeVariableImpl(int pLength, String pVar) {
+ long sort = BitwuzlaJNI.bitwuzla_mk_bv_sort(pLength);
+ return getFormulaCreator().makeVariable(sort, pVar);
+ }
+
+ @Override
+ protected Long shiftRight(Long pNumber, Long toShift, boolean signed) {
+ if (signed) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_ASHR.swigValue(), pNumber, toShift);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SHR.swigValue(), pNumber, toShift);
+ }
+ }
+
+ @Override
+ protected Long shiftLeft(Long pNumber, Long toShift) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SHL.swigValue(), pNumber, toShift);
+ }
+
+ @Override
+ protected Long concat(Long number, Long pAppend) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_CONCAT.swigValue(), number, pAppend);
+ }
+
+ @Override
+ protected Long extract(Long pNumber, int pMsb, int pLsb) {
+ return BitwuzlaJNI.bitwuzla_mk_term1_indexed2(
+ BitwuzlaKind.BITWUZLA_KIND_BV_EXTRACT.swigValue(), pNumber, pMsb, pLsb);
+ }
+
+ @Override
+ protected Long extend(Long pNumber, int pExtensionBits, boolean pSigned) {
+ if (pSigned) {
+ return BitwuzlaJNI.bitwuzla_mk_term1_indexed1(
+ BitwuzlaKind.BITWUZLA_KIND_BV_SIGN_EXTEND.swigValue(), pNumber, pExtensionBits);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term1_indexed1(
+ BitwuzlaKind.BITWUZLA_KIND_BV_ZERO_EXTEND.swigValue(), pNumber, pExtensionBits);
+ }
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBooleanFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBooleanFormulaManager.java
new file mode 100644
index 0000000000..cdaa9c96bd
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaBooleanFormulaManager.java
@@ -0,0 +1,126 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import org.sosy_lab.java_smt.basicimpl.AbstractBooleanFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class BitwuzlaBooleanFormulaManager
+ extends AbstractBooleanFormulaManager {
+ // private final long bitwuzla;
+ private final long pTrue;
+ private final long pFalse;
+
+ protected BitwuzlaBooleanFormulaManager(
+ FormulaCreator pCreator) {
+ super(pCreator);
+ // bitwuzla = getFormulaCreator().getEnv();
+ pTrue = BitwuzlaJNI.bitwuzla_mk_true();
+ pFalse = BitwuzlaJNI.bitwuzla_mk_false();
+ }
+
+ @Override
+ protected Long makeVariableImpl(String pVar) {
+ long boolType = getFormulaCreator().getBoolType();
+ return getFormulaCreator().makeVariable(boolType, pVar);
+ }
+
+ @Override
+ protected Long makeBooleanImpl(boolean value) {
+ return value ? pTrue : pFalse;
+ }
+
+ @Override
+ protected Long not(Long pParam1) {
+ if (isTrue(pParam1)) {
+ return pFalse;
+ } else if (isFalse(pParam1)) {
+ return pTrue;
+ }
+
+ if (BitwuzlaJNI.bitwuzla_term_get_kind(pParam1) == BitwuzlaKind.BITWUZLA_KIND_NOT.swigValue()) {
+ long[] size = new long[1];
+ long[] pChildren = BitwuzlaJNI.bitwuzla_term_get_children(pParam1, size);
+ return pChildren[0];
+ }
+ return BitwuzlaJNI.bitwuzla_mk_term1(BitwuzlaKind.BITWUZLA_KIND_NOT.swigValue(), pParam1);
+ }
+
+ @Override
+ protected Long and(Long pParam1, Long pParam2) {
+ if (isTrue(pParam1)) {
+ return pParam2;
+ } else if (isTrue(pParam2)) {
+ return pParam1;
+ } else if (isFalse(pParam1)) {
+ return pFalse;
+ } else if (isFalse(pParam2)) {
+ return pFalse;
+ } else if (pParam1.equals(pParam2)) {
+ return pParam1;
+ }
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_AND.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long or(Long pParam1, Long pParam2) {
+ if (isTrue(pParam1)) {
+ return pTrue;
+ } else if (isTrue(pParam2)) {
+ return pTrue;
+ } else if (isFalse(pParam1)) {
+ return pParam2;
+ } else if (isFalse(pParam2)) {
+ return pParam1;
+ } else if (pParam1.equals(pParam2)) {
+ return pParam1;
+ }
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_OR.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long xor(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_XOR.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long equivalence(Long bits1, Long bits2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BitwuzlaKind.BITWUZLA_KIND_IFF.swigValue(), bits1, bits2);
+ }
+
+ @Override
+ protected boolean isTrue(Long bits) {
+ return BitwuzlaJNI.bitwuzla_term_is_true(bits);
+ }
+
+ @Override
+ protected boolean isFalse(Long bits) {
+ return BitwuzlaJNI.bitwuzla_term_is_false(bits);
+ }
+
+ @Override
+ protected Long ifThenElse(Long pCond, Long pF1, Long pF2) {
+ if (isTrue(pCond)) {
+ return pF1;
+ } else if (isFalse(pCond)) {
+ return pF2;
+ } else if (pF1.equals(pF2)) {
+ return pF1;
+ } else if (isTrue(pF1) && isFalse(pF2)) {
+ return pCond;
+ } else if (isFalse(pF1) && isTrue(pF2)) {
+ return not(pCond);
+ }
+ return BitwuzlaJNI.bitwuzla_mk_term3(
+ BitwuzlaKind.BITWUZLA_KIND_ITE.swigValue(), pCond, pF1, pF2);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaDeclaration.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaDeclaration.java
new file mode 100644
index 0000000000..c93da123ac
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaDeclaration.java
@@ -0,0 +1,59 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import java.util.Objects;
+
+// Declarations sometimes need the info of a Term, but mostly those of Kinds.
+// We can not discern between the two however, hence this wrapper
+public class BitwuzlaDeclaration {
+ private final Long decl;
+
+ // If isKind, decl == KIND; else decl == term
+ private final boolean isKind;
+
+ BitwuzlaDeclaration(long pDecl, boolean pIsKind) {
+ decl = pDecl;
+ isKind = pIsKind;
+ }
+
+ public boolean isKind() {
+ return isKind;
+ }
+
+ public long getTerm() {
+ assert !isKind;
+ return decl;
+ }
+
+ public int getKind() {
+ assert isKind;
+ return decl.intValue();
+ }
+
+ @Override
+ public boolean equals(Object any) {
+ if (any == this) {
+ return true;
+ }
+ if (any instanceof BitwuzlaDeclaration) {
+ BitwuzlaDeclaration otherDecl = (BitwuzlaDeclaration) any;
+ if (this.isKind == otherDecl.isKind && Objects.equals(this.decl, otherDecl.decl)) {
+ return true;
+ }
+ }
+ return false;
+ }
+
+ @Override
+ public int hashCode() {
+ // Might be errorprone as term and kind might have the same hashcode but not be equal
+ return decl != null ? decl.hashCode() : 0;
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java
new file mode 100644
index 0000000000..7e0a2a92c1
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFloatingPointManager.java
@@ -0,0 +1,339 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_EQUAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_ABS;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_ADD;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_DIV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_EQUAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_GEQ;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_GT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_INF;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_NAN;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_NEG;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_NORMAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_SUBNORMAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_ZERO;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_LEQ;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_LT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_MAX;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_MIN;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_MUL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_NEG;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_RTI;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_SQRT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_SUB;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_BV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_FP;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_SBV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_UBV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_SBV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_UBV;
+
+import java.math.BigInteger;
+import org.sosy_lab.java_smt.api.FloatingPointRoundingMode;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType;
+import org.sosy_lab.java_smt.basicimpl.AbstractFloatingPointFormulaManager;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+
+public class BitwuzlaFloatingPointManager
+ extends AbstractFloatingPointFormulaManager {
+ // private final long bitwuzla;
+ private final long roundingMode;
+
+ protected BitwuzlaFloatingPointManager(
+ FormulaCreator pCreator,
+ FloatingPointRoundingMode pFloatingPointRoundingMode) {
+ super(pCreator);
+ // bitwuzla = pCreator.getEnv();
+ roundingMode = getRoundingModeImpl(pFloatingPointRoundingMode);
+ }
+
+ @Override
+ protected Long getDefaultRoundingMode() {
+ return roundingMode;
+ }
+
+ @Override
+ protected Long getRoundingModeImpl(FloatingPointRoundingMode pFloatingPointRoundingMode) {
+ long out;
+ switch (pFloatingPointRoundingMode) {
+ case NEAREST_TIES_TO_EVEN:
+ out = BitwuzlaJNI.bitwuzla_mk_rm_value(BitwuzlaJNI.BITWUZLA_RM_RNE_get());
+ break;
+ case NEAREST_TIES_AWAY:
+ out = BitwuzlaJNI.bitwuzla_mk_rm_value(BitwuzlaJNI.BITWUZLA_RM_RNA_get());
+ break;
+ case TOWARD_POSITIVE:
+ out = BitwuzlaJNI.bitwuzla_mk_rm_value(BitwuzlaJNI.BITWUZLA_RM_RTP_get());
+ break;
+ case TOWARD_NEGATIVE:
+ out = BitwuzlaJNI.bitwuzla_mk_rm_value(BitwuzlaJNI.BITWUZLA_RM_RTN_get());
+ break;
+ case TOWARD_ZERO:
+ out = BitwuzlaJNI.bitwuzla_mk_rm_value(BitwuzlaJNI.BITWUZLA_RM_RTZ_get());
+ break;
+ default:
+ throw new AssertionError("Unexpected value");
+ }
+ return out;
+ }
+
+ @Override
+ protected Long makeNumberImpl(double n, FloatingPointType type, Long pFloatingPointRoundingMode) {
+ if (Double.compare(n, -0.0) == 0) {
+ return BitwuzlaJNI.bitwuzla_mk_fp_neg_zero(mkFpaSort(type));
+ } else {
+ return makeNumberImpl(String.format("%f", n), type, pFloatingPointRoundingMode);
+ }
+ }
+
+ @Override
+ protected Long makeNumberImpl(
+ BigInteger exponent,
+ BigInteger mantissa,
+ boolean signBit,
+ FloatingPointType type) {
+ // FIXME: Implement by converting the arguments to bitvectors?
+ throw new UnsupportedOperationException();
+ }
+
+ private long mkFpaSort(FloatingPointType pType) {
+ return getFormulaCreator().getFloatingPointType(pType);
+ }
+
+ @Override
+ protected Long makeNumberAndRound(
+ String pN, FloatingPointType pType, Long pFloatingPointRoundingMode) {
+ // Convert scientific notation (f.ex "1.234E2") to a plain decimal string (f.ex "123.4")
+ String decimals = String.format("%.0f", Double.parseDouble(pN));
+ if (Double.compare(Double.parseDouble(pN), -0.0) == 0) {
+ return BitwuzlaJNI.bitwuzla_mk_fp_neg_zero(mkFpaSort(pType));
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_fp_from_real(
+ mkFpaSort(pType), pFloatingPointRoundingMode, decimals);
+ }
+ }
+
+ @Override
+ protected Long makeVariableImpl(String pVar, FloatingPointType pType) {
+ return getFormulaCreator().makeVariable(mkFpaSort(pType), pVar);
+ }
+
+ @Override
+ protected Long makePlusInfinityImpl(FloatingPointType pType) {
+ return BitwuzlaJNI.bitwuzla_mk_fp_pos_inf(mkFpaSort(pType));
+ }
+
+ @Override
+ protected Long makeMinusInfinityImpl(FloatingPointType pType) {
+ return BitwuzlaJNI.bitwuzla_mk_fp_neg_inf(mkFpaSort(pType));
+ }
+
+ @Override
+ protected Long makeNaNImpl(FloatingPointType pType) {
+ return BitwuzlaJNI.bitwuzla_mk_fp_nan(mkFpaSort(pType));
+ }
+
+ @Override
+ protected Long castToImpl(
+ Long pNumber, boolean pSigned, FormulaType> pTargetType, Long pRoundingMode) {
+ if (pTargetType.isFloatingPointType()) {
+ FormulaType.FloatingPointType targetType = (FormulaType.FloatingPointType) pTargetType;
+ return BitwuzlaJNI.bitwuzla_mk_term2_indexed2(
+ BITWUZLA_KIND_FP_TO_FP_FROM_FP.swigValue(),
+ pRoundingMode,
+ pNumber,
+ targetType.getExponentSize(),
+ targetType.getMantissaSize() + 1);
+ } else if (pTargetType.isBitvectorType()) {
+ FormulaType.BitvectorType targetType = (FormulaType.BitvectorType) pTargetType;
+ if (pSigned) {
+ return BitwuzlaJNI.bitwuzla_mk_term2_indexed1(
+ BITWUZLA_KIND_FP_TO_SBV.swigValue(), pRoundingMode, pNumber, targetType.getSize());
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2_indexed1(
+ BITWUZLA_KIND_FP_TO_UBV.swigValue(), pRoundingMode, pNumber, targetType.getSize());
+ }
+ } else {
+ throw new UnsupportedOperationException("Attempted cast to an unsupported type.");
+ }
+ }
+
+ @Override
+ protected Long castFromImpl(
+ Long pNumber, boolean pSigned, FloatingPointType pTargetType, Long pRoundingMode) {
+ FormulaType> formulaType = getFormulaCreator().getFormulaType(pNumber);
+ if (formulaType.isFloatingPointType()) {
+ return castToImpl(pNumber, pSigned, pTargetType, pRoundingMode);
+ } else if (formulaType.isBitvectorType()) {
+ if (pSigned) {
+ return BitwuzlaJNI.bitwuzla_mk_term2_indexed2(
+ BITWUZLA_KIND_FP_TO_FP_FROM_SBV.swigValue(),
+ roundingMode,
+ pNumber,
+ pTargetType.getExponentSize(),
+ pTargetType.getMantissaSize() + 1);
+ } else {
+ return BitwuzlaJNI.bitwuzla_mk_term2_indexed2(
+ BITWUZLA_KIND_FP_TO_FP_FROM_UBV.swigValue(),
+ roundingMode,
+ pNumber,
+ pTargetType.getExponentSize(),
+ pTargetType.getMantissaSize() + 1);
+ }
+
+ } else {
+ throw new UnsupportedOperationException("Attempted cast from an unsupported type.");
+ }
+ }
+
+ @Override
+ protected Long fromIeeeBitvectorImpl(Long pNumber, FloatingPointType pTargetType) {
+ return BitwuzlaJNI.bitwuzla_mk_term1_indexed2(
+ BITWUZLA_KIND_FP_TO_FP_FROM_BV.swigValue(),
+ pNumber,
+ pTargetType.getExponentSize(),
+ pTargetType.getMantissaSize() + 1);
+ }
+
+ @Override
+ protected Long toIeeeBitvectorImpl(Long pNumber) {
+ long rm = BitwuzlaJNI.bitwuzla_mk_rm_value(BitwuzlaJNI.BITWUZLA_RM_RTZ_get());
+ long inputBits =
+ BitwuzlaJNI.bitwuzla_term_fp_get_exp_size(pNumber)
+ + BitwuzlaJNI.bitwuzla_term_fp_get_sig_size(pNumber);
+ // This is most likely wrong/inprecise!
+ return BitwuzlaJNI.bitwuzla_mk_term2_indexed1(
+ BITWUZLA_KIND_FP_TO_SBV.swigValue(), rm, pNumber, inputBits);
+ }
+
+ @Override
+ protected Long negate(Long pParam1) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_NEG.swigValue(), pParam1);
+ }
+
+ @Override
+ protected Long abs(Long pParam1) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_ABS.swigValue(), pParam1);
+ }
+
+ @Override
+ protected Long max(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_MAX.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long min(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_MIN.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long sqrt(Long pNumber, Long pRoundingMode) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_SQRT.swigValue(), pRoundingMode, pNumber);
+ }
+
+ @Override
+ protected Long add(Long pParam1, Long pParam2, Long pRoundingMode) {
+ return BitwuzlaJNI.bitwuzla_mk_term3(
+ BITWUZLA_KIND_FP_ADD.swigValue(), pRoundingMode, pParam1, pParam2);
+ }
+
+ @Override
+ protected Long subtract(Long pParam1, Long pParam2, Long pFloatingPointRoundingMode) {
+ return BitwuzlaJNI.bitwuzla_mk_term3(
+ BITWUZLA_KIND_FP_SUB.swigValue(), pFloatingPointRoundingMode, pParam1, pParam2);
+ }
+
+ @Override
+ protected Long divide(Long pParam1, Long pParam2, Long pFloatingPointRoundingMode) {
+ return BitwuzlaJNI.bitwuzla_mk_term3(
+ BITWUZLA_KIND_FP_DIV.swigValue(), pFloatingPointRoundingMode, pParam1, pParam2);
+ }
+
+ @Override
+ protected Long multiply(Long pParam1, Long pParam2, Long pFloatingPointRoundingMode) {
+ return BitwuzlaJNI.bitwuzla_mk_term3(
+ BITWUZLA_KIND_FP_MUL.swigValue(), pFloatingPointRoundingMode, pParam1, pParam2);
+ }
+
+ @Override
+ protected Long remainder(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(
+ BitwuzlaKind.BITWUZLA_KIND_FP_REM.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long assignment(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_EQUAL.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long equalWithFPSemantics(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_EQUAL.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long greaterThan(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_GT.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long greaterOrEquals(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_GEQ.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long lessThan(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_LT.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long lessOrEquals(Long pParam1, Long pParam2) {
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_LEQ.swigValue(), pParam1, pParam2);
+ }
+
+ @Override
+ protected Long isNaN(Long pParam) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_IS_NAN.swigValue(), pParam);
+ }
+
+ @Override
+ protected Long isInfinity(Long pParam) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_IS_INF.swigValue(), pParam);
+ }
+
+ @Override
+ protected Long isZero(Long pParam) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_IS_ZERO.swigValue(), pParam);
+ }
+
+ @Override
+ protected Long isSubnormal(Long pParam) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_IS_SUBNORMAL.swigValue(), pParam);
+ }
+
+ @Override
+ protected Long isNormal(Long pParam) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_IS_NORMAL.swigValue(), pParam);
+ }
+
+ @Override
+ protected Long isNegative(Long pParam) {
+ return BitwuzlaJNI.bitwuzla_mk_term1(BITWUZLA_KIND_FP_IS_NEG.swigValue(), pParam);
+ }
+
+ @Override
+ protected Long round(Long pFormula, FloatingPointRoundingMode pRoundingMode) {
+ long rm = getRoundingModeImpl(pRoundingMode);
+ return BitwuzlaJNI.bitwuzla_mk_term2(BITWUZLA_KIND_FP_RTI.swigValue(), rm, pFormula);
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormula.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormula.java
new file mode 100644
index 0000000000..d47f7a05d6
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormula.java
@@ -0,0 +1,123 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import com.google.errorprone.annotations.Immutable;
+import org.sosy_lab.java_smt.api.ArrayFormula;
+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.FloatingPointRoundingModeFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.api.FormulaType;
+import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
+
+@Immutable
+abstract class BitwuzlaFormula implements Formula {
+ private final long bitwuzlaTerm;
+
+ BitwuzlaFormula(long term) {
+ bitwuzlaTerm = term;
+ }
+
+ final long getTerm() {
+ return bitwuzlaTerm;
+ }
+
+ /**
+ * returns an arbitrary representation of the formula, might be human- or machine-readable.
+ *
+ *
We do not guarantee that the returned String is in any way related to the formula. The
+ * solver might apply escaping or even un-escaping. A user should not use the returned String for
+ * further processing. For analyzing formulas, we recommend using a {@link FormulaVisitor}.
+ */
+ @Override
+ public String toString() {
+ return BitwuzlaJNI.bitwuzla_term_to_string(this.bitwuzlaTerm);
+ }
+
+ /**
+ * checks whether the other object is a formula of the same structure. Does not apply an expensive
+ * SAT-check to check equisatisfiability.
+ *
+ *
Two formulas that are structured in the same way, are determined as "equal". Due to
+ * transformations and simplifications, two equisatisfiable formulas with different structure
+ * might not be determined as "equal".
+ */
+ @Override
+ public boolean equals(Object other) {
+ if (other == this) {
+ return true;
+ }
+ if (!(other instanceof BitwuzlaFormula)) {
+ return false;
+ }
+ return bitwuzlaTerm == ((BitwuzlaFormula) other).getTerm();
+ }
+
+ /** returns a valid hashCode satisfying the constraints given by {@link #equals}. */
+ @Override
+ public int hashCode() {
+ // In this case, the long returned by the JNI is not a pointer, but the value itself.
+ return (int) BitwuzlaJNI.bitwuzla_term_hash(bitwuzlaTerm);
+ }
+
+ @Immutable
+ @SuppressWarnings("ClassTypeParameterName")
+ static final class BitwuzlaArrayFormula
+ extends BitwuzlaFormula implements ArrayFormula {
+
+ private final FormulaType indexType;
+ private final FormulaType elementType;
+
+ BitwuzlaArrayFormula(long pTerm, FormulaType pIndexType, FormulaType pElementType) {
+ super(pTerm);
+ indexType = pIndexType;
+ elementType = pElementType;
+ }
+
+ public FormulaType getIndexType() {
+ return indexType;
+ }
+
+ public FormulaType getElementType() {
+ return elementType;
+ }
+ }
+
+ @Immutable
+ static final class BitwuzlaBitvectorFormula extends BitwuzlaFormula implements BitvectorFormula {
+ BitwuzlaBitvectorFormula(long pTerm) {
+ super(pTerm);
+ }
+ }
+
+ @Immutable
+ static final class BitwuzlaFloatingPointFormula extends BitwuzlaFormula
+ implements FloatingPointFormula {
+ BitwuzlaFloatingPointFormula(long pTerm) {
+ super(pTerm);
+ }
+ }
+
+ @Immutable
+ static final class BitwuzlaFloatingPointRoundingModeFormula extends BitwuzlaFormula
+ implements FloatingPointRoundingModeFormula {
+ BitwuzlaFloatingPointRoundingModeFormula(long pTerm) {
+ super(pTerm);
+ }
+ }
+
+ @Immutable
+ static final class BitwuzlaBooleanFormula extends BitwuzlaFormula implements BooleanFormula {
+ BitwuzlaBooleanFormula(long pTerm) {
+ super(pTerm);
+ }
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
new file mode 100644
index 0000000000..02cf419bdb
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaCreator.java
@@ -0,0 +1,695 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import static com.google.common.base.Preconditions.checkArgument;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_AND;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_APPLY;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_ARRAY_SELECT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_ARRAY_STORE;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_ADD;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_AND;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_ASHR;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_CONCAT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_EXTRACT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_MUL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_NEG;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_NOT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_OR;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SDIV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SGE;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SGT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SHL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SIGN_EXTEND;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SLE;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SLT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SMOD;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SREM;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_SUB;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_UDIV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_UGE;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_UGT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_ULE;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_ULT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_UREM;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_XOR;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_BV_ZERO_EXTEND;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_CONSTANT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_DISTINCT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_EQUAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_EXISTS;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FORALL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_ABS;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_ADD;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_DIV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_EQUAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_GEQ;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_GT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_INF;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_NAN;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_NEG;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_NORMAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_SUBNORMAL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_IS_ZERO;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_LEQ;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_LT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_MAX;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_MIN;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_MUL;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_NEG;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_RTI;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_SQRT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_SUB;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_BV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_FP;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_SBV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_FP_FROM_UBV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_SBV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_FP_TO_UBV;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_IFF;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_IMPLIES;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_ITE;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_NOT;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_OR;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_VALUE;
+import static org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaKind.BITWUZLA_KIND_XOR;
+
+import com.google.common.collect.HashBasedTable;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.Table;
+import java.math.BigDecimal;
+import java.math.BigInteger;
+import java.util.ArrayList;
+import java.util.Iterator;
+import java.util.List;
+import java.util.Map.Entry;
+import java.util.Optional;
+import java.util.stream.LongStream;
+import org.sosy_lab.java_smt.api.ArrayFormula;
+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.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.FloatingPointType;
+import org.sosy_lab.java_smt.api.FunctionDeclarationKind;
+import org.sosy_lab.java_smt.api.QuantifiedFormulaManager.Quantifier;
+import org.sosy_lab.java_smt.api.visitors.FormulaVisitor;
+import org.sosy_lab.java_smt.basicimpl.FormulaCreator;
+import org.sosy_lab.java_smt.basicimpl.FunctionDeclarationImpl;
+import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormula.BitwuzlaArrayFormula;
+import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormula.BitwuzlaBitvectorFormula;
+import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormula.BitwuzlaBooleanFormula;
+import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormula.BitwuzlaFloatingPointFormula;
+import org.sosy_lab.java_smt.solvers.bitwuzla.BitwuzlaFormula.BitwuzlaFloatingPointRoundingModeFormula;
+
+public class BitwuzlaFormulaCreator extends FormulaCreator {
+ private final Table formulaCache = HashBasedTable.create();
+
+ // private final Table boundFormulaCache = HashBasedTable.create();
+
+ protected BitwuzlaFormulaCreator(Long pBitwuzlaEnv) {
+ super(pBitwuzlaEnv, BitwuzlaJNI.bitwuzla_mk_bool_sort(), null, null, null, null);
+ }
+
+ @Override
+ public Long getBitvectorType(int bitwidth) {
+ return BitwuzlaJNI.bitwuzla_mk_bv_sort(bitwidth);
+ }
+
+ @Override
+ public BitvectorFormula encapsulateBitvector(Long pTerm) {
+ assert getFormulaType(pTerm).isBitvectorType()
+ : "Unexpected formula type for BV formula: " + getFormulaType(pTerm);
+ return new BitwuzlaBitvectorFormula(pTerm);
+ }
+
+ // Assuming that JavaSMT FloatingPointType follows IEEE 754, if it is in the decimal
+ // system instead use bitwuzla_mk_fp_value_from_real somehow or convert myself
+ @Override
+ public Long getFloatingPointType(FloatingPointType type) {
+ long fpSort =
+ BitwuzlaJNI.bitwuzla_mk_fp_sort(type.getExponentSize(), type.getMantissaSize() + 1);
+ return fpSort;
+ }
+
+ @Override
+ @SuppressWarnings("MethodTypeParameterName")
+ protected FormulaType getArrayFormulaElementType(
+ ArrayFormula pArray) {
+ return ((BitwuzlaArrayFormula) pArray).getElementType();
+ }
+
+ @Override
+ @SuppressWarnings("MethodTypeParameterName")
+ protected FormulaType getArrayFormulaIndexType(
+ ArrayFormula pArray) {
+ return ((BitwuzlaArrayFormula) pArray).getIndexType();
+ }
+
+ @Override
+ public Long getArrayType(Long indexType, Long elementType) {
+ return BitwuzlaJNI.bitwuzla_mk_array_sort(indexType, elementType);
+ }
+
+ @Override
+ protected FloatingPointFormula encapsulateFloatingPoint(Long pTerm) {
+ assert getFormulaType(pTerm).isFloatingPointType()
+ : String.format(
+ "%s is no FP, but %s (%s)",
+ pTerm, BitwuzlaJNI.bitwuzla_term_get_sort(pTerm), getFormulaType(pTerm));
+ return new BitwuzlaFloatingPointFormula(pTerm);
+ }
+
+ @Override
+ @SuppressWarnings("MethodTypeParameterName")
+ protected ArrayFormula encapsulateArray(
+ Long pTerm, FormulaType pIndexType, FormulaType pElementType) {
+ assert getFormulaType(pTerm).isArrayType()
+ : "Unexpected formula type for array formula: " + getFormulaType(pTerm);
+ return new BitwuzlaArrayFormula<>(pTerm, pIndexType, pElementType);
+ }
+
+ @Override
+ public Long makeVariable(Long pSort, String varName) {
+ Long maybeFormula = formulaCache.get(varName, pSort);
+ if (maybeFormula != null) {
+ return maybeFormula;
+ }
+
+ long newVar = BitwuzlaJNI.bitwuzla_mk_const(pSort, varName);
+ formulaCache.put(varName, pSort, newVar);
+ return newVar;
+ }
+
+ public long makeBoundVariable(long var) {
+ String name = BitwuzlaJNI.bitwuzla_term_get_symbol(var);
+ Long sort = BitwuzlaJNI.bitwuzla_term_get_sort(var);
+ // TODO: do we need a bound cache?
+ // Long maybeVar = boundFormulaCache.get(name, sort);
+ // if (maybeVar != null) {
+ // return maybeVar;
+ // }
+
+ long newVar = BitwuzlaJNI.bitwuzla_mk_var(sort, name);
+ // boundFormulaCache.put(name, sort, newVar);
+ return newVar;
+ }
+
+ public FormulaType> bitwuzlaSortToType(Long pSort) {
+ // UFs play by different rules. For them, we need to extract the domain
+ if (BitwuzlaJNI.bitwuzla_sort_is_fp(pSort)) {
+ long exponent = BitwuzlaJNI.bitwuzla_sort_fp_get_exp_size(pSort);
+ long mantissa = BitwuzlaJNI.bitwuzla_sort_fp_get_sig_size(pSort) - 1;
+ return FormulaType.getFloatingPointType((int) exponent, (int) mantissa);
+ } else if (BitwuzlaJNI.bitwuzla_sort_is_bv(pSort)) {
+ return FormulaType.getBitvectorTypeWithSize(
+ (int) BitwuzlaJNI.bitwuzla_sort_bv_get_size(pSort));
+ } else if (BitwuzlaJNI.bitwuzla_sort_is_array(pSort)) {
+ FormulaType> domainSort =
+ bitwuzlaSortToType(BitwuzlaJNI.bitwuzla_sort_array_get_element(pSort));
+ FormulaType> rangeSort =
+ bitwuzlaSortToType(BitwuzlaJNI.bitwuzla_sort_array_get_index(pSort));
+ return FormulaType.getArrayType(domainSort, rangeSort);
+ } else if (BitwuzlaJNI.bitwuzla_sort_is_bool(pSort)) {
+ return FormulaType.BooleanType;
+ } else if (BitwuzlaJNI.bitwuzla_sort_is_rm(pSort)) {
+ return FormulaType.FloatingPointRoundingModeType;
+ }
+
+ throw new UnsupportedOperationException(
+ "Could not find the JavaSMT type for sort"
+ + BitwuzlaJNI.bitwuzla_sort_to_string(pSort)
+ + ".");
+ }
+
+ private FunctionDeclarationKind getDeclarationKind(Long term) {
+ BitwuzlaKind kind = BitwuzlaKind.swigToEnum(BitwuzlaJNI.bitwuzla_term_get_kind(term));
+
+ if (kind.equals(BITWUZLA_KIND_AND)) {
+ return FunctionDeclarationKind.AND;
+ } else if (kind.equals(BITWUZLA_KIND_DISTINCT)) {
+ return FunctionDeclarationKind.DISTINCT;
+ } else if (kind.equals(BITWUZLA_KIND_EQUAL)) {
+ return FunctionDeclarationKind.EQ;
+ } else if (kind.equals(BITWUZLA_KIND_IFF)) {
+ return FunctionDeclarationKind.IFF;
+ } else if (kind.equals(BITWUZLA_KIND_IMPLIES)) {
+ return FunctionDeclarationKind.IMPLIES;
+ } else if (kind.equals(BITWUZLA_KIND_NOT)) {
+ return FunctionDeclarationKind.NOT;
+ } else if (kind.equals(BITWUZLA_KIND_OR)) {
+ return FunctionDeclarationKind.OR;
+ } else if (kind.equals(BITWUZLA_KIND_XOR)) {
+ return FunctionDeclarationKind.XOR;
+ } else if (kind.equals(BITWUZLA_KIND_ITE)) {
+ return FunctionDeclarationKind.ITE;
+ } else if (kind.equals(BITWUZLA_KIND_APPLY)) {
+ return FunctionDeclarationKind.UF;
+ } else if (kind.equals(BITWUZLA_KIND_ARRAY_SELECT)) {
+ return FunctionDeclarationKind.SELECT;
+ } else if (kind.equals(BITWUZLA_KIND_ARRAY_STORE)) {
+ return FunctionDeclarationKind.STORE;
+ } else if (kind.equals(BITWUZLA_KIND_BV_ADD)) {
+ return FunctionDeclarationKind.BV_ADD;
+ } else if (kind.equals(BITWUZLA_KIND_BV_AND)) {
+ return FunctionDeclarationKind.BV_AND;
+ } else if (kind.equals(BITWUZLA_KIND_BV_ASHR)) {
+ return FunctionDeclarationKind.BV_ASHR;
+ } else if (kind.equals(BITWUZLA_KIND_BV_CONCAT)) {
+ return FunctionDeclarationKind.BV_CONCAT;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SMOD)) {
+ return FunctionDeclarationKind.BV_SMOD;
+ } else if (kind.equals(BITWUZLA_KIND_BV_MUL)) {
+ return FunctionDeclarationKind.BV_MUL;
+ } else if (kind.equals(BITWUZLA_KIND_BV_NEG)) {
+ return FunctionDeclarationKind.BV_NEG;
+ } else if (kind.equals(BITWUZLA_KIND_BV_NOT)) {
+ return FunctionDeclarationKind.BV_NOT;
+ } else if (kind.equals(BITWUZLA_KIND_BV_OR)) {
+ return FunctionDeclarationKind.BV_OR;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SDIV)) {
+ return FunctionDeclarationKind.BV_SDIV;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SGE)) {
+ return FunctionDeclarationKind.BV_SGE;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SGT)) {
+ return FunctionDeclarationKind.BV_SGT;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SHL)) {
+ return FunctionDeclarationKind.BV_SHL;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SLE)) {
+ return FunctionDeclarationKind.BV_SLE;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SLT)) {
+ return FunctionDeclarationKind.BV_SLT;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SREM)) {
+ return FunctionDeclarationKind.BV_SREM;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SUB)) {
+ return FunctionDeclarationKind.BV_SUB;
+ } else if (kind.equals(BITWUZLA_KIND_BV_UDIV)) {
+ return FunctionDeclarationKind.BV_UDIV;
+ } else if (kind.equals(BITWUZLA_KIND_BV_UGE)) {
+ return FunctionDeclarationKind.BV_UGE;
+ } else if (kind.equals(BITWUZLA_KIND_BV_UGT)) {
+ return FunctionDeclarationKind.BV_UGT;
+ } else if (kind.equals(BITWUZLA_KIND_BV_ULE)) {
+ return FunctionDeclarationKind.BV_ULE;
+ } else if (kind.equals(BITWUZLA_KIND_BV_ULT)) {
+ return FunctionDeclarationKind.BV_ULT;
+ } else if (kind.equals(BITWUZLA_KIND_BV_UREM)) {
+ return FunctionDeclarationKind.BV_UREM;
+ } else if (kind.equals(BITWUZLA_KIND_BV_EXTRACT)) {
+ return FunctionDeclarationKind.BV_EXTRACT;
+ } else if (kind.equals(BITWUZLA_KIND_BV_SIGN_EXTEND)) {
+ return FunctionDeclarationKind.BV_SIGN_EXTENSION;
+ } else if (kind.equals(BITWUZLA_KIND_BV_ZERO_EXTEND)) {
+ return FunctionDeclarationKind.BV_ZERO_EXTENSION;
+ } else if (kind.equals(BITWUZLA_KIND_FP_ABS)) {
+ return FunctionDeclarationKind.FP_ABS;
+ } else if (kind.equals(BITWUZLA_KIND_FP_ADD)) {
+ return FunctionDeclarationKind.FP_ADD;
+ } else if (kind.equals(BITWUZLA_KIND_FP_DIV)) {
+ return FunctionDeclarationKind.FP_DIV;
+ } else if (kind.equals(BITWUZLA_KIND_FP_EQUAL)) {
+ return FunctionDeclarationKind.FP_EQ;
+ } else if (kind.equals(BITWUZLA_KIND_FP_GEQ)) {
+ return FunctionDeclarationKind.FP_GE;
+ } else if (kind.equals(BITWUZLA_KIND_FP_GT)) {
+ return FunctionDeclarationKind.FP_GT;
+ } else if (kind.equals(BITWUZLA_KIND_FP_IS_INF)) {
+ return FunctionDeclarationKind.FP_IS_INF;
+ } else if (kind.equals(BITWUZLA_KIND_FP_IS_NAN)) {
+ return FunctionDeclarationKind.FP_IS_NAN;
+ } else if (kind.equals(BITWUZLA_KIND_FP_IS_NEG)) {
+ return FunctionDeclarationKind.FP_IS_NEGATIVE;
+ } else if (kind.equals(BITWUZLA_KIND_FP_IS_NORMAL)) {
+ return FunctionDeclarationKind.FP_IS_NORMAL;
+ } else if (kind.equals(BITWUZLA_KIND_FP_IS_SUBNORMAL)) {
+ return FunctionDeclarationKind.FP_IS_SUBNORMAL;
+ } else if (kind.equals(BITWUZLA_KIND_FP_IS_ZERO)) {
+ return FunctionDeclarationKind.FP_IS_ZERO;
+ } else if (kind.equals(BITWUZLA_KIND_FP_LEQ)) {
+ return FunctionDeclarationKind.FP_LE;
+ } else if (kind.equals(BITWUZLA_KIND_FP_LT)) {
+ return FunctionDeclarationKind.FP_LT;
+ } else if (kind.equals(BITWUZLA_KIND_FP_MAX)) {
+ return FunctionDeclarationKind.FP_MAX;
+ } else if (kind.equals(BITWUZLA_KIND_FP_MIN)) {
+ return FunctionDeclarationKind.FP_MIN;
+ } else if (kind.equals(BITWUZLA_KIND_FP_MUL)) {
+ return FunctionDeclarationKind.FP_MUL;
+ } else if (kind.equals(BITWUZLA_KIND_FP_NEG)) {
+ return FunctionDeclarationKind.FP_NEG;
+ } else if (kind.equals(BITWUZLA_KIND_FP_RTI)) {
+ return FunctionDeclarationKind.FP_ROUND_TO_INTEGRAL;
+ } else if (kind.equals(BITWUZLA_KIND_FP_SQRT)) {
+ return FunctionDeclarationKind.FP_SQRT;
+ } else if (kind.equals(BITWUZLA_KIND_FP_SUB)) {
+ return FunctionDeclarationKind.FP_SUB;
+ } else if (kind.equals(BITWUZLA_KIND_FP_TO_FP_FROM_BV)) {
+ return FunctionDeclarationKind.BV_UCASTTO_FP;
+ } else if (kind.equals(BITWUZLA_KIND_FP_TO_FP_FROM_FP)) {
+ return FunctionDeclarationKind.FP_CASTTO_FP;
+ } else if (kind.equals(BITWUZLA_KIND_FP_TO_FP_FROM_SBV)) {
+ return FunctionDeclarationKind.BV_SCASTTO_FP;
+ } else if (kind.equals(BITWUZLA_KIND_FP_TO_FP_FROM_UBV)) {
+ return FunctionDeclarationKind.BV_UCASTTO_FP;
+ } else if (kind.equals(BITWUZLA_KIND_FP_TO_SBV)) {
+ return FunctionDeclarationKind.FP_CASTTO_SBV;
+ } else if (kind.equals(BITWUZLA_KIND_FP_TO_UBV)) {
+ return FunctionDeclarationKind.FP_CASTTO_UBV;
+ } else if (kind.equals(BITWUZLA_KIND_BV_XOR)) {
+ return FunctionDeclarationKind.BV_XOR;
+ }
+ throw new UnsupportedOperationException("Can not discern formula kind " + kind);
+ }
+
+ @SuppressWarnings("unchecked")
+ @Override
+ public T encapsulate(FormulaType pType, Long pTerm) {
+ assert pType.equals(getFormulaType(pTerm))
+ : String.format(
+ "Trying to encapsulate formula of type %s as %s", getFormulaType(pTerm), pType);
+ if (pType.isBooleanType()) {
+ return (T) new BitwuzlaBooleanFormula(pTerm);
+ } else if (pType.isArrayType()) {
+ ArrayFormulaType, ?> arrFt = (ArrayFormulaType, ?>) pType;
+ return (T) new BitwuzlaArrayFormula<>(pTerm, arrFt.getIndexType(), arrFt.getElementType());
+ } else if (pType.isBitvectorType()) {
+ return (T) new BitwuzlaBitvectorFormula(pTerm);
+ } else if (pType.isFloatingPointType()) {
+ return (T) new BitwuzlaFloatingPointFormula(pTerm);
+ } else if (pType.isFloatingPointRoundingModeType()) {
+ return (T) new BitwuzlaFloatingPointRoundingModeFormula(pTerm);
+ }
+ throw new IllegalArgumentException("Cannot create formulas of type " + pType + " in Bitwuzla");
+ }
+
+ @SuppressWarnings("unchecked")
+ @Override
+ public FormulaType getFormulaType(T pFormula) {
+ long sort = BitwuzlaJNI.bitwuzla_term_get_sort(extractInfo(pFormula));
+ if (pFormula instanceof BitvectorFormula) {
+ checkArgument(
+ BitwuzlaJNI.bitwuzla_sort_is_bv(sort),
+ "BitvectorFormula with type missmatch: %s",
+ pFormula);
+ return (FormulaType)
+ FormulaType.getBitvectorTypeWithSize(
+ Math.toIntExact(BitwuzlaJNI.bitwuzla_sort_bv_get_size(sort)));
+ } else if (pFormula instanceof ArrayFormula, ?>) {
+ FormulaType arrayIndexType = getArrayFormulaIndexType((ArrayFormula) pFormula);
+ FormulaType arrayElementType = getArrayFormulaElementType((ArrayFormula) pFormula);
+ return (FormulaType) FormulaType.getArrayType(arrayIndexType, arrayElementType);
+ } else if (pFormula instanceof FloatingPointFormula) {
+ if (!BitwuzlaJNI.bitwuzla_sort_is_fp(sort)) {
+ throw new IllegalArgumentException(
+ "FloatingPointFormula with actual type "
+ + BitwuzlaJNI.bitwuzla_sort_to_string(sort)
+ + ": "
+ + pFormula);
+ }
+ int exp = (int) BitwuzlaJNI.bitwuzla_sort_fp_get_exp_size(sort);
+ int man = (int) BitwuzlaJNI.bitwuzla_sort_fp_get_sig_size(sort) - 1;
+ return (FormulaType) FormulaType.getFloatingPointType(exp, man);
+ } else if (BitwuzlaJNI.bitwuzla_sort_is_rm(sort)) {
+ return (FormulaType) FormulaType.FloatingPointRoundingModeType;
+ }
+ return super.getFormulaType(pFormula);
+ }
+
+ @Override
+ public FormulaType> getFormulaType(Long formula) {
+ long pType = BitwuzlaJNI.bitwuzla_term_get_sort(formula);
+ return bitwuzlaSortToType(pType);
+ }
+
+ private BigDecimal parseIEEEbinaryFP(long pTerm) {
+ // The Bitwuzla string for FPs is always in binary, regardless of the second argument.
+
+ String fp = BitwuzlaJNI.bitwuzla_term_value_get_str(pTerm);
+
+ if (fp.length() == 32) {
+ float result = Float.intBitsToFloat(Integer.parseUnsignedInt(fp, 2));
+ return new BigDecimal(result);
+ } else if (fp.length() == 64) {
+ double result = Double.longBitsToDouble(Long.parseUnsignedLong(fp, 2));
+ return new BigDecimal(result);
+ } else {
+ throw new UnsupportedOperationException(
+ "Visitor can only visit constant FPs of 32 or 64 " + "bits.");
+ }
+
+ // String fpSMTLIB = bitwuzlaJNI.bitwuzla_term_to_string(pTerm);
+ // String[] mySplit = fpSMTLIB.split(" #b");
+ // mySplit[3] = mySplit[3].replace(")", "");
+ // double result = calculateDecimal(mySplit[3], mySplit[2], mySplit[1]);
+ }
+
+ @Override
+ public R visit(FormulaVisitor visitor, Formula formula, Long f)
+ throws UnsupportedOperationException {
+ BitwuzlaKind kind = BitwuzlaKind.swigToEnum(BitwuzlaJNI.bitwuzla_term_get_kind(f));
+ if (termIsConstant(f)) {
+ return visitor.visitConstant(formula, convertValue(f));
+
+ } else if (BitwuzlaJNI.bitwuzla_term_is_fp_value(f)) {
+ return visitor.visitConstant(formula, parseIEEEbinaryFP(f));
+
+ } else if (BitwuzlaJNI.bitwuzla_term_is_const(f)) {
+ String name = BitwuzlaJNI.bitwuzla_term_get_symbol(f);
+ return visitor.visitFreeVariable(formula, name);
+
+ } else if (BitwuzlaJNI.bitwuzla_term_is_var(f)) {
+ String name = BitwuzlaJNI.bitwuzla_term_get_symbol(f);
+ long sort = BitwuzlaJNI.bitwuzla_term_get_sort(f);
+ long originalVar = formulaCache.get(name, sort);
+ return visitor.visitBoundVariable(encapsulate(getFormulaType(originalVar), originalVar), 0);
+
+ } else if (kind.equals(BITWUZLA_KIND_EXISTS) || kind.equals(BITWUZLA_KIND_FORALL)) {
+ long[] children = BitwuzlaJNI.bitwuzla_term_get_children(f, new long[1]);
+ // QUANTIFIER: replace bound variable with free variable for visitation
+ int size = children.length;
+ assert children.length == 2;
+ long bodyUnSub = children[size - 1];
+ List freeEncVars = new ArrayList<>();
+ // The first length - 2 elements are bound vars, and the last element is the body
+ long[] boundVars = new long[size - 1];
+ long[] freeVars = new long[size - 1];
+ for (int i = 0; i < size - 1; i++) {
+ long boundVar = children[i];
+ boundVars[i] = boundVar;
+ String name = BitwuzlaJNI.bitwuzla_term_get_symbol(boundVar);
+ assert name != null;
+ long sort = BitwuzlaJNI.bitwuzla_term_get_sort(boundVar);
+ long freeVar;
+ if (formulaCache.contains(name, sort)) {
+ freeVar = formulaCache.get(name, sort);
+ } else {
+ // no free var existing (e.g. from parsing), create a new one
+ freeVar = makeVariable(sort, name);
+ }
+ freeVars[i] = freeVar;
+ freeEncVars.add(encapsulate(getFormulaType(freeVar), freeVar));
+ }
+
+ long bodySubbed = BitwuzlaJNI.bitwuzla_substitute_term(bodyUnSub, 1, boundVars, freeVars);
+
+ Quantifier quant = kind.equals(BITWUZLA_KIND_EXISTS) ? Quantifier.EXISTS : Quantifier.FORALL;
+ return visitor.visitQuantifier(
+ (BooleanFormula) formula, quant, freeEncVars, encapsulateBoolean(bodySubbed));
+
+ } else {
+ long[] args = BitwuzlaJNI.bitwuzla_term_get_children(f, new long[1]);
+ ImmutableList.Builder arguments = ImmutableList.builder();
+ ImmutableList.Builder> argumentTypes = ImmutableList.builder();
+
+ String name = BitwuzlaJNI.bitwuzla_term_get_symbol(f);
+
+ BitwuzlaDeclaration decl = null;
+ for (int i = 0; i < args.length; i++) {
+ long argument = args[i];
+ if (kind == BITWUZLA_KIND_APPLY && i == 0) {
+ // UFs carry the decl in the first child and the decl has the name
+ decl = new BitwuzlaDeclaration(argument, false);
+ name = BitwuzlaJNI.bitwuzla_term_get_symbol(argument);
+ continue;
+ }
+ FormulaType> type = getFormulaType(argument);
+ arguments.add(encapsulate(type, argument));
+ argumentTypes.add(type);
+ }
+
+ if (name == null) {
+ name = BitwuzlaJNI.bitwuzla_kind_to_string(BitwuzlaJNI.bitwuzla_term_get_kind(f));
+ }
+ if (decl == null) {
+ decl = new BitwuzlaDeclaration(BitwuzlaJNI.bitwuzla_term_get_kind(f), true);
+ }
+ if (BitwuzlaJNI.bitwuzla_term_is_indexed(f)) {
+ // We need to retain the original formula as the declaration for indexed formulas,
+ // otherwise we loose the index info, but we also need to know if its a kind or term
+ decl = new BitwuzlaDeclaration(f, false);
+ }
+
+ return visitor.visitFunction(
+ formula,
+ arguments.build(),
+ FunctionDeclarationImpl.of(
+ name, getDeclarationKind(f), argumentTypes.build(), getFormulaType(f), decl));
+ }
+ }
+
+ private boolean termIsConstant(long term) {
+ return BITWUZLA_KIND_VALUE.swigValue() == BitwuzlaJNI.bitwuzla_term_get_kind(term);
+ }
+
+ @Override
+ public Long callFunctionImpl(BitwuzlaDeclaration declaration, List args) {
+ // For UFs the declaration needs to be a const wrapping of the function sort
+ // For all other functions it needs to be the kind
+ // BUT, we can never use a bitwuzla_term_is... function on a KIND
+ if (!declaration.isKind() && BitwuzlaJNI.bitwuzla_term_is_indexed(declaration.getTerm())) {
+ // The term might be indexed, then we need index creation
+ long term = declaration.getTerm();
+ int properKind = BitwuzlaJNI.bitwuzla_term_get_kind(term);
+ if (BitwuzlaKind.swigToEnum(properKind) == BITWUZLA_KIND_BV_ZERO_EXTEND) {
+ System.out.println();
+ }
+ long[] indices = BitwuzlaJNI.bitwuzla_term_get_indices(term, new long[1]);
+ return BitwuzlaJNI.bitwuzla_mk_term_indexed(
+ properKind,
+ args.size(),
+ args.stream().mapToLong(Long::longValue).toArray(),
+ indices.length,
+ indices);
+ }
+
+ if (!declaration.isKind() && BitwuzlaJNI.bitwuzla_term_is_fun(declaration.getTerm())) {
+ long[] functionAndArgs =
+ LongStream.concat(
+ LongStream.of(declaration.getTerm()), args.stream().mapToLong(Long::longValue))
+ .toArray();
+ return BitwuzlaJNI.bitwuzla_mk_term(
+ BITWUZLA_KIND_APPLY.swigValue(), functionAndArgs.length, functionAndArgs);
+ }
+
+ assert declaration.isKind();
+ long declKind = declaration.getKind();
+
+ return BitwuzlaJNI.bitwuzla_mk_term(
+ (int) declKind, args.size(), args.stream().mapToLong(Long::longValue).toArray());
+ }
+
+ @Override
+ public BitwuzlaDeclaration declareUFImpl(String name, Long pReturnType, List pArgTypes) {
+ if (pArgTypes.isEmpty()) {
+ // Bitwuzla does not support UFs with no args, so we make a variable
+ // TODO: implement
+ throw new UnsupportedOperationException("Bitwuzla does not support 0 arity UFs.");
+ }
+ long functionSort =
+ BitwuzlaJNI.bitwuzla_mk_fun_sort(
+ pArgTypes.size(), pArgTypes.stream().mapToLong(Long::longValue).toArray(), pReturnType);
+
+ Long maybeFormula = formulaCache.get(name, functionSort);
+ if (maybeFormula != null) {
+ return new BitwuzlaDeclaration(maybeFormula, false);
+ }
+
+ long uf = BitwuzlaJNI.bitwuzla_mk_const(functionSort, name);
+ formulaCache.put(name, functionSort, uf);
+ return new BitwuzlaDeclaration(uf, false);
+ }
+
+ @Override
+ protected BitwuzlaDeclaration getBooleanVarDeclarationImpl(Long pLong) {
+ long kind = BitwuzlaJNI.bitwuzla_term_get_kind(pLong);
+
+ // CONSTANTS are "variables" and Kind.VARIABLES are bound variables in for example quantifiers
+ assert kind == BITWUZLA_KIND_APPLY.swigValue() || kind == BITWUZLA_KIND_CONSTANT.swigValue()
+ : BitwuzlaJNI.bitwuzla_term_to_string(kind);
+ if (kind == BITWUZLA_KIND_APPLY.swigValue()) {
+ long[] size = new long[1];
+ long[] pChildren = BitwuzlaJNI.bitwuzla_term_get_children(pLong, size);
+ // Returns pointer to Uninterpreted Function used in Apply
+ return new BitwuzlaDeclaration(pChildren[0], false);
+ } else {
+ return new BitwuzlaDeclaration(pLong, true);
+ }
+ }
+
+ @Override
+ public Long extractInfo(Formula pT) {
+ return BitwuzlaFormulaManager.getBitwuzlaTerm(pT);
+ }
+
+ @Override
+ public BooleanFormula encapsulateBoolean(Long pTerm) {
+ assert getFormulaType(pTerm).isBooleanType();
+ return new BitwuzlaBooleanFormula(pTerm);
+ }
+
+ protected Table getCache() {
+ return formulaCache;
+ }
+
+ // True if the entered String has an existing variable in the cache.
+ protected boolean formulaCacheContains(String variable) {
+ // There is always only 1 type permitted per variable
+ return formulaCache.containsRow(variable);
+ }
+
+ // Optional that contains the variable to the entered String if there is one.
+ protected Optional getFormulaFromCache(String variable) {
+ Iterator> entrySetIter = formulaCache.row(variable).entrySet().iterator();
+ if (entrySetIter.hasNext()) {
+ // If there is a non empty row for an entry, there is only one entry
+ return Optional.of(entrySetIter.next().getValue());
+ }
+ return Optional.empty();
+ }
+
+ @Override
+ public Object convertValue(Long term) {
+ String value;
+ long sort = BitwuzlaJNI.bitwuzla_term_get_sort(term);
+ if (BitwuzlaJNI.bitwuzla_term_is_const(term)) {
+ return null;
+ }
+ if (BitwuzlaJNI.bitwuzla_sort_is_fun(sort)) {
+ // TODO: this is wrong
+ throw new AssertionError("Error: Unknown sort and term");
+ } else {
+ value = BitwuzlaJNI.bitwuzla_term_to_string(term);
+ if (value.startsWith("#b")) {
+ // Bitvectors in Bitwuzla start with a #b
+ return new BigInteger(value.substring(2), 2);
+ } else if (value.equals("true")) {
+ return true;
+ } else if (value.equals("false")) {
+ return false;
+ } else if (value.startsWith("(fp")) {
+ return value
+ .replace("(fp", "")
+ .replace(")", "")
+ .replace("#b", "")
+ .replace("#b", "")
+ .replace("#b", "")
+ .strip();
+ } else if (BitwuzlaJNI.bitwuzla_sort_is_rm(sort)) {
+ return value;
+ }
+ }
+
+ throw new AssertionError(
+ "Error: Could not convert term to value; Unknown sort and term. "
+ + "Value: "
+ + BitwuzlaJNI.bitwuzla_term_to_string(term));
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java
new file mode 100644
index 0000000000..da61462db4
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaFormulaManager.java
@@ -0,0 +1,99 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import com.google.common.base.Preconditions;
+import java.io.IOException;
+import org.sosy_lab.common.Appender;
+import org.sosy_lab.common.Appenders;
+import org.sosy_lab.java_smt.api.BooleanFormula;
+import org.sosy_lab.java_smt.api.Formula;
+import org.sosy_lab.java_smt.basicimpl.AbstractFormulaManager;
+
+final class BitwuzlaFormulaManager
+ extends AbstractFormulaManager {
+
+ BitwuzlaFormulaManager(
+ BitwuzlaFormulaCreator pFormulaCreator,
+ BitwuzlaUFManager pFunctionManager,
+ BitwuzlaBooleanFormulaManager pBooleanManager,
+ BitwuzlaBitvectorFormulaManager pBitvectorManager,
+ BitwuzlaQuantifiedFormulaManager pQuantifierManager,
+ BitwuzlaFloatingPointManager pFloatingPointManager,
+ BitwuzlaArrayFormulaManager pArrayManager) {
+ super(
+ pFormulaCreator,
+ pFunctionManager,
+ pBooleanManager,
+ null,
+ null,
+ pBitvectorManager,
+ pFloatingPointManager,
+ pQuantifierManager,
+ pArrayManager,
+ null,
+ null,
+ null);
+ }
+
+ @Override
+ public BooleanFormula parse(String s) throws IllegalArgumentException {
+ if (s.contains("(check-sat)")) {
+ s = s.replace("(check-sat)", "");
+ }
+ if (s.contains("(exit)")) {
+ s = s.replace("(exit)", "");
+ }
+ long[] terms = BitwuzlaJNI.parse(s);
+ Preconditions.checkArgument(terms != null, "Could not parse input string \"%s\"", s);
+ assert terms != null;
+ // AND all the terms
+ Long retForm;
+ if (terms.length > 1) {
+ retForm =
+ BitwuzlaJNI.bitwuzla_mk_term(
+ BitwuzlaKind.BITWUZLA_KIND_AND.swigValue(), terms.length, terms);
+ } else {
+ retForm = terms[0];
+ }
+ assert BitwuzlaJNI.bitwuzla_term_is_bool(retForm);
+ return super.getFormulaCreator().encapsulateBoolean(retForm);
+ }
+
+ @Override
+ public Appender dumpFormula(Long pTerm) {
+ // There are 2 ways of SMT2 printing in Bitwuzla, bitwuzla_term_print() and
+ // bitwuzla_term_print_fmt(), which print a single formula, and bitwuzla_print_formula(),
+ // which prints the complete assertion stack of the bitwuzla instance given to the function.
+ // Only bitwuzla_print_formula() gives us the proper SMT2 format, with (check-sat) etc.
+ // Note: bitwuzla_print_formula() is wrapped in dump_assertions_smt2()
+ return new Appenders.AbstractAppender() {
+ @Override
+ public void appendTo(Appendable out) throws IOException {
+ long printCtx = getFormulaCreator().getEnv();
+ BitwuzlaJNI.bitwuzla_push(printCtx, 1);
+ BitwuzlaJNI.bitwuzla_assert(printCtx, pTerm);
+ String dump = BitwuzlaJNI.dump_assertions_smt2(printCtx, 10);
+ BitwuzlaJNI.bitwuzla_pop(printCtx, 1);
+ // Bitwuzla prints (check-sat)\n(exit)\n in the end. We remove that.
+ if (dump.contains("(check-sat)\n")) {
+ dump = dump.replace("(check-sat)", "");
+ }
+ if (dump.contains("(exit)")) {
+ dump = dump.replace("(exit)", "");
+ }
+ out.append(dump);
+ }
+ };
+ }
+
+ static long getBitwuzlaTerm(Formula pT) {
+ return ((BitwuzlaFormula) pT).getTerm();
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaJNI.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaJNI.java
new file mode 100644
index 0000000000..3939559601
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaJNI.java
@@ -0,0 +1,758 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/* ----------------------------------------------------------------------------
+ * This file was automatically generated by SWIG (http://www.swig.org).
+ * Version 4.0.2
+ *
+ * Do not make changes to this file unless you know what you are doing--modify
+ * the SWIG interface file instead.
+ * ----------------------------------------------------------------------------- */
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+@SuppressWarnings({"unused", "checkstyle:methodname", "checkstyle:parametername"})
+public class BitwuzlaJNI {
+ private BitwuzlaJNI() {}
+
+ public static final native long new_BitwuzlaTermArray(int jarg1);
+
+ public static final native void delete_BitwuzlaTermArray(long jarg1);
+
+ public static final native long BitwuzlaTermArray_getitem(long jarg1, int jarg2);
+
+ public static final native void BitwuzlaTermArray_setitem(long jarg1, int jarg2, long jarg3);
+
+ public static final native long new_BitwuzlaSortArray(int jarg1);
+
+ public static final native void delete_BitwuzlaSortArray(long jarg1);
+
+ public static final native long BitwuzlaSortArray_getitem(long jarg1, int jarg2);
+
+ public static final native void BitwuzlaSortArray_setitem(long jarg1, int jarg2, long jarg3);
+
+ public static final native long new_uint64_tArray(int jarg1);
+
+ public static final native void delete_uint64_tArray(long jarg1);
+
+ public static final native long uint64_tArray_getitem(long jarg1, int jarg2);
+
+ public static final native void uint64_tArray_setitem(long jarg1, int jarg2, long jarg3);
+
+ public static final native int true_get();
+
+ public static final native int false_get();
+
+ public static final native int __bool_true_false_are_defined_get();
+
+ public static final native int _STDIO_H_get();
+
+ public static final native int _FEATURES_H_get();
+
+ public static final native int _DEFAULT_SOURCE_get();
+
+ public static final native int __GLIBC_USE_ISOC2X_get();
+
+ public static final native int __USE_POSIX_IMPLICITLY_get();
+
+ public static final native int _POSIX_SOURCE_get();
+
+ public static final native int _POSIX_C_SOURCE_get();
+
+ public static final native int __USE_POSIX_get();
+
+ public static final native int __USE_POSIX2_get();
+
+ public static final native int __USE_POSIX199309_get();
+
+ public static final native int __USE_POSIX199506_get();
+
+ public static final native int __USE_XOPEN2K_get();
+
+ public static final native int __USE_ISOC95_get();
+
+ public static final native int __USE_ISOC99_get();
+
+ public static final native int __USE_XOPEN2K8_get();
+
+ public static final native int _ATFILE_SOURCE_get();
+
+ public static final native int __WORDSIZE_get();
+
+ public static final native int __WORDSIZE32_SIZE_ULONG_get();
+
+ public static final native int __WORDSIZE32_PTRDIFF_LONG_get();
+
+ public static final native int __WORDSIZE_TIME64_COMPAT32_get();
+
+ public static final native int __TIMESIZE_get();
+
+ public static final native int __USE_MISC_get();
+
+ public static final native int __USE_ATFILE_get();
+
+ public static final native int __USE_FORTIFY_LEVEL_get();
+
+ public static final native int __GLIBC_USE_DEPRECATED_GETS_get();
+
+ public static final native int __GLIBC_USE_DEPRECATED_SCANF_get();
+
+ public static final native int _STDC_PREDEF_H_get();
+
+ public static final native int __STDC_IEC_559___get();
+
+ public static final native int __STDC_IEC_60559_BFP___get();
+
+ public static final native int __STDC_IEC_559_COMPLEX___get();
+
+ public static final native int __STDC_IEC_60559_COMPLEX___get();
+
+ public static final native int __STDC_ISO_10646___get();
+
+ public static final native int __GNU_LIBRARY___get();
+
+ public static final native int __GLIBC___get();
+
+ public static final native int __GLIBC_MINOR___get();
+
+ public static final native int _SYS_CDEFS_H_get();
+
+ public static final native int __glibc_c99_flexarr_available_get();
+
+ public static final native int __LDOUBLE_REDIRECTS_TO_FLOAT128_ABI_get();
+
+ public static final native int __HAVE_GENERIC_SELECTION_get();
+
+ public static final native int __GLIBC_USE_LIB_EXT2_get();
+
+ public static final native int __GLIBC_USE_IEC_60559_BFP_EXT_get();
+
+ public static final native int __GLIBC_USE_IEC_60559_BFP_EXT_C2X_get();
+
+ public static final native int __GLIBC_USE_IEC_60559_EXT_get();
+
+ public static final native int __GLIBC_USE_IEC_60559_FUNCS_EXT_get();
+
+ public static final native int __GLIBC_USE_IEC_60559_FUNCS_EXT_C2X_get();
+
+ public static final native int __GLIBC_USE_IEC_60559_TYPES_EXT_get();
+
+ public static final native int _BITS_TYPES_H_get();
+
+ public static final native int _BITS_TYPESIZES_H_get();
+
+ public static final native int __RLIM_T_MATCHES_RLIM64_T_get();
+
+ public static final native int __STATFS_MATCHES_STATFS64_get();
+
+ public static final native int __KERNEL_OLD_TIMEVAL_MATCHES_TIMEVAL64_get();
+
+ public static final native int __FD_SETSIZE_get();
+
+ public static final native int _BITS_TIME64_H_get();
+
+ public static final native long new___fpos64_t();
+
+ public static final native void delete___fpos64_t(long jarg1);
+
+ public static final native int ____FILE_defined_get();
+
+ public static final native int __FILE_defined_get();
+
+ public static final native int __struct_FILE_defined_get();
+
+ public static final native long new__IO_FILE();
+
+ public static final native void delete__IO_FILE(long jarg1);
+
+ public static final native int _IO_EOF_SEEN_get();
+
+ public static final native int _IO_ERR_SEEN_get();
+
+ public static final native int _IO_USER_LOCK_get();
+
+ public static final native int _IOFBF_get();
+
+ public static final native int _IOLBF_get();
+
+ public static final native int _IONBF_get();
+
+ public static final native int BUFSIZ_get();
+
+ public static final native int EOF_get();
+
+ public static final native int SEEK_SET_get();
+
+ public static final native int SEEK_CUR_get();
+
+ public static final native int SEEK_END_get();
+
+ public static final native String P_tmpdir_get();
+
+ public static final native int _BITS_STDIO_LIM_H_get();
+
+ public static final native int L_tmpnam_get();
+
+ public static final native int TMP_MAX_get();
+
+ public static final native int FILENAME_MAX_get();
+
+ public static final native int L_ctermid_get();
+
+ public static final native int FOPEN_MAX_get();
+
+ public static final native long stdin_get();
+
+ public static final native long stdout_get();
+
+ public static final native long stderr_get();
+
+ public static final native int remove(String jarg1);
+
+ public static final native int rename(String jarg1, String jarg2);
+
+ public static final native int renameat(int jarg1, String jarg2, int jarg3, String jarg4);
+
+ public static final native long tmpfile();
+
+ public static final native String tmpnam(String jarg1);
+
+ public static final native String tmpnam_r(String jarg1);
+
+ public static final native String tempnam(String jarg1, String jarg2);
+
+ public static final native long fopen(String jarg1, String jarg2);
+
+ public static final native long fdopen(int jarg1, String jarg2);
+
+ public static final native long fmemopen(long jarg1, long jarg2, String jarg3);
+
+ public static final native long open_memstream(long jarg1, long jarg2);
+
+ public static final native int printf(String jarg1);
+
+ public static final native int sprintf(String jarg1, String jarg2);
+
+ public static final native int vprintf(String jarg1, long jarg2);
+
+ public static final native int vsprintf(String jarg1, String jarg2, long jarg3);
+
+ public static final native int snprintf(String jarg1, long jarg2, String jarg3);
+
+ public static final native int vsnprintf(String jarg1, long jarg2, String jarg3, long jarg4);
+
+ public static final native int vdprintf(int jarg1, String jarg2, long jarg3);
+
+ public static final native int dprintf(int jarg1, String jarg2);
+
+ public static final native int scanf(String jarg1);
+
+ public static final native int sscanf(String jarg1, String jarg2);
+
+ public static final native int __HAVE_FLOAT128_get();
+
+ public static final native int __HAVE_DISTINCT_FLOAT128_get();
+
+ public static final native int __HAVE_FLOAT64X_get();
+
+ public static final native int __HAVE_FLOAT64X_LONG_DOUBLE_get();
+
+ public static final native int __HAVE_FLOAT16_get();
+
+ public static final native int __HAVE_FLOAT32_get();
+
+ public static final native int __HAVE_FLOAT64_get();
+
+ public static final native int __HAVE_FLOAT32X_get();
+
+ public static final native int __HAVE_FLOAT128X_get();
+
+ public static final native int __HAVE_DISTINCT_FLOAT16_get();
+
+ public static final native int __HAVE_DISTINCT_FLOAT32_get();
+
+ public static final native int __HAVE_DISTINCT_FLOAT64_get();
+
+ public static final native int __HAVE_DISTINCT_FLOAT32X_get();
+
+ public static final native int __HAVE_DISTINCT_FLOAT64X_get();
+
+ public static final native int __HAVE_DISTINCT_FLOAT128X_get();
+
+ public static final native int __HAVE_FLOATN_NOT_TYPEDEF_get();
+
+ public static final native int __isoc99_scanf(String jarg1);
+
+ public static final native int __isoc99_sscanf(String jarg1, String jarg2);
+
+ public static final native int vscanf(String jarg1, long jarg2);
+
+ public static final native int vsscanf(String jarg1, String jarg2, long jarg3);
+
+ public static final native int __isoc99_vscanf(String jarg1, long jarg2);
+
+ public static final native int __isoc99_vsscanf(String jarg1, String jarg2, long jarg3);
+
+ public static final native int getchar();
+
+ public static final native int getchar_unlocked();
+
+ public static final native int putchar(int jarg1);
+
+ public static final native int putchar_unlocked(int jarg1);
+
+ public static final native int puts(String jarg1);
+
+ public static final native void perror(String jarg1);
+
+ public static final native long popen(String jarg1, String jarg2);
+
+ public static final native String ctermid(String jarg1);
+
+ public static final native int BITWUZLA_SAT_get();
+
+ public static final native int BITWUZLA_UNSAT_get();
+
+ public static final native int BITWUZLA_UNKNOWN_get();
+
+ public static final native int BITWUZLA_RM_RNE_get();
+
+ public static final native int BITWUZLA_RM_RNA_get();
+
+ public static final native int BITWUZLA_RM_RTN_get();
+
+ public static final native int BITWUZLA_RM_RTP_get();
+
+ public static final native int BITWUZLA_RM_RTZ_get();
+
+ public static final native int BITWUZLA_RM_MAX_get();
+
+ public static final native int BITWUZLA_KIND_CONSTANT_get();
+
+ public static final native String bitwuzla_copyright();
+
+ public static final native String bitwuzla_version();
+
+ public static final native String bitwuzla_git_id();
+
+ public static final native void BitwuzlaOptionInfo_opt_set(
+ long jarg1, BitwuzlaOptionInfo jarg1_, int jarg2);
+
+ public static final native int BitwuzlaOptionInfo_opt_get(long jarg1, BitwuzlaOptionInfo jarg1_);
+
+ public static final native void BitwuzlaOptionInfo_shrt_set(
+ long jarg1, BitwuzlaOptionInfo jarg1_, String jarg2);
+
+ public static final native String BitwuzlaOptionInfo_shrt_get(
+ long jarg1, BitwuzlaOptionInfo jarg1_);
+
+ public static final native void BitwuzlaOptionInfo_lng_set(
+ long jarg1, BitwuzlaOptionInfo jarg1_, String jarg2);
+
+ public static final native String BitwuzlaOptionInfo_lng_get(
+ long jarg1, BitwuzlaOptionInfo jarg1_);
+
+ public static final native void BitwuzlaOptionInfo_description_set(
+ long jarg1, BitwuzlaOptionInfo jarg1_, String jarg2);
+
+ public static final native String BitwuzlaOptionInfo_description_get(
+ long jarg1, BitwuzlaOptionInfo jarg1_);
+
+ public static final native void BitwuzlaOptionInfo_is_numeric_set(
+ long jarg1, BitwuzlaOptionInfo jarg1_, boolean jarg2);
+
+ public static final native boolean BitwuzlaOptionInfo_is_numeric_get(
+ long jarg1, BitwuzlaOptionInfo jarg1_);
+
+ public static final native void BitwuzlaOptionInfo_numeric_set(
+ long jarg1, BitwuzlaOptionInfo jarg1_, long jarg2, NumericValue jarg2_);
+
+ public static final native long BitwuzlaOptionInfo_numeric_get(
+ long jarg1, BitwuzlaOptionInfo jarg1_);
+
+ public static final native long BitwuzlaOptionInfo_mode_get(
+ long jarg1, BitwuzlaOptionInfo jarg1_);
+
+ public static final native long new_BitwuzlaOptionInfo();
+
+ public static final native void delete_BitwuzlaOptionInfo(long jarg1);
+
+ public static final native void NumericValue_cur_set(long jarg1, NumericValue jarg1_, long jarg2);
+
+ public static final native long NumericValue_cur_get(long jarg1, NumericValue jarg1_);
+
+ public static final native void NumericValue_dflt_set(
+ long jarg1, NumericValue jarg1_, long jarg2);
+
+ public static final native long NumericValue_dflt_get(long jarg1, NumericValue jarg1_);
+
+ public static final native void NumericValue_min_set(long jarg1, NumericValue jarg1_, long jarg2);
+
+ public static final native long NumericValue_min_get(long jarg1, NumericValue jarg1_);
+
+ public static final native void NumericValue_max_set(long jarg1, NumericValue jarg1_, long jarg2);
+
+ public static final native long NumericValue_max_get(long jarg1, NumericValue jarg1_);
+
+ public static final native long new_NumericValue();
+
+ public static final native void delete_NumericValue(long jarg1);
+
+ public static final native long new_ModeValue();
+
+ public static final native void delete_ModeValue(long jarg1);
+
+ public static final native long bitwuzla_options_new();
+
+ public static final native void bitwuzla_options_delete(long jarg1);
+
+ public static final native boolean bitwuzla_option_is_valid(long jarg1, String jarg2);
+
+ public static final native boolean bitwuzla_option_is_numeric(long jarg1, int jarg2);
+
+ public static final native boolean bitwuzla_option_is_mode(long jarg1, int jarg2);
+
+ public static final native void bitwuzla_set_option(long jarg1, int jarg2, long jarg3);
+
+ public static final native void bitwuzla_set_option_mode(long jarg1, int jarg2, String jarg3);
+
+ public static final native long bitwuzla_get_option(long jarg1, int jarg2);
+
+ public static final native String bitwuzla_get_option_mode(long jarg1, int jarg2);
+
+ public static final native void bitwuzla_get_option_info(
+ long jarg1, int jarg2, long jarg3, BitwuzlaOptionInfo jarg3_);
+
+ public static final native String bitwuzla_result_to_string(int jarg1);
+
+ public static final native String bitwuzla_rm_to_string(int jarg1);
+
+ public static final native String bitwuzla_kind_to_string(int jarg1);
+
+ public static final native long bitwuzla_sort_hash(long jarg1);
+
+ public static final native long bitwuzla_sort_bv_get_size(long jarg1);
+
+ public static final native long bitwuzla_sort_fp_get_exp_size(long jarg1);
+
+ public static final native long bitwuzla_sort_fp_get_sig_size(long jarg1);
+
+ public static final native long bitwuzla_sort_array_get_index(long jarg1);
+
+ public static final native long bitwuzla_sort_array_get_element(long jarg1);
+
+ public static final native long bitwuzla_sort_fun_get_domain_sorts(long jarg1, long[] jarg2);
+
+ public static final native long bitwuzla_sort_fun_get_codomain(long jarg1);
+
+ public static final native long bitwuzla_sort_fun_get_arity(long jarg1);
+
+ public static final native String bitwuzla_sort_get_uninterpreted_symbol(long jarg1);
+
+ public static final native boolean bitwuzla_sort_is_equal(long jarg1, long jarg2);
+
+ public static final native boolean bitwuzla_sort_is_array(long jarg1);
+
+ public static final native boolean bitwuzla_sort_is_bool(long jarg1);
+
+ public static final native boolean bitwuzla_sort_is_bv(long jarg1);
+
+ public static final native boolean bitwuzla_sort_is_fp(long jarg1);
+
+ public static final native boolean bitwuzla_sort_is_fun(long jarg1);
+
+ public static final native boolean bitwuzla_sort_is_rm(long jarg1);
+
+ public static final native boolean bitwuzla_sort_is_uninterpreted(long jarg1);
+
+ public static final native String bitwuzla_sort_to_string(long jarg1);
+
+ public static final native long bitwuzla_term_hash(long jarg1);
+
+ public static final native int bitwuzla_term_get_kind(long jarg1);
+
+ public static final native long[] bitwuzla_term_get_children(long jarg1, long[] jarg2);
+
+ public static final native long[] bitwuzla_term_get_indices(long jarg1, long[] jarg2);
+
+ public static final native boolean bitwuzla_term_is_indexed(long jarg1);
+
+ public static final native long bitwuzla_term_get_sort(long jarg1);
+
+ public static final native long bitwuzla_term_array_get_index_sort(long jarg1);
+
+ public static final native long bitwuzla_term_array_get_element_sort(long jarg1);
+
+ public static final native long bitwuzla_term_fun_get_domain_sorts(long jarg1, long[] jarg2);
+
+ public static final native long bitwuzla_term_fun_get_codomain_sort(long jarg1);
+
+ public static final native long bitwuzla_term_bv_get_size(long jarg1);
+
+ public static final native long bitwuzla_term_fp_get_exp_size(long jarg1);
+
+ public static final native long bitwuzla_term_fp_get_sig_size(long jarg1);
+
+ public static final native long bitwuzla_term_fun_get_arity(long jarg1);
+
+ public static final native String bitwuzla_term_get_symbol(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_equal_sort(long jarg1, long jarg2);
+
+ public static final native boolean bitwuzla_term_is_array(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_const(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fun(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_var(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_value(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bv_value(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fp_value(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_rm_value(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bool(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bv(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fp(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_rm(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_uninterpreted(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_true(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_false(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bv_value_zero(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bv_value_one(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bv_value_ones(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bv_value_min_signed(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_bv_value_max_signed(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fp_value_pos_zero(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fp_value_neg_zero(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fp_value_pos_inf(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fp_value_neg_inf(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_fp_value_nan(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_rm_value_rna(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_rm_value_rne(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_rm_value_rtn(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_rm_value_rtp(long jarg1);
+
+ public static final native boolean bitwuzla_term_is_rm_value_rtz(long jarg1);
+
+ public static final native boolean bitwuzla_term_value_get_bool(long jarg1);
+
+ public static final native String bitwuzla_term_value_get_str(long jarg1);
+
+ public static final native String bitwuzla_term_value_get_str_fmt(long jarg1, int jarg2);
+
+ public static final native void bitwuzla_term_value_get_fp_ieee(
+ long jarg1, long jarg2, long jarg3, long jarg4, int jarg5);
+
+ public static final native int bitwuzla_term_value_get_rm(long jarg1);
+
+ public static final native String bitwuzla_term_to_string(long jarg1);
+
+ public static final native String bitwuzla_term_to_string_fmt(long jarg1, int jarg2);
+
+ public static final native long bitwuzla_new(long options);
+
+ public static final native void bitwuzla_delete(long env);
+
+ public static final native void bitwuzla_set_termination_callback(
+ long jarg1, long jarg2, long jarg3);
+
+ public static final native long bitwuzla_get_termination_callback_state(long jarg1);
+
+ public static final native void bitwuzla_set_abort_callback(long jarg1);
+
+ public static final native void bitwuzla_push(long env, long numOfLevels);
+
+ public static final native void bitwuzla_pop(long env, long numOfLevel);
+
+ public static final native void bitwuzla_assert(long env, long jarg2);
+
+ public static final native long bitwuzla_get_assertions(long jarg1, long[] jarg2);
+
+ public static final native boolean bitwuzla_is_unsat_assumption(long jarg1, long jarg2);
+
+ public static final native long bitwuzla_get_unsat_assumptions(long jarg1, long[] jarg2);
+
+ public static final native long bitwuzla_get_unsat_core(long env, long[] jarg2);
+
+ public static final native void bitwuzla_simplify(long jarg1);
+
+ public static final native int bitwuzla_check_sat(long env);
+
+ public static final native int bitwuzla_check_sat_assuming(long jarg1, long jarg2, long[] jarg3);
+
+ public static final native long bitwuzla_get_value(long env, long term);
+
+ public static final native void bitwuzla_get_statistics(
+ long jarg1, long jarg2, long jarg3, long[] jarg4);
+
+ public static final native long bitwuzla_mk_array_sort(long index, long element);
+
+ public static final native long bitwuzla_mk_bool_sort();
+
+ public static final native long bitwuzla_mk_bv_sort(long width);
+
+ public static final native long bitwuzla_mk_fp_sort(long exponent, long significant);
+
+ public static final native long bitwuzla_mk_fun_sort(long arity, long[] domain, long codomain);
+
+ public static final native long bitwuzla_mk_rm_sort();
+
+ public static final native long bitwuzla_mk_uninterpreted_sort(String symbol);
+
+ public static final native long bitwuzla_mk_true();
+
+ public static final native long bitwuzla_mk_false();
+
+ public static final native long bitwuzla_mk_bv_zero(long jarg1);
+
+ public static final native long bitwuzla_mk_bv_one(long jarg1);
+
+ public static final native long bitwuzla_mk_bv_ones(long jarg1);
+
+ public static final native long bitwuzla_mk_bv_min_signed(long jarg1);
+
+ public static final native long bitwuzla_mk_bv_max_signed(long jarg1);
+
+ public static final native long bitwuzla_mk_fp_pos_zero(long jarg1);
+
+ public static final native long bitwuzla_mk_fp_neg_zero(long jarg1);
+
+ public static final native long bitwuzla_mk_fp_pos_inf(long jarg1);
+
+ public static final native long bitwuzla_mk_fp_neg_inf(long jarg1);
+
+ public static final native long bitwuzla_mk_fp_nan(long jarg1);
+
+ public static final native long bitwuzla_mk_bv_value(long jarg1, String jarg2, int jarg3);
+
+ public static final native long bitwuzla_mk_bv_value_uint64(long jarg1, long jarg2);
+
+ public static final native long bitwuzla_mk_bv_value_int64(long jarg1, int jarg2);
+
+ public static final native long bitwuzla_mk_fp_value(long jarg1, long jarg2, long jarg3);
+
+ public static final native long bitwuzla_mk_fp_from_real(long jarg1, long jarg2, String jarg3);
+
+ public static final native long bitwuzla_mk_fp_from_rational(
+ long jarg1, long jarg2, String jarg3, String jarg4);
+
+ public static final native long bitwuzla_mk_rm_value(int jarg1);
+
+ public static final native long bitwuzla_mk_term1(int jarg1, long jarg2);
+
+ public static final native long bitwuzla_mk_term2(int jarg1, long jarg2, long jarg3);
+
+ public static final native long bitwuzla_mk_term3(int jarg1, long jarg2, long jarg3, long jarg4);
+
+ public static final native long bitwuzla_mk_term(int jarg1, long jarg2, long[] jarg3);
+
+ public static final native long bitwuzla_mk_term1_indexed1(int jarg1, long jarg2, long jarg3);
+
+ public static final native long bitwuzla_mk_term1_indexed2(
+ int jarg1, long jarg2, long jarg3, long jarg4);
+
+ public static final native long bitwuzla_mk_term2_indexed1(
+ int jarg1, long jarg2, long jarg3, long jarg4);
+
+ public static final native long bitwuzla_mk_term2_indexed2(
+ int jarg1, long jarg2, long jarg3, long jarg4, long jarg5);
+
+ public static final native long bitwuzla_mk_term_indexed(
+ int jarg1, long jarg2, long[] jarg3, long jarg4, long[] jarg5);
+
+ public static final native long bitwuzla_mk_const(long jarg1, String jarg2);
+
+ public static final native long bitwuzla_mk_const_array(long jarg1, long jarg2);
+
+ public static final native long bitwuzla_mk_var(long jarg1, String jarg2);
+
+ public static final native long bitwuzla_substitute_term(
+ long jarg1, long jarg2, long[] jarg3, long[] jarg4);
+
+ public static final native void bitwuzla_substitute_terms(
+ long sizeOfTermsToSubstituteIn,
+ long[] termsToSubstituteIn,
+ long sizeOfSubstitutionMap,
+ long[] mapKeys,
+ long[] mapValues);
+
+ public static final native void bitwuzla_parser_delete(long jarg1);
+
+ public static final native String bitwuzla_parser_parse(long jarg1, boolean jarg2);
+
+ public static final native long bitwuzla_parser_get_bitwuzla(long jarg1);
+
+ // This returns the assertions of the input String as formulas individually
+ public static final native long[] parse(String jarg);
+
+ /**
+ * Dumps the SMT2 String representation of a entered Bitwuzla term.
+ *
+ * @param term Bitwuzla term.
+ * @param baseOfValueInterpretation base of the values to be printed. I.e. 2, 10 or 16.
+ * @return String of the term.
+ */
+ public static final native String dump_formula_smt2(long term, int baseOfValueInterpretation);
+
+ /**
+ * Prints the assertion stack of the entered Bitwuzla environment.
+ *
+ * @param env a Bitwuzla environment where the assertion stack should be printed.
+ * @param baseOfValueInterpretation base of the values to be printed. I.e. 2, 10 or 16.
+ * @return String of the terms on the assertion stack.
+ */
+ public static final native String dump_assertions_smt2(long env, int baseOfValueInterpretation);
+
+ /**
+ * Sets termination callback to chosen implementation of a method.
+ *
+ * @param env instance
+ * @param terminationCallback TerminationCallback method
+ * @return address to helper struct. Call method boolector_free_termination with it to free its
+ * ressources after termination!
+ */
+ protected static native long set_termination(long env, TerminationCallback terminationCallback);
+
+ /**
+ * Frees resources of the termination callback function. Call ONLY after termination has occured
+ * with the return value of set_termination of its instance!
+ *
+ * @param helper address to helper struct used in termination callback.
+ */
+ protected static native void free_termination(long helper);
+
+ /** This is used to get the methodID for the JNI call to the termination callback method. */
+ interface TerminationCallback {
+ boolean shouldTerminate() throws InterruptedException;
+ }
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaKind.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaKind.java
new file mode 100644
index 0000000000..430c46069d
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaKind.java
@@ -0,0 +1,314 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+/* ----------------------------------------------------------------------------
+ * This file was automatically generated by SWIG (http://www.swig.org).
+ * Version 4.0.2
+ *
+ * Do not make changes to this file unless you know what you are doing--modify
+ * the SWIG interface file instead.
+ * ----------------------------------------------------------------------------- */
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+public final class BitwuzlaKind {
+ // FIXME: We should use SWIG to auto-generate the enum for us. This class will break whenever
+ // bitwuzla changes their definitions.
+
+ private static int swigNext = 0;
+ private final int swigValue;
+ private final String swigName;
+ public static final BitwuzlaKind BITWUZLA_KIND_CONSTANT =
+ BitwuzlaKind.of("BITWUZLA_KIND_CONSTANT", BitwuzlaJNI.BITWUZLA_KIND_CONSTANT_get());
+ public static final BitwuzlaKind BITWUZLA_KIND_CONST_ARRAY =
+ BitwuzlaKind.of("BITWUZLA_KIND_CONST_ARRAY");
+ public static final BitwuzlaKind BITWUZLA_KIND_VALUE = BitwuzlaKind.of("BITWUZLA_KIND_VALUE");
+ public static final BitwuzlaKind BITWUZLA_KIND_VARIABLE =
+ BitwuzlaKind.of("BITWUZLA_KIND_VARIABLE");
+ public static final BitwuzlaKind BITWUZLA_KIND_AND = BitwuzlaKind.of("BITWUZLA_KIND_AND");
+ public static final BitwuzlaKind BITWUZLA_KIND_DISTINCT =
+ BitwuzlaKind.of("BITWUZLA_KIND_DISTINCT");
+ public static final BitwuzlaKind BITWUZLA_KIND_EQUAL = BitwuzlaKind.of("BITWUZLA_KIND_EQUAL");
+ public static final BitwuzlaKind BITWUZLA_KIND_IFF = BitwuzlaKind.of("BITWUZLA_KIND_IFF");
+ public static final BitwuzlaKind BITWUZLA_KIND_IMPLIES = BitwuzlaKind.of("BITWUZLA_KIND_IMPLIES");
+ public static final BitwuzlaKind BITWUZLA_KIND_NOT = BitwuzlaKind.of("BITWUZLA_KIND_NOT");
+ public static final BitwuzlaKind BITWUZLA_KIND_OR = BitwuzlaKind.of("BITWUZLA_KIND_OR");
+ public static final BitwuzlaKind BITWUZLA_KIND_XOR = BitwuzlaKind.of("BITWUZLA_KIND_XOR");
+ public static final BitwuzlaKind BITWUZLA_KIND_ITE = BitwuzlaKind.of("BITWUZLA_KIND_ITE");
+ public static final BitwuzlaKind BITWUZLA_KIND_EXISTS = BitwuzlaKind.of("BITWUZLA_KIND_EXISTS");
+ public static final BitwuzlaKind BITWUZLA_KIND_FORALL = BitwuzlaKind.of("BITWUZLA_KIND_FORALL");
+ public static final BitwuzlaKind BITWUZLA_KIND_APPLY = BitwuzlaKind.of("BITWUZLA_KIND_APPLY");
+ public static final BitwuzlaKind BITWUZLA_KIND_LAMBDA = BitwuzlaKind.of("BITWUZLA_KIND_LAMBDA");
+ public static final BitwuzlaKind BITWUZLA_KIND_ARRAY_SELECT =
+ BitwuzlaKind.of("BITWUZLA_KIND_ARRAY_SELECT");
+ public static final BitwuzlaKind BITWUZLA_KIND_ARRAY_STORE =
+ BitwuzlaKind.of("BITWUZLA_KIND_ARRAY_STORE");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ADD = BitwuzlaKind.of("BITWUZLA_KIND_BV_ADD");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_AND = BitwuzlaKind.of("BITWUZLA_KIND_BV_AND");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ASHR = BitwuzlaKind.of("BITWUZLA_KIND_BV_ASHR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_COMP = BitwuzlaKind.of("BITWUZLA_KIND_BV_COMP");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_CONCAT =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_CONCAT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_DEC = BitwuzlaKind.of("BITWUZLA_KIND_BV_DEC");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_INC = BitwuzlaKind.of("BITWUZLA_KIND_BV_INC");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_MUL = BitwuzlaKind.of("BITWUZLA_KIND_BV_MUL");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_NAND = BitwuzlaKind.of("BITWUZLA_KIND_BV_NAND");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_NEG = BitwuzlaKind.of("BITWUZLA_KIND_BV_NEG");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_NEG_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_NEG_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_NOR = BitwuzlaKind.of("BITWUZLA_KIND_BV_NOR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_NOT = BitwuzlaKind.of("BITWUZLA_KIND_BV_NOT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_OR = BitwuzlaKind.of("BITWUZLA_KIND_BV_OR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_REDAND =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_REDAND");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_REDOR =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_REDOR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_REDXOR =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_REDXOR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ROL = BitwuzlaKind.of("BITWUZLA_KIND_BV_ROL");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ROR = BitwuzlaKind.of("BITWUZLA_KIND_BV_ROR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SADD_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_SADD_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SDIV_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_SDIV_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SDIV = BitwuzlaKind.of("BITWUZLA_KIND_BV_SDIV");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SGE = BitwuzlaKind.of("BITWUZLA_KIND_BV_SGE");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SGT = BitwuzlaKind.of("BITWUZLA_KIND_BV_SGT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SHL = BitwuzlaKind.of("BITWUZLA_KIND_BV_SHL");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SHR = BitwuzlaKind.of("BITWUZLA_KIND_BV_SHR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SLE = BitwuzlaKind.of("BITWUZLA_KIND_BV_SLE");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SLT = BitwuzlaKind.of("BITWUZLA_KIND_BV_SLT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SMOD = BitwuzlaKind.of("BITWUZLA_KIND_BV_SMOD");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SMUL_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_SMUL_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SREM = BitwuzlaKind.of("BITWUZLA_KIND_BV_SREM");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SSUB_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_SSUB_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SUB = BitwuzlaKind.of("BITWUZLA_KIND_BV_SUB");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_UADD_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_UADD_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_UDIV = BitwuzlaKind.of("BITWUZLA_KIND_BV_UDIV");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_UGE = BitwuzlaKind.of("BITWUZLA_KIND_BV_UGE");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_UGT = BitwuzlaKind.of("BITWUZLA_KIND_BV_UGT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ULE = BitwuzlaKind.of("BITWUZLA_KIND_BV_ULE");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ULT = BitwuzlaKind.of("BITWUZLA_KIND_BV_ULT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_UMUL_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_UMUL_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_UREM = BitwuzlaKind.of("BITWUZLA_KIND_BV_UREM");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_USUB_OVERFLOW =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_USUB_OVERFLOW");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_XNOR = BitwuzlaKind.of("BITWUZLA_KIND_BV_XNOR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_XOR = BitwuzlaKind.of("BITWUZLA_KIND_BV_XOR");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_EXTRACT =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_EXTRACT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_REPEAT =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_REPEAT");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ROLI = BitwuzlaKind.of("BITWUZLA_KIND_BV_ROLI");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_RORI = BitwuzlaKind.of("BITWUZLA_KIND_BV_RORI");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_SIGN_EXTEND =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_SIGN_EXTEND");
+ public static final BitwuzlaKind BITWUZLA_KIND_BV_ZERO_EXTEND =
+ BitwuzlaKind.of("BITWUZLA_KIND_BV_ZERO_EXTEND");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_ABS = BitwuzlaKind.of("BITWUZLA_KIND_FP_ABS");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_ADD = BitwuzlaKind.of("BITWUZLA_KIND_FP_ADD");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_DIV = BitwuzlaKind.of("BITWUZLA_KIND_FP_DIV");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_EQUAL =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_EQUAL");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_FMA = BitwuzlaKind.of("BITWUZLA_KIND_FP_FMA");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_FP = BitwuzlaKind.of("BITWUZLA_KIND_FP_FP");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_GEQ = BitwuzlaKind.of("BITWUZLA_KIND_FP_GEQ");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_GT = BitwuzlaKind.of("BITWUZLA_KIND_FP_GT");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_IS_INF =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_IS_INF");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_IS_NAN =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_IS_NAN");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_IS_NEG =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_IS_NEG");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_IS_NORMAL =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_IS_NORMAL");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_IS_POS =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_IS_POS");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_IS_SUBNORMAL =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_IS_SUBNORMAL");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_IS_ZERO =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_IS_ZERO");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_LEQ = BitwuzlaKind.of("BITWUZLA_KIND_FP_LEQ");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_LT = BitwuzlaKind.of("BITWUZLA_KIND_FP_LT");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_MAX = BitwuzlaKind.of("BITWUZLA_KIND_FP_MAX");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_MIN = BitwuzlaKind.of("BITWUZLA_KIND_FP_MIN");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_MUL = BitwuzlaKind.of("BITWUZLA_KIND_FP_MUL");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_NEG = BitwuzlaKind.of("BITWUZLA_KIND_FP_NEG");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_REM = BitwuzlaKind.of("BITWUZLA_KIND_FP_REM");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_RTI = BitwuzlaKind.of("BITWUZLA_KIND_FP_RTI");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_SQRT = BitwuzlaKind.of("BITWUZLA_KIND_FP_SQRT");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_SUB = BitwuzlaKind.of("BITWUZLA_KIND_FP_SUB");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_TO_FP_FROM_BV =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_TO_FP_FROM_BV");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_TO_FP_FROM_FP =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_TO_FP_FROM_FP");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_TO_FP_FROM_SBV =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_TO_FP_FROM_SBV");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_TO_FP_FROM_UBV =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_TO_FP_FROM_UBV");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_TO_SBV =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_TO_SBV");
+ public static final BitwuzlaKind BITWUZLA_KIND_FP_TO_UBV =
+ BitwuzlaKind.of("BITWUZLA_KIND_FP_TO_UBV");
+ public static final BitwuzlaKind BITWUZLA_KIND_NUM_KINDS =
+ BitwuzlaKind.of("BITWUZLA_KIND_NUM_KINDS");
+
+ public int swigValue() {
+ return swigValue;
+ }
+
+ @Override
+ public String toString() {
+ return swigName;
+ }
+
+ public static BitwuzlaKind swigToEnum(int swigValue) {
+ if (swigValue < swigValues.length
+ && swigValue >= 0
+ && swigValues[swigValue].swigValue == swigValue) {
+ return swigValues[swigValue];
+ }
+ for (int i = 0; i < swigValues.length; i++) {
+ if (swigValues[i].swigValue == swigValue) {
+ return swigValues[i];
+ }
+ }
+ throw new IllegalArgumentException(
+ "No enum " + BitwuzlaKind.class + " with value " + swigValue);
+ }
+
+ private BitwuzlaKind(String swigName) {
+ this.swigName = swigName;
+ this.swigValue = BitwuzlaKind.swigNext;
+ }
+
+ private static BitwuzlaKind of(String swigName) {
+ BitwuzlaKind kind = new BitwuzlaKind(swigName);
+ BitwuzlaKind.swigNext++;
+ return kind;
+ }
+
+ private BitwuzlaKind(String swigName, int swigValue) {
+ this.swigName = swigName;
+ this.swigValue = swigValue;
+ }
+
+ private static BitwuzlaKind of(String swigName, int swigValue) {
+ BitwuzlaKind kind = new BitwuzlaKind(swigName, swigValue);
+ BitwuzlaKind.swigNext = swigValue + 1;
+ return kind;
+ }
+
+ private static BitwuzlaKind[] swigValues = {
+ BITWUZLA_KIND_CONSTANT,
+ BITWUZLA_KIND_CONST_ARRAY,
+ BITWUZLA_KIND_VALUE,
+ BITWUZLA_KIND_VARIABLE,
+ BITWUZLA_KIND_AND,
+ BITWUZLA_KIND_DISTINCT,
+ BITWUZLA_KIND_EQUAL,
+ BITWUZLA_KIND_IFF,
+ BITWUZLA_KIND_IMPLIES,
+ BITWUZLA_KIND_NOT,
+ BITWUZLA_KIND_OR,
+ BITWUZLA_KIND_XOR,
+ BITWUZLA_KIND_ITE,
+ BITWUZLA_KIND_EXISTS,
+ BITWUZLA_KIND_FORALL,
+ BITWUZLA_KIND_APPLY,
+ BITWUZLA_KIND_LAMBDA,
+ BITWUZLA_KIND_ARRAY_SELECT,
+ BITWUZLA_KIND_ARRAY_STORE,
+ BITWUZLA_KIND_BV_ADD,
+ BITWUZLA_KIND_BV_AND,
+ BITWUZLA_KIND_BV_ASHR,
+ BITWUZLA_KIND_BV_COMP,
+ BITWUZLA_KIND_BV_CONCAT,
+ BITWUZLA_KIND_BV_DEC,
+ BITWUZLA_KIND_BV_INC,
+ BITWUZLA_KIND_BV_MUL,
+ BITWUZLA_KIND_BV_NAND,
+ BITWUZLA_KIND_BV_NEG,
+ BITWUZLA_KIND_BV_NEG_OVERFLOW,
+ BITWUZLA_KIND_BV_NOR,
+ BITWUZLA_KIND_BV_NOT,
+ BITWUZLA_KIND_BV_OR,
+ BITWUZLA_KIND_BV_REDAND,
+ BITWUZLA_KIND_BV_REDOR,
+ BITWUZLA_KIND_BV_REDXOR,
+ BITWUZLA_KIND_BV_ROL,
+ BITWUZLA_KIND_BV_ROR,
+ BITWUZLA_KIND_BV_SADD_OVERFLOW,
+ BITWUZLA_KIND_BV_SDIV_OVERFLOW,
+ BITWUZLA_KIND_BV_SDIV,
+ BITWUZLA_KIND_BV_SGE,
+ BITWUZLA_KIND_BV_SGT,
+ BITWUZLA_KIND_BV_SHL,
+ BITWUZLA_KIND_BV_SHR,
+ BITWUZLA_KIND_BV_SLE,
+ BITWUZLA_KIND_BV_SLT,
+ BITWUZLA_KIND_BV_SMOD,
+ BITWUZLA_KIND_BV_SMUL_OVERFLOW,
+ BITWUZLA_KIND_BV_SREM,
+ BITWUZLA_KIND_BV_SSUB_OVERFLOW,
+ BITWUZLA_KIND_BV_SUB,
+ BITWUZLA_KIND_BV_UADD_OVERFLOW,
+ BITWUZLA_KIND_BV_UDIV,
+ BITWUZLA_KIND_BV_UGE,
+ BITWUZLA_KIND_BV_UGT,
+ BITWUZLA_KIND_BV_ULE,
+ BITWUZLA_KIND_BV_ULT,
+ BITWUZLA_KIND_BV_UMUL_OVERFLOW,
+ BITWUZLA_KIND_BV_UREM,
+ BITWUZLA_KIND_BV_USUB_OVERFLOW,
+ BITWUZLA_KIND_BV_XNOR,
+ BITWUZLA_KIND_BV_XOR,
+ BITWUZLA_KIND_BV_EXTRACT,
+ BITWUZLA_KIND_BV_REPEAT,
+ BITWUZLA_KIND_BV_ROLI,
+ BITWUZLA_KIND_BV_RORI,
+ BITWUZLA_KIND_BV_SIGN_EXTEND,
+ BITWUZLA_KIND_BV_ZERO_EXTEND,
+ BITWUZLA_KIND_FP_ABS,
+ BITWUZLA_KIND_FP_ADD,
+ BITWUZLA_KIND_FP_DIV,
+ BITWUZLA_KIND_FP_EQUAL,
+ BITWUZLA_KIND_FP_FMA,
+ BITWUZLA_KIND_FP_FP,
+ BITWUZLA_KIND_FP_GEQ,
+ BITWUZLA_KIND_FP_GT,
+ BITWUZLA_KIND_FP_IS_INF,
+ BITWUZLA_KIND_FP_IS_NAN,
+ BITWUZLA_KIND_FP_IS_NEG,
+ BITWUZLA_KIND_FP_IS_NORMAL,
+ BITWUZLA_KIND_FP_IS_POS,
+ BITWUZLA_KIND_FP_IS_SUBNORMAL,
+ BITWUZLA_KIND_FP_IS_ZERO,
+ BITWUZLA_KIND_FP_LEQ,
+ BITWUZLA_KIND_FP_LT,
+ BITWUZLA_KIND_FP_MAX,
+ BITWUZLA_KIND_FP_MIN,
+ BITWUZLA_KIND_FP_MUL,
+ BITWUZLA_KIND_FP_NEG,
+ BITWUZLA_KIND_FP_REM,
+ BITWUZLA_KIND_FP_RTI,
+ BITWUZLA_KIND_FP_SQRT,
+ BITWUZLA_KIND_FP_SUB,
+ BITWUZLA_KIND_FP_TO_FP_FROM_BV,
+ BITWUZLA_KIND_FP_TO_FP_FROM_FP,
+ BITWUZLA_KIND_FP_TO_FP_FROM_SBV,
+ BITWUZLA_KIND_FP_TO_FP_FROM_UBV,
+ BITWUZLA_KIND_FP_TO_SBV,
+ BITWUZLA_KIND_FP_TO_UBV,
+ BITWUZLA_KIND_NUM_KINDS,
+ };
+}
diff --git a/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
new file mode 100644
index 0000000000..d9ea7d77d0
--- /dev/null
+++ b/src/org/sosy_lab/java_smt/solvers/bitwuzla/BitwuzlaModel.java
@@ -0,0 +1,238 @@
+// This file is part of JavaSMT,
+// an API wrapper for a collection of SMT solvers:
+// https://github.com/sosy-lab/java-smt
+//
+// SPDX-FileCopyrightText: 2023 Dirk Beyer
+//
+// SPDX-License-Identifier: Apache-2.0
+
+package org.sosy_lab.java_smt.solvers.bitwuzla;
+
+import com.google.common.base.Preconditions;
+import com.google.common.collect.ImmutableList;
+import com.google.common.collect.ImmutableSet;
+import java.util.ArrayDeque;
+import java.util.ArrayList;
+import java.util.Collection;
+import java.util.Deque;
+import java.util.HashSet;
+import java.util.List;
+import java.util.Set;
+import org.checkerframework.checker.nullness.qual.Nullable;
+import org.sosy_lab.java_smt.basicimpl.AbstractModel;
+
+class BitwuzlaModel extends AbstractModel {
+
+ // The prover env, not the creator env!
+ private final long bitwuzlaEnv;
+
+ private final BitwuzlaTheoremProver prover;
+
+ private final BitwuzlaFormulaCreator bitwuzlaCreator;
+ private final ImmutableList assertedTerms;
+
+ protected BitwuzlaModel(
+ long bitwuzlaEnv,
+ BitwuzlaTheoremProver prover,
+ BitwuzlaFormulaCreator bitwuzlaCreator,
+ Collection assertedTerms) {
+ super(prover, bitwuzlaCreator);
+ this.bitwuzlaEnv = bitwuzlaEnv;
+ this.prover = prover;
+ this.bitwuzlaCreator = bitwuzlaCreator;
+ this.assertedTerms = ImmutableList.copyOf(assertedTerms);
+ }
+
+ /** Build a list of assignments that stays valid after closing the model. */
+ @Override
+ public ImmutableList asList() {
+ Preconditions.checkState(!isClosed());
+ Preconditions.checkState(!prover.isClosed(), "Cannot use model after prover is closed");
+ ImmutableSet.Builder variablesBuilder = ImmutableSet.builder();
+ Deque queue = new ArrayDeque<>(assertedTerms);
+ while (!queue.isEmpty()) {
+ long term = queue.removeFirst();
+ long[] children = BitwuzlaJNI.bitwuzla_term_get_children(term, new long[1]);
+ // The term might be a value (variable or const, w only variable having a symbol)
+ // an array, an UF, or an FP or a function.
+ // Functions are just split into their children and those are traversed
+ if (BitwuzlaJNI.bitwuzla_term_is_rm(term)) {
+ // Do nothing
+ } else if (BitwuzlaJNI.bitwuzla_term_get_kind(term)
+ == BitwuzlaKind.BITWUZLA_KIND_APPLY.swigValue()) {
+ variablesBuilder.add(getUFAssignment(term));
+ for (int i = 1; i < children.length; i++) {
+ queue.addLast(children[i]);
+ }
+
+ } else if (BitwuzlaJNI.bitwuzla_term_is_bv(term)
+ && BitwuzlaJNI.bitwuzla_term_is_const(term)) {
+ variablesBuilder.add(getSimpleAssignment(term));
+
+ } else if (BitwuzlaJNI.bitwuzla_term_is_bool(term)
+ && BitwuzlaJNI.bitwuzla_term_is_const(term)) {
+ variablesBuilder.add(getSimpleAssignment(term));
+
+ } else if (BitwuzlaJNI.bitwuzla_term_is_fp(term)
+ && BitwuzlaJNI.bitwuzla_term_is_const(term)) {
+ // We can't eval FP properly at the moment, we just return whatever the solver gives us
+ // (BV representation of the FP)
+ variablesBuilder.add(getSimpleAssignment(term));
+
+ } else if (BitwuzlaJNI.bitwuzla_term_is_array(term)
+ && BitwuzlaJNI.bitwuzla_term_is_const(term)) {
+ variablesBuilder.addAll(getArrayAssignment(term));
+
+ } else {
+ for (long child : children) {
+ queue.addLast(child);
+ }
+ }
+ }
+
+ return variablesBuilder.build().asList();
+ }
+
+ private ValueAssignment getSimpleAssignment(long pTerm) {
+ List