diff options
| author |  boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
|---|---|---|
| committer | boehmes <unknown> | 2012-09-27 17:13:45 +0200 |
| commit | 43b80b13bd24bb789849aac3385df6ac4a8233be (patch) | |
| tree | 499b3dffd74fd84fdf8aedffacbca424d25680b2 | |
| parent | dfb77ee06c82cf8b9c465f3a2acbc5ceb035c6e5 (diff) | |
Boogie: added type 'real' with overloaded arithmetic operations plus real division '/' and (uninterpreted) real exponentiation '**', real literals and coercion functions 'int' and 'real';
Integer operations 'div' and 'mod' are now mapped to corresponding SMT-LIB operations instead of treating them uninterpreted;
Made unary minus valid Boogie syntax again (the expression '- e' used to be rewritten by the parser to '0 - e', now this is done when generating VCs);
Extended the BigDec class with additional functionality;
Added test cases for SMT-LIB prover backend (the Z3 API interface has been adapted accordingly, but is untested)
39 files changed, 1825 insertions, 751 deletions
diff --git a/Binaries/UnivBackPred2.smt2 b/Binaries/UnivBackPred2.smt2 index d3e3777f..9bb05bfb 100644 --- a/Binaries/UnivBackPred2.smt2 +++ b/Binaries/UnivBackPred2.smt2 @@ -3,7 +3,6 @@ (set-info :category "industrial")
(declare-sort |T@U| 0)
(declare-sort |T@T| 0)
-(declare-fun int_div (Int Int) Int)
-(declare-fun int_mod (Int Int) Int)
+(declare-fun real_pow (Real Real) Real)
(declare-fun UOrdering2 (|T@U| |T@U|) Bool)
(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool)
diff --git a/Source/AbsInt/IntervalDomain.cs b/Source/AbsInt/IntervalDomain.cs index 247a357d..51391105 100644 --- a/Source/AbsInt/IntervalDomain.cs +++ b/Source/AbsInt/IntervalDomain.cs @@ -632,6 +632,10 @@ namespace Microsoft.Boogie.AbstractInterpretation var n = ((BigNum)node.Val).ToBigInteger;
Lo = n;
Hi = n + 1;
+ } else if (node.Val is BigDec) {
+ var n = ((BigDec)node.Val).Floor(-BigInteger.Pow(10, 12), BigInteger.Pow(10, 12));
+ Lo = n;
+ Hi = n + 1;
} else if (node.Val is bool) {
if ((bool)node.Val) {
// true
@@ -646,7 +650,7 @@ namespace Microsoft.Boogie.AbstractInterpretation return node;
}
public override Expr VisitIdentifierExpr(IdentifierExpr node) {
- if (node.Type.IsBool || node.Type.IsInt) {
+ if (node.Type.IsBool || node.Type.IsInt || node.Type.IsReal) {
Node.GetBounds(N, node.Decl, out Lo, out Hi);
}
return node;
@@ -655,7 +659,18 @@ namespace Microsoft.Boogie.AbstractInterpretation if (node.Fun is UnaryOperator) {
var op = (UnaryOperator)node.Fun;
Contract.Assert(node.Args.Length == 1);
- if (op.Op == UnaryOperator.Opcode.Not) {
+ if (op.Op == UnaryOperator.Opcode.Neg) {
+ BigInteger? lo, hi;
+ VisitExpr(node.Args[0]);
+ lo = Lo; hi = Hi;
+ if (hi != null) {
+ Lo = 1 - hi;
+ }
+ if (lo != null) {
+ Hi = -lo;
+ }
+ }
+ else if (op.Op == UnaryOperator.Opcode.Not) {
VisitExpr(node.Args[0]);
Contract.Assert((Lo == null && Hi == null) ||
(Lo == null && (BigInteger)Hi == 1) ||
@@ -803,6 +818,20 @@ namespace Microsoft.Boogie.AbstractInterpretation Hi = hi1;
}
break;
+ case BinaryOperator.Opcode.RealDiv:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = new BigInteger(0);
+ Hi = hi1;
+ }
+ break;
+ case BinaryOperator.Opcode.Pow:
+ // this uses an incomplete approximation that could be tightened up
+ if (lo0 != null && lo1 != null && 0 <= (BigInteger)lo0 && 0 <= (BigInteger)lo1) {
+ Lo = new BigInteger(0);
+ Hi = hi1;
+ }
+ break;
default:
break;
}
diff --git a/Source/Basetypes/BigDec.cs b/Source/Basetypes/BigDec.cs index 78b19794..6059539b 100755 --- a/Source/Basetypes/BigDec.cs +++ b/Source/Basetypes/BigDec.cs @@ -19,59 +19,86 @@ namespace Microsoft.Basetypes { // the internal representation
[Rep]
- internal readonly BIM mantisse;
+ internal readonly BIM mantissa;
[Rep]
- internal readonly BIM exponent;
+ internal readonly int exponent;
- private static readonly BIM ONE = BIM.One;
- private static readonly BIM TEN = new BIM(10);
+ public BIM Mantissa {
+ get {
+ return mantissa;
+ }
+ }
+
+ public int Exponent {
+ get {
+ return exponent;
+ }
+ }
+
+ public static readonly BigDec ZERO = FromInt(0);
+ private static readonly BIM ten = new BIM(10);
////////////////////////////////////////////////////////////////////////////
// Constructors
[Pure]
+ public static BigDec FromInt(int v) {
+ return new BigDec(v, 0);
+ }
+
+ [Pure]
public static BigDec FromString(string v) {
if (v == null) throw new FormatException();
BIM integral = BIM.Zero;
BIM fraction = BIM.Zero;
- BIM exponent = BIM.Zero;
+ int exponent = 0;
int len = v.Length;
int i = v.IndexOf('e');
if (i >= 0) {
- exponent = BIM.Parse(v.Substring(i + 1, len - i));
+ if (i + 1 == v.Length) throw new FormatException();
+ exponent = Int32.Parse(v.Substring(i + 1, len - i - 1));
len = i;
}
- int fraction_len = 0;
+ int fractionLen = 0;
i = v.IndexOf('.');
if (i >= 0) {
- fraction = BIM.Parse(v.Substring(i + 1, len - i));
- fraction_len = len - i;
+ if (i + 1 == v.Length) throw new FormatException();
+ fractionLen = len - i - 1;
+ fraction = BIM.Parse(v.Substring(i + 1, fractionLen));
len = i;
}
integral = BIM.Parse(v.Substring(0, len));
- while (fraction_len > 0) {
- integral = integral * TEN;
- exponent = exponent - ONE;
+ if (!fraction.IsZero) {
+ while (fractionLen > 0) {
+ integral = integral * ten;
+ exponent = exponent - 1;
+ fractionLen = fractionLen - 1;
+ }
}
return new BigDec(integral + fraction, exponent);
}
- internal BigDec(BIM mantisse, BIM exponent) {
- while (mantisse % TEN == BIM.Zero) {
- mantisse = mantisse / TEN;
- exponent = exponent + ONE;
+ internal BigDec(BIM mantissa, int exponent) {
+ if (mantissa.IsZero) {
+ this.mantissa = mantissa;
+ this.exponent = 0;
+ }
+ else {
+ while (mantissa % ten == BIM.Zero) {
+ mantissa = mantissa / ten;
+ exponent = exponent + 1;
+ }
+ this.mantissa = mantissa;
+ this.exponent = exponent;
}
-
- this.mantisse = mantisse;
- this.exponent = exponent;
}
@@ -86,19 +113,84 @@ namespace Microsoft.Basetypes { if (!(obj is BigDec))
return false;
- BigDec other = (BigDec)obj;
- return (this.mantisse == other.mantisse && this.exponent == other.exponent);
+ return (this == (BigDec)obj);
}
[Pure]
public override int GetHashCode() {
- return this.mantisse.GetHashCode() * 13 + this.exponent.GetHashCode();
+ return this.mantissa.GetHashCode() * 13 + this.exponent.GetHashCode();
}
[Pure]
public override string/*!*/ ToString() {
Contract.Ensures(Contract.Result<string>() != null);
- return String.Format("%se%s", this.mantisse.ToString(), this.exponent.ToString());
+ return String.Format("{0}e{1}", this.mantissa.ToString(), this.exponent.ToString());
+ }
+
+
+ ////////////////////////////////////////////////////////////////////////////
+ // Conversion operations
+
+ [Pure]
+ public BIM Floor(BIM? minimum, BIM? maximum) {
+ BIM n = this.mantissa;
+
+ if (this.exponent >= 0) {
+ int e = this.exponent;
+ while (e > 0 && (minimum == null || minimum <= n) && (maximum == null || n <= maximum)) {
+ n = n * ten;
+ e = e - 1;
+ }
+ }
+ else {
+ int e = -this.exponent;
+ while (e > 0 && !n.IsZero) {
+ n = n / ten;
+ e = e - 1;
+ }
+ }
+
+ if (minimum != null && n < minimum)
+ return (BIM)minimum;
+ else if (maximum != null && maximum < n)
+ return (BIM)maximum;
+ else
+ return n;
+ }
+
+ [Pure]
+ public String ToDecimalString(int maxDigits) {
+ string s = this.mantissa.ToString();
+ int digits = (this.mantissa >= 0) ? s.Length : s.Length - 1;
+ BIM max = BIM.Pow(10, maxDigits);
+ BIM min = -max;
+
+ if (this.exponent >= 0) {
+ if (maxDigits < digits || maxDigits - digits < this.exponent) {
+ return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
+ }
+ else {
+ return String.Format("{0}{1}.0", s, new string('0', this.exponent));
+ }
+ }
+ else {
+ int exp = -this.exponent;
+
+ if (exp < digits) {
+ int intDigits = digits - exp;
+ if (maxDigits < intDigits) {
+ return String.Format("{0}.0", (this.mantissa >= 0) ? max.ToString() : min.ToString());
+ }
+ else {
+ int fracDigits = Math.Min(maxDigits, digits - intDigits);
+ return String.Format("{0}.{1}", s.Substring(0, intDigits), s.Substring(intDigits, fracDigits));
+ }
+ }
+ else {
+ int fracDigits = Math.Min(maxDigits, digits);
+ return String.Format("0.{0}{1}", new string('0', exp - fracDigits), s.Substring(0, fracDigits));
+ }
+ }
}
@@ -106,26 +198,40 @@ namespace Microsoft.Basetypes { // Basic arithmetic operations
[Pure]
+ public BigDec Abs {
+ get {
+ return new BigDec(BIM.Abs(this.mantissa), this.exponent);
+ }
+ }
+
+ [Pure]
+ public BigDec Negate {
+ get {
+ return new BigDec(BIM.Negate(this.mantissa), this.exponent);
+ }
+ }
+
+ [Pure]
public static BigDec operator -(BigDec x) {
- return new BigDec(BIM.Negate(x.mantisse), x.exponent);
+ return x.Negate;
}
[Pure]
public static BigDec operator +(BigDec x, BigDec y) {
- BIM m1 = x.mantisse;
- BIM e1 = x.exponent;
- BIM m2 = y.mantisse;
- BIM e2 = y.exponent;
+ BIM m1 = x.mantissa;
+ int e1 = x.exponent;
+ BIM m2 = y.mantissa;
+ int e2 = y.exponent;
if (e2 < e1) {
- m1 = y.mantisse;
+ m1 = y.mantissa;
e1 = y.exponent;
- m2 = x.mantisse;
+ m2 = x.mantissa;
e2 = x.exponent;
}
while (e2 > e1) {
- m2 = m2 * TEN;
- e2 = e2 - ONE;
+ m2 = m2 * ten;
+ e2 = e2 - 1;
}
return new BigDec(m1 + m2, e1);
@@ -133,12 +239,12 @@ namespace Microsoft.Basetypes { [Pure]
public static BigDec operator -(BigDec x, BigDec y) {
- return x + (-y);
+ return x + y.Negate;
}
[Pure]
public static BigDec operator *(BigDec x, BigDec y) {
- return new BigDec(x.mantisse * y.mantisse, x.exponent + y.exponent);
+ return new BigDec(x.mantissa * y.mantissa, x.exponent + y.exponent);
}
@@ -147,38 +253,44 @@ namespace Microsoft.Basetypes { public bool IsPositive {
get {
- return (this.mantisse > BIM.Zero);
+ return (this.mantissa > BIM.Zero);
}
}
public bool IsNegative {
get {
- return (this.mantisse < BIM.Zero);
+ return (this.mantissa < BIM.Zero);
}
}
public bool IsZero {
get {
- return this.mantisse.IsZero;
+ return this.mantissa.IsZero;
}
}
[Pure]
public int CompareTo(BigDec that) {
- BigDec d = this - that;
-
- if (d.IsZero) {
+ if (this.mantissa == that.mantissa && this.exponent == that.exponent) {
return 0;
}
- else if (d.IsNegative) {
- return -1;
- }
else {
- return 1;
+ BigDec d = this - that;
+ return d.IsNegative ? -1 : 1;
}
}
[Pure]
+ public static bool operator ==(BigDec x, BigDec y) {
+ return x.CompareTo(y) == 0;
+ }
+
+ [Pure]
+ public static bool operator !=(BigDec x, BigDec y) {
+ return x.CompareTo(y) != 0;
+ }
+
+ [Pure]
public static bool operator <(BigDec x, BigDec y) {
return x.CompareTo(y) < 0;
}
diff --git a/Source/Core/AbsyExpr.cs b/Source/Core/AbsyExpr.cs index d2b8506a..61511b33 100644 --- a/Source/Core/AbsyExpr.cs +++ b/Source/Core/AbsyExpr.cs @@ -250,6 +250,18 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<NAryExpr>() != null);
return Binary(BinaryOperator.Opcode.Mod, e1, e2);
}
+ public static NAryExpr RealDiv(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.RealDiv, e1, e2);
+ }
+ public static NAryExpr Pow(Expr e1, Expr e2) {
+ Contract.Requires(e2 != null);
+ Contract.Requires(e1 != null);
+ Contract.Ensures(Contract.Result<NAryExpr>() != null);
+ return Binary(BinaryOperator.Opcode.Pow, e1, e2);
+ }
public static NAryExpr Subtype(Expr e1, Expr e2) {
Contract.Requires(e2 != null);
Contract.Requires(e1 != null);
@@ -283,6 +295,10 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<LiteralExpr>() != null);
return new LiteralExpr(Token.NoToken, value);
}
+ public static LiteralExpr Literal(BigDec value) {
+ Contract.Ensures(Contract.Result<LiteralExpr>() != null);
+ return new LiteralExpr(Token.NoToken, value);
+ }
private static LiteralExpr/*!*/ true_ = Literal(true);
public static LiteralExpr/*!*/ True {
@@ -401,7 +417,7 @@ namespace Microsoft.Boogie { }
public class LiteralExpr : Expr {
- public readonly object/*!*/ Val; // false, true, a BigNum, or a BvConst
+ public readonly object/*!*/ Val; // false, true, a BigNum, a BigDec, or a BvConst
[ContractInvariantMethod]
void ObjectInvariant() {
Contract.Invariant(Val != null);
@@ -418,6 +434,7 @@ namespace Microsoft.Boogie { Val = b;
Type = Type.Bool;
}
+
/// <summary>
/// Creates a literal expression for the integer value "v".
/// </summary>
@@ -431,6 +448,18 @@ namespace Microsoft.Boogie { }
/// <summary>
+ /// Creates a literal expression for the real value "v".
+ /// </summary>
+ /// <param name="tok"></param>
+ /// <param name="v"></param>
+ public LiteralExpr(IToken/*!*/ tok, BigDec v)
+ : base(tok) {
+ Contract.Requires(tok != null);
+ Val = v;
+ Type = Type.Real;
+ }
+
+ /// <summary>
/// Creates a literal expression for the bitvector value "v".
/// </summary>
public LiteralExpr(IToken/*!*/ tok, BigNum v, int b)
@@ -487,6 +516,8 @@ namespace Microsoft.Boogie { return Type.Bool;
} else if (Val is BigNum) {
return Type.Int;
+ } else if (Val is BigDec) {
+ return Type.Real;
} else if (Val is BvConst) {
return Type.GetBvType(((BvConst)Val).Bits);
} else {
@@ -529,6 +560,19 @@ namespace Microsoft.Boogie { }
}
+ public bool isBigDec {
+ get {
+ return Val is BigDec;
+ }
+ }
+
+ public BigDec asBigDec {
+ get {
+ Contract.Assert(isBigDec);
+ return (BigDec)cce.NonNull(Val);
+ }
+ }
+
public bool isBool {
get {
return Val is bool;
@@ -838,6 +882,7 @@ namespace Microsoft.Boogie { T Visit(MapSelect/*!*/ mapSelect);
T Visit(MapStore/*!*/ mapStore);
T Visit(TypeCoercion/*!*/ typeCoercion);
+ T Visit(ArithmeticCoercion/*!*/ arithCoercion);
T Visit(IfThenElse/*!*/ ifThenElse);
}
[ContractClassFor(typeof(IAppliableVisitor<>))]
@@ -875,6 +920,11 @@ namespace Microsoft.Boogie { throw new NotImplementedException();
}
+ public T Visit(ArithmeticCoercion arithCoercion) {
+ Contract.Requires(arithCoercion != null);
+ throw new NotImplementedException();
+ }
+
public T Visit(IfThenElse ifThenElse) {
Contract.Requires(ifThenElse != null);
throw new NotImplementedException();
@@ -1012,6 +1062,7 @@ namespace Microsoft.Boogie { }
public enum Opcode {
+ Neg,
Not
};
private Opcode op;
@@ -1047,6 +1098,8 @@ namespace Microsoft.Boogie { Contract.Ensures(Contract.Result<string>() != null);
switch (this.op) {
+ case Opcode.Neg:
+ return "-";
case Opcode.Not:
return "!";
}
@@ -1061,7 +1114,7 @@ namespace Microsoft.Boogie { stream.SetToken(ref this.tok);
Contract.Assert(args.Length == 1);
// determine if parens are needed
- int opBindingStrength = 0x60;
+ int opBindingStrength = 0x70;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
@@ -1099,6 +1152,14 @@ namespace Microsoft.Boogie { tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
Type arg0type = cce.NonNull(cce.NonNull(args[0]).Type);
switch (this.op) {
+ case Opcode.Neg:
+ if (arg0type.Unify(Type.Int)) {
+ return Type.Int;
+ }
+ if (arg0type.Unify(Type.Real)) {
+ return Type.Real;
+ }
+ goto BAD_TYPE;
case Opcode.Not:
if (arg0type.Unify(Type.Bool)) {
return Type.Bool;
@@ -1119,6 +1180,8 @@ namespace Microsoft.Boogie { //Contract.Requires(args != null);
Contract.Ensures(Contract.Result<Type>() != null);
switch (this.op) {
+ case Opcode.Neg:
+ return cce.NonNull(cce.NonNull(args[0]).Type);
case Opcode.Not:
return Type.Bool;
default: {
@@ -1133,6 +1196,14 @@ namespace Microsoft.Boogie { return null;
}
switch (this.op) {
+ case Opcode.Neg:
+ if (argument is BigNum) {
+ return -((BigNum)argument);
+ }
+ if (argument is BigDec) {
+ return -((BigDec)argument);
+ }
+ break;
case Opcode.Not:
if (argument is bool) {
return !((bool)argument);
@@ -1161,6 +1232,8 @@ namespace Microsoft.Boogie { Mul,
Div,
Mod,
+ RealDiv,
+ Pow,
Eq,
Neq,
Gt,
@@ -1217,6 +1290,10 @@ namespace Microsoft.Boogie { return "div";
case Opcode.Mod:
return "mod";
+ case Opcode.RealDiv:
+ return "/";
+ case Opcode.Pow:
+ return "**";
case Opcode.Eq:
return "==";
case Opcode.Neq:
@@ -1273,6 +1350,14 @@ namespace Microsoft.Boogie { opBindingStrength = 0x50;
fragileRightContext = true;
break;
+ case Opcode.RealDiv:
+ opBindingStrength = 0x50;
+ fragileRightContext = true;
+ break;
+ case Opcode.Pow:
+ opBindingStrength = 0x60;
+ fragileRightContext = true;
+ break;
case Opcode.Eq:
case Opcode.Neq:
case Opcode.Gt:
@@ -1326,6 +1411,8 @@ namespace Microsoft.Boogie { case Opcode.Mul:
case Opcode.Div:
case Opcode.Mod:
+ case Opcode.RealDiv:
+ case Opcode.Pow:
case Opcode.Neq: // Neq is allowed, but not Eq
case Opcode.Subtype:
// These are fine
@@ -1377,12 +1464,30 @@ namespace Microsoft.Boogie { case Opcode.Add:
case Opcode.Sub:
case Opcode.Mul:
+ if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
+ return Type.Int;
+ }
+ if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
+ return Type.Real;
+ }
+ goto BAD_TYPE;
case Opcode.Div:
case Opcode.Mod:
if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
return Type.Int;
}
goto BAD_TYPE;
+ case Opcode.RealDiv:
+ if ((arg0type.Unify(Type.Int) || arg0type.Unify(Type.Real)) &&
+ (arg1type.Unify(Type.Int) || arg1type.Unify(Type.Real))) {
+ return Type.Real;
+ }
+ goto BAD_TYPE;
+ case Opcode.Pow:
+ if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
+ return Type.Real;
+ }
+ goto BAD_TYPE;
case Opcode.Eq:
case Opcode.Neq:
// Comparison is allowed if the argument types are unifiable
@@ -1406,6 +1511,9 @@ namespace Microsoft.Boogie { if (arg0type.Unify(Type.Int) && arg1type.Unify(Type.Int)) {
return Type.Bool;
}
+ if (arg0type.Unify(Type.Real) && arg1type.Unify(Type.Real)) {
+ return Type.Bool;
+ }
goto BAD_TYPE;
case Opcode.And:
case Opcode.Or:
@@ -1440,10 +1548,16 @@ namespace Microsoft.Boogie { case Opcode.Add:
case Opcode.Sub:
case Opcode.Mul:
+ return cce.NonNull(args[0]).ShallowType;
+
case Opcode.Div:
case Opcode.Mod:
return Type.Int;
+ case Opcode.RealDiv:
+ case Opcode.Pow:
+ return Type.Real;
+
case Opcode.Eq:
case Opcode.Neq:
case Opcode.Gt:
@@ -1500,16 +1614,25 @@ namespace Microsoft.Boogie { if (e1 is BigNum && e2 is BigNum) {
return ((BigNum)e1) + ((BigNum)e2);
}
+ if (e1 is BigDec && e2 is BigDec) {
+ return ((BigDec)e1) + ((BigDec)e2);
+ }
break;
case Opcode.Sub:
if (e1 is BigNum && e2 is BigNum) {
return ((BigNum)e1) - ((BigNum)e2);
}
+ if (e1 is BigDec && e2 is BigDec) {
+ return ((BigDec)e1) - ((BigDec)e2);
+ }
break;
case Opcode.Mul:
if (e1 is BigNum && e2 is BigNum) {
return ((BigNum)e1) * ((BigNum)e2);
}
+ if (e1 is BigDec && e2 is BigDec) {
+ return ((BigDec)e1) * ((BigDec)e2);
+ }
break;
case Opcode.Div:
if (e1 is BigNum && e2 is BigNum) {
@@ -1521,25 +1644,43 @@ namespace Microsoft.Boogie { return /* TODO: right semantics? */ ((BigNum)e1) % ((BigNum)e2);
}
break;
+ case Opcode.RealDiv:
+ // TODO: add partial evaluation fro real division
+ break;
+ case Opcode.Pow:
+ // TODO: add partial evaluation fro real exponentiation
+ break;
case Opcode.Lt:
if (e1 is BigNum && e2 is BigNum) {
return ((BigNum)e1) < ((BigNum)e2);
}
+ if (e1 is BigDec && e2 is BigDec) {
+ return ((BigDec)e1) < ((BigDec)e2);
+ }
break;
case Opcode.Le:
if (e1 is BigNum && e2 is BigNum) {
return ((BigNum)e1) <= ((BigNum)e2);
}
+ if (e1 is BigDec && e2 is BigDec) {
+ return ((BigDec)e1) <= ((BigDec)e2);
+ }
break;
case Opcode.Gt:
if (e1 is BigNum && e2 is BigNum) {
return ((BigNum)e1) > ((BigNum)e2);
}
+ if (e1 is BigDec && e2 is BigDec) {
+ return ((BigDec)e1) > ((BigDec)e2);
+ }
break;
case Opcode.Ge:
if (e1 is BigNum && e2 is BigNum) {
return ((BigNum)e1) >= ((BigNum)e2);
}
+ if (e1 is BigDec && e2 is BigDec) {
+ return ((BigDec)e1) >= ((BigDec)e2);
+ }
break;
case Opcode.And:
@@ -1724,7 +1865,7 @@ namespace Microsoft.Boogie { stream.SetToken(ref this.tok);
Contract.Assert(args.Length == 1);
// determine if parens are needed
- int opBindingStrength = 0x70;
+ int opBindingStrength = 0x80;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
@@ -1782,6 +1923,114 @@ namespace Microsoft.Boogie { }
+ public class ArithmeticCoercion : IAppliable {
+ public enum CoercionType {
+ ToInt,
+ ToReal
+ }
+
+ private IToken/*!*/ tok;
+ public readonly CoercionType Coercion;
+ private readonly string name;
+ private readonly Type type;
+ private readonly Type argType;
+ private readonly int hashCode;
+
+ public ArithmeticCoercion(IToken tok, CoercionType coercion) {
+ this.tok = tok;
+ this.Coercion = coercion;
+
+ switch (coercion) {
+ case CoercionType.ToInt:
+ this.name = "int";
+ this.type = Type.Int;
+ this.argType = Type.Real;
+ this.hashCode = 1;
+ break;
+ case CoercionType.ToReal:
+ this.name = "real";
+ this.type = Type.Real;
+ this.argType = Type.Int;
+ this.hashCode = 2;
+ break;
+ default:
+ Contract.Assert(false);
+ break;
+ }
+ }
+
+ [Pure]
+ public override string ToString() {
+ Contract.Ensures(Contract.Result<string>() != null);
+ return this.name;
+ }
+
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object other) {
+ ArithmeticCoercion ac = other as ArithmeticCoercion;
+ return ac != null && this.Coercion == ac.Coercion;
+ }
+
+ [Pure]
+ public override int GetHashCode() {
+ return this.hashCode;
+ }
+
+ public string/*!*/ FunctionName {
+ get {
+ return this.name;
+ }
+ }
+
+ public int ArgumentCount {
+ get {
+ return 1;
+ }
+ }
+
+ virtual public void Emit(ExprSeq args, TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
+ //Contract.Requires(stream != null);
+ //Contract.Requires(args != null);
+ stream.Write(this.name);
+ stream.Write("(");
+ args.Emit(stream);
+ stream.Write(")");
+ }
+
+ public void Resolve(ResolutionContext rc, Expr subjectForErrorReporting) {
+ //Contract.Requires(subjectForErrorReporting != null);
+ //Contract.Requires(rc != null);
+ }
+
+ public virtual Type Typecheck(ref ExprSeq args, out TypeParamInstantiation tpInstantiation, TypecheckingContext tc) {
+ //Contract.Requires(tc != null);
+ //Contract.Requires(args != null);
+ Contract.Assert(args.Length == 1);
+ Contract.Ensures(args != null);
+ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null);
+
+ tpInstantiation = SimpleTypeParamInstantiation.EMPTY;
+
+ 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;
+ }
+
+ public Type ShallowType(ExprSeq args) {
+ //Contract.Requires(args != null);
+ Contract.Ensures(Contract.Result<Type>() != null);
+ return this.type;
+ }
+
+ public virtual T Dispatch<T>(IAppliableVisitor<T> visitor) {
+ //Contract.Requires(visitor != null);
+ return visitor.Visit(this);
+ }
+ }
+
public class NAryExpr : Expr {
[Additive]
[Peer]
@@ -1949,7 +2198,7 @@ namespace Microsoft.Boogie { bool withRhs) {
Contract.Requires(args != null);
Contract.Requires(stream != null);
- const int opBindingStrength = 0x80;
+ const int opBindingStrength = 0x90;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
@@ -2440,7 +2689,7 @@ namespace Microsoft.Boogie { public override void Emit(TokenTextWriter stream, int contextBindingStrength, bool fragileContext) {
//Contract.Requires(stream != null);
stream.SetToken(this);
- int opBindingStrength = 0x80;
+ int opBindingStrength = 0x90;
bool parensNeeded = opBindingStrength < contextBindingStrength ||
(fragileContext && opBindingStrength == contextBindingStrength);
diff --git a/Source/Core/AbsyType.cs b/Source/Core/AbsyType.cs index 706d6298..d78e0d34 100644 --- a/Source/Core/AbsyType.cs +++ b/Source/Core/AbsyType.cs @@ -239,6 +239,11 @@ namespace Microsoft.Boogie { return false;
}
}
+ public virtual bool IsReal {
+ get {
+ return false;
+ }
+ }
public virtual bool IsBool {
get {
return false;
@@ -330,6 +335,7 @@ namespace Microsoft.Boogie { }
public static readonly Type/*!*/ Int = new BasicType(SimpleType.Int);
+ public static readonly Type/*!*/ Real = new BasicType(SimpleType.Real);
public static readonly Type/*!*/ Bool = new BasicType(SimpleType.Bool);
private static BvType[] bvtypeCache;
@@ -865,6 +871,8 @@ namespace Microsoft.Boogie { switch (T) {
case SimpleType.Int:
return "int";
+ case SimpleType.Real:
+ return "real";
case SimpleType.Bool:
return "bool";
}
@@ -982,6 +990,11 @@ namespace Microsoft.Boogie { return this.T == SimpleType.Int;
}
}
+ public override bool IsReal {
+ get {
+ return this.T == SimpleType.Real;
+ }
+ }
public override bool IsBool {
get {
return this.T == SimpleType.Bool;
@@ -1883,6 +1896,12 @@ Contract.Requires(that != null); return p != null && p.IsInt;
}
}
+ public override bool IsReal {
+ get {
+ Type p = ProxyFor;
+ return p != null && p.IsReal;
+ }
+ }
public override bool IsBool {
get {
Type p = ProxyFor;
@@ -2726,6 +2745,11 @@ Contract.Requires(that != null); return ExpandedType.IsInt;
}
}
+ public override bool IsReal {
+ get {
+ return ExpandedType.IsReal;
+ }
+ }
public override bool IsBool {
get {
return ExpandedType.IsBool;
@@ -3499,6 +3523,7 @@ Contract.Ensures(Contract.ValueAtReturn(out tpInstantiation) != null); public enum SimpleType {
Int,
+ Real,
Bool
};
diff --git a/Source/Core/BoogiePL.atg b/Source/Core/BoogiePL.atg index 26b70bd3..96ba9824 100644 --- a/Source/Core/BoogiePL.atg +++ b/Source/Core/BoogiePL.atg @@ -145,7 +145,8 @@ TOKENS string = quote { regularStringChar | "\\\"" } quote.
- float = digit {digit} '.' {digit}.
+ decimal = digit {digit} 'e' [ '-' ] digit {digit} .
+ float = digit {digit} '.' digit {digit} [ 'e' [ '-' ] digit {digit} ] .
COMMENTS FROM "/*" TO "*/" NESTED
COMMENTS FROM "//" TO lf
@@ -313,6 +314,7 @@ TypeArgs<TypeSeq/*!*/ ts> TypeAtom<out Bpl.Type/*!*/ ty>
= (.Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType; .)
( "int" (. ty = new BasicType(t, SimpleType.Int); .)
+ | "real" (. ty = new BasicType(t, SimpleType.Real); .)
| "bool" (. ty = new BasicType(t, SimpleType.Bool); .)
/* note: bitvectors are handled in UnresolvedTypeIdentifier */
|
@@ -1162,9 +1164,9 @@ AddOp<out IToken/*!*/ x, out BinaryOperator.Opcode op> /*------------------------------------------------------------------------*/
Factor<out Expr/*!*/ e0>
= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op; .)
- UnaryExpression<out e0>
+ Power<out e0>
{ MulOp<out x, out op>
- UnaryExpression<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
+ Power<out e1> (. e0 = Expr.Binary(x, op, e0, e1); .)
}
.
@@ -1173,16 +1175,28 @@ MulOp<out IToken/*!*/ x, out BinaryOperator.Opcode op> ( "*" (. x = t; op=BinaryOperator.Opcode.Mul; .)
| "div" (. x = t; op=BinaryOperator.Opcode.Div; .)
| "mod" (. x = t; op=BinaryOperator.Opcode.Mod; .)
+ | "/" (. x = t; op=BinaryOperator.Opcode.RealDiv; .)
)
.
/*------------------------------------------------------------------------*/
+Power<out Expr/*!*/ e0>
+= (.Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; .)
+ UnaryExpression<out e0>
+ [
+ "**" (. x = t; .)
+ /* recurse because exponentation is right-associative */
+ Power<out e1> (. e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1); .)
+ ]
+ .
+
+/*------------------------------------------------------------------------*/
UnaryExpression<out Expr/*!*/ e>
= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
e = dummyExpr;
.)
( "-" (. x = t; .)
- UnaryExpression<out e> (. e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e); .)
+ UnaryExpression<out e> (. e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e); .)
| NegOp (. x = t; .)
UnaryExpression<out e> (. e = Expr.Unary(x, UnaryOperator.Opcode.Not, e); .)
| CoercionExpression<out e>
@@ -1271,7 +1285,7 @@ ArrayExpression<out Expr/*!*/ e> /*------------------------------------------------------------------------*/
AtomExpression<out Expr/*!*/ e>
-= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn;
+= (. Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
ExprSeq/*!*/ es; VariableSeq/*!*/ ds; Trigger trig;
TypeVariableSeq/*!*/ typeParams;
IdentifierExpr/*!*/ id;
@@ -1283,6 +1297,7 @@ AtomExpression<out Expr/*!*/ e> ( "false" (. e = new LiteralExpr(t, false); .)
| "true" (. e = new LiteralExpr(t, true); .)
| Nat<out bn> (. e = new LiteralExpr(t, bn); .)
+ | Dec<out bd> (. e = new LiteralExpr(t, bd); .)
| BvLit<out bn, out n> (. e = new LiteralExpr(t, bn, n); .)
| Ident<out x> (. id = new IdentifierExpr(x, x.val); e = id; .)
@@ -1298,6 +1313,16 @@ AtomExpression<out Expr/*!*/ e> Expression<out e>
")" (. e = new OldExpr(x, e); .)
+ | "int" (. x = t; .)
+ "("
+ Expression<out e>
+ ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e)); .)
+
+ | "real" (. x = t; .)
+ "("
+ Expression<out e>
+ ")" (. e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e)); .)
+
| "(" ( Expression<out e> (. if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
"are not allowed"); .)
@@ -1482,6 +1507,23 @@ Nat<out BigNum n> .
/*------------------------------------------------------------------------*/
+Dec<out BigDec n>
+= (. string s = ""; .)
+ (
+ decimal (. s = t.val; .)
+ |
+ float (. s = t.val; .)
+ )
+ (. try {
+ n = BigDec.FromString(s);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted number");
+ n = BigDec.ZERO;
+ }
+ .)
+ .
+
+/*------------------------------------------------------------------------*/
BvLit<out BigNum n, out int m>
=
bvlit
diff --git a/Source/Core/Parser.cs b/Source/Core/Parser.cs index 8638d9c3..0a10b0a1 100644 --- a/Source/Core/Parser.cs +++ b/Source/Core/Parser.cs @@ -23,8 +23,9 @@ public class Parser { public const int _bvlit = 2;
public const int _digits = 3;
public const int _string = 4;
- public const int _float = 5;
- public const int maxT = 88;
+ public const int _decimal = 5;
+ public const int _float = 6;
+ public const int maxT = 92;
const bool T = true;
const bool x = false;
@@ -217,7 +218,7 @@ private class BvBounds : Expr { while (StartOf(1)) {
switch (la.kind) {
- case 19: {
+ case 21: {
Consts(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
@@ -226,7 +227,7 @@ private class BvBounds : Expr { break;
}
- case 23: {
+ case 25: {
Function(out ds);
foreach(Bpl.Declaration/*!*/ d in ds){
Contract.Assert(d != null);
@@ -235,12 +236,12 @@ private class BvBounds : Expr { break;
}
- case 27: {
+ case 29: {
Axiom(out ax);
Pgm.TopLevelDeclarations.Add(ax);
break;
}
- case 28: {
+ case 30: {
UserDefinedTypes(out ts);
foreach(Declaration/*!*/ td in ts){
Contract.Assert(td != null);
@@ -249,7 +250,7 @@ private class BvBounds : Expr { break;
}
- case 6: {
+ case 7: {
GlobalVars(out vs);
foreach(Bpl.Variable/*!*/ v in vs){
Contract.Assert(v != null);
@@ -258,7 +259,7 @@ private class BvBounds : Expr { break;
}
- case 30: {
+ case 32: {
Procedure(out pr, out im);
Pgm.TopLevelDeclarations.Add(pr);
if (im != null) {
@@ -267,7 +268,7 @@ private class BvBounds : Expr { break;
}
- case 31: {
+ case 33: {
Implementation(out nnim);
Pgm.TopLevelDeclarations.Add(nnim);
break;
@@ -283,17 +284,17 @@ private class BvBounds : Expr { bool u = false; QKeyValue kv = null;
bool ChildrenComplete = false;
List<ConstantParent/*!*/> Parents = null;
- Expect(19);
+ Expect(21);
y = t;
- while (la.kind == 25) {
+ while (la.kind == 27) {
Attribute(ref kv);
}
- if (la.kind == 20) {
+ if (la.kind == 22) {
Get();
u = true;
}
IdsType(out xs);
- if (la.kind == 21) {
+ if (la.kind == 23) {
OrderSpec(out ChildrenComplete, out Parents);
}
bool makeClone = false;
@@ -317,7 +318,7 @@ private class BvBounds : Expr { ds.Add(new Constant(y, x, u, ParentsClone, ChildrenComplete, kv));
}
- Expect(7);
+ Expect(8);
}
void Function(out DeclarationSeq/*!*/ ds) {
@@ -333,44 +334,44 @@ private class BvBounds : Expr { Expr definition = null;
Expr/*!*/ tmp;
- Expect(23);
- while (la.kind == 25) {
+ Expect(25);
+ while (la.kind == 27) {
Attribute(ref kv);
}
Ident(out z);
- if (la.kind == 17) {
+ if (la.kind == 19) {
TypeParams(out typeParamTok, out typeParams);
}
- Expect(8);
+ Expect(9);
if (StartOf(2)) {
VarOrType(out tyd);
arguments.Add(new Formal(tyd.tok, tyd, true));
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
VarOrType(out tyd);
arguments.Add(new Formal(tyd.tok, tyd, true));
}
}
- Expect(9);
- if (la.kind == 24) {
+ Expect(10);
+ if (la.kind == 26) {
Get();
- Expect(8);
- VarOrType(out tyd);
Expect(9);
+ VarOrType(out tyd);
+ Expect(10);
retTyd = tyd;
- } else if (la.kind == 10) {
+ } else if (la.kind == 11) {
Get();
Type(out retTy);
retTyd = new TypedIdent(retTy.tok, "", retTy);
- } else SynErr(89);
- if (la.kind == 25) {
+ } else SynErr(93);
+ if (la.kind == 27) {
Get();
Expression(out tmp);
definition = tmp;
- Expect(26);
- } else if (la.kind == 7) {
+ Expect(28);
+ } else if (la.kind == 8) {
Get();
- } else SynErr(90);
+ } else SynErr(94);
if (retTyd == null) {
// construct a dummy type for the case of syntax error
tyd = new TypedIdent(t, "", new BasicType(t, SimpleType.Int));
@@ -451,40 +452,40 @@ private class BvBounds : Expr { void Axiom(out Axiom/*!*/ m) {
Contract.Ensures(Contract.ValueAtReturn(out m) != null); Expr/*!*/ e; QKeyValue kv = null;
- Expect(27);
- while (la.kind == 25) {
+ Expect(29);
+ while (la.kind == 27) {
Attribute(ref kv);
}
IToken/*!*/ x = t;
Proposition(out e);
- Expect(7);
+ Expect(8);
m = new Axiom(x,e, null, kv);
}
void UserDefinedTypes(out List<Declaration/*!*/>/*!*/ ts) {
Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out ts))); Declaration/*!*/ decl; QKeyValue kv = null; ts = new List<Declaration/*!*/> ();
- Expect(28);
- while (la.kind == 25) {
+ Expect(30);
+ while (la.kind == 27) {
Attribute(ref kv);
}
UserDefinedType(out decl, kv);
ts.Add(decl);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
UserDefinedType(out decl, kv);
ts.Add(decl);
}
- Expect(7);
+ Expect(8);
}
void GlobalVars(out VariableSeq/*!*/ ds) {
Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq(); QKeyValue kv = null;
- Expect(6);
- while (la.kind == 25) {
+ Expect(7);
+ while (la.kind == 27) {
Attribute(ref kv);
}
IdsTypeWheres(true, tyds);
- Expect(7);
+ Expect(8);
foreach(TypedIdent/*!*/ tyd in tyds){
Contract.Assert(tyd != null);
ds.Add(new GlobalVariable(tyd.tok, tyd, kv));
@@ -505,9 +506,9 @@ private class BvBounds : Expr { QKeyValue kv = null;
impl = null;
- Expect(30);
+ Expect(32);
ProcSignature(true, out x, out typeParams, out ins, out outs, out kv);
- if (la.kind == 7) {
+ if (la.kind == 8) {
Get();
while (StartOf(3)) {
Spec(pre, mods, post);
@@ -520,7 +521,7 @@ private class BvBounds : Expr { impl = new Implementation(x, x.val, typeParams,
Formal.StripWhereClauses(ins), Formal.StripWhereClauses(outs), locals, stmtList, kv == null ? null : (QKeyValue)kv.Clone(), this.errors);
- } else SynErr(91);
+ } else SynErr(95);
proc = new Procedure(x, x.val, typeParams, ins, outs, pre, mods, post, kv);
}
@@ -532,7 +533,7 @@ private class BvBounds : Expr { StmtList/*!*/ stmtList;
QKeyValue kv;
- Expect(31);
+ Expect(33);
ProcSignature(false, out x, out typeParams, out ins, out outs, out kv);
ImplBody(out locals, out stmtList);
impl = new Implementation(x, x.val, typeParams, ins, outs, locals, stmtList, kv, this.errors);
@@ -547,7 +548,7 @@ private class BvBounds : Expr { void IdsTypeWheres(bool allowWhereClauses, TypedIdentSeq/*!*/ tyds) {
Contract.Requires(tyds != null);
IdsTypeWhere(allowWhereClauses, tyds);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
IdsTypeWhere(allowWhereClauses, tyds);
}
@@ -555,12 +556,12 @@ private class BvBounds : Expr { void LocalVars(VariableSeq/*!*/ ds) {
Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); QKeyValue kv = null;
- Expect(6);
- while (la.kind == 25) {
+ Expect(7);
+ while (la.kind == 27) {
Attribute(ref kv);
}
IdsTypeWheres(true, tyds);
- Expect(7);
+ Expect(8);
foreach(TypedIdent/*!*/ tyd in tyds){
Contract.Assert(tyd != null);
ds.Add(new LocalVariable(tyd.tok, tyd, kv));
@@ -570,11 +571,11 @@ private class BvBounds : Expr { void ProcFormals(bool incoming, bool allowWhereClauses, out VariableSeq/*!*/ ds) {
Contract.Ensures(Contract.ValueAtReturn(out ds) != null); TypedIdentSeq/*!*/ tyds = new TypedIdentSeq(); ds = new VariableSeq();
- Expect(8);
+ Expect(9);
if (la.kind == 1) {
IdsTypeWheres(allowWhereClauses, tyds);
}
- Expect(9);
+ Expect(10);
foreach(TypedIdent/*!*/ tyd in tyds){
Contract.Assert(tyd != null);
ds.Add(new Formal(tyd.tok, tyd, incoming));
@@ -595,7 +596,7 @@ private class BvBounds : Expr { void IdsType(out TypedIdentSeq/*!*/ tyds) {
Contract.Ensures(Contract.ValueAtReturn(out tyds) != null); TokenSeq/*!*/ ids; Bpl.Type/*!*/ ty;
Idents(out ids);
- Expect(10);
+ Expect(11);
Type(out ty);
tyds = new TypedIdentSeq();
foreach(Token/*!*/ id in ids){
@@ -609,7 +610,7 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out xs) != null); IToken/*!*/ id; xs = new TokenSeq();
Ident(out id);
xs.Add(id);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Ident(out id);
xs.Add(id);
@@ -618,7 +619,7 @@ private class BvBounds : Expr { void Type(out Bpl.Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out ty) != null); IToken/*!*/ tok; ty = dummyType;
- if (la.kind == 8 || la.kind == 13 || la.kind == 14) {
+ if (StartOf(5)) {
TypeAtom(out ty);
} else if (la.kind == 1) {
Ident(out tok);
@@ -627,17 +628,17 @@ private class BvBounds : Expr { TypeArgs(args);
}
ty = new UnresolvedTypeIdentifier (tok, tok.val, args);
- } else if (la.kind == 15 || la.kind == 17) {
+ } else if (la.kind == 17 || la.kind == 19) {
MapType(out ty);
- } else SynErr(92);
+ } else SynErr(96);
}
void IdsTypeWhere(bool allowWhereClauses, TypedIdentSeq/*!*/ tyds) {
Contract.Requires(tyds != null); TokenSeq/*!*/ ids; Bpl.Type/*!*/ ty; Expr wh = null; Expr/*!*/ nne;
Idents(out ids);
- Expect(10);
+ Expect(11);
Type(out ty);
- if (la.kind == 12) {
+ if (la.kind == 13) {
Get();
Expression(out nne);
if (allowWhereClauses) {
@@ -657,7 +658,7 @@ private class BvBounds : Expr { void Expression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
ImpliesExpression(false, out e0);
- while (la.kind == 50 || la.kind == 51) {
+ while (la.kind == 52 || la.kind == 53) {
EquivOp();
x = t;
ImpliesExpression(false, out e1);
@@ -667,17 +668,20 @@ private class BvBounds : Expr { void TypeAtom(out Bpl.Type/*!*/ ty) {
Contract.Ensures(Contract.ValueAtReturn(out ty) != null); ty = dummyType;
- if (la.kind == 13) {
+ if (la.kind == 14) {
Get();
ty = new BasicType(t, SimpleType.Int);
- } else if (la.kind == 14) {
+ } else if (la.kind == 15) {
+ Get();
+ ty = new BasicType(t, SimpleType.Real);
+ } else if (la.kind == 16) {
Get();
ty = new BasicType(t, SimpleType.Bool);
- } else if (la.kind == 8) {
+ } else if (la.kind == 9) {
Get();
Type(out ty);
- Expect(9);
- } else SynErr(93);
+ Expect(10);
+ } else SynErr(97);
}
void Ident(out IToken/*!*/ x) {
@@ -691,7 +695,7 @@ private class BvBounds : Expr { void TypeArgs(TypeSeq/*!*/ ts) {
Contract.Requires(ts != null); IToken/*!*/ tok; Type/*!*/ ty;
- if (la.kind == 8 || la.kind == 13 || la.kind == 14) {
+ if (StartOf(5)) {
TypeAtom(out ty);
ts.Add(ty);
if (StartOf(2)) {
@@ -704,10 +708,10 @@ private class BvBounds : Expr { if (StartOf(2)) {
TypeArgs(ts);
}
- } else if (la.kind == 15 || la.kind == 17) {
+ } else if (la.kind == 17 || la.kind == 19) {
MapType(out ty);
ts.Add(ty);
- } else SynErr(94);
+ } else SynErr(98);
}
void MapType(out Bpl.Type/*!*/ ty) {
@@ -717,16 +721,16 @@ private class BvBounds : Expr { Type/*!*/ result;
TypeVariableSeq/*!*/ typeParameters = new TypeVariableSeq();
- if (la.kind == 17) {
+ if (la.kind == 19) {
TypeParams(out nnTok, out typeParameters);
tok = nnTok;
}
- Expect(15);
+ Expect(17);
if (tok == null) tok = t;
if (StartOf(2)) {
Types(arguments);
}
- Expect(16);
+ Expect(18);
Type(out result);
ty = new MapType(tok, typeParameters, arguments, result);
@@ -734,10 +738,10 @@ private class BvBounds : Expr { void TypeParams(out IToken/*!*/ tok, out Bpl.TypeVariableSeq/*!*/ typeParams) {
Contract.Ensures(Contract.ValueAtReturn(out tok) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); TokenSeq/*!*/ typeParamToks;
- Expect(17);
+ Expect(19);
tok = t;
Idents(out typeParamToks);
- Expect(18);
+ Expect(20);
typeParams = new TypeVariableSeq ();
foreach(Token/*!*/ id in typeParamToks){
Contract.Assert(id != null);
@@ -749,7 +753,7 @@ private class BvBounds : Expr { Contract.Requires(ts != null); Bpl.Type/*!*/ ty;
Type(out ty);
ts.Add(ty);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Type(out ty);
ts.Add(ty);
@@ -761,21 +765,21 @@ private class BvBounds : Expr { Parents = null;
bool u;
IToken/*!*/ parent;
- Expect(21);
+ Expect(23);
Parents = new List<ConstantParent/*!*/> ();
u = false;
- if (la.kind == 1 || la.kind == 20) {
- if (la.kind == 20) {
+ if (la.kind == 1 || la.kind == 22) {
+ if (la.kind == 22) {
Get();
u = true;
}
Ident(out parent);
Parents.Add(new ConstantParent (
new IdentifierExpr(parent, parent.val), u));
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
u = false;
- if (la.kind == 20) {
+ if (la.kind == 22) {
Get();
u = true;
}
@@ -784,7 +788,7 @@ private class BvBounds : Expr { new IdentifierExpr(parent, parent.val), u));
}
}
- if (la.kind == 22) {
+ if (la.kind == 24) {
Get();
ChildrenComplete = true;
}
@@ -794,7 +798,7 @@ private class BvBounds : Expr { Contract.Ensures(Contract.ValueAtReturn(out tyd) != null); string/*!*/ varName = ""; Bpl.Type/*!*/ ty; IToken/*!*/ tok;
Type(out ty);
tok = ty.tok;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
if (ty is UnresolvedTypeIdentifier &&
cce.NonNull(ty as UnresolvedTypeIdentifier).Arguments.Length == 0) {
@@ -820,7 +824,7 @@ private class BvBounds : Expr { if (la.kind == 1) {
WhiteSpaceIdents(out paramTokens);
}
- if (la.kind == 29) {
+ if (la.kind == 31) {
Get();
Type(out body);
synonym = true;
@@ -852,15 +856,15 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out name) != null); Contract.Ensures(Contract.ValueAtReturn(out typeParams) != null); Contract.Ensures(Contract.ValueAtReturn(out ins) != null); Contract.Ensures(Contract.ValueAtReturn(out outs) != null);
IToken/*!*/ typeParamTok; typeParams = new TypeVariableSeq();
outs = new VariableSeq(); kv = null;
- while (la.kind == 25) {
+ while (la.kind == 27) {
Attribute(ref kv);
}
Ident(out name);
- if (la.kind == 17) {
+ if (la.kind == 19) {
TypeParams(out typeParamTok, out typeParams);
}
ProcFormals(true, allowWhereClausesOnFormals, out ins);
- if (la.kind == 24) {
+ if (la.kind == 26) {
Get();
ProcFormals(false, allowWhereClausesOnFormals, out outs);
}
@@ -868,7 +872,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void Spec(RequiresSeq/*!*/ pre, IdentifierExprSeq/*!*/ mods, EnsuresSeq/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(mods != null); Contract.Requires(post != null); TokenSeq/*!*/ ms;
- if (la.kind == 32) {
+ if (la.kind == 34) {
Get();
if (la.kind == 1) {
Idents(out ms);
@@ -878,19 +882,19 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
}
- Expect(7);
- } else if (la.kind == 33) {
+ Expect(8);
+ } else if (la.kind == 35) {
Get();
SpecPrePost(true, pre, post);
- } else if (la.kind == 34 || la.kind == 35) {
+ } else if (la.kind == 36 || la.kind == 37) {
SpecPrePost(false, pre, post);
- } else SynErr(95);
+ } else SynErr(99);
}
void ImplBody(out VariableSeq/*!*/ locals, out StmtList/*!*/ stmtList) {
Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(Contract.ValueAtReturn(out stmtList) != null); locals = new VariableSeq();
- Expect(25);
- while (la.kind == 6) {
+ Expect(27);
+ while (la.kind == 7) {
LocalVars(locals);
}
StmtList(out stmtList);
@@ -898,25 +902,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void SpecPrePost(bool free, RequiresSeq/*!*/ pre, EnsuresSeq/*!*/ post) {
Contract.Requires(pre != null); Contract.Requires(post != null); Expr/*!*/ e; Token tok = null; QKeyValue kv = null;
- if (la.kind == 34) {
+ if (la.kind == 36) {
Get();
tok = t;
- while (la.kind == 25) {
+ while (la.kind == 27) {
Attribute(ref kv);
}
Proposition(out e);
- Expect(7);
+ Expect(8);
pre.Add(new Requires(tok, free, e, null, kv));
- } else if (la.kind == 35) {
+ } else if (la.kind == 37) {
Get();
tok = t;
- while (la.kind == 25) {
+ while (la.kind == 27) {
Attribute(ref kv);
}
Proposition(out e);
- Expect(7);
+ Expect(8);
post.Add(new Ensures(tok, free, e, null, kv));
- } else SynErr(96);
+ } else SynErr(100);
}
void StmtList(out StmtList/*!*/ stmtList) {
@@ -929,8 +933,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { StructuredCmd ec = null; StructuredCmd/*!*/ ecn;
TransferCmd tc = null; TransferCmd/*!*/ tcn;
- while (StartOf(5)) {
- if (StartOf(6)) {
+ while (StartOf(6)) {
+ if (StartOf(7)) {
LabelOrCmd(out c, out label);
if (c != null) {
// LabelOrCmd read a Cmd
@@ -953,7 +957,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { cs = new CmdSeq();
}
- } else if (la.kind == 38 || la.kind == 40 || la.kind == 43) {
+ } else if (la.kind == 40 || la.kind == 42 || la.kind == 45) {
StructuredCmd(out ecn);
ec = ecn;
if (startToken == null) { startToken = ec.tok; cs = new CmdSeq(); }
@@ -973,7 +977,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
}
- Expect(26);
+ Expect(28);
IToken/*!*/ endCurly = t;
if (startToken == null && bigblocks.Count == 0) {
startToken = t; cs = new CmdSeq();
@@ -998,29 +1002,29 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { if (la.kind == 1) {
LabelOrAssign(out c, out label);
- } else if (la.kind == 44) {
+ } else if (la.kind == 46) {
Get();
x = t;
- while (la.kind == 25) {
+ while (la.kind == 27) {
Attribute(ref kv);
}
Proposition(out e);
c = new AssertCmd(x, e, kv);
- Expect(7);
- } else if (la.kind == 45) {
+ Expect(8);
+ } else if (la.kind == 47) {
Get();
x = t;
- while (la.kind == 25) {
+ while (la.kind == 27) {
Attribute(ref kv);
}
Proposition(out e);
c = new AssumeCmd(x, e, kv);
- Expect(7);
- } else if (la.kind == 46) {
+ Expect(8);
+ } else if (la.kind == 48) {
Get();
x = t;
Idents(out xs);
- Expect(7);
+ Expect(8);
ids = new IdentifierExprSeq();
foreach(IToken/*!*/ y in xs){
Contract.Assert(y != null);
@@ -1028,27 +1032,27 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
c = new HavocCmd(x,ids);
- } else if (la.kind == 33 || la.kind == 48) {
+ } else if (la.kind == 35 || la.kind == 50) {
CallCmd(out cn);
- Expect(7);
+ Expect(8);
c = cn;
- } else SynErr(97);
+ } else SynErr(101);
}
void StructuredCmd(out StructuredCmd/*!*/ ec) {
Contract.Ensures(Contract.ValueAtReturn(out ec) != null); ec = dummyStructuredCmd; Contract.Assume(cce.IsPeerConsistent(ec));
IfCmd/*!*/ ifcmd; WhileCmd/*!*/ wcmd; BreakCmd/*!*/ bcmd;
- if (la.kind == 38) {
+ if (la.kind == 40) {
IfCmd(out ifcmd);
ec = ifcmd;
- } else if (la.kind == 40) {
+ } else if (la.kind == 42) {
WhileCmd(out wcmd);
ec = wcmd;
- } else if (la.kind == 43) {
+ } else if (la.kind == 45) {
BreakCmd(out bcmd);
ec = bcmd;
- } else SynErr(98);
+ } else SynErr(102);
}
void TransferCmd(out TransferCmd/*!*/ tc) {
@@ -1056,7 +1060,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Token y; TokenSeq/*!*/ xs;
StringSeq ss = new StringSeq();
- if (la.kind == 36) {
+ if (la.kind == 38) {
Get();
y = t;
Idents(out xs);
@@ -1065,11 +1069,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ss.Add(s.val); }
tc = new GotoCmd(y, ss);
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
tc = new ReturnCmd(t);
- } else SynErr(99);
- Expect(7);
+ } else SynErr(103);
+ Expect(8);
}
void IfCmd(out IfCmd/*!*/ ifcmd) {
@@ -1079,21 +1083,21 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { IfCmd/*!*/ elseIf; IfCmd elseIfOption = null;
StmtList/*!*/ els; StmtList elseOption = null;
- Expect(38);
+ Expect(40);
x = t;
Guard(out guard);
- Expect(25);
+ Expect(27);
StmtList(out thn);
- if (la.kind == 39) {
+ if (la.kind == 41) {
Get();
- if (la.kind == 38) {
+ if (la.kind == 40) {
IfCmd(out elseIf);
elseIfOption = elseIf;
- } else if (la.kind == 25) {
+ } else if (la.kind == 27) {
Get();
StmtList(out els);
elseOption = els;
- } else SynErr(100);
+ } else SynErr(104);
}
ifcmd = new IfCmd(x, guard, thn, elseIfOption, elseOption);
}
@@ -1105,18 +1109,18 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { StmtList/*!*/ body;
QKeyValue kv = null;
- Expect(40);
+ Expect(42);
x = t;
Guard(out guard);
Contract.Assume(guard == null || cce.Owner.None(guard));
- while (la.kind == 33 || la.kind == 41) {
+ while (la.kind == 35 || la.kind == 43) {
isFree = false; z = la/*lookahead token*/;
- if (la.kind == 33) {
+ if (la.kind == 35) {
Get();
isFree = true;
}
- Expect(41);
- while (la.kind == 25) {
+ Expect(43);
+ while (la.kind == 27) {
Attribute(ref kv);
}
Expression(out e);
@@ -1126,9 +1130,9 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { invariants.Add(new AssertCmd(z, e, kv));
}
- Expect(7);
+ Expect(8);
}
- Expect(25);
+ Expect(27);
StmtList(out body);
wcmd = new WhileCmd(x, guard, invariants, body);
}
@@ -1137,27 +1141,27 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Contract.Ensures(Contract.ValueAtReturn(out bcmd) != null); IToken/*!*/ x; IToken/*!*/ y;
string breakLabel = null;
- Expect(43);
+ Expect(45);
x = t;
if (la.kind == 1) {
Ident(out y);
breakLabel = y.val;
}
- Expect(7);
+ Expect(8);
bcmd = new BreakCmd(x, breakLabel);
}
void Guard(out Expr e) {
Expr/*!*/ ee; e = null;
- Expect(8);
- if (la.kind == 42) {
+ Expect(9);
+ if (la.kind == 44) {
Get();
e = null;
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out ee);
e = ee;
- } else SynErr(101);
- Expect(9);
+ } else SynErr(105);
+ Expect(10);
}
void LabelOrAssign(out Cmd c, out IToken label) {
@@ -1170,40 +1174,40 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { Ident(out id);
x = t;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
c = null; label = x;
- } else if (la.kind == 11 || la.kind == 15 || la.kind == 47) {
+ } else if (la.kind == 12 || la.kind == 17 || la.kind == 49) {
lhss = new List<AssignLhs/*!*/>();
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 15) {
+ while (la.kind == 17) {
MapAssignIndex(out y, out indexes);
lhs = new MapAssignLhs(y, lhs, indexes);
}
lhss.Add(lhs);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Ident(out id);
lhs = new SimpleAssignLhs(id, new IdentifierExpr(id, id.val));
- while (la.kind == 15) {
+ while (la.kind == 17) {
MapAssignIndex(out y, out indexes);
lhs = new MapAssignLhs(y, lhs, indexes);
}
lhss.Add(lhs);
}
- Expect(47);
+ Expect(49);
x = t; /* use location of := */
Expression(out e0);
rhss = new List<Expr/*!*/> ();
rhss.Add(e0);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Expression(out e0);
rhss.Add(e0);
}
- Expect(7);
+ Expect(8);
c = new AssignCmd(x, lhss, rhss);
- } else SynErr(102);
+ } else SynErr(106);
}
void CallCmd(out Cmd/*!*/ c) {
@@ -1215,33 +1219,33 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { c = dummyCmd;
bool isFree = false;
- if (la.kind == 33) {
+ if (la.kind == 35) {
Get();
isFree = true;
}
- Expect(48);
+ Expect(50);
x = t;
- while (la.kind == 25) {
+ while (la.kind == 27) {
Attribute(ref kv);
}
if (la.kind == 1) {
Ident(out first);
- if (la.kind == 8) {
+ if (la.kind == 9) {
Get();
- if (StartOf(8)) {
+ if (StartOf(9)) {
CallForallArg(out en);
es.Add(en);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
CallForallArg(out en);
es.Add(en);
}
}
- Expect(9);
+ Expect(10);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
- } else if (la.kind == 11 || la.kind == 47) {
+ } else if (la.kind == 12 || la.kind == 49) {
ids.Add(new IdentifierExpr(first, first.val));
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
CallOutIdent(out p);
if (p==null) {
@@ -1250,7 +1254,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ids.Add(new IdentifierExpr(p, p.val));
}
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
CallOutIdent(out p);
if (p==null) {
@@ -1261,41 +1265,41 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
}
- Expect(47);
+ Expect(49);
Ident(out first);
- Expect(8);
- if (StartOf(8)) {
+ Expect(9);
+ if (StartOf(9)) {
CallForallArg(out en);
es.Add(en);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
CallForallArg(out en);
es.Add(en);
}
}
- Expect(9);
+ Expect(10);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
- } else SynErr(103);
- } else if (la.kind == 49) {
+ } else SynErr(107);
+ } else if (la.kind == 51) {
Get();
Ident(out first);
- Expect(8);
+ Expect(9);
args = new List<Expr>();
- if (StartOf(8)) {
+ if (StartOf(9)) {
CallForallArg(out en);
args.Add(en);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
CallForallArg(out en);
args.Add(en);
}
}
- Expect(9);
+ Expect(10);
c = new CallForallCmd(x, first.val, args, kv); ((CallForallCmd) c).IsFree = isFree;
- } else if (la.kind == 42) {
+ } else if (la.kind == 44) {
Get();
ids.Add(null);
- if (la.kind == 11) {
+ if (la.kind == 12) {
Get();
CallOutIdent(out p);
if (p==null) {
@@ -1304,7 +1308,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ids.Add(new IdentifierExpr(p, p.val));
}
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
CallOutIdent(out p);
if (p==null) {
@@ -1315,70 +1319,70 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
}
- Expect(47);
+ Expect(49);
Ident(out first);
- Expect(8);
- if (StartOf(8)) {
+ Expect(9);
+ if (StartOf(9)) {
CallForallArg(out en);
es.Add(en);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
CallForallArg(out en);
es.Add(en);
}
}
- Expect(9);
+ Expect(10);
c = new CallCmd(x, first.val, es, ids, kv); ((CallCmd) c).IsFree = isFree;
- } else SynErr(104);
+ } else SynErr(108);
}
void MapAssignIndex(out IToken/*!*/ x, out List<Expr/*!*/>/*!*/ indexes) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out indexes))); indexes = new List<Expr/*!*/> ();
Expr/*!*/ e;
- Expect(15);
+ Expect(17);
x = t;
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expression(out e);
indexes.Add(e);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Expression(out e);
indexes.Add(e);
}
}
- Expect(16);
+ Expect(18);
}
void CallForallArg(out Expr exprOptional) {
exprOptional = null;
Expr/*!*/ e;
- if (la.kind == 42) {
+ if (la.kind == 44) {
Get();
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
exprOptional = e;
- } else SynErr(105);
+ } else SynErr(109);
}
void CallOutIdent(out IToken id) {
id = null;
IToken/*!*/ p;
- if (la.kind == 42) {
+ if (la.kind == 44) {
Get();
} else if (la.kind == 1) {
Ident(out p);
id = p;
- } else SynErr(106);
+ } else SynErr(110);
}
void Expressions(out ExprSeq/*!*/ es) {
Contract.Ensures(Contract.ValueAtReturn(out es) != null); Expr/*!*/ e; es = new ExprSeq();
Expression(out e);
es.Add(e);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Expression(out e);
es.Add(e);
@@ -1388,8 +1392,8 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void ImpliesExpression(bool noExplies, out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
LogicalExpression(out e0);
- if (StartOf(9)) {
- if (la.kind == 52 || la.kind == 53) {
+ if (StartOf(10)) {
+ if (la.kind == 54 || la.kind == 55) {
ImpliesOp();
x = t;
ImpliesExpression(true, out e1);
@@ -1401,7 +1405,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { x = t;
LogicalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Imp, e1, e0);
- while (la.kind == 54 || la.kind == 55) {
+ while (la.kind == 56 || la.kind == 57) {
ExpliesOp();
x = t;
LogicalExpression(out e1);
@@ -1412,23 +1416,23 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
void EquivOp() {
- if (la.kind == 50) {
+ if (la.kind == 52) {
Get();
- } else if (la.kind == 51) {
+ } else if (la.kind == 53) {
Get();
- } else SynErr(107);
+ } else SynErr(111);
}
void LogicalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
RelationalExpression(out e0);
- if (StartOf(10)) {
- if (la.kind == 56 || la.kind == 57) {
+ if (StartOf(11)) {
+ if (la.kind == 58 || la.kind == 59) {
AndOp();
x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.And, e0, e1);
- while (la.kind == 56 || la.kind == 57) {
+ while (la.kind == 58 || la.kind == 59) {
AndOp();
x = t;
RelationalExpression(out e1);
@@ -1439,7 +1443,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { x = t;
RelationalExpression(out e1);
e0 = Expr.Binary(x, BinaryOperator.Opcode.Or, e0, e1);
- while (la.kind == 58 || la.kind == 59) {
+ while (la.kind == 60 || la.kind == 61) {
OrOp();
x = t;
RelationalExpression(out e1);
@@ -1450,25 +1454,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
void ImpliesOp() {
- if (la.kind == 52) {
+ if (la.kind == 54) {
Get();
- } else if (la.kind == 53) {
+ } else if (la.kind == 55) {
Get();
- } else SynErr(108);
+ } else SynErr(112);
}
void ExpliesOp() {
- if (la.kind == 54) {
+ if (la.kind == 56) {
Get();
- } else if (la.kind == 55) {
+ } else if (la.kind == 57) {
Get();
- } else SynErr(109);
+ } else SynErr(113);
}
void RelationalExpression(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
BvTerm(out e0);
- if (StartOf(11)) {
+ if (StartOf(12)) {
RelOp(out x, out op);
BvTerm(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1476,25 +1480,25 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
void AndOp() {
- if (la.kind == 56) {
+ if (la.kind == 58) {
Get();
- } else if (la.kind == 57) {
+ } else if (la.kind == 59) {
Get();
- } else SynErr(110);
+ } else SynErr(114);
}
void OrOp() {
- if (la.kind == 58) {
+ if (la.kind == 60) {
Get();
- } else if (la.kind == 59) {
+ } else if (la.kind == 61) {
Get();
- } else SynErr(111);
+ } else SynErr(115);
}
void BvTerm(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
Term(out e0);
- while (la.kind == 68) {
+ while (la.kind == 70) {
Get();
x = t;
Term(out e1);
@@ -1505,64 +1509,64 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void RelOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
switch (la.kind) {
- case 60: {
+ case 62: {
Get();
x = t; op=BinaryOperator.Opcode.Eq;
break;
}
- case 17: {
+ case 19: {
Get();
x = t; op=BinaryOperator.Opcode.Lt;
break;
}
- case 18: {
+ case 20: {
Get();
x = t; op=BinaryOperator.Opcode.Gt;
break;
}
- case 61: {
+ case 63: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 62: {
+ case 64: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- case 63: {
+ case 65: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 64: {
+ case 66: {
Get();
x = t; op=BinaryOperator.Opcode.Subtype;
break;
}
- case 65: {
+ case 67: {
Get();
x = t; op=BinaryOperator.Opcode.Neq;
break;
}
- case 66: {
+ case 68: {
Get();
x = t; op=BinaryOperator.Opcode.Le;
break;
}
- case 67: {
+ case 69: {
Get();
x = t; op=BinaryOperator.Opcode.Ge;
break;
}
- default: SynErr(112); break;
+ default: SynErr(116); break;
}
}
void Term(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
Factor(out e0);
- while (la.kind == 69 || la.kind == 70) {
+ while (la.kind == 71 || la.kind == 72) {
AddOp(out x, out op);
Factor(out e1);
e0 = Expr.Binary(x, op, e0, e1);
@@ -1571,64 +1575,78 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { void Factor(out Expr/*!*/ e0) {
Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1; BinaryOperator.Opcode op;
- UnaryExpression(out e0);
- while (la.kind == 42 || la.kind == 71 || la.kind == 72) {
+ Power(out e0);
+ while (StartOf(13)) {
MulOp(out x, out op);
- UnaryExpression(out e1);
+ Power(out e1);
e0 = Expr.Binary(x, op, e0, e1);
}
}
void AddOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 69) {
+ if (la.kind == 71) {
Get();
x = t; op=BinaryOperator.Opcode.Add;
- } else if (la.kind == 70) {
+ } else if (la.kind == 72) {
Get();
x = t; op=BinaryOperator.Opcode.Sub;
- } else SynErr(113);
+ } else SynErr(117);
}
- void UnaryExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
- e = dummyExpr;
-
- if (la.kind == 70) {
+ void Power(out Expr/*!*/ e0) {
+ Contract.Ensures(Contract.ValueAtReturn(out e0) != null); IToken/*!*/ x; Expr/*!*/ e1;
+ UnaryExpression(out e0);
+ if (la.kind == 76) {
Get();
x = t;
- UnaryExpression(out e);
- e = Expr.Binary(x, BinaryOperator.Opcode.Sub, new LiteralExpr(x, BigNum.ZERO), e);
- } else if (la.kind == 73 || la.kind == 74) {
- NegOp();
- x = t;
- UnaryExpression(out e);
- e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
- } else if (StartOf(12)) {
- CoercionExpression(out e);
- } else SynErr(114);
+ Power(out e1);
+ e0 = Expr.Binary(x, BinaryOperator.Opcode.Pow, e0, e1);
+ }
}
void MulOp(out IToken/*!*/ x, out BinaryOperator.Opcode op) {
Contract.Ensures(Contract.ValueAtReturn(out x) != null); x = Token.NoToken; op=BinaryOperator.Opcode.Add/*(dummy)*/;
- if (la.kind == 42) {
+ if (la.kind == 44) {
Get();
x = t; op=BinaryOperator.Opcode.Mul;
- } else if (la.kind == 71) {
+ } else if (la.kind == 73) {
Get();
x = t; op=BinaryOperator.Opcode.Div;
- } else if (la.kind == 72) {
+ } else if (la.kind == 74) {
Get();
x = t; op=BinaryOperator.Opcode.Mod;
- } else SynErr(115);
+ } else if (la.kind == 75) {
+ Get();
+ x = t; op=BinaryOperator.Opcode.RealDiv;
+ } else SynErr(118);
+ }
+
+ void UnaryExpression(out Expr/*!*/ e) {
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x;
+ e = dummyExpr;
+
+ if (la.kind == 72) {
+ Get();
+ x = t;
+ UnaryExpression(out e);
+ e = Expr.Unary(x, UnaryOperator.Opcode.Neg, e);
+ } else if (la.kind == 77 || la.kind == 78) {
+ NegOp();
+ x = t;
+ UnaryExpression(out e);
+ e = Expr.Unary(x, UnaryOperator.Opcode.Not, e);
+ } else if (StartOf(14)) {
+ CoercionExpression(out e);
+ } else SynErr(119);
}
void NegOp() {
- if (la.kind == 73) {
+ if (la.kind == 77) {
Get();
- } else if (la.kind == 74) {
+ } else if (la.kind == 78) {
Get();
- } else SynErr(116);
+ } else SynErr(120);
}
void CoercionExpression(out Expr/*!*/ e) {
@@ -1637,7 +1655,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { BigNum bn;
ArrayExpression(out e);
- while (la.kind == 10) {
+ while (la.kind == 11) {
Get();
x = t;
if (StartOf(2)) {
@@ -1652,7 +1670,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { e = new BvBounds(x, bn, ((LiteralExpr)e).asBigNum);
}
- } else SynErr(117);
+ } else SynErr(121);
}
}
@@ -1663,20 +1681,20 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { ExprSeq/*!*/ allArgs = dummyExprSeq;
AtomExpression(out e);
- while (la.kind == 15) {
+ while (la.kind == 17) {
Get();
x = t; allArgs = new ExprSeq ();
allArgs.Add(e);
store = false; bvExtract = false;
- if (StartOf(13)) {
- if (StartOf(7)) {
+ if (StartOf(15)) {
+ if (StartOf(8)) {
Expression(out index0);
if (index0 is BvBounds)
bvExtract = true;
else
allArgs.Add(index0);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1684,7 +1702,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1);
}
- if (la.kind == 47) {
+ if (la.kind == 49) {
Get();
Expression(out e1);
if (bvExtract || e1 is BvBounds)
@@ -1698,7 +1716,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { allArgs.Add(e1); store = true;
}
}
- Expect(16);
+ Expect(18);
if (store)
e = new NAryExpr(x, new MapStore(x, allArgs.Length - 2), allArgs);
else if (bvExtract)
@@ -1723,7 +1741,7 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
void AtomExpression(out Expr/*!*/ e) {
- Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn;
+ Contract.Ensures(Contract.ValueAtReturn(out e) != null); IToken/*!*/ x; int n; BigNum bn; BigDec bd;
ExprSeq/*!*/ es; VariableSeq/*!*/ ds; Trigger trig;
TypeVariableSeq/*!*/ typeParams;
IdentifierExpr/*!*/ id;
@@ -1733,12 +1751,12 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { List<Block/*!*/>/*!*/ blocks;
switch (la.kind) {
- case 75: {
+ case 79: {
Get();
e = new LiteralExpr(t, false);
break;
}
- case 76: {
+ case 80: {
Get();
e = new LiteralExpr(t, true);
break;
@@ -1748,6 +1766,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { e = new LiteralExpr(t, bn);
break;
}
+ case 5: case 6: {
+ Dec(out bd);
+ e = new LiteralExpr(t, bd);
+ break;
+ }
case 2: {
BvLit(out bn, out n);
e = new LiteralExpr(t, bn, n);
@@ -1756,47 +1779,65 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { case 1: {
Ident(out x);
id = new IdentifierExpr(x, x.val); e = id;
- if (la.kind == 8) {
+ if (la.kind == 9) {
Get();
- if (StartOf(7)) {
+ if (StartOf(8)) {
Expressions(out es);
e = new NAryExpr(x, new FunctionCall(id), es);
- } else if (la.kind == 9) {
+ } else if (la.kind == 10) {
e = new NAryExpr(x, new FunctionCall(id), new ExprSeq());
- } else SynErr(118);
- Expect(9);
+ } else SynErr(122);
+ Expect(10);
}
break;
}
- case 77: {
+ case 81: {
Get();
x = t;
- Expect(8);
- Expression(out e);
Expect(9);
+ Expression(out e);
+ Expect(10);
e = new OldExpr(x, e);
break;
}
- case 8: {
+ case 14: {
Get();
- if (StartOf(7)) {
+ x = t;
+ Expect(9);
+ Expression(out e);
+ Expect(10);
+ e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToInt), new ExprSeq(e));
+ break;
+ }
+ case 15: {
+ Get();
+ x = t;
+ Expect(9);
+ Expression(out e);
+ Expect(10);
+ e = new NAryExpr(x, new ArithmeticCoercion(x, ArithmeticCoercion.CoercionType.ToReal), new ExprSeq(e));
+ break;
+ }
+ case 9: {
+ Get();
+ if (StartOf(8)) {
Expression(out e);
if (e is BvBounds)
this.SemErr("parentheses around bitvector bounds " +
"are not allowed");
- } else if (la.kind == 49 || la.kind == 81) {
+ } else if (la.kind == 51 || la.kind == 85) {
Forall();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ForallExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 82 || la.kind == 83) {
+ } else if (la.kind == 86 || la.kind == 87) {
Exists();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
if (typeParams.Length + ds.Length > 0)
e = new ExistsExpr(x, typeParams, ds, kv, trig, e);
- } else if (la.kind == 84 || la.kind == 85) {
+ } else if (la.kind == 88 || la.kind == 89) {
Lambda();
x = t;
QuantifierBody(x, out typeParams, out ds, out kv, out trig, out e);
@@ -1804,21 +1845,39 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { SemErr("triggers not allowed in lambda expressions");
if (typeParams.Length + ds.Length > 0)
e = new LambdaExpr(x, typeParams, ds, kv, e);
- } else SynErr(119);
- Expect(9);
+ } else SynErr(123);
+ Expect(10);
break;
}
- case 38: {
+ case 40: {
IfThenElseExpression(out e);
break;
}
- case 78: {
+ case 82: {
CodeExpression(out locals, out blocks);
e = new CodeExpr(locals, blocks);
break;
}
- default: SynErr(120); break;
+ default: SynErr(124); break;
+ }
+ }
+
+ void Dec(out BigDec n) {
+ string s = "";
+ if (la.kind == 5) {
+ Get();
+ s = t.val;
+ } else if (la.kind == 6) {
+ Get();
+ s = t.val;
+ } else SynErr(125);
+ try {
+ n = BigDec.FromString(s);
+ } catch (FormatException) {
+ this.SemErr("incorrectly formatted number");
+ n = BigDec.ZERO;
}
+
}
void BvLit(out BigNum n, out int m) {
@@ -1838,11 +1897,11 @@ out VariableSeq/*!*/ ins, out VariableSeq/*!*/ outs, out QKeyValue kv) { }
void Forall() {
- if (la.kind == 49) {
+ if (la.kind == 51) {
Get();
- } else if (la.kind == 81) {
+ } else if (la.kind == 85) {
Get();
- } else SynErr(121);
+ } else SynErr(126);
}
void QuantifierBody(IToken/*!*/ q, out TypeVariableSeq/*!*/ typeParams, out VariableSeq/*!*/ ds,
@@ -1853,35 +1912,35 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { kv = null;
ds = new VariableSeq ();
- if (la.kind == 17) {
+ if (la.kind == 19) {
TypeParams(out tok, out typeParams);
if (la.kind == 1) {
BoundVars(q, out ds);
}
} else if (la.kind == 1) {
BoundVars(q, out ds);
- } else SynErr(122);
+ } else SynErr(127);
QSep();
- while (la.kind == 25) {
+ while (la.kind == 27) {
AttributeOrTrigger(ref kv, ref trig);
}
Expression(out body);
}
void Exists() {
- if (la.kind == 82) {
+ if (la.kind == 86) {
Get();
- } else if (la.kind == 83) {
+ } else if (la.kind == 87) {
Get();
- } else SynErr(123);
+ } else SynErr(128);
}
void Lambda() {
- if (la.kind == 84) {
+ if (la.kind == 88) {
Get();
- } else if (la.kind == 85) {
+ } else if (la.kind == 89) {
Get();
- } else SynErr(124);
+ } else SynErr(129);
}
void IfThenElseExpression(out Expr/*!*/ e) {
@@ -1889,12 +1948,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { IToken/*!*/ tok;
Expr/*!*/ e0, e1, e2;
e = dummyExpr;
- Expect(38);
+ Expect(40);
tok = t;
Expression(out e0);
- Expect(80);
+ Expect(84);
Expression(out e1);
- Expect(39);
+ Expect(41);
Expression(out e2);
e = new NAryExpr(tok, new IfThenElse(tok), new ExprSeq(e0, e1, e2));
}
@@ -1903,8 +1962,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Contract.Ensures(Contract.ValueAtReturn(out locals) != null); Contract.Ensures(cce.NonNullElements(Contract.ValueAtReturn(out blocks))); locals = new VariableSeq(); Block/*!*/ b;
blocks = new List<Block/*!*/>();
- Expect(78);
- while (la.kind == 6) {
+ Expect(82);
+ while (la.kind == 7) {
LocalVars(locals);
}
SpecBlock(out b);
@@ -1913,7 +1972,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { SpecBlock(out b);
blocks.Add(b);
}
- Expect(79);
+ Expect(83);
}
void SpecBlock(out Block/*!*/ b) {
@@ -1926,8 +1985,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { Expr/*!*/ e;
Ident(out x);
- Expect(10);
- while (StartOf(6)) {
+ Expect(11);
+ while (StartOf(7)) {
LabelOrCmd(out c, out label);
if (c != null) {
Contract.Assert(label == null);
@@ -1938,7 +1997,7 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { }
}
- if (la.kind == 36) {
+ if (la.kind == 38) {
Get();
y = t;
Idents(out xs);
@@ -1947,12 +2006,12 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { ss.Add(s.val); }
b = new Block(x,x.val,cs,new GotoCmd(y,ss));
- } else if (la.kind == 37) {
+ } else if (la.kind == 39) {
Get();
Expression(out e);
b = new Block(x,x.val,cs,new ReturnExprCmd(t,e));
- } else SynErr(125);
- Expect(7);
+ } else SynErr(130);
+ Expect(8);
}
void AttributeOrTrigger(ref QKeyValue kv, ref Trigger trig) {
@@ -1960,16 +2019,16 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { string key;
List<object/*!*/> parameters; object/*!*/ param;
- Expect(25);
+ Expect(27);
tok = t;
- if (la.kind == 10) {
+ if (la.kind == 11) {
Get();
Expect(1);
key = t.val; parameters = new List<object/*!*/>();
- if (StartOf(14)) {
+ if (StartOf(16)) {
AttributeParameter(out param);
parameters.Add(param);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
AttributeParameter(out param);
parameters.Add(param);
@@ -1994,10 +2053,10 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { }
}
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
es = new ExprSeq(e);
- while (la.kind == 11) {
+ while (la.kind == 12) {
Get();
Expression(out e);
es.Add(e);
@@ -2008,8 +2067,8 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { trig.AddLast(new Trigger(tok, true, es, null));
}
- } else SynErr(126);
- Expect(26);
+ } else SynErr(131);
+ Expect(28);
}
void AttributeParameter(out object/*!*/ o) {
@@ -2020,18 +2079,18 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { if (la.kind == 4) {
Get();
o = t.val.Substring(1, t.val.Length-2);
- } else if (StartOf(7)) {
+ } else if (StartOf(8)) {
Expression(out e);
o = e;
- } else SynErr(127);
+ } else SynErr(132);
}
void QSep() {
- if (la.kind == 86) {
+ if (la.kind == 90) {
Get();
- } else if (la.kind == 87) {
+ } else if (la.kind == 91) {
Get();
- } else SynErr(128);
+ } else SynErr(133);
}
@@ -2047,21 +2106,23 @@ out QKeyValue kv, out Trigger trig, out Expr/*!*/ body) { }
static readonly bool[,]/*!*/ set = {
- {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,T, x,x,x,T, T,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, T,x,x,x, x,T,T,T, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, T,T,T,x, T,x,x,T, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, T,T,T,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,T,T,T, T,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
- {x,T,T,T, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}
+ {T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,T,x,x, x,T,x,x, x,T,T,x, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,T,x,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,T,x,x, x,x,T,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,T,T, T,x,T,x, x,T,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, x,x,x,x, x,x,x,x, x,x,T,T, T,x,T,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,T,T, T,T,T,T, T,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,T,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, x,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,T,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x},
+ {x,T,T,T, T,T,T,x, x,T,x,x, x,x,T,T, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, x,x,x,x, T,x,x,x, x,T,T,T, T,T,T,x, x,x,x,x, x,x,x,x, x,x}
};
} // end Parser
@@ -2091,130 +2152,135 @@ public class Errors { case 2: s = "bvlit expected"; break;
case 3: s = "digits expected"; break;
case 4: s = "string expected"; break;
- case 5: s = "float expected"; break;
- case 6: s = "\"var\" expected"; break;
- case 7: s = "\";\" expected"; break;
- case 8: s = "\"(\" expected"; break;
- case 9: s = "\")\" expected"; break;
- case 10: s = "\":\" expected"; break;
- case 11: s = "\",\" expected"; break;
- case 12: s = "\"where\" expected"; break;
- case 13: s = "\"int\" expected"; break;
- case 14: s = "\"bool\" expected"; break;
- case 15: s = "\"[\" expected"; break;
- case 16: s = "\"]\" expected"; break;
- case 17: s = "\"<\" expected"; break;
- case 18: s = "\">\" expected"; break;
- case 19: s = "\"const\" expected"; break;
- case 20: s = "\"unique\" expected"; break;
- case 21: s = "\"extends\" expected"; break;
- case 22: s = "\"complete\" expected"; break;
- case 23: s = "\"function\" expected"; break;
- case 24: s = "\"returns\" expected"; break;
- case 25: s = "\"{\" expected"; break;
- case 26: s = "\"}\" expected"; break;
- case 27: s = "\"axiom\" expected"; break;
- case 28: s = "\"type\" expected"; break;
- case 29: s = "\"=\" expected"; break;
- case 30: s = "\"procedure\" expected"; break;
- case 31: s = "\"implementation\" expected"; break;
- case 32: s = "\"modifies\" expected"; break;
- case 33: s = "\"free\" expected"; break;
- case 34: s = "\"requires\" expected"; break;
- case 35: s = "\"ensures\" expected"; break;
- case 36: s = "\"goto\" expected"; break;
- case 37: s = "\"return\" expected"; break;
- case 38: s = "\"if\" expected"; break;
- case 39: s = "\"else\" expected"; break;
- case 40: s = "\"while\" expected"; break;
- case 41: s = "\"invariant\" expected"; break;
- case 42: s = "\"*\" expected"; break;
- case 43: s = "\"break\" expected"; break;
- case 44: s = "\"assert\" expected"; break;
- case 45: s = "\"assume\" expected"; break;
- case 46: s = "\"havoc\" expected"; break;
- case 47: s = "\":=\" expected"; break;
- case 48: s = "\"call\" expected"; break;
- case 49: s = "\"forall\" expected"; break;
- case 50: s = "\"<==>\" expected"; break;
- case 51: s = "\"\\u21d4\" expected"; break;
- case 52: s = "\"==>\" expected"; break;
- case 53: s = "\"\\u21d2\" expected"; break;
- case 54: s = "\"<==\" expected"; break;
- case 55: s = "\"\\u21d0\" expected"; break;
- case 56: s = "\"&&\" expected"; break;
- case 57: s = "\"\\u2227\" expected"; break;
- case 58: s = "\"||\" expected"; break;
- case 59: s = "\"\\u2228\" expected"; break;
- case 60: s = "\"==\" expected"; break;
- case 61: s = "\"<=\" expected"; break;
- case 62: s = "\">=\" expected"; break;
- case 63: s = "\"!=\" expected"; break;
- case 64: s = "\"<:\" expected"; break;
- case 65: s = "\"\\u2260\" expected"; break;
- case 66: s = "\"\\u2264\" expected"; break;
- case 67: s = "\"\\u2265\" expected"; break;
- case 68: s = "\"++\" expected"; break;
- case 69: s = "\"+\" expected"; break;
- case 70: s = "\"-\" expected"; break;
- case 71: s = "\"div\" expected"; break;
- case 72: s = "\"mod\" expected"; break;
- case 73: s = "\"!\" expected"; break;
- case 74: s = "\"\\u00ac\" expected"; break;
- case 75: s = "\"false\" expected"; break;
- case 76: s = "\"true\" expected"; break;
- case 77: s = "\"old\" expected"; break;
- case 78: s = "\"|{\" expected"; break;
- case 79: s = "\"}|\" expected"; break;
- case 80: s = "\"then\" expected"; break;
- case 81: s = "\"\\u2200\" expected"; break;
- case 82: s = "\"exists\" expected"; break;
- case 83: s = "\"\\u2203\" expected"; break;
- case 84: s = "\"lambda\" expected"; break;
- case 85: s = "\"\\u03bb\" expected"; break;
- case 86: s = "\"::\" expected"; break;
- case 87: s = "\"\\u2022\" expected"; break;
- case 88: s = "??? expected"; break;
- case 89: s = "invalid Function"; break;
- case 90: s = "invalid Function"; break;
- case 91: s = "invalid Procedure"; break;
- case 92: s = "invalid Type"; break;
- case 93: s = "invalid TypeAtom"; break;
- case 94: s = "invalid TypeArgs"; break;
- case 95: s = "invalid Spec"; break;
- case 96: s = "invalid SpecPrePost"; break;
- case 97: s = "invalid LabelOrCmd"; break;
- case 98: s = "invalid StructuredCmd"; break;
- case 99: s = "invalid TransferCmd"; break;
- case 100: s = "invalid IfCmd"; break;
- case 101: s = "invalid Guard"; break;
- case 102: s = "invalid LabelOrAssign"; break;
- case 103: s = "invalid CallCmd"; break;
- case 104: s = "invalid CallCmd"; break;
- case 105: s = "invalid CallForallArg"; break;
- case 106: s = "invalid CallOutIdent"; break;
- case 107: s = "invalid EquivOp"; break;
- case 108: s = "invalid ImpliesOp"; break;
- case 109: s = "invalid ExpliesOp"; break;
- case 110: s = "invalid AndOp"; break;
- case 111: s = "invalid OrOp"; break;
- case 112: s = "invalid RelOp"; break;
- case 113: s = "invalid AddOp"; break;
- case 114: s = "invalid UnaryExpression"; break;
- case 115: s = "invalid MulOp"; break;
- case 116: s = "invalid NegOp"; break;
- case 117: s = "invalid CoercionExpression"; break;
- case 118: s = "invalid AtomExpression"; break;
- case 119: s = "invalid AtomExpression"; break;
- case 120: s = "invalid AtomExpression"; break;
- case 121: s = "invalid Forall"; break;
- case 122: s = "invalid QuantifierBody"; break;
- case 123: s = "invalid Exists"; break;
- case 124: s = "invalid Lambda"; break;
- case 125: s = "invalid SpecBlock"; break;
- case 126: s = "invalid AttributeOrTrigger"; break;
- case 127: s = "invalid AttributeParameter"; break;
- case 128: s = "invalid QSep"; break;
+ case 5: s = "decimal expected"; break;
+ case 6: s = "float expected"; break;
+ case 7: s = "\"var\" expected"; break;
+ case 8: s = "\";\" expected"; break;
+ case 9: s = "\"(\" expected"; break;
+ case 10: s = "\")\" expected"; break;
+ case 11: s = "\":\" expected"; break;
+ case 12: s = "\",\" expected"; break;
+ case 13: s = "\"where\" expected"; break;
+ case 14: s = "\"int\" expected"; break;
+ case 15: s = "\"real\" expected"; break;
+ case 16: s = "\"bool\" expected"; break;
+ case 17: s = "\"[\" expected"; break;
+ case 18: s = "\"]\" expected"; break;
+ case 19: s = "\"<\" expected"; break;
+ case 20: s = "\">\" expected"; break;
+ case 21: s = "\"const\" expected"; break;
+ case 22: s = "\"unique\" expected"; break;
+ case 23: s = "\"extends\" expected"; break;
+ case 24: s = "\"complete\" expected"; break;
+ case 25: s = "\"function\" expected"; break;
+ case 26: s = "\"returns\" expected"; break;
+ case 27: s = "\"{\" expected"; break;
+ case 28: s = "\"}\" expected"; break;
+ case 29: s = "\"axiom\" expected"; break;
+ case 30: s = "\"type\" expected"; break;
+ case 31: s = "\"=\" expected"; break;
+ case 32: s = "\"procedure\" expected"; break;
+ case 33: s = "\"implementation\" expected"; break;
+ case 34: s = "\"modifies\" expected"; break;
+ case 35: s = "\"free\" expected"; break;
+ case 36: s = "\"requires\" expected"; break;
+ case 37: s = "\"ensures\" expected"; break;
+ case 38: s = "\"goto\" expected"; break;
+ case 39: s = "\"return\" expected"; break;
+ case 40: s = "\"if\" expected"; break;
+ case 41: s = "\"else\" expected"; break;
+ case 42: s = "\"while\" expected"; break;
+ case 43: s = "\"invariant\" expected"; break;
+ case 44: s = "\"*\" expected"; break;
+ case 45: s = "\"break\" expected"; break;
+ case 46: s = "\"assert\" expected"; break;
+ case 47: s = "\"assume\" expected"; break;
+ case 48: s = "\"havoc\" expected"; break;
+ case 49: s = "\":=\" expected"; break;
+ case 50: s = "\"call\" expected"; break;
+ case 51: s = "\"forall\" expected"; break;
+ case 52: s = "\"<==>\" expected"; break;
+ case 53: s = "\"\\u21d4\" expected"; break;
+ case 54: s = "\"==>\" expected"; break;
+ case 55: s = "\"\\u21d2\" expected"; break;
+ case 56: s = "\"<==\" expected"; break;
+ case 57: s = "\"\\u21d0\" expected"; break;
+ case 58: s = "\"&&\" expected"; break;
+ case 59: s = "\"\\u2227\" expected"; break;
+ case 60: s = "\"||\" expected"; break;
+ case 61: s = "\"\\u2228\" expected"; break;
+ case 62: s = "\"==\" expected"; break;
+ case 63: s = "\"<=\" expected"; break;
+ case 64: s = "\">=\" expected"; break;
+ case 65: s = "\"!=\" expected"; break;
+ case 66: s = "\"<:\" expected"; break;
+ case 67: s = "\"\\u2260\" expected"; break;
+ case 68: s = "\"\\u2264\" expected"; break;
+ case 69: s = "\"\\u2265\" expected"; break;
+ case 70: s = "\"++\" expected"; break;
+ case 71: s = "\"+\" expected"; break;
+ case 72: s = "\"-\" expected"; break;
+ case 73: s = "\"div\" expected"; break;
+ case 74: s = "\"mod\" expected"; break;
+ case 75: s = "\"/\" expected"; break;
+ case 76: s = "\"**\" expected"; break;
+ case 77: s = "\"!\" expected"; break;
+ case 78: s = "\"\\u00ac\" expected"; break;
+ case 79: s = "\"false\" expected"; break;
+ case 80: s = "\"true\" expected"; break;
+ case 81: s = "\"old\" expected"; break;
+ case 82: s = "\"|{\" expected"; break;
+ case 83: s = "\"}|\" expected"; break;
+ case 84: s = "\"then\" expected"; break;
+ case 85: s = "\"\\u2200\" expected"; break;
+ case 86: s = "\"exists\" expected"; break;
+ case 87: s = "\"\\u2203\" expected"; break;
+ case 88: s = "\"lambda\" expected"; break;
+ case 89: s = "\"\\u03bb\" expected"; break;
+ case 90: s = "\"::\" expected"; break;
+ case 91: s = "\"\\u2022\" expected"; break;
+ case 92: s = "??? expected"; break;
+ case 93: s = "invalid Function"; break;
+ case 94: s = "invalid Function"; break;
+ case 95: s = "invalid Procedure"; break;
+ case 96: s = "invalid Type"; break;
+ case 97: s = "invalid TypeAtom"; break;
+ case 98: s = "invalid TypeArgs"; break;
+ case 99: s = "invalid Spec"; break;
+ case 100: s = "invalid SpecPrePost"; break;
+ case 101: s = "invalid LabelOrCmd"; break;
+ case 102: s = "invalid StructuredCmd"; break;
+ case 103: s = "invalid TransferCmd"; break;
+ case 104: s = "invalid IfCmd"; break;
+ case 105: s = "invalid Guard"; break;
+ case 106: s = "invalid LabelOrAssign"; break;
+ case 107: s = "invalid CallCmd"; break;
+ case 108: s = "invalid CallCmd"; break;
+ case 109: s = "invalid CallForallArg"; break;
+ case 110: s = "invalid CallOutIdent"; break;
+ case 111: s = "invalid EquivOp"; break;
+ case 112: s = "invalid ImpliesOp"; break;
+ case 113: s = "invalid ExpliesOp"; break;
+ case 114: s = "invalid AndOp"; break;
+ case 115: s = "invalid OrOp"; break;
+ case 116: s = "invalid RelOp"; break;
+ case 117: s = "invalid AddOp"; break;
+ case 118: s = "invalid MulOp"; break;
+ case 119: s = "invalid UnaryExpression"; break;
+ case 120: s = "invalid NegOp"; break;
+ case 121: s = "invalid CoercionExpression"; break;
+ case 122: s = "invalid AtomExpression"; break;
+ case 123: s = "invalid AtomExpression"; break;
+ case 124: s = "invalid AtomExpression"; break;
+ case 125: s = "invalid Dec"; break;
+ case 126: s = "invalid Forall"; break;
+ case 127: s = "invalid QuantifierBody"; break;
+ case 128: s = "invalid Exists"; break;
+ case 129: s = "invalid Lambda"; break;
+ case 130: s = "invalid SpecBlock"; break;
+ case 131: s = "invalid AttributeOrTrigger"; break;
+ case 132: s = "invalid AttributeParameter"; break;
+ case 133: s = "invalid QSep"; break;
default: s = "error " + n; break;
}
diff --git a/Source/Core/Scanner.cs b/Source/Core/Scanner.cs index b9f4ec42..60c15b41 100644 --- a/Source/Core/Scanner.cs +++ b/Source/Core/Scanner.cs @@ -211,8 +211,8 @@ public class UTF8Buffer: Buffer { public class Scanner {
const char EOL = '\n';
const int eofSym = 0; /* pdt */
- const int maxT = 88;
- const int noSym = 88;
+ const int maxT = 92;
+ const int noSym = 92;
[ContractInvariantMethod]
@@ -256,40 +256,41 @@ public class Scanner { for (int i = 65; i <= 90; ++i) start[i] = 2;
for (int i = 94; i <= 122; ++i) start[i] = 2;
for (int i = 126; i <= 126; ++i) start[i] = 2;
- for (int i = 48; i <= 57; ++i) start[i] = 9;
+ for (int i = 48; i <= 57; ++i) start[i] = 16;
for (int i = 34; i <= 34; ++i) start[i] = 6;
start[92] = 1;
- start[59] = 12;
- start[40] = 13;
- start[41] = 14;
- start[58] = 47;
- start[44] = 15;
- start[91] = 16;
- start[93] = 17;
- start[60] = 48;
- start[62] = 49;
- start[123] = 18;
- start[125] = 50;
- start[61] = 51;
- start[42] = 19;
- start[8660] = 22;
- start[8658] = 24;
- start[8656] = 25;
- start[38] = 26;
- start[8743] = 28;
- start[124] = 52;
- start[8744] = 30;
- start[33] = 53;
- start[8800] = 34;
- start[8804] = 35;
- start[8805] = 36;
- start[43] = 54;
- start[45] = 38;
- start[172] = 39;
- start[8704] = 42;
- start[8707] = 43;
- start[955] = 44;
- start[8226] = 46;
+ start[59] = 19;
+ start[40] = 20;
+ start[41] = 21;
+ start[58] = 55;
+ start[44] = 22;
+ start[91] = 23;
+ start[93] = 24;
+ start[60] = 56;
+ start[62] = 57;
+ start[123] = 25;
+ start[125] = 58;
+ start[61] = 59;
+ start[42] = 60;
+ start[8660] = 28;
+ start[8658] = 30;
+ start[8656] = 31;
+ start[38] = 32;
+ start[8743] = 34;
+ start[124] = 61;
+ start[8744] = 36;
+ start[33] = 62;
+ start[8800] = 40;
+ start[8804] = 41;
+ start[8805] = 42;
+ start[43] = 63;
+ start[45] = 44;
+ start[47] = 45;
+ start[172] = 47;
+ start[8704] = 50;
+ start[8707] = 51;
+ start[955] = 52;
+ start[8226] = 54;
start[Buffer.EOF] = -1;
}
@@ -487,44 +488,45 @@ public class Scanner { void CheckLiteral() {
switch (t.val) {
- case "var": t.kind = 6; break;
- case "where": t.kind = 12; break;
- case "int": t.kind = 13; break;
- case "bool": t.kind = 14; break;
- case "const": t.kind = 19; break;
- case "unique": t.kind = 20; break;
- case "extends": t.kind = 21; break;
- case "complete": t.kind = 22; break;
- case "function": t.kind = 23; break;
- case "returns": t.kind = 24; break;
- case "axiom": t.kind = 27; break;
- case "type": t.kind = 28; break;
- case "procedure": t.kind = 30; break;
- case "implementation": t.kind = 31; break;
- case "modifies": t.kind = 32; break;
- case "free": t.kind = 33; break;
- case "requires": t.kind = 34; break;
- case "ensures": t.kind = 35; break;
- case "goto": t.kind = 36; break;
- case "return": t.kind = 37; break;
- case "if": t.kind = 38; break;
- case "else": t.kind = 39; break;
- case "while": t.kind = 40; break;
- case "invariant": t.kind = 41; break;
- case "break": t.kind = 43; break;
- case "assert": t.kind = 44; break;
- case "assume": t.kind = 45; break;
- case "havoc": t.kind = 46; break;
- case "call": t.kind = 48; break;
- case "forall": t.kind = 49; break;
- case "div": t.kind = 71; break;
- case "mod": t.kind = 72; break;
- case "false": t.kind = 75; break;
- case "true": t.kind = 76; break;
- case "old": t.kind = 77; break;
- case "then": t.kind = 80; break;
- case "exists": t.kind = 82; break;
- case "lambda": t.kind = 84; break;
+ case "var": t.kind = 7; break;
+ case "where": t.kind = 13; break;
+ case "int": t.kind = 14; break;
+ case "real": t.kind = 15; break;
+ case "bool": t.kind = 16; break;
+ case "const": t.kind = 21; break;
+ case "unique": t.kind = 22; break;
+ case "extends": t.kind = 23; break;
+ case "complete": t.kind = 24; break;
+ case "function": t.kind = 25; break;
+ case "returns": t.kind = 26; break;
+ case "axiom": t.kind = 29; break;
+ case "type": t.kind = 30; break;
+ case "procedure": t.kind = 32; break;
+ case "implementation": t.kind = 33; break;
+ case "modifies": t.kind = 34; break;
+ case "free": t.kind = 35; break;
+ case "requires": t.kind = 36; break;
+ case "ensures": t.kind = 37; break;
+ case "goto": t.kind = 38; break;
+ case "return": t.kind = 39; break;
+ case "if": t.kind = 40; break;
+ case "else": t.kind = 41; break;
+ case "while": t.kind = 42; break;
+ case "invariant": t.kind = 43; break;
+ case "break": t.kind = 45; break;
+ case "assert": t.kind = 46; break;
+ case "assume": t.kind = 47; break;
+ case "havoc": t.kind = 48; break;
+ case "call": t.kind = 50; break;
+ case "forall": t.kind = 51; break;
+ case "div": t.kind = 73; break;
+ case "mod": t.kind = 74; break;
+ case "false": t.kind = 79; break;
+ case "true": t.kind = 80; break;
+ case "old": t.kind = 81; break;
+ case "then": t.kind = 84; break;
+ case "exists": t.kind = 86; break;
+ case "lambda": t.kind = 88; break;
default: break;
}
}
@@ -577,148 +579,181 @@ public class Scanner { case 6:
if (ch == '"') {AddCh(); goto case 7;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 10;}
+ else if (ch == 92) {AddCh(); goto case 17;}
else {goto case 0;}
case 7:
{t.kind = 4; break;}
case 8:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
+ else if (ch == '-') {AddCh(); goto case 9;}
+ else {goto case 0;}
+ case 9:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
+ else {goto case 0;}
+ case 10:
recEnd = pos; recKind = 5;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 8;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 10;}
else {t.kind = 5; break;}
- case 9:
+ case 11:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ else {goto case 0;}
+ case 12:
+ recEnd = pos; recKind = 6;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 12;}
+ else if (ch == 'e') {AddCh(); goto case 13;}
+ else {t.kind = 6; break;}
+ case 13:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+ else if (ch == '-') {AddCh(); goto case 14;}
+ else {goto case 0;}
+ case 14:
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+ else {goto case 0;}
+ case 15:
+ recEnd = pos; recKind = 6;
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 15;}
+ else {t.kind = 6; break;}
+ case 16:
recEnd = pos; recKind = 3;
- if (ch >= '0' && ch <= '9') {AddCh(); goto case 9;}
+ if (ch >= '0' && ch <= '9') {AddCh(); goto case 16;}
else if (ch == 'b') {AddCh(); goto case 3;}
- else if (ch == '.') {AddCh(); goto case 8;}
+ else if (ch == 'e') {AddCh(); goto case 8;}
+ else if (ch == '.') {AddCh(); goto case 11;}
else {t.kind = 3; break;}
- case 10:
- if (ch == '"') {AddCh(); goto case 11;}
+ case 17:
+ if (ch == '"') {AddCh(); goto case 18;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 10;}
+ else if (ch == 92) {AddCh(); goto case 17;}
else {goto case 0;}
- case 11:
+ case 18:
recEnd = pos; recKind = 4;
if (ch == '"') {AddCh(); goto case 7;}
else if (ch <= 9 || ch >= 11 && ch <= 12 || ch >= 14 && ch <= '!' || ch >= '#' && ch <= '[' || ch >= ']' && ch <= 65535) {AddCh(); goto case 6;}
- else if (ch == 92) {AddCh(); goto case 10;}
+ else if (ch == 92) {AddCh(); goto case 17;}
else {t.kind = 4; break;}
- case 12:
- {t.kind = 7; break;}
- case 13:
- {t.kind = 8; break;}
- case 14:
- {t.kind = 9; break;}
- case 15:
- {t.kind = 11; break;}
- case 16:
- {t.kind = 15; break;}
- case 17:
- {t.kind = 16; break;}
- case 18:
- {t.kind = 25; break;}
case 19:
- {t.kind = 42; break;}
+ {t.kind = 8; break;}
case 20:
- {t.kind = 47; break;}
+ {t.kind = 9; break;}
case 21:
- {t.kind = 50; break;}
+ {t.kind = 10; break;}
case 22:
- {t.kind = 51; break;}
+ {t.kind = 12; break;}
case 23:
- {t.kind = 52; break;}
+ {t.kind = 17; break;}
case 24:
- {t.kind = 53; break;}
+ {t.kind = 18; break;}
case 25:
- {t.kind = 55; break;}
+ {t.kind = 27; break;}
case 26:
- if (ch == '&') {AddCh(); goto case 27;}
- else {goto case 0;}
+ {t.kind = 49; break;}
case 27:
- {t.kind = 56; break;}
+ {t.kind = 52; break;}
case 28:
- {t.kind = 57; break;}
+ {t.kind = 53; break;}
case 29:
- {t.kind = 58; break;}
+ {t.kind = 54; break;}
case 30:
- {t.kind = 59; break;}
+ {t.kind = 55; break;}
case 31:
- {t.kind = 62; break;}
+ {t.kind = 57; break;}
case 32:
- {t.kind = 63; break;}
+ if (ch == '&') {AddCh(); goto case 33;}
+ else {goto case 0;}
case 33:
- {t.kind = 64; break;}
+ {t.kind = 58; break;}
case 34:
- {t.kind = 65; break;}
+ {t.kind = 59; break;}
case 35:
- {t.kind = 66; break;}
+ {t.kind = 60; break;}
case 36:
- {t.kind = 67; break;}
+ {t.kind = 61; break;}
case 37:
- {t.kind = 68; break;}
+ {t.kind = 64; break;}
case 38:
- {t.kind = 70; break;}
+ {t.kind = 65; break;}
case 39:
- {t.kind = 74; break;}
+ {t.kind = 66; break;}
case 40:
- {t.kind = 78; break;}
+ {t.kind = 67; break;}
case 41:
- {t.kind = 79; break;}
+ {t.kind = 68; break;}
case 42:
- {t.kind = 81; break;}
+ {t.kind = 69; break;}
case 43:
- {t.kind = 83; break;}
+ {t.kind = 70; break;}
case 44:
- {t.kind = 85; break;}
+ {t.kind = 72; break;}
case 45:
- {t.kind = 86; break;}
+ {t.kind = 75; break;}
case 46:
- {t.kind = 87; break;}
+ {t.kind = 76; break;}
case 47:
- recEnd = pos; recKind = 10;
- if (ch == '=') {AddCh(); goto case 20;}
- else if (ch == ':') {AddCh(); goto case 45;}
- else {t.kind = 10; break;}
+ {t.kind = 78; break;}
case 48:
- recEnd = pos; recKind = 17;
- if (ch == '=') {AddCh(); goto case 55;}
- else if (ch == ':') {AddCh(); goto case 33;}
- else {t.kind = 17; break;}
+ {t.kind = 82; break;}
case 49:
- recEnd = pos; recKind = 18;
- if (ch == '=') {AddCh(); goto case 31;}
- else {t.kind = 18; break;}
+ {t.kind = 83; break;}
case 50:
- recEnd = pos; recKind = 26;
- if (ch == '|') {AddCh(); goto case 41;}
- else {t.kind = 26; break;}
+ {t.kind = 85; break;}
case 51:
- recEnd = pos; recKind = 29;
- if (ch == '=') {AddCh(); goto case 56;}
- else {t.kind = 29; break;}
+ {t.kind = 87; break;}
case 52:
- if (ch == '|') {AddCh(); goto case 29;}
- else if (ch == '{') {AddCh(); goto case 40;}
- else {goto case 0;}
+ {t.kind = 89; break;}
case 53:
- recEnd = pos; recKind = 73;
- if (ch == '=') {AddCh(); goto case 32;}
- else {t.kind = 73; break;}
+ {t.kind = 90; break;}
case 54:
- recEnd = pos; recKind = 69;
- if (ch == '+') {AddCh(); goto case 37;}
- else {t.kind = 69; break;}
+ {t.kind = 91; break;}
case 55:
- recEnd = pos; recKind = 61;
- if (ch == '=') {AddCh(); goto case 57;}
- else {t.kind = 61; break;}
+ recEnd = pos; recKind = 11;
+ if (ch == '=') {AddCh(); goto case 26;}
+ else if (ch == ':') {AddCh(); goto case 53;}
+ else {t.kind = 11; break;}
case 56:
- recEnd = pos; recKind = 60;
- if (ch == '>') {AddCh(); goto case 23;}
- else {t.kind = 60; break;}
+ recEnd = pos; recKind = 19;
+ if (ch == '=') {AddCh(); goto case 64;}
+ else if (ch == ':') {AddCh(); goto case 39;}
+ else {t.kind = 19; break;}
case 57:
- recEnd = pos; recKind = 54;
- if (ch == '>') {AddCh(); goto case 21;}
- else {t.kind = 54; break;}
+ recEnd = pos; recKind = 20;
+ if (ch == '=') {AddCh(); goto case 37;}
+ else {t.kind = 20; break;}
+ case 58:
+ recEnd = pos; recKind = 28;
+ if (ch == '|') {AddCh(); goto case 49;}
+ else {t.kind = 28; break;}
+ case 59:
+ recEnd = pos; recKind = 31;
+ if (ch == '=') {AddCh(); goto case 65;}
+ else {t.kind = 31; break;}
+ case 60:
+ recEnd = pos; recKind = 44;
+ if (ch == '*') {AddCh(); goto case 46;}
+ else {t.kind = 44; break;}
+ case 61:
+ if (ch == '|') {AddCh(); goto case 35;}
+ else if (ch == '{') {AddCh(); goto case 48;}
+ else {goto case 0;}
+ case 62:
+ recEnd = pos; recKind = 77;
+ if (ch == '=') {AddCh(); goto case 38;}
+ else {t.kind = 77; break;}
+ case 63:
+ recEnd = pos; recKind = 71;
+ if (ch == '+') {AddCh(); goto case 43;}
+ else {t.kind = 71; break;}
+ case 64:
+ recEnd = pos; recKind = 63;
+ if (ch == '=') {AddCh(); goto case 66;}
+ else {t.kind = 63; break;}
+ case 65:
+ recEnd = pos; recKind = 62;
+ if (ch == '>') {AddCh(); goto case 29;}
+ else {t.kind = 62; break;}
+ case 66:
+ recEnd = pos; recKind = 56;
+ if (ch == '>') {AddCh(); goto case 27;}
+ else {t.kind = 56; break;}
}
t.val = new String(tval, 0, tlen);
diff --git a/Source/Core/Util.cs b/Source/Core/Util.cs index f8b8b82b..9a7fec0c 100644 --- a/Source/Core/Util.cs +++ b/Source/Core/Util.cs @@ -486,6 +486,12 @@ namespace Microsoft.Boogie { case Microsoft.Boogie.BinaryOperator.Opcode.Or:
op = " || ";
break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.Pow:
+ op = " ** ";
+ break;
+ case Microsoft.Boogie.BinaryOperator.Opcode.RealDiv:
+ op = " / ";
+ break;
case Microsoft.Boogie.BinaryOperator.Opcode.Sub:
op = " - ";
break;
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 6a2cbb6a..cf125c76 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -115,7 +115,7 @@ namespace Microsoft.Boogie.SMTLib }
sb.Append(']');
TypeToStringHelper(m.Result, sb);
- } else if (t.IsBool || t.IsInt || t.IsBv) {
+ } else if (t.IsBool || t.IsInt || t.IsReal || t.IsBv) {
sb.Append(TypeToString(t));
} else {
System.IO.StringWriter buffer = new System.IO.StringWriter();
@@ -137,6 +137,8 @@ namespace Microsoft.Boogie.SMTLib return "Bool";
else if (t.IsInt)
return "Int";
+ else if (t.IsReal)
+ return "Real";
else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
@@ -181,7 +183,16 @@ namespace Microsoft.Boogie.SMTLib wr.Write("(- 0 {0})", lit.Abs);
else
wr.Write(lit);
- } else {
+ }
+ else if (node is VCExprRealLit) {
+ BigDec lit = ((VCExprRealLit)node).Val;
+ if (lit.IsNegative)
+ // In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
+ wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString(20));
+ else
+ wr.Write(lit.ToDecimalString(20));
+ }
+ else {
Contract.Assert(false);
throw new cce.UnreachableException();
}
@@ -609,13 +620,23 @@ namespace Microsoft.Boogie.SMTLib public bool VisitDivOp(VCExprNAry node, LineariserOptions options)
{
- WriteApplication("int_div", node, options);
+ WriteApplication("div", node, options);
return true;
}
public bool VisitModOp(VCExprNAry node, LineariserOptions options)
{
- WriteApplication("int_mod", node, options);
+ WriteApplication("mod", node, options);
+ return true;
+ }
+
+ public bool VisitRealDivOp(VCExprNAry node, LineariserOptions options) {
+ WriteApplication("/", node, options);
+ return true;
+ }
+
+ public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
+ WriteApplication("real_pow", node, options);
return true;
}
@@ -655,6 +676,16 @@ namespace Microsoft.Boogie.SMTLib return true;
}
+ public bool VisitToIntOp(VCExprNAry node, LineariserOptions options) {
+ WriteApplication("to_int", node, options);
+ return true;
+ }
+
+ public bool VisitToRealOp(VCExprNAry node, LineariserOptions options) {
+ WriteApplication("to_real", node, options);
+ return true;
+ }
+
private string ExtractDatatype(Function func) {
if (func is DatatypeSelector) {
DatatypeSelector selector = (DatatypeSelector) func;
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 5629c0d6..101b07a0 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -22,8 +22,8 @@ namespace Microsoft.Boogie.SMTLib // Core theory:
"and", "or", "not", "iff", "true", "false", "xor", "distinct", "ite", "=", "Bool",
"=>", // implies (sic!)
- // Integers
- "Int", "*", "/", "-", "+", "<", "<=", ">", ">=",
+ // Integers and reals
+ "Int", "Real", "*", "/", "-", "+", "<", "<=", ">", ">=", "div", "mod",
// Bitvectors
"extract", "concat",
"bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",
@@ -48,7 +48,7 @@ namespace Microsoft.Boogie.SMTLib "lblneg", "lblpos", "lbl-lit",
"if", "&&", "||", "equals", "equiv", "bool",
// Boogie-defined
- "int_mod", "int_div", "UOrdering2", "UOrdering3",
+ "real_pow", "UOrdering2", "UOrdering3",
};
static HashSet<string> reservedSmtWords;
diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs index a4bdee51..bff949ea 100644 --- a/Source/Provers/SMTLib/TypeDeclCollector.cs +++ b/Source/Provers/SMTLib/TypeDeclCollector.cs @@ -255,7 +255,7 @@ void ObjectInvariant() return;
}
- if (type.IsBool || type.IsInt || type.IsBv)
+ if (type.IsBool || type.IsInt || type.IsReal || type.IsBv)
return;
CtorType ctorType = type as CtorType;
diff --git a/Source/Provers/Z3api/ContextLayer.cs b/Source/Provers/Z3api/ContextLayer.cs index df40df3d..ad0c2239 100644 --- a/Source/Provers/Z3api/ContextLayer.cs +++ b/Source/Provers/Z3api/ContextLayer.cs @@ -139,8 +139,12 @@ namespace Microsoft.Boogie.Z3 { {
case TermKind.Numeral:
var numstr = arg.GetNumeralString();
- var bignum = Basetypes.BigNum.FromString(numstr);
- res = gen.Integer(bignum);
+ if (arg.GetSort().GetSortKind() == SortKind.Int) {
+ res = gen.Integer(Basetypes.BigNum.FromString(numstr));
+ }
+ else {
+ res = gen.Real(Basetypes.BigDec.FromString(numstr));
+ }
break;
case TermKind.App:
var args = arg.GetAppArgs();
@@ -151,8 +155,14 @@ namespace Microsoft.Boogie.Z3 { switch (arg.GetAppDecl().GetKind())
{
case DeclKind.Add:
- if (vcargs.Length == 0)
- res = gen.Integer(Basetypes.BigNum.FromInt(0));
+ if (vcargs.Length == 0) {
+ if (arg.GetSort().GetSortKind() == SortKind.Int) {
+ res = gen.Integer(Basetypes.BigNum.ZERO);
+ }
+ else {
+ res = gen.Real(Basetypes.BigDec.ZERO);
+ }
+ }
else
{
res = vcargs[0];
@@ -167,7 +177,7 @@ namespace Microsoft.Boogie.Z3 { break;
case DeclKind.Div:
Debug.Assert(vcargs.Length == 2);
- res = gen.Function(VCExpressionGenerator.DivOp, vcargs[0], vcargs[1]);
+ res = gen.Function(VCExpressionGenerator.RealDivOp, vcargs[0], vcargs[1]);
break;
case DeclKind.Eq:
Debug.Assert(vcargs.Length == 2);
@@ -243,8 +253,22 @@ namespace Microsoft.Boogie.Z3 { break;
case DeclKind.Uminus:
Debug.Assert(vcargs.Length == 1);
- var bigzero = Basetypes.BigNum.FromInt(0);
- res = gen.Function(VCExpressionGenerator.SubOp, gen.Integer(bigzero), vcargs[0]);
+ var argzero = null;
+ if (vcargs[0].Type.IsInt) {
+ argzero = gen.Integer(Basetypes.BigNum.ZERO);
+ }
+ else {
+ argzero = gen.Real(Basetypes.BigDec.ZERO);
+ }
+ res = gen.Function(VCExpressionGenerator.SubOp, argzero, vcargs[0]);
+ break;
+ case DeclKind.ToInt:
+ Debug.Assert(vcargs.Length == 1);
+ res = gen.Function(VCExpressionGenerator.ToIntOp, vcargs[0]);
+ break;
+ case DeclKind.ToReal:
+ Debug.Assert(vcargs.Length == 1);
+ res = gen.Function(VCExpressionGenerator.ToRealOp, vcargs[0]);
break;
case DeclKind.Uninterpreted:
var name = arg.GetAppDecl().GetDeclName();
diff --git a/Source/Provers/Z3api/TypeAdapter.cs b/Source/Provers/Z3api/TypeAdapter.cs index e1c6de0b..879211f7 100644 --- a/Source/Provers/Z3api/TypeAdapter.cs +++ b/Source/Provers/Z3api/TypeAdapter.cs @@ -51,7 +51,8 @@ namespace Microsoft.Boogie.Z3 public bool Equals(BasicType x, BasicType y)
{
return (x.IsBool == y.IsBool) &&
- (x.IsInt == y.IsInt);
+ (x.IsInt == y.IsInt) &&
+ (x.IsReal == y.IsReal);
}
public int GetHashCode(BasicType basicType)
@@ -60,6 +61,8 @@ namespace Microsoft.Boogie.Z3 return 1;
else if (basicType.IsInt)
return 2;
+ else if (basicType.IsReal)
+ return 3;
else
throw new Exception("Basic Type " + basicType.ToString() + " is unkwown");
}
@@ -175,6 +178,10 @@ namespace Microsoft.Boogie.Z3 {
typeAst = z3.MkIntSort();
}
+ else if (basicType.IsReal)
+ {
+ typeAst = z3.MkRealSort();
+ }
else
throw new Exception("Unknown Basic Type " + basicType.ToString());
return typeAst;
diff --git a/Source/Provers/Z3api/VCExprVisitor.cs b/Source/Provers/Z3api/VCExprVisitor.cs index 0605a854..e56a7950 100644 --- a/Source/Provers/Z3api/VCExprVisitor.cs +++ b/Source/Provers/Z3api/VCExprVisitor.cs @@ -15,6 +15,8 @@ using Microsoft.Z3; namespace Microsoft.Boogie.Z3
{
+ using System.Numerics.BigInteger;
+
public class Z3apiExprLineariser : IVCExprVisitor<Term, LineariserOptions>
{
private Z3apiOpLineariser opLineariser = null;
@@ -110,7 +112,7 @@ namespace Microsoft.Boogie.Z3 return z3.MkSub(unwrapChildren);
}
- if (op == VCExpressionGenerator.DivOp) {
+ if (op == VCExpressionGenerator.DivOp || op == VCExpressionGenerator.RealDivOp) {
return z3.MkDiv(unwrapChildren[0], unwrapChildren[1]);
}
@@ -126,6 +128,14 @@ namespace Microsoft.Boogie.Z3 return z3.MkIte(unwrapChildren[0], unwrapChildren[1], unwrapChildren[2]);
}
+ if (op == VCExpressionGenerator.ToIntOp) {
+ return z3.MkToInt(unwrapChildren[0]);
+ }
+
+ if (op == VCExpressionGenerator.ToRealOp) {
+ return z3.MkToReal(unwrapChildren[0]);
+ }
+
throw new Exception("unhandled boogie operator");
}
@@ -139,11 +149,25 @@ namespace Microsoft.Boogie.Z3 else if (node == VCExpressionGenerator.False)
return cm.z3.MkFalse();
else if (node is VCExprIntLit)
- return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());
- else
- {
- Contract.Assert(false);
- throw new cce.UnreachableException();
+ return cm.z3.MkNumeral(((VCExprIntLit)node).Val.ToInt, cm.z3.MkIntSort());
+ else if (node is VCExprRealLit) {
+ string m = ((VCExprRealLit)node).Val.Mantissa.ToString();
+ BigInteger e = ((VCExprRealLit)node).Val.Exponent;
+ string f = BigInteger.Pow(10, e.Abs);
+
+ if (e == 0) {
+ return cm.z3.MkNumeral(m, cm.z3.MkRealSort());
+ }
+ else if (((VCExprRealLit)node).Val.Exponent > 0) {
+ return cm.z3.MkMul(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));
+ }
+ else {
+ return cm.z3.MkDiv(cm.z3.MkNumeral(m, cm.z3.MkRealSort()), cm.z3.MkNumeral(f, cm.z3.MkRealSort()));
+ }
+ }
+ else {
+ Contract.Assert(false);
+ throw new cce.UnreachableException();
}
}
@@ -548,6 +572,18 @@ namespace Microsoft.Boogie.Z3 return WriteApplication(node.Op, node, options);
}
+ public Term VisitRealDivOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
+ }
+
+ public Term VisitPowOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
+ }
+
public Term VisitLtOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
@@ -590,6 +626,18 @@ namespace Microsoft.Boogie.Z3 return WriteApplication(node.Op, node, options);
}
+ public Term VisitToIntOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
+ }
+
+ public Term VisitToRealOp(VCExprNAry node, LineariserOptions options) {
+ Contract.Requires(options != null);
+ Contract.Requires(node != null);
+ return WriteApplication(node.Op, node, options);
+ }
+
public Term VisitBoogieFunctionOp(VCExprNAry node, LineariserOptions options)
{
Contract.Requires(options != null);
diff --git a/Source/VCExpr/BigLiteralAbstracter.cs b/Source/VCExpr/BigLiteralAbstracter.cs index 7eb93541..879ab6d6 100644 --- a/Source/VCExpr/BigLiteralAbstracter.cs +++ b/Source/VCExpr/BigLiteralAbstracter.cs @@ -120,7 +120,7 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Ensures(Contract.Result<VCExpr>() != null);
if (lit.IsNegative)
- return Gen.Function(VCExpressionGenerator.SubOp,
+ return Gen.Function(VCExpressionGenerator.SubIOp,
Gen.Integer(BigNum.ZERO), RepresentPos(lit.Neg));
else
return RepresentPos(lit);
@@ -145,7 +145,7 @@ namespace Microsoft.Boogie.VCExprAST { BigNum dist = lit - Literals[index - 1].Key;
if (dist < resDistance) {
resDistance = dist;
- res = Gen.Function(VCExpressionGenerator.AddOp,
+ res = Gen.Function(VCExpressionGenerator.AddIOp,
Literals[index - 1].Value, Gen.Integer(dist));
}
}
@@ -154,7 +154,7 @@ namespace Microsoft.Boogie.VCExprAST { BigNum dist = Literals[index].Key - lit;
if (dist < resDistance) {
resDistance = dist;
- res = Gen.Function(VCExpressionGenerator.SubOp,
+ res = Gen.Function(VCExpressionGenerator.SubIOp,
Literals[index].Value, Gen.Integer(dist));
}
}
@@ -198,7 +198,7 @@ namespace Microsoft.Boogie.VCExprAST { Contract.Requires(bExpr != null);
BigNum dist = bValue - aValue;
- VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubOp, bExpr, aExpr);
+ VCExpr distExpr = Gen.Function(VCExpressionGenerator.SubIOp, bExpr, aExpr);
if (dist <= ConstantDistanceTPO)
// constants that are sufficiently close to each other are put
// into a precise relationship
diff --git a/Source/VCExpr/Boogie2VCExpr.cs b/Source/VCExpr/Boogie2VCExpr.cs index 1561aec0..3035c9de 100644 --- a/Source/VCExpr/Boogie2VCExpr.cs +++ b/Source/VCExpr/Boogie2VCExpr.cs @@ -328,6 +328,8 @@ namespace Microsoft.Boogie.VCExprAST { }
} else if (node.Val is BigNum) {
return Gen.Integer(node.asBigNum);
+ } else if (node.Val is BigDec) {
+ return Gen.Real(node.asBigDec);
} else if (node.Val is BvConst) {
return Gen.Bitvector((BvConst)node.Val);
} else {
@@ -961,8 +963,20 @@ namespace Microsoft.Boogie.VCExprAST { public VCExpr Visit(UnaryOperator unaryOperator) {
//Contract.Requires(unaryOperator != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Not && this.args.Count == 1);
- return Gen.Not(this.args);
+ Contract.Assert(unaryOperator.Op == UnaryOperator.Opcode.Neg || unaryOperator.Op == UnaryOperator.Opcode.Not);
+ Contract.Assert(this.args.Count == 1);
+ if (unaryOperator.Op == UnaryOperator.Opcode.Neg) {
+ VCExpr e = cce.NonNull(this.args[0]);
+ if (cce.NonNull(e.Type).IsInt) {
+ return Gen.Function(VCExpressionGenerator.SubIOp, Gen.Integer(BigNum.ZERO), e);
+ }
+ else {
+ return Gen.Function(VCExpressionGenerator.SubROp, Gen.Real(BigDec.ZERO), e);
+ }
+ }
+ else {
+ return Gen.Not(this.args);
+ }
}
public VCExpr Visit(BinaryOperator binaryOperator) {
@@ -996,6 +1010,21 @@ namespace Microsoft.Boogie.VCExprAST { return this.args[0];
}
+ public VCExpr Visit(ArithmeticCoercion arithCoercion) {
+ //Contract.Requires(arithCoercion != null);
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ Contract.Assert(this.args.Count == 1);
+ switch (arithCoercion.Coercion) {
+ case ArithmeticCoercion.CoercionType.ToInt:
+ return Gen.Function(VCExpressionGenerator.ToIntOp, this.args);
+ case ArithmeticCoercion.CoercionType.ToReal:
+ return Gen.Function(VCExpressionGenerator.ToRealOp, this.args);
+ default:
+ Contract.Assert(false);
+ return null;
+ }
+ }
+
public VCExpr Visit(IfThenElse ite) {
//Contract.Requires(ite != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
@@ -1012,15 +1041,42 @@ namespace Microsoft.Boogie.VCExprAST { switch (app.Op) {
case BinaryOperator.Opcode.Add:
- return Gen.Function(VCExpressionGenerator.AddOp, args);
+ if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ return Gen.Function(VCExpressionGenerator.AddIOp, args);
+ }
+ else {
+ return Gen.Function(VCExpressionGenerator.AddROp, args);
+ }
case BinaryOperator.Opcode.Sub:
- return Gen.Function(VCExpressionGenerator.SubOp, args);
+ if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ return Gen.Function(VCExpressionGenerator.SubIOp, args);
+ }
+ else {
+ return Gen.Function(VCExpressionGenerator.SubROp, args);
+ }
case BinaryOperator.Opcode.Mul:
- return Gen.Function(VCExpressionGenerator.MulOp, args);
+ if (cce.NonNull(cce.NonNull(args[0]).Type).IsInt) {
+ return Gen.Function(VCExpressionGenerator.MulIOp, args);
+ }
+ else {
+ return Gen.Function(VCExpressionGenerator.MulROp, args);
+ }
case BinaryOperator.Opcode.Div:
- return Gen.Function(VCExpressionGenerator.DivOp, args);
+ return Gen.Function(VCExpressionGenerator.DivIOp, args);
case BinaryOperator.Opcode.Mod:
return Gen.Function(VCExpressionGenerator.ModOp, args);
+ case BinaryOperator.Opcode.RealDiv:
+ VCExpr arg0 = cce.NonNull(args[0]);
+ VCExpr arg1 = cce.NonNull(args[1]);
+ if (cce.NonNull(arg0.Type).IsInt) {
+ arg0 = Gen.Function(VCExpressionGenerator.ToRealOp, arg0);
+ }
+ if (cce.NonNull(arg1.Type).IsInt) {
+ arg1 = Gen.Function(VCExpressionGenerator.ToRealOp, arg1);
+ }
+ return Gen.Function(VCExpressionGenerator.DivROp, arg0, arg1);
+ case BinaryOperator.Opcode.Pow:
+ return Gen.Function(VCExpressionGenerator.PowOp, args);
case BinaryOperator.Opcode.Eq:
case BinaryOperator.Opcode.Iff:
// we don't distinguish between equality and equivalence at this point
diff --git a/Source/VCExpr/SimplifyLikeLineariser.cs b/Source/VCExpr/SimplifyLikeLineariser.cs index 848fafcb..02e3adda 100644 --- a/Source/VCExpr/SimplifyLikeLineariser.cs +++ b/Source/VCExpr/SimplifyLikeLineariser.cs @@ -376,6 +376,13 @@ namespace Microsoft.Boogie.VCExprAST { internal const string intMulName = "*";
internal const string intDivName = "/";
internal const string intModName = "%";
+ internal const string realAddName = "realAdd";
+ internal const string realSubName = "realSub";
+ internal const string realMulName = "realMul";
+ internal const string realDivName = "realDiv";
+ internal const string realPowName = "realPow";
+ internal const string toIntName = "toIntCoercion";
+ internal const string toRealName = "toRealCoercion";
internal void AssertAsTerm(string x, LineariserOptions options) {
Contract.Requires(options != null);
@@ -928,10 +935,16 @@ namespace Microsoft.Boogie.VCExprAST { public bool VisitAddOp(VCExprNAry node, LineariserOptions options) {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
- if (CommandLineOptions.Clo.ReflectAdd) {
- WriteTermApplication(intAddNameReflect, node, options);
- } else {
- WriteTermApplication(intAddName, node, options);
+ if (node.Type.IsInt) {
+ if (CommandLineOptions.Clo.ReflectAdd) {
+ WriteTermApplication(intAddNameReflect, node, options);
+ }
+ else {
+ WriteTermApplication(intAddName, node, options);
+ }
+ }
+ else {
+ WriteTermApplication(realAddName, node, options);
}
return true;
}
@@ -939,14 +952,24 @@ namespace Microsoft.Boogie.VCExprAST { public bool VisitSubOp(VCExprNAry node, LineariserOptions options) {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
- WriteTermApplication(intSubName, node, options);
+ if (node.Type.IsInt) {
+ WriteTermApplication(intSubName, node, options);
+ }
+ else {
+ WriteTermApplication(realSubName, node, options);
+ }
return true;
}
public bool VisitMulOp(VCExprNAry node, LineariserOptions options) {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
- WriteTermApplication(intMulName, node, options);
+ if (node.Type.IsInt) {
+ WriteTermApplication(intMulName, node, options);
+ }
+ else {
+ WriteTermApplication(realMulName, node, options);
+ }
return true;
}
@@ -964,6 +987,20 @@ namespace Microsoft.Boogie.VCExprAST { return true;
}
+ public bool VisitRealDivOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(realDivName, node, options);
+ return true;
+ }
+
+ public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteTermApplication(realPowName, node, options);
+ return true;
+ }
+
public bool VisitLtOp(VCExprNAry node, LineariserOptions options) {
//Contract.Requires(options != null);
//Contract.Requires(node != null);
@@ -1006,6 +1043,20 @@ namespace Microsoft.Boogie.VCExprAST { return true;
}
+ public bool VisitToIntOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteApplication(toIntName, node, options);
+ return true;
+ }
+
+ public bool VisitToRealOp(VCExprNAry node, LineariserOptions options) {
+ //Contract.Requires(options != null);
+ //Contract.Requires(node != null);
+ WriteApplication(toRealName, node, options);
+ return true;
+ }
+
public bool VisitBoogieFunctionOp(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 fb91d326..9d366c9f 100644 --- a/Source/VCExpr/TypeErasure.cs +++ b/Source/VCExpr/TypeErasure.cs @@ -524,6 +524,7 @@ namespace Microsoft.Boogie.TypeErasure { public virtual void Setup() {
GetBasicTypeRepr(Type.Int);
+ GetBasicTypeRepr(Type.Real);
GetBasicTypeRepr(Type.Bool);
}
@@ -625,6 +626,7 @@ namespace Microsoft.Boogie.TypeErasure { base.Setup();
GetTypeCasts(Type.Int);
+ GetTypeCasts(Type.Real);
GetTypeCasts(Type.Bool);
}
@@ -730,7 +732,7 @@ namespace Microsoft.Boogie.TypeErasure { ////////////////////////////////////////////////////////////////////////////
// the only types that we allow in "untyped" expressions are U,
- // Type.Int, and Type.Bool
+ // Type.Int, Type.Real, and Type.Bool
public override Type TypeAfterErasure(Type type) {
//Contract.Requires(type != null);
@@ -746,7 +748,7 @@ namespace Microsoft.Boogie.TypeErasure { [Pure]
public override bool UnchangedType(Type type) {
//Contract.Requires(type != null);
- return type.IsInt || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
+ return type.IsInt || type.IsReal || type.IsBool || type.IsBv || (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays);
}
public VCExpr Cast(VCExpr expr, Type toType) {
@@ -1143,7 +1145,7 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires(bindings != null);
Contract.Requires(node != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int);
+ Contract.Assume(node.Type == Type.Bool || node.Type == Type.Int || node.Type == Type.Real);
return node;
}
@@ -1360,7 +1362,7 @@ namespace Microsoft.Boogie.TypeErasure { }
// Cast the arguments of the node to their old type if necessary and possible; otherwise use
- // their new type (int, bool, or U)
+ // their new type (int, real, bool, or U)
private VCExpr CastArgumentsToOldType(VCExprNAry node, VariableBindings bindings, int newPolarity) {
Contract.Requires(bindings != null);
Contract.Requires(node != null);
@@ -1448,19 +1450,19 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Requires((bindings != null));
Contract.Requires((node != null));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return CastArguments(node, Type.Int, bindings, 0);
+ return CastArguments(node, node.Type, bindings, 0);
}
public override VCExpr VisitSubOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return CastArguments(node, Type.Int, bindings, 0);
+ return CastArguments(node, node.Type, bindings, 0);
}
public override VCExpr VisitMulOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return CastArguments(node, Type.Int, bindings, 0);
+ return CastArguments(node, node.Type, bindings, 0);
}
public override VCExpr VisitDivOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
@@ -1474,29 +1476,41 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, Type.Int, bindings, 0);
}
+ public override VCExpr VisitRealDivOp(VCExprNAry node, VariableBindings bindings) {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArguments(node, Type.Real, bindings, 0);
+ }
+ public override VCExpr VisitPowOp(VCExprNAry node, VariableBindings bindings) {
+ Contract.Requires((bindings != null));
+ Contract.Requires((node != null));
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+ return CastArguments(node, Type.Real, bindings, 0);
+ }
public override VCExpr VisitLtOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return CastArguments(node, Type.Int, bindings, 0);
+ return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitLeOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return CastArguments(node, Type.Int, bindings, 0);
+ return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitGtOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return CastArguments(node, Type.Int, bindings, 0);
+ return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitGeOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
Contract.Requires((node != null));
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return CastArguments(node, Type.Int, bindings, 0);
+ return CastArgumentsToOldType(node, bindings, 0);
}
public override VCExpr VisitSubtypeOp(VCExprNAry node, VariableBindings bindings) {
Contract.Requires((bindings != null));
@@ -1504,6 +1518,18 @@ namespace Microsoft.Boogie.TypeErasure { Contract.Ensures(Contract.Result<VCExpr>() != null);
return CastArguments(node, AxBuilder.U, bindings, 0);
}
+ public override VCExpr VisitToIntOp(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 VisitToRealOp(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 38541881..fcfd0041 100644 --- a/Source/VCExpr/VCExprAST.cs +++ b/Source/VCExpr/VCExprAST.cs @@ -49,6 +49,12 @@ namespace Microsoft.Boogie { return new VCExprIntLit(x);
}
+ public VCExpr/*!*/ Real(BigDec x) {
+ Contract.Ensures(Contract.Result<VCExpr>() != null);
+
+ return new VCExprRealLit(x);
+ }
+
public VCExpr/*!*/ Function(VCExprOp/*!*/ op,
List<VCExpr/*!*/>/*!*/ arguments,
List<Type/*!*/>/*!*/ typeArguments) {
@@ -199,7 +205,8 @@ namespace Microsoft.Boogie { Contract.Requires(e1 != null);
Contract.Ensures(Contract.Result<VCExpr>() != null);
- return Function(AddOp, e0, e1);
+ VCExprOp op = cce.NonNull(cce.NonNull(e0).Type).IsInt ? AddIOp : AddROp;
+ return Function(op, e0, e1);
}
public VCExpr/*!*/ Or(VCExpr/*!*/ e0, VCExpr/*!*/ e1) {
Contract.Requires(e0 != null);
@@ -308,11 +315,16 @@ namespace Microsoft.Boogie { ////////////////////////////////////////////////////////////////////////////////
// Further operators
- public static readonly VCExprOp AddOp = new VCExprNAryOp(2, Type.Int);
- public static readonly VCExprOp SubOp = new VCExprNAryOp(2, Type.Int);
- public static readonly VCExprOp MulOp = new VCExprNAryOp(2, Type.Int);
- public static readonly VCExprOp DivOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp AddIOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp AddROp = new VCExprNAryOp(2, Type.Real);
+ public static readonly VCExprOp SubIOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp SubROp = new VCExprNAryOp(2, Type.Real);
+ public static readonly VCExprOp MulIOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp MulROp = new VCExprNAryOp(2, Type.Real);
+ public static readonly VCExprOp DivIOp = new VCExprNAryOp(2, Type.Int);
+ public static readonly VCExprOp DivROp = new VCExprNAryOp(2, Type.Real);
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);
public static readonly VCExprOp LeOp = new VCExprNAryOp(2, Type.Bool);
public static readonly VCExprOp GtOp = new VCExprNAryOp(2, Type.Bool);
@@ -322,6 +334,8 @@ namespace Microsoft.Boogie { // the type of the compared terms
public static readonly VCExprOp Subtype3Op = new VCExprNAryOp(3, Type.Bool);
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 TickleBoolOp = new VCExprCustomOp("tickleBool", 1, Type.Bool);
@@ -376,13 +390,17 @@ namespace Microsoft.Boogie { MulOp,
DivOp,
ModOp,
+ RealDivOp,
+ PowOp,
LtOp,
LeOp,
GtOp,
GeOp,
SubtypeOp,
Subtype3Op,
- BvConcatOp
+ BvConcatOp,
+ ToIntOp,
+ ToRealOp
};
internal static Dictionary<VCExprOp/*!*/, SingletonOp>/*!*/ SingletonOpDict;
[ContractInvariantMethod]
@@ -399,17 +417,24 @@ namespace Microsoft.Boogie { SingletonOpDict.Add(AndOp, SingletonOp.AndOp);
SingletonOpDict.Add(OrOp, SingletonOp.OrOp);
SingletonOpDict.Add(ImpliesOp, SingletonOp.ImpliesOp);
- SingletonOpDict.Add(AddOp, SingletonOp.AddOp);
- SingletonOpDict.Add(SubOp, SingletonOp.SubOp);
- SingletonOpDict.Add(MulOp, SingletonOp.MulOp);
- SingletonOpDict.Add(DivOp, SingletonOp.DivOp);
+ SingletonOpDict.Add(AddIOp, SingletonOp.AddOp);
+ SingletonOpDict.Add(AddROp, SingletonOp.AddOp);
+ SingletonOpDict.Add(SubIOp, SingletonOp.SubOp);
+ SingletonOpDict.Add(SubROp, SingletonOp.SubOp);
+ SingletonOpDict.Add(MulIOp, SingletonOp.MulOp);
+ SingletonOpDict.Add(MulROp, SingletonOp.MulOp);
+ SingletonOpDict.Add(DivIOp, SingletonOp.DivOp);
+ SingletonOpDict.Add(DivROp, SingletonOp.RealDivOp);
SingletonOpDict.Add(ModOp, SingletonOp.ModOp);
+ SingletonOpDict.Add(PowOp, SingletonOp.PowOp);
SingletonOpDict.Add(LtOp, SingletonOp.LtOp);
SingletonOpDict.Add(LeOp, SingletonOp.LeOp);
SingletonOpDict.Add(GtOp, SingletonOp.GtOp);
SingletonOpDict.Add(GeOp, SingletonOp.GeOp);
SingletonOpDict.Add(SubtypeOp, SingletonOp.SubtypeOp);
SingletonOpDict.Add(Subtype3Op, SingletonOp.Subtype3Op);
+ SingletonOpDict.Add(ToIntOp, SingletonOp.ToIntOp);
+ SingletonOpDict.Add(ToRealOp, SingletonOp.ToRealOp);
}
////////////////////////////////////////////////////////////////////////////////
@@ -810,6 +835,27 @@ namespace Microsoft.Boogie.VCExprAST { }
}
+ public class VCExprRealLit : VCExprLiteral {
+ public readonly BigDec Val;
+ internal VCExprRealLit(BigDec val)
+ : base(Type.Real) {
+ this.Val = val;
+ }
+ [Pure]
+ [Reads(ReadsAttribute.Reads.Nothing)]
+ public override bool Equals(object that) {
+ if (Object.ReferenceEquals(this, that))
+ return true;
+ if (that is VCExprRealLit)
+ return Val == ((VCExprRealLit)that).Val;
+ return false;
+ }
+ [Pure]
+ public override int GetHashCode() {
+ return Val.GetHashCode() * 72321;
+ }
+ }
+
/////////////////////////////////////////////////////////////////////////////////
// Operator expressions with fixed arity
[ContractClassFor(typeof(VCExprNAry))]
@@ -1218,6 +1264,10 @@ namespace Microsoft.Boogie.VCExprAST { return visitor.VisitDivOp(expr, arg);
case VCExpressionGenerator.SingletonOp.ModOp:
return visitor.VisitModOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.RealDivOp:
+ return visitor.VisitRealDivOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.PowOp:
+ return visitor.VisitPowOp(expr, arg);
case VCExpressionGenerator.SingletonOp.LtOp:
return visitor.VisitLtOp(expr, arg);
case VCExpressionGenerator.SingletonOp.LeOp:
@@ -1232,6 +1282,10 @@ namespace Microsoft.Boogie.VCExprAST { return visitor.VisitSubtype3Op(expr, arg);
case VCExpressionGenerator.SingletonOp.BvConcatOp:
return visitor.VisitBvConcatOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.ToIntOp:
+ return visitor.VisitToIntOp(expr, arg);
+ case VCExpressionGenerator.SingletonOp.ToRealOp:
+ return visitor.VisitToRealOp(expr, arg);
default:
Contract.Assert(false);
throw new cce.UnreachableException();
diff --git a/Source/VCExpr/VCExprASTPrinter.cs b/Source/VCExpr/VCExprASTPrinter.cs index adb3b27e..00e6fb9c 100644 --- a/Source/VCExpr/VCExprASTPrinter.cs +++ b/Source/VCExpr/VCExprASTPrinter.cs @@ -290,12 +290,22 @@ namespace Microsoft.Boogie.VCExprAST { public bool VisitDivOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
- return PrintNAry("/", node, wr);
+ return PrintNAry("div", node, wr);
}
public bool VisitModOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
//Contract.Requires(node != null);
- return PrintNAry("%", node, wr);
+ return PrintNAry("mod", node, wr);
+ }
+ public bool VisitRealDivOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("/", node, wr);
+ }
+ public bool VisitPowOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("**", node, wr);
}
public bool VisitLtOp(VCExprNAry node, TextWriter wr) {
//Contract.Requires(wr != null);
@@ -327,6 +337,16 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null);
return PrintNAry("<::", node, wr);
}
+ public bool VisitToIntOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("int", node, wr);
+ }
+ public bool VisitToRealOp(VCExprNAry node, TextWriter wr) {
+ //Contract.Requires(wr != null);
+ //Contract.Requires(node != null);
+ return PrintNAry("real", 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 1a29bbeb..1dd1cac9 100644 --- a/Source/VCExpr/VCExprASTVisitors.cs +++ b/Source/VCExpr/VCExprASTVisitors.cs @@ -75,12 +75,16 @@ namespace Microsoft.Boogie.VCExprAST { Result VisitMulOp(VCExprNAry node, Arg arg);
Result VisitDivOp(VCExprNAry node, Arg arg);
Result VisitModOp(VCExprNAry node, Arg arg);
+ Result VisitRealDivOp(VCExprNAry node, Arg arg);
+ Result VisitPowOp(VCExprNAry node, Arg arg);
Result VisitLtOp(VCExprNAry node, Arg arg);
Result VisitLeOp(VCExprNAry node, Arg arg);
Result VisitGtOp(VCExprNAry node, Arg arg);
Result VisitGeOp(VCExprNAry node, Arg arg);
Result VisitSubtypeOp(VCExprNAry node, Arg arg);
Result VisitSubtype3Op(VCExprNAry node, Arg arg);
+ Result VisitToIntOp(VCExprNAry node, Arg arg);
+ Result VisitToRealOp(VCExprNAry node, Arg arg);
Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg);
Result VisitIfThenElseOp(VCExprNAry node, Arg arg);
Result VisitCustomOp(VCExprNAry node, Arg arg);
@@ -179,6 +183,16 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException();
}
+ public Result VisitRealDivOp(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();
+ }
+
public Result VisitLtOp(VCExprNAry node, Arg arg) {
Contract.Requires(node != null);
throw new NotImplementedException();
@@ -209,6 +223,16 @@ namespace Microsoft.Boogie.VCExprAST { throw new NotImplementedException();
}
+ public Result VisitToIntOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
+ public Result VisitToRealOp(VCExprNAry node, Arg arg) {
+ Contract.Requires(node != null);
+ throw new NotImplementedException();
+ }
+
public Result VisitBoogieFunctionOp(VCExprNAry node, Arg arg) {
Contract.Requires(node != null);
throw new NotImplementedException();
@@ -1427,6 +1451,14 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null);
return StandardResult(node, arg);
}
+ public virtual Result VisitRealDivOp(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);
+ }
public virtual Result VisitLtOp(VCExprNAry node, Arg arg) {
//Contract.Requires(node != null);
return StandardResult(node, arg);
@@ -1451,6 +1483,14 @@ namespace Microsoft.Boogie.VCExprAST { //Contract.Requires(node != null);
return StandardResult(node, arg);
}
+ public virtual Result VisitToIntOp(VCExprNAry node, Arg arg) {
+ //Contract.Requires(node != null);
+ return StandardResult(node, arg);
+ }
+ public virtual Result VisitToRealOp(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);
diff --git a/Test/aitest1/Answer b/Test/aitest1/Answer index dd5bcff2..bfe185e7 100644 --- a/Test/aitest1/Answer +++ b/Test/aitest1/Answer @@ -268,7 +268,7 @@ implementation p() A:
assume {:inferred} true;
- assume 0 - 1 <= x;
+ assume -1 <= x;
assume {:inferred} -1 <= x;
goto B, E;
diff --git a/Test/inline/Answer b/Test/inline/Answer index 655143fa..eddeb64f 100644 --- a/Test/inline/Answer +++ b/Test/inline/Answer @@ -566,7 +566,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in var b: bool;
anon0:
- ret := 0 - 1;
+ ret := -1;
b := false;
found := b;
i := 0;
@@ -659,7 +659,7 @@ implementation main(x: int) goto inline$find$0$anon0;
inline$find$0$anon0:
- inline$find$0$ret := 0 - 1;
+ inline$find$0$ret := -1;
inline$find$0$b := false;
inline$find$0$found := inline$find$0$b;
inline$find$0$i := 0;
@@ -756,7 +756,7 @@ implementation {:inline 1} find(A: [int]int, size: int, x: int) returns (ret: in var inline$check$0$ret: bool;
anon0:
- ret := 0 - 1;
+ ret := -1;
b := false;
found := b;
i := 0;
diff --git a/Test/test0/Answer b/Test/test0/Answer index d57e7647..0eda9e2e 100644 --- a/Test/test0/Answer +++ b/Test/test0/Answer @@ -34,6 +34,12 @@ const y: int; const z: int;
+const r: real;
+
+const s: real;
+
+const t: real;
+
const P: bool;
const Q: bool;
@@ -56,6 +62,36 @@ axiom x + y mod z == y mod z + x; axiom (x + y) mod z == x mod z + y mod z;
+axiom x / y / z == x / (y / z);
+
+axiom x / y / (z / x) == x / y / z;
+
+axiom x / s / z == x / (s / z);
+
+axiom x / s / (z / x) == x / s / z;
+
+axiom r / s / t == r / (s / t);
+
+axiom r / s / (t / r) == r / s / t;
+
+axiom r * s / t == r * s / t;
+
+axiom r / s * t == r / s * t;
+
+axiom (r * s) ** t == r ** t * s ** t;
+
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+
+axiom r >= 0e0 ==> real(int(r)) <= r;
+
+axiom int(0e0 - 2e-2) == 0;
+
+axiom int(0e0 - 35e0) == -35;
+
+axiom int(27e-1) == 2;
+
axiom x - y - z == x - (y - z);
axiom x - y - (z - x) == x - y - z;
diff --git a/Test/test0/ModifiedBag.bpl b/Test/test0/ModifiedBag.bpl index cb69aa5f..5fffc20a 100644 --- a/Test/test0/ModifiedBag.bpl +++ b/Test/test0/ModifiedBag.bpl @@ -1,5 +1,5 @@ // ----------- BEGIN PRELUDE
-type real;
+
type elements;
diff --git a/Test/test0/PrettyPrint.bpl b/Test/test0/PrettyPrint.bpl index 955faad8..7e4a9ce7 100644 --- a/Test/test0/PrettyPrint.bpl +++ b/Test/test0/PrettyPrint.bpl @@ -1,6 +1,9 @@ const x: int;
const y: int;
const z: int;
+const r: real;
+const s: real;
+const t: real;
const P: bool;
const Q: bool;
const R: bool;
@@ -17,6 +20,25 @@ axiom (x div y) div (z div x) == (x div y) div z; axiom x + y mod z == ((y mod z) + x);
axiom (x + y) mod z == (x mod z) + (y mod z);
+axiom x / y / z == (x / (y / z));
+axiom (x / y) / (z / x) == (x / y) / z;
+axiom x / s / z == (x / (s / z));
+axiom (x / s) / (z / x) == (x / s) / z;
+axiom r / s / t == (r / (s / t));
+axiom (r / s) / (t / r) == (r / s) / t;
+
+axiom ((r * s) / t) == r * s / t;
+axiom ((r / s) * t) == (r / s) * t;
+
+axiom (r * s) ** t == (r ** t) * (s ** t);
+axiom r ** (s + t) == r ** s * r ** t;
+
+axiom int(real(x)) == x;
+axiom r >= 0.0 ==> real(int(r)) <= r;
+axiom int(0e-3 - 0.02) == 0;
+axiom int(0e2 - 3.5e1) == -35;
+axiom int(27e-1) == 2;
+
axiom x - y - z == (x - (y - z));
axiom (x - y) - (z - x) == (x - y) - z;
diff --git a/Test/test0/Prog0.bpl b/Test/test0/Prog0.bpl index ac87476f..79a4d2ab 100644 --- a/Test/test0/Prog0.bpl +++ b/Test/test0/Prog0.bpl @@ -1,5 +1,5 @@ // BoogiePL Examples
-type real;
+
type elements;
var x:int; var y:real; var z:ref; // Variables
diff --git a/Test/test1/Answer b/Test/test1/Answer index a8b73b53..94bf2d9a 100644 --- a/Test/test1/Answer +++ b/Test/test1/Answer @@ -145,3 +145,22 @@ Lambda.bpl(12,8): Error: the type variable T does not occur in types of the lamb Lambda.bpl(12,2): Error: mismatched types in assignment command (cannot assign <T>[int]int to [int]int)
Lambda.bpl(18,27): Error: invalid argument types (bool and int) to binary operator +
5 type checking errors detected in Lambda.bpl
+IntReal.bpl(5,8): Error: invalid argument types (int and real) to binary operator >=
+IntReal.bpl(6,8): Error: invalid argument types (int and real) to binary operator <=
+IntReal.bpl(7,8): Error: invalid argument types (int and real) to binary operator <
+IntReal.bpl(8,8): Error: invalid argument types (int and real) to binary operator >
+IntReal.bpl(10,9): Error: invalid argument types (int and real) to binary operator ==
+IntReal.bpl(11,8): Error: invalid argument types (int and real) to binary operator +
+IntReal.bpl(12,8): Error: invalid argument types (int and real) to binary operator -
+IntReal.bpl(13,8): Error: invalid argument types (int and real) to binary operator *
+IntReal.bpl(14,8): Error: invalid argument types (int and real) to binary operator div
+IntReal.bpl(15,8): Error: invalid argument types (int and real) to binary operator mod
+IntReal.bpl(17,12): Error: invalid argument types (real and int) to binary operator ==
+IntReal.bpl(23,8): Error: invalid argument types (int and real) to binary operator **
+IntReal.bpl(27,14): Error: invalid argument types (real and int) to binary operator ==
+IntReal.bpl(29,13): Error: invalid argument types (int and real) to binary operator ==
+IntReal.bpl(32,6): Error: argument type int does not match expected type real
+IntReal.bpl(33,6): Error: argument type real does not match expected type int
+IntReal.bpl(45,8): Error: invalid argument types (real and int) to binary operator div
+IntReal.bpl(46,8): Error: invalid argument types (real and int) to binary operator mod
+18 type checking errors detected in IntReal.bpl
\ No newline at end of file diff --git a/Test/test1/IntReal.bpl b/Test/test1/IntReal.bpl new file mode 100644 index 00000000..fac41d57 --- /dev/null +++ b/Test/test1/IntReal.bpl @@ -0,0 +1,48 @@ +const i: int;
+const r: real;
+
+axiom i == 0;
+axiom i >= 0.0; // type errror
+axiom i <= 0.0e0; // type errror
+axiom i < 0.0e-0; // type errror
+axiom i > 0.0e20; // type errror
+
+axiom -i == r; // type errror
+axiom i + r == 0.0; // type errror
+axiom i - r == 0.0; // type errror
+axiom i * r == 0.0; // type errror
+axiom i div r == 0; // type errror
+axiom i mod r == 0; // type errror
+
+axiom i / i == 0; // type errror
+axiom i / i == 0.0;
+axiom i / r == 0.0;
+axiom r / i == 0.0;
+axiom r / r == 0.0;
+
+axiom i ** r == 0.0; // type errror
+axiom r ** r == 0.0;
+
+axiom real(i) == 0.0;
+axiom real(i) == i; // type errror
+axiom int(r) == 0;
+axiom int(r) == r; // type errror
+axiom int(real(i)) == i;
+axiom real(int(r)) == r;
+axiom int(int(r)) == i; // type errror
+axiom real(real(i)) == r; // type errror
+
+axiom i == 0;
+axiom real(i) >= 0.0;
+axiom real(i) <= 0.0e0;
+axiom r < 0.0e-0;
+axiom r > 0.0e20;
+
+axiom -r == real(i);
+axiom real(i) + r == 0.0;
+axiom r - real(0) == 0.0;
+axiom r * r == 0.0;
+axiom r div 0 == 0; // type errror
+axiom r mod 0 == 0; // type errror
+
+axiom r ** r == 0.0;
diff --git a/Test/test1/runtest.bat b/Test/test1/runtest.bat index 979c36e4..149e6dc9 100644 --- a/Test/test1/runtest.bat +++ b/Test/test1/runtest.bat @@ -19,3 +19,4 @@ rem set BGEXE=mono ..\..\Binaries\Boogie.exe %BGEXE% %* /noVerify FunBody.bpl
%BGEXE% %* /noVerify IfThenElse0.bpl
%BGEXE% %* /noVerify Lambda.bpl
+%BGEXE% %* /noVerify IntReal.bpl
diff --git a/Test/test2/strings-no-where.bpl b/Test/test2/strings-no-where.bpl index c8ef88c8..6aee18ea 100644 --- a/Test/test2/strings-no-where.bpl +++ b/Test/test2/strings-no-where.bpl @@ -1,4 +1,4 @@ -type real;
+
type elements;
diff --git a/Test/test2/strings-where.bpl b/Test/test2/strings-where.bpl index 05e392cb..f196899f 100644 --- a/Test/test2/strings-where.bpl +++ b/Test/test2/strings-where.bpl @@ -1,4 +1,4 @@ -type real;
+
type elements;
diff --git a/Test/test20/Answer b/Test/test20/Answer index efa5bced..fa33507e 100644 --- a/Test/test20/Answer +++ b/Test/test20/Answer @@ -118,7 +118,7 @@ axiom (forall x: int :: intSet0[x] == (x == 0 || x == 2 || x == 3)); const intSet1: Set int;
-axiom (forall x: int :: intSet1[x] == (x == 0 - 5 || x == 3));
+axiom (forall x: int :: intSet1[x] == (x == -5 || x == 3));
procedure P();
@@ -126,7 +126,7 @@ procedure P(); implementation P()
{
- assert (forall x: int :: union(intSet0, intSet1)[x] == (x == 0 - 5 || x == 0 || x == 2 || x == 3));
+ assert (forall x: int :: union(intSet0, intSet1)[x] == (x == -5 || x == 0 || x == 2 || x == 3));
}
@@ -143,7 +143,7 @@ axiom (forall x: int :: intSet0[x] <==> x == 0 || x == 2 || x == 3); const intSet1: Set int;
-axiom (forall x: int :: intSet1[x] <==> x == 0 - 5 || x == 3);
+axiom (forall x: int :: intSet1[x] <==> x == -5 || x == 3);
procedure P();
@@ -151,7 +151,7 @@ procedure P(); implementation P()
{
- assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == 0 - 5 || x == 0 || x == 2 || x == 3);
+ assert (forall x: int :: union(intSet0, intSet1)[x] <==> x == -5 || x == 0 || x == 2 || x == 3);
}
diff --git a/Test/test20/Prog0.bpl b/Test/test20/Prog0.bpl index ea71b8a8..8fc7b7c7 100644 --- a/Test/test20/Prog0.bpl +++ b/Test/test20/Prog0.bpl @@ -1,5 +1,5 @@ // Let's test some Boogie 2 features ...
-type real;
+
type elements;
type Field a;
diff --git a/Test/test20/Prog1.bpl b/Test/test20/Prog1.bpl index 1d75805c..0e9413c1 100644 --- a/Test/test20/Prog1.bpl +++ b/Test/test20/Prog1.bpl @@ -1,5 +1,5 @@ // Let's test some Boogie 2 features ...
-type real;
+
type elements;
type Field a;
diff --git a/Test/test21/Answer b/Test/test21/Answer index 914e56a1..28aa4e8b 100644 --- a/Test/test21/Answer +++ b/Test/test21/Answer @@ -278,6 +278,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -549,6 +552,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
@@ -826,6 +832,9 @@ Execution trace: LargeLiterals0.bpl(7,5): anon0
Boogie program verifier finished with 0 verified, 1 error
+--------------------- File Real.bpl ----------------------------
+
+Boogie program verifier finished with 1 verified, 0 errors
--------------------- File NameClash.bpl ----------------------------
Boogie program verifier finished with 1 verified, 0 errors
diff --git a/Test/test21/Real.bpl b/Test/test21/Real.bpl new file mode 100644 index 00000000..3dcf3ea3 --- /dev/null +++ b/Test/test21/Real.bpl @@ -0,0 +1,17 @@ +axiom (forall r: real :: r == 0.0 || r / r == 1.0);
+
+procedure P(a: real, b: real) returns () {
+ assume a >= b && a != 0.0 && a >= 1.3579;
+
+ assert 2e0 * (a + 3.0) - 0.5 >= b;
+ assert 2e0 * (a + 3.0) - 0.5 > b;
+ assert b <= 2e0 * (a + 3.0) - 0.5;
+ assert b < 2e0 * (a + 3.0) - 0.5;
+
+ assert 1/2 <= 0.65;
+ assert a > 100e-2 ==> 1 / a <= a;
+ assert a / 2 != a || a == 0.00;
+ assert a != 0.0 ==> a / a == 1.0;
+
+ assert int(a) >= 0 ==> real(3) * a > a;
+}
\ No newline at end of file diff --git a/Test/test21/runtest.bat b/Test/test21/runtest.bat index d994a4da..bfdcc570 100644 --- a/Test/test21/runtest.bat +++ b/Test/test21/runtest.bat @@ -4,6 +4,7 @@ setlocal set BGEXE=..\..\Binaries\Boogie.exe
rem set BGEXE=mono ..\..\Binaries\Boogie.exe
+
for %%m in (
n p a
) do (
@@ -16,7 +17,8 @@ for %%f in (DisjointDomains.bpl DisjointDomains2.bpl FunAxioms.bpl Keywords.bpl Casts.bpl BooleanQuantification.bpl EmptyList.bpl Boxing.bpl
MapOutputTypeParams.bpl ParallelAssignment.bpl BooleanQuantification2.bpl
Flattening.bpl Orderings.bpl Orderings2.bpl Orderings3.bpl Orderings4.bpl
- EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl) do (
+ EmptySetBug.bpl Coercions2.bpl MapAxiomsConsistency.bpl LargeLiterals0.bpl
+ Real.bpl) do (
echo --------------------- File %%f ----------------------------
%BGEXE% %* /typeEncoding:%%m /logPrefix:0%%m %%f
)
|