9 #include "llvm/Config/config.h"
27 friend class Z3Context;
32 Z3Config() : Config(Z3_mk_config()) {
34 Z3_set_param_value(Config,
"model",
"true");
36 Z3_set_param_value(Config,
"proof",
"false");
38 Z3_set_param_value(Config,
"timeout",
"15000");
41 ~Z3Config() { Z3_del_config(Config); }
45 void Z3ErrorHandler(Z3_context
Context, Z3_error_code
Error) {
56 Context = Z3_mk_context_rc(Z3Config().Config);
59 Z3_set_error_handler(
Context, Z3ErrorHandler);
62 virtual ~Z3Context() {
70 friend class Z3Solver;
78 Z3Sort(Z3Context &
C, Z3_sort ZS) :
Context(
C), Sort(ZS) {
79 Z3_inc_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
84 Z3_inc_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
89 Z3Sort &operator=(
const Z3Sort &
Other) {
90 Z3_inc_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(
Other.Sort));
91 Z3_dec_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
96 Z3Sort(Z3Sort &&
Other) =
delete;
97 Z3Sort &operator=(Z3Sort &&
Other) =
delete;
101 Z3_dec_ref(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
106 Z3_get_ast_id(
Context.Context,
reinterpret_cast<Z3_ast
>(Sort)));
109 bool isBitvectorSortImpl()
const override {
110 return (Z3_get_sort_kind(
Context.Context, Sort) == Z3_BV_SORT);
113 bool isFloatSortImpl()
const override {
114 return (Z3_get_sort_kind(
Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
117 bool isBooleanSortImpl()
const override {
118 return (Z3_get_sort_kind(
Context.Context, Sort) == Z3_BOOL_SORT);
121 unsigned getBitvectorSortSizeImpl()
const override {
122 return Z3_get_bv_sort_size(
Context.Context, Sort);
125 unsigned getFloatSortSizeImpl()
const override {
126 return Z3_fpa_get_ebits(
Context.Context, Sort) +
127 Z3_fpa_get_sbits(
Context.Context, Sort);
131 return Z3_is_eq_sort(
Context.Context, Sort,
132 static_cast<const Z3Sort &
>(
Other).Sort);
136 OS << Z3_sort_to_string(
Context.Context, Sort);
140 static const Z3Sort &toZ3Sort(
const SMTSort &
S) {
141 return static_cast<const Z3Sort &
>(
S);
144 class Z3Expr :
public SMTExpr {
145 friend class Z3Solver;
153 Z3_inc_ref(
Context.Context, AST);
158 Z3_inc_ref(
Context.Context, AST);
163 Z3Expr &operator=(
const Z3Expr &
Other) {
165 Z3_dec_ref(
Context.Context, AST);
170 Z3Expr(Z3Expr &&
Other) =
delete;
171 Z3Expr &operator=(Z3Expr &&
Other) =
delete;
175 Z3_dec_ref(
Context.Context, AST);
179 ID.AddInteger(Z3_get_ast_id(
Context.Context, AST));
186 static_cast<const Z3Expr &
>(
Other).AST)) &&
187 "AST's must have the same sort");
188 return Z3_is_eq_ast(
Context.Context, AST,
189 static_cast<const Z3Expr &
>(
Other).AST);
193 OS << Z3_ast_to_string(
Context.Context, AST);
197 static const Z3Expr &toZ3Expr(
const SMTExpr &
E) {
198 return static_cast<const Z3Expr &
>(
E);
202 friend class Z3Solver;
213 Z3Model(
const Z3Model &
Other) =
delete;
214 Z3Model(Z3Model &&
Other) =
delete;
215 Z3Model &operator=(Z3Model &
Other) =
delete;
216 Z3Model &operator=(Z3Model &&
Other) =
delete;
261 friend class Z3ConstraintManager;
268 std::set<Z3Sort> CachedSorts;
271 std::set<Z3Expr> CachedExprs;
275 Z3_solver_inc_ref(
Context.Context, Solver);
278 Z3Solver(
const Z3Solver &
Other) =
delete;
279 Z3Solver(Z3Solver &&
Other) =
delete;
280 Z3Solver &operator=(Z3Solver &
Other) =
delete;
281 Z3Solver &operator=(Z3Solver &&
Other) =
delete;
285 Z3_solver_dec_ref(
Context.Context, Solver);
288 void addConstraint(
const SMTExprRef &Exp)
const override {
289 Z3_solver_assert(
Context.Context, Solver, toZ3Expr(*Exp).AST);
295 auto It = CachedSorts.insert(toZ3Sort(Sort));
302 auto It = CachedExprs.insert(toZ3Expr(Exp));
307 return newSortRef(Z3Sort(
Context, Z3_mk_bool_sort(
Context.Context)));
317 Z3Sort(
Context, Z3_get_sort(
Context.Context, toZ3Expr(*Exp).AST)));
321 return newSortRef(Z3Sort(
Context, Z3_mk_fpa_sort_16(
Context.Context)));
325 return newSortRef(Z3Sort(
Context, Z3_mk_fpa_sort_32(
Context.Context)));
329 return newSortRef(Z3Sort(
Context, Z3_mk_fpa_sort_64(
Context.Context)));
333 return newSortRef(Z3Sort(
Context, Z3_mk_fpa_sort_128(
Context.Context)));
338 Z3Expr(
Context, Z3_mk_bvneg(
Context.Context, toZ3Expr(*Exp).AST)));
343 Z3Expr(
Context, Z3_mk_bvnot(
Context.Context, toZ3Expr(*Exp).AST)));
354 toZ3Expr(*RHS).AST)));
360 toZ3Expr(*RHS).AST)));
366 toZ3Expr(*RHS).AST)));
372 toZ3Expr(*RHS).AST)));
378 toZ3Expr(*RHS).AST)));
384 toZ3Expr(*RHS).AST)));
390 toZ3Expr(*RHS).AST)));
396 toZ3Expr(*RHS).AST)));
402 toZ3Expr(*RHS).AST)));
408 toZ3Expr(*RHS).AST)));
414 toZ3Expr(*RHS).AST)));
420 toZ3Expr(*RHS).AST)));
426 toZ3Expr(*RHS).AST)));
432 toZ3Expr(*RHS).AST)));
438 toZ3Expr(*RHS).AST)));
444 toZ3Expr(*RHS).AST)));
450 toZ3Expr(*RHS).AST)));
456 toZ3Expr(*RHS).AST)));
462 toZ3Expr(*RHS).AST)));
468 toZ3Expr(*RHS).AST)));
474 toZ3Expr(*RHS).AST)));
478 Z3_ast
Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
483 Z3_ast
Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
490 toZ3Expr(*RHS).AST)));
495 Z3Expr(
Context, Z3_mk_fpa_neg(
Context.Context, toZ3Expr(*Exp).AST)));
499 return newExprRef(Z3Expr(
500 Context, Z3_mk_fpa_is_infinite(
Context.Context, toZ3Expr(*Exp).AST)));
505 Z3Expr(
Context, Z3_mk_fpa_is_nan(
Context.Context, toZ3Expr(*Exp).AST)));
509 return newExprRef(Z3Expr(
510 Context, Z3_mk_fpa_is_normal(
Context.Context, toZ3Expr(*Exp).AST)));
514 return newExprRef(Z3Expr(
515 Context, Z3_mk_fpa_is_zero(
Context.Context, toZ3Expr(*Exp).AST)));
522 Z3_mk_fpa_mul(
Context.Context, toZ3Expr(*RoundingMode).AST,
523 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
530 Z3_mk_fpa_div(
Context.Context, toZ3Expr(*RoundingMode).AST,
531 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
536 Z3Expr(
Context, Z3_mk_fpa_rem(
Context.Context, toZ3Expr(*LHS).AST,
537 toZ3Expr(*RHS).AST)));
544 Z3_mk_fpa_add(
Context.Context, toZ3Expr(*RoundingMode).AST,
545 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
552 Z3_mk_fpa_sub(
Context.Context, toZ3Expr(*RoundingMode).AST,
553 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
559 toZ3Expr(*RHS).AST)));
565 toZ3Expr(*RHS).AST)));
570 Z3Expr(
Context, Z3_mk_fpa_leq(
Context.Context, toZ3Expr(*LHS).AST,
571 toZ3Expr(*RHS).AST)));
576 Z3Expr(
Context, Z3_mk_fpa_geq(
Context.Context, toZ3Expr(*LHS).AST,
577 toZ3Expr(*RHS).AST)));
583 toZ3Expr(*RHS).AST)));
590 toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
594 return newExprRef(Z3Expr(
599 return newExprRef(Z3Expr(
606 toZ3Expr(*Exp).AST)));
612 bool isSigned)
override {
613 return newExprRef(Z3Expr(
614 Context, Z3_mk_bvadd_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
615 toZ3Expr(*RHS).AST, isSigned)));
622 return newExprRef(Z3Expr(
623 Context, Z3_mk_bvadd_no_underflow(
Context.Context, toZ3Expr(*LHS).AST,
624 toZ3Expr(*RHS).AST)));
631 return newExprRef(Z3Expr(
632 Context, Z3_mk_bvsub_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
633 toZ3Expr(*RHS).AST)));
639 bool isSigned)
override {
640 return newExprRef(Z3Expr(
641 Context, Z3_mk_bvsub_no_underflow(
Context.Context, toZ3Expr(*LHS).AST,
642 toZ3Expr(*RHS).AST, isSigned)));
649 return newExprRef(Z3Expr(
650 Context, Z3_mk_bvsdiv_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
651 toZ3Expr(*RHS).AST)));
657 return newExprRef(Z3Expr(
658 Context, Z3_mk_bvneg_no_overflow(
Context.Context, toZ3Expr(*Exp).AST)));
664 bool isSigned)
override {
665 return newExprRef(Z3Expr(
666 Context, Z3_mk_bvmul_no_overflow(
Context.Context, toZ3Expr(*LHS).AST,
667 toZ3Expr(*RHS).AST, isSigned)));
674 return newExprRef(Z3Expr(
675 Context, Z3_mk_bvmul_no_underflow(
Context.Context, toZ3Expr(*LHS).AST,
676 toZ3Expr(*RHS).AST)));
682 toZ3Expr(*RHS).AST)));
687 return newExprRef(Z3Expr(
689 Z3_mk_fpa_to_fp_float(
Context.Context, toZ3Expr(*RoundingMode).AST,
690 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
695 return newExprRef(Z3Expr(
697 Z3_mk_fpa_to_fp_signed(
Context.Context, toZ3Expr(*RoundingMode).AST,
698 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
703 return newExprRef(Z3Expr(
705 Z3_mk_fpa_to_fp_unsigned(
Context.Context, toZ3Expr(*RoundingMode).AST,
706 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
711 return newExprRef(Z3Expr(
712 Context, Z3_mk_fpa_to_sbv(
Context.Context, toZ3Expr(*RoundingMode).AST,
713 toZ3Expr(*From).AST, ToWidth)));
718 return newExprRef(Z3Expr(
719 Context, Z3_mk_fpa_to_ubv(
Context.Context, toZ3Expr(*RoundingMode).AST,
720 toZ3Expr(*From).AST, ToWidth)));
725 : Z3_mk_false(
Context.Context)));
729 const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(
BitWidth)).Sort;
734 Int.toString(Buffer, 10);
735 return newExprRef(Z3Expr(
739 const int64_t BitReprAsSigned =
Int.getExtValue();
741 reinterpret_cast<const uint64_t &
>(BitReprAsSigned);
745 ? Z3_mk_int64(
Context.Context, BitReprAsSigned, Z3Sort)
746 : Z3_mk_unsigned_int64(
Context.
Context, BitReprAsUnsigned, Z3Sort);
747 return newExprRef(Z3Expr(
Context, Literal));
756 return newExprRef(Z3Expr(
757 Context, Z3_mk_fpa_to_fp_bv(
Context.Context, toZ3Expr(*Z3Int).AST,
758 toZ3Sort(*Sort).Sort)));
765 toZ3Sort(*Sort).Sort)));
769 bool isUnsigned)
override {
772 Z3_get_numeral_string(
Context.Context, toZ3Expr(*Exp).AST),
777 bool getBoolean(
const SMTExprRef &Exp)
override {
778 return Z3_get_bool_value(
Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
783 return newExprRef(Z3Expr(
Context, Z3_mk_fpa_rne(
Context.Context)));
794 if (!toAPSInt(BVSort, AST,
Int,
true)) {
798 if (useSemantics && !areEquivalent(
Float.getSemantics(), Semantics)) {
799 assert(
false &&
"Floating-point types don't match!");
811 assert(
false &&
"Bitvector types don't match!");
823 Int = getBitvector(AST,
Int.getBitWidth(),
Int.isUnsigned());
827 assert(
false &&
"Bitwidth not supported!");
832 if (useSemantics &&
Int.getBitWidth() < 1) {
833 assert(
false &&
"Boolean type doesn't match!");
847 Z3_func_decl
Func = Z3_get_app_decl(
849 if (Z3_model_has_interp(
Context.Context,
Model.Model, Func) != Z3_L_TRUE)
854 Z3_model_get_const_interp(
Context.Context,
Model.Model, Func)));
856 return toAPSInt(Sort, Assign,
Int,
true);
861 Z3_func_decl
Func = Z3_get_app_decl(
863 if (Z3_model_has_interp(
Context.Context,
Model.Model, Func) != Z3_L_TRUE)
868 Z3_model_get_const_interp(
Context.Context,
Model.Model, Func)));
870 return toAPFloat(Sort, Assign,
Float,
true);
874 Z3_lbool res = Z3_solver_check(
Context.Context, Solver);
875 if (res == Z3_L_TRUE)
878 if (res == Z3_L_FALSE)
884 void push()
override {
return Z3_solver_push(
Context.Context, Solver); }
886 void pop(
unsigned NumStates = 1)
override {
887 assert(Z3_solver_get_num_scopes(
Context.Context, Solver) >= NumStates);
888 return Z3_solver_pop(
Context.Context, Solver, NumStates);
891 bool isFPSupported()
override {
return true; }
894 void reset()
override { Z3_solver_reset(
Context.Context, Solver); }
897 OS << Z3_solver_to_string(
Context.Context, Solver);
907 return std::make_unique<Z3Solver>();
910 "with -DLLVM_ENABLE_Z3_SOLVER=ON",