Searched refs:negLit (Results 1 – 3 of 3) sorted by relevance
| /freebsd/contrib/llvm-project/clang/lib/Analysis/FlowSensitive/ |
| H A D | CNFFormula.cpp | 181 CNF.addClause(F->literal() ? posLit(Var) : negLit(Var)); in buildCNF()
191 builder.addClause({negLit(Var), posLit(LHS)}); in buildCNF()
192 builder.addClause({posLit(Var), negLit(LHS)}); in buildCNF()
197 builder.addClause({negLit(Var), posLit(LHS)}); in buildCNF()
198 builder.addClause({negLit(Var), posLit(RHS)}); in buildCNF()
199 builder.addClause({posLit(Var), negLit(LHS), negLit(RHS)}); in buildCNF()
211 builder.addClause({negLit(Var), posLit(LHS)}); in buildCNF()
212 builder.addClause({posLit(Var), negLit(LHS)}); in buildCNF()
217 builder.addClause({negLit(Var), posLit(LHS), posLit(RHS)}); in buildCNF()
218 builder.addClause({posLit(Var), negLit(LHS)}); in buildCNF()
[all …]
|
| H A D | WatchedLiteralsSolver.cpp | 139 if (isWatched(posLit(Var)) || isWatched(negLit(Var))) in WatchedLiteralsSolverImpl()
173 const bool unitNegLit = watchedByUnitClause(negLit(ActiveVar)); in solve()
271 if (isWatched(posLit(Var)) || isWatched(negLit(Var))) in reverseForcedMoves()
283 ? negLit(Var) in updateWatchedLiterals()
357 return !isWatched(posLit(Var)) || isWatched(negLit(Var)) in decideAssignment()
385 WatchedLiterals.contains(negLit(Var)); in activeVarsFormWatchedLiterals()
|
| /freebsd/contrib/llvm-project/clang/include/clang/Analysis/FlowSensitive/ |
| H A D | CNFFormula.h | 52 inline constexpr Literal negLit(Variable V) { return 2 * V + 1; } in negLit() function
|