#include <Z3Expr.h>
|
static z3::context * | ctx = nullptr |
|
static z3::solver * | solver = nullptr |
|
|
Z3Expr | operator== (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator!= (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator> (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator< (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator<= (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator>= (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator+ (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator- (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator* (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator/ (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator% (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator^ (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator& (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator| (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | ashr (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | shl (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | int2bv (u32_t n, const Z3Expr &e) |
|
Z3Expr | bv2int (const Z3Expr &e, bool isSigned) |
|
Z3Expr | operator&& (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator|| (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Z3Expr | operator! (const Z3Expr &lhs) |
|
Z3Expr | ite (const Z3Expr &cond, const Z3Expr &lhs, const Z3Expr &rhs) |
|
std::ostream & | operator<< (std::ostream &out, const Z3Expr &expr) |
|
bool | eq (const Z3Expr &lhs, const Z3Expr &rhs) |
|
Definition at line 38 of file Z3Expr.h.
◆ Z3Expr() [1/6]
Definition at line 51 of file Z3Expr.h.
static z3::expr nullExpr()
null expression
◆ Z3Expr() [2/6]
SVF::Z3Expr::Z3Expr |
( |
const z3::expr & |
_e | ) |
|
|
inline |
◆ Z3Expr() [3/6]
SVF::Z3Expr::Z3Expr |
( |
int |
i | ) |
|
|
inline |
Definition at line 59 of file Z3Expr.h.
static z3::context & getContext()
Get z3 context, singleton design here to make sure we only have one context.
◆ Z3Expr() [4/6]
SVF::Z3Expr::Z3Expr |
( |
const Z3Expr & |
z3Expr | ) |
|
|
inline |
◆ Z3Expr() [5/6]
SVF::Z3Expr::Z3Expr |
( |
float |
f | ) |
|
|
inline |
◆ Z3Expr() [6/6]
SVF::Z3Expr::Z3Expr |
( |
double |
f | ) |
|
|
inline |
◆ ~Z3Expr()
virtual SVF::Z3Expr::~Z3Expr |
( |
| ) |
|
|
virtualdefault |
◆ AND()
compute AND, used for branch condition
Definition at line 92 of file Z3Expr.cpp.
114 z3::check_result res =
getSolver().check();
116 if (res != z3::unsat)
static const Option< u32_t > MaxZ3Size
static z3::solver & getSolver()
Get z3 solver, singleton design here to make sure we only have one context.
static u32_t getExprSize(const Z3Expr &z3Expr)
get the number of subexpression of a Z3 expression
static Z3Expr getTrueCond()
Return the unique true condition.
friend bool eq(const Z3Expr &lhs, const Z3Expr &rhs)
static Z3Expr getFalseCond()
Return the unique false condition.
◆ dumpStr()
output Z3 expression as a string
Definition at line 168 of file Z3Expr.cpp.
170 std::ostringstream out;
171 out << z3Expr.getExpr();
◆ get_numeral_int()
int SVF::Z3Expr::get_numeral_int |
( |
| ) |
const |
|
inline |
Definition at line 147 of file Z3Expr.h.
149 return e.get_numeral_int();
◆ get_numeral_int64()
int64_t SVF::Z3Expr::get_numeral_int64 |
( |
| ) |
const |
|
inline |
Definition at line 142 of file Z3Expr.h.
144 return e.get_numeral_int64();
◆ get_sort()
z3::sort SVF::Z3Expr::get_sort |
( |
| ) |
const |
|
inline |
Definition at line 274 of file Z3Expr.h.
const z3::expr & getExpr() const
◆ getContext()
z3::context & SVF::Z3Expr::getContext |
( |
| ) |
|
|
static |
Get z3 context, singleton design here to make sure we only have one context.
Definition at line 66 of file Z3Expr.cpp.
70 ctx =
new z3::context();
◆ getExpr()
const z3::expr& SVF::Z3Expr::getExpr |
( |
| ) |
const |
|
inline |
◆ getExprSize()
u32_t SVF::Z3Expr::getExprSize |
( |
const Z3Expr & |
z3Expr | ) |
|
|
static |
get the number of subexpression of a Z3 expression
Definition at line 76 of file Z3Expr.cpp.
79 if (z3Expr.getExpr().num_args() == 0)
83 for (
u32_t i = 0; i < z3Expr.getExpr().num_args(); ++i)
85 Z3Expr expr = z3Expr.getExpr().arg(i);
◆ getFalseCond()
static Z3Expr SVF::Z3Expr::getFalseCond |
( |
| ) |
|
|
inlinestatic |
Return the unique false condition.
Definition at line 295 of file Z3Expr.h.
◆ getSolver()
z3::solver & SVF::Z3Expr::getSolver |
( |
| ) |
|
|
static |
Get z3 solver, singleton design here to make sure we only have one context.
Definition at line 56 of file Z3Expr.cpp.
static z3::solver * solver
◆ getTrueCond()
static Z3Expr SVF::Z3Expr::getTrueCond |
( |
| ) |
|
|
inlinestatic |
Return the unique true condition.
Definition at line 288 of file Z3Expr.h.
◆ hash()
u32_t SVF::Z3Expr::hash |
( |
void |
| ) |
const |
|
inline |
◆ id()
u32_t SVF::Z3Expr::id |
( |
| ) |
const |
|
inline |
◆ is_bool()
bool SVF::Z3Expr::is_bool |
( |
| ) |
const |
|
inline |
◆ is_numeral()
bool SVF::Z3Expr::is_numeral |
( |
| ) |
const |
|
inline |
Definition at line 127 of file Z3Expr.h.
129 return e.is_numeral();
◆ NEG()
compute NEG
Definition at line 301 of file Z3Expr.h.
303 return (!z3Expr).simplify();
◆ nullExpr()
static z3::expr SVF::Z3Expr::nullExpr |
( |
| ) |
|
|
inlinestatic |
null expression
Definition at line 105 of file Z3Expr.h.
◆ operator=()
Definition at line 77 of file Z3Expr.h.
79 if (this->
id() != rhs.id())
◆ OR()
compute OR, used for branch condition
Definition at line 130 of file Z3Expr.cpp.
152 z3::check_result res =
getSolver().check();
154 if (res != z3::unsat)
◆ releaseContext()
void SVF::Z3Expr::releaseContext |
( |
| ) |
|
|
static |
release z3 context
Definition at line 40 of file Z3Expr.cpp.
static void releaseSolver()
release z3 solver
◆ releaseSolver()
void SVF::Z3Expr::releaseSolver |
( |
| ) |
|
|
static |
◆ simplify()
Z3Expr SVF::Z3Expr::simplify |
( |
| ) |
const |
|
inline |
◆ to_string()
Definition at line 122 of file Z3Expr.h.
124 return e.to_string();
◆ ashr
Definition at line 223 of file Z3Expr.h.
225 return ashr(lhs.getExpr(), rhs.getExpr());
friend Z3Expr ashr(const Z3Expr &lhs, const Z3Expr &rhs)
◆ bv2int
Definition at line 238 of file Z3Expr.h.
240 return z3::bv2int(
e.getExpr(), isSigned);
◆ eq
Definition at line 269 of file Z3Expr.h.
271 return eq(lhs.getExpr().simplify(), rhs.getExpr().simplify());
◆ int2bv
Definition at line 233 of file Z3Expr.h.
friend Z3Expr int2bv(u32_t n, const Z3Expr &e)
◆ ite
Definition at line 258 of file Z3Expr.h.
260 return ite(cond.getExpr(), lhs.getExpr(), rhs.getExpr());
friend Z3Expr ite(const Z3Expr &cond, const Z3Expr &lhs, const Z3Expr &rhs)
◆ operator!
Definition at line 253 of file Z3Expr.h.
255 return !lhs.getExpr();
◆ operator!=
Definition at line 158 of file Z3Expr.h.
160 return lhs.getExpr() != rhs.getExpr();
◆ operator%
Definition at line 203 of file Z3Expr.h.
205 return lhs.getExpr() % rhs.getExpr();
◆ operator&
Definition at line 213 of file Z3Expr.h.
215 return lhs.getExpr() & rhs.getExpr();
◆ operator&&
Definition at line 243 of file Z3Expr.h.
245 return lhs.getExpr() && rhs.getExpr();
◆ operator*
Definition at line 193 of file Z3Expr.h.
195 return lhs.getExpr() * rhs.getExpr();
◆ operator+
Definition at line 183 of file Z3Expr.h.
185 return lhs.getExpr() + rhs.getExpr();
◆ operator-
Definition at line 188 of file Z3Expr.h.
190 return lhs.getExpr() - rhs.getExpr();
◆ operator/
Definition at line 198 of file Z3Expr.h.
200 return lhs.getExpr() / rhs.getExpr();
◆ operator<
Definition at line 168 of file Z3Expr.h.
170 return lhs.getExpr() < rhs.getExpr();
◆ operator<<
std::ostream& operator<< |
( |
std::ostream & |
out, |
|
|
const Z3Expr & |
expr |
|
) |
| |
|
friend |
Definition at line 263 of file Z3Expr.h.
265 out << expr.getExpr();
◆ operator<=
Definition at line 173 of file Z3Expr.h.
175 return lhs.getExpr() <= rhs.getExpr();
◆ operator==
Definition at line 153 of file Z3Expr.h.
155 return lhs.getExpr() == rhs.getExpr();
◆ operator>
Definition at line 163 of file Z3Expr.h.
165 return lhs.getExpr() > rhs.getExpr();
◆ operator>=
Definition at line 178 of file Z3Expr.h.
180 return lhs.getExpr() >= rhs.getExpr();
◆ operator^
Definition at line 208 of file Z3Expr.h.
210 return lhs.getExpr() ^ rhs.getExpr();
◆ operator|
Definition at line 218 of file Z3Expr.h.
220 return lhs.getExpr() | rhs.getExpr();
◆ operator||
Definition at line 248 of file Z3Expr.h.
250 return lhs.getExpr() || rhs.getExpr();
◆ shl
Definition at line 228 of file Z3Expr.h.
230 return shl(lhs.getExpr(), rhs.getExpr());
friend Z3Expr shl(const Z3Expr &lhs, const Z3Expr &rhs)
◆ ctx
z3::context * SVF::Z3Expr::ctx = nullptr |
|
static |
◆ solver
z3::solver * SVF::Z3Expr::solver = nullptr |
|
static |
The documentation for this class was generated from the following files:
- /home/runner/work/SVF/SVF/svf/include/Util/Z3Expr.h
- /home/runner/work/SVF/SVF/svf/lib/Util/Z3Expr.cpp