add new API method for FP_ABS returning the absolute of a FP value.

This is related to #173.

Author: kfriedberger

src/org/sosy_lab/java_smt/api/FloatingPointFormulaManager.java

@@ -140,6 +140,8 @@ FloatingPointFormula castFrom(
 
   FloatingPointFormula negate(FloatingPointFormula number);
 
+  FloatingPointFormula abs(FloatingPointFormula number);
+
   FloatingPointFormula add(FloatingPointFormula number1, FloatingPointFormula number2);
 
   FloatingPointFormula add(

src/org/sosy_lab/java_smt/api/FunctionDeclarationKind.java

@@ -197,6 +197,9 @@ public enum FunctionDeclarationKind {
   /** Negation of a floating point. */
   FP_NEG,
 
+  /** Absolute value of a floating point. */
+  FP_ABS,
+
   /** Subtraction over floating points. */
   FP_SUB,
 

src/org/sosy_lab/java_smt/basicimpl/AbstractFloatingPointFormulaManager.java

@@ -250,6 +250,14 @@ public FloatingPointFormula negate(FloatingPointFormula pNumber) {
 
   protected abstract TFormulaInfo negate(TFormulaInfo pParam1);
 
+  @Override
+  public FloatingPointFormula abs(FloatingPointFormula pNumber) {
+    TFormulaInfo param1 = extractInfo(pNumber);
+    return wrap(abs(param1));
+  }
+
+  protected abstract TFormulaInfo abs(TFormulaInfo pParam1);
+
   @Override
   public FloatingPointFormula add(FloatingPointFormula pNumber1, FloatingPointFormula pNumber2) {
     TFormulaInfo param1 = extractInfo(pNumber1);

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FloatingPointFormulaManager.java

@@ -246,6 +246,11 @@ protected Expr negate(Expr pParam1) {
     return exprManager.mkExpr(Kind.FLOATINGPOINT_NEG, pParam1);
   }
 
+  @Override
+  protected Expr abs(Expr pParam1) {
+    return exprManager.mkExpr(Kind.FLOATINGPOINT_ABS, pParam1);
+  }
+
   @Override
   protected Expr add(Expr pParam1, Expr pParam2, Expr pRoundingMode) {
     return exprManager.mkExpr(Kind.FLOATINGPOINT_PLUS, pRoundingMode, pParam1, pParam2);

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4FormulaCreator.java

@@ -370,6 +370,7 @@ public <R> R visit(FormulaVisitor<R> visitor, Formula formula, final Expr f) {
           .put(Kind.FLOATINGPOINT_ISSN, FunctionDeclarationKind.FP_IS_SUBNORMAL)
           .put(Kind.FLOATINGPOINT_ISZ, FunctionDeclarationKind.FP_IS_ZERO)
           .put(Kind.FLOATINGPOINT_EQ, FunctionDeclarationKind.FP_EQ)
+          .put(Kind.FLOATINGPOINT_ABS, FunctionDeclarationKind.FP_ABS)
           .put(Kind.FLOATINGPOINT_PLUS, FunctionDeclarationKind.FP_ADD)
           .put(Kind.FLOATINGPOINT_SUB, FunctionDeclarationKind.FP_SUB)
           .put(Kind.FLOATINGPOINT_MULT, FunctionDeclarationKind.FP_MUL)

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FloatingPointFormulaManager.java

@@ -20,6 +20,7 @@
 package org.sosy_lab.java_smt.solvers.mathsat5;
 
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_equal;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_abs;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_cast;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_div;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.msat_make_fp_equal;
@@ -214,6 +215,11 @@ protected Long negate(Long pNumber) {
     return msat_make_fp_neg(mathsatEnv, pNumber);
   }
 
+  @Override
+  protected Long abs(Long pNumber) {
+    return msat_make_fp_abs(mathsatEnv, pNumber);
+  }
+
   @Override
   protected Long add(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return msat_make_fp_plus(mathsatEnv, pRoundingMode, pNumber1, pNumber2);

src/org/sosy_lab/java_smt/solvers/mathsat5/Mathsat5FormulaCreator.java

@@ -48,6 +48,7 @@
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_BV_ZEXT;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_EQ;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FLOOR;
+import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_ABS;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_ADD;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_AS_IEEEBV;
 import static org.sosy_lab.java_smt.solvers.mathsat5.Mathsat5NativeApi.MSAT_TAG_FP_CAST;
@@ -432,6 +433,8 @@ private FunctionDeclarationKind getDeclarationKind(long pF) {
 
       case MSAT_TAG_FP_NEG:
         return FunctionDeclarationKind.FP_NEG;
+      case MSAT_TAG_FP_ABS:
+        return FunctionDeclarationKind.FP_ABS;
       case MSAT_TAG_FP_ADD:
         return FunctionDeclarationKind.FP_ADD;
       case MSAT_TAG_FP_SUB:

src/org/sosy_lab/java_smt/solvers/z3/Z3FloatingPointFormulaManager.java

@@ -186,6 +186,11 @@ protected Long negate(Long pNumber) {
     return Native.mkFpaNeg(z3context, pNumber);
   }
 
+  @Override
+  protected Long abs(Long pNumber) {
+    return Native.mkFpaAbs(z3context, pNumber);
+  }
+
   @Override
   protected Long add(Long pNumber1, Long pNumber2, Long pRoundingMode) {
     return Native.mkFpaAdd(z3context, pRoundingMode, pNumber1, pNumber2);

src/org/sosy_lab/java_smt/solvers/z3/Z3FormulaCreator.java

@@ -563,6 +563,8 @@ private FunctionDeclarationKind getDeclarationKind(long f) {
 
       case Z3_OP_FPA_NEG:
         return FunctionDeclarationKind.FP_NEG;
+      case Z3_OP_FPA_ABS:
+        return FunctionDeclarationKind.FP_ABS;
       case Z3_OP_FPA_SUB:
         return FunctionDeclarationKind.FP_SUB;
       case Z3_OP_FPA_ADD:

src/org/sosy_lab/java_smt/test/FloatingPointFormulaManagerTest.java

@@ -117,11 +117,14 @@ public void negative() throws SolverException, InterruptedException {
       FloatingPointFormula formula = fpmgr.makeNumber(d, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isTautological();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isUnsatisfiable();
+      assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.negate(formula), fpmgr.abs(formula)))
+          .isTautological();
     }
     for (double d : new double[] {1, 2, 0.0, Double.POSITIVE_INFINITY}) {
       FloatingPointFormula formula = fpmgr.makeNumber(d, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isUnsatisfiable();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isTautological();
+      assertThatFormula(fpmgr.equalWithFPSemantics(formula, fpmgr.abs(formula))).isTautological();
     }
   }
 
@@ -131,16 +134,20 @@ public void parser() throws SolverException, InterruptedException {
       FloatingPointFormula formula = fpmgr.makeNumber(s, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isTautological();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isUnsatisfiable();
+      assertThatFormula(fpmgr.equalWithFPSemantics(fpmgr.negate(formula), fpmgr.abs(formula)))
+          .isTautological();
     }
     for (String s : new String[] {"1", "Infinity", "0", "0.0", "0.000"}) {
       FloatingPointFormula formula = fpmgr.makeNumber(s, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isUnsatisfiable();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isTautological();
+      assertThatFormula(fpmgr.equalWithFPSemantics(formula, fpmgr.abs(formula))).isTautological();
     }
     for (String s : new String[] {"+1", "+Infinity", "+0", "+0.0", "+0.000"}) {
       FloatingPointFormula formula = fpmgr.makeNumber(s, singlePrecType);
       assertThatFormula(fpmgr.isNegative(formula)).isUnsatisfiable();
       assertThatFormula(fpmgr.isNegative(fpmgr.negate(formula))).isTautological();
+      assertThatFormula(fpmgr.equalWithFPSemantics(formula, fpmgr.abs(formula))).isTautological();
     }
     // NaN is not positive and not negative.
     for (String s : new String[] {"NaN", "-NaN", "+NaN"}) {

src/org/sosy_lab/java_smt/test/SolverVisitorTest.java

@@ -205,6 +205,7 @@ public void floatMoreVisit() {
     checkKind(fpmgr.isNormal(x), FunctionDeclarationKind.FP_IS_NORMAL);
     checkKind(fpmgr.isSubnormal(x), FunctionDeclarationKind.FP_IS_SUBNORMAL);
     checkKind(fpmgr.isZero(x), FunctionDeclarationKind.FP_IS_ZERO);
+    checkKind(fpmgr.abs(x), FunctionDeclarationKind.FP_ABS);
     if (Solvers.CVC4 != solverToUse()) { // CVC4 does not support this operation
       checkKind(fpmgr.toIeeeBitvector(x), FunctionDeclarationKind.FP_AS_IEEEBV);
     }