diff options
author | Checkmate50 <dgeisler50@gmail.com> | 2015-09-23 04:08:00 -0600 |
---|---|---|
committer | Checkmate50 <dgeisler50@gmail.com> | 2015-09-23 04:08:00 -0600 |
commit | 80f3d4ed1bb221adbd3c7162acea10920b9fab73 (patch) | |
tree | 218275e91b58fdb3cbce0376a4b423fa34e4e763 /Source/Provers/SMTLib/SMTLibLineariser.cs | |
parent | 28a20e6eba2919e008f70874b4c12a3ce7ad049c (diff) |
Modified BigFloat to avoid evaluating the floating point value before sending it to z3
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')
-rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 12 |
1 files changed, 0 insertions, 12 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index 3633a9c0..f030870e 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -689,12 +689,6 @@ namespace Microsoft.Boogie.SMTLib return true;
}
- public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
- { //TODO: match z3
- WriteApplication("/f", node, options);
- return true;
- }
-
public bool VisitPowOp(VCExprNAry node, LineariserOptions options) {
WriteApplication("real_pow", node, options);
return true;
@@ -746,12 +740,6 @@ namespace Microsoft.Boogie.SMTLib return true;
}
- public bool VisitToFloatOp(VCExprNAry node, LineariserOptions options)
- {
- WriteApplication("to_float", node, options);
- return true;
- }
-
private string ExtractDatatype(Function func) {
if (func is DatatypeSelector) {
DatatypeSelector selector = (DatatypeSelector) func;
|