diff options
| author |  Dietrich <dgeisler50@gmail.com> | 2015-07-13 19:40:09 -0600 |
|---|---|---|
| committer | Dietrich <dgeisler50@gmail.com> | 2015-07-13 19:40:09 -0600 |
| commit | 52aa9b8f63a3d955031e7a0dfd6e575ca7cf76b3 (patch) | |
| tree | b24be506dda4eae8b2f98486ddacd8df031dc119 /Source/Provers | |
| parent | fe331e0a63c7921a996e007860182bad9628fb0d (diff) | |
Modified internal abstract float representation to allow user-defined mantissa and exponent
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 4 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibProcess.cs | 1 |
2 files changed, 3 insertions, 2 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index b834aa6b..c7ae9d57 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -141,7 +141,7 @@ namespace Microsoft.Boogie.SMTLib else if (t.IsReal)
return "Real";
else if (t.IsFloat)
- return "Real"; //TODO: Make to be a float
+ return t.ToString(); //TODO: Match z3 syntax
else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
@@ -690,7 +690,7 @@ namespace Microsoft.Boogie.SMTLib }
public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
- {
+ { //TODO: match z3
WriteApplication("/f", node, options);
return true;
}
diff --git a/Source/Provers/SMTLib/SMTLibProcess.cs b/Source/Provers/SMTLib/SMTLibProcess.cs index 4a1331c5..2b09362b 100644 --- a/Source/Provers/SMTLib/SMTLibProcess.cs +++ b/Source/Provers/SMTLib/SMTLibProcess.cs @@ -93,6 +93,7 @@ namespace Microsoft.Boogie.SMTLib log = log.Replace("\r", "").Replace("\n", " ");
Console.WriteLine("[SMT-INP-{0}] {1}", smtProcessId, log);
}
+ Console.WriteLine(cmd); //TODO: Remove This Line
toProver.WriteLine(cmd);
}
|