Searched refs:SMTSortRef (Results 1 – 3 of 3) sorted by relevance
97 using SMTSortRef = const SMTSort *; variable157 SMTSortRef getFloatSort(unsigned BitWidth) { in getFloatSort()173 virtual SMTSortRef getBoolSort() = 0;176 virtual SMTSortRef getBitvectorSort(const unsigned BitWidth) = 0;179 virtual SMTSortRef getFloat16Sort() = 0;182 virtual SMTSortRef getFloat32Sort() = 0;185 virtual SMTSortRef getFloat64Sort() = 0;188 virtual SMTSortRef getFloat128Sort() = 0;191 virtual SMTSortRef getSort(const SMTExprRef &AST) = 0;385 virtual SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) = 0;[all …]
306 SMTSortRef newSortRef(const SMTSort &Sort) { in newSortRef()318 SMTSortRef getBoolSort() override { in getBoolSort()322 SMTSortRef getBitvectorSort(unsigned BitWidth) override { in getBitvectorSort()327 SMTSortRef getSort(const SMTExprRef &Exp) override { in getSort()332 SMTSortRef getFloat16Sort() override { in getFloat16Sort()336 SMTSortRef getFloat32Sort() override { in getFloat32Sort()340 SMTSortRef getFloat64Sort() override { in getFloat64Sort()344 SMTSortRef getFloat128Sort() override { in getFloat128Sort()697 SMTExprRef mkFPtoFP(const SMTExprRef &From, const SMTSortRef &To) override { in mkFPtoFP()705 SMTExprRef mkSBVtoFP(const SMTExprRef &From, const SMTSortRef &To) override { in mkSBVtoFP()[all …]
27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, in mkSort()298 llvm::SMTSortRef Sort = Solver->getFloatSort(ToBitWidth); in fromCast()