16#ifndef OR_TOOLS_SAT_SAT_BASE_H_
17#define OR_TOOLS_SAT_SAT_BASE_H_
25#include "absl/strings/str_format.h"
26#include "absl/types/span.h"
69 : index_(signed_value > 0 ? ((signed_value - 1) << 1)
70 : ((-signed_value - 1) << 1) ^ 1) {
76 Literal(BooleanVariable variable,
bool is_positive)
77 : index_(is_positive ? (variable.
value() << 1)
78 : (variable.
value() << 1) ^ 1) {}
80 BooleanVariable
Variable()
const {
return BooleanVariable(index_ >> 1); }
84 LiteralIndex
Index()
const {
return LiteralIndex(index_); }
85 LiteralIndex
NegatedIndex()
const {
return LiteralIndex(index_ ^ 1); }
88 return (index_ & 1) ? -((index_ >> 1) + 1) : ((index_ >> 1) + 1);
113 absl::Span<const Literal> literals) {
127 assignment_.
Resize(LiteralIndex(num_variables << 1));
211 return absl::StrFormat(
"level:%d type:%d trail_index:%d",
level,
type,
215static_assert(
sizeof(AssignmentInfo) == 8,
216 "ERROR_AssignmentInfo_is_not_well_compacted");
239 current_info_.
level = 0;
242 void Resize(
int num_variables);
253 current_info_.
type = propagator_id;
254 info_[true_literal.
Variable()] = current_info_;
273 BooleanVariable reference_var) {
274 reference_var_with_same_reason_as_[true_literal.
Variable()] = reference_var;
293 const BooleanVariable
var = true_literal.
Variable();
294 reasons_[
var] = reasons_repository_[info_[
var].trail_index];
295 old_type_[
var] = info_[
var].type;
305 absl::Span<const Literal>
Reason(BooleanVariable
var)
const;
321 if (trail_index >= reasons_repository_.size()) {
322 reasons_repository_.resize(trail_index + 1);
324 reasons_repository_[trail_index].clear();
325 return &reasons_repository_[trail_index];
336 const BooleanVariable
var = trail_[trail_index].Variable();
337 info_[
var].type = propagator_id;
338 old_type_[
var] = propagator_id;
345 num_untrailed_enqueues_ +=
index - target_trail_index;
346 for (
int i = target_trail_index; i <
index; ++i) {
362 failing_sat_clause_ =
nullptr;
390 for (
int i = 0; i < current_info_.
trail_index; ++i) {
391 if (!result.empty()) result +=
" ";
392 result += trail_[i].DebugString();
398 int64 num_untrailed_enqueues_ = 0;
401 std::vector<Literal> trail_;
402 std::vector<Literal> conflict_;
408 reference_var_with_same_reason_as_;
433 mutable std::deque<std::vector<Literal>> reasons_repository_;
439 std::vector<SatPropagator*> propagators_;
441 DISALLOW_COPY_AND_ASSIGN(
Trail);
490 int trail_index)
const {
518 const Trail& trail)
const {
522 <<
" trail_.Index()=" << trail.
Index();
530 <<
" trail_.Index()=" << trail.
Index()
531 <<
" level_at_propagation_index="
540 assignment_.
Resize(num_variables);
541 info_.resize(num_variables);
542 trail_.resize(num_variables);
543 reasons_.resize(num_variables);
547 old_type_.
resize(num_variables);
548 reference_var_with_same_reason_as_.
resize(num_variables);
552 if (propagators_.empty()) {
557 propagators_.push_back(propagator);
561 BooleanVariable
var)
const {
565 var = reference_var_with_same_reason_as_[
var];
574 var = reference_var_with_same_reason_as_[
var];
577 const int type = info_[
var].type;
599 return reasons_[
var];
#define DCHECK_NE(val1, val2)
#define CHECK_LT(val1, val2)
#define DCHECK_GE(val1, val2)
#define CHECK_NE(val1, val2)
#define DCHECK_LT(val1, val2)
#define DCHECK(condition)
void resize(size_type new_size)
void Resize(IndexType size)
bool IsSet(IndexType i) const
void ClearTwoBits(IndexType i)
bool AreOneOfTwoBitsSet(IndexType i) const
Literal(int signed_value)
LiteralIndex NegatedIndex() const
LiteralIndex Index() const
Literal(LiteralIndex index)
Literal(BooleanVariable variable, bool is_positive)
BooleanVariable Variable() const
std::string DebugString() const
bool operator==(Literal other) const
bool operator!=(Literal other) const
bool operator<(const Literal &literal) const
Class that owns everything related to a particular optimization model.
int propagation_trail_index_
void SetPropagatorId(int id)
virtual bool Propagate(Trail *trail)=0
SatPropagator(const std::string &name)
bool PropagatePreconditionsAreSatisfied(const Trail &trail) const
virtual void Untrail(const Trail &trail, int trail_index)
virtual absl::Span< const Literal > Reason(const Trail &trail, int trail_index) const
bool PropagationIsDone(const Trail &trail) const
void RegisterPropagator(SatPropagator *propagator)
void Enqueue(Literal true_literal, int propagator_id)
SatClause * FailingSatClause() const
void ChangeReason(int trail_index, int propagator_id)
std::vector< Literal > * GetEmptyVectorToStoreReason(int trail_index) const
void EnqueueWithSameReasonAs(Literal true_literal, BooleanVariable reference_var)
const VariablesAssignment & Assignment() const
int AssignmentType(BooleanVariable var) const
std::string DebugString()
void SetFailingSatClause(SatClause *clause)
absl::Span< const Literal > Reason(BooleanVariable var) const
BooleanVariable ReferenceVarWithSameReason(BooleanVariable var) const
ABSL_MUST_USE_RESULT bool EnqueueWithStoredReason(Literal true_literal)
void Untrail(int target_trail_index)
int64 NumberOfEnqueues() const
std::vector< Literal > * MutableConflict()
const AssignmentInfo & Info(BooleanVariable var) const
absl::Span< const Literal > FailingClause() const
int CurrentDecisionLevel() const
void SetDecisionLevel(int level)
std::vector< Literal > * GetEmptyVectorToStoreReason() const
const Literal & operator[](int index) const
void Resize(int num_variables)
void EnqueueWithUnitReason(Literal true_literal)
void EnqueueSearchDecision(Literal true_literal)
bool LiteralIsAssigned(Literal literal) const
bool VariableIsAssigned(BooleanVariable var) const
bool LiteralIsTrue(Literal literal) const
void AssignFromTrueLiteral(Literal literal)
void UnassignLiteral(Literal literal)
Literal GetTrueLiteralForAssignedVariable(BooleanVariable var) const
bool LiteralIsFalse(Literal literal) const
int NumberOfVariables() const
VariablesAssignment(int num_variables)
void Resize(int num_variables)
const LiteralIndex kFalseLiteralIndex(-3)
std::ostream & operator<<(std::ostream &os, const BoolVar &var)
const LiteralIndex kNoLiteralIndex(-1)
DEFINE_INT_TYPE(ClauseIndex, int)
const BooleanVariable kNoBooleanVariable(-1)
const LiteralIndex kTrueLiteralIndex(-2)
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...
std::string DebugString() const
static constexpr int kUnitReason
static constexpr int kSameReasonAs
static constexpr int kFirstFreePropagationId
static constexpr int kSearchDecision
static constexpr int kCachedReason