Home
last modified time | relevance | path

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

/llvm-project-15.0.7/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
H A DSMTConv.h95 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 DSMTConstraintManager.h31 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 …]
/llvm-project-15.0.7/libc/benchmarks/automemcpy/lib/
H A DRandomFunctionGenerator.cpp119 Solver.add(ContiguousBegin == 0); in RandomFunctionGenerator()
139 Solver.add( in RandomFunctionGenerator()
144 Solver.add(IsMemcpy || in RandomFunctionGenerator()
151 Solver.add(LoopBegin == LoopEnd); in RandomFunctionGenerator()
207 if (Solver.check() != z3::sat) in next()
210 z3::model m = Solver.get_model(); in next()
246 Solver.add(!CurrentLayout); in next()
264 Solver.add(Begin >= 0); in addBoundsAndAnchors()
265 Solver.add(Begin <= End); in addBoundsAndAnchors()
266 Solver.add(End <= kMaxSize); in addBoundsAndAnchors()
[all …]
/llvm-project-15.0.7/llvm/lib/Transforms/Scalar/
H A DSCCP.cpp202 SCCPSolver Solver( in runSCCP() local
207 Solver.markBlockExecutable(&F.front()); in runSCCP()
211 Solver.markOverdefined(&AI); in runSCCP()
216 Solver.solve(); in runSCCP()
328 if (Solver.mustPreserveReturn(&F)) { in findReturnsToZap()
339 [&Solver](User *U) { in findReturnsToZap()
484 Solver.addTrackedFunction(&F); in runIPSCCP()
498 Solver.markOverdefined(&AI); in runIPSCCP()
512 Solver.solve(); in runIPSCCP()
517 if (Solver.resolvedUndefsIn(F)) in runIPSCCP()
[all …]
/llvm-project-15.0.7/llvm/unittests/Analysis/
H A DSparsePropagation.cpp268 Solver.MarkBlockExecutable(FEntry); in TEST_F()
269 Solver.Solve(); in TEST_F()
309 Solver.Solve(); in TEST_F()
350 Solver.Solve(); in TEST_F()
389 Solver.MarkBlockExecutable(If); in TEST_F()
390 Solver.Solve(); in TEST_F()
429 Solver.MarkBlockExecutable(If); in TEST_F()
430 Solver.Solve(); in TEST_F()
477 Solver.Solve(); in TEST_F()
535 Solver.MarkBlockExecutable(Entry); in TEST_F()
[all …]
/llvm-project-15.0.7/llvm/lib/Transforms/IPO/
H A DFunctionSpecialization.cpp242 Solver.visitCall(*Call); in constantArgPropagation()
272 SCCPSolver &Solver; member in __anonfb6321fa0211::FunctionSpecializer
285 FunctionSpecializer(SCCPSolver &Solver, in FunctionSpecializer() argument
289 : Solver(Solver), GetAC(GetAC), GetTTI(GetTTI), GetTLI(GetTLI) {} in FunctionSpecializer()
375 Solver.visit(I); in tryToReplaceWithConstant()
381 Solver.removeLatticeValueFor(I); in tryToReplaceWithConstant()
541 Solver.markFunctionUnreachable(F); in specializeFunction()
798 Solver.markOverdefined(CS); in rewriteCallSites()
810 Solver.addTrackedFunction(F); in updateSpecializedFuncs()
865 Solver.markOverdefined(&AI); in runFunctionSpecialization()
[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()
/llvm-project-15.0.7/llvm/include/llvm/CodeGen/PBQP/
H A DGraph.h358 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 …]
/llvm-project-15.0.7/clang/unittests/Analysis/FlowSensitive/
H A DSolverTest.cpp33 Solver::Result solve(llvm::DenseSet<BoolValue *> Vals) { in solve()
37 void expectUnsatisfiable(Solver::Result Result) { in expectUnsatisfiable()
38 EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Unsatisfiable); in expectUnsatisfiable()
43 void expectSatisfiable(Solver::Result Result, Matcher Solution) { in expectSatisfiable()
44 EXPECT_EQ(Result.getStatus(), Solver::Result::Status::Satisfiable); in expectSatisfiable()
55 UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue))); in TEST()
87 UnorderedElementsAre(Pair(X, Solver::Result::Assignment::AssignedTrue), in TEST()
242 Pair(X, Solver::Result::Assignment::AssignedTrue), in TEST()
243 Pair(Y, Solver::Result::Assignment::AssignedTrue)), in TEST()
245 Pair(X, Solver::Result::Assignment::AssignedFalse), in TEST()
[all …]
H A DDebugSupportTest.cpp207 Solver::Result CheckSAT(std::vector<BoolValue *> Constraints) { in CheckSAT()
/llvm-project-15.0.7/clang/lib/Analysis/FlowSensitive/
H A DDebugSupport.cpp34 std::string debugString(Solver::Result::Assignment Assignment) { in debugString()
36 case Solver::Result::Assignment::AssignedFalse: in debugString()
38 case Solver::Result::Assignment::AssignedTrue: in debugString()
44 std::string debugString(Solver::Result::Status Status) { in debugString()
46 case Solver::Result::Status::Satisfiable: in debugString()
48 case Solver::Result::Status::Unsatisfiable: in debugString()
50 case Solver::Result::Status::TimedOut: in debugString()
139 const Solver::Result &Result) { in debugString()
170 const llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> in debugString()
223 debugString(ArrayRef<BoolValue *> Constraints, const Solver::Result &Result, in debugString()
H A DWatchedLiteralsSolver.cpp456 Solver::Result solve() && { in solve()
485 return Solver::Result::Unsatisfiable(); in solve()
542 return Solver::Result::Satisfiable(buildSolution()); in solve()
548 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment>
550 llvm::DenseMap<AtomicBoolValue *, Solver::Result::Assignment> Solution; in buildSolution()
557 ? Solver::Result::Assignment::AssignedFalse in buildSolution()
558 : Solver::Result::Assignment::AssignedTrue; in buildSolution()
710 Solver::Result WatchedLiteralsSolver::solve(llvm::DenseSet<BoolValue *> Vals) { in solve()
711 return Vals.empty() ? Solver::Result::Satisfiable({{}}) in solve()
H A DDataflowAnalysisContext.cpp170 Solver::Result
/llvm-project-15.0.7/clang/include/clang/Analysis/FlowSensitive/
H A DDebugSupport.h28 std::string debugString(Solver::Result::Assignment Assignment);
31 std::string debugString(Solver::Result::Status Status);
70 ArrayRef<BoolValue *> Constraints, const Solver::Result &Result,
74 const Solver::Result &Result,
H A DDataflowAnalysisContext.h61 DataflowAnalysisContext(std::unique_ptr<Solver> S) in DataflowAnalysisContext()
282 Solver::Result querySolver(llvm::DenseSet<BoolValue *> Constraints);
288 Solver::Result::Status::Unsatisfiable; in isUnsatisfiable()
308 std::unique_ptr<Solver> S;
H A DSolver.h26 class Solver {
82 virtual ~Solver() = default;
H A DWatchedLiteralsSolver.h29 class WatchedLiteralsSolver : public Solver {
/llvm-project-15.0.7/llvm/lib/Support/
H A DZ3Solver.cpp265 Z3_solver Solver; member in __anonae660b540111::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()
874 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
888 return Z3_solver_pop(Context.Context, Solver, NumStates); in pop()
894 void reset() override { Z3_solver_reset(Context.Context, Solver); } in reset()
[all …]
/llvm-project-15.0.7/libc/benchmarks/automemcpy/include/automemcpy/
H A DRandomFunctionGenerator.h47 z3::solver Solver; member
/llvm-project-15.0.7/clang/docs/tools/
H A Dclang-formatted-files.txt137 clang/include/clang/Analysis/FlowSensitive/Solver.h