diff options
| -rw-r--r-- | Binaries/DafnyPrelude.bpl | 15 | ||||
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 103 |
3 files changed, 105 insertions, 19 deletions
diff --git a/Binaries/DafnyPrelude.bpl b/Binaries/DafnyPrelude.bpl index 9b410b1e..91d8a01a 100644 --- a/Binaries/DafnyPrelude.bpl +++ b/Binaries/DafnyPrelude.bpl @@ -1022,3 +1022,18 @@ axiom (forall<U, V> m: Map U V, m': Map U V :: { Map#Disjoint(m, m') }
Map#Disjoint(m, m') <==> (forall o: U :: {Map#Domain(m)[o]} {Map#Domain(m')[o]} !Map#Domain(m)[o] || !Map#Domain(m')[o]));
+// -------------------------------------------------------------------------
+// -- Provide arithmetic wrappers to improve triggering and non-linear math
+// -------------------------------------------------------------------------
+
+function INTERNAL_add_boogie(x:int, y:int) : int { x + y }
+function INTERNAL_sub_boogie(x:int, y:int) : int { x - y }
+function INTERNAL_mul_boogie(x:int, y:int) : int { x * y }
+function INTERNAL_div_boogie(x:int, y:int) : int { x div y }
+function INTERNAL_mod_boogie(x:int, y:int) : int { x mod y }
+function {:never_pattern true} INTERNAL_lt_boogie(x:int, y:int) : bool { x < y }
+function {:never_pattern true} INTERNAL_le_boogie(x:int, y:int) : bool { x <= y }
+function {:never_pattern true} INTERNAL_gt_boogie(x:int, y:int) : bool { x > y }
+function {:never_pattern true} INTERNAL_ge_boogie(x:int, y:int) : bool { x >= y }
+
+// -------------------------------------------------------------------------
diff --git a/Source/Dafny/DafnyOptions.cs b/Source/Dafny/DafnyOptions.cs index 31fe6edd..b198e224 100644 --- a/Source/Dafny/DafnyOptions.cs +++ b/Source/Dafny/DafnyOptions.cs @@ -41,6 +41,7 @@ namespace Microsoft.Dafny public bool RunAfterCompile = false;
public bool SpillTargetCode = false;
public bool DisallowIncludes = false;
+ public bool DisableNLarith = false;
protected override bool ParseOption(string name, Bpl.CommandLineOptionEngine.CommandLineParseState ps) {
var args = ps.args; // convenient synonym
@@ -103,6 +104,11 @@ namespace Microsoft.Dafny DisallowIncludes = true;
return true;
+ case "noNLarith":
+ DisableNLarith = true;
+ this.Z3Options.Add("NL_ARITH=false");
+ return true;
+
default:
break;
}
diff --git a/Source/Dafny/Translator.cs b/Source/Dafny/Translator.cs index 4f0f3b61..0b240dfb 100644 --- a/Source/Dafny/Translator.cs +++ b/Source/Dafny/Translator.cs @@ -10676,41 +10676,106 @@ namespace Microsoft.Dafny { }
typ = Bpl.Type.Bool;
bOpcode = BinaryOperator.Opcode.Neq; break;
-
case BinaryExpr.ResolvedOpcode.Lt:
- typ = Bpl.Type.Bool;
- bOpcode = BinaryOperator.Opcode.Lt; break;
+ if (isReal || !DafnyOptions.O.DisableNLarith) {
+ typ = Bpl.Type.Bool;
+ bOpcode = BinaryOperator.Opcode.Lt;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_lt_boogie", Bpl.Type.Int, e0, e1);
+ }
+
case BinaryExpr.ResolvedOpcode.Le:
keepLits = true;
- typ = Bpl.Type.Bool;
- bOpcode = BinaryOperator.Opcode.Le; break;
+ if (isReal || !DafnyOptions.O.DisableNLarith) {
+ typ = Bpl.Type.Bool;
+ bOpcode = BinaryOperator.Opcode.Le;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_le_boogie", Bpl.Type.Int, e0, e1);
+ }
case BinaryExpr.ResolvedOpcode.Ge:
keepLits = true;
- typ = Bpl.Type.Bool;
- bOpcode = BinaryOperator.Opcode.Ge; break;
+ if (isReal || !DafnyOptions.O.DisableNLarith) {
+ typ = Bpl.Type.Bool;
+ bOpcode = BinaryOperator.Opcode.Ge;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_ge_boogie", Bpl.Type.Int, e0, e1);
+ }
case BinaryExpr.ResolvedOpcode.Gt:
- typ = Bpl.Type.Bool;
- bOpcode = BinaryOperator.Opcode.Gt; break;
+ if (isReal || !DafnyOptions.O.DisableNLarith) {
+ typ = Bpl.Type.Bool;
+ bOpcode = BinaryOperator.Opcode.Gt;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_gt_boogie", Bpl.Type.Int, e0, e1);
+ }
case BinaryExpr.ResolvedOpcode.Add:
- typ = isReal ? Bpl.Type.Real : Bpl.Type.Int;
- bOpcode = BinaryOperator.Opcode.Add; break;
+ if (!DafnyOptions.O.DisableNLarith) {
+ typ = isReal ? Bpl.Type.Real : Bpl.Type.Int;
+ bOpcode = BinaryOperator.Opcode.Add; break;
+ } else {
+ if (isReal) {
+ typ = Bpl.Type.Real;
+ bOpcode = BinaryOperator.Opcode.Add;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_add_boogie", Bpl.Type.Int, e0, e1);
+ }
+ }
case BinaryExpr.ResolvedOpcode.Sub:
- typ = isReal ? Bpl.Type.Real : Bpl.Type.Int;
- bOpcode = BinaryOperator.Opcode.Sub; break;
+ if (!DafnyOptions.O.DisableNLarith) {
+ typ = isReal ? Bpl.Type.Real : Bpl.Type.Int;
+ bOpcode = BinaryOperator.Opcode.Sub; break;
+ } else {
+ if (isReal) {
+ typ = Bpl.Type.Real;
+ bOpcode = BinaryOperator.Opcode.Sub;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_sub_boogie", Bpl.Type.Int, e0, e1);
+ }
+ }
case BinaryExpr.ResolvedOpcode.Mul:
- typ = isReal ? Bpl.Type.Real : Bpl.Type.Int;
- bOpcode = BinaryOperator.Opcode.Mul; break;
+ if (!DafnyOptions.O.DisableNLarith) {
+ typ = isReal ? Bpl.Type.Real : Bpl.Type.Int;
+ bOpcode = BinaryOperator.Opcode.Mul; break;
+ } else {
+ if (isReal) {
+ typ = Bpl.Type.Real;
+ bOpcode = BinaryOperator.Opcode.Mul;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_mul_boogie", Bpl.Type.Int, e0, e1);
+ }
+ }
+
case BinaryExpr.ResolvedOpcode.Div:
if (isReal) {
typ = Bpl.Type.Real;
bOpcode = BinaryOperator.Opcode.RealDiv; break;
} else {
- typ = Bpl.Type.Int;
- bOpcode = BinaryOperator.Opcode.Div; break;
+ if (!DafnyOptions.O.DisableNLarith) {
+ typ = Bpl.Type.Int;
+ bOpcode = BinaryOperator.Opcode.Div; break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_div_boogie", Bpl.Type.Int, e0, e1);
+ }
}
case BinaryExpr.ResolvedOpcode.Mod:
- typ = Bpl.Type.Int;
- bOpcode = BinaryOperator.Opcode.Mod; break;
+ if (!DafnyOptions.O.DisableNLarith) {
+ typ = Bpl.Type.Int;
+ bOpcode = BinaryOperator.Opcode.Mod; break;
+ } else {
+ if (isReal) {
+ typ = Bpl.Type.Real;
+ bOpcode = BinaryOperator.Opcode.Mod;
+ break;
+ } else {
+ return translator.FunctionCall(expr.tok, "INTERNAL_mod_boogie", Bpl.Type.Int, e0, e1);
+ }
+ }
case BinaryExpr.ResolvedOpcode.LtChar:
case BinaryExpr.ResolvedOpcode.LeChar:
|