diff options
| author |  Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-27 11:51:35 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2015-02-27 11:51:35 +0000 |
| commit | aa48ab54832d6301ad0511227dea40df2b959a5f (patch) | |
| tree | ae164d774930959ee2a6f686af2998eb56741967 /Source/Provers | |
| parent | 23d9c5c2f60f25c8aa237be46ea9625b4792bfb7 (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')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 15 |
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;
|