294   SMTSortRef newSortRef(const SMTSort &Sort) {  in newSortRef()
306   SMTSortRef getBoolSort() override {  in getBoolSort()
310   SMTSortRef getBitvectorSort(unsigned BitWidth) override {  in getBitvectorSort()
315   SMTSortRef getSort(const SMTExprRef &Exp) override {  in getSort()
320   SMTSortRef getFloat16Sort() override {  in getFloat16Sort()
324   SMTSortRef getFloat32Sort() override {  in getFloat32Sort()
328   SMTSortRef getFloat64Sort() override {  in getFloat64Sort()
332   SMTSortRef getFloat128Sort() override {  in getFloat128Sort()
685   SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override {  in mkFPtoFP()
693   SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {  in mkSBVtoFP()
701   SMTExprRef mkUBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override {  in mkUBVtoFP()
751     SMTSortRef Sort =  in mkFloat()
761   SMTExprRef mkSymbol(const char *Name, SMTSortRef Sort) override {  in mkSymbol()
786   bool toAPFloat(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPFloat()
793     SMTSortRef BVSort = getBitvectorSort(Sort->getFloatSortSize());  in toAPFloat()
807   bool toAPSInt(const SMTSortRef &Sort, const SMTExprRef &AST,  in toAPSInt()
855     SMTSortRef Sort = getSort(Assign);  in getInterpretation()
869     SMTSortRef Sort = getSort(Assign);  in getInterpretation()