summaryrefslogtreecommitdiff
path: root/Source
diff options
context:
space:
mode:
Diffstat (limited to 'Source')
-rw-r--r--Source/Core/AbsyExpr.cs8
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs12
-rw-r--r--Source/VCExpr/Boogie2VCExpr.cs10
-rw-r--r--Source/VCExpr/SimplifyLikeLineariser.cs36
-rw-r--r--Source/VCExpr/VCExprAST.cs45
-rw-r--r--Source/VCExpr/VCExprASTPrinter.cs12
-rw-r--r--Source/VCExpr/VCExprASTVisitors.cs23
7 files changed, 140 insertions, 6 deletions
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs
index a8c82f08..9297bcbc 100644
--- a/Source/Core/AbsyExpr.cs
+++ b/Source/Core/AbsyExpr.cs
@@ -1706,6 +1706,10 @@ namespace Microsoft.Boogie {
if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
return Type.Real;
}
+ if (arg0type.Unify(Type.Float) && arg1type.Unify(Type.Float))
+ {
+ return Type.Float;
+ }
goto BAD_TYPE;
case Opcode.Div:
case Opcode.Mod:
@@ -1757,6 +1761,10 @@ 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;
+ }
goto BAD_TYPE;
case Opcode.And:
case Opcode.Or:
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f431c3d5..6accf79f 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -678,6 +678,12 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
+ public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("/f", node, options);
+ return true;
+ }
+
public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
WriteApplication("real_pow", node, options);
return true;
@@ -729,6 +735,12 @@ namespace Microsoft.Boogie.SMTLib
return true;
}
+ public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("to_float", node, options);
+ return true;
+ }
+
private string ExtractDatatype(Function func) {
if (func is DatatypeSelector) {
DatatypeSelector selector = (DatatypeSelector) func;
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs
index 8674f8c0..aa246c37 100644
--- a/Source/VCExpr/Boogie2VCExpr.cs
+++ b/Source/VCExpr/Boogie2VCExpr.cs
@@ -334,7 +334,10 @@ namespace Microsoft.Boogie.VCExprAST {
return Gen.Integer(node.asBigNum);
} else if (node.Val is BigDec) {
return Gen.Real(node.asBigDec);
- } else if (node.Val is BvConst) {
+ } else if (node.Val is BigFloat) {
+ return Gen.Float(node.asBigFloat);
+ }
+ else if (node.Val is BvConst) {
return Gen.Bitvector((BvConst)node.Val);
} else {
System.Diagnostics.Debug.Assert(false, "unknown kind of literal " + node.tok.ToString());
@@ -1002,9 +1005,12 @@ namespace Microsoft.Boogie.VCExprAST {
if (cce.NonNull(e.Type).IsInt) {
return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);
}
- else {
+ else if (cce.NonNull(e.Type).IsReal) {
return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);
}
+ else {//is float
+ return Gen.Function(VCExpressionGenerator.SubFOp, Gen.Float(BigFloat.ZERO), e);
+ }
}
else {
return Gen.Not(this.args);
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs
index e0a4b4c6..0ff6d67f 100644
--- a/Source/VCExpr/SimplifyLikeLineariser.cs
+++ b/Source/VCExpr/SimplifyLikeLineariser.cs
@@ -380,9 +380,14 @@ namespace Microsoft.Boogie.VCExprAST {
internal const string realSubName = "realSub";
internal const string realMulName = "realMul";
internal const string realDivName = "realDiv";
+ internal const string floatAddName = "floatAdd";
+ internal const string floatSubName = "floatSub";
+ internal const string floatMulName = "floatMul";
+ internal const string floatDivName = "floatDiv";
internal const string realPowName = "realPow";
internal const string toIntName = "toIntCoercion";
internal const string toRealName = "toRealCoercion";
+ internal const string toFloatName = "toFloatCoercion";
internal void AssertAsTerm(string x, LineariserOptions options) {
Contract.Requires(options != null);
@@ -943,9 +948,12 @@ namespace Microsoft.Boogie.VCExprAST {
WriteTermApplication(intAddName, node, options);
}
}
- else {
+ else if (node.Type.IsReal) {
WriteTermApplication(realAddName, node, options);
}
+ else {
+ WriteTermApplication(floatAddName, node, options);
+ }
return true;
}
@@ -955,9 +963,12 @@ namespace Microsoft.Boogie.VCExprAST {
if (node.Type.IsInt) {
WriteTermApplication(intSubName, node, options);
}
- else {
+ else if (node.Type.IsReal) {
WriteTermApplication(realSubName, node, options);
}
+ else {
+ WriteTermApplication(floatSubName, node, options);
+ }
return true;
}
@@ -967,9 +978,12 @@ namespace Microsoft.Boogie.VCExprAST {
if (node.Type.IsInt) {
WriteTermApplication(intMulName, node, options);
}
- else {
+ else if (node.Type.IsReal) {
WriteTermApplication(realMulName, node, options);
}
+ else {
+ WriteTermApplication(floatMulName, node, options);
+ }
return true;
}
@@ -994,6 +1008,14 @@ namespace Microsoft.Boogie.VCExprAST {
return true;
}
+ public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatDivName, node, options);
+ return true;
+ }
+
public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
@@ -1057,6 +1079,14 @@ namespace Microsoft.Boogie.VCExprAST {
return true;
}
+ public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteApplication(toFloatName, node, options);
+ return true;
+ }
+
public bool VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options) {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs
index 4f8dc08e..291d6d42 100644
--- a/Source/VCExpr/VCExprAST.cs
+++ b/Source/VCExpr/VCExprAST.cs
@@ -55,6 +55,13 @@ namespace Microsoft.Boogie {
return new VCExprRealLit(x);
}
+ public VCExpr/*!*/ Float(BigFloat x)
+ {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ return new VCExprFloatLit(x);
+ }
+
public VCExpr/*!*/ Function(VCExprOp/*!*/ op,
List<VCExpr/*!*/>/*!*/ arguments,
List<Type/*!*/>/*!*/ typeArguments) {
@@ -317,12 +324,16 @@ namespace Microsoft.Boogie {
public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real);
+ public static readonly VCExprOp AddFOp = new VCExprNAryOp(2, Type.Float);
public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real);
+ public static readonly VCExprOp SubFOp = new VCExprNAryOp(2, Type.Float);
public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real);
+ public static readonly VCExprOp MulFOp = new VCExprNAryOp(2, Type.Float);
public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real);
+ public static readonly VCExprOp DivFOp = new VCExprNAryOp(2, Type.Float);
public static readonly VCExprOp ModOp = new VCExprNAryOp(2, Type.Int);
public static readonly VCExprOp PowOp = new VCExprNAryOp(2, Type.Real);
public static readonly VCExprOp LtOp = new VCExprNAryOp(2, Type.Bool);
@@ -336,6 +347,7 @@ namespace Microsoft.Boogie {
public static readonly VCExprOp IfThenElseOp = new VCExprIfThenElseOp();
public static readonly VCExprOp ToIntOp = new VCExprNAryOp(1, Type.Int);
public static readonly VCExprOp ToRealOp = new VCExprNAryOp(1, Type.Real);
+ public static readonly VCExprOp ToFloatOp = new VCExprNAryOp(1, Type.Float);
public static readonly VCExprOp TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);
@@ -391,6 +403,7 @@ namespace Microsoft.Boogie {
DivOp,
ModOp,
RealDivOp,
+ FloatDivOp,
PowOp,
LtOp,
LeOp,
@@ -400,7 +413,8 @@ namespace Microsoft.Boogie {
Subtype3Op,
BvConcatOp,
ToIntOp,
- ToRealOp
+ ToRealOp,
+ ToFloatOp
};
internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;
[ContractInvariantMethod]
@@ -425,6 +439,7 @@ namespace Microsoft.Boogie {
SingletonOpDict.Add(MulROp, SingletonOp.MulOp);
SingletonOpDict.Add(DivIOp, SingletonOp.DivOp);
SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp);
+ SingletonOpDict.Add(DivFOp, SingletonOp.FloatDivOp);
SingletonOpDict.Add(ModOp, SingletonOp.ModOp);
SingletonOpDict.Add(PowOp, SingletonOp.PowOp);
SingletonOpDict.Add(LtOp, SingletonOp.LtOp);
@@ -435,6 +450,7 @@ namespace Microsoft.Boogie {
SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);
SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp);
SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp);
+ SingletonOpDict.Add(ToFloatOp, SingletonOp.ToFloatOp);
}
////////////////////////////////////////////////////////////////////////////////
@@ -856,6 +872,31 @@ namespace Microsoft.Boogie.VCExprAST {
}
}
+ public class VCExprFloatLit : VCExprLiteral
+ {
+ public readonly BigFloat Val;
+ internal VCExprFloatLit(BigFloat val)
+ : base(Type.Float)
+ {
+ this.Val = val;
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that)
+ {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprFloatLit)
+ return Val == ((VCExprFloatLit)that).Val;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode()
+ {
+ return Val.GetHashCode() * 72321;
+ }
+ }
+
/////////////////////////////////////////////////////////////////////////////////
// Operator expressions with fixed arity
[ContractClassFor(typeof(VCExprNAry))]
@@ -1265,6 +1306,8 @@ namespace Microsoft.Boogie.VCExprAST {
return visitor.VisitModOp(expr, arg);
case VCExpressionGenerator.SingletonOp.RealDivOp:
return visitor.VisitRealDivOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.FloatDivOp:
+ return visitor.VisitFloatDivOp(expr, arg);
case VCExpressionGenerator.SingletonOp.PowOp:
return visitor.VisitPowOp(expr, arg);
case VCExpressionGenerator.SingletonOp.LtOp:
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs
index 00e6fb9c..8b79b0e5 100644
--- a/Source/VCExpr/VCExprASTPrinter.cs
+++ b/Source/VCExpr/VCExprASTPrinter.cs
@@ -302,6 +302,12 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return PrintNAry("/", node, wr);
}
+ public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("/f", node, wr);
+ }
public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
@@ -347,6 +353,12 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return PrintNAry("real", node, wr);
}
+ public bool VisitToFloatOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("float", node, wr);
+ }
public bool VisitBoogieFunctionOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
diff --git a/Source/VCExpr/VCExprASTVisitors.cs b/Source/VCExpr/VCExprASTVisitors.cs
index ad0c270d..1bcce113 100644
--- a/Source/VCExpr/VCExprASTVisitors.cs
+++ b/Source/VCExpr/VCExprASTVisitors.cs
@@ -77,6 +77,7 @@ namespace Microsoft.Boogie.VCExprAST {
Result VisitDivOp(VCExprNAry node, Arg arg);
Result VisitModOp(VCExprNAry node, Arg arg);
Result VisitRealDivOp(VCExprNAry node, Arg arg);
+ Result VisitFloatDivOp(VCExprNAry node, Arg arg); //TODO: Add this to references from above and below
Result VisitPowOp(VCExprNAry node, Arg arg);
Result VisitLtOp(VCExprNAry node, Arg arg);
Result VisitLeOp(VCExprNAry node, Arg arg);
@@ -189,6 +190,12 @@ namespace Microsoft.Boogie.VCExprAST {
throw new NotImplementedException();
}
+ public Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
public Result VisitPowOp(VCExprNAry node, Arg arg) {
Contract.Requires(node != null);
throw new NotImplementedException();
@@ -234,6 +241,12 @@ namespace Microsoft.Boogie.VCExprAST {
throw new NotImplementedException();
}
+ public Result VisitToFloat(VCExprNAry node, Arg arg) //TODO: modify later
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
Contract.Requires(node != null);
throw new NotImplementedException();
@@ -1482,6 +1495,11 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return StandardResult(node, arg);
}
+ public virtual Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
public virtual Result VisitPowOp(VCExprNAry node, Arg arg) {
//Contract.Requires(node != null);
return StandardResult(node, arg);
@@ -1518,6 +1536,11 @@ namespace Microsoft.Boogie.VCExprAST {
//Contract.Requires(node != null);
return StandardResult(node, arg);
}
+ public virtual Result VisitToFloatOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
public virtual Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
//Contract.Requires(node != null);
return StandardResult(node, arg);
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-24 02:54:20 +0000