Package de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint

Class FloatValue

java.lang.Object
de.uzl.its.swat.symbolic.value.Value<T,K>
de.uzl.its.swat.symbolic.value.primitive.numeric.NumericalValue<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>
de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.FloatValue
public class FloatValue extends NumericalValue<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>

  • Field Details

    • precision

      public static final org.sosy_lab.java_smt.api.FormulaType.FloatingPointType precision

  • Constructor Details

    • FloatValue

      public FloatValue(org.sosy_lab.java_smt.api.SolverContext context, float concrete)

    • FloatValue

      public FloatValue(org.sosy_lab.java_smt.api.SolverContext context, float concrete, org.sosy_lab.java_smt.api.FloatingPointFormula formula)

  • Method Details

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC(String namePrefix)
      Turns this DoubleValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>
      Parameters:
      namePrefix -
      Returns:
      The numerical identifier of this symbolic variable

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC(long idx)
      Turns this IntValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>
      Parameters:
      idx -
      Returns:
      The numerical identifier of this symbolic variable

    • MAKE_SYMBOLIC

      public String MAKE_SYMBOLIC()
      Turns this DoubleValue into a symbolic variable
      Overrides:
      MAKE_SYMBOLIC in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>
      Returns:
      The numerical identifier of this symbolic variable

    • getBounds

      public org.sosy_lab.java_smt.api.BooleanFormula getBounds(boolean upper)
      Creates a formula that asserts that this symbolic value is withing the bounds of this type
      Overrides:
      getBounds in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>
      Parameters:
      upper - If the upper or lower bound should be created
      Returns:
      The BooleanFormula that represents the bounds check

    • FADD

      public FloatValue FADD(FloatValue f)
      Adds two floats
      Parameters:
      f - The other float
      Returns:
      The resulting FloatValue

    • FDIV

      public FloatValue FDIV(FloatValue f)
      Divides two floats
      Parameters:
      f - The other float
      Returns:
      The resulting FloatValue

    • FMUL

      public FloatValue FMUL(FloatValue f)
      Multiplies two floats
      Parameters:
      f - The other float
      Returns:
      The resulting FloatValue

    • FNEG

      public FloatValue FNEG()
      Negates a float
      Returns:
      The resulting FloatValue

    • FREM

      public FloatValue FREM(FloatValue f)
      Gets the remainder from the division of two floats WARNING: This is not symbolically tracked!
      Parameters:
      f - The other flaot
      Returns:
      The resulting FloatValue

    • FSUB

      public FloatValue FSUB(FloatValue f)
      Subtracts two floats
      Parameters:
      f - The other float
      Returns:
      The resulting FloatValue

    • F2I

      public IntValue F2I()
      Casts a float to an integer
      Returns:
      The resulting IntValue

    • F2D

      public DoubleValue F2D()
      Casts a float to a double
      Returns:
      The resulting IntValue

    • F2L

      public LongValue F2L()
      Casts a float to a long
      Returns:
      The resulting IntValue

    • FCMPG

      public IntValue FCMPG(FloatValue f)
      Compares two floats and returns: 0 if both values are equal; 1 if this float is greater or either float is NaN; -1 if the parameter is greater ToDo (Nils): This method is not validated
      Parameters:
      f - The other FloatValue
      Returns:
      The resulting IntValue with the boolean conditions

    • FCMPL

      public IntValue FCMPL(FloatValue f)
      Compares two floats and returns: 0 if both values are equal 1 if this float is greater -1 if the parameter is greater or either float is NaN ToDo (Nils): This method is not validated
      Parameters:
      f - The other FloatValue
      Returns:
      The resulting IntValue with the boolean conditions

    • asFloatValue

      public FloatValue asFloatValue()
      Overrides:
      asFloatValue in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>

    • asStringValue

      public StringValue asStringValue()
      Overrides:
      asStringValue in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>

    • getConcreteEncoded

      public String getConcreteEncoded()
      Overrides:
      getConcreteEncoded in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>

    • toString

      public String toString()
      Returns the string representation of the value used to visualize the stack. The representation is not complete.
      Overrides:
      toString in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Float>
      Returns:
      the string representation of the value.