Searched refs:ClauseIndex (Results 1 – 9 of 9) sorted by relevance
/dports/math/py-or-tools/or-tools-9.2/ortools/sat/ |
H A D | drat_checker.h | 31 DEFINE_INT_TYPE(ClauseIndex, int); 32 const ClauseIndex kNoClauseIndex(-1); 122 ClauseIndex deleted_index = ClauseIndex(std::numeric_limits<int>::max()); 126 std::vector<ClauseIndex> deleted_clauses; 155 ClauseIndex source_clause_index; 186 void WatchClause(ClauseIndex clause_index); 193 bool HasRupProperty(ClauseIndex num_clauses, 204 ClauseIndex AssignAndPropagate(ClauseIndex num_clauses, Literal literal, 218 ClauseIndex begin, ClauseIndex end) const; 224 ClauseIndex first_infered_clause_index_; [all …]
|
H A D | drat_checker.cc | 34 const ClauseIndex clause_index) const { 43 const ClauseIndex clause_index1, const ClauseIndex clause_index2) const { 59 const ClauseIndex clause_index = AddClause(clause); 109 return ClauseIndex(clauses_.size() - 1); 191 for (ClauseIndex j(0); j < i; ++j) { 219 ClauseIndex begin, ClauseIndex end) const { 221 for (ClauseIndex i = begin; i < end; ++i) { 280 ClauseIndex conflict = kNoClauseIndex; 343 ClauseIndex DratChecker::AssignAndPropagate(ClauseIndex num_clauses, 353 ClauseIndex conflict_index = kNoClauseIndex; [all …]
|
H A D | simplification.h | 148 typedef int32_t ClauseIndex; typedef 185 const std::vector<Literal>& Clause(ClauseIndex ci) const { in Clause() 211 bool ProcessClauseToSimplifyOthers(ClauseIndex clause_index); 230 bool ProcessClauseToSimplifyOthersUsingLiteral(ClauseIndex clause_index, 239 void Remove(ClauseIndex ci); 240 void RemoveAndRegisterForPostsolve(ClauseIndex ci, Literal x); 274 uint64_t ComputeSignatureOfClauseVariables(ClauseIndex ci); 328 std::vector<ClauseIndex> m_cls_; 330 std::vector<std::pair<LiteralIndex, ClauseIndex>> flattened_p_; 336 std::deque<ClauseIndex> clause_to_process_; [all …]
|
H A D | simplification.cc | 163 const ClauseIndex ci(clauses_.size()); in AddClause() 229 const ClauseIndex ci(clauses_.size()); in AddClauseInternal() 298 [this](ClauseIndex c1, ClauseIndex c2) { in ProcessAllClauses() 302 const ClauseIndex ci = clause_to_process_.front(); in ProcessAllClauses() 400 for (const ClauseIndex c : m_cls_) { in SimpleBva() 486 for (const ClauseIndex ci : m_cls_) { in SimpleBva() 509 for (const ClauseIndex c : m_cls_) { in SimpleBva() 552 ClauseIndex clause_index, Literal lit) { in ProcessClauseToSimplifyOthersUsingLiteral() 612 for (const ClauseIndex ci : occurrence_list_ref) { in ProcessClauseToSimplifyOthersUsingLiteral() 652 for (const ClauseIndex ci : occurrence_list_ref) { in ProcessClauseToSimplifyOthers() [all …]
|
H A D | sat_inprocessing.h | 288 DEFINE_INT_TYPE(ClauseIndex, int32_t); 289 absl::StrongVector<ClauseIndex, SatClause*> clauses_; 290 absl::StrongVector<LiteralIndex, std::vector<ClauseIndex>> 371 DEFINE_INT_TYPE(ClauseIndex, int32_t); 372 absl::StrongVector<ClauseIndex, SatClause*> clauses_; 373 absl::StrongVector<LiteralIndex, std::vector<ClauseIndex>>
|
H A D | sat_inprocessing.cc | 947 for (ClauseIndex i(0); i < clauses_.size(); ++i) { in InitializeForNewRound() 983 std::vector<ClauseIndex> clauses_to_process; in ProcessLiteral() 1019 for (const ClauseIndex i : clauses_to_process) { in ProcessLiteral() 1053 for (const ClauseIndex i : in ClauseIsBlocked() 1106 for (ClauseIndex i(0); i < clauses_.size(); ++i) { in DoOneRound() 1231 for (const ClauseIndex index : literal_to_clauses_[l.Index()]) { in Propagate() 1286 for (const ClauseIndex i : literal_to_clauses_[literal.Index()]) { in DeleteAllClausesContaining() 1302 const ClauseIndex index(clauses_.size()); in AddClause() 1322 const ClauseIndex clause_index = clause_containing_lit[i]; in ResolveAllClauseContaining() 1523 for (const ClauseIndex i : literal_to_clauses_[lit.Index()]) { in CrossProduct() [all …]
|
/dports/lang/swi-pl/swipl-8.2.3/src/ |
H A D | pl-index.c | 90 ClauseIndex *cip, ClauseIndex ci); 415 ClauseIndex *cip; in first_clause_guarded() 457 { ClauseIndex ci; in first_clause_guarded() 502 { ClauseIndex ci; in first_clause_guarded() 638 static ClauseIndex 765 { ClauseIndex *cip; in addClauseToListIndexes() 1180 { ClauseIndex *cip; in cleanClauseIndexes() 1396 { ClauseIndex *cip; in deleteActiveClauseFromIndexes() 1611 static ClauseIndex 1614 ClauseIndex ci; in hashDefinition() [all …]
|
H A D | pl-incl.h | 688 typedef struct clause_index * ClauseIndex; /* Clause indexing table */ typedef 1314 ClauseIndex *clause_indexes; /* Hash index(es) */
|
H A D | pl-funcs.h | 129 COMMON(void) unallocClauseIndexTable(ClauseIndex ci);
|