llvm/Support/SMTAPI.h

29   virtual ~SMTSort() = default;
32   virtual bool isBitvectorSort() const { return isBitvectorSortImpl(); }  in isBitvectorSort()
35   virtual bool isFloatSort() const { return isFloatSortImpl(); }  in isFloatSort()
38   virtual bool isBooleanSort() const { return isBooleanSortImpl(); }  in isBooleanSort()
42   virtual unsigned getBitvectorSortSize() const {  in getBitvectorSortSize()
51   virtual unsigned getFloatSortSize() const {  in getFloatSortSize()
58   virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
71   virtual void print(raw_ostream &OS) const = 0;
78   virtual bool equal_to(SMTSort const &other) const = 0;
81   virtual bool isBitvectorSortImpl() const = 0;
84   virtual bool isFloatSortImpl() const = 0;
87   virtual bool isBooleanSortImpl() const = 0;
90   virtual unsigned getBitvectorSortSizeImpl() const = 0;
93   virtual unsigned getFloatSortSizeImpl() const = 0;
103   virtual ~SMTExpr() = default;
112   virtual void Profile(llvm::FoldingSetNodeID &ID) const = 0;
118   virtual void print(raw_ostream &OS) const = 0;
125   virtual bool equal_to(SMTExpr const &other) const = 0;
139   virtual ~SMTSolver() = default;
160   virtual SMTSortRef getBoolSort() = 0;
163   virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;
166   virtual SMTSortRef getFloat16Sort() = 0;
169   virtual SMTSortRef getFloat32Sort() = 0;
172   virtual SMTSortRef getFloat64Sort() = 0;
175   virtual SMTSortRef getFloat128Sort() = 0;
178   virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;
181   virtual void addConstraint(const SMTExprRef &Exp) const = 0;
184   virtual SMTExprRef mkBVAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
187   virtual SMTExprRef mkBVSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
190   virtual SMTExprRef mkBVMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
193   virtual SMTExprRef mkBVSRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
196   virtual SMTExprRef mkBVURem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
199   virtual SMTExprRef mkBVSDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
202   virtual SMTExprRef mkBVUDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
205   virtual SMTExprRef mkBVShl(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
208   virtual SMTExprRef mkBVAshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
211   virtual SMTExprRef mkBVLshr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
214   virtual SMTExprRef mkBVNeg(const SMTExprRef &Exp) = 0;
217   virtual SMTExprRef mkBVNot(const SMTExprRef &Exp) = 0;
220   virtual SMTExprRef mkBVXor(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
223   virtual SMTExprRef mkBVOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
226   virtual SMTExprRef mkBVAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
229   virtual SMTExprRef mkBVUlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
232   virtual SMTExprRef mkBVSlt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
235   virtual SMTExprRef mkBVUgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
238   virtual SMTExprRef mkBVSgt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
241   virtual SMTExprRef mkBVUle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
244   virtual SMTExprRef mkBVSle(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
247   virtual SMTExprRef mkBVUge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
250   virtual SMTExprRef mkBVSge(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
253   virtual SMTExprRef mkNot(const SMTExprRef &Exp) = 0;
256   virtual SMTExprRef mkEqual(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
259   virtual SMTExprRef mkAnd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
262   virtual SMTExprRef mkOr(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
265   virtual SMTExprRef mkIte(const SMTExprRef &Cond, const SMTExprRef &T,
269   virtual SMTExprRef mkBVSignExt(unsigned i, const SMTExprRef &Exp) = 0;
272   virtual SMTExprRef mkBVZeroExt(unsigned i, const SMTExprRef &Exp) = 0;
275   virtual SMTExprRef mkBVExtract(unsigned High, unsigned Low,
279   virtual SMTExprRef mkBVConcat(const SMTExprRef &LHS,
284   virtual SMTExprRef mkBVAddNoOverflow(const SMTExprRef &LHS,
290   virtual SMTExprRef mkBVAddNoUnderflow(const SMTExprRef &LHS,
295   virtual SMTExprRef mkBVSubNoOverflow(const SMTExprRef &LHS,
300   virtual SMTExprRef mkBVSubNoUnderflow(const SMTExprRef &LHS,
306   virtual SMTExprRef mkBVSDivNoOverflow(const SMTExprRef &LHS,
311   virtual SMTExprRef mkBVNegNoOverflow(const SMTExprRef &Exp) = 0;
315   virtual SMTExprRef mkBVMulNoOverflow(const SMTExprRef &LHS,
321   virtual SMTExprRef mkBVMulNoUnderflow(const SMTExprRef &LHS,
325   virtual SMTExprRef mkFPNeg(const SMTExprRef &Exp) = 0;
328   virtual SMTExprRef mkFPIsInfinite(const SMTExprRef &Exp) = 0;
331   virtual SMTExprRef mkFPIsNaN(const SMTExprRef &Exp) = 0;
334   virtual SMTExprRef mkFPIsNormal(const SMTExprRef &Exp) = 0;
337   virtual SMTExprRef mkFPIsZero(const SMTExprRef &Exp) = 0;
340   virtual SMTExprRef mkFPMul(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
343   virtual SMTExprRef mkFPDiv(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
346   virtual SMTExprRef mkFPRem(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
349   virtual SMTExprRef mkFPAdd(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
352   virtual SMTExprRef mkFPSub(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
355   virtual SMTExprRef mkFPLt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
358   virtual SMTExprRef mkFPGt(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
361   virtual SMTExprRef mkFPLe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
364   virtual SMTExprRef mkFPGe(const SMTExprRef &LHS, const SMTExprRef &RHS) = 0;
367   virtual SMTExprRef mkFPEqual(const SMTExprRef &LHS,
372   virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;
376   virtual SMTExprRef mkSBVtoFP(const SMTExprRef &From,
381   virtual SMTExprRef mkUBVtoFP(const SMTExprRef &From,
386   virtual SMTExprRef mkFPtoSBV(const SMTExprRef &From, unsigned ToWidth) = 0;
390   virtual SMTExprRef mkFPtoUBV(const SMTExprRef &From, unsigned ToWidth) = 0;
393   virtual SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) = 0;
396   virtual SMTExprRef getFloatRoundingMode() = 0;
399   virtual llvm::APSInt getBitvector(const SMTExprRef &Exp, unsigned BitWidth,
403   virtual bool getBoolean(const SMTExprRef &Exp) = 0;
406   virtual SMTExprRef mkBoolean(const bool b) = 0;
409   virtual SMTExprRef mkFloat(const llvm::APFloat Float) = 0;
412   virtual SMTExprRef mkBitvector(const llvm::APSInt Int, unsigned BitWidth) = 0;
415   virtual bool getInterpretation(const SMTExprRef &Exp, llvm::APSInt &Int) = 0;
418   virtual bool getInterpretation(const SMTExprRef &Exp,
422   virtual std::optional<bool> check() const = 0;
425   virtual void push() = 0;
428   virtual void pop(unsigned NumStates = 1) = 0;
431   virtual void reset() = 0;
434   virtual bool isFPSupported() = 0;
436   virtual void print(raw_ostream &OS) const = 0;