diff options
| author |  MichalMoskal <unknown> | 2011-02-18 01:02:15 +0000 |
|---|---|---|
| committer | MichalMoskal <unknown> | 2011-02-18 01:02:15 +0000 |
| commit | d6221bcb829c5034d062500680652e0d261f3332 (patch) | |
| tree | 69a5da7455230c0912bef7df1ebc8bd66b3d7d55 /Source/Provers/SMTLib/SMTLibNamer.cs | |
| parent | ff9f8978724c4e43238bd2a9fe19fed008b61ca6 (diff) | |
Handle bitvectors
Diffstat (limited to 'Source/Provers/SMTLib/SMTLibNamer.cs')
| -rw-r--r-- | Source/Provers/SMTLib/SMTLibNamer.cs | 9 |
1 files changed, 9 insertions, 0 deletions
diff --git a/Source/Provers/SMTLib/SMTLibNamer.cs b/Source/Provers/SMTLib/SMTLibNamer.cs index 80de8e3f..8a40bd84 100644 --- a/Source/Provers/SMTLib/SMTLibNamer.cs +++ b/Source/Provers/SMTLib/SMTLibNamer.cs @@ -25,6 +25,15 @@ namespace Microsoft.Boogie.SMTLib "=>", // implies (sic!)
// Integers
"Int", "*", "/", "-", "+", "<", "<=", ">", ">=",
+ // Bitvectors
+ "extract", "concat",
+ "bvnot", "bvneg", "bvand", "bvor", "bvadd", "bvmul", "bvudiv", "bvurem", "bvshl", "bvlshr", "bvult",
+ // Z3 (and not only?) extensions to bitvectors
+ "bit1", "bit0", "bvsub", "bvsdiv", "bvsrem", "bvsmod", "bvsdiv0", "bvudiv0", "bvsrem0", "bvurem0",
+ "bvsmod0", "bvsdiv_i", "bvudiv_i", "bvsrem_i", "bvurem_i", "bvumod_i", "bvule", "bvsle", "bvuge",
+ "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",
// SMT v1 stuff
"flet", "implies", "!=", "if_then_else",
// Z3 extensions
|