diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2015-09-23 04:08:00 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2015-09-23 04:08:00 -0600 |
| commit | 80f3d4ed1bb221adbd3c7162acea10920b9fab73 (patch) | |
| tree | 218275e91b58fdb3cbce0376a4b423fa34e4e763 /Source/Core | |
| parent | 28a20e6eba2919e008f70874b4c12a3ce7ad049c (diff) | |
Modified BigFloat to avoid evaluating the floating point value before sending it to z3
Diffstat (limited to 'Source/Core')
| -rw-r--r-- | Source/Core/AbsyExpr.cs | 20 |
1 files changed, 11 insertions, 9 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index 181076a7..cf6fb922 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -1702,10 +1702,10 @@ namespace Microsoft.Boogie { return Type.Real;
}
if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
- return new FloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
+ return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
}
if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
- return new FloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
+ return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
}
goto BAD_TYPE;
case Opcode.Div:
@@ -1719,6 +1719,12 @@ namespace Microsoft.Boogie { (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) {
return Type.Real;
}
+ if (arg0type.IsFloat && arg0type.Unify(arg1type)) {
+ return Type.GetFloatType(arg0.Type.FloatExponent, arg0.Type.FloatMantissa);
+ }
+ if (arg1type.IsFloat && arg1type.Unify(arg0type)) {
+ return Type.GetFloatType(arg1.Type.FloatExponent, arg1.Type.FloatMantissa);
+ }
goto BAD_TYPE;
case Opcode.Pow:
if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
@@ -1751,10 +1757,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Bool;
}
- //if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))
- //{
- //return Type.Bool;
- //}
+ if ((arg0type.IsFloat && arg0type.Unify(arg1type)) || (arg1type.IsFloat && arg1type.Unify(arg0type))) {
+ return Type.Bool;
+ }
goto BAD_TYPE;
case Opcode.And:
case Opcode.Or:
@@ -1799,9 +1804,6 @@ namespace Microsoft.Boogie { case Opcode.Pow:
return Type.Real;
- //case Opcode.FloatDiv:
- //return Type.Float;
-
case Opcode.Eq:
case Opcode.Neq:
case Opcode.Gt:
|