| /freebsd-13.1/contrib/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 95 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && in fromBinOp()
104 return isSigned ? Solver->mkBVSDiv(LHS, RHS) : Solver->mkBVUDiv(LHS, RHS); in fromBinOp()
107 return isSigned ? Solver->mkBVSRem(LHS, RHS) : Solver->mkBVURem(LHS, RHS); in fromBinOp()
121 return isSigned ? Solver->mkBVAshr(LHS, RHS) : Solver->mkBVLshr(LHS, RHS); in fromBinOp()
125 return isSigned ? Solver->mkBVSlt(LHS, RHS) : Solver->mkBVUlt(LHS, RHS); in fromBinOp()
128 return isSigned ? Solver->mkBVSgt(LHS, RHS) : Solver->mkBVUgt(LHS, RHS); in fromBinOp()
131 return isSigned ? Solver->mkBVSle(LHS, RHS) : Solver->mkBVUle(LHS, RHS); in fromBinOp()
134 return isSigned ? Solver->mkBVSge(LHS, RHS) : Solver->mkBVUge(LHS, RHS); in fromBinOp()
205 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && in fromFloatBinOp()
292 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth)); in fromCast()
[all …]
|
| H A D | SMTConstraintManager.h | 31 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); in REGISTER_TRAIT_WITH_PROGRAMSTATE() local
127 Solver->reset(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
131 Optional<bool> isSat = Solver->check(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
136 if (!Solver->getInterpretation(Exp, Value)) in REGISTER_TRAIT_WITH_PROGRAMSTATE()
141 Solver, Exp, BO_NE, in REGISTER_TRAIT_WITH_PROGRAMSTATE()
146 Solver->addConstraint(NotExp); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
148 Optional<bool> isNotSat = Solver->check(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
267 return Solver->isFPSupported(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
322 Solver->addConstraint(Constraint); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
340 Solver->reset(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
[all …]
|
| /freebsd-13.1/contrib/llvm-project/llvm/lib/Transforms/Scalar/ |
| H A D | SCCP.cpp | 191 SCCPSolver Solver( in runSCCP() local
200 Solver.markOverdefined(&AI); in runSCCP()
205 Solver.solve(); in runSCCP()
300 if (Solver.mustPreserveReturn(&F)) { in findReturnsToZap()
311 [&Solver](User *U) { in findReturnsToZap()
350 if (Solver.isEdgeFeasible(BB, Succ)) in removeNonFeasibleEdges()
426 Solver.addTrackedFunction(&F); in runIPSCCP()
440 Solver.markOverdefined(&AI); in runIPSCCP()
454 Solver.solve(); in runIPSCCP()
459 if (Solver.resolvedUndefsIn(F)) in runIPSCCP()
[all …]
|
| /freebsd-13.1/contrib/llvm-project/llvm/lib/Transforms/IPO/ |
| H A D | FunctionSpecialization.cpp | 79 SCCPSolver &Solver; member in FunctionSpecializer
89 FunctionSpecializer(SCCPSolver &Solver, in FunctionSpecializer() argument
93 : Solver(Solver), GetAC(GetAC), GetTTI(GetTTI), GetTLI(GetTLI) {} in FunctionSpecializer()
525 Solver.markOverdefined(CS); in rewriteCallSites()
569 Solver.addAnalysis(F, GetAnalysis(F)); in runFunctionSpecialization()
575 Solver.addArgumentTrackedFunction(&F); in runFunctionSpecialization()
584 Solver.markBlockExecutable(&F.front()); in runFunctionSpecialization()
588 Solver.markOverdefined(&AI); in runFunctionSpecialization()
606 Solver.solve(); in runFunctionSpecialization()
610 if (Solver.resolvedUndefsIn(*F)) in runFunctionSpecialization()
[all …]
|
| H A D | CalledValuePropagation.cpp | 371 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice); in runCVP() local
377 Solver.MarkBlockExecutable(&F.front()); in runCVP()
381 Solver.Solve(); in runCVP()
389 CVPLatticeVal LV = Solver.getExistingValueState(RegI); in runCVP()
|
| /freebsd-13.1/contrib/llvm-project/llvm/include/llvm/CodeGen/PBQP/ |
| H A D | Graph.h | 358 Solver = &S; in setSolver()
379 if (Solver) in addNode()
398 if (Solver) in addNodeBypassingCostAllocator()
416 if (Solver) in addEdge()
441 if (Solver) in addEdgeBypassingCostAllocator()
468 if (Solver) in setNodeCosts()
510 if (Solver) in updateEdgeCosts()
586 if (Solver) in removeNode()
626 if (Solver) in disconnectEdge()
647 if (Solver) in reconnectEdge()
[all …]
|
| /freebsd-13.1/contrib/llvm-project/llvm/lib/Support/ |
| H A D | Z3Solver.cpp | 263 Z3_solver Solver; member in __anonca7d1dd80111::Z3Solver
272 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { in Z3Solver()
273 Z3_solver_inc_ref(Context.Context, Solver); in Z3Solver()
282 if (Solver) in ~Z3Solver()
283 Z3_solver_dec_ref(Context.Context, Solver); in ~Z3Solver()
287 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
844 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
872 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
886 return Z3_solver_pop(Context.Context, Solver, NumStates); in pop()
892 void reset() override { Z3_solver_reset(Context.Context, Solver); } in reset()
[all …]
|