From aa48ab54832d6301ad0511227dea40df2b959a5f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 27 Feb 2015 11:51:35 +0000 Subject: 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. --- Source/Provers/SMTLib/SMTLibNamer.cs | 15 +++++++++++---- 1 file changed, 11 insertions(+), 4 deletions(-) (limited to 'Source/Provers') 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 reservedSmtWords; -- cgit v1.2.3