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

Class DoubleValue

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,Double>
de.uzl.its.swat.symbolic.value.primitive.numeric.floatingpoint.DoubleValue
public class DoubleValue extends NumericalValue<org.sosy_lab.java_smt.api.FloatingPointFormula,Double>
Wrapper for doubles to represent symbolic and concrete information on the symbolic stack

  • Field Details

    • precision

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

  • Constructor Details

    • DoubleValue

      public DoubleValue(org.sosy_lab.java_smt.api.SolverContext context, double concrete)
      Constructor that creates a new DoubleValue without prior symbolic information and only a concrete value
      Parameters:
      context - The Java-smt solver context
      concrete - The concrete double value

    • DoubleValue

      public DoubleValue(org.sosy_lab.java_smt.api.SolverContext context, double concrete, org.sosy_lab.java_smt.api.FloatingPointFormula formula)
      Constructor that creates a new DoubleValue with prior symbolic information and a concrete value
      Parameters:
      context - The Java-smt solver context
      concrete - The concrete double value
      formula - Prior symbolic information

  • 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,Double>
      Parameters:
      namePrefix -
      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,Double>
      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,Double>
      Parameters:
      idx -
      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,Double>
      Parameters:
      upper - If the upper or lower bound should be created
      Returns:
      The BooleanFormula that represents the bounds check

    • DADD

      public DoubleValue DADD(DoubleValue d)
      Adds two doubles
      Parameters:
      d - The other double
      Returns:
      The resulting DoubleValue

    • DSUB

      public DoubleValue DSUB(DoubleValue d)
      Subtracts two doubles
      Parameters:
      d - The other double
      Returns:
      The resulting DoubleValue

    • DMUL

      public DoubleValue DMUL(DoubleValue d)
      Multiplies two doubles
      Parameters:
      d - The other double
      Returns:
      The resulting DoubleValue

    • DDIV

      public DoubleValue DDIV(DoubleValue d)
      Divides two doubles
      Parameters:
      d - The other double
      Returns:
      The resulting DoubleValue

    • DREM

      public DoubleValue DREM(DoubleValue d)
      Gets the remainder from the division of two doubles WARNING: This is not symbolically tracked!
      Parameters:
      d - The other double
      Returns:
      The resulting DoubleValue

    • DNEG

      public DoubleValue DNEG()
      Negates a double
      Returns:
      The resulting DoubleValue

    • DCMPG

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

    • DCMPL

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

    • D2I

      public IntValue D2I()
      Casts a double to an integer
      Returns:
      The resulting IntValue

    • D2F

      public FloatValue D2F()
      Casts a double to a float
      Returns:
      The resulting FloatValue

    • D2L

      public LongValue D2L()
      Casts a double to a long
      Returns:
      The resulting LongValue

    • getConcreteEncoded

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

    • asDoubleValue

      public DoubleValue asDoubleValue()
      Overrides:
      asDoubleValue in class Value<org.sosy_lab.java_smt.api.FloatingPointFormula,Double>

    • asStringValue

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

    • 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,Double>
      Returns:
      the string representation of the value.