diff options
| author |  Checkmate50 <dgeisler50@gmail.com> | 2015-10-14 12:57:50 -0600 |
|---|---|---|
| committer | Checkmate50 <dgeisler50@gmail.com> | 2015-10-14 12:57:50 -0600 |
| commit | 0324757fb1a12d76861a51be988690bf8de75f64 (patch) | |
| tree | 48693a6815c6ced0eebee81657a0c44c200ef62d /Source/Provers | |
| parent | 80f3d4ed1bb221adbd3c7162acea10920b9fab73 (diff) | |
Modified translation so that z3 runs with type checking for simple binary operations
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibLineariser.cs | 76 | ||||
| -rw-r--r-- | Source/Provers/SMTLib/Z3.cs | 4 |
2 files changed, 77 insertions, 3 deletions
diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs index f030870e..629f7e2d 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 "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")"; //TODO: Match z3 syntax
+ return "(_ FloatingPoint " + t.FloatExponent + " " + t.FloatMantissa + ")";
else if (t.IsBv) {
return "(_ BitVec " + t.BvBits + ")";
} else {
@@ -204,11 +204,13 @@ namespace Microsoft.Boogie.SMTLib else if (node is VCExprFloatLit)
{
BigFloat lit = ((VCExprFloatLit)node).Val;
+ wr.Write(("((_ to_fp 8 24) roundTowardZero "));
if (lit.IsNegative)
// In SMT2 "-42" is an identifier (SMT2, Sect. 3.2 "Symbols")
wr.Write("(- 0.0 {0})", lit.Abs.ToDecimalString());
else
wr.Write(lit.ToDecimalString());
+ wr.Write(")");
}
else {
Contract.Assert(false);
@@ -616,6 +618,78 @@ namespace Microsoft.Boogie.SMTLib return true;
}
+ public bool VisitFloatAddOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.add roundTowardZero", node, options);
+ return true;
+ }
+
+ public bool VisitFloatSubOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.sub roundTowardZero", node, options);
+ return true;
+ }
+
+ public bool VisitFloatMulOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.mul roundTowardZero", node, options);
+ return true;
+ }
+
+ public bool VisitFloatDivOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.div roundTowardZero", node, options);
+ return true;
+ }
+
+ public bool VisitFloatRemOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.rem roundTowardZero", node, options);
+ return true;
+ }
+
+ public bool VisitFloatMinOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.min", node, options);
+ return true;
+ }
+
+ public bool VisitFloatMaxOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.max", node, options);
+ return true;
+ }
+
+ public bool VisitFloatLeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.leq", node, options);
+ return true;
+ }
+
+ public bool VisitFloatLtOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.lt", node, options);
+ return true;
+ }
+
+ public bool VisitFloatGeqOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.geq", node, options);
+ return true;
+ }
+
+ public bool VisitFloatGtOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.gt", node, options);
+ return true;
+ }
+
+ public bool VisitFloatEqOp(VCExprNAry node, LineariserOptions options)
+ {
+ WriteApplication("fp.eq", node, options);
+ return true;
+ }
+
static char[] hex = { '0', '1', '2', '3', '4', '5', '6', '7', '8', '9', 'a', 'b', 'c', 'd', 'e', 'f' };
public bool VisitBvOp(VCExprNAry node, LineariserOptions options)
{
diff --git a/Source/Provers/SMTLib/Z3.cs b/Source/Provers/SMTLib/Z3.cs index 8e8b2d55..250e04c9 100644 --- a/Source/Provers/SMTLib/Z3.cs +++ b/Source/Provers/SMTLib/Z3.cs @@ -253,7 +253,7 @@ namespace Microsoft.Boogie.SMTLib //if (options.Inspector != null)
// options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
- options.AddWeakSmtOption("TYPE_CHECK", "false");
+ options.AddWeakSmtOption("TYPE_CHECK", "true");
options.AddWeakSmtOption("smt.BV.REFLECT", "true");
if (options.TimeLimit > 0)
@@ -334,7 +334,7 @@ namespace Microsoft.Boogie.SMTLib //if (options.Inspector != null)
// options.WeakAddSmtOption("PROGRESS_SAMPLING_FREQ", "100");
- options.AddWeakSmtOption("TYPE_CHECK", "false");
+ options.AddWeakSmtOption("TYPE_CHECK", "true");
options.AddWeakSmtOption("BV_REFLECT", "true");
if (options.TimeLimit > 0)
|