Lines Matching full:context
44 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
46 llvm::Twine(Z3_get_error_msg(Context, Error)));
49 /// Wrapper for Z3 context
53 Z3_context Context;
56 Context = Z3_mk_context_rc(Config.Config);
57 // The error function is set here because the context is the first object
59 Z3_set_error_handler(Context, Z3ErrorHandler);
68 Z3_del_context(Context);
69 Context = nullptr;
77 Z3Context &Context;
83 Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
84 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
88 Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {
89 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
95 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));
96 Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
106 Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
111 Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));
115 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
119 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
123 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
127 return Z3_get_bv_sort_size(Context.Context, Sort);
131 return Z3_fpa_get_ebits(Context.Context, Sort) +
132 Z3_fpa_get_sbits(Context.Context, Sort);
136 return Z3_is_eq_sort(Context.Context, Sort,
141 OS << Z3_sort_to_string(Context.Context, Sort);
152 Z3Context &Context;
157 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
158 Z3_inc_ref(Context.Context, AST);
162 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
163 Z3_inc_ref(Context.Context, AST);
169 Z3_inc_ref(Context.Context, Other.AST);
170 Z3_dec_ref(Context.Context, AST);
180 Z3_dec_ref(Context.Context, AST);
184 ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
189 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
190 Z3_get_sort(Context.Context,
193 return Z3_is_eq_ast(Context.Context, AST,
198 OS << Z3_ast_to_string(Context.Context, AST);
209 Z3Context &Context;
214 Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
215 Z3_model_inc_ref(Context.Context, Model);
225 Z3_model_dec_ref(Context.Context, Model);
229 OS << Z3_model_to_string(Context.Context, Model);
268 Z3Context Context;
271 Z3_solver S = Z3_mk_simple_solver(Context.Context);
272 Z3_solver_inc_ref(Context.Context, S);
277 Z3_params P = Z3_mk_params(Context.Context);
278 Z3_params_inc_ref(Context.Context, P);
296 Z3_params_dec_ref(Context.Context, Params);
297 Z3_solver_dec_ref(Context.Context, Solver);
301 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
319 return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
324 Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
329 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
333 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
337 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
341 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
345 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
350 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
355 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
360 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
365 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
371 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
377 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
383 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
389 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
395 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
401 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
407 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
413 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
419 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
425 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
431 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
437 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
443 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
449 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
455 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
461 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
467 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
473 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
479 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
485 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
491 return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
496 return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
501 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
507 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
512 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
517 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
522 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
527 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
533 Z3Expr(Context,
534 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
541 Z3Expr(Context,
542 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
548 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
555 Z3Expr(Context,
556 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
563 Z3Expr(Context,
564 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
570 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
576 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
582 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
588 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
594 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
601 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
607 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
612 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
617 return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
626 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
635 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
644 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
653 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
662 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
670 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
678 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
687 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
693 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
700 Context,
701 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
708 Context,
709 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
716 Context,
717 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
724 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
731 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
736 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
737 : Z3_mk_false(Context.Context)));
748 Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));
757 ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)
758 : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);
759 return newExprRef(Z3Expr(Context, Literal));
769 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
775 Z3Expr(Context, Z3_mk_const(Context.Context,
776 Z3_mk_string_symbol(Context.Context, Name),
784 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
790 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
795 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
858 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
860 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
861 if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
865 Z3Expr(Context,
866 Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
872 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
874 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
875 if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE)
879 Z3Expr(Context,
880 Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
886 Z3_solver_set_params(Context.Context, Solver, Params);
887 Z3_lbool res = Z3_solver_check(Context.Context, Solver);
897 void push() override { return Z3_solver_push(Context.Context, Solver); }
900 assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
901 return Z3_solver_pop(Context.Context, Solver, NumStates);
907 void reset() override { Z3_solver_reset(Context.Context, Solver); }
910 OS << Z3_solver_to_string(Context.Context, Solver);
914 Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str());
915 Z3_params_set_uint(Context.Context, Params, Sym, Value);
919 Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str());
920 Z3_params_set_bool(Context.Context, Params, Sym, Value);
956 auto const &C = Context.Context;