Home
last modified time | relevance | path

Searched refs:toZ3Expr (Results 1 – 2 of 2) sorted by relevance

/external/swiftshader/third_party/llvm-10.0/llvm/lib/Support/
DZ3Solver.cpp194 static const Z3Expr &toZ3Expr(const SMTExpr &E) { in toZ3Expr() function
286 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
299 auto It = CachedExprs.insert(toZ3Expr(Exp)); in newExprRef()
314 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); in getSort()
335 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNeg()
340 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNot()
345 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); in mkNot()
350 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, in mkBVAdd()
351 toZ3Expr(*RHS).AST))); in mkBVAdd()
356 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
[all …]
/external/llvm-project/llvm/lib/Support/
DZ3Solver.cpp195 static const Z3Expr &toZ3Expr(const SMTExpr &E) { in toZ3Expr() function
287 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
300 auto It = CachedExprs.insert(toZ3Expr(Exp)); in newExprRef()
315 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); in getSort()
336 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNeg()
341 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNot()
346 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); in mkNot()
351 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, in mkBVAdd()
352 toZ3Expr(*RHS).AST))); in mkBVAdd()
357 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
[all …]