1 //== Z3Solver.cpp -----------------------------------------------*- C++ -*--==//
2 //
3 // Part of the LLVM Project, under the Apache License v2.0 with LLVM Exceptions.
4 // See https://llvm.org/LICENSE.txt for license information.
5 // SPDX-License-Identifier: Apache-2.0 WITH LLVM-exception
6 //
7 //===----------------------------------------------------------------------===//
8
9 #include "llvm/ADT/ScopeExit.h"
10 #include "llvm/Config/config.h"
11 #include "llvm/Support/NativeFormatting.h"
12 #include "llvm/Support/SMTAPI.h"
13
14 using namespace llvm;
15
16 #if LLVM_WITH_Z3
17
18 #include "llvm/ADT/SmallString.h"
19 #include "llvm/ADT/Twine.h"
20
21 #include <set>
22 #include <unordered_map>
23
24 #include <z3.h>
25
26 namespace {
27
28 /// Configuration class for Z3
29 class Z3Config {
30 friend class Z3Context;
31
32 Z3_config Config = Z3_mk_config();
33
34 public:
35 Z3Config() = default;
36 Z3Config(const Z3Config &) = delete;
37 Z3Config(Z3Config &&) = default;
38 Z3Config &operator=(Z3Config &) = delete;
39 Z3Config &operator=(Z3Config &&) = default;
~Z3Config()40 ~Z3Config() { Z3_del_config(Config); }
41 }; // end class Z3Config
42
43 // Function used to report errors
Z3ErrorHandler(Z3_context Context,Z3_error_code Error)44 void Z3ErrorHandler(Z3_context Context, Z3_error_code Error) {
45 llvm::report_fatal_error("Z3 error: " +
46 llvm::Twine(Z3_get_error_msg(Context, Error)));
47 }
48
49 /// Wrapper for Z3 context
50 class Z3Context {
51 public:
52 Z3Config Config;
53 Z3_context Context;
54
Z3Context()55 Z3Context() {
56 Context = Z3_mk_context_rc(Config.Config);
57 // The error function is set here because the context is the first object
58 // created by the backend
59 Z3_set_error_handler(Context, Z3ErrorHandler);
60 }
61
62 Z3Context(const Z3Context &) = delete;
63 Z3Context(Z3Context &&) = default;
64 Z3Context &operator=(Z3Context &) = delete;
65 Z3Context &operator=(Z3Context &&) = default;
66
~Z3Context()67 ~Z3Context() {
68 Z3_del_context(Context);
69 Context = nullptr;
70 }
71 }; // end class Z3Context
72
73 /// Wrapper for Z3 Sort
74 class Z3Sort : public SMTSort {
75 friend class Z3Solver;
76
77 Z3Context &Context;
78
79 Z3_sort Sort;
80
81 public:
82 /// Default constructor, mainly used by make_shared
Z3Sort(Z3Context & C,Z3_sort ZS)83 Z3Sort(Z3Context &C, Z3_sort ZS) : Context(C), Sort(ZS) {
84 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
85 }
86
87 /// Override implicit copy constructor for correct reference counting.
Z3Sort(const Z3Sort & Other)88 Z3Sort(const Z3Sort &Other) : Context(Other.Context), Sort(Other.Sort) {
89 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
90 }
91
92 /// Override implicit copy assignment constructor for correct reference
93 /// counting.
operator =(const Z3Sort & Other)94 Z3Sort &operator=(const Z3Sort &Other) {
95 Z3_inc_ref(Context.Context, reinterpret_cast<Z3_ast>(Other.Sort));
96 Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
97 Sort = Other.Sort;
98 return *this;
99 }
100
101 Z3Sort(Z3Sort &&Other) = delete;
102 Z3Sort &operator=(Z3Sort &&Other) = delete;
103
~Z3Sort()104 ~Z3Sort() {
105 if (Sort)
106 Z3_dec_ref(Context.Context, reinterpret_cast<Z3_ast>(Sort));
107 }
108
Profile(llvm::FoldingSetNodeID & ID) const109 void Profile(llvm::FoldingSetNodeID &ID) const override {
110 ID.AddInteger(
111 Z3_get_ast_id(Context.Context, reinterpret_cast<Z3_ast>(Sort)));
112 }
113
isBitvectorSortImpl() const114 bool isBitvectorSortImpl() const override {
115 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
116 }
117
isFloatSortImpl() const118 bool isFloatSortImpl() const override {
119 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
120 }
121
isBooleanSortImpl() const122 bool isBooleanSortImpl() const override {
123 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
124 }
125
getBitvectorSortSizeImpl() const126 unsigned getBitvectorSortSizeImpl() const override {
127 return Z3_get_bv_sort_size(Context.Context, Sort);
128 }
129
getFloatSortSizeImpl() const130 unsigned getFloatSortSizeImpl() const override {
131 return Z3_fpa_get_ebits(Context.Context, Sort) +
132 Z3_fpa_get_sbits(Context.Context, Sort);
133 }
134
equal_to(SMTSort const & Other) const135 bool equal_to(SMTSort const &Other) const override {
136 return Z3_is_eq_sort(Context.Context, Sort,
137 static_cast<const Z3Sort &>(Other).Sort);
138 }
139
print(raw_ostream & OS) const140 void print(raw_ostream &OS) const override {
141 OS << Z3_sort_to_string(Context.Context, Sort);
142 }
143 }; // end class Z3Sort
144
toZ3Sort(const SMTSort & S)145 static const Z3Sort &toZ3Sort(const SMTSort &S) {
146 return static_cast<const Z3Sort &>(S);
147 }
148
149 class Z3Expr : public SMTExpr {
150 friend class Z3Solver;
151
152 Z3Context &Context;
153
154 Z3_ast AST;
155
156 public:
Z3Expr(Z3Context & C,Z3_ast ZA)157 Z3Expr(Z3Context &C, Z3_ast ZA) : SMTExpr(), Context(C), AST(ZA) {
158 Z3_inc_ref(Context.Context, AST);
159 }
160
161 /// Override implicit copy constructor for correct reference counting.
Z3Expr(const Z3Expr & Copy)162 Z3Expr(const Z3Expr &Copy) : SMTExpr(), Context(Copy.Context), AST(Copy.AST) {
163 Z3_inc_ref(Context.Context, AST);
164 }
165
166 /// Override implicit copy assignment constructor for correct reference
167 /// counting.
operator =(const Z3Expr & Other)168 Z3Expr &operator=(const Z3Expr &Other) {
169 Z3_inc_ref(Context.Context, Other.AST);
170 Z3_dec_ref(Context.Context, AST);
171 AST = Other.AST;
172 return *this;
173 }
174
175 Z3Expr(Z3Expr &&Other) = delete;
176 Z3Expr &operator=(Z3Expr &&Other) = delete;
177
~Z3Expr()178 ~Z3Expr() {
179 if (AST)
180 Z3_dec_ref(Context.Context, AST);
181 }
182
Profile(llvm::FoldingSetNodeID & ID) const183 void Profile(llvm::FoldingSetNodeID &ID) const override {
184 ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
185 }
186
187 /// Comparison of AST equality, not model equivalence.
equal_to(SMTExpr const & Other) const188 bool equal_to(SMTExpr const &Other) const override {
189 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
190 Z3_get_sort(Context.Context,
191 static_cast<const Z3Expr &>(Other).AST)) &&
192 "AST's must have the same sort");
193 return Z3_is_eq_ast(Context.Context, AST,
194 static_cast<const Z3Expr &>(Other).AST);
195 }
196
print(raw_ostream & OS) const197 void print(raw_ostream &OS) const override {
198 OS << Z3_ast_to_string(Context.Context, AST);
199 }
200 }; // end class Z3Expr
201
toZ3Expr(const SMTExpr & E)202 static const Z3Expr &toZ3Expr(const SMTExpr &E) {
203 return static_cast<const Z3Expr &>(E);
204 }
205
206 class Z3Model {
207 friend class Z3Solver;
208
209 Z3Context &Context;
210
211 Z3_model Model;
212
213 public:
Z3Model(Z3Context & C,Z3_model ZM)214 Z3Model(Z3Context &C, Z3_model ZM) : Context(C), Model(ZM) {
215 Z3_model_inc_ref(Context.Context, Model);
216 }
217
218 Z3Model(const Z3Model &Other) = delete;
219 Z3Model(Z3Model &&Other) = delete;
220 Z3Model &operator=(Z3Model &Other) = delete;
221 Z3Model &operator=(Z3Model &&Other) = delete;
222
~Z3Model()223 ~Z3Model() {
224 if (Model)
225 Z3_model_dec_ref(Context.Context, Model);
226 }
227
print(raw_ostream & OS) const228 void print(raw_ostream &OS) const {
229 OS << Z3_model_to_string(Context.Context, Model);
230 }
231
dump() const232 LLVM_DUMP_METHOD void dump() const { print(llvm::errs()); }
233 }; // end class Z3Model
234
235 /// Get the corresponding IEEE floating-point type for a given bitwidth.
getFloatSemantics(unsigned BitWidth)236 static const llvm::fltSemantics &getFloatSemantics(unsigned BitWidth) {
237 switch (BitWidth) {
238 default:
239 llvm_unreachable("Unsupported floating-point semantics!");
240 break;
241 case 16:
242 return llvm::APFloat::IEEEhalf();
243 case 32:
244 return llvm::APFloat::IEEEsingle();
245 case 64:
246 return llvm::APFloat::IEEEdouble();
247 case 128:
248 return llvm::APFloat::IEEEquad();
249 }
250 }
251
252 // Determine whether two float semantics are equivalent
areEquivalent(const llvm::fltSemantics & LHS,const llvm::fltSemantics & RHS)253 static bool areEquivalent(const llvm::fltSemantics &LHS,
254 const llvm::fltSemantics &RHS) {
255 return (llvm::APFloat::semanticsPrecision(LHS) ==
256 llvm::APFloat::semanticsPrecision(RHS)) &&
257 (llvm::APFloat::semanticsMinExponent(LHS) ==
258 llvm::APFloat::semanticsMinExponent(RHS)) &&
259 (llvm::APFloat::semanticsMaxExponent(LHS) ==
260 llvm::APFloat::semanticsMaxExponent(RHS)) &&
261 (llvm::APFloat::semanticsSizeInBits(LHS) ==
262 llvm::APFloat::semanticsSizeInBits(RHS));
263 }
264
265 class Z3Solver : public SMTSolver {
266 friend class Z3ConstraintManager;
267
268 Z3Context Context;
269
__anona2cc94240202null270 Z3_solver Solver = [this] {
271 Z3_solver S = Z3_mk_simple_solver(Context.Context);
272 Z3_solver_inc_ref(Context.Context, S);
273 return S;
274 }();
275
__anona2cc94240302null276 Z3_params Params = [this] {
277 Z3_params P = Z3_mk_params(Context.Context);
278 Z3_params_inc_ref(Context.Context, P);
279 return P;
280 }();
281
282 // Cache Sorts
283 std::set<Z3Sort> CachedSorts;
284
285 // Cache Exprs
286 std::set<Z3Expr> CachedExprs;
287
288 public:
289 Z3Solver() = default;
290 Z3Solver(const Z3Solver &Other) = delete;
291 Z3Solver(Z3Solver &&Other) = delete;
292 Z3Solver &operator=(Z3Solver &Other) = delete;
293 Z3Solver &operator=(Z3Solver &&Other) = delete;
294
~Z3Solver()295 ~Z3Solver() override {
296 Z3_params_dec_ref(Context.Context, Params);
297 Z3_solver_dec_ref(Context.Context, Solver);
298 }
299
addConstraint(const SMTExprRef & Exp) const300 void addConstraint(const SMTExprRef &Exp) const override {
301 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
302 }
303
304 // Given an SMTSort, adds/retrives it from the cache and returns
305 // an SMTSortRef to the SMTSort in the cache
newSortRef(const SMTSort & Sort)306 SMTSortRef newSortRef(const SMTSort &Sort) {
307 auto It = CachedSorts.insert(toZ3Sort(Sort));
308 return &(*It.first);
309 }
310
311 // Given an SMTExpr, adds/retrives it from the cache and returns
312 // an SMTExprRef to the SMTExpr in the cache
newExprRef(const SMTExpr & Exp)313 SMTExprRef newExprRef(const SMTExpr &Exp) {
314 auto It = CachedExprs.insert(toZ3Expr(Exp));
315 return &(*It.first);
316 }
317
getBoolSort()318 SMTSortRef getBoolSort() override {
319 return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
320 }
321
getBitvectorSort(unsigned BitWidth)322 SMTSortRef getBitvectorSort(unsigned BitWidth) override {
323 return newSortRef(
324 Z3Sort(Context, Z3_mk_bv_sort(Context.Context, BitWidth)));
325 }
326
getSort(const SMTExprRef & Exp)327 SMTSortRef getSort(const SMTExprRef &Exp) override {
328 return newSortRef(
329 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
330 }
331
getFloat16Sort()332 SMTSortRef getFloat16Sort() override {
333 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
334 }
335
getFloat32Sort()336 SMTSortRef getFloat32Sort() override {
337 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
338 }
339
getFloat64Sort()340 SMTSortRef getFloat64Sort() override {
341 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
342 }
343
getFloat128Sort()344 SMTSortRef getFloat128Sort() override {
345 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
346 }
347
mkBVNeg(const SMTExprRef & Exp)348 SMTExprRef mkBVNeg(const SMTExprRef &Exp) override {
349 return newExprRef(
350 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
351 }
352
mkBVNot(const SMTExprRef & Exp)353 SMTExprRef mkBVNot(const SMTExprRef &Exp) override {
354 return newExprRef(
355 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
356 }
357
mkNot(const SMTExprRef & Exp)358 SMTExprRef mkNot(const SMTExprRef &Exp) override {
359 return newExprRef(
360 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
361 }
362
mkBVAdd(const SMTExprRef & LHS,const SMTExprRef & RHS)363 SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
364 return newExprRef(
365 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
366 toZ3Expr(*RHS).AST)));
367 }
368
mkBVSub(const SMTExprRef & LHS,const SMTExprRef & RHS)369 SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
370 return newExprRef(
371 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
372 toZ3Expr(*RHS).AST)));
373 }
374
mkBVMul(const SMTExprRef & LHS,const SMTExprRef & RHS)375 SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
376 return newExprRef(
377 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
378 toZ3Expr(*RHS).AST)));
379 }
380
mkBVSRem(const SMTExprRef & LHS,const SMTExprRef & RHS)381 SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
382 return newExprRef(
383 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
384 toZ3Expr(*RHS).AST)));
385 }
386
mkBVURem(const SMTExprRef & LHS,const SMTExprRef & RHS)387 SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
388 return newExprRef(
389 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
390 toZ3Expr(*RHS).AST)));
391 }
392
mkBVSDiv(const SMTExprRef & LHS,const SMTExprRef & RHS)393 SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
394 return newExprRef(
395 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
396 toZ3Expr(*RHS).AST)));
397 }
398
mkBVUDiv(const SMTExprRef & LHS,const SMTExprRef & RHS)399 SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
400 return newExprRef(
401 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
402 toZ3Expr(*RHS).AST)));
403 }
404
mkBVShl(const SMTExprRef & LHS,const SMTExprRef & RHS)405 SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
406 return newExprRef(
407 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
408 toZ3Expr(*RHS).AST)));
409 }
410
mkBVAshr(const SMTExprRef & LHS,const SMTExprRef & RHS)411 SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
412 return newExprRef(
413 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
414 toZ3Expr(*RHS).AST)));
415 }
416
mkBVLshr(const SMTExprRef & LHS,const SMTExprRef & RHS)417 SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
418 return newExprRef(
419 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
420 toZ3Expr(*RHS).AST)));
421 }
422
mkBVXor(const SMTExprRef & LHS,const SMTExprRef & RHS)423 SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
424 return newExprRef(
425 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
426 toZ3Expr(*RHS).AST)));
427 }
428
mkBVOr(const SMTExprRef & LHS,const SMTExprRef & RHS)429 SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
430 return newExprRef(
431 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
432 toZ3Expr(*RHS).AST)));
433 }
434
mkBVAnd(const SMTExprRef & LHS,const SMTExprRef & RHS)435 SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
436 return newExprRef(
437 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
438 toZ3Expr(*RHS).AST)));
439 }
440
mkBVUlt(const SMTExprRef & LHS,const SMTExprRef & RHS)441 SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
442 return newExprRef(
443 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
444 toZ3Expr(*RHS).AST)));
445 }
446
mkBVSlt(const SMTExprRef & LHS,const SMTExprRef & RHS)447 SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
448 return newExprRef(
449 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
450 toZ3Expr(*RHS).AST)));
451 }
452
mkBVUgt(const SMTExprRef & LHS,const SMTExprRef & RHS)453 SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
454 return newExprRef(
455 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
456 toZ3Expr(*RHS).AST)));
457 }
458
mkBVSgt(const SMTExprRef & LHS,const SMTExprRef & RHS)459 SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
460 return newExprRef(
461 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
462 toZ3Expr(*RHS).AST)));
463 }
464
mkBVUle(const SMTExprRef & LHS,const SMTExprRef & RHS)465 SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
466 return newExprRef(
467 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
468 toZ3Expr(*RHS).AST)));
469 }
470
mkBVSle(const SMTExprRef & LHS,const SMTExprRef & RHS)471 SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
472 return newExprRef(
473 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
474 toZ3Expr(*RHS).AST)));
475 }
476
mkBVUge(const SMTExprRef & LHS,const SMTExprRef & RHS)477 SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
478 return newExprRef(
479 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
480 toZ3Expr(*RHS).AST)));
481 }
482
mkBVSge(const SMTExprRef & LHS,const SMTExprRef & RHS)483 SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
484 return newExprRef(
485 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
486 toZ3Expr(*RHS).AST)));
487 }
488
mkAnd(const SMTExprRef & LHS,const SMTExprRef & RHS)489 SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
490 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
491 return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
492 }
493
mkOr(const SMTExprRef & LHS,const SMTExprRef & RHS)494 SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
495 Z3_ast Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
496 return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
497 }
498
mkEqual(const SMTExprRef & LHS,const SMTExprRef & RHS)499 SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
500 return newExprRef(
501 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
502 toZ3Expr(*RHS).AST)));
503 }
504
mkFPNeg(const SMTExprRef & Exp)505 SMTExprRef mkFPNeg(const SMTExprRef &Exp) override {
506 return newExprRef(
507 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
508 }
509
mkFPIsInfinite(const SMTExprRef & Exp)510 SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) override {
511 return newExprRef(Z3Expr(
512 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
513 }
514
mkFPIsNaN(const SMTExprRef & Exp)515 SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) override {
516 return newExprRef(
517 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
518 }
519
mkFPIsNormal(const SMTExprRef & Exp)520 SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) override {
521 return newExprRef(Z3Expr(
522 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
523 }
524
mkFPIsZero(const SMTExprRef & Exp)525 SMTExprRef mkFPIsZero(const SMTExprRef &Exp) override {
526 return newExprRef(Z3Expr(
527 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
528 }
529
mkFPMul(const SMTExprRef & LHS,const SMTExprRef & RHS)530 SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
531 SMTExprRef RoundingMode = getFloatRoundingMode();
532 return newExprRef(
533 Z3Expr(Context,
534 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
535 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
536 }
537
mkFPDiv(const SMTExprRef & LHS,const SMTExprRef & RHS)538 SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
539 SMTExprRef RoundingMode = getFloatRoundingMode();
540 return newExprRef(
541 Z3Expr(Context,
542 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
543 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
544 }
545
mkFPRem(const SMTExprRef & LHS,const SMTExprRef & RHS)546 SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
547 return newExprRef(
548 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
549 toZ3Expr(*RHS).AST)));
550 }
551
mkFPAdd(const SMTExprRef & LHS,const SMTExprRef & RHS)552 SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
553 SMTExprRef RoundingMode = getFloatRoundingMode();
554 return newExprRef(
555 Z3Expr(Context,
556 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
557 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
558 }
559
mkFPSub(const SMTExprRef & LHS,const SMTExprRef & RHS)560 SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
561 SMTExprRef RoundingMode = getFloatRoundingMode();
562 return newExprRef(
563 Z3Expr(Context,
564 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
565 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
566 }
567
mkFPLt(const SMTExprRef & LHS,const SMTExprRef & RHS)568 SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
569 return newExprRef(
570 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
571 toZ3Expr(*RHS).AST)));
572 }
573
mkFPGt(const SMTExprRef & LHS,const SMTExprRef & RHS)574 SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
575 return newExprRef(
576 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
577 toZ3Expr(*RHS).AST)));
578 }
579
mkFPLe(const SMTExprRef & LHS,const SMTExprRef & RHS)580 SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
581 return newExprRef(
582 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
583 toZ3Expr(*RHS).AST)));
584 }
585
mkFPGe(const SMTExprRef & LHS,const SMTExprRef & RHS)586 SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
587 return newExprRef(
588 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
589 toZ3Expr(*RHS).AST)));
590 }
591
mkFPEqual(const SMTExprRef & LHS,const SMTExprRef & RHS)592 SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
593 return newExprRef(
594 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
595 toZ3Expr(*RHS).AST)));
596 }
597
mkIte(const SMTExprRef & Cond,const SMTExprRef & T,const SMTExprRef & F)598 SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
599 const SMTExprRef &F) override {
600 return newExprRef(
601 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
602 toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
603 }
604
mkBVSignExt(unsigned i,const SMTExprRef & Exp)605 SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) override {
606 return newExprRef(Z3Expr(
607 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
608 }
609
mkBVZeroExt(unsigned i,const SMTExprRef & Exp)610 SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) override {
611 return newExprRef(Z3Expr(
612 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
613 }
614
mkBVExtract(unsigned High,unsigned Low,const SMTExprRef & Exp)615 SMTExprRef mkBVExtract(unsigned High, unsigned Low,
616 const SMTExprRef &Exp) override {
617 return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context, High, Low,
618 toZ3Expr(*Exp).AST)));
619 }
620
621 /// Creates a predicate that checks for overflow in a bitvector addition
622 /// operation
mkBVAddNoOverflow(const SMTExprRef & LHS,const SMTExprRef & RHS,bool isSigned)623 SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
624 bool isSigned) override {
625 return newExprRef(Z3Expr(
626 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
627 toZ3Expr(*RHS).AST, isSigned)));
628 }
629
630 /// Creates a predicate that checks for underflow in a signed bitvector
631 /// addition operation
mkBVAddNoUnderflow(const SMTExprRef & LHS,const SMTExprRef & RHS)632 SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS,
633 const SMTExprRef &RHS) override {
634 return newExprRef(Z3Expr(
635 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
636 toZ3Expr(*RHS).AST)));
637 }
638
639 /// Creates a predicate that checks for overflow in a signed bitvector
640 /// subtraction operation
mkBVSubNoOverflow(const SMTExprRef & LHS,const SMTExprRef & RHS)641 SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS,
642 const SMTExprRef &RHS) override {
643 return newExprRef(Z3Expr(
644 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
645 toZ3Expr(*RHS).AST)));
646 }
647
648 /// Creates a predicate that checks for underflow in a bitvector subtraction
649 /// operation
mkBVSubNoUnderflow(const SMTExprRef & LHS,const SMTExprRef & RHS,bool isSigned)650 SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
651 bool isSigned) override {
652 return newExprRef(Z3Expr(
653 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
654 toZ3Expr(*RHS).AST, isSigned)));
655 }
656
657 /// Creates a predicate that checks for overflow in a signed bitvector
658 /// division/modulus operation
mkBVSDivNoOverflow(const SMTExprRef & LHS,const SMTExprRef & RHS)659 SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS,
660 const SMTExprRef &RHS) override {
661 return newExprRef(Z3Expr(
662 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
663 toZ3Expr(*RHS).AST)));
664 }
665
666 /// Creates a predicate that checks for overflow in a bitvector negation
667 /// operation
mkBVNegNoOverflow(const SMTExprRef & Exp)668 SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) override {
669 return newExprRef(Z3Expr(
670 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
671 }
672
673 /// Creates a predicate that checks for overflow in a bitvector multiplication
674 /// operation
mkBVMulNoOverflow(const SMTExprRef & LHS,const SMTExprRef & RHS,bool isSigned)675 SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS,
676 bool isSigned) override {
677 return newExprRef(Z3Expr(
678 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
679 toZ3Expr(*RHS).AST, isSigned)));
680 }
681
682 /// Creates a predicate that checks for underflow in a signed bitvector
683 /// multiplication operation
mkBVMulNoUnderflow(const SMTExprRef & LHS,const SMTExprRef & RHS)684 SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS,
685 const SMTExprRef &RHS) override {
686 return newExprRef(Z3Expr(
687 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
688 toZ3Expr(*RHS).AST)));
689 }
690
mkBVConcat(const SMTExprRef & LHS,const SMTExprRef & RHS)691 SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS) override {
692 return newExprRef(
693 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
694 toZ3Expr(*RHS).AST)));
695 }
696
mkFPtoFP(const SMTExprRef & From,const SMTSortRef & To)697 SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
698 SMTExprRef RoundingMode = getFloatRoundingMode();
699 return newExprRef(Z3Expr(
700 Context,
701 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
702 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
703 }
704
mkSBVtoFP(const SMTExprRef & From,const SMTSortRef & To)705 SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
706 SMTExprRef RoundingMode = getFloatRoundingMode();
707 return newExprRef(Z3Expr(
708 Context,
709 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
710 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
711 }
712
mkUBVtoFP(const SMTExprRef & From,const SMTSortRef & To)713 SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {
714 SMTExprRef RoundingMode = getFloatRoundingMode();
715 return newExprRef(Z3Expr(
716 Context,
717 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
718 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
719 }
720
mkFPtoSBV(const SMTExprRef & From,unsigned ToWidth)721 SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) override {
722 SMTExprRef RoundingMode = getFloatRoundingMode();
723 return newExprRef(Z3Expr(
724 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
725 toZ3Expr(*From).AST, ToWidth)));
726 }
727
mkFPtoUBV(const SMTExprRef & From,unsigned ToWidth)728 SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) override {
729 SMTExprRef RoundingMode = getFloatRoundingMode();
730 return newExprRef(Z3Expr(
731 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
732 toZ3Expr(*From).AST, ToWidth)));
733 }
734
mkBoolean(const bool b)735 SMTExprRef mkBoolean(const bool b) override {
736 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
737 : Z3_mk_false(Context.Context)));
738 }
739
mkBitvector(const llvm::APSInt Int,unsigned BitWidth)740 SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) override {
741 const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(BitWidth)).Sort;
742
743 // Slow path, when 64 bits are not enough.
744 if (LLVM_UNLIKELY(!Int.isRepresentableByInt64())) {
745 SmallString<40> Buffer;
746 Int.toString(Buffer, 10);
747 return newExprRef(Z3Expr(
748 Context, Z3_mk_numeral(Context.Context, Buffer.c_str(), Z3Sort)));
749 }
750
751 const int64_t BitReprAsSigned = Int.getExtValue();
752 const uint64_t BitReprAsUnsigned =
753 reinterpret_cast<const uint64_t &>(BitReprAsSigned);
754
755 Z3_ast Literal =
756 Int.isSigned()
757 ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)
758 : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);
759 return newExprRef(Z3Expr(Context, Literal));
760 }
761
mkFloat(const llvm::APFloat Float)762 SMTExprRef mkFloat(const llvm::APFloat Float) override {
763 SMTSortRef Sort =
764 getFloatSort(llvm::APFloat::semanticsSizeInBits(Float.getSemantics()));
765
766 llvm::APSInt Int = llvm::APSInt(Float.bitcastToAPInt(), false);
767 SMTExprRef Z3Int = mkBitvector(Int, Int.getBitWidth());
768 return newExprRef(Z3Expr(
769 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
770 toZ3Sort(*Sort).Sort)));
771 }
772
mkSymbol(const char * Name,SMTSortRef Sort)773 SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {
774 return newExprRef(
775 Z3Expr(Context, Z3_mk_const(Context.Context,
776 Z3_mk_string_symbol(Context.Context, Name),
777 toZ3Sort(*Sort).Sort)));
778 }
779
getBitvector(const SMTExprRef & Exp,unsigned BitWidth,bool isUnsigned)780 llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
781 bool isUnsigned) override {
782 return llvm::APSInt(
783 llvm::APInt(BitWidth,
784 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
785 10),
786 isUnsigned);
787 }
788
getBoolean(const SMTExprRef & Exp)789 bool getBoolean(const SMTExprRef &Exp) override {
790 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
791 }
792
getFloatRoundingMode()793 SMTExprRef getFloatRoundingMode() override {
794 // TODO: Don't assume nearest ties to even rounding mode
795 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
796 }
797
toAPFloat(const SMTSortRef & Sort,const SMTExprRef & AST,llvm::APFloat & Float,bool useSemantics)798 bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,
799 llvm::APFloat &Float, bool useSemantics) {
800 assert(Sort->isFloatSort() && "Unsupported sort to floating-point!");
801
802 llvm::APSInt Int(Sort->getFloatSortSize(), true);
803 const llvm::fltSemantics &Semantics =
804 getFloatSemantics(Sort->getFloatSortSize());
805 SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());
806 if (!toAPSInt(BVSort, AST, Int, true)) {
807 return false;
808 }
809
810 if (useSemantics && !areEquivalent(Float.getSemantics(), Semantics)) {
811 assert(false && "Floating-point types don't match!");
812 return false;
813 }
814
815 Float = llvm::APFloat(Semantics, Int);
816 return true;
817 }
818
toAPSInt(const SMTSortRef & Sort,const SMTExprRef & AST,llvm::APSInt & Int,bool useSemantics)819 bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,
820 llvm::APSInt &Int, bool useSemantics) {
821 if (Sort->isBitvectorSort()) {
822 if (useSemantics && Int.getBitWidth() != Sort->getBitvectorSortSize()) {
823 assert(false && "Bitvector types don't match!");
824 return false;
825 }
826
827 // FIXME: This function is also used to retrieve floating-point values,
828 // which can be 16, 32, 64 or 128 bits long. Bitvectors can be anything
829 // between 1 and 64 bits long, which is the reason we have this weird
830 // guard. In the future, we need proper calls in the backend to retrieve
831 // floating-points and its special values (NaN, +/-infinity, +/-zero),
832 // then we can drop this weird condition.
833 if (Sort->getBitvectorSortSize() <= 64 ||
834 Sort->getBitvectorSortSize() == 128) {
835 Int = getBitvector(AST, Int.getBitWidth(), Int.isUnsigned());
836 return true;
837 }
838
839 assert(false && "Bitwidth not supported!");
840 return false;
841 }
842
843 if (Sort->isBooleanSort()) {
844 if (useSemantics && Int.getBitWidth() < 1) {
845 assert(false && "Boolean type doesn't match!");
846 return false;
847 }
848
849 Int = llvm::APSInt(llvm::APInt(Int.getBitWidth(), getBoolean(AST)),
850 Int.isUnsigned());
851 return true;
852 }
853
854 llvm_unreachable("Unsupported sort to integer!");
855 }
856
getInterpretation(const SMTExprRef & Exp,llvm::APSInt & Int)857 bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) override {
858 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
859 Z3_func_decl Func = Z3_get_app_decl(
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)
862 return false;
863
864 SMTExprRef Assign = newExprRef(
865 Z3Expr(Context,
866 Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
867 SMTSortRef Sort = getSort(Assign);
868 return toAPSInt(Sort, Assign, Int, true);
869 }
870
getInterpretation(const SMTExprRef & Exp,llvm::APFloat & Float)871 bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float) override {
872 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
873 Z3_func_decl Func = Z3_get_app_decl(
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)
876 return false;
877
878 SMTExprRef Assign = newExprRef(
879 Z3Expr(Context,
880 Z3_model_get_const_interp(Context.Context, Model.Model, Func)));
881 SMTSortRef Sort = getSort(Assign);
882 return toAPFloat(Sort, Assign, Float, true);
883 }
884
check() const885 std::optional<bool> check() const override {
886 Z3_solver_set_params(Context.Context, Solver, Params);
887 Z3_lbool res = Z3_solver_check(Context.Context, Solver);
888 if (res == Z3_L_TRUE)
889 return true;
890
891 if (res == Z3_L_FALSE)
892 return false;
893
894 return std::nullopt;
895 }
896
push()897 void push() override { return Z3_solver_push(Context.Context, Solver); }
898
pop(unsigned NumStates=1)899 void pop(unsigned NumStates = 1) override {
900 assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
901 return Z3_solver_pop(Context.Context, Solver, NumStates);
902 }
903
isFPSupported()904 bool isFPSupported() override { return true; }
905
906 /// Reset the solver and remove all constraints.
reset()907 void reset() override { Z3_solver_reset(Context.Context, Solver); }
908
print(raw_ostream & OS) const909 void print(raw_ostream &OS) const override {
910 OS << Z3_solver_to_string(Context.Context, Solver);
911 }
912
setUnsignedParam(StringRef Key,unsigned Value)913 void setUnsignedParam(StringRef Key, unsigned Value) override {
914 Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str());
915 Z3_params_set_uint(Context.Context, Params, Sym, Value);
916 }
917
setBoolParam(StringRef Key,bool Value)918 void setBoolParam(StringRef Key, bool Value) override {
919 Z3_symbol Sym = Z3_mk_string_symbol(Context.Context, Key.str().c_str());
920 Z3_params_set_bool(Context.Context, Params, Sym, Value);
921 }
922
923 std::unique_ptr<SMTSolverStatistics> getStatistics() const override;
924 }; // end class Z3Solver
925
926 class Z3Statistics final : public SMTSolverStatistics {
927 public:
getDouble(StringRef Key) const928 double getDouble(StringRef Key) const override {
929 auto It = DoubleValues.find(Key.str());
930 assert(It != DoubleValues.end());
931 return It->second;
932 };
getUnsigned(StringRef Key) const933 unsigned getUnsigned(StringRef Key) const override {
934 auto It = UnsignedValues.find(Key.str());
935 assert(It != UnsignedValues.end());
936 return It->second;
937 };
938
print(raw_ostream & OS) const939 void print(raw_ostream &OS) const override {
940 for (auto const &[K, V] : UnsignedValues) {
941 OS << K << ": " << V << '\n';
942 }
943 for (auto const &[K, V] : DoubleValues) {
944 write_double(OS << K << ": ", V, FloatStyle::Fixed);
945 OS << '\n';
946 }
947 }
948
949 private:
950 friend class Z3Solver;
951 std::unordered_map<std::string, unsigned> UnsignedValues;
952 std::unordered_map<std::string, double> DoubleValues;
953 };
954
getStatistics() const955 std::unique_ptr<SMTSolverStatistics> Z3Solver::getStatistics() const {
956 auto const &C = Context.Context;
957 Z3_stats S = Z3_solver_get_statistics(C, Solver);
958 Z3_stats_inc_ref(C, S);
959 auto StatsGuard = llvm::make_scope_exit([&C, &S] { Z3_stats_dec_ref(C, S); });
960 Z3Statistics Result;
961
962 unsigned NumKeys = Z3_stats_size(C, S);
963 for (unsigned Idx = 0; Idx < NumKeys; ++Idx) {
964 const char *Key = Z3_stats_get_key(C, S, Idx);
965 if (Z3_stats_is_uint(C, S, Idx)) {
966 auto Value = Z3_stats_get_uint_value(C, S, Idx);
967 Result.UnsignedValues.try_emplace(Key, Value);
968 } else {
969 assert(Z3_stats_is_double(C, S, Idx));
970 auto Value = Z3_stats_get_double_value(C, S, Idx);
971 Result.DoubleValues.try_emplace(Key, Value);
972 }
973 }
974 return std::make_unique<Z3Statistics>(std::move(Result));
975 }
976
977 } // end anonymous namespace
978
979 #endif
980
CreateZ3Solver()981 llvm::SMTSolverRef llvm::CreateZ3Solver() {
982 #if LLVM_WITH_Z3
983 return std::make_unique<Z3Solver>();
984 #else
985 llvm::report_fatal_error("LLVM was not compiled with Z3 support, rebuild "
986 "with -DLLVM_ENABLE_Z3_SOLVER=ON",
987 false);
988 return nullptr;
989 #endif
990 }
991
dump() const992 LLVM_DUMP_METHOD void SMTSort::dump() const { print(llvm::errs()); }
dump() const993 LLVM_DUMP_METHOD void SMTExpr::dump() const { print(llvm::errs()); }
dump() const994 LLVM_DUMP_METHOD void SMTSolver::dump() const { print(llvm::errs()); }
dump() const995 LLVM_DUMP_METHOD void SMTSolverStatistics::dump() const { print(llvm::errs()); }
996