Lines Matching refs:ClauseID
81 using ClauseID = uint32_t; typedef
85 static constexpr ClauseID NullClause = 0;
120 std::vector<ClauseID> WatchedHead;
128 std::vector<ClauseID> NextWatched;
159 const ClauseID C = ClauseStarts.size(); in addClause()
170 size_t clauseSize(ClauseID C) const { in clauseSize()
176 llvm::ArrayRef<Literal> clauseLiterals(ClauseID C) const { in clauseLiterals()
429 for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) { in buildCNF()
436 for (ClauseID C = 1; C < CNF.ClauseStarts.size(); ++C) { in buildCNF()
664 ClauseID FalseLitWatcher = CNF.WatchedHead[FalseLit]; in updateWatchedLiterals()
667 const ClauseID NextFalseLitWatcher = CNF.NextWatched[FalseLitWatcher]; in updateWatchedLiterals()
700 for (ClauseID LitWatcher = CNF.WatchedHead[Lit]; LitWatcher != NullClause; in watchedByUnitClause()