| /netbsd-src/external/apache2/llvm/dist/clang/include/clang/StaticAnalyzer/Core/PathSensitive/ |
| H A D | SMTConv.h | 27 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 D | SMTConstraintManager.h | 31 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver(); in REGISTER_TRAIT_WITH_PROGRAMSTATE() local
51 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
58 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
60 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
69 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange)); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
87 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
89 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
93 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
125 llvm::SMTExprRef Exp = SMTConv::fromData(Solver, Ctx, SD); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
127 Solver->reset(); in REGISTER_TRAIT_WITH_PROGRAMSTATE()
[all …]
|
| /netbsd-src/external/apache2/llvm/dist/llvm/lib/Transforms/Scalar/ |
| H A D | SCCP.cpp | 103 static bool tryToReplaceWithConstant(SCCPSolver &Solver, Value *V) { in tryToReplaceWithConstant() argument
106 std::vector<ValueLatticeElement> IVs = Solver.getStructLatticeValueFor(V); in tryToReplaceWithConstant()
115 ? Solver.getConstant(V) in tryToReplaceWithConstant()
120 const ValueLatticeElement &IV = Solver.getLatticeValueFor(V); in tryToReplaceWithConstant()
125 isConstant(IV) ? Solver.getConstant(IV) : UndefValue::get(V->getType()); in tryToReplaceWithConstant()
140 Solver.addToMustPreserveReturnsInFunctions(F); in tryToReplaceWithConstant()
154 static bool simplifyInstsInBlock(SCCPSolver &Solver, BasicBlock &BB, in simplifyInstsInBlock() argument
162 if (tryToReplaceWithConstant(Solver, &Inst)) { in simplifyInstsInBlock()
172 const ValueLatticeElement &IV = Solver.getLatticeValueFor(ExtOp); in simplifyInstsInBlock()
179 Solver.removeLatticeValueFor(&Inst); in simplifyInstsInBlock()
[all …]
|
| /netbsd-src/external/apache2/llvm/dist/llvm/include/llvm/CodeGen/PBQP/ |
| H A D | Graph.h | 164 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 …]
|
| /netbsd-src/external/apache2/llvm/dist/llvm/lib/Support/ |
| H A D | Z3Solver.cpp | 263 Z3_solver Solver; member in __anondfffcc6f0111::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()
858 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
872 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
882 void push() override { return Z3_solver_push(Context.Context, Solver); } in push()
[all …]
|
| /netbsd-src/external/apache2/llvm/dist/llvm/lib/Transforms/IPO/ |
| 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()
|
| /netbsd-src/external/historical/nawk/dist/testdir/ |
| H A D | funstack.ok | 908 Solver . . . . . . . . . . . . . . . . . 274--274
|
| H A D | funstack.in | 6363 title = "{ACM} Algorithm 423: Linear Equation Solver",
16255 …abstract = "The Designer Problem Solver (DPS) demonstrates that the computer can perform simpl…
|