Lines Matching refs:Context
43 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) { in Z3ErrorHandler() argument
45 llvm::Twine(Z3_get_error_msg(Context, Error))); in Z3ErrorHandler()
51 Z3_context Context; member in __anonca7d1dd80111::Z3Context
54 Context = Z3_mk_context_rc(Z3Config().Config); in Z3Context()
57 Z3_set_error_handler(Context, Z3ErrorHandler); in Z3Context()
61 Z3_del_context(Context); in ~Z3Context()
62 Context = nullptr; in ~Z3Context()
70 Z3Context &Context; member in __anonca7d1dd80111::Z3Sort
76 Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) { in Z3Sort()
77 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); in Z3Sort()
81 Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) { in Z3Sort()
82 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); in Z3Sort()
88 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort)); in operator =()
89 Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); in operator =()
99 Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort)); in ~Z3Sort()
104 Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort))); in Profile()
108 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT); in isBitvectorSortImpl()
112 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT); in isFloatSortImpl()
116 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT); in isBooleanSortImpl()
120 return Z3_get_bv_sort_size(Context.Context, Sort); in getBitvectorSortSizeImpl()
124 return Z3_fpa_get_ebits(Context.Context, Sort) + in getFloatSortSizeImpl()
125 Z3_fpa_get_sbits(Context.Context, Sort); in getFloatSortSizeImpl()
129 return Z3_is_eq_sort(Context.Context, Sort, in equal_to()
134 OS << Z3_sort_to_string(Context.Context, Sort); in print()
145 Z3Context &Context; member in __anonca7d1dd80111::Z3Expr
150 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) { in Z3Expr()
151 Z3_inc_ref(Context.Context, AST); in Z3Expr()
155 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) { in Z3Expr()
156 Z3_inc_ref(Context.Context, AST); in Z3Expr()
162 Z3_inc_ref(Context.Context, Other.AST); in operator =()
163 Z3_dec_ref(Context.Context, AST); in operator =()
173 Z3_dec_ref(Context.Context, AST); in ~Z3Expr()
177 ID.AddInteger(Z3_get_ast_id(Context.Context, AST)); in Profile()
182 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST), in equal_to()
183 Z3_get_sort(Context.Context, in equal_to()
186 return Z3_is_eq_ast(Context.Context, AST, in equal_to()
191 OS << Z3_ast_to_string(Context.Context, AST); in print()
202 Z3Context &Context; member in __anonca7d1dd80111::Z3Model
207 Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) { in Z3Model()
208 Z3_model_inc_ref(Context.Context, Model); in Z3Model()
218 Z3_model_dec_ref(Context.Context, Model); in ~Z3Model()
222 OS << Z3_model_to_string(Context.Context, Model); in print()
261 Z3Context Context; member in __anonca7d1dd80111::Z3Solver
272 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { in Z3Solver()
273 Z3_solver_inc_ref(Context.Context, Solver); in Z3Solver()
283 Z3_solver_dec_ref(Context.Context, Solver); in ~Z3Solver()
287 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
305 return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context))); in getBoolSort()
310 Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth))); in getBitvectorSort()
315 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST))); in getSort()
319 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context))); in getFloat16Sort()
323 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context))); in getFloat32Sort()
327 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context))); in getFloat64Sort()
331 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context))); in getFloat128Sort()
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()
357 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST, in mkBVSub()
363 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST, in mkBVMul()
369 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST, in mkBVSRem()
375 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST, in mkBVURem()
381 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDiv()
387 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST, in mkBVUDiv()
393 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST, in mkBVShl()
399 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST, in mkBVAshr()
405 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST, in mkBVLshr()
411 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST, in mkBVXor()
417 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST, in mkBVOr()
423 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST, in mkBVAnd()
429 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST, in mkBVUlt()
435 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSlt()
441 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST, in mkBVUgt()
447 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST, in mkBVSgt()
453 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST, in mkBVUle()
459 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST, in mkBVSle()
465 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST, in mkBVUge()
471 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST, in mkBVSge()
477 return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args))); in mkAnd()
482 return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args))); in mkOr()
487 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST, in mkEqual()
493 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST))); in mkFPNeg()
498 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsInfinite()
503 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsNaN()
508 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsNormal()
513 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST))); in mkFPIsZero()
519 Z3Expr(Context, in mkFPMul()
520 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPMul()
527 Z3Expr(Context, in mkFPDiv()
528 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPDiv()
534 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST, in mkFPRem()
541 Z3Expr(Context, in mkFPAdd()
542 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPAdd()
549 Z3Expr(Context, in mkFPSub()
550 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPSub()
556 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST, in mkFPLt()
562 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST, in mkFPGt()
568 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST, in mkFPLe()
574 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST, in mkFPGe()
580 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST, in mkFPEqual()
587 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST, in mkIte()
593 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST))); in mkBVSignExt()
598 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST))); in mkBVZeroExt()
603 return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low, in mkBVExtract()
612 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoOverflow()
621 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVAddNoUnderflow()
630 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoOverflow()
639 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSubNoUnderflow()
648 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVSDivNoOverflow()
656 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST))); in mkBVNegNoOverflow()
664 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoOverflow()
673 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST, in mkBVMulNoUnderflow()
679 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST, in mkBVConcat()
686 Context, in mkFPtoFP()
687 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoFP()
694 Context, in mkSBVtoFP()
695 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST, in mkSBVtoFP()
702 Context, in mkUBVtoFP()
703 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST, in mkUBVtoFP()
710 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoSBV()
717 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST, in mkFPtoUBV()
722 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context) in mkBoolean()
723 : Z3_mk_false(Context.Context))); in mkBoolean()
734 Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort))); in mkBitvector()
743 ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort) in mkBitvector()
744 : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort); in mkBitvector()
745 return newExprRef(Z3Expr(Context, Literal)); in mkBitvector()
755 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST, in mkFloat()
761 Z3Expr(Context, Z3_mk_const(Context.Context, in mkSymbol()
762 Z3_mk_string_symbol(Context.Context, Name), in mkSymbol()
770 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST), in getBitvector()
776 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE; in getBoolean()
781 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context))); in getFloatRoundingMode()
844 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
846 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); in getInterpretation()
847 if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) in getInterpretation()
851 Z3Expr(Context, in getInterpretation()
852 Z3_model_get_const_interp(Context.Context, Model.Model, Func))); in getInterpretation()
858 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
860 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST)); in getInterpretation()
861 if (Z3_model_has_interp(Context.Context, Model.Model, Func) != Z3_L_TRUE) in getInterpretation()
865 Z3Expr(Context, in getInterpretation()
866 Z3_model_get_const_interp(Context.Context, Model.Model, Func))); in getInterpretation()
872 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
882 void push() override { return Z3_solver_push(Context.Context, Solver); } in push()
885 assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates); in pop()
886 return Z3_solver_pop(Context.Context, Solver, NumStates); in pop()
892 void reset() override { Z3_solver_reset(Context.Context, Solver); } in reset()
895 OS << Z3_solver_to_string(Context.Context, Solver); in print()