From e4c43587fc773632a781ea750ec1b91dcd8d6217 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 4 Feb 2024 22:56:46 +0100 Subject: [PATCH 1/2] Evaluator: cleanup --- .../java_smt/basicimpl/AbstractEvaluator.java | 8 +- .../java_smt/solvers/yices2/Yices2Model.java | 2 +- .../solvers/yices2/Yices2NativeApiTest.java | 81 +------------------ 3 files changed, 5 insertions(+), 86 deletions(-) diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java index e06de97054..fb6e46f8f9 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java @@ -31,8 +31,8 @@ public abstract class AbstractEvaluator implements Ev protected AbstractEvaluator( AbstractProver pProver, FormulaCreator creator) { - this.prover = pProver; - this.creator = creator; + this.prover = Preconditions.checkNotNull(pProver); + this.creator = Preconditions.checkNotNull(creator); } @SuppressWarnings("unchecked") @@ -126,9 +126,7 @@ protected boolean isClosed() { @Override public void close() { - if (prover != null) { // can be NULL for testing - prover.unregisterEvaluator(this); - } + prover.unregisterEvaluator(this); closed = true; } } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java index 0386251baa..201784138a 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2Model.java @@ -68,7 +68,7 @@ public class Yices2Model extends AbstractModel { protected Yices2Model(long model, Yices2TheoremProver prover, Yices2FormulaCreator pCreator) { super(prover, pCreator); this.model = model; - this.prover = prover; // can be NULL for testing + this.prover = prover; this.formulaCreator = Preconditions.checkNotNull(pCreator); } diff --git a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java index eb31d0f0bb..4cba71dd14 100644 --- a/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java +++ b/src/org/sosy_lab/java_smt/solvers/yices2/Yices2NativeApiTest.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2020 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 OR GPL-3.0-or-later @@ -17,15 +17,12 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_EQ_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_NOT_TERM; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_OR_TERM; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YICES_STATUS_SAT; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.YVAL_RATIONAL; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_add; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_and; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_and2; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_application; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_arith_eq_atom; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_arith_gt_atom; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_arith_lt_atom; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_assert_formula; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bool_const_value; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bool_type; @@ -43,23 +40,19 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_bvxor2; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_check_context; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_context_disable_option; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_def_terms; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_eq; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_exit; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_false; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_free_config; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_free_context; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_function_type; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_model; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_term_name; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_get_value; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_idiv; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_iff; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_init; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_int32; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_int64; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_int_type; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_model_to_string; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_mul; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_named_variable; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_new_config; @@ -73,9 +66,7 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_parse_term; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_product_component; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_proj_arg; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_push; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_rational32; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_real_type; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_redand; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_set_config; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_set_term_name; @@ -90,7 +81,6 @@ import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_num_children; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_term_to_string; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_true; -import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_val_get_mpq; import static org.sosy_lab.java_smt.solvers.yices2.Yices2NativeApi.yices_zero_extend; import com.google.common.base.Joiner; @@ -108,7 +98,6 @@ import org.junit.Test; import org.sosy_lab.common.NativeLibraries; import org.sosy_lab.common.rationals.Rational; -import org.sosy_lab.java_smt.api.Model; @SuppressWarnings("unused") public class Yices2NativeApiTest { @@ -451,74 +440,6 @@ public void uf2Constructor() { assertThat(yices_term_constructor(app)).isEqualTo(YICES_APP_TERM); } - @SuppressWarnings("resource") - @Test - public void modelTest() { - int varx = yices_named_variable(yices_real_type(), "x"); - int eq = yices_arith_eq_atom(varx, yices_int32(10)); - int query = yices_named_variable(yices_real_type(), "x"); - Yices2FormulaCreator creator = new Yices2FormulaCreator(); - yices_push(env); - yices_assert_formula(env, eq); - System.out.println("varx: " + varx); - System.out.println("query: " + query); - if (yices_check_context(env, 0) == YICES_STATUS_SAT) { - Model m = new Yices2Model(yices_get_model(env, 1), null, creator); - Object val = m.evaluate(creator.encapsulateWithTypeOf(varx)); - System.out.println(val); - m.close(); - } - } - - @SuppressWarnings("resource") - @Test - public void modelExplorationTest() { - int x = yices_int32(5); - int y = yices_int32(7); - int z = yices_named_variable(yices_int_type(), "z"); - int gt = yices_arith_gt_atom(z, x); - int lt = yices_arith_lt_atom(z, y); - int x2 = yices_int32(333); - int y2 = yices_int32(335); - int z2 = yices_named_variable(yices_int_type(), "z2"); - int gt2 = yices_arith_gt_atom(z2, x2); - int lt2 = yices_arith_lt_atom(z2, y2); - int sub = yices_sub(z2, z); - int eq = yices_arith_eq_atom(sub, yices_int32(328)); - Yices2FormulaCreator creator = new Yices2FormulaCreator(); - yices_push(env); - yices_assert_formula(env, gt); - yices_assert_formula(env, lt); - yices_assert_formula(env, gt2); - yices_assert_formula(env, lt2); - yices_assert_formula(env, eq); - if (yices_check_context(env, 0) == YICES_STATUS_SAT) { - long model = yices_get_model(env, 1); - Model m = new Yices2Model(model, null, creator); - System.out.println(yices_model_to_string(model)); - Object val = m.evaluate(creator.encapsulateWithTypeOf(eq)); - System.out.println(val); - int addT = yices_add(z, z2); - Object val2 = m.evaluate(creator.encapsulateWithTypeOf(addT)); - System.out.println(val2); - System.out.println("DEFINED TERMS"); - int[] terms = yices_def_terms(model); - for (int term : terms) { - System.out.println(yices_term_to_string(term)); - System.out.println("Term id is: " + term); - int[] yval = yices_get_value(model, term); - System.out.println("Node id is: " + yval[0]); - System.out.println("Node tag is: " + yval[1]); - if (yval[1] == YVAL_RATIONAL) { - System.out.println("Value is: " + yices_val_get_mpq(model, yval[0], yval[1])); - } - } - m.close(); - } else { - throw new IllegalArgumentException("The environment is not solvable!"); - } - } - @Test public void parseTerm() { // int x = yices_parse_term("define x::int"); From d2b1532ea06edeecf1af26b0fc134789731f9502 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 4 Feb 2024 22:58:25 +0100 Subject: [PATCH 2/2] #352: add model-evaluation for floating-point numbers. --- src/org/sosy_lab/java_smt/api/Evaluator.java | 9 +- .../java_smt/api/FloatingPointNumber.java | 130 ++++++++++++++++++ .../sosy_lab/java_smt/api/FormulaType.java | 11 +- .../java_smt/basicimpl/AbstractEvaluator.java | 10 +- .../java_smt/basicimpl/CachingModel.java | 7 + .../delegate/statistics/StatisticsModel.java | 8 ++ .../synchronize/SynchronizedModel.java | 9 ++ .../SynchronizedModelWithContext.java | 7 + .../solvers/cvc4/CVC4FormulaCreator.java | 40 +++--- .../solvers/cvc5/CVC5FormulaCreator.java | 47 ++----- .../mathsat5/Mathsat5FormulaCreator.java | 32 +++-- .../java_smt/solvers/z3/Z3FormulaCreator.java | 67 ++++++++- .../test/FloatingPointFormulaManagerTest.java | 96 ++++++------- .../test/FloatingPointNumberTest.java | 97 +++++++++++++ src/org/sosy_lab/java_smt/test/ModelTest.java | 13 +- 15 files changed, 457 insertions(+), 126 deletions(-) create mode 100644 src/org/sosy_lab/java_smt/api/FloatingPointNumber.java create mode 100644 src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java diff --git a/src/org/sosy_lab/java_smt/api/Evaluator.java b/src/org/sosy_lab/java_smt/api/Evaluator.java index 9ae3964f04..03ca8b00a0 100644 --- a/src/org/sosy_lab/java_smt/api/Evaluator.java +++ b/src/org/sosy_lab/java_smt/api/Evaluator.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2022 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -106,6 +106,13 @@ public interface Evaluator extends AutoCloseable { */ @Nullable String evaluate(EnumerationFormula formula); + /** + * Type-safe evaluation for floating-point formulas. + * + *

The formula does not need to be a variable, we also allow complex expression. + */ + @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula); + /** * Free resources associated with this evaluator (existing {@link Formula} instances stay valid, * but {@link #evaluate(Formula)} etc. must not be called again). diff --git a/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java new file mode 100644 index 0000000000..302df2f162 --- /dev/null +++ b/src/org/sosy_lab/java_smt/api/FloatingPointNumber.java @@ -0,0 +1,130 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.api; + +import com.google.auto.value.AutoValue; +import com.google.common.base.Preconditions; +import com.google.errorprone.annotations.Immutable; +import java.math.BigInteger; +import java.util.BitSet; + +/** + * Represents a floating-point number with customizable precision, consisting of sign, exponent, and + * mantissa components. + */ +@Immutable +@AutoValue +public abstract class FloatingPointNumber { + + public static final int SINGLE_PRECISION_EXPONENT_SIZE = 8; + public static final int SINGLE_PRECISION_MANTISSA_SIZE = 23; + 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). */ + public abstract boolean getSign(); + + /** 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. */ + public abstract BigInteger getMantissa(); + + public abstract int getExponentSize(); + + public abstract int getMantissaSize(); + + public static FloatingPointNumber of( + boolean sign, BigInteger exponent, BigInteger mantissa, int exponentSize, int mantissaSize) { + Preconditions.checkArgument(exponent.bitLength() <= exponentSize); + Preconditions.checkArgument(mantissa.bitLength() <= mantissaSize); + Preconditions.checkArgument(exponent.compareTo(BigInteger.ZERO) >= 0); + Preconditions.checkArgument(mantissa.compareTo(BigInteger.ZERO) >= 0); + return new AutoValue_FloatingPointNumber(sign, exponent, mantissa, exponentSize, mantissaSize); + } + + public static FloatingPointNumber of(String bits, int exponentSize, int mantissaSize) { + Preconditions.checkArgument(0 < exponentSize); + Preconditions.checkArgument(0 < mantissaSize); + Preconditions.checkArgument(bits.length() == 1 + exponentSize + mantissaSize); + Preconditions.checkArgument(bits.chars().allMatch(c -> c == '0' || c == '1')); + boolean sign = bits.charAt(0) == '1'; + BigInteger exponent = new BigInteger(bits.substring(1, 1 + exponentSize), 2); + BigInteger mantissa = + new BigInteger(bits.substring(1 + exponentSize, 1 + exponentSize + mantissaSize), 2); + return of(sign, exponent, mantissa, exponentSize, mantissaSize); + } + + private boolean isSinglePrecision() { + return getExponentSize() == SINGLE_PRECISION_EXPONENT_SIZE + && getMantissaSize() == SINGLE_PRECISION_MANTISSA_SIZE; + } + + private boolean isDoublePrecision() { + return getExponentSize() == DOUBLE_PRECISION_EXPONENT_SIZE + && getMantissaSize() == DOUBLE_PRECISION_MANTISSA_SIZE; + } + + /** compute a representation as Java-based float value, if possible. */ + public float floatValue() { + Preconditions.checkArgument( + isSinglePrecision(), + "Can not represent floating point number %s as Java-based float value.", + this); + var bits = getBits(); + return Float.intBitsToFloat(bits.length() == 0 ? 0 : (int) bits.toLongArray()[0]); + } + + /** compute a representation as Java-based double value, if possible. */ + public double doubleValue() { + Preconditions.checkArgument( + isSinglePrecision() || isDoublePrecision(), + "Can not represent floating point number %s as Java-based double value.", + this); + if (isSinglePrecision()) { + // lets be nice to the user and automatically convert from single to double precision + return floatValue(); + } + var bits = getBits(); + return Double.longBitsToDouble(bits.length() == 0 ? 0 : getBits().toLongArray()[0]); + } + + private BitSet getBits() { + var mantissaSize = getMantissaSize(); + var exponentSize = getExponentSize(); + var mantissa = getMantissa(); + var exponent = getExponent(); + var bits = new BitSet(1 + exponentSize + mantissaSize); + if (getSign()) { + bits.set(exponentSize + mantissaSize); + } + for (int i = 0; i < exponentSize; i++) { + bits.set(mantissaSize + i, exponent.testBit(i)); + } + for (int i = 0; i < mantissaSize; i++) { + bits.set(i, mantissa.testBit(i)); + } + return bits; + } + + /** + * Return a bit-representation of sign-bit, exponent, and mantissa, i.e., a concatenation of their + * bit-representations in this exact ordering. + */ + @Override + public final String toString() { + var length = 1 + getExponentSize() + getMantissaSize(); + var str = new StringBuilder(length); + var bits = getBits(); + for (int i = 0; i < length; i++) { + str.append(bits.get(i) ? '1' : '0'); + } + return str.reverse().toString(); + } +} diff --git a/src/org/sosy_lab/java_smt/api/FormulaType.java b/src/org/sosy_lab/java_smt/api/FormulaType.java index 1c91663682..0dbcb96534 100644 --- a/src/org/sosy_lab/java_smt/api/FormulaType.java +++ b/src/org/sosy_lab/java_smt/api/FormulaType.java @@ -8,6 +8,11 @@ package org.sosy_lab.java_smt.api; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_EXPONENT_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE; + import com.google.common.base.Joiner; import com.google.common.base.Preconditions; import com.google.common.base.Splitter; @@ -213,8 +218,10 @@ public static FloatingPointType getDoublePrecisionFloatingPointType() { @Immutable public static final class FloatingPointType extends FormulaType { - private static final FloatingPointType SINGLE_PRECISION_FP_TYPE = new FloatingPointType(8, 23); - private static final FloatingPointType DOUBLE_PRECISION_FP_TYPE = new FloatingPointType(11, 52); + private static final FloatingPointType SINGLE_PRECISION_FP_TYPE = + new FloatingPointType(SINGLE_PRECISION_EXPONENT_SIZE, SINGLE_PRECISION_MANTISSA_SIZE); + private static final FloatingPointType DOUBLE_PRECISION_FP_TYPE = + new FloatingPointType(DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE); private final int exponentSize; private final int mantissaSize; diff --git a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java index fb6e46f8f9..176dbebd85 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java +++ b/src/org/sosy_lab/java_smt/basicimpl/AbstractEvaluator.java @@ -2,7 +2,7 @@ // an API wrapper for a collection of SMT solvers: // https://github.com/sosy-lab/java-smt // -// SPDX-FileCopyrightText: 2022 Dirk Beyer +// SPDX-FileCopyrightText: 2024 Dirk Beyer // // SPDX-License-Identifier: Apache-2.0 @@ -17,6 +17,8 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; import org.sosy_lab.java_smt.api.Evaluator; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; import org.sosy_lab.java_smt.api.NumeralFormula.RationalFormula; @@ -84,6 +86,12 @@ public final String evaluate(EnumerationFormula f) { return (String) evaluateImpl(creator.extractInfo(f)); } + @Override + public final @Nullable FloatingPointNumber evaluate(FloatingPointFormula f) { + Preconditions.checkState(!isClosed()); + return (FloatingPointNumber) evaluateImpl(creator.extractInfo(f)); + } + @Nullable @Override public final BigInteger evaluate(BitvectorFormula f) { diff --git a/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java b/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java index 64a71f20ae..ee379c61e1 100644 --- a/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java +++ b/src/org/sosy_lab/java_smt/basicimpl/CachingModel.java @@ -16,6 +16,8 @@ import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -85,6 +87,11 @@ public void close() { return delegate.evaluate(formula); } + @Override + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) { + return delegate.evaluate(formula); + } + @Override public String toString() { return delegate.toString(); diff --git a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java index 2d82aea19c..e16ae324e1 100644 --- a/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java +++ b/src/org/sosy_lab/java_smt/delegate/statistics/StatisticsModel.java @@ -17,6 +17,8 @@ import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -81,6 +83,12 @@ class StatisticsModel implements Model { return delegate.evaluate(pF); } + @Override + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) { + stats.modelEvaluations.getAndIncrement(); + return delegate.evaluate(pF); + } + @Override public ImmutableList asList() { stats.modelListings.getAndIncrement(); diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java index 2cd4a4a33a..3ebd078170 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModel.java @@ -17,6 +17,8 @@ import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.Model; import org.sosy_lab.java_smt.api.NumeralFormula.IntegerFormula; @@ -90,6 +92,13 @@ class SynchronizedModel implements Model { } } + @Override + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula pF) { + synchronized (sync) { + return delegate.evaluate(pF); + } + } + @Override public ImmutableList asList() { synchronized (sync) { diff --git a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java index 1c75a4a508..e260776fce 100644 --- a/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java +++ b/src/org/sosy_lab/java_smt/delegate/synchronize/SynchronizedModelWithContext.java @@ -17,6 +17,8 @@ import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; +import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaManager; import org.sosy_lab.java_smt.api.Model; @@ -87,6 +89,11 @@ class SynchronizedModelWithContext implements Model { throw new UnsupportedOperationException(UNSUPPORTED_OPERATION); } + @Override + public @Nullable FloatingPointNumber evaluate(FloatingPointFormula formula) { + throw new UnsupportedOperationException(UNSUPPORTED_OPERATION); + } + @Override public ImmutableList asList() { throw new UnsupportedOperationException(UNSUPPORTED_OPERATION); diff --git a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java index eb30ec43a2..9fe21c61fb 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java @@ -15,14 +15,11 @@ import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; import com.google.common.collect.Iterables; -import com.google.common.primitives.UnsignedInteger; -import com.google.common.primitives.UnsignedLong; +import com.google.common.primitives.Ints; import edu.stanford.CVC4.ArrayType; import edu.stanford.CVC4.BitVectorType; import edu.stanford.CVC4.Expr; import edu.stanford.CVC4.ExprManager; -import edu.stanford.CVC4.FloatingPoint; -import edu.stanford.CVC4.FloatingPointSize; import edu.stanford.CVC4.FunctionType; import edu.stanford.CVC4.Integer; import edu.stanford.CVC4.Kind; @@ -35,12 +32,12 @@ import java.util.HashMap; import java.util.List; import java.util.Map; -import java.util.regex.Matcher; import java.util.regex.Pattern; 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.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -591,7 +588,7 @@ public Object convertValue(Expr expForType, Expr value) { } } else if (valueType.isFloatingPoint()) { - return parseFloatingPoint(value); + return convertFloatingPoint(value); } else if (valueType.isString()) { return value.getConstString().toString(); @@ -602,29 +599,26 @@ public Object convertValue(Expr expForType, Expr value) { } } - private Object parseFloatingPoint(Expr fpExpr) { - Matcher matcher = FLOATING_POINT_PATTERN.matcher(fpExpr.toString()); + private FloatingPointNumber convertFloatingPoint(Expr fpExpr) { + final var matcher = FLOATING_POINT_PATTERN.matcher(fpExpr.toString()); if (!matcher.matches()) { throw new NumberFormatException("Unknown floating-point format: " + fpExpr); } - FloatingPoint fp = fpExpr.getConstFloatingPoint(); - FloatingPointSize fpType = fp.getT(); - long expWidth = fpType.exponentWidth(); - long mantWidth = fpType.significandWidth() - 1; // without sign bit + final var fp = fpExpr.getConstFloatingPoint(); + final var fpType = fp.getT(); + final var expWidth = Ints.checkedCast(fpType.exponentWidth()); + final var mantWidth = Ints.checkedCast(fpType.significandWidth() - 1); // without sign bit - assert matcher.group("sign").length() == 1; - assert matcher.group("exp").length() == expWidth; - assert matcher.group("mant").length() == mantWidth; + final var sign = matcher.group("sign"); + final var exp = matcher.group("exp"); + final var mant = matcher.group("mant"); - String str = matcher.group("sign") + matcher.group("exp") + matcher.group("mant"); - if (expWidth == 11 && mantWidth == 52) { - return Double.longBitsToDouble(UnsignedLong.valueOf(str, 2).longValue()); - } else if (expWidth == 8 && mantWidth == 23) { - return Float.intBitsToFloat(UnsignedInteger.valueOf(str, 2).intValue()); - } + Preconditions.checkArgument(sign.length() == 1 && "01".contains(sign)); + Preconditions.checkArgument(exp.length() == expWidth); + Preconditions.checkArgument(mant.length() == mantWidth); - // TODO to be fully correct, we would need to interpret this string - return fpExpr.toString(); + return FloatingPointNumber.of( + sign.equals("1"), new BigInteger(exp, 2), new BigInteger(mant, 2), expWidth, mantWidth); } } diff --git a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java index 6379eee4e9..dbb95e64ef 100644 --- a/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/cvc5/CVC5FormulaCreator.java @@ -20,6 +20,7 @@ import com.google.common.collect.ImmutableSet; import com.google.common.collect.Iterables; import com.google.common.collect.Table; +import com.google.common.primitives.Ints; import io.github.cvc5.CVC5ApiException; import io.github.cvc5.Datatype; import io.github.cvc5.DatatypeConstructor; @@ -29,9 +30,7 @@ import io.github.cvc5.Solver; import io.github.cvc5.Sort; import io.github.cvc5.Term; -import io.github.cvc5.Triplet; import java.lang.reflect.Array; -import java.math.BigDecimal; import java.math.BigInteger; import java.util.ArrayList; import java.util.HashMap; @@ -44,6 +43,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -801,38 +801,9 @@ public Object convertValue(Term expForType, Term value) { String bitvectorValue = value.getBitVectorValue(); return new BigInteger(bitvectorValue, 2); - } else if (value.isFloatingPointNaN()) { - return Float.NaN; - - } else if (value.isFloatingPointNegInf()) { - return Float.NEGATIVE_INFINITY; - - } else if (value.isFloatingPointPosInf()) { - return Float.POSITIVE_INFINITY; - - } else if (value.isFloatingPointPosZero()) { - return BigDecimal.ZERO; - } else if (value.isFloatingPointValue()) { - // Negative zero falls under this category - // String valueString = - // solver.getValue(solver.mkTerm(Kind.FLOATINGPOINT_TO_REAL, fpTerm)).toString(); - // return new BigDecimal(valueString).stripTrailingZeros(); - final Triplet fpValue = value.getFloatingPointValue(); - final long expWidth = fpValue.first; - final long mantWidth = fpValue.second - 1; // CVC5 also counts the sign-bit in the mantissa - final Term bvValue = fpValue.third; - Preconditions.checkState(bvValue.isBitVectorValue()); - BigInteger bits = new BigInteger(bvValue.getBitVectorValue(), 2); - - if (expWidth == 11 && mantWidth == 52) { // standard IEEE double type with 64 bits - return Double.longBitsToDouble(bits.longValue()); - } else if (expWidth == 8 && mantWidth == 23) { // standard IEEE float type with 32 bits - return Float.intBitsToFloat(bits.intValue()); - } else { - // TODO to be fully correct, we would need to interpret the BV as FP or Rational - return value.toString(); // returns a BV representation of the FP - } + return convertFloatingPoint(value); + } else if (value.isBooleanValue()) { return value.getBooleanValue(); @@ -852,6 +823,16 @@ public Object convertValue(Term expForType, Term value) { } } + private FloatingPointNumber convertFloatingPoint(Term value) throws CVC5ApiException { + final var fpValue = value.getFloatingPointValue(); + final var expWidth = Ints.checkedCast(fpValue.first); + final var mantWidth = Ints.checkedCast(fpValue.second - 1); // without sign bit + final var bvValue = fpValue.third; + Preconditions.checkState(bvValue.isBitVectorValue()); + final var bits = bvValue.getBitVectorValue(); + return FloatingPointNumber.of(bits, expWidth, mantWidth); + } + private Term accessVariablesCache(String name, Sort sort) { Term existingVar = variablesCache.get(name, sort.toString()); if (existingVar == null) { diff --git a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java index b4f51e7bdb..b5938894ab 100644 --- a/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java @@ -108,11 +108,10 @@ import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_term_repr; import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_type_repr; +import com.google.common.base.Preconditions; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableSet; import com.google.common.primitives.Longs; -import com.google.common.primitives.UnsignedInteger; -import com.google.common.primitives.UnsignedLong; import java.math.BigInteger; import java.util.List; import java.util.regex.Matcher; @@ -123,6 +122,7 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -555,25 +555,35 @@ public Object convertValue(Long key, Long term) { } } - private Number parseFloatingPoint(String lTermRepresentation) { + private FloatingPointNumber parseFloatingPoint(String lTermRepresentation) { - // the term is of the format "__" + // the term is of the format "__" Matcher matcher = FLOATING_POINT_PATTERN.matcher(lTermRepresentation); if (!matcher.matches()) { throw new NumberFormatException("Unknown floating-point format: " + lTermRepresentation); } + BigInteger bits = new BigInteger(matcher.group(1)); int expWidth = Integer.parseInt(matcher.group(2)); int mantWidth = Integer.parseInt(matcher.group(3)); - if (expWidth == 11 && mantWidth == 52) { - return Double.longBitsToDouble(UnsignedLong.valueOf(matcher.group(1)).longValue()); - } else if (expWidth == 8 && mantWidth == 23) { - return Float.intBitsToFloat(UnsignedInteger.valueOf(matcher.group(1)).intValue()); - } + boolean sign = bits.testBit(expWidth + mantWidth); + BigInteger exponent = extractBitsFrom(bits, mantWidth, expWidth); + BigInteger mantissa = extractBitsFrom(bits, 0, mantWidth); + + return FloatingPointNumber.of(sign, exponent, mantissa, expWidth, mantWidth); + } - // TODO to be fully correct, we would need to interpret this string - return new BigInteger(matcher.group(1)); + /** + * Returns a range of bits from the bitvector representation of a number. + * + * @param start the index of the lowest significant bit to be extracted. + * @param length how many bits to extract? + */ + private static BigInteger extractBitsFrom(BigInteger number, int start, int length) { + Preconditions.checkArgument(0 <= start && 0 < length); + BigInteger mask = BigInteger.ONE.shiftLeft(length).subtract(BigInteger.ONE); + return number.shiftRight(start).and(mask); } // TODO: change this to the latest version diff --git a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java index 000aa7a35b..59b5105015 100644 --- a/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java +++ b/src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java @@ -10,6 +10,7 @@ import static com.google.common.base.Preconditions.checkArgument; +import com.google.common.base.Preconditions; import com.google.common.collect.HashBasedTable; import com.google.common.collect.ImmutableList; import com.google.common.collect.ImmutableMap; @@ -44,10 +45,12 @@ import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.EnumerationFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.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.RegexFormula; @@ -74,11 +77,6 @@ class Z3FormulaCreator extends FormulaCreator { ImmutableMap.builder() .put(Z3_decl_kind.Z3_OP_TRUE.toInt(), true) .put(Z3_decl_kind.Z3_OP_FALSE.toInt(), false) - .put(Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO.toInt(), +0.0) - .put(Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO.toInt(), -0.0) - .put(Z3_decl_kind.Z3_OP_FPA_PLUS_INF.toInt(), Double.POSITIVE_INFINITY) - .put(Z3_decl_kind.Z3_OP_FPA_MINUS_INF.toInt(), Double.NEGATIVE_INFINITY) - .put(Z3_decl_kind.Z3_OP_FPA_NAN.toInt(), Double.NaN) .put( Z3_decl_kind.Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN.toInt(), FloatingPointRoundingMode.NEAREST_TIES_TO_EVEN) @@ -94,6 +92,14 @@ class Z3FormulaCreator extends FormulaCreator { .put(Z3_decl_kind.Z3_OP_FPA_RM_TOWARD_ZERO.toInt(), FloatingPointRoundingMode.TOWARD_ZERO) .buildOrThrow(); + private static final ImmutableSet Z3_FP_CONSTANTS = + ImmutableSet.of( + Z3_decl_kind.Z3_OP_FPA_PLUS_ZERO.toInt(), + Z3_decl_kind.Z3_OP_FPA_MINUS_ZERO.toInt(), + Z3_decl_kind.Z3_OP_FPA_PLUS_INF.toInt(), + Z3_decl_kind.Z3_OP_FPA_MINUS_INF.toInt(), + Z3_decl_kind.Z3_OP_FPA_NAN.toInt()); + // Set of error messages that might occur if Z3 is interrupted. private static final ImmutableSet Z3_INTERRUPT_ERRORS = ImmutableSet.of( @@ -423,6 +429,9 @@ public R visit(FormulaVisitor visitor, final Formula formula, final Long if (value != null) { return visitor.visitConstant(formula, value); + } else if (Z3_FP_CONSTANTS.contains(declKind)) { + return visitor.visitConstant(formula, convertValue(f)); + // Rounding mode } else if (declKind == Z3_decl_kind.Z3_OP_FPA_NUM.toInt() || Native.getSortKind(environment, Native.getSort(environment, f)) @@ -810,8 +819,7 @@ public Object convertValue(Long value) { } else if (type.isBitvectorType()) { return new BigInteger(Native.getNumeralString(environment, value)); } else if (type.isFloatingPointType()) { - // Converting to Rational first. - return convertValue(Native.simplify(environment, Native.mkFpaToReal(environment, value))); + return convertFloatingPoint((FloatingPointType) type, value); } else if (type.isEnumerationType()) { return Native.astToString(environment, value); } else { @@ -825,6 +833,51 @@ public Object convertValue(Long value) { } } + private FloatingPointNumber convertFloatingPoint(FloatingPointType pType, Long pValue) { + if (Native.fpaIsNumeralInf(environment, pValue)) { + // Floating Point Inf uses: + // - an sign for posiive/negative infinity, + // - "11..11" as exponent, + // - "00..00" as mantissa. + String sign = getSign(pValue) ? "1" : "0"; + return FloatingPointNumber.of( + sign + "1".repeat(pType.getExponentSize()) + "0".repeat(pType.getMantissaSize()), + pType.getExponentSize(), + pType.getMantissaSize()); + } else if (Native.fpaIsNumeralNan(environment, pValue)) { + // TODO We are underspecified here and choose several bits on our own. + // This is not sound, if we combine FP anf BV theory. + // Floating Point NaN uses: + // - an unspecified sign (we choose "0"), + // - "11..11" as exponent, + // - an unspecified mantissa (we choose all "1"). + return FloatingPointNumber.of( + "0" + "1".repeat(pType.getExponentSize()) + "1".repeat(pType.getMantissaSize()), + pType.getExponentSize(), + pType.getMantissaSize()); + } else { + boolean sign = getSign(pValue); + var exponentBv = Native.fpaGetNumeralExponentBv(environment, pValue, true); + var exponent = Native.getNumeralString(environment, exponentBv); + var mantissaBv = Native.fpaGetNumeralSignificandBv(environment, pValue); + var mantissa = Native.getNumeralString(environment, mantissaBv); + return FloatingPointNumber.of( + sign, + new BigInteger(exponent), + new BigInteger(mantissa), + pType.getExponentSize(), + pType.getMantissaSize()); + } + } + + private boolean getSign(Long pValue) { + Native.IntPtr signPtr = new Native.IntPtr(); + Preconditions.checkState( + Native.fpaGetNumeralSign(environment, pValue, signPtr), "Sign is not a Boolean value"); + var sign = signPtr.value != 0; + return sign; + } + @Override public Long declareUFImpl(String pName, Long returnType, List pArgTypes) { long symbol = Native.mkStringSymbol(environment, pName); diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java index 06d4aa0bef..fe94a97062 100644 --- a/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java +++ b/src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java @@ -18,17 +18,16 @@ import com.google.common.collect.ImmutableSet; import com.google.common.collect.Lists; import java.math.BigDecimal; -import java.math.BigInteger; import java.util.List; import java.util.Random; import org.junit.Before; import org.junit.Test; -import org.sosy_lab.common.rationals.ExtendedRational; import org.sosy_lab.common.rationals.Rational; import org.sosy_lab.java_smt.SolverContextFactory.Solvers; import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.FloatingPointRoundingMode; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.FloatingPointType; @@ -815,7 +814,7 @@ private void checkFP(FloatingPointType type, BitvectorFormula bv, FloatingPointF } @Test - public void fpModelValue() throws SolverException, InterruptedException { + public void fpModelContent() throws SolverException, InterruptedException { FloatingPointFormula zeroVar = fpmgr.makeVariable("zero", singlePrecType); BooleanFormula zeroEq = fpmgr.assignment(zeroVar, zero); @@ -825,63 +824,68 @@ public void fpModelValue() throws SolverException, InterruptedException { FloatingPointFormula nanVar = fpmgr.makeVariable("nan", singlePrecType); BooleanFormula nanEq = fpmgr.assignment(nanVar, nan); - FloatingPointFormula posInfVar = fpmgr.makeVariable("posInf", singlePrecType); - BooleanFormula posInfEq = fpmgr.assignment(posInfVar, posInf); - - FloatingPointFormula negInfVar = fpmgr.makeVariable("negInf", singlePrecType); - BooleanFormula negInfEq = fpmgr.assignment(negInfVar, negInf); - try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { prover.push(zeroEq); prover.push(oneEq); prover.push(nanEq); - prover.push(posInfEq); - prover.push(negInfEq); assertThat(prover).isSatisfiable(); try (Model model = prover.getModel()) { - Object zeroValue = model.evaluate(zeroVar); + FloatingPointNumber oneValue = model.evaluate(oneVar); + ValueAssignment oneAssignment = + new ValueAssignment(oneVar, one, oneEq, "one", oneValue, ImmutableList.of()); + + FloatingPointNumber zeroValue = model.evaluate(zeroVar); ValueAssignment zeroAssignment = new ValueAssignment(zeroVar, zero, zeroEq, "zero", zeroValue, ImmutableList.of()); - assertThat(zeroValue) - .isAnyOf(ExtendedRational.ZERO, Rational.ZERO, BigDecimal.ZERO, 0.0, 0.0f); - Object oneValue = model.evaluate(oneVar); - ValueAssignment oneAssignment = - new ValueAssignment(oneVar, one, oneEq, "one", oneValue, ImmutableList.of()); - assertThat(oneValue) - .isAnyOf( - new ExtendedRational(Rational.ONE), - BigInteger.ONE, - Rational.ONE, - BigDecimal.ONE, - 1.0, - 1.0f); - - Object nanValue = model.evaluate(nanVar); + FloatingPointNumber nanValue = model.evaluate(nanVar); ValueAssignment nanAssignment = new ValueAssignment(nanVar, nan, nanEq, "nan", nanValue, ImmutableList.of()); - assertThat(nanValue).isAnyOf(ExtendedRational.NaN, Double.NaN, Float.NaN); - - Object posInfValue = model.evaluate(posInfVar); - ValueAssignment posInfAssignment = - new ValueAssignment( - posInfVar, posInf, posInfEq, "posInf", posInfValue, ImmutableList.of()); - assertThat(posInfValue) - .isAnyOf(ExtendedRational.INFTY, Double.POSITIVE_INFINITY, Float.POSITIVE_INFINITY); - - Object negInfValue = model.evaluate(negInfVar); - ValueAssignment negInfAssignment = - new ValueAssignment( - negInfVar, negInf, negInfEq, "negInf", negInfValue, ImmutableList.of()); - assertThat(negInfValue) - .isAnyOf(ExtendedRational.NEG_INFTY, Double.NEGATIVE_INFINITY, Float.NEGATIVE_INFINITY); - - assertThat(model) - .containsExactly( - zeroAssignment, oneAssignment, nanAssignment, posInfAssignment, negInfAssignment); + + assertThat(model).containsExactly(zeroAssignment, oneAssignment, nanAssignment); + } + } + } + + @Test + public void fpModelValue() throws SolverException, InterruptedException { + try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) { + prover.push(bmgr.makeTrue()); + + assertThat(prover).isSatisfiable(); + + try (Model model = prover.getModel()) { + assertThat(model).isEmpty(); + + for (float f : + new float[] { + 0, + 1, + 2, + 3, + 4, + 256, + 1000, + 1024, + -1, + -2, + -3, + -4, + -1000, + -1024, + Float.NEGATIVE_INFINITY, + Float.POSITIVE_INFINITY, + Float.MAX_VALUE, + Float.MIN_VALUE, + Float.MIN_NORMAL, + }) { + FloatingPointNumber fiveValue = model.evaluate(fpmgr.makeNumber(f, singlePrecType)); + assertThat(fiveValue.floatValue()).isEqualTo(f); + assertThat(fiveValue.doubleValue()).isEqualTo((double) f); + } } } } diff --git a/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java new file mode 100644 index 0000000000..18d73b1b89 --- /dev/null +++ b/src/org/sosy_lab/java_smt/test/FloatingPointNumberTest.java @@ -0,0 +1,97 @@ +// This file is part of JavaSMT, +// an API wrapper for a collection of SMT solvers: +// https://github.com/sosy-lab/java-smt +// +// SPDX-FileCopyrightText: 2024 Dirk Beyer +// +// SPDX-License-Identifier: Apache-2.0 + +package org.sosy_lab.java_smt.test; + +import static com.google.common.truth.Truth.assertThat; +import static org.junit.Assert.assertThrows; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_EXPONENT_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.DOUBLE_PRECISION_MANTISSA_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_EXPONENT_SIZE; +import static org.sosy_lab.java_smt.api.FloatingPointNumber.SINGLE_PRECISION_MANTISSA_SIZE; + +import com.google.common.base.Strings; +import java.math.BigInteger; +import org.junit.Test; +import org.sosy_lab.java_smt.api.FloatingPointNumber; + +public class FloatingPointNumberTest { + + @Test + public void floatingPointNumberWithSinglePrecision() { + for (float f : + new float[] { + 0, + 1, + 2, + 3, + 4, + 256, + 1000, + 1024, + -1, + -2, + -3, + -4, + -1000, + -1024, + Float.NEGATIVE_INFINITY, + Float.POSITIVE_INFINITY, + Float.MAX_VALUE, + Float.MIN_VALUE, + Float.MIN_NORMAL, + }) { + var bits = Strings.padStart(Integer.toBinaryString(Float.floatToRawIntBits(f)), 32, '0'); + var fpNum = + FloatingPointNumber.of( + bits, SINGLE_PRECISION_EXPONENT_SIZE, SINGLE_PRECISION_MANTISSA_SIZE); + assertThat(fpNum.floatValue()).isEqualTo(f); + assertThat(fpNum.doubleValue()).isEqualTo((double) f); // float is a strict subtype of double. + } + } + + @Test + public void floatingPointNumberWithDoublePrecision() { + for (double d : + new double[] { + 0, + 1, + 2, + 3, + 4, + 256, + 1000, + 1024, + -1, + -2, + -3, + -4, + -1000, + -1024, + Double.NEGATIVE_INFINITY, + Double.POSITIVE_INFINITY, + Double.MAX_VALUE, + Double.MIN_VALUE, + Double.MIN_NORMAL, + }) { + var bits = Strings.padStart(Long.toBinaryString(Double.doubleToRawLongBits(d)), 64, '0'); + var fpNum = + FloatingPointNumber.of( + bits, DOUBLE_PRECISION_EXPONENT_SIZE, DOUBLE_PRECISION_MANTISSA_SIZE); + assertThat(fpNum.doubleValue()).isEqualTo(d); + } + } + + @Test + public void floatingPointNumberWithArbitraryPrecision() { + var fpNum = FloatingPointNumber.of(false, BigInteger.valueOf(10), BigInteger.ONE, 5, 7); + assertThat(fpNum.toString()).isEqualTo("0" + "01010" + "0000001"); + assertThrows(IllegalArgumentException.class, () -> fpNum.floatValue()); + assertThrows(IllegalArgumentException.class, () -> fpNum.doubleValue()); + } +} diff --git a/src/org/sosy_lab/java_smt/test/ModelTest.java b/src/org/sosy_lab/java_smt/test/ModelTest.java index b89f14a658..f1622b109b 100644 --- a/src/org/sosy_lab/java_smt/test/ModelTest.java +++ b/src/org/sosy_lab/java_smt/test/ModelTest.java @@ -35,6 +35,7 @@ import org.sosy_lab.java_smt.api.BitvectorFormula; import org.sosy_lab.java_smt.api.BooleanFormula; import org.sosy_lab.java_smt.api.FloatingPointFormula; +import org.sosy_lab.java_smt.api.FloatingPointNumber; import org.sosy_lab.java_smt.api.Formula; import org.sosy_lab.java_smt.api.FormulaType; import org.sosy_lab.java_smt.api.FormulaType.ArrayFormulaType; @@ -1788,8 +1789,16 @@ private void checkModelIteration(BooleanFormula f, boolean useOptProver) assignmentFormulas.add(va.getAssignmentAsFormula()); assertThatFormula(va.getAssignmentAsFormula()) .isEqualTo(makeAssignment(va.getKey(), va.getValueAsFormula())); - assertThat(va.getValue().getClass()) - .isIn(ImmutableList.of(Boolean.class, BigInteger.class, Rational.class, Double.class)); + assertThat( + ImmutableList.of( + Boolean.class, + BigInteger.class, + Rational.class, + Double.class, + FloatingPointNumber.class) + .stream() + .anyMatch(cls -> cls.isInstance(va.getValue()))) + .isTrue(); } // Check that model is not contradicting