reference, declaration → definition definition → references, declarations, derived classes, virtual overrides reference to multiple definitions → definitions unreferenced |
443 SMTSolverRef CreateZ3Solver();
lib/Support/Z3Solver.cpp 887 llvm::SMTSolverRef llvm::CreateZ3Solver() {
tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConstraintManager.h 30 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
tools/clang/include/clang/StaticAnalyzer/Core/PathSensitive/SMTConv.h27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, 39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, 58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, 75 fromNBinOp(llvm::SMTSolverRef &Solver, const BinaryOperator::Opcode Op, 90 static inline llvm::SMTExprRef fromBinOp(llvm::SMTSolverRef &Solver, 169 fromFloatSpecialBinOp(llvm::SMTSolverRef &Solver, const llvm::SMTExprRef &LHS, 201 static inline llvm::SMTExprRef fromFloatBinOp(llvm::SMTSolverRef &Solver, 260 static inline llvm::SMTExprRef fromCast(llvm::SMTSolverRef &Solver, 313 static inline llvm::APSInt castAPSInt(llvm::SMTSolverRef &Solver, 322 static inline llvm::SMTExprRef fromData(llvm::SMTSolverRef &Solver, 330 static inline llvm::SMTExprRef getCastExpr(llvm::SMTSolverRef &Solver, 341 getBinExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, 376 static inline llvm::SMTExprRef getSymBinExpr(llvm::SMTSolverRef &Solver, 417 static inline llvm::SMTExprRef getSymExpr(llvm::SMTSolverRef &Solver, 461 static inline llvm::SMTExprRef getExpr(llvm::SMTSolverRef &Solver, 473 static inline llvm::SMTExprRef getZeroExpr(llvm::SMTSolverRef &Solver, 504 getRangeExpr(llvm::SMTSolverRef &Solver, ASTContext &Ctx, SymbolRef Sym, 567 static inline void doTypeConversion(llvm::SMTSolverRef &Solver, 644 static inline void doIntTypeConversion(llvm::SMTSolverRef &Solver, 727 doFloatTypeConversion(llvm::SMTSolverRef &Solver, ASTContext &Ctx, T &LHS,tools/clang/lib/StaticAnalyzer/Core/BugReporterVisitors.cpp
2826 llvm::SMTSolverRef RefutationSolver = llvm::CreateZ3Solver();