Home
last modified time | relevance | path

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

/freebsd-12.1/contrib/llvm/tools/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()
204 assert(*Solver->getSort(LHS) == *Solver->getSort(RHS) && in fromFloatBinOp()
289 return Solver->mkFPtoFP(Exp, Solver->getFloatSort(ToBitWidth)); in fromCast()
[all …]
H A DSMTConstraintManager.h26 SMTSolverRef &Solver; variable
122 Solver->reset(); in getSymVal()
126 Optional<bool> isSat = Solver->check(); in getSymVal()
136 Solver, Exp, BO_NE, in getSymVal()
141 Solver->addConstraint(NotExp); in getSymVal()
143 Optional<bool> isNotSat = Solver->check(); in getSymVal()
242 return Solver->isFPSupported(); in canReasonAbout()
295 Constraint = Solver->mkAnd(Constraint, Solver->newExprRef(I++->second)); in addStateConstraints()
298 Solver->addConstraint(Constraint); in addStateConstraints()
316 Solver->reset(); in checkModel()
[all …]
/freebsd-12.1/contrib/llvm/include/llvm/CodeGen/PBQP/
H A DGraph.h359 Solver = &S; in setSolver()
380 if (Solver) in addNode()
399 if (Solver) in addNodeBypassingCostAllocator()
417 if (Solver) in addEdge()
442 if (Solver) in addEdgeBypassingCostAllocator()
469 if (Solver) in setNodeCosts()
511 if (Solver) in updateEdgeCosts()
587 if (Solver) in removeNode()
627 if (Solver) in disconnectEdge()
648 if (Solver) in reconnectEdge()
[all …]
/freebsd-12.1/contrib/llvm/lib/Transforms/Scalar/
H A DSCCP.cpp1740 Solver.AddMustTailCallee(F); in tryToReplaceWithConstant()
1759 SCCPSolver Solver(DL, TLI); in runSCCP() local
1766 Solver.markOverdefined(&AI); in runSCCP()
1771 Solver.Solve(); in runSCCP()
1881 if (Solver.isMustTailCallee(&F)) { in findReturnsToZap()
1939 SCCPSolver Solver(DL, TLI); in runIPSCCP() local
1952 Solver.AddTrackedFunction(&F); in runIPSCCP()
1966 Solver.markOverdefined(&AI); in runIPSCCP()
1980 Solver.Solve(); in runIPSCCP()
1985 if (Solver.ResolvedUndefsIn(F)) { in runIPSCCP()
[all …]
/freebsd-12.1/contrib/llvm/tools/clang/lib/StaticAnalyzer/Core/
H A DZ3ConstraintManager.cpp269 Z3_solver Solver; member in __anon1f86e14b0211::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()
781 Z3_lbool res = Z3_solver_check(Context.Context, Solver); in check()
795 return Z3_solver_pop(Context.Context, Solver, NumStates); in pop()
804 OS << Z3_solver_to_string(Context.Context, Solver); in print()
809 SMTSolverRef Solver = CreateZ3Solver(); member in __anon1f86e14b0211::Z3ConstraintManager
[all …]
/freebsd-12.1/contrib/llvm/lib/Transforms/IPO/
H A DCalledValuePropagation.cpp374 SparseSolver<CVPLatticeKey, CVPLatticeVal> Solver(&Lattice); in runCVP() local
380 Solver.MarkBlockExecutable(&F.front()); in runCVP()
384 Solver.Solve(); in runCVP()
393 CVPLatticeVal LV = Solver.getExistingValueState(RegI); in runCVP()