14 #ifndef OR_TOOLS_SAT_PRESOLVE_CONTEXT_H_
15 #define OR_TOOLS_SAT_PRESOLVE_CONTEXT_H_
20 #include "ortools/sat/cp_model.pb.h"
24 #include "ortools/sat/sat_parameters.pb.h"
71 CpModelProto* mapping)
75 params_(*
model->GetOrCreate<SatParameters>()),
104 int64 MinOf(
const LinearExpressionProto& expr)
const;
105 int64 MaxOf(
const LinearExpressionProto& expr)
const;
109 return domains[
var].IsIncludedIn(domain);
136 int ref,
const Domain& domain,
bool* domain_modified =
nullptr);
145 const std::string&
message =
"") {
300 int var_in_equality,
int64 coeff_in_equality,
301 const ConstraintProto& equality,
302 std::vector<int>* new_vars_in_objective =
nullptr);
307 return objective_map_;
310 return objective_domain_is_constraining_;
326 return constraint_to_vars_[c];
330 return var_to_constraints_[
var];
334 return interval_usage_[c];
359 const SatParameters&
params()
const {
return params_; }
414 void AddVariableUsage(
int c);
415 void UpdateLinear1Usage(
const ConstraintProto&
ct,
int c);
419 bool VariableIsNotRepresentativeOfEquivalenceClass(
int var)
const;
423 bool RemapEncodingMaps();
429 bool CanonicalizeEncoding(
int* ref,
int64*
value);
444 bool add_constraints);
446 const bool log_info_;
447 const SatParameters& params_;
452 bool is_unsat =
false;
455 std::vector<Domain> domains;
461 absl::flat_hash_map<int, int64> objective_map_;
462 int64 objective_overflow_detection_;
463 std::vector<std::pair<int, int64>> tmp_entries_;
464 bool objective_domain_is_constraining_ =
false;
466 double objective_offset_;
467 double objective_scaling_factor_;
470 std::vector<std::vector<int>> constraint_to_vars_;
471 std::vector<absl::flat_hash_set<int>> var_to_constraints_;
474 std::vector<int> constraint_to_linear1_var_;
475 std::vector<int> var_to_num_linear1_;
478 std::vector<std::vector<int>> constraint_to_intervals_;
479 std::vector<int> interval_usage_;
482 absl::flat_hash_map<int, SavedVariable> abs_relations_;
488 absl::flat_hash_map<int64, SavedVariable> constant_to_ref_;
492 std::deque<int> encoding_remap_queue_;
496 absl::flat_hash_map<int, absl::flat_hash_map<int64, SavedLiteral>> encoding_;
502 absl::flat_hash_map<int, absl::flat_hash_map<int64, absl::flat_hash_set<int>>>
504 absl::flat_hash_map<int, absl::flat_hash_map<int64, absl::flat_hash_set<int>>>
515 std::vector<int> tmp_new_usage_;
518 absl::flat_hash_set<int> removed_variables_;
523 absl::flat_hash_map<std::tuple<int, int, int, int>,
int>
524 reified_precedences_cache_;
#define DCHECK(condition)
#define VLOG(verboselevel)
We call domain any subset of Int64 = [kint64min, kint64max].
A simple class to enforce both an elapsed time limit and a deterministic time limit in the same threa...
Class that owns everything related to a particular optimization model.
bool StoreAbsRelation(int target_ref, int ref)
SparseBitset< int64 > modified_domains
bool ConstraintVariableUsageIsConsistent()
int64 num_presolve_operations
void AddImplication(int a, int b)
bool ModelIsUnsat() const
bool VariableIsOnlyUsedInEncoding(int ref) const
ABSL_MUST_USE_RESULT bool IntersectDomainWith(int ref, const Domain &domain, bool *domain_modified=nullptr)
void InsertVarValueEncoding(int literal, int ref, int64 value)
std::vector< absl::flat_hash_set< int > > var_to_lb_only_constraints
bool ConstraintVariableGraphIsUpToDate() const
int GetOrCreateVarValueEncoding(int ref, int64 value)
bool DomainContains(int ref, int64 value) const
bool StoreLiteralImpliesVarNEqValue(int literal, int var, int64 value)
const Domain & ObjectiveDomain() const
bool DomainOfVarIsIncludedIn(int var, const Domain &domain)
bool VariableWithCostIsUniqueAndRemovable(int ref) const
void WriteObjectiveToProto() const
int GetLiteralRepresentative(int ref) const
ABSL_MUST_USE_RESULT bool SetLiteralToTrue(int lit)
bool StoreLiteralImpliesVarEqValue(int literal, int var, int64 value)
std::vector< int > tmp_literals
int64 MaxOf(int ref) const
std::vector< absl::flat_hash_set< int > > var_to_ub_only_constraints
bool ObjectiveDomainIsConstraining() const
CpModelProto * mapping_model
const std::vector< int > & ConstraintToVars(int c) const
void UpdateNewConstraintsVariableUsage()
bool VariableIsUniqueAndRemovable(int ref) const
void RemoveVariableFromAffineRelation(int var)
ABSL_MUST_USE_RESULT bool NotifyThatModelIsUnsat(const std::string &message="")
bool PropagateAffineRelation(int ref)
bool HasVarValueEncoding(int ref, int64 value, int *literal=nullptr)
Domain DomainOf(int ref) const
void InitializeNewDomains()
int GetVariableRepresentative(int ref) const
std::string AffineRelationDebugString(int ref) const
int NewIntVar(const Domain &domain)
void MarkVariableAsRemoved(int ref)
DomainDeductions deductions
std::vector< Domain > tmp_left_domains
bool DomainIsEmpty(int ref) const
void CanonicalizeDomainOfSizeTwo(int var)
bool LiteralIsTrue(int lit) const
absl::flat_hash_map< std::string, int > stats_by_rule_name
void StoreBooleanEqualityRelation(int ref_a, int ref_b)
int IntervalUsage(int c) const
CpModelProto * working_model
bool SubstituteVariableInObjective(int var_in_equality, int64 coeff_in_equality, const ConstraintProto &equality, std::vector< int > *new_vars_in_objective=nullptr)
int GetOrCreateConstantVar(int64 cst)
bool LiteralIsFalse(int lit) const
const absl::flat_hash_map< int, int64 > & ObjectiveMap() const
PresolveContext(bool log_info, Model *model, CpModelProto *cp_model, CpModelProto *mapping)
void UpdateRuleStats(const std::string &name, int num_times=1)
ABSL_MUST_USE_RESULT bool CanonicalizeObjective()
const SatParameters & params() const
void RemoveAllVariablesFromAffineRelationConstraint()
AffineRelation::Relation GetAffineRelation(int ref) const
bool VariableIsNotUsedAnymore(int ref) const
void UpdateConstraintVariableUsage(int c)
bool keep_all_feasible_solutions
bool IsFixed(int ref) const
int NumAffineRelations() const
std::vector< Domain > tmp_term_domains
int NumEquivRelations() const
const absl::flat_hash_set< int > & VarToConstraints(int var) const
ModelRandomGenerator * random()
ABSL_MUST_USE_RESULT bool SetLiteralToFalse(int lit)
std::string RefDebugString(int ref) const
int64 MinOf(int ref) const
int GetOrCreateReifiedPrecedenceLiteral(int time_i, int time_j, int active_i, int active_j)
void ClearPrecedenceCache()
absl::flat_hash_set< int > tmp_literal_set
void ReadObjectiveFromProto()
void AddImplyInDomain(int b, int x, const Domain &domain)
bool CanBeUsedAsLiteral(int ref) const
bool VariableWasRemoved(int ref) const
void RegisterVariablesUsedInAssumptions()
void ExploitFixedDomain(int var)
bool GetAbsRelation(int target_ref, int *ref)
bool StoreAffineRelation(int ref_x, int ref_y, int64 coeff, int64 offset)
int Get(PresolveContext *context) const
int Get(PresolveContext *context) const
GurobiMPCallbackContext * context
constexpr int kAffineRelationConstraint
constexpr int kAssumptionsConstraint
constexpr int kObjectiveConstraint
The vehicle routing library lets one model and solve generic vehicle routing problems ranging from th...