Home
last modified time | relevance | path

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

12

/external/llvm-project/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
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 …]
DSMTConstraintManager.h31 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 …]
/external/eigen/test/
Dsparse_solver.h14 template<typename Solver, typename Rhs, typename Guess,typename Result>
15 void solve_with_guess(IterativeSolverBase<Solver>& solver, const MatrixBase<Rhs>& b, const Guess& g… in solve_with_guess()
28 template<typename Solver, typename Rhs, typename Guess,typename Result>
29 void solve_with_guess(SparseSolverBase<Solver>& solver, const MatrixBase<Rhs>& b, const Guess& , Re… in solve_with_guess()
36 template<typename Solver, typename Rhs, typename Guess,typename Result>
37 void solve_with_guess(SparseSolverBase<Solver>& solver, const SparseMatrixBase<Rhs>& b, const Guess… in solve_with_guess()
41 template<typename Solver, typename Rhs, typename DenseMat, typename DenseRhs>
42 void check_sparse_solving(Solver& solver, const typename Solver::MatrixType& A, const Rhs& b, const… in check_sparse_solving()
44 typedef typename Solver::MatrixType Mat; in check_sparse_solving()
56 …std::cerr << "ERROR | sparse solver testing, factorization failed (" << typeid(Solver).name() << "… in check_sparse_solving()
[all …]
/external/llvm-project/llvm/unittests/Analysis/
DSparsePropagation.cpp230 SparseSolver<TestLatticeKey, TestLatticeVal> Solver; member in __anona7d1fd010211::SparsePropagationTest
234 : M("", Context), Builder(Context), Solver(&Lattice) {} in SparsePropagationTest()
268 Solver.MarkBlockExecutable(FEntry); in TEST_F()
269 Solver.Solve(); in TEST_F()
271 EXPECT_TRUE(Solver.isBlockExecutable(GEntry)); in TEST_F()
307 Solver.MarkBlockExecutable(FEntry); in TEST_F()
308 Solver.MarkBlockExecutable(GEntry); in TEST_F()
309 Solver.Solve(); in TEST_F()
312 EXPECT_TRUE(Solver.getExistingValueState(MemGV).isConstant()); in TEST_F()
348 Solver.MarkBlockExecutable(FEntry); in TEST_F()
[all …]
/external/llvm/include/llvm/CodeGen/PBQP/
DGraph.h179 SolverT *Solver; variable
347 Graph() : Solver(nullptr) {} in Graph()
351 : Metadata(std::move(Metadata)), Solver(nullptr) {} in Graph()
364 assert(!Solver && "Solver already set. Call unsetSolver()."); in setSolver()
365 Solver = &S; in setSolver()
367 Solver->handleAddNode(NId); in setSolver()
369 Solver->handleAddEdge(EId); in setSolver()
374 assert(Solver && "Solver not set."); in unsetSolver()
375 Solver = nullptr; in unsetSolver()
386 if (Solver) in addNode()
[all …]
/external/llvm-project/llvm/include/llvm/CodeGen/PBQP/
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 …]
/external/swiftshader/third_party/llvm-10.0/llvm/include/llvm/CodeGen/PBQP/
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 …]
/external/llvm-project/llvm/lib/Transforms/Scalar/
DSCCP.cpp1627 static bool tryToReplaceWithConstant(SCCPSolver &Solver, Value *V) { in tryToReplaceWithConstant() argument
1630 std::vector<ValueLatticeElement> IVs = Solver.getStructLatticeValueFor(V); in tryToReplaceWithConstant()
1639 ? Solver.getConstant(V) in tryToReplaceWithConstant()
1644 const ValueLatticeElement &IV = Solver.getLatticeValueFor(V); in tryToReplaceWithConstant()
1649 isConstant(IV) ? Solver.getConstant(IV) : UndefValue::get(V->getType()); in tryToReplaceWithConstant()
1661 Solver.AddMustTailCallee(F); in tryToReplaceWithConstant()
1675 static bool simplifyInstsInBlock(SCCPSolver &Solver, BasicBlock &BB, in simplifyInstsInBlock() argument
1683 if (tryToReplaceWithConstant(Solver, &Inst)) { in simplifyInstsInBlock()
1693 const ValueLatticeElement &IV = Solver.getLatticeValueFor(ExtOp); in simplifyInstsInBlock()
1700 Solver.removeLatticeValueFor(&Inst); in simplifyInstsInBlock()
[all …]
/external/swiftshader/third_party/llvm-10.0/llvm/lib/Transforms/Scalar/
DSCCP.cpp1753 static bool tryToReplaceWithConstant(SCCPSolver &Solver, Value *V) { in tryToReplaceWithConstant() argument
1756 std::vector<LatticeVal> IVs = Solver.getStructLatticeValueFor(V); in tryToReplaceWithConstant()
1770 const LatticeVal &IV = Solver.getLatticeValueFor(V); in tryToReplaceWithConstant()
1787 Solver.AddMustTailCallee(F); in tryToReplaceWithConstant()
1806 SCCPSolver Solver( in runSCCP() local
1810 Solver.MarkBlockExecutable(&F.front()); in runSCCP()
1814 Solver.markOverdefined(&AI); in runSCCP()
1819 Solver.Solve(); in runSCCP()
1821 ResolvedUndefs = Solver.ResolvedUndefsIn(F); in runSCCP()
1831 if (!Solver.isBlockExecutable(&BB)) { in runSCCP()
[all …]
/external/eigen/bench/spbench/
Dspbenchsolver.h213 template<typename Solver, typename Scalar>
214 void call_solver(Solver &solver, const int solver_id, const typename Solver::MatrixType& A, const M… in call_solver()
278 template<typename Solver, typename Scalar>
279 void call_directsolver(Solver& solver, const int solver_id, const typename Solver::MatrixType& A, c… in call_directsolver()
288 template<typename Solver, typename Scalar>
289 void call_itersolver(Solver &solver, const int solver_id, const typename Solver::MatrixType& A, con… in call_itersolver()
/external/llvm/lib/Transforms/Scalar/
DSCCP.cpp1513 static bool tryToReplaceWithConstant(SCCPSolver &Solver, Value *V) { in tryToReplaceWithConstant() argument
1516 std::vector<LatticeVal> IVs = Solver.getStructLatticeValueFor(V); in tryToReplaceWithConstant()
1530 LatticeVal IV = Solver.getLatticeValueFor(V); in tryToReplaceWithConstant()
1543 static bool tryToReplaceInstWithConstant(SCCPSolver &Solver, Instruction *Inst, in tryToReplaceInstWithConstant() argument
1545 if (!tryToReplaceWithConstant(Solver, Inst)) in tryToReplaceInstWithConstant()
1560 SCCPSolver Solver(DL, TLI); in runSCCP() local
1563 Solver.MarkBlockExecutable(&F.front()); in runSCCP()
1567 Solver.markAnythingOverdefined(&AI); in runSCCP()
1572 Solver.Solve(); in runSCCP()
1574 ResolvedUndefs = Solver.ResolvedUndefsIn(F); in runSCCP()
[all …]
/external/swiftshader/third_party/llvm-10.0/llvm/lib/Support/
DZ3Solver.cpp262 Z3_solver Solver; member in __anond0ee00280111::Z3Solver
271 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) { in Z3Solver()
272 Z3_solver_inc_ref(Context.Context, Solver); in Z3Solver()
281 if (Solver) in ~Z3Solver()
282 Z3_solver_dec_ref(Context.Context, Solver); in ~Z3Solver()
286 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST); in addConstraint()
828 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
842 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver)); in getInterpretation()
856 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
866 void push() override { return Z3_solver_push(Context.Context, Solver); } in push()
[all …]
/external/llvm-project/llvm/lib/Support/
DZ3Solver.cpp263 Z3_solver Solver; member in __anon764e5f140111::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 …]
/external/eigen/bench/
Ddense_solvers.cpp14 template<typename Solver,typename MatrixType>
16 void compute_norm_equation(Solver &solver, const MatrixType &A) { in compute_norm_equation()
23 template<typename Solver,typename MatrixType>
25 void compute(Solver &solver, const MatrixType &A) { in compute()
/external/apache-commons-math/src/main/java/org/apache/commons/math/linear/
DSingularValueDecompositionImpl.java268 return new Solver(singularValues, getUT(), getV(), getRank() == Math in getSolver()
273 private static class Solver implements DecompositionSolver { class in SingularValueDecompositionImpl
292 private Solver(final double[] singularValues, final RealMatrix uT, in Solver() method in SingularValueDecompositionImpl.Solver
DCholeskyDecompositionImpl.java187 return new Solver(lTData); in getSolver()
191 private static class Solver implements DecompositionSolver { class in CholeskyDecompositionImpl
200 private Solver(final double[][] lTData) { in Solver() method in CholeskyDecompositionImpl.Solver
DQRDecompositionImpl.java248 return new Solver(qrt, rDiag); in getSolver()
252 private static class Solver implements DecompositionSolver { class in QRDecompositionImpl
270 private Solver(final double[][] qrt, final double[] rDiag) { in Solver() method in QRDecompositionImpl.Solver
DLUDecompositionImpl.java228 return new Solver(lu, pivot, singular); in getSolver()
232 private static class Solver implements DecompositionSolver { class in LUDecompositionImpl
249 private Solver(final double[][] lu, final int[] pivot, final boolean singular) { in Solver() method in LUDecompositionImpl.Solver
DFieldLUDecompositionImpl.java219 return new Solver<T>(field, lu, pivot, singular); in getSolver()
223 private static class Solver<T extends FieldElement<T>> implements FieldDecompositionSolver<T> { class in FieldLUDecompositionImpl
247 private Solver(final Field<T> field, final T[][] lu, in Solver() method in FieldLUDecompositionImpl.Solver
DEigenDecompositionImpl.java240 return new Solver(realEigenvalues, imagEigenvalues, eigenvectors); in getSolver()
244 private static class Solver implements DecompositionSolver { class in EigenDecompositionImpl
264 private Solver(final double[] realEigenvalues, in Solver() method in EigenDecompositionImpl.Solver
/external/swiftshader/third_party/llvm-10.0/llvm/lib/Transforms/IPO/
DCalledValuePropagation.cpp375 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice); in runCVP() local
381 Solver.MarkBlockExecutable(&F.front()); in runCVP()
385 Solver.Solve(); in runCVP()
394 CVPLatticeVal LV = Solver.getExistingValueState(RegI); in runCVP()
/external/llvm-project/llvm/lib/Transforms/IPO/
DCalledValuePropagation.cpp371 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()
/external/tensorflow/tensorflow/compiler/xla/service/
Dalgebraic_simplifier_proof_distributive_property.py46 s = z3.Solver()
/external/javaparser/
Dchangelog.md403 * BETA: the below work on Java Symbol Solver is still ongoing.
409 * BETA: the below work on Java Symbol Solver is still ongoing.
414 * BETA: the below work on Java Symbol Solver is still ongoing.
421 * BETA: the below work on Java Symbol Solver is still ongoing.
427 * BETA: the below work on Java Symbol Solver is still ongoing.
432 * BETA: the below work on Java Symbol Solver is still ongoing.
441 * BETA: the below work on Java Symbol Solver is still ongoing.
446 * BETA: the below work on Java Symbol Solver is still ongoing.
451 * BETA: we're still doing work to integrate parts of [Java Symbol Solver](https://github.com/javapa…
458 * BETA: we're doing work to integrate parts of [Java Symbol Solver](https://github.com/javaparser/j…
/external/llvm-project/llvm/test/Transforms/SCCP/
Dreturn-zapped.ll3 ; After the first round of Solver.Solve(), the return value of @testf still

12