Searched refs:posLit (Results 1 – 3 of 3) sorted by relevance
| /freebsd/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/ |
| H A D | CNFFormula.cpp | 160 builder.addClause(posLit(GetVar(F))); in buildCNF()
180 CNF.addClause(F->literal() ? posLit(Var) : negLit(Var)); in buildCNF()
190 builder.addClause({negLit(Var), posLit(LHS)}); in buildCNF()
191 builder.addClause({posLit(Var), negLit(LHS)}); in buildCNF()
196 builder.addClause({negLit(Var), posLit(LHS)}); in buildCNF()
197 builder.addClause({negLit(Var), posLit(RHS)}); in buildCNF()
198 builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)}); in buildCNF()
210 builder.addClause({negLit(Var), posLit(LHS)}); in buildCNF()
211 builder.addClause({posLit(Var), negLit(LHS)}); in buildCNF()
216 builder.addClause({negLit(Var), posLit(LHS), posLit(RHS)}); in buildCNF()
[all …]
|
| H A D | WatchedLiteralsSolver.cpp | 139 if (isWatched(posLit(Var)) || isWatched(negLit(Var))) in WatchedLiteralsSolverImpl()
172 const bool unitPosLit = watchedByUnitClause(posLit(ActiveVar)); in solve()
271 if (isWatched(posLit(Var)) || isWatched(negLit(Var))) in reverseForcedMoves()
284 : posLit(Var); in updateWatchedLiterals()
357 return !isWatched(posLit(Var)) || isWatched(negLit(Var)) in decideAssignment()
384 return WatchedLiterals.contains(posLit(Var)) || in activeVarsFormWatchedLiterals()
|
| /freebsd/contrib/llvm-project/clang/include/clang/Analysis/FlowSensitive/ |
| H A D | CNFFormula.h | 49 inline constexpr Literal posLit(Variable V) { return 2 * V; } in posLit() function
|