Home
last modified time | relevance | path

Searched refs:Solver (Results 1 – 21 of 21) sorted by relevance

/openbsd-src/gnu/llvm/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
H A DSMTConv.h27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver, in mkSort() argument
30 return Solver->getBoolSort(); in mkSort()
33 return Solver->getFloatSort(BitWidth); in mkSort()
35 return Solver->getBitvectorSort(BitWidth); in mkSort()
39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver, in fromUnOp() argument
44 return Solver->mkBVNeg(Exp); in fromUnOp()
47 return Solver->mkBVNot(Exp); in fromUnOp()
50 return Solver->mkNot(Exp); in fromUnOp()
58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver, in fromFloatUnOp() argument
63 return Solver->mkFPNeg(Exp); in fromFloatUnOp()
[all …]
H A DSMTConstraintManager.h32 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); in REGISTER_TRAIT_WITH_PROGRAMSTATE() local
52 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
59 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
61 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
70 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
88 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
90 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
94 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
126 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
128 Solver->reset(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
[all …]
/openbsd-src/gnu/llvm/llvm/lib/Transforms/IPO/
H A DSCCP.cpp51 SCCPSolver &Solver) { in findReturnsToZap() argument
53 if (!Solver.isArgumentTrackedFunction(&F)) in findReturnsToZap()
56 if (Solver.mustPreserveReturn(&F)) { in findReturnsToZap()
67 [&Solver](User *U) { in findReturnsToZap()
69 !Solver.isBlockExecutable(cast<Instruction>(U)->getParent())) in findReturnsToZap()
78 return all_of(Solver.getStructLatticeValueFor(U), in findReturnsToZap()
91 return !SCCPSolver::isOverdefined(Solver.getLatticeValueFor(U)); in findReturnsToZap()
116 SCCPSolver Solver(DL, GetTLI, M.getContext()); in runIPSCCP() local
117 FunctionSpecializer Specializer(Solver, M, FAM, GetTLI, GetTTI, GetAC); in runIPSCCP()
125 Solver.addAnalysis(F, getAnalysis(F)); in runIPSCCP()
[all …]
H A DFunctionSpecialization.cpp173 if (!Solver.isArgumentTrackedFunction(&F)) in promoteConstantStackValues()
182 if (!Solver.isBlockExecutable(Call->getParent())) in promoteConstantStackValues()
210 Solver.visitCall(*Call); in promoteConstantStackValues()
346 Solver.solveWhileResolvedUndefsIn(Clones); in run()
437 if (!Solver.isBlockExecutable(CS.getParent())) in findSpecializations()
473 getSpecializationBonus(A.Formal, A.Actual, Solver.getLoopInfo(*F)); in findSpecializations()
501 if (!Solver.isArgumentTrackedFunction(F)) in isCandidateFunction()
515 if (!Solver.isBlockExecutable(&F->getEntryBlock())) in isCandidateFunction()
533 Solver.markArgInFuncSpecialization(Clone, S.Args); in createSpecialization()
535 Solver.addArgumentTrackedFunction(Clone); in createSpecialization()
[all …]
H A DCalledValuePropagation.cpp374 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice); in runCVP() local
380 Solver.MarkBlockExecutable(&F.front()); in runCVP()
384 Solver.Solve(); in runCVP()
392 CVPLatticeVal LV = Solver.getExistingValueState(RegI); in runCVP()
/openbsd-src/gnu/llvm/llvm/include/llvm/CodeGen/PBQP/
H A DGraph.h164 SolverT *Solver = nullptr; variable
357 assert(!Solver && "Solver already set. Call unsetSolver()."); in setSolver()
358 Solver = &S; in setSolver()
360 Solver->handleAddNode(NId); in setSolver()
362 Solver->handleAddEdge(EId); in setSolver()
367 assert(Solver && "Solver not set."); in unsetSolver()
368 Solver = nullptr; in unsetSolver()
379 if (Solver) in addNode()
380 Solver->handleAddNode(NId); in addNode()
398 if (Solver) in addNodeBypassingCostAllocator()
[all …]
/openbsd-src/gnu/llvm/llvm/lib/Transforms/Scalar/
H A DSCCP.cpp71 SCCPSolver Solver( in runSCCP() local
76 Solver.markBlockExecutable(&F.front()); in runSCCP()
80 Solver.markOverdefined(&AI); in runSCCP()
85 Solver.solve(); in runSCCP()
87 ResolvedUndefs = Solver.resolvedUndefsIn(F); in runSCCP()
99 if (!Solver.isBlockExecutable(&BB)) { in runSCCP()
107 MadeChanges |= Solver.simplifyInstsInBlock(BB, InsertedValues, in runSCCP()
118 MadeChanges |= Solver.removeNonFeasibleEdges(&BB, DTU, NewUnreachableBB); in runSCCP()
/openbsd-src/gnu/llvm/clang/lib/Analysis/FlowSensitive/
H A DDebugSupport.cpp63 llvm::StringRef debugString(Solver::Result::Assignment Assignment) { in debugString()
65 case Solver::Result::Assignment::AssignedFalse: in debugString()
67 case Solver::Result::Assignment::AssignedTrue: in debugString()
73 llvm::StringRef debugString(Solver::Result::Status Status) { in debugString()
75 case Solver::Result::Status::Satisfiable: in debugString()
77 case Solver::Result::Status::Unsatisfiable: in debugString()
79 case Solver::Result::Status::TimedOut: in debugString()
168 const Solver::Result &Result) { in debugString()
199 const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> in debugString()
252 debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, in debugString()
H A DWatchedLiteralsSolver.cpp461 Solver::Result solve() && { in solve()
490 return Solver::Result::Unsatisfiable(); in solve()
547 return Solver::Result::Satisfiable(buildSolution()); in solve()
553 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
555 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution; in buildSolution()
562 ? Solver::Result::Assignment::AssignedFalse in buildSolution()
563 : Solver::Result::Assignment::AssignedTrue; in buildSolution()
715 Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) { in solve()
716 return Vals.empty() ? Solver::Result::Satisfiable({{}}) in solve()
H A DDataflowAnalysisContext.cpp189 Solver::Result
/openbsd-src/gnu/llvm/clang/include/clang/Analysis/FlowSensitive/
H A DDebugSupport.h32 llvm::StringRef debugString(Solver::Result::Assignment Assignment);
35 llvm::StringRef debugString(Solver::Result::Status Status);
74 ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
78 const Solver::Result &Result,
H A DSolver.h26 class Solver {
82 virtual ~Solver() = default;
H A DDataflowAnalysisContext.h77 DataflowAnalysisContext(std::unique_ptr<Solver> S,
309 Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
315 Solver::Result::Status::Unsatisfiable; in isUnsatisfiable()
335 std::unique_ptr<Solver> S;
H A DWatchedLiteralsSolver.h29 class WatchedLiteralsSolver : public Solver {
/openbsd-src/gnu/llvm/llvm/include/llvm/Transforms/IPO/
H A DFunctionSpecialization.h118 SCCPSolver &Solver; variable
140 SCCPSolver &Solver, Module &M, FunctionAnalysisManager *FAM, in FunctionSpecializer() argument
144 : Solver(Solver), M(M), FAM(FAM), GetTLI(GetTLI), GetTTI(GetTTI), in FunctionSpecializer()
/openbsd-src/gnu/llvm/llvm/lib/Support/
H A DZ3Solver.cpp265 Z3_solver Solver; member in __anon0349533b0111::Z3Solver
274 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { in Z3Solver()
275 Z3_solver_inc_ref(Context.Context, Solver); in Z3Solver()
284 if (Solver) in ~Z3Solver()
285 Z3_solver_dec_ref(Context.Context, Solver); in ~Z3Solver()
289 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
846 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
860 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
874 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
884 void push() override { return Z3_solver_push(Context.Context, Solver); } in push()
[all …]
/openbsd-src/gnu/llvm/llvm/lib/Transforms/Utils/
H A DSCCPSolver.cpp119 static bool replaceSignedInst(SCCPSolver &Solver, in replaceSignedInst() argument
123 auto isNonNegative = [&Solver](Value *V) { in replaceSignedInst()
130 const ValueLatticeElement &IV = Solver.getLatticeValueFor(V); in replaceSignedInst()
176 Solver.removeLatticeValueFor(&Inst); in replaceSignedInst()
/openbsd-src/usr.sbin/pkg_add/OpenBSD/
H A DUpdateSet.pm207 return OpenBSD::Dependencies::Solver->new($self);
H A DDependencies.pm115 package OpenBSD::Dependencies::Solver;
H A DIntro.pod193 A specific C<OpenBSD::Dependencies::Solver> object is used for the resolution
/openbsd-src/gnu/llvm/clang/docs/tools/
H A Dclang-formatted-files.txt136 clang/include/clang/Analysis/FlowSensitive/Solver.h