Searched refs:toZ3Expr (Results 1 – 1 of 1) sorted by relevance
| /freebsd/contrib/llvm-project/llvm/lib/Support/ |
| H A D | Z3Solver.cpp | 202 static const Z3Expr &toZ3Expr(const SMTExpr &E) { in toZ3Expr() function
301 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
314 auto It = CachedExprs.insert(toZ3Expr(Exp)); in newExprRef()
329 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); in getSort()
350 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNeg()
355 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNot()
360 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); in mkNot()
365 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, in mkBVAdd()
366 toZ3Expr(*RHS).AST))); in mkBVAdd()
371 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
[all …]
|