Home
last modified time | relevance | path

Searched refs:EnqueueWithUnitReason (Results 1 – 4 of 4) sorted by relevance

/dports/math/py-or-tools/or-tools-9.2/ortools/sat/
H A Dinteger.cc539 trail_->EnqueueWithUnitReason(lit); in Propagate()
701 trail_->EnqueueWithUnitReason(pair.literal.Negated()); in UpdateInitialDomain()
1156 trail_->EnqueueWithUnitReason(literal); in EnqueueLiteralInternal()
1320 trail_->EnqueueWithUnitReason(is_ignored); in EnqueueInternal()
1418 trail_->EnqueueWithUnitReason(to_enqueue); in EnqueueInternal()
H A Dsat_solver.cc176 trail_->EnqueueWithUnitReason(true_literal); in AddUnitClause()
231 trail_->EnqueueWithUnitReason(literals[0]); // Not assigned. in AddProblemClauseInternal()
370 trail_->EnqueueWithUnitReason(literals[0]); in AddLearnedClauseAndEnqueueUnitPropagation()
1089 trail_->EnqueueWithUnitReason(candidate[0]); in TryToMinimizeClause()
H A Dsat_base.h267 void EnqueueWithUnitReason(Literal true_literal) { in EnqueueWithUnitReason() function
H A Dclause.cc348 trail_->EnqueueWithUnitReason(true_literal); in InprocessingFixLiteral()
559 trail_->EnqueueWithUnitReason(true_literal); in FixLiteral()