diff options
| author |  Bryan Parno <parno@microsoft.com> | 2014-10-24 14:43:40 -0700 |
|---|---|---|
| committer | Bryan Parno <parno@microsoft.com> | 2014-10-24 14:43:40 -0700 |
| commit | c9e1adac517c5954e628c4088e4efb79b4ca8cec (patch) | |
| tree | bb33f46a08c738264f417412b6034297e5e23f37 /Source | |
| parent | 40f36d68b8cb9489d052ababada29539c7d8de92 (diff) | |
Add an option to use reduce Z3's knowledge of non-linear arithmetic.
Results in more manual work, but it also produces more predictable behavior.
Diffstat (limited to 'Source')
| -rw-r--r-- | Source/Dafny/DafnyOptions.cs | 6 | ||||
| -rw-r--r-- | Source/Dafny/Translator.cs | 103 |
2 files changed, 90 insertions, 19 deletions
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:
|