diff options
| author |  qadeer <qadeer@microsoft.com> | 2012-02-20 14:59:04 -0800 |
|---|---|---|
| committer | qadeer <qadeer@microsoft.com> | 2012-02-20 14:59:04 -0800 |
| commit | c793a5ea9bf33f9f7028af9920e569b5ec7fcc4f (patch) | |
| tree | 3aca8ecef601c7140be93ffaa1ee50815774a162 /Source/Provers | |
| parent | 51e9ec1d1b9fd9d707a7eb5b9c903e266efbdad1 (diff) | |
added floating point keywords to reserved SMTwords list
Diffstat (limited to 'Source/Provers')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index a874c6c5..5629c0d6 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -36,6 +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",
+ "+", "-", "/", "*", "==", "<", ">", "<=", ">=",
+ "abs", "remainder", "fusedMA", "squareRoot", "roundToIntegral",
+ "isZero", "isNZero", "isPZero", "isSignMinus", "min", "max", "asFloat",
// SMT v1 stuff
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
|