ilang  1.1.4
ILAng: A Modeling and Verification Platform for SoCs
 All Classes Namespaces Files Functions Variables Typedefs Enumerations Friends Macros
z3_helper.h
Go to the documentation of this file.
1 
4 #ifndef ILANG_UTIL_Z3_HELPER_H__
5 #define ILANG_UTIL_Z3_HELPER_H__
6 
7 #include <string>
8 
9 #include <ilang/config.h>
10 #include <ilang/ila/ast/sort_value.h>
11 #include <z3++.h>
12 
13 namespace ilang {
14 
15 #ifndef Z3_LEGACY_API
16 inline BvValType Z3BvVal(const BvValType& bv_val) { return bv_val; }
18 #else
19 inline __int64 Z3BvVal(const BvValType& bv_val) {
21  return static_cast<__int64>(bv_val);
22 }
23 #endif
24 
26 inline z3::expr Z3Implies(z3::context& ctx, const z3::expr& a,
27  const z3::expr& b) {
28 #ifndef Z3_LEGACY_API
29  return z3::implies(a, b);
30 #else
31  return z3::expr(ctx, Z3_mk_implies(ctx, a, b));
32 #endif
33 }
34 
36 inline z3::expr Z3Shl(z3::context& ctx, const z3::expr& a, const z3::expr& b) {
37 #ifndef Z3_LEGACY_API
38  return z3::shl(a, b);
39 #else
40  return z3::expr(ctx, Z3_mk_bvshl(ctx, a, b));
41 #endif
42 }
43 
45 inline z3::expr Z3Ashr(z3::context& ctx, const z3::expr& a, const z3::expr& b) {
46 #ifndef Z3_LEGACY_API
47  return z3::ashr(a, b);
48 #else
49  return z3::expr(ctx, Z3_mk_bvashr(ctx, a, b));
50 #endif
51 }
52 
54 inline z3::expr Z3Lshr(z3::context& ctx, const z3::expr& a, const z3::expr& b) {
55 #ifndef Z3_LEGACY_API
56  return z3::lshr(a, b);
57 #else
58  return z3::expr(ctx, Z3_mk_bvlshr(ctx, a, b));
59 #endif
60 }
61 
63 inline z3::expr Z3SRem(z3::context& ctx, const z3::expr& a, const z3::expr& b) {
64 #ifndef Z3_LEGACY_API
65  return z3::srem(a, b);
66 #else
67  return z3::expr(ctx, Z3_mk_bvsrem(ctx, a, b));
68 #endif
69 }
70 
72 inline z3::expr Z3URem(z3::context& ctx, const z3::expr& a, const z3::expr& b) {
73 #ifndef Z3_LEGACY_API
74  return z3::urem(a, b);
75 #else
76  return z3::expr(ctx, Z3_mk_bvurem(ctx, a, b));
77 #endif
78 }
79 
81 inline z3::expr Z3SMod(z3::context& ctx, const z3::expr& a, const z3::expr& b) {
82 #ifndef Z3_LEGACY_API
83  return z3::smod(a, b);
84 #else
85  return z3::expr(ctx, Z3_mk_bvsmod(ctx, a, b));
86 #endif
87 }
88 
90 inline z3::expr Z3ZExt(z3::context& ctx, const z3::expr& e, const unsigned& w) {
91 #ifndef Z3_LEGACY_API
92  return z3::zext(e, w);
93 #else
94  return z3::expr(ctx, Z3_mk_zero_ext(ctx, w, e));
95 #endif
96 }
97 
99 inline z3::expr Z3SExt(z3::context& ctx, const z3::expr& e, const unsigned& w) {
100 #ifndef Z3_LEGACY_API
101  return z3::sext(e, w);
102 #else
103  return z3::expr(ctx, Z3_mk_sign_ext(ctx, w, e));
104 #endif
105 }
106 
108 inline z3::expr Z3LRotate(z3::context& ctx, z3::expr& e, unsigned& w) {
109 #ifndef Z3_LEGACY_API
110  return e.rotate_left(w);
111 #else
112  return z3::expr(ctx, Z3_mk_rotate_left(ctx, w, e));
113 #endif
114 }
115 
117 inline z3::expr Z3RRotate(z3::context& ctx, z3::expr& e, unsigned& w) {
118 #ifndef Z3_LEGACY_API
119  return e.rotate_right(w);
120 #else
121  return z3::expr(ctx, Z3_mk_rotate_right(ctx, w, e));
122 #endif
123 }
124 
126 inline std::string Z3Expr2String(z3::context& ctx, const z3::expr& e) {
127 #ifndef Z3_LEGACY_API
128  return e.to_string();
129 #else
130  return static_cast<std::string>(Z3_ast_to_string(ctx, e));
131 #endif
132 }
133 
134 }; // namespace ilang
135 
136 #endif // ILANG_UTIL_Z3_HELPER_H__
ilang::Z3Lshr
z3::expr Z3Lshr(z3::context &ctx, const z3::expr &a, const z3::expr &b)
Interface z3 lshr ast node construction.
Definition: z3_helper.h:54
ilang::Z3Implies
z3::expr Z3Implies(z3::context &ctx, const z3::expr &a, const z3::expr &b)
Interface z3 implies ast node construction.
Definition: z3_helper.h:26
ilang::Z3BvVal
BvValType Z3BvVal(const BvValType &bv_val)
Interface z3 bit-vector constant numeric.
Definition: z3_helper.h:17
ilang::Z3SMod
z3::expr Z3SMod(z3::context &ctx, const z3::expr &a, const z3::expr &b)
Interface z3 shl ast node construction.
Definition: z3_helper.h:81
ilang::Z3Shl
z3::expr Z3Shl(z3::context &ctx, const z3::expr &a, const z3::expr &b)
Interface z3 shl ast node construction.
Definition: z3_helper.h:36
ilang::Z3RRotate
z3::expr Z3RRotate(z3::context &ctx, z3::expr &e, unsigned &w)
Interface z3 right rotate ast node construction.
Definition: z3_helper.h:117
ilang::Z3Ashr
z3::expr Z3Ashr(z3::context &ctx, const z3::expr &a, const z3::expr &b)
Interface z3 ashr ast node construction.
Definition: z3_helper.h:45
ilang::Z3Expr2String
std::string Z3Expr2String(z3::context &ctx, const z3::expr &e)
Return the output string of the given z3::expr.
Definition: z3_helper.h:126
ilang::Z3URem
z3::expr Z3URem(z3::context &ctx, const z3::expr &a, const z3::expr &b)
Interface z3 shl ast node construction.
Definition: z3_helper.h:72
ilang::Z3LRotate
z3::expr Z3LRotate(z3::context &ctx, z3::expr &e, unsigned &w)
Interface z3 left rotate ast node construction.
Definition: z3_helper.h:108
sort_value.h
ilang::Z3SExt
z3::expr Z3SExt(z3::context &ctx, const z3::expr &e, const unsigned &w)
Interface z3 sext ast node construction.
Definition: z3_helper.h:99
ilang::BvValType
BvVal::BvValType BvValType
Data type for storing BvVal.
Definition: sort_value.h:103
ilang::Z3SRem
z3::expr Z3SRem(z3::context &ctx, const z3::expr &a, const z3::expr &b)
Interface z3 shl ast node construction.
Definition: z3_helper.h:63
ilang::Z3ZExt
z3::expr Z3ZExt(z3::context &ctx, const z3::expr &e, const unsigned &w)
Interface z3 zext ast node construction.
Definition: z3_helper.h:90
Generated by   doxygen 1.8.5