10#include "llvm/Config/config.h"
29 friend class Z3Context;
31 Z3_config
Config = Z3_mk_config();
35 Z3Config(
const Z3Config &) =
delete;
36 Z3Config(Z3Config &&) =
default;
37 Z3Config &operator=(Z3Config &) =
delete;
38 Z3Config &operator=(Z3Config &&) =
default;
39 ~Z3Config() { Z3_del_config(
Config); }
43void Z3ErrorHandler(Z3_context Context, Z3_error_code
Error) {
55 Context = Z3_mk_context_rc(
Config.Config);
58 Z3_set_error_handler(Context, Z3ErrorHandler);
61 Z3Context(
const Z3Context &) =
delete;
62 Z3Context(Z3Context &&) =
default;
63 Z3Context &operator=(Z3Context &) =
delete;
64 Z3Context &operator=(Z3Context &&) =
default;
67 Z3_del_context(Context);
74 friend class Z3Solver;
82 Z3Sort(Z3Context &
C, Z3_sort ZS) : Context(
C), Sort(ZS) {
83 Z3_inc_ref(Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
87 Z3Sort(
const Z3Sort &
Other) : Context(
Other.Context), Sort(
Other.Sort) {
88 Z3_inc_ref(Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
93 Z3Sort &operator=(
const Z3Sort &
Other) {
94 Z3_inc_ref(Context.Context,
reinterpret_cast<Z3_ast
>(
Other.Sort));
95 Z3_dec_ref(Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
100 Z3Sort(Z3Sort &&
Other) =
delete;
101 Z3Sort &operator=(Z3Sort &&
Other) =
delete;
105 Z3_dec_ref(Context.Context,
reinterpret_cast<Z3_ast
>(Sort));
110 Z3_get_ast_id(Context.Context,
reinterpret_cast<Z3_ast
>(Sort)));
113 bool isBitvectorSortImpl()
const override {
114 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BV_SORT);
117 bool isFloatSortImpl()
const override {
118 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_FLOATING_POINT_SORT);
121 bool isBooleanSortImpl()
const override {
122 return (Z3_get_sort_kind(Context.Context, Sort) == Z3_BOOL_SORT);
125 unsigned getBitvectorSortSizeImpl()
const override {
126 return Z3_get_bv_sort_size(Context.Context, Sort);
129 unsigned getFloatSortSizeImpl()
const override {
130 return Z3_fpa_get_ebits(Context.Context, Sort) +
131 Z3_fpa_get_sbits(Context.Context, Sort);
135 return Z3_is_eq_sort(Context.Context, Sort,
136 static_cast<const Z3Sort &
>(
Other).Sort);
140 OS << Z3_sort_to_string(Context.Context, Sort);
144static const Z3Sort &toZ3Sort(
const SMTSort &S) {
145 return static_cast<const Z3Sort &
>(S);
149 friend class Z3Solver;
156 Z3Expr(Z3Context &
C, Z3_ast ZA) :
SMTExpr(), Context(
C), AST(ZA) {
157 Z3_inc_ref(Context.Context, AST);
161 Z3Expr(
const Z3Expr &Copy) :
SMTExpr(), Context(
Copy.Context), AST(
Copy.AST) {
162 Z3_inc_ref(Context.Context, AST);
167 Z3Expr &operator=(
const Z3Expr &
Other) {
168 Z3_inc_ref(Context.Context,
Other.AST);
169 Z3_dec_ref(Context.Context, AST);
174 Z3Expr(Z3Expr &&
Other) =
delete;
175 Z3Expr &operator=(Z3Expr &&
Other) =
delete;
179 Z3_dec_ref(Context.Context, AST);
183 ID.AddInteger(Z3_get_ast_id(Context.Context, AST));
188 assert(Z3_is_eq_sort(Context.Context, Z3_get_sort(Context.Context, AST),
189 Z3_get_sort(Context.Context,
190 static_cast<const Z3Expr &
>(
Other).AST)) &&
191 "AST's must have the same sort");
192 return Z3_is_eq_ast(Context.Context, AST,
193 static_cast<const Z3Expr &
>(
Other).AST);
197 OS << Z3_ast_to_string(Context.Context, AST);
201static const Z3Expr &toZ3Expr(
const SMTExpr &
E) {
202 return static_cast<const Z3Expr &
>(
E);
206 friend class Z3Solver;
213 Z3Model(Z3Context &
C, Z3_model ZM) : Context(
C),
Model(ZM) {
214 Z3_model_inc_ref(Context.Context, Model);
217 Z3Model(
const Z3Model &
Other) =
delete;
218 Z3Model(Z3Model &&
Other) =
delete;
219 Z3Model &operator=(Z3Model &
Other) =
delete;
220 Z3Model &operator=(Z3Model &&
Other) =
delete;
224 Z3_model_dec_ref(Context.Context, Model);
228 OS << Z3_model_to_string(Context.Context, Model);
265 friend class Z3ConstraintManager;
269 Z3_solver Solver = [
this] {
270 Z3_solver S = Z3_mk_simple_solver(Context.Context);
271 Z3_solver_inc_ref(Context.Context, S);
275 Z3_params Params = [
this] {
276 Z3_params
P = Z3_mk_params(Context.Context);
277 Z3_params_inc_ref(Context.Context,
P);
282 std::set<Z3Sort> CachedSorts;
285 std::set<Z3Expr> CachedExprs;
288 Z3Solver() =
default;
289 Z3Solver(
const Z3Solver &
Other) =
delete;
290 Z3Solver(Z3Solver &&
Other) =
delete;
291 Z3Solver &operator=(Z3Solver &
Other) =
delete;
292 Z3Solver &operator=(Z3Solver &&
Other) =
delete;
294 ~Z3Solver()
override {
295 Z3_params_dec_ref(Context.Context, Params);
296 Z3_solver_dec_ref(Context.Context, Solver);
299 void addConstraint(
const SMTExprRef &Exp)
const override {
300 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
306 auto It = CachedSorts.insert(toZ3Sort(Sort));
313 auto It = CachedExprs.insert(toZ3Expr(Exp));
318 return newSortRef(Z3Sort(Context, Z3_mk_bool_sort(Context.Context)));
323 Z3Sort(Context, Z3_mk_bv_sort(Context.Context,
BitWidth)));
328 Z3Sort(Context, Z3_get_sort(Context.Context, toZ3Expr(*Exp).AST)));
332 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_16(Context.Context)));
336 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_32(Context.Context)));
340 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_64(Context.Context)));
344 return newSortRef(Z3Sort(Context, Z3_mk_fpa_sort_128(Context.Context)));
349 Z3Expr(Context, Z3_mk_bvneg(Context.Context, toZ3Expr(*Exp).AST)));
354 Z3Expr(Context, Z3_mk_bvnot(Context.Context, toZ3Expr(*Exp).AST)));
359 Z3Expr(Context, Z3_mk_not(Context.Context, toZ3Expr(*Exp).AST)));
364 Z3Expr(Context, Z3_mk_bvadd(Context.Context, toZ3Expr(*LHS).AST,
365 toZ3Expr(*RHS).AST)));
370 Z3Expr(Context, Z3_mk_bvsub(Context.Context, toZ3Expr(*LHS).AST,
371 toZ3Expr(*RHS).AST)));
376 Z3Expr(Context, Z3_mk_bvmul(Context.Context, toZ3Expr(*LHS).AST,
377 toZ3Expr(*RHS).AST)));
382 Z3Expr(Context, Z3_mk_bvsrem(Context.Context, toZ3Expr(*LHS).AST,
383 toZ3Expr(*RHS).AST)));
388 Z3Expr(Context, Z3_mk_bvurem(Context.Context, toZ3Expr(*LHS).AST,
389 toZ3Expr(*RHS).AST)));
394 Z3Expr(Context, Z3_mk_bvsdiv(Context.Context, toZ3Expr(*LHS).AST,
395 toZ3Expr(*RHS).AST)));
400 Z3Expr(Context, Z3_mk_bvudiv(Context.Context, toZ3Expr(*LHS).AST,
401 toZ3Expr(*RHS).AST)));
406 Z3Expr(Context, Z3_mk_bvshl(Context.Context, toZ3Expr(*LHS).AST,
407 toZ3Expr(*RHS).AST)));
412 Z3Expr(Context, Z3_mk_bvashr(Context.Context, toZ3Expr(*LHS).AST,
413 toZ3Expr(*RHS).AST)));
418 Z3Expr(Context, Z3_mk_bvlshr(Context.Context, toZ3Expr(*LHS).AST,
419 toZ3Expr(*RHS).AST)));
424 Z3Expr(Context, Z3_mk_bvxor(Context.Context, toZ3Expr(*LHS).AST,
425 toZ3Expr(*RHS).AST)));
430 Z3Expr(Context, Z3_mk_bvor(Context.Context, toZ3Expr(*LHS).AST,
431 toZ3Expr(*RHS).AST)));
436 Z3Expr(Context, Z3_mk_bvand(Context.Context, toZ3Expr(*LHS).AST,
437 toZ3Expr(*RHS).AST)));
442 Z3Expr(Context, Z3_mk_bvult(Context.Context, toZ3Expr(*LHS).AST,
443 toZ3Expr(*RHS).AST)));
448 Z3Expr(Context, Z3_mk_bvslt(Context.Context, toZ3Expr(*LHS).AST,
449 toZ3Expr(*RHS).AST)));
454 Z3Expr(Context, Z3_mk_bvugt(Context.Context, toZ3Expr(*LHS).AST,
455 toZ3Expr(*RHS).AST)));
460 Z3Expr(Context, Z3_mk_bvsgt(Context.Context, toZ3Expr(*LHS).AST,
461 toZ3Expr(*RHS).AST)));
466 Z3Expr(Context, Z3_mk_bvule(Context.Context, toZ3Expr(*LHS).AST,
467 toZ3Expr(*RHS).AST)));
472 Z3Expr(Context, Z3_mk_bvsle(Context.Context, toZ3Expr(*LHS).AST,
473 toZ3Expr(*RHS).AST)));
478 Z3Expr(Context, Z3_mk_bvuge(Context.Context, toZ3Expr(*LHS).AST,
479 toZ3Expr(*RHS).AST)));
484 Z3Expr(Context, Z3_mk_bvsge(Context.Context, toZ3Expr(*LHS).AST,
485 toZ3Expr(*RHS).AST)));
489 Z3_ast
Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
490 return newExprRef(Z3Expr(Context, Z3_mk_and(Context.Context, 2, Args)));
494 Z3_ast
Args[2] = {toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST};
495 return newExprRef(Z3Expr(Context, Z3_mk_or(Context.Context, 2, Args)));
500 Z3Expr(Context, Z3_mk_eq(Context.Context, toZ3Expr(*LHS).AST,
501 toZ3Expr(*RHS).AST)));
506 Z3Expr(Context, Z3_mk_fpa_neg(Context.Context, toZ3Expr(*Exp).AST)));
510 return newExprRef(Z3Expr(
511 Context, Z3_mk_fpa_is_infinite(Context.Context, toZ3Expr(*Exp).AST)));
516 Z3Expr(Context, Z3_mk_fpa_is_nan(Context.Context, toZ3Expr(*Exp).AST)));
520 return newExprRef(Z3Expr(
521 Context, Z3_mk_fpa_is_normal(Context.Context, toZ3Expr(*Exp).AST)));
525 return newExprRef(Z3Expr(
526 Context, Z3_mk_fpa_is_zero(Context.Context, toZ3Expr(*Exp).AST)));
533 Z3_mk_fpa_mul(Context.Context, toZ3Expr(*RoundingMode).AST,
534 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
541 Z3_mk_fpa_div(Context.Context, toZ3Expr(*RoundingMode).AST,
542 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
547 Z3Expr(Context, Z3_mk_fpa_rem(Context.Context, toZ3Expr(*LHS).AST,
548 toZ3Expr(*RHS).AST)));
555 Z3_mk_fpa_add(Context.Context, toZ3Expr(*RoundingMode).AST,
556 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
563 Z3_mk_fpa_sub(Context.Context, toZ3Expr(*RoundingMode).AST,
564 toZ3Expr(*LHS).AST, toZ3Expr(*RHS).AST)));
569 Z3Expr(Context, Z3_mk_fpa_lt(Context.Context, toZ3Expr(*LHS).AST,
570 toZ3Expr(*RHS).AST)));
575 Z3Expr(Context, Z3_mk_fpa_gt(Context.Context, toZ3Expr(*LHS).AST,
576 toZ3Expr(*RHS).AST)));
581 Z3Expr(Context, Z3_mk_fpa_leq(Context.Context, toZ3Expr(*LHS).AST,
582 toZ3Expr(*RHS).AST)));
587 Z3Expr(Context, Z3_mk_fpa_geq(Context.Context, toZ3Expr(*LHS).AST,
588 toZ3Expr(*RHS).AST)));
593 Z3Expr(Context, Z3_mk_fpa_eq(Context.Context, toZ3Expr(*LHS).AST,
594 toZ3Expr(*RHS).AST)));
600 Z3Expr(Context, Z3_mk_ite(Context.Context, toZ3Expr(*Cond).AST,
601 toZ3Expr(*T).AST, toZ3Expr(*F).AST)));
605 return newExprRef(Z3Expr(
606 Context, Z3_mk_sign_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
610 return newExprRef(Z3Expr(
611 Context, Z3_mk_zero_ext(Context.Context, i, toZ3Expr(*Exp).AST)));
616 return newExprRef(Z3Expr(Context, Z3_mk_extract(Context.Context,
High,
Low,
617 toZ3Expr(*Exp).AST)));
624 return newExprRef(Z3Expr(
625 Context, Z3_mk_bvadd_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
633 return newExprRef(Z3Expr(
634 Context, Z3_mk_bvadd_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
635 toZ3Expr(*RHS).AST)));
642 return newExprRef(Z3Expr(
643 Context, Z3_mk_bvsub_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
644 toZ3Expr(*RHS).AST)));
651 return newExprRef(Z3Expr(
652 Context, Z3_mk_bvsub_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
660 return newExprRef(Z3Expr(
661 Context, Z3_mk_bvsdiv_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
662 toZ3Expr(*RHS).AST)));
668 return newExprRef(Z3Expr(
669 Context, Z3_mk_bvneg_no_overflow(Context.Context, toZ3Expr(*Exp).AST)));
676 return newExprRef(Z3Expr(
677 Context, Z3_mk_bvmul_no_overflow(Context.Context, toZ3Expr(*LHS).AST,
685 return newExprRef(Z3Expr(
686 Context, Z3_mk_bvmul_no_underflow(Context.Context, toZ3Expr(*LHS).AST,
687 toZ3Expr(*RHS).AST)));
692 Z3Expr(Context, Z3_mk_concat(Context.Context, toZ3Expr(*LHS).AST,
693 toZ3Expr(*RHS).AST)));
698 return newExprRef(Z3Expr(
700 Z3_mk_fpa_to_fp_float(Context.Context, toZ3Expr(*RoundingMode).AST,
701 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
706 return newExprRef(Z3Expr(
708 Z3_mk_fpa_to_fp_signed(Context.Context, toZ3Expr(*RoundingMode).AST,
709 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
714 return newExprRef(Z3Expr(
716 Z3_mk_fpa_to_fp_unsigned(Context.Context, toZ3Expr(*RoundingMode).AST,
717 toZ3Expr(*From).AST, toZ3Sort(*To).Sort)));
722 return newExprRef(Z3Expr(
723 Context, Z3_mk_fpa_to_sbv(Context.Context, toZ3Expr(*RoundingMode).AST,
724 toZ3Expr(*From).AST, ToWidth)));
729 return newExprRef(Z3Expr(
730 Context, Z3_mk_fpa_to_ubv(Context.Context, toZ3Expr(*RoundingMode).AST,
731 toZ3Expr(*From).AST, ToWidth)));
735 return newExprRef(Z3Expr(Context, b ? Z3_mk_true(Context.Context)
736 : Z3_mk_false(Context.Context)));
740 const Z3_sort Z3Sort = toZ3Sort(*getBitvectorSort(
BitWidth)).Sort;
745 Int.toString(Buffer, 10);
746 return newExprRef(Z3Expr(
747 Context, Z3_mk_numeral(Context.Context, Buffer.
c_str(), Z3Sort)));
750 const int64_t BitReprAsSigned =
Int.getExtValue();
752 reinterpret_cast<const uint64_t &
>(BitReprAsSigned);
756 ? Z3_mk_int64(Context.Context, BitReprAsSigned, Z3Sort)
757 : Z3_mk_unsigned_int64(Context.Context, BitReprAsUnsigned, Z3Sort);
758 return newExprRef(Z3Expr(Context,
Literal));
767 return newExprRef(Z3Expr(
768 Context, Z3_mk_fpa_to_fp_bv(Context.Context, toZ3Expr(*Z3Int).AST,
769 toZ3Sort(*Sort).Sort)));
774 Z3Expr(Context, Z3_mk_const(Context.Context,
775 Z3_mk_string_symbol(Context.Context,
Name),
776 toZ3Sort(*Sort).Sort)));
780 bool isUnsigned)
override {
783 Z3_get_numeral_string(Context.Context, toZ3Expr(*Exp).AST),
788 bool getBoolean(
const SMTExprRef &Exp)
override {
789 return Z3_get_bool_value(Context.Context, toZ3Expr(*Exp).AST) == Z3_L_TRUE;
794 return newExprRef(Z3Expr(Context, Z3_mk_fpa_rne(Context.Context)));
805 if (!toAPSInt(BVSort, AST,
Int,
true)) {
809 if (useSemantics && !areEquivalent(
Float.getSemantics(), Semantics)) {
810 assert(
false &&
"Floating-point types don't match!");
822 assert(
false &&
"Bitvector types don't match!");
834 Int = getBitvector(AST,
Int.getBitWidth(),
Int.isUnsigned());
838 assert(
false &&
"Bitwidth not supported!");
843 if (useSemantics &&
Int.getBitWidth() < 1) {
844 assert(
false &&
"Boolean type doesn't match!");
857 Z3Model
Model(Context, Z3_solver_get_model(Context.Context, Solver));
858 Z3_func_decl
Func = Z3_get_app_decl(
859 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
860 if (Z3_model_has_interp(Context.Context,
Model.Model, Func) != Z3_L_TRUE)
865 Z3_model_get_const_interp(Context.Context,
Model.Model, Func)));
867 return toAPSInt(Sort, Assign,
Int,
true);
871 Z3Model
Model(Context, Z3_solver_get_model(Context.Context, Solver));
872 Z3_func_decl
Func = Z3_get_app_decl(
873 Context.Context, Z3_to_app(Context.Context, toZ3Expr(*Exp).AST));
874 if (Z3_model_has_interp(Context.Context,
Model.Model, Func) != Z3_L_TRUE)
879 Z3_model_get_const_interp(Context.Context,
Model.Model, Func)));
881 return toAPFloat(Sort, Assign, Float,
true);
884 std::optional<bool>
check()
const override {
885 Z3_solver_set_params(Context.Context, Solver, Params);
886 Z3_lbool res = Z3_solver_check(Context.Context, Solver);
887 if (res == Z3_L_TRUE)
890 if (res == Z3_L_FALSE)
896 void push()
override {
return Z3_solver_push(Context.Context, Solver); }
898 void pop(
unsigned NumStates = 1)
override {
899 assert(Z3_solver_get_num_scopes(Context.Context, Solver) >= NumStates);
900 return Z3_solver_pop(Context.Context, Solver, NumStates);
903 bool isFPSupported()
override {
return true; }
906 void reset()
override { Z3_solver_reset(Context.Context, Solver); }
909 OS << Z3_solver_to_string(Context.Context, Solver);
913 Z3_symbol
Sym = Z3_mk_string_symbol(Context.Context,
Key.str().c_str());
914 Z3_params_set_uint(Context.Context, Params,
Sym,
Value);
918 Z3_symbol
Sym = Z3_mk_string_symbol(Context.Context,
Key.str().c_str());
919 Z3_params_set_bool(Context.Context, Params,
Sym,
Value);
922 std::unique_ptr<SMTSolverStatistics> getStatistics()
const override;
928 auto It = DoubleValues.find(
Key.str());
929 assert(It != DoubleValues.end());
933 auto It = UnsignedValues.find(
Key.str());
934 assert(It != UnsignedValues.end());
939 for (
auto const &[K, V] : UnsignedValues) {
940 OS <<
K <<
": " <<
V <<
'\n';
942 for (
auto const &[K, V] : DoubleValues) {
949 friend class Z3Solver;
950 std::unordered_map<std::string, unsigned> UnsignedValues;
951 std::unordered_map<std::string, double> DoubleValues;
954std::unique_ptr<SMTSolverStatistics> Z3Solver::getStatistics()
const {
955 auto const &
C = Context.Context;
956 Z3_stats S = Z3_solver_get_statistics(
C, Solver);
957 Z3_stats_inc_ref(
C, S);
961 unsigned NumKeys = Z3_stats_size(
C, S);
962 for (
unsigned Idx = 0;
Idx < NumKeys; ++
Idx) {
963 const char *
Key = Z3_stats_get_key(
C, S,
Idx);
964 if (Z3_stats_is_uint(
C, S,
Idx)) {
965 auto Value = Z3_stats_get_uint_value(
C, S,
Idx);
969 auto Value = Z3_stats_get_double_value(
C, S,
Idx);
973 return std::make_unique<Z3Statistics>(std::move(Result));
982 return std::make_unique<Z3Solver>();
985 "with -DLLVM_ENABLE_Z3_SOLVER=ON",
static void print(raw_ostream &Out, object::Archive::Kind Kind, T Val)
BlockVerifier::State From
static GCRegistry::Add< CoreCLRGC > E("coreclr", "CoreCLR-compatible GC")
#define LLVM_UNLIKELY(EXPR)
#define LLVM_DUMP_METHOD
Mark debug helper function definitions like dump() that should not be stripped from debug builds.
Returns the sub type a function will return at a given Idx Should correspond to the result type of an ExtractValue instruction executed with just that one unsigned Idx
std::optional< std::vector< StOtherPiece > > Other
static bool isSigned(unsigned int Opcode)
const SmallVectorImpl< MachineOperand > & Cond
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
This file defines the make_scope_exit function, which executes user-defined cleanup logic at scope ex...
This file defines the SmallString class.
Class for arbitrary precision integers.
An arbitrary precision integer that knows its signedness.
Lightweight error class with error context and mandatory checking.
FoldingSetNodeID - This class is used to gather all the unique data bits of a node.
Generic base class for SMT exprs.
LLVM_DUMP_METHOD void dump() const
virtual void print(raw_ostream &OS) const =0
virtual unsigned getUnsigned(llvm::StringRef) const =0
LLVM_DUMP_METHOD void dump() const
virtual double getDouble(llvm::StringRef) const =0
virtual void print(raw_ostream &OS) const =0
Generic base class for SMT Solvers.
virtual void print(raw_ostream &OS) const =0
LLVM_DUMP_METHOD void dump() const
Generic base class for SMT sorts.
virtual void print(raw_ostream &OS) const =0
virtual bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
LLVM_DUMP_METHOD void dump() const
SmallString - A SmallString is just a SmallVector with methods and accessors that make it work better...
StringRef - Represent a constant reference to a string, i.e.
Twine - A lightweight data structure for efficiently representing the concatenation of temporary valu...
LLVM Value Representation.
This class implements an extremely fast bulk output stream that can only output to a stream.
#define llvm_unreachable(msg)
Marks that the current location is not supposed to be reachable.
constexpr char Args[]
Key for Kernel::Metadata::mArgs.
@ C
The default llvm calling convention, compatible with C.
NodeAddr< FuncNode * > Func
This is an optimization pass for GlobalISel generic memory operations.
void dump(const SparseBitVector< ElementSize > &LHS, raw_ostream &out)
@ Low
Lower the current thread's priority such that it does not affect foreground tasks significantly.
detail::scope_exit< std::decay_t< Callable > > make_scope_exit(Callable &&F)
void report_fatal_error(Error Err, bool gen_crash_diag=true)
Report a serious error, calling any installed error handler.
raw_fd_ostream & errs()
This returns a reference to a raw_ostream for standard error.
RoundingMode
Rounding mode.
void write_double(raw_ostream &S, double D, FloatStyle Style, std::optional< size_t > Precision=std::nullopt)
constexpr unsigned BitWidth
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
static const fltSemantics & IEEEsingle() LLVM_READNONE
static ExponentType semanticsMinExponent(const fltSemantics &)
static unsigned int semanticsSizeInBits(const fltSemantics &)
static const fltSemantics & IEEEquad() LLVM_READNONE
static ExponentType semanticsMaxExponent(const fltSemantics &)
static unsigned int semanticsPrecision(const fltSemantics &)
static const fltSemantics & IEEEdouble() LLVM_READNONE
static const fltSemantics & IEEEhalf() LLVM_READNONE