summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
diff options
context:
space:
mode:
authorGravatar Dietrich <dgeisler50@gmail.com>2015-04-27 05:37:19 -0600
committerGravatar Dietrich <dgeisler50@gmail.com>2015-04-27 05:37:19 -0600
commit2dae113e5996e050ca6595542de5030747245929 (patch)
tree74454d160c292949bedd02ebc1477930a763d2e1 /Source/Provers/SMTLib
parent94a9542de594ef210d1ede1ff05e12289dfb2dc7 (diff)
Began adding the float type to VC expression
Diffstat (limited to 'Source/Provers/SMTLib')
-rw-r--r--Source/Provers/SMTLib/SMTLibLineariser.cs12
1 files changed, 12 insertions, 0 deletions
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;