Searched refs:toZ3Expr (Results 1 – 1 of 1) sorted by relevance
| /openbsd/src/gnu/llvm/llvm/lib/Support/ |
| D | Z3Solver.cpp | 197 static const Z3Expr &toZ3Expr(const SMTExpr &E) { in toZ3Expr() function
289 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
302 auto It = CachedExprs.insert(toZ3Expr(Exp)); in newExprRef()
317 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); in getSort()
338 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNeg()
343 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNot()
348 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); in mkNot()
353 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, in mkBVAdd()
354 toZ3Expr(*RHS).AST))); in mkBVAdd()
359 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
[all …]
|