From 2dae113e5996e050ca6595542de5030747245929 Mon Sep 17 00:00:00 2001 From: Dietrich Date: Mon, 27 Apr 2015 05:37:19 -0600 Subject: Began adding the float type to VC expression --- Source/Provers/SMTLib/SMTLibLineariser.cs | 12 ++++++++++++ 1 file changed, 12 insertions(+) (limited to 'Source/Provers') diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index f431c3d5..6accf79f 100644 --- a/Source/Provers/SMTLib/SMTLibLineariser.cs +++ b/Source/Provers/SMTLib/SMTLibLineariser.cs @@ -678,6 +678,12 @@ namespace Microsoft.Boogie.SMTLib return true; } + public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options) + { + WriteApplication("/f", node, options); + return true; + } + public bool VisitPowOp(VCExprNAry node, LineariserOptions options) { WriteApplication("real_pow", node, options); return true; @@ -729,6 +735,12 @@ 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; -- cgit v1.2.3