Home
last modified time | relevance | path

Searched refs:ClauseIndex (Results 1 – 9 of 9) sorted by relevance

/dports/math/py-or-tools/or-tools-9.2/ortools/sat/
H A Ddrat_checker.h31 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 Ddrat_checker.cc34 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 Dsimplification.h148 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 Dsimplification.cc163 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 Dsat_inprocessing.h288 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 Dsat_inprocessing.cc947 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 Dpl-index.c90 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 Dpl-incl.h688 typedef struct clause_index * ClauseIndex; /* Clause indexing table */ typedef
1314 ClauseIndex *clause_indexes; /* Hash index(es) */
H A Dpl-funcs.h129 COMMON(void) unallocClauseIndexTable(ClauseIndex ci);