LLVM 19.0.0git
SMTAPI.h
Go to the documentation of this file.
1//===- SMTAPI.h -------------------------------------------------*- 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// This file defines a SMT generic Solver API, which will be the base class
10// for every SMT solver specific class.
11//
12//===----------------------------------------------------------------------===//
13
14#ifndef LLVM_SUPPORT_SMTAPI_H
15#define LLVM_SUPPORT_SMTAPI_H
16
17#include "llvm/ADT/APFloat.h"
18#include "llvm/ADT/APSInt.h"
19#include "llvm/ADT/FoldingSet.h"
21#include <memory>
22
23namespace llvm {
24
25/// Generic base class for SMT sorts
26class SMTSort {
27public:
28 SMTSort() = default;
29 virtual ~SMTSort() = default;
30
31 /// Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
32 virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }
33
34 /// Returns true if the sort is a floating-point, calls isFloatSortImpl().
35 virtual bool isFloatSort() const { return isFloatSortImpl(); }
36
37 /// Returns true if the sort is a boolean, calls isBooleanSortImpl().
38 virtual bool isBooleanSort() const { return isBooleanSortImpl(); }
39
40 /// Returns the bitvector size, fails if the sort is not a bitvector
41 /// Calls getBitvectorSortSizeImpl().
42 virtual unsigned getBitvectorSortSize() const {
43 assert(isBitvectorSort() && "Not a bitvector sort!");
44 unsigned Size = getBitvectorSortSizeImpl();
45 assert(Size && "Size is zero!");
46 return Size;
47 };
48
49 /// Returns the floating-point size, fails if the sort is not a floating-point
50 /// Calls getFloatSortSizeImpl().
51 virtual unsigned getFloatSortSize() const {
52 assert(isFloatSort() && "Not a floating-point sort!");
53 unsigned Size = getFloatSortSizeImpl();
54 assert(Size && "Size is zero!");
55 return Size;
56 };
57
58 virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
59
60 bool operator<(const SMTSort &Other) const {
62 Profile(ID1);
63 Other.Profile(ID2);
64 return ID1 < ID2;
65 }
66
67 friend bool operator==(SMTSort const &LHS, SMTSort const &RHS) {
68 return LHS.equal_to(RHS);
69 }
70
71 virtual void print(raw_ostream &OS) const = 0;
72
73 LLVM_DUMP_METHOD void dump() const;
74
75protected:
76 /// Query the SMT solver and returns true if two sorts are equal (same kind
77 /// and bit width). This does not check if the two sorts are the same objects.
78 virtual bool equal_to(SMTSort const &other) const = 0;
79
80 /// Query the SMT solver and checks if a sort is bitvector.
81 virtual bool isBitvectorSortImpl() const = 0;
82
83 /// Query the SMT solver and checks if a sort is floating-point.
84 virtual bool isFloatSortImpl() const = 0;
85
86 /// Query the SMT solver and checks if a sort is boolean.
87 virtual bool isBooleanSortImpl() const = 0;
88
89 /// Query the SMT solver and returns the sort bit width.
90 virtual unsigned getBitvectorSortSizeImpl() const = 0;
91
92 /// Query the SMT solver and returns the sort bit width.
93 virtual unsigned getFloatSortSizeImpl() const = 0;
94};
95
96/// Shared pointer for SMTSorts, used by SMTSolver API.
97using SMTSortRef = const SMTSort *;
98
99/// Generic base class for SMT exprs
100class SMTExpr {
101public:
102 SMTExpr() = default;
103 virtual ~SMTExpr() = default;
104
105 bool operator<(const SMTExpr &Other) const {
106 llvm::FoldingSetNodeID ID1, ID2;
107 Profile(ID1);
108 Other.Profile(ID2);
109 return ID1 < ID2;
110 }
111
112 virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
113
114 friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS) {
115 return LHS.equal_to(RHS);
116 }
117
118 virtual void print(raw_ostream &OS) const = 0;
119
120 LLVM_DUMP_METHOD void dump() const;
121
122protected:
123 /// Query the SMT solver and returns true if two sorts are equal (same kind
124 /// and bit width). This does not check if the two sorts are the same objects.
125 virtual bool equal_to(SMTExpr const &other) const = 0;
126};
127
128/// Shared pointer for SMTExprs, used by SMTSolver API.
129using SMTExprRef = const SMTExpr *;
130
131/// Generic base class for SMT Solvers
132///
133/// This class is responsible for wrapping all sorts and expression generation,
134/// through the mk* methods. It also provides methods to create SMT expressions
135/// straight from clang's AST, through the from* methods.
137public:
138 SMTSolver() = default;
139 virtual ~SMTSolver() = default;
140
141 LLVM_DUMP_METHOD void dump() const;
142
143 // Returns an appropriate floating-point sort for the given bitwidth.
145 switch (BitWidth) {
146 case 16:
147 return getFloat16Sort();
148 case 32:
149 return getFloat32Sort();
150 case 64:
151 return getFloat64Sort();
152 case 128:
153 return getFloat128Sort();
154 default:;
155 }
156 llvm_unreachable("Unsupported floating-point bitwidth!");
157 }
158
159 // Returns a boolean sort.
160 virtual SMTSortRef getBoolSort() = 0;
161
162 // Returns an appropriate bitvector sort for the given bitwidth.
163 virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
164
165 // Returns a floating-point sort of width 16
167
168 // Returns a floating-point sort of width 32
170
171 // Returns a floating-point sort of width 64
173
174 // Returns a floating-point sort of width 128
176
177 // Returns an appropriate sort for the given AST.
178 virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
179
180 /// Given a constraint, adds it to the solver
181 virtual void addConstraint(const SMTExprRef &Exp) const = 0;
182
183 /// Creates a bitvector addition operation
184 virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
185
186 /// Creates a bitvector subtraction operation
187 virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
188
189 /// Creates a bitvector multiplication operation
190 virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
191
192 /// Creates a bitvector signed modulus operation
193 virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
194
195 /// Creates a bitvector unsigned modulus operation
196 virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
197
198 /// Creates a bitvector signed division operation
199 virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
200
201 /// Creates a bitvector unsigned division operation
202 virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
203
204 /// Creates a bitvector logical shift left operation
205 virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
206
207 /// Creates a bitvector arithmetic shift right operation
208 virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
209
210 /// Creates a bitvector logical shift right operation
211 virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
212
213 /// Creates a bitvector negation operation
214 virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
215
216 /// Creates a bitvector not operation
217 virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
218
219 /// Creates a bitvector xor operation
220 virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
221
222 /// Creates a bitvector or operation
223 virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
224
225 /// Creates a bitvector and operation
226 virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
227
228 /// Creates a bitvector unsigned less-than operation
229 virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
230
231 /// Creates a bitvector signed less-than operation
232 virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
233
234 /// Creates a bitvector unsigned greater-than operation
235 virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
236
237 /// Creates a bitvector signed greater-than operation
238 virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
239
240 /// Creates a bitvector unsigned less-equal-than operation
241 virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
242
243 /// Creates a bitvector signed less-equal-than operation
244 virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
245
246 /// Creates a bitvector unsigned greater-equal-than operation
247 virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
248
249 /// Creates a bitvector signed greater-equal-than operation
250 virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
251
252 /// Creates a boolean not operation
253 virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
254
255 /// Creates a boolean equality operation
256 virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
257
258 /// Creates a boolean and operation
259 virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
260
261 /// Creates a boolean or operation
262 virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
263
264 /// Creates a boolean ite operation
265 virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
266 const SMTExprRef &F) = 0;
267
268 /// Creates a bitvector sign extension operation
269 virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
270
271 /// Creates a bitvector zero extension operation
272 virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
273
274 /// Creates a bitvector extract operation
275 virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
276 const SMTExprRef &Exp) = 0;
277
278 /// Creates a bitvector concat operation
280 const SMTExprRef &RHS) = 0;
281
282 /// Creates a predicate that checks for overflow in a bitvector addition
283 /// operation
285 const SMTExprRef &RHS,
286 bool isSigned) = 0;
287
288 /// Creates a predicate that checks for underflow in a signed bitvector
289 /// addition operation
291 const SMTExprRef &RHS) = 0;
292
293 /// Creates a predicate that checks for overflow in a signed bitvector
294 /// subtraction operation
296 const SMTExprRef &RHS) = 0;
297
298 /// Creates a predicate that checks for underflow in a bitvector subtraction
299 /// operation
301 const SMTExprRef &RHS,
302 bool isSigned) = 0;
303
304 /// Creates a predicate that checks for overflow in a signed bitvector
305 /// division/modulus operation
307 const SMTExprRef &RHS) = 0;
308
309 /// Creates a predicate that checks for overflow in a bitvector negation
310 /// operation
311 virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0;
312
313 /// Creates a predicate that checks for overflow in a bitvector multiplication
314 /// operation
316 const SMTExprRef &RHS,
317 bool isSigned) = 0;
318
319 /// Creates a predicate that checks for underflow in a signed bitvector
320 /// multiplication operation
322 const SMTExprRef &RHS) = 0;
323
324 /// Creates a floating-point negation operation
325 virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
326
327 /// Creates a floating-point isInfinite operation
328 virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
329
330 /// Creates a floating-point isNaN operation
331 virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
332
333 /// Creates a floating-point isNormal operation
334 virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
335
336 /// Creates a floating-point isZero operation
337 virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
338
339 /// Creates a floating-point multiplication operation
340 virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
341
342 /// Creates a floating-point division operation
343 virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
344
345 /// Creates a floating-point remainder operation
346 virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
347
348 /// Creates a floating-point addition operation
349 virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
350
351 /// Creates a floating-point subtraction operation
352 virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
353
354 /// Creates a floating-point less-than operation
355 virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
356
357 /// Creates a floating-point greater-than operation
358 virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
359
360 /// Creates a floating-point less-than-or-equal operation
361 virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
362
363 /// Creates a floating-point greater-than-or-equal operation
364 virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
365
366 /// Creates a floating-point equality operation
368 const SMTExprRef &RHS) = 0;
369
370 /// Creates a floating-point conversion from floatint-point to floating-point
371 /// operation
372 virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
373
374 /// Creates a floating-point conversion from signed bitvector to
375 /// floatint-point operation
377 const SMTSortRef &To) = 0;
378
379 /// Creates a floating-point conversion from unsigned bitvector to
380 /// floatint-point operation
382 const SMTSortRef &To) = 0;
383
384 /// Creates a floating-point conversion from floatint-point to signed
385 /// bitvector operation
386 virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
387
388 /// Creates a floating-point conversion from floatint-point to unsigned
389 /// bitvector operation
390 virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
391
392 /// Creates a new symbol, given a name and a sort
393 virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
394
395 // Returns an appropriate floating-point rounding mode.
397
398 // If the a model is available, returns the value of a given bitvector symbol
399 virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
400 bool isUnsigned) = 0;
401
402 // If the a model is available, returns the value of a given boolean symbol
403 virtual bool getBoolean(const SMTExprRef &Exp) = 0;
404
405 /// Constructs an SMTExprRef from a boolean.
406 virtual SMTExprRef mkBoolean(const bool b) = 0;
407
408 /// Constructs an SMTExprRef from a finite APFloat.
409 virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
410
411 /// Constructs an SMTExprRef from an APSInt and its bit width
412 virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
413
414 /// Given an expression, extract the value of this operand in the model.
415 virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
416
417 /// Given an expression extract the value of this operand in the model.
418 virtual bool getInterpretation(const SMTExprRef &Exp,
419 llvm::APFloat &Float) = 0;
420
421 /// Check if the constraints are satisfiable
422 virtual std::optional<bool> check() const = 0;
423
424 /// Push the current solver state
425 virtual void push() = 0;
426
427 /// Pop the previous solver state
428 virtual void pop(unsigned NumStates = 1) = 0;
429
430 /// Reset the solver and remove all constraints.
431 virtual void reset() = 0;
432
433 /// Checks if the solver supports floating-points.
434 virtual bool isFPSupported() = 0;
435
436 virtual void print(raw_ostream &OS) const = 0;
437};
438
439/// Shared pointer for SMTSolvers.
440using SMTSolverRef = std::shared_ptr<SMTSolver>;
441
442/// Convenience method to create and Z3Solver object
444
445} // namespace llvm
446
447#endif
This file declares a class to represent arbitrary precision floating point values and provide a varie...
This file implements the APSInt class, which is a simple class that represents an arbitrary sized int...
BlockVerifier::State From
#define LLVM_DUMP_METHOD
Mark debug helper function definitions like dump() that should not be stripped from debug builds.
Definition: Compiler.h:529
std::string Name
uint64_t Size
static bool isSigned(unsigned int Opcode)
This file defines a hash set that can be used to remove duplication of nodes in a graph.
#define F(x, y, z)
Definition: MD5.cpp:55
Load MIR Sample Profile
uint64_t High
const SmallVectorImpl< MachineOperand > & Cond
assert(ImpDefSCC.getReg()==AMDGPU::SCC &&ImpDefSCC.isDef())
raw_pwrite_stream & OS
Value * RHS
Value * LHS
An arbitrary precision integer that knows its signedness.
Definition: APSInt.h:23
FoldingSetNodeID - This class is used to gather all the unique data bits of a node.
Definition: FoldingSet.h:320
Generic base class for SMT exprs.
Definition: SMTAPI.h:100
virtual bool equal_to(SMTExpr const &other) const =0
Query the SMT solver and returns true if two sorts are equal (same kind and bit width).
bool operator<(const SMTExpr &Other) const
Definition: SMTAPI.h:105
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
SMTExpr()=default
friend bool operator==(SMTExpr const &LHS, SMTExpr const &RHS)
Definition: SMTAPI.h:114
virtual ~SMTExpr()=default
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:917
virtual void print(raw_ostream &OS) const =0
Generic base class for SMT Solvers.
Definition: SMTAPI.h:136
virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-equal-than operation.
virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector or operation.
virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APFloat &Float)=0
Given an expression extract the value of this operand in the model.
virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T, const SMTExprRef &F)=0
Creates a boolean ite operation.
virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-equal-than operation.
virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp)=0
Creates a bitvector negation operation.
virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than-or-equal operation.
virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp)=0
Creates a predicate that checks for overflow in a bitvector negation operation.
virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp)=0
Creates a floating-point negation operation.
virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-than operation.
virtual ~SMTSolver()=default
virtual bool isFPSupported()=0
Checks if the solver supports floating-points.
virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector addition operation.
virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than-or-equal operation.
virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector multiplication operation.
virtual void push()=0
Push the current solver state.
virtual SMTSortRef getBitvectorSort(const unsigned BitWidth)=0
virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift right operation.
virtual SMTSortRef getFloat128Sort()=0
virtual SMTSortRef getSort(const SMTExprRef &AST)=0
virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp)=0
Creates a floating-point isNormal operation.
virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point multiplication operation.
virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned less-than operation.
virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point greater-than operation.
virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp)=0
Creates a floating-point isInfinite operation.
virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point division operation.
virtual SMTSortRef getFloat32Sort()=0
virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector subtraction operation.
virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned greater-than operation.
virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point less-than operation.
virtual SMTSortRef getFloat16Sort()=0
virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector addition operation.
virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector multiplication operation.
virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-than operation.
virtual SMTExprRef mkBoolean(const bool b)=0
Constructs an SMTExprRef from a boolean.
virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector zero extension operation.
virtual void pop(unsigned NumStates=1)=0
Pop the previous solver state.
virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector and operation.
virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from unsigned bitvector to floatint-point operation.
virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp)=0
Creates a floating-point isNaN operation.
virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low, const SMTExprRef &Exp)=0
Creates a bitvector extract operation.
virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point remainder operation.
virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector subtraction operation.
virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for overflow in a bitvector addition operation.
virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector xor operation.
virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean and operation.
virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point subtraction operation.
virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS, bool isSigned)=0
Creates a predicate that checks for underflow in a bitvector subtraction operation.
virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort)=0
Creates a new symbol, given a name and a sort.
virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned modulus operation.
virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from signed bitvector to floatint-point operation.
virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean or operation.
virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp)=0
Creates a bitvector sign extension operation.
virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To)=0
Creates a floating-point conversion from floatint-point to floating-point operation.
virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector arithmetic shift right operation.
virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth, bool isUnsigned)=0
virtual void reset()=0
Reset the solver and remove all constraints.
virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp)=0
Creates a floating-point isZero operation.
SMTSolver()=default
virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector logical shift left operation.
virtual void print(raw_ostream &OS) const =0
virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int)=0
Given an expression, extract the value of this operand in the model.
virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed division operation.
virtual SMTExprRef mkNot(const SMTExprRef &Exp)=0
Creates a boolean not operation.
virtual bool getBoolean(const SMTExprRef &Exp)=0
virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a boolean equality operation.
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:918
virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector concat operation.
virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to unsigned bitvector operation.
virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed modulus operation.
virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for underflow in a signed bitvector multiplication operation.
virtual SMTSortRef getFloat64Sort()=0
virtual std::optional< bool > check() const =0
Check if the constraints are satisfiable.
virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector unsigned division operation.
virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth)=0
Constructs an SMTExprRef from an APSInt and its bit width.
virtual SMTSortRef getBoolSort()=0
SMTSortRef getFloatSort(unsigned BitWidth)
Definition: SMTAPI.h:144
virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point addition operation.
virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a floating-point equality operation.
virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth)=0
Creates a floating-point conversion from floatint-point to signed bitvector operation.
virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed less-equal-than operation.
virtual void addConstraint(const SMTExprRef &Exp) const =0
Given a constraint, adds it to the solver.
virtual SMTExprRef getFloatRoundingMode()=0
virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a predicate that checks for overflow in a signed bitvector division/modulus operation.
virtual SMTExprRef mkFloat(const llvm::APFloat Float)=0
Constructs an SMTExprRef from a finite APFloat.
virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS)=0
Creates a bitvector signed greater-equal-than operation.
virtual SMTExprRef mkBVNot(const SMTExprRef &Exp)=0
Creates a bitvector not operation.
Generic base class for SMT sorts.
Definition: SMTAPI.h:26
virtual bool isBitvectorSortImpl() const =0
Query the SMT solver and checks if a sort is bitvector.
bool operator<(const SMTSort &Other) const
Definition: SMTAPI.h:60
virtual void print(raw_ostream &OS) const =0
virtual bool isBitvectorSort() const
Returns true if the sort is a bitvector, calls isBitvectorSortImpl().
Definition: SMTAPI.h:32
virtual unsigned getFloatSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
virtual bool equal_to(SMTSort const &other) const =0
Query the SMT solver and returns true if two sorts are equal (same kind and bit width).
SMTSort()=default
virtual bool isFloatSort() const
Returns true if the sort is a floating-point, calls isFloatSortImpl().
Definition: SMTAPI.h:35
virtual unsigned getFloatSortSize() const
Returns the floating-point size, fails if the sort is not a floating-point Calls getFloatSortSizeImpl...
Definition: SMTAPI.h:51
virtual unsigned getBitvectorSortSize() const
Returns the bitvector size, fails if the sort is not a bitvector Calls getBitvectorSortSizeImpl().
Definition: SMTAPI.h:42
virtual ~SMTSort()=default
friend bool operator==(SMTSort const &LHS, SMTSort const &RHS)
Definition: SMTAPI.h:67
virtual void Profile(llvm::FoldingSetNodeID &ID) const =0
virtual bool isFloatSortImpl() const =0
Query the SMT solver and checks if a sort is floating-point.
virtual bool isBooleanSort() const
Returns true if the sort is a boolean, calls isBooleanSortImpl().
Definition: SMTAPI.h:38
LLVM_DUMP_METHOD void dump() const
Definition: Z3Solver.cpp:916
virtual bool isBooleanSortImpl() const =0
Query the SMT solver and checks if a sort is boolean.
virtual unsigned getBitvectorSortSizeImpl() const =0
Query the SMT solver and returns the sort bit width.
This class implements an extremely fast bulk output stream that can only output to a stream.
Definition: raw_ostream.h:52
#define llvm_unreachable(msg)
Marks that the current location is not supposed to be reachable.
This is an optimization pass for GlobalISel generic memory operations.
Definition: AddressRanges.h:18
@ Low
Lower the current thread's priority such that it does not affect foreground tasks significantly.
@ Other
Any other memory.
constexpr unsigned BitWidth
Definition: BitmaskEnum.h:191
std::shared_ptr< SMTSolver > SMTSolverRef
Shared pointer for SMTSolvers.
Definition: SMTAPI.h:440
SMTSolverRef CreateZ3Solver()
Convenience method to create and Z3Solver object.
Definition: Z3Solver.cpp:905