diff options
Diffstat (limited to 'Source/VCExpr')
| -rw-r--r-- | Source/VCExpr/Boogie2VCExpr.cs | 36 | ||||
| -rw-r--r-- | Source/VCExpr/SimplifyLikeLineariser.cs | 120 | ||||
| -rw-r--r-- | Source/VCExpr/TypeErasure.cs | 84 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprAST.cs | 56 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTPrinter.cs | 72 | ||||
| -rw-r--r-- | Source/VCExpr/VCExprASTVisitors.cs | 154 |
6 files changed, 479 insertions, 43 deletions
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index f0dc505d..ad319c0e 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -1076,34 +1076,48 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(cce.NonNullElements(args));
Contract.Ensures(Contract.Result<VCExpr>() != null);
Contract.Assert(args.Count == 2);
+ Type t = cce.NonNull(cce.NonNull(args[0]).Type);
switch (app.Op) {
case BinaryOperator.Opcode.Add:
- if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ if (t.IsInt) {
return Gen.Function(VCExpressionGenerator.AddIOp, args);
}
- else {
+ else if (t.IsReal) {
return Gen.Function(VCExpressionGenerator.AddROp, args);
}
+ else { //t is float
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "+"), args);
+ }
case BinaryOperator.Opcode.Sub:
- if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ if (t.IsInt) {
return Gen.Function(VCExpressionGenerator.SubIOp, args);
}
- else {
+ else if (t.IsReal) {
return Gen.Function(VCExpressionGenerator.SubROp, args);
}
+ else { //t is float
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "-"), args);
+ }
case BinaryOperator.Opcode.Mul:
- if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ if (t.IsInt) {
return Gen.Function(VCExpressionGenerator.MulIOp, args);
}
- else {
+ else if (t.IsReal) {
return Gen.Function(VCExpressionGenerator.MulROp, args);
}
+ else
+ { //t is float
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "*"), args);
+ }
case BinaryOperator.Opcode.Div:
return Gen.Function(VCExpressionGenerator.DivIOp, args);
case BinaryOperator.Opcode.Mod:
return Gen.Function(VCExpressionGenerator.ModOp, args);
case BinaryOperator.Opcode.RealDiv:
+ if (t.IsFloat) {
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "/"), args);
+ }
VCExpr arg0 = cce.NonNull(args[0]);
VCExpr arg1 = cce.NonNull(args[1]);
if (cce.NonNull(arg0.Type).IsInt) {
@@ -1118,16 +1132,26 @@ namespace Microsoft.Boogie.VCExprAST { case BinaryOperator.Opcode.Eq:
case BinaryOperator.Opcode.Iff:
// we don't distinguish between equality and equivalence at this point
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "=="), args);
return Gen.Function(VCExpressionGenerator.EqOp, args);
case BinaryOperator.Opcode.Neq:
return Gen.Function(VCExpressionGenerator.NeqOp, args);
case BinaryOperator.Opcode.Lt:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "<"), args);
return Gen.Function(VCExpressionGenerator.LtOp, args);
case BinaryOperator.Opcode.Le:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, "<="), args);
return Gen.Function(VCExpressionGenerator.LeOp, args);
case BinaryOperator.Opcode.Ge:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, ">="), args);
return Gen.Function(VCExpressionGenerator.GeOp, args);
case BinaryOperator.Opcode.Gt:
+ if (t.IsFloat)
+ return Gen.Function(Gen.BinaryFloatOp(t.FloatExponent, t.FloatMantissa, ">"), args);
return Gen.Function(VCExpressionGenerator.GtOp, args);
case BinaryOperator.Opcode.Imp:
return Gen.Function(VCExpressionGenerator.ImpliesOp, args);
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 0ff6d67f..6f74fe08 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -384,6 +384,14 @@ namespace Microsoft.Boogie.VCExprAST { internal const string floatSubName = "floatSub";
internal const string floatMulName = "floatMul";
internal const string floatDivName = "floatDiv";
+ internal const string floatRemName = "floatRem";
+ internal const string floatMinName = "floatMin";
+ internal const string floatMaxName = "floatMax";
+ internal const string floatLeqName = "floatLeq";
+ internal const string floatLtName = "floatLt";
+ internal const string floatGeqName = "floatGeq";
+ internal const string floatGtName = "floatGt";
+ internal const string floatEqName = "floatEq";
internal const string realPowName = "realPow";
internal const string toIntName = "toIntCoercion";
internal const string toRealName = "toRealCoercion";
@@ -888,7 +896,104 @@ namespace Microsoft.Boogie.VCExprAST { return true;
}
- public bool VisitBvOp(VCExprNAry node, LineariserOptions options) {
+ public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatAddName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatSubName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatMulName, node, options);
+ 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 VisitFloatRemOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatRemName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatMinName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatMaxName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatLeqName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatLtName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatGeqName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatGtName, node, options);
+ return true;
+ }
+
+ public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options)
+ {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(floatEqName, node, options);
+ return true;
+ }
+
+ public bool VisitBvOp(VCExprNAry node, LineariserOptions options)
+ {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
WriteTermApplication("$make_bv" + node.Type.BvBits, node, options);
@@ -948,11 +1053,8 @@ namespace Microsoft.Boogie.VCExprAST { WriteTermApplication(intAddName, node, options);
}
}
- else if (node.Type.IsReal) {
- WriteTermApplication(realAddName, node, options);
- }
else {
- WriteTermApplication(floatAddName, node, options);
+ WriteTermApplication(realAddName, node, options);
}
return true;
}
@@ -1008,14 +1110,6 @@ 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);
diff --git a/Source/VCExpr/TypeErasure.cs b/Source/VCExpr/TypeErasure.cs index 5e821ea2..6fb38c27 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -1479,6 +1479,90 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArgumentsToOldType(node, bindings, 0);
}
+ public override VCExpr VisitFloatAddOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatSubOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatMulOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatDivOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatRemOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatMinOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatMaxOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatLeqOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatLtOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatGeqOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatGtOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
+ public override VCExpr VisitFloatEqOp(VCExprNAry node, VariableBindings bindings)
+ {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArgumentsToOldType(node, bindings, 0);
+ }
public override VCExpr VisitBvOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
diff --git a/Source/VCExpr/VCExprAST.cs b/Source/VCExpr/VCExprAST.cs index c44800fc..3f6e3b7a 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -324,7 +324,6 @@ 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);
@@ -359,11 +358,13 @@ namespace Microsoft.Boogie { // Float nodes
- public VCExpr AddFOp(VCExpr f1, VCExpr f2)
+ public VCExprOp BinaryFloatOp(int exp, int man, string op)
{
- Contract.Requires(f1 != null);
- Contract.Requires(f2 != null);
- return Function(new VCExprFloatOp(f1.Type.FloatExponent, f1.Type.FloatMantissa));
+ Contract.Requires(exp > 0);
+ Contract.Requires(man > 0);
+ Contract.Requires(op != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return new VCExprBinaryFloatOp(exp, man, op);
}
// Bitvector nodes
@@ -441,7 +442,6 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);
SingletonOpDict.Add(AddIOp, SingletonOp.AddOp);
SingletonOpDict.Add(AddROp, SingletonOp.AddOp);
- //SingletonOpDict.Add(AddFOp, SingletonOp.AddOp);
SingletonOpDict.Add(SubIOp, SingletonOp.SubOp);
SingletonOpDict.Add(SubROp, SingletonOp.SubOp);
//SingletonOpDict.Add(SubFOp, SingletonOp.SubOp);
@@ -1677,18 +1677,19 @@ namespace Microsoft.Boogie.VCExprAST { /////////////////////////////////////////////////////////////////////////////////
// Float operators
- public class VCExprFloatOp : VCExprOp {
+ public class VCExprBinaryFloatOp : VCExprOp {
public readonly int Mantissa;
public readonly int Exponent;
+ private string op;
public override int Arity {
get {
- return 1;
+ return 2;
}
}
public override int TypeParamArity {
get {
- return 0;
+ return 2;
}
}
public override Type InferType(List<VCExpr> args, List<Type/*!*/>/*!*/ typeArgs) {
@@ -1703,8 +1704,8 @@ namespace Microsoft.Boogie.VCExprAST { public override bool Equals(object that) {
if (Object.ReferenceEquals(this, that))
return true;
- if (that is VCExprFloatOp)
- return this.Exponent == ((VCExprFloatOp)that).Exponent && this.Mantissa == ((VCExprFloatOp)that).Mantissa;
+ if (that is VCExprBinaryFloatOp)
+ return this.Exponent == ((VCExprBinaryFloatOp)that).Exponent && this.Mantissa == ((VCExprBinaryFloatOp)that).Mantissa;
return false;
}
[Pure]
@@ -1712,15 +1713,44 @@ namespace Microsoft.Boogie.VCExprAST { return Exponent * 81748912 + Mantissa * 67867979;
}
- internal VCExprFloatOp(int exp, int man) {
+ internal VCExprBinaryFloatOp(int exp, int man, string op) {
this.Exponent = exp;
this.Mantissa = man;
+ this.op = op;
}
public override Result Accept<Result, Arg>
(VCExprNAry expr, IVCExprOpVisitor<Result, Arg> visitor, Arg arg) {
//Contract.Requires(visitor != null);
//Contract.Requires(expr != null);
- return visitor.VisitBvOp(expr, arg);
+ switch (op) {
+ case ("+"):
+ return visitor.VisitFloatAddOp(expr, arg);
+ case ("-"):
+ return visitor.VisitFloatSubOp(expr, arg);
+ case ("*"):
+ return visitor.VisitFloatMulOp(expr, arg);
+ case ("/"):
+ return visitor.VisitFloatDivOp(expr, arg);
+ case ("rem"):
+ return visitor.VisitFloatRemOp(expr, arg);
+ case ("min"):
+ return visitor.VisitFloatMinOp(expr, arg);
+ case ("max"):
+ return visitor.VisitFloatMaxOp(expr, arg);
+ case ("<="):
+ return visitor.VisitFloatLeqOp(expr, arg);
+ case ("<"):
+ return visitor.VisitFloatLtOp(expr, arg);
+ case (">="):
+ return visitor.VisitFloatGeqOp(expr, arg);
+ case (">"):
+ return visitor.VisitFloatGtOp(expr, arg);
+ case ("=="):
+ return visitor.VisitFloatEqOp(expr, arg);
+ default:
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
+ }
}
}
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index 00e6fb9c..8e2f5d12 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -242,6 +242,78 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null);
return PrintNAry("Store", node, wr);
}
+ public bool VisitFloatAddOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.add", node, wr);
+ }
+ public bool VisitFloatSubOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.sub", node, wr);
+ }
+ public bool VisitFloatMulOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.mul", node, wr);
+ }
+ public bool VisitFloatDivOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.div", node, wr);
+ }
+ public bool VisitFloatRemOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.rem", node, wr);
+ }
+ public bool VisitFloatMinOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.min", node, wr);
+ }
+ public bool VisitFloatMaxOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.max", node, wr);
+ }
+ public bool VisitFloatLeqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.leq", node, wr);
+ }
+ public bool VisitFloatLtOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.lt", node, wr);
+ }
+ public bool VisitFloatGeqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.geq", node, wr);
+ }
+ public bool VisitFloatGtOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.gt", node, wr);
+ }
+ public bool VisitFloatEqOp(VCExprNAry node, TextWriter wr)
+ {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("fp.eq", node, wr);
+ }
public bool VisitBvOp(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 a1fb2ff4..c81f69e5 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -68,6 +68,18 @@ namespace Microsoft.Boogie.VCExprAST { Result VisitLabelOp(VCExprNAry node, Arg arg);
Result VisitSelectOp(VCExprNAry node, Arg arg);
Result VisitStoreOp(VCExprNAry node, Arg arg);
+ Result VisitFloatAddOp(VCExprNAry node, Arg arg);
+ Result VisitFloatSubOp(VCExprNAry node, Arg arg);
+ Result VisitFloatMulOp(VCExprNAry node, Arg arg);
+ Result VisitFloatDivOp(VCExprNAry node, Arg arg);
+ Result VisitFloatRemOp(VCExprNAry node, Arg arg);
+ Result VisitFloatMinOp(VCExprNAry node, Arg arg);
+ Result VisitFloatMaxOp(VCExprNAry node, Arg arg);
+ Result VisitFloatLeqOp(VCExprNAry node, Arg arg);
+ Result VisitFloatLtOp(VCExprNAry node, Arg arg);
+ Result VisitFloatGeqOp(VCExprNAry node, Arg arg);
+ Result VisitFloatGtOp(VCExprNAry node, Arg arg);
+ Result VisitFloatEqOp(VCExprNAry node, Arg arg);
Result VisitBvOp(VCExprNAry node, Arg arg);
Result VisitBvExtractOp(VCExprNAry node, Arg arg);
Result VisitBvConcatOp(VCExprNAry node, Arg arg);
@@ -144,6 +156,78 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException();
}
+ public Result VisitFloatAddOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatDivOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatRemOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+ {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
public Result VisitBvOp(VCExprNAry node, Arg arg) {
Contract.Requires(node != null);
throw new NotImplementedException();
@@ -189,12 +273,6 @@ 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();
@@ -1450,6 +1528,65 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null);
return StandardResult(node, arg);
}
+ public virtual Result VisitFloatAddOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatSubOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatMulOp(VCExprNAry node, Arg arg)
+ {
+ //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 VisitFloatRemOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatMinOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatMaxOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatLeqOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatLtOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatGeqOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatGtOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitFloatEqOp(VCExprNAry node, Arg arg)
+ {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
public virtual Result VisitBvOp(VCExprNAry node, Arg arg) {
//Contract.Requires(node != null);
return StandardResult(node, arg);
@@ -1494,11 +1631,6 @@ 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);
|