summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Source/Core/AbsyExpr.cs104
-rw-r--r--Source/Provers/SMTLib/SMTLibProcess.cs5
-rw-r--r--Source/Provers/SMTLib/TypeDeclCollector.cs4
-rw-r--r--Test/floats/float3.bpl.expect4
-rw-r--r--Test/floats/float4.bpl.expect4
5 files changed, 13 insertions, 108 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index b980a22b..7ffd5f7f 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -313,13 +313,6 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<NAryExpr>() != null);
return Binary(BinaryOperator.Opcode.RealDiv, e1, e2);
}
- public static NAryExpr FloatDiv(Expr e1, Expr e2)
- {
- Contract.Requires(e2 != null);
- Contract.Requires(e1 != null);
- Contract.Ensures(Contract.Result<NAryExpr>() != null);
- return Binary(BinaryOperator.Opcode.FloatDiv, e1, e2);
- }
public static NAryExpr Pow(Expr e1, Expr e2) {
Contract.Requires(e2 != null);
Contract.Requires(e1 != null);
@@ -363,11 +356,6 @@ namespace Microsoft.Boogie {
Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
}
- public static LiteralExpr Literal(BigFloat value)
- {
- Contract.Ensures(Contract.Result<LiteralExpr>() != null);
- return new LiteralExpr(Token.NoToken, value);
- }
private static LiteralExpr/*!*/ true_ = Literal(true);
public static LiteralExpr/*!*/ True {
@@ -526,7 +514,7 @@ namespace Microsoft.Boogie {
}
public class LiteralExpr : Expr {
- public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, a BigFloat, or a BvConst
+ public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, or a BvConst
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Val != null);
@@ -575,21 +563,6 @@ namespace Microsoft.Boogie {
}
/// <summary>
- /// Creates a literal expression for the floating point value "v".
- /// </summary>
- /// <param name="tok"></param>
- /// <param name="v"></param>
- public LiteralExpr(IToken/*!*/ tok, BigFloat v, bool immutable = false)
- : base(tok, immutable)
- {
- Contract.Requires(tok != null);
- Val = v;
- Type = Type.GetFloatType(v.ExponentSize, v.SignificandSize);
- if (immutable)
- CachedHashCode = ComputeHashCode();
- }
-
- /// <summary>
/// Creates a literal expression for the bitvector value "v".
/// </summary>
public LiteralExpr(IToken/*!*/ tok, BigNum v, int b, bool immutable=false)
@@ -660,9 +633,6 @@ namespace Microsoft.Boogie {
return Type.Int;
} else if (Val is BigDec) {
return Type.Real;
- } else if (Val is BigFloat) {
- BigFloat temp = (BigFloat)Val;
- return Type.GetFloatType(temp.ExponentSize, temp.SignificandSize);
} else if (Val is BvConst) {
return Type.GetBvType(((BvConst)Val).Bits);
} else {
@@ -711,14 +681,6 @@ namespace Microsoft.Boogie {
}
}
- public bool isBigFloat
- {
- get
- {
- return Val is BigFloat;
- }
- }
-
public BigDec asBigDec {
get {
Contract.Assert(isBigDec);
@@ -726,13 +688,6 @@ namespace Microsoft.Boogie {
}
}
- public BigFloat asBigFloat {
- get {
- Contract.Assert(isBigFloat);
- return (BigFloat)cce.NonNull(Val);
- }
- }
-
public bool isBool {
get {
return Val is bool;
@@ -1400,9 +1355,6 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real)) {
return Type.Real;
}
- //if (arg0type.Unify(Type.Float)) {
- //return Type.Float;
- //}
goto BAD_TYPE;
case Opcode.Not:
if (arg0type.Unify(Type.Bool)) {
@@ -1447,9 +1399,6 @@ namespace Microsoft.Boogie {
if (argument is BigDec) {
return -((BigDec)argument);
}
- if (argument is BigFloat) {
- return -((BigFloat)argument);
- }
break;
case Opcode.Not:
if (argument is bool) {
@@ -1482,7 +1431,6 @@ namespace Microsoft.Boogie {
Div,
Mod,
RealDiv,
- FloatDiv,
Pow,
Eq,
Neq,
@@ -1723,12 +1671,6 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real) && 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.Div:
case Opcode.Mod:
@@ -1741,12 +1683,6 @@ 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)) {
@@ -1779,9 +1715,6 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
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:
@@ -1892,9 +1825,6 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) + ((BigDec)e2);
}
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) + ((BigFloat)e2);
- }
break;
case Opcode.Sub:
if (e1 is BigNum && e2 is BigNum) {
@@ -1903,9 +1833,6 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) - ((BigDec)e2);
}
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) - ((BigFloat)e2);
- }
break;
case Opcode.Mul:
if (e1 is BigNum && e2 is BigNum) {
@@ -1914,9 +1841,6 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) * ((BigDec)e2);
}
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) * ((BigFloat)e2);
- }
break;
case Opcode.Div:
if (e1 is BigNum && e2 is BigNum) {
@@ -1931,9 +1855,6 @@ namespace Microsoft.Boogie {
case Opcode.RealDiv:
// TODO: add partial evaluation fro real division
break;
- case Opcode.FloatDiv:
- //TODO: add float division
- break;
case Opcode.Pow:
// TODO: add partial evaluation fro real exponentiation
break;
@@ -1944,9 +1865,6 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) < ((BigDec)e2);
}
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) < ((BigFloat)e2);
- }
break;
case Opcode.Le:
if (e1 is BigNum && e2 is BigNum) {
@@ -1955,9 +1873,6 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) <= ((BigDec)e2);
}
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) <= ((BigFloat)e2);
- }
break;
case Opcode.Gt:
if (e1 is BigNum && e2 is BigNum) {
@@ -1966,9 +1881,6 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) > ((BigDec)e2);
}
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) > ((BigFloat)e2);
- }
break;
case Opcode.Ge:
if (e1 is BigNum && e2 is BigNum) {
@@ -1977,9 +1889,6 @@ namespace Microsoft.Boogie {
if (e1 is BigDec && e2 is BigDec) {
return ((BigDec)e1) >= ((BigDec)e2);
}
- if (e1 is BigFloat && e2 is BigFloat) {
- return ((BigFloat)e1) >= ((BigFloat)e2);
- }
break;
case Opcode.And:
@@ -2081,7 +1990,7 @@ namespace Microsoft.Boogie {
}
else
{
- this.name.Emit(stream, 0xF0, false);
+ this.name.Emit(stream, 0xF0, false);
}
if (stream.UseForComputingChecksums)
{
@@ -2268,8 +2177,7 @@ namespace Microsoft.Boogie {
public class ArithmeticCoercion : IAppliable {
public enum CoercionType {
ToInt,
- ToReal,
- ToFloat
+ ToReal
}
private IToken/*!*/ tok;
@@ -2277,7 +2185,6 @@ namespace Microsoft.Boogie {
private readonly string name;
private readonly Type type;
private readonly Type argType;
- private readonly Type argType2;
private readonly int hashCode;
public ArithmeticCoercion(IToken tok, CoercionType coercion) {
@@ -2357,9 +2264,8 @@ namespace Microsoft.Boogie {
tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
- if (!(cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType) || cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType2)))
- {
- tc.Error(this.tok, "argument type {0} does not match expected type {1} or type {2}", cce.NonNull(args[0]).Type, this.argType, this.argType2);
+ if (!cce.NonNull(cce.NonNull(args[0]).Type).Unify(argType)) {
+ tc.Error(this.tok, "argument type {0} does not match expected type {1}", cce.NonNull(args[0]).Type, this.argType);
}
return this.type;
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs
index a2fe4d4e..9fda36e7 100644
--- a/Source/Provers/SMTLib/SMTLibProcess.cs
+++ b/Source/Provers/SMTLib/SMTLibProcess.cs
@@ -91,8 +91,8 @@ namespace Microsoft.Boogie.SMTLib
// Give it a chance to exit cleanly (e.g. to flush buffers)
if (!prover.WaitForExit(timeout)) {
- prover.Kill();
- }
+ prover.Kill();
+ }
} catch { /* Swallow errors */ }
}
@@ -105,7 +105,6 @@ namespace Microsoft.Boogie.SMTLib
log = log.Replace("\r", "").Replace("\n", " ");
Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
}
- //Console.WriteLine(cmd);
toProver.WriteLine(cmd);
}
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index d7c56d90..eaed83e9 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -268,7 +268,7 @@ void ObjectInvariant()
"(declare-fun " + printedName + " () " + TypeToString(node.Type) + ")";
if (!(printedName.StartsWith("assume$$") || printedName.StartsWith("soft$$") || printedName.StartsWith("try$$")))
{
- AddDeclaration(decl);
+ AddDeclaration(decl);
}
KnownVariables.Add(node);
if(declHandler != null)
@@ -311,7 +311,7 @@ void ObjectInvariant()
return;
}
- if (type.IsBool || type.IsInt || type.IsReal || type.IsFloat || type.IsBv)
+ if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)
return;
CtorType ctorType = type as CtorType;
diff --git a/Test/floats/float3.bpl.expect b/Test/floats/float3.bpl.expect
index 6abb715b..37fad75c 100644
--- a/Test/floats/float3.bpl.expect
+++ b/Test/floats/float3.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/floats/float4.bpl.expect b/Test/floats/float4.bpl.expect
index 6abb715b..37fad75c 100644
--- a/Test/floats/float4.bpl.expect
+++ b/Test/floats/float4.bpl.expect
@@ -1,2 +1,2 @@
-
-Boogie program verifier finished with 1 verified, 0 errors
+
+Boogie program verifier finished with 1 verified, 0 errors
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-21 13:40:40 +0000