HomeSort by: relevance | last modified time | path
    Searched refs:Solver (Results 1 - 6 of 6) sorted by relevancy

  /src/external/apache2/llvm/dist/clang/include/clang/StaticAnalyzer/Core/PathSensitive/
SMTConv.h 27 static inline llvm::SMTSortRef mkSort(llvm::SMTSolverRef &Solver,
30 return Solver->getBoolSort();
33 return Solver->getFloatSort(BitWidth);
35 return Solver->getBitvectorSort(BitWidth);
39 static inline llvm::SMTExprRef fromUnOp(llvm::SMTSolverRef &Solver,
44 return Solver->mkBVNeg(Exp);
47 return Solver->mkBVNot(Exp);
50 return Solver->mkNot(Exp);
58 static inline llvm::SMTExprRef fromFloatUnOp(llvm::SMTSolverRef &Solver,
63 return Solver->mkFPNeg(Exp)
    [all...]
SMTConstraintManager.h 10 // every SMT solver specific class.
31 mutable llvm::SMTSolverRef Solver = llvm::CreateZ3Solver();
51 SMTConv::getExpr(Solver, Ctx, Sym, &RetTy, &hasComparison);
58 SMTConv::getZeroExpr(Solver, Ctx, Exp, RetTy, !Assumption));
60 return assumeExpr(State, Sym, Assumption ? Exp : Solver->mkNot(Exp));
69 State, Sym, SMTConv::getRangeExpr(Solver, Ctx, Sym, From, To, InRange));
87 llvm::SMTExprRef VarExp = SMTConv::getExpr(Solver, Ctx, Sym, &RetTy);
89 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/true);
93 SMTConv::getZeroExpr(Solver, Ctx, VarExp, RetTy, /*Assumption=*/false);
123 // the solver, which is currently not cached
    [all...]
  /src/external/apache2/llvm/dist/llvm/lib/Transforms/Scalar/
SCCP.cpp 103 static bool tryToReplaceWithConstant(SCCPSolver &Solver, Value *V) {
106 std::vector<ValueLatticeElement> IVs = Solver.getStructLatticeValueFor(V);
115 ? Solver.getConstant(V)
120 const ValueLatticeElement &IV = Solver.getLatticeValueFor(V);
125 isConstant(IV) ? Solver.getConstant(IV) : UndefValue::get(V->getType());
140 Solver.addToMustPreserveReturnsInFunctions(F);
154 static bool simplifyInstsInBlock(SCCPSolver &Solver, BasicBlock &BB,
162 if (tryToReplaceWithConstant(Solver, &Inst)) {
172 const ValueLatticeElement &IV = Solver.getLatticeValueFor(ExtOp);
179 Solver.removeLatticeValueFor(&Inst)
    [all...]
  /src/external/apache2/llvm/dist/llvm/include/llvm/CodeGen/PBQP/
Graph.h 164 SolverT *Solver = nullptr;
352 /// Lock this graph to the given solver instance in preparation
353 /// for running the solver. This method will call solver.handleAddNode for
355 /// solver an opportunity to set up any requried metadata.
357 assert(!Solver && "Solver already set. Call unsetSolver().");
358 Solver = &S;
360 Solver->handleAddNode(NId);
362 Solver->handleAddEdge(EId)
    [all...]
  /src/external/apache2/llvm/dist/llvm/lib/Support/
Z3Solver.cpp 263 Z3_solver Solver;
272 Z3Solver() : Solver(Z3_mk_simple_solver(Context.Context)) {
273 Z3_solver_inc_ref(Context.Context, Solver);
282 if (Solver)
283 Z3_solver_dec_ref(Context.Context, Solver);
287 Z3_solver_assert(Context.Context, Solver, toZ3Expr(*Exp).AST);
844 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
858 Z3Model Model(Context, Z3_solver_get_model(Context.Context, Solver));
872 Z3_lbool res = Z3_solver_check(Context.Context, Solver);
882 void push() override { return Z3_solver_push(Context.Context, Solver); }
    [all...]
  /src/external/apache2/llvm/dist/llvm/lib/Transforms/IPO/
CalledValuePropagation.cpp 15 // makes uses of the generic sparse propagation solver.
108 /// The custom lattice function used by the generic sparse propagation solver.
276 // Inform the solver that the called function is executable, and perform
355 /// A specialization of LatticeKeyInfo for CVPLatticeKeys. The generic solver
369 // Our custom lattice function and generic sparse propagation solver.
371 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice);
374 // generic solver assume it is executable.
377 Solver.MarkBlockExecutable(&F.front());
379 // Solver our custom lattice. In doing so, we will also build a set of
381 Solver.Solve()
    [all...]

Completed in 59 milliseconds