Searched refs:toZ3Expr (Results 1 - 1 of 1) sorted by relevance
/freebsd-12-stable/contrib/llvm-project/llvm/lib/Support/ |
H A D | Z3Solver.cpp | 194 static const Z3Expr &toZ3Expr(const SMTExpr &E) { function in namespace:__anon4884 286 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); 299 auto It = CachedExprs.insert(toZ3Expr(Exp)); 314 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); 335 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST))); 340 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST))); 345 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST))); 350 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST, 351 toZ3Expr(*RHS).AST))); 356 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LH [all...] |
Completed in 54 milliseconds