Fixed errors

ftsrg · Mar 19, 2024 · 82626c8 · 82626c8
1 parent f96e095
commit 82626c8
Show file tree

Hide file tree

Showing 5 changed files with 10 additions and 5 deletions.
diff --git a/...rojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvSignChangeExpr.java b/...rojects/common/core/src/main/java/hu/bme/mit/theta/core/type/bvtype/BvSignChangeExpr.java
@@ -25,7 +25,7 @@
 public final class BvSignChangeExpr extends PosExpr<BvType> {
 
     private static final int HASH_SEED = 8963;
-    private static final String OPERATOR_LABEL = "bvsign";
+    private static final String OPERATOR_LABEL = "bvpos";
 
     private final BvType newType;
 

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpAssignExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpAssignExpr.java
@@ -56,7 +56,7 @@ public BoolLitExpr eval(final Valuation val) {
         final FpLitExpr leftOpVal = (FpLitExpr) getLeftOp().eval(val);
         final FpLitExpr rightOpVal = (FpLitExpr) getRightOp().eval(val);
 
-        return leftOpVal.eq(rightOpVal);
+        return leftOpVal.assign(rightOpVal);
     }
 
     @Override

diff --git a/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java b/subprojects/common/core/src/main/java/hu/bme/mit/theta/core/type/fptype/FpLitExpr.java
@@ -171,6 +171,13 @@ public BoolLitExpr eq(final FpLitExpr that) {
         return BoolExprs.Bool(this.hidden == that.hidden && this.exponent.equals(that.exponent) && this.significand.equals(that.significand));
     }
 
+    public BoolLitExpr assign(final FpLitExpr that) {
+        checkArgument(this.getType().equals(that.getType()));
+        var left = fpLitExprToBigFloat(FpRoundingMode.getDefaultRoundingMode(), this);
+        var right = fpLitExprToBigFloat(FpRoundingMode.getDefaultRoundingMode(), that);
+        return BoolExprs.Bool(this.hidden == that.hidden && this.exponent.equals(that.exponent) && this.significand.equals(that.significand));
+    }
+
     public BoolLitExpr gt(final FpLitExpr that) {
         checkArgument(this.getType().equals(that.getType()));
         var left = fpLitExprToBigFloat(FpRoundingMode.getDefaultRoundingMode(), this);

diff --git a/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BvTestUtils.java b/subprojects/common/core/src/testFixtures/java/hu/bme/mit/theta/core/utils/BvTestUtils.java
@@ -40,7 +40,6 @@
 import hu.bme.mit.theta.core.type.bvtype.BvSModExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvSRemExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvShiftLeftExpr;
-import hu.bme.mit.theta.core.type.bvtype.BvSignChangeExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvSubExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvUDivExpr;
 import hu.bme.mit.theta.core.type.bvtype.BvUGeqExpr;
@@ -138,7 +137,6 @@ public static Collection<?> BasicOperations() {
 
                 {BvPosExpr.class, SBv16(-5), Pos(SBv16(-5))},
                 {BvNegExpr.class, SBv16(5), Neg(SBv16(-5))},
-                {BvSignChangeExpr.class, SBv16(5), BvSignChangeExpr.of(SBv16(-5), SBv16(5).getType())},
         });
     }
 

diff --git a/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java b/.../solver-javasmt/src/main/java/hu/bme/mit/theta/solver/javasmt/JavaSMTExprTransformer.java
@@ -843,7 +843,7 @@ private Formula transformBvPos(final BvPosExpr expr) {
     }
 
     private Formula transformBvSignChange(final BvSignChangeExpr expr) {
-        return bitvectorFormulaManager.negate((BitvectorFormula) toTerm(expr.getOp()));
+        return (BitvectorFormula) toTerm(expr.getOp());
     }
 
     private Formula transformBvNeg(final BvNegExpr expr) {