Analysis/FlowSensitive/WatchedLiteralsSolver.cpp

58 using Literal = uint32_t;
62 [[maybe_unused]] static constexpr Literal NullLit = 0;
65 static constexpr Literal posLit(Variable V) { return 2 * V; }
67 static constexpr bool isPosLit(Literal L) { return 0 == (L & 1); }
69 static constexpr bool isNegLit(Literal L) { return 1 == (L & 1); }
72 static constexpr Literal negLit(Variable V) { return 2 * V + 1; }
75 static constexpr Literal notLit(Literal L) { return L ^ 1; }
78 static constexpr Variable var(Literal L) { return L >> 1; }
101   std::vector<Literal> Clauses;
155   void addClause(ArrayRef<Literal> lits) {
157     assert(llvm::all_of(lits, [](Literal L) { return L != NullLit; }));
176   llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const {
177     return llvm::ArrayRef<Literal>(&Clauses[ClauseStarts[C]], clauseSize(C));
205   void addClause(ArrayRef<Literal> Literals) {
209     llvm::SmallVector<Literal> Simplified;
213                           [L](Literal S) { return  S != L; }));
239       const Literal lit = Simplified.front();
325     case Formula::Literal:
661     const Literal FalseLit = VarAssignments[Var] == Assignment::AssignedTrue
674       const Literal NewWatchedLit = CNF.Clauses[NewWatchedLitIdx];
699   bool watchedByUnitClause(Literal Lit) const {
702       llvm::ArrayRef<Literal> Clause = CNF.clauseLiterals(LitWatcher);
718   bool isUnit(llvm::ArrayRef<Literal> Clause) const {
720                         [this](Literal L) { return isCurrentlyFalse(L); });
725   bool isCurrentlyFalse(Literal Lit) const {
731   bool isWatched(Literal Lit) const {
743   llvm::DenseSet<Literal> watchedLiterals() const {
744     llvm::DenseSet<Literal> WatchedLiterals;
745     for (Literal Lit = 2; Lit < CNF.WatchedHead.size(); Lit++) {
762     const llvm::DenseSet<Literal> WatchedLiterals = watchedLiterals();
774     for (Literal Lit : watchedLiterals()) {