summaryrefslogtreecommitdiff
path: root/Source/Provers/SMTLib
diff options
context:
space:
mode:
authorGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-27 11:51:35 +0000
committerGravatar Dan Liew <daniel.liew@imperial.ac.uk>2015-02-27 11:51:35 +0000
commitaa48ab54832d6301ad0511227dea40df2b959a5f (patch)
treeae164d774930959ee2a6f686af2998eb56741967 /Source/Provers/SMTLib
parent23d9c5c2f60f25c8aa237be46ea9625b4792bfb7 (diff)
Fix using reserved Z3 keywords for float operators. These are taken
from ``float_decl_plugin::get_op_names(..)`` in ``src/ast/float_decl_plugin.cpp`` from the Z3 4.3.2 source code.
Diffstat (limited to 'Source/Provers/SMTLib')
-rw-r--r--Source/Provers/SMTLib/SMTLibNamer.cs15
1 files changed, 11 insertions, 4 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs
index b6a6aafa..502e89e5 100644
--- a/Source/Provers/SMTLib/SMTLibNamer.cs
+++ b/Source/Provers/SMTLib/SMTLibNamer.cs
@@ -36,13 +36,12 @@ namespace Microsoft.Boogie.SMTLib
"bvsge", "bvslt", "bvugt", "bvsgt", "bvxor", "bvnand", "bvnor", "bvxnor", "sign_extend", "zero_extend",
"repeat", "bvredor", "bvredand", "bvcomp", "bvumul_noovfl", "bvsmul_noovfl", "bvsmul_noudfl", "bvashr",
"rotate_left", "rotate_right", "ext_rotate_left", "ext_rotate_right", "int2bv", "bv2int",
- // floating point
- "plusInfinity", "minusInfinity", "NaN",
- "roundNearestTiesToEven", "roundNearestTiesToAway", "roundTowardPositive", "roundTowardNegative", "roundTowardZero",
+ // floating point (FIXME: Legacy, remove this)
+ "plusInfinity", "minusInfinity",
"+", "-", "/", "*", "==", "<", ">", "<=", ">=",
"abs", "remainder", "fusedMA", "squareRoot", "roundToIntegral",
"isZero", "isNZero", "isPZero", "isSignMinus", "min", "max", "asFloat",
- // SMT v1 stuff
+ // SMT v1 stuff (FIXME: Legacy, remove this)
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
"lblneg", "lblpos", "lbl-lit",
@@ -50,6 +49,14 @@ namespace Microsoft.Boogie.SMTLib
"sin", "cos", "tan", "asin", "acos", "atan",
// Boogie-defined
"real_pow", "UOrdering2", "UOrdering3",
+ // Floating point (final draft SMTLIB-v2.5)
+ "NaN",
+ "roundNearestTiesToEven", "roundNearestTiesToAway", "roundTowardPositive", "roundTowardNegative", "roundTowardZero",
+ "RNE", "RNA", "RTP", "RTN", "RTZ",
+ "fp.abs", "fp.neg", "fp.add", "fp.sub", "fp.mul", "fp.div", "fp.fma", "fp.sqrt", "fp.rem", "fp.roundToIntegral",
+ "fp.min", "fp.max", "fp.leq", "fp.lt", "fp.geq", "fp.gt", "fp.eq",
+ "fp.isNormal", "fp.isSubnormal", "fp.isZero", "fp.isInfinite", "fp.isNaN", "fp.isNegative", "fp.isPositive",
+ "fp", "fp.to_ubv", "fp.to_sbv", "to_fp",
};
static HashSet<string> reservedSmtWords;