From 8fe2df9a185c810d3be6c8294114b1b4e0d5ee6a Mon Sep 17 00:00:00 2001 From: Laurent Perron Date: Tue, 15 Feb 2022 18:00:11 +0100 Subject: [PATCH] [CP-SAT] regenerates all includes; improve core solver when the objective is pseudo-boolean --- ortools/sat/all_different.cc | 10 +- ortools/sat/all_different.h | 3 + ortools/sat/boolean_problem.cc | 23 ++++- ortools/sat/circuit.cc | 10 +- ortools/sat/circuit.h | 2 + ortools/sat/clause.cc | 21 ++++- ortools/sat/clause.h | 2 + ortools/sat/cp_constraints.cc | 10 +- ortools/sat/cp_constraints.h | 1 + ortools/sat/cp_model.cc | 9 +- ortools/sat/cp_model.h | 4 +- ortools/sat/cp_model_checker.cc | 10 +- ortools/sat/cp_model_expand.cc | 12 ++- ortools/sat/cp_model_lns.cc | 24 ++++- ortools/sat/cp_model_lns.h | 12 +++ ortools/sat/cp_model_loader.cc | 14 +-- ortools/sat/cp_model_mapping.h | 1 + ortools/sat/cp_model_objective.cc | 5 + ortools/sat/cp_model_postsolve.cc | 5 + ortools/sat/cp_model_presolve.cc | 28 ++++-- ortools/sat/cp_model_presolve.h | 5 + ortools/sat/cp_model_search.cc | 20 +++- ortools/sat/cp_model_search.h | 2 + ortools/sat/cp_model_solver.cc | 92 ++++++++++++++----- ortools/sat/cp_model_symmetries.cc | 22 ++++- ortools/sat/cp_model_utils.cc | 5 + ortools/sat/cumulative.cc | 7 +- ortools/sat/cumulative_energy.cc | 8 +- ortools/sat/cuts.cc | 15 ++- ortools/sat/cuts.h | 5 + ortools/sat/diffn.cc | 20 ++-- ortools/sat/diffn.h | 3 + ortools/sat/diffn_util.cc | 15 ++- ortools/sat/diffn_util.h | 7 ++ ortools/sat/disjunctive.cc | 12 ++- ortools/sat/doc/README.md | 6 ++ ortools/sat/doc/boolean_logic.md | 9 ++ ortools/sat/doc/channeling.md | 13 +++ ortools/sat/doc/integer_arithmetic.md | 22 +++++ ortools/sat/doc/model.md | 13 ++- ortools/sat/doc/scheduling.md | 26 ++++++ ortools/sat/doc/solver.md | 24 +++++ ortools/sat/drat_checker.cc | 15 ++- ortools/sat/drat_checker.h | 3 + ortools/sat/drat_proof_handler.cc | 13 ++- ortools/sat/drat_proof_handler.h | 3 + ortools/sat/drat_writer.cc | 6 +- ortools/sat/encoding.cc | 8 +- ortools/sat/feasibility_pump.cc | 25 ++++- ortools/sat/feasibility_pump.h | 8 ++ ortools/sat/implied_bounds.cc | 17 ++++ ortools/sat/implied_bounds.h | 3 + ortools/sat/inclusion.h | 8 ++ ortools/sat/integer.cc | 25 ++++- ortools/sat/integer.h | 6 ++ ortools/sat/integer_expr.cc | 16 +++- ortools/sat/integer_expr.h | 6 ++ ortools/sat/integer_search.cc | 17 +++- ortools/sat/integer_search.h | 11 +++ ortools/sat/intervals.cc | 14 ++- ortools/sat/intervals.h | 3 + ortools/sat/lb_tree_search.cc | 24 +++++ ortools/sat/lb_tree_search.h | 14 ++- ortools/sat/linear_constraint.cc | 14 +++ ortools/sat/linear_constraint.h | 8 ++ ortools/sat/linear_constraint_manager.cc | 16 +++- ortools/sat/linear_constraint_manager.h | 9 +- ortools/sat/linear_programming_constraint.cc | 33 +++++-- ortools/sat/linear_programming_constraint.h | 6 ++ ortools/sat/linear_relaxation.cc | 13 ++- ortools/sat/linear_relaxation.h | 3 + ortools/sat/lp_utils.cc | 13 ++- ortools/sat/lp_utils.h | 5 + ortools/sat/max_hs.cc | 43 +++------ ortools/sat/max_hs.h | 10 ++ ortools/sat/model.h | 5 + ortools/sat/optimization.cc | 14 ++- ortools/sat/optimization.h | 4 + ortools/sat/parameters_validation.cc | 4 + ortools/sat/pb_constraint.cc | 12 +++ ortools/sat/pb_constraint.h | 2 +- ortools/sat/precedences.cc | 14 ++- ortools/sat/precedences.h | 2 + ortools/sat/presolve_context.cc | 25 +++++ ortools/sat/presolve_context.h | 7 ++ ortools/sat/presolve_util.cc | 13 +++ ortools/sat/presolve_util.h | 3 + ortools/sat/probing.cc | 12 ++- ortools/sat/probing.h | 8 ++ ortools/sat/pseudo_costs.cc | 9 +- ortools/sat/pseudo_costs.h | 5 + ortools/sat/restart.cc | 7 ++ ortools/sat/restart.h | 2 + ortools/sat/rins.cc | 9 +- ortools/sat/rins.h | 2 + ortools/sat/samples/assignment_groups_sat.cc | 8 ++ ortools/sat/samples/assignment_sat.cc | 8 ++ .../sat/samples/assignment_task_sizes_sat.cc | 7 ++ ortools/sat/samples/assignment_teams_sat.cc | 7 +- ortools/sat/samples/assumptions_sample_sat.cc | 11 ++- ortools/sat/samples/binpacking_problem_sat.cc | 7 ++ ortools/sat/samples/bool_or_sample_sat.cc | 3 + ortools/sat/samples/channeling_sample_sat.cc | 6 ++ ortools/sat/samples/code_samples.bzl | 41 +++++---- ortools/sat/samples/copy_model_sample_sat.cc | 7 +- ortools/sat/samples/cp_is_fun_sat.cc | 9 +- ortools/sat/samples/cp_sat_example.cc | 7 ++ .../earliness_tardiness_cost_sample_sat.cc | 6 ++ ortools/sat/samples/interval_sample_sat.cc | 4 + ortools/sat/samples/literal_sample_sat.cc | 3 + ortools/sat/samples/minimal_jobshop_sat.cc | 12 ++- ortools/sat/samples/multiple_knapsack_sat.cc | 5 + ortools/sat/samples/no_overlap_sample_sat.cc | 8 ++ ortools/sat/samples/nqueens_sat.cc | 9 +- ortools/sat/samples/nurses_sat.cc | 6 ++ .../samples/optional_interval_sample_sat.cc | 4 + .../sat/samples/rabbits_and_pheasants_sat.cc | 6 ++ ortools/sat/samples/ranking_sample_sat.cc | 10 ++ ortools/sat/samples/reified_sample_sat.cc | 3 + ortools/sat/samples/schedule_requests_sat.cc | 12 ++- .../search_for_all_solutions_sample_sat.cc | 6 ++ ortools/sat/samples/simple_sat_program.cc | 6 ++ .../samples/solution_hinting_sample_sat.cc | 6 ++ ...print_intermediate_solutions_sample_sat.cc | 6 ++ .../solve_with_time_limit_sample_sat.cc | 6 ++ .../sat/samples/step_function_sample_sat.cc | 10 ++ .../stop_after_n_solutions_sample_sat.cc | 6 ++ ortools/sat/sat_base.h | 1 + ortools/sat/sat_decision.cc | 13 +++ ortools/sat/sat_decision.h | 1 + ortools/sat/sat_inprocessing.cc | 17 ++++ ortools/sat/sat_inprocessing.h | 9 +- ortools/sat/sat_solver.cc | 28 +++++- ortools/sat/sat_solver.h | 2 + ortools/sat/scheduling_constraints.cc | 14 +++ ortools/sat/scheduling_constraints.h | 1 + ortools/sat/scheduling_cuts.cc | 12 +-- ortools/sat/simplification.cc | 14 ++- ortools/sat/simplification.h | 1 + ortools/sat/subsolver.cc | 13 ++- ortools/sat/subsolver.h | 2 + ortools/sat/swig_helper.h | 4 + ortools/sat/symmetry.cc | 8 ++ ortools/sat/symmetry_util.cc | 5 + ortools/sat/symmetry_util.h | 3 + ortools/sat/synchronization.cc | 31 ++++++- ortools/sat/synchronization.h | 8 ++ ortools/sat/table.cc | 15 +-- ortools/sat/theta_tree.cc | 4 +- ortools/sat/timetable.cc | 10 +- ortools/sat/timetable.h | 3 + ortools/sat/timetable_edgefinding.cc | 6 +- ortools/sat/util.cc | 18 ++++ ortools/sat/util.h | 4 + ortools/sat/var_domination.cc | 23 ++++- ortools/sat/var_domination.h | 4 + ortools/sat/zero_half_cuts.cc | 11 +++ ortools/sat/zero_half_cuts.h | 2 + 158 files changed, 1444 insertions(+), 232 deletions(-) diff --git a/ortools/sat/all_different.cc b/ortools/sat/all_different.cc index 8e1724ef8d..f417102a9e 100644 --- a/ortools/sat/all_different.cc +++ b/ortools/sat/all_different.cc @@ -15,14 +15,18 @@ #include #include +#include #include #include -#include +#include +#include -#include "absl/container/flat_hash_set.h" +#include "absl/types/span.h" #include "ortools/base/logging.h" -#include "ortools/base/map_util.h" #include "ortools/graph/strongly_connected_components.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_solver.h" #include "ortools/util/sort.h" #include "ortools/util/strong_integers.h" diff --git a/ortools/sat/all_different.h b/ortools/sat/all_different.h index 78ff7c4c46..cb533e38b5 100644 --- a/ortools/sat/all_different.h +++ b/ortools/sat/all_different.h @@ -20,11 +20,14 @@ #include #include "absl/container/flat_hash_map.h" +#include "absl/types/span.h" #include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" #include "ortools/base/macros.h" #include "ortools/sat/integer.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/boolean_problem.cc b/ortools/sat/boolean_problem.cc index 023c43d475..1796ab198c 100644 --- a/ortools/sat/boolean_problem.cc +++ b/ortools/sat/boolean_problem.cc @@ -14,28 +14,39 @@ #include "ortools/sat/boolean_problem.h" #include +#include #include #include #include +#include #include +#include #include +#include #include "absl/container/flat_hash_map.h" +#include "absl/flags/flag.h" #include "absl/status/status.h" #include "absl/strings/str_format.h" -#include "ortools/base/commandlineflags.h" -#include "ortools/base/integral_types.h" +#include "absl/strings/string_view.h" #include "ortools/base/logging.h" +#include "ortools/graph/graph.h" #if !defined(__PORTABLE_PLATFORM__) #include "ortools/graph/io.h" #endif // __PORTABLE_PLATFORM__ #include "ortools/algorithms/find_graph_symmetries.h" -#include "ortools/base/hash.h" +#include "ortools/algorithms/sparse_permutation.h" #include "ortools/base/map_util.h" #include "ortools/base/strong_vector.h" #include "ortools/graph/util.h" #include "ortools/port/proto_utils.h" +#include "ortools/sat/boolean_problem.pb.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/pb_constraint.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/sat/simplification.h" #include "ortools/util/strong_integers.h" ABSL_FLAG(std::string, debug_dump_symmetry_graph_to_file, "", @@ -706,8 +717,10 @@ void FindLinearBooleanProblemSymmetries( /*is_undirected=*/true); std::vector factorized_automorphism_group_size; // TODO(user): inject the appropriate time limit here. - CHECK_OK(symmetry_finder.FindSymmetries(&equivalence_classes, generators, - &factorized_automorphism_group_size)); + CHECK(symmetry_finder + .FindSymmetries(&equivalence_classes, generators, + &factorized_automorphism_group_size) + .ok()); // Remove from the permutations the part not concerning the literals. // Note that some permutation may becomes empty, which means that we had diff --git a/ortools/sat/circuit.cc b/ortools/sat/circuit.cc index 321b0e46c4..2e72ccec1a 100644 --- a/ortools/sat/circuit.cc +++ b/ortools/sat/circuit.cc @@ -13,11 +13,19 @@ #include "ortools/sat/circuit.h" -#include +#include +#include +#include #include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" +#include "ortools/base/logging.h" #include "ortools/base/map_util.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_solver.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/circuit.h b/ortools/sat/circuit.h index bc1618e975..897075313d 100644 --- a/ortools/sat/circuit.h +++ b/ortools/sat/circuit.h @@ -16,6 +16,8 @@ #include #include +#include +#include #include #include "absl/container/flat_hash_map.h" diff --git a/ortools/sat/clause.cc b/ortools/sat/clause.cc index 837aaa9223..301e6f17c2 100644 --- a/ortools/sat/clause.cc +++ b/ortools/sat/clause.cc @@ -13,18 +13,35 @@ #include "ortools/sat/clause.h" +#include + #include #include -#include -#include +#include #include +#include #include +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" +#include "absl/container/inlined_vector.h" +#include "absl/random/bit_gen_ref.h" +#include "absl/random/distributions.h" +#include "absl/types/span.h" +#include "ortools/base/hash.h" #include "ortools/base/logging.h" +#include "ortools/base/map_util.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" #include "ortools/base/timer.h" #include "ortools/graph/strongly_connected_components.h" +#include "ortools/sat/drat_proof_handler.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/util/bitset.h" +#include "ortools/util/stats.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/clause.h b/ortools/sat/clause.h index e829233fec..6b4f9f50d8 100644 --- a/ortools/sat/clause.h +++ b/ortools/sat/clause.h @@ -23,6 +23,7 @@ #include #include +#include "absl/base/attributes.h" #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" #include "absl/container/inlined_vector.h" @@ -30,6 +31,7 @@ #include "absl/types/span.h" #include "ortools/base/hash.h" #include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" #include "ortools/base/macros.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/drat_proof_handler.h" diff --git a/ortools/sat/cp_constraints.cc b/ortools/sat/cp_constraints.cc index 6b9d55b46f..e81f3b688e 100644 --- a/ortools/sat/cp_constraints.cc +++ b/ortools/sat/cp_constraints.cc @@ -14,11 +14,13 @@ #include "ortools/sat/cp_constraints.h" #include +#include -#include "absl/container/flat_hash_map.h" -#include "ortools/base/map_util.h" -#include "ortools/sat/sat_solver.h" -#include "ortools/util/sort.h" +#include "absl/types/span.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_constraints.h b/ortools/sat/cp_constraints.h index ab0e6a33bb..8d1f5baf0b 100644 --- a/ortools/sat/cp_constraints.h +++ b/ortools/sat/cp_constraints.h @@ -19,6 +19,7 @@ #include #include +#include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/macros.h" diff --git a/ortools/sat/cp_model.cc b/ortools/sat/cp_model.cc index 92cc64cece..6f2df586f1 100644 --- a/ortools/sat/cp_model.cc +++ b/ortools/sat/cp_model.cc @@ -17,13 +17,16 @@ #include #include #include +#include +#include "absl/container/flat_hash_map.h" +#include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" -#include "ortools/base/map_util.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.pb.h" -#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/cp_model_utils.h" -#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model.h b/ortools/sat/cp_model.h index a24ff75d7a..c7177dd041 100644 --- a/ortools/sat/cp_model.h +++ b/ortools/sat/cp_model.h @@ -40,9 +40,11 @@ #include #include +#include #include #include #include +#include #include "absl/container/flat_hash_map.h" #include "absl/types/span.h" @@ -57,8 +59,8 @@ namespace operations_research { namespace sat { class CpModelBuilder; -class LinearExpr; class IntVar; +class LinearExpr; /** * A Boolean variable. diff --git a/ortools/sat/cp_model_checker.cc b/ortools/sat/cp_model_checker.cc index 0b3e4f35f5..4a06f341ab 100644 --- a/ortools/sat/cp_model_checker.cc +++ b/ortools/sat/cp_model_checker.cc @@ -14,20 +14,24 @@ #include "ortools/sat/cp_model_checker.h" #include +#include #include +#include #include -#include +#include +#include #include +#include #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" +#include "absl/meta/type_traits.h" #include "absl/strings/str_cat.h" -#include "ortools/base/hash.h" #include "ortools/base/logging.h" -#include "ortools/base/map_util.h" #include "ortools/port/proto_utils.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/saturated_arithmetic.h" #include "ortools/util/sorted_interval_list.h" diff --git a/ortools/sat/cp_model_expand.cc b/ortools/sat/cp_model_expand.cc index 3f954e562f..198964aef9 100644 --- a/ortools/sat/cp_model_expand.cc +++ b/ortools/sat/cp_model_expand.cc @@ -18,16 +18,24 @@ #include #include #include +#include +#include #include "absl/container/flat_hash_map.h" -#include "ortools/base/hash.h" -#include "ortools/base/map_util.h" +#include "absl/container/flat_hash_set.h" +#include "absl/meta/type_traits.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" +#include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" #include "ortools/port/proto_utils.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/presolve_context.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/util.h" +#include "ortools/util/logging.h" #include "ortools/util/saturated_arithmetic.h" #include "ortools/util/sorted_interval_list.h" diff --git a/ortools/sat/cp_model_lns.cc b/ortools/sat/cp_model_lns.cc index 3b6a19a48f..ddc532d7c9 100644 --- a/ortools/sat/cp_model_lns.cc +++ b/ortools/sat/cp_model_lns.cc @@ -14,24 +14,42 @@ #include "ortools/sat/cp_model_lns.h" #include +#include #include #include -#include +#include +#include +#include #include +#include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" +#include "absl/meta/type_traits.h" +#include "absl/random/bit_gen_ref.h" +#include "absl/random/distributions.h" +#include "absl/strings/str_cat.h" #include "absl/strings/str_join.h" #include "absl/synchronization/mutex.h" +#include "absl/time/clock.h" +#include "absl/time/time.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/graph/connected_components.h" #include "ortools/sat/cp_model.pb.h" -#include "ortools/sat/cp_model_mapping.h" +#include "ortools/sat/cp_model_presolve.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/integer.h" -#include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/presolve_context.h" #include "ortools/sat/rins.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/subsolver.h" #include "ortools/sat/synchronization.h" +#include "ortools/util/adaptative_parameter_value.h" #include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model_lns.h b/ortools/sat/cp_model_lns.h index bcd7d2bbf5..25940b7cf2 100644 --- a/ortools/sat/cp_model_lns.h +++ b/ortools/sat/cp_model_lns.h @@ -14,21 +14,33 @@ #ifndef OR_TOOLS_SAT_CP_MODEL_LNS_H_ #define OR_TOOLS_SAT_CP_MODEL_LNS_H_ +#include #include +#include +#include +#include #include +#include "absl/base/thread_annotations.h" #include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" #include "absl/random/bit_gen_ref.h" #include "absl/synchronization/mutex.h" +#include "absl/time/time.h" #include "absl/types/span.h" #include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_presolve.h" +#include "ortools/sat/integer.h" #include "ortools/sat/model.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/subsolver.h" #include "ortools/sat/synchronization.h" #include "ortools/util/adaptative_parameter_value.h" #include "ortools/util/logging.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model_loader.cc b/ortools/sat/cp_model_loader.cc index 52bdb7735f..4eaa3e63a5 100644 --- a/ortools/sat/cp_model_loader.cc +++ b/ortools/sat/cp_model_loader.cc @@ -16,7 +16,6 @@ #include #include #include -#include #include #include #include @@ -25,15 +24,20 @@ #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" +#include "absl/memory/memory.h" +#include "absl/meta/type_traits.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" +#include "ortools/algorithms/sparse_permutation.h" #include "ortools/base/logging.h" #include "ortools/base/map_util.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" -#include "ortools/base/vlog_is_on.h" #include "ortools/sat/all_different.h" #include "ortools/sat/circuit.h" #include "ortools/sat/cp_constraints.h" #include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/cumulative.h" #include "ortools/sat/diffn.h" @@ -42,16 +46,14 @@ #include "ortools/sat/integer.h" #include "ortools/sat/integer_expr.h" #include "ortools/sat/intervals.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/pb_constraint.h" -#include "ortools/sat/precedences.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/symmetry.h" -#include "ortools/sat/table.h" -#include "ortools/sat/timetable.h" #include "ortools/util/logging.h" -#include "ortools/util/saturated_arithmetic.h" #include "ortools/util/sorted_interval_list.h" #include "ortools/util/strong_integers.h" diff --git a/ortools/sat/cp_model_mapping.h b/ortools/sat/cp_model_mapping.h index ad28fd28f2..6269d441c5 100644 --- a/ortools/sat/cp_model_mapping.h +++ b/ortools/sat/cp_model_mapping.h @@ -20,6 +20,7 @@ #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" +#include "absl/meta/type_traits.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/strong_vector.h" diff --git a/ortools/sat/cp_model_objective.cc b/ortools/sat/cp_model_objective.cc index 602de4fe43..b2ffe5e62d 100644 --- a/ortools/sat/cp_model_objective.cc +++ b/ortools/sat/cp_model_objective.cc @@ -13,9 +13,14 @@ #include "ortools/sat/cp_model_objective.h" +#include #include +#include +#include "ortools/base/logging.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model_postsolve.cc b/ortools/sat/cp_model_postsolve.cc index 9ed2de7909..2914f07c3d 100644 --- a/ortools/sat/cp_model_postsolve.cc +++ b/ortools/sat/cp_model_postsolve.cc @@ -13,10 +13,15 @@ #include "ortools/sat/cp_model_postsolve.h" +#include #include #include +#include +#include "ortools/base/logging.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model_presolve.cc b/ortools/sat/cp_model_presolve.cc index 1aa10a7afb..804f2236e7 100644 --- a/ortools/sat/cp_model_presolve.cc +++ b/ortools/sat/cp_model_presolve.cc @@ -13,18 +13,16 @@ #include "ortools/sat/cp_model_presolve.h" -#include - #include +#include #include #include #include #include #include -#include -#include #include #include +#include #include #include @@ -32,31 +30,43 @@ #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" #include "absl/hash/hash.h" -#include "absl/random/random.h" -#include "absl/strings/str_join.h" +#include "absl/meta/type_traits.h" +#include "absl/numeric/int128.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/map_util.h" #include "ortools/base/mathutil.h" #include "ortools/base/stl_util.h" -#include "ortools/port/proto_utils.h" +#include "ortools/base/timer.h" #include "ortools/sat/circuit.h" +#include "ortools/sat/clause.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_checker.h" #include "ortools/sat/cp_model_expand.h" -#include "ortools/sat/cp_model_loader.h" #include "ortools/sat/cp_model_mapping.h" -#include "ortools/sat/cp_model_objective.h" #include "ortools/sat/cp_model_symmetries.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/diffn_util.h" #include "ortools/sat/inclusion.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/model.h" +#include "ortools/sat/presolve_context.h" #include "ortools/sat/presolve_util.h" #include "ortools/sat/probing.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" #include "ortools/sat/simplification.h" +#include "ortools/sat/util.h" #include "ortools/sat/var_domination.h" +#include "ortools/util/affine_relation.h" +#include "ortools/util/bitset.h" +#include "ortools/util/logging.h" +#include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model_presolve.h b/ortools/sat/cp_model_presolve.h index 8205b01bc8..b7a6eb0c42 100644 --- a/ortools/sat/cp_model_presolve.h +++ b/ortools/sat/cp_model_presolve.h @@ -15,8 +15,12 @@ #define OR_TOOLS_SAT_CP_MODEL_PRESOLVE_H_ #include +#include #include +#include "absl/base/attributes.h" +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/presolve_context.h" @@ -24,6 +28,7 @@ #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/affine_relation.h" #include "ortools/util/bitset.h" +#include "ortools/util/logging.h" #include "ortools/util/sorted_interval_list.h" #include "ortools/util/time_limit.h" diff --git a/ortools/sat/cp_model_search.cc b/ortools/sat/cp_model_search.cc index 645a778ddf..7d6e6ee81a 100644 --- a/ortools/sat/cp_model_search.cc +++ b/ortools/sat/cp_model_search.cc @@ -13,15 +13,31 @@ #include "ortools/sat/cp_model_search.h" +#include #include +#include #include -#include +#include +#include +#include #include "absl/container/flat_hash_map.h" -#include "absl/strings/str_format.h" +#include "absl/container/flat_hash_set.h" +#include "absl/flags/flag.h" +#include "absl/random/distributions.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/string_view.h" +#include "ortools/base/logging.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/integer.h" +#include "ortools/sat/integer_search.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/util.h" +#include "ortools/util/strong_integers.h" // TODO(user): remove this when the code is stable and does not use SCIP // anymore. diff --git a/ortools/sat/cp_model_search.h b/ortools/sat/cp_model_search.h index 1dbef42156..9263a62184 100644 --- a/ortools/sat/cp_model_search.h +++ b/ortools/sat/cp_model_search.h @@ -24,6 +24,8 @@ #include "ortools/sat/integer.h" #include "ortools/sat/integer_search.h" #include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model_solver.cc b/ortools/sat/cp_model_solver.cc index 4cd07a3f1e..e5203dc1f9 100644 --- a/ortools/sat/cp_model_solver.cc +++ b/ortools/sat/cp_model_solver.cc @@ -14,9 +14,10 @@ #include "ortools/sat/cp_model_solver.h" #include -#include #include #include +#include +#include #include #include #include @@ -28,39 +29,35 @@ #include #include +#include "ortools/base/logging.h" +#include "ortools/base/timer.h" #if !defined(__PORTABLE_PLATFORM__) -#include "absl/synchronization/notification.h" #include "google/protobuf/text_format.h" #include "ortools/base/file.h" -#include "ortools/util/sigint.h" #endif // __PORTABLE_PLATFORM__ - -#include "absl/base/attributes.h" +#include "absl/base/thread_annotations.h" #include "absl/container/flat_hash_set.h" +#include "absl/flags/flag.h" #include "absl/memory/memory.h" #include "absl/status/status.h" +#include "absl/status/statusor.h" #include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" #include "absl/strings/str_join.h" #include "absl/strings/str_split.h" +#include "absl/strings/string_view.h" #include "absl/synchronization/mutex.h" +#include "absl/types/span.h" #include "ortools/base/cleanup.h" -#include "ortools/base/commandlineflags.h" -#include "ortools/base/integral_types.h" -#include "ortools/base/logging.h" #include "ortools/base/map_util.h" -#include "ortools/base/threadpool.h" -#include "ortools/base/timer.h" -#include "ortools/base/version.h" -#include "ortools/base/vlog_is_on.h" #include "ortools/graph/connected_components.h" #include "ortools/port/proto_utils.h" -#include "ortools/sat/circuit.h" #include "ortools/sat/clause.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_checker.h" #include "ortools/sat/cp_model_lns.h" #include "ortools/sat/cp_model_loader.h" +#include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/cp_model_postsolve.h" #include "ortools/sat/cp_model_presolve.h" #include "ortools/sat/cp_model_search.h" @@ -73,15 +70,17 @@ #include "ortools/sat/integer.h" #include "ortools/sat/integer_expr.h" #include "ortools/sat/integer_search.h" -#include "ortools/sat/intervals.h" #include "ortools/sat/lb_tree_search.h" +#include "ortools/sat/linear_constraint.h" #include "ortools/sat/linear_programming_constraint.h" #include "ortools/sat/linear_relaxation.h" #include "ortools/sat/lp_utils.h" #include "ortools/sat/max_hs.h" +#include "ortools/sat/model.h" #include "ortools/sat/optimization.h" #include "ortools/sat/parameters_validation.h" #include "ortools/sat/precedences.h" +#include "ortools/sat/presolve_context.h" #include "ortools/sat/probing.h" #include "ortools/sat/rins.h" #include "ortools/sat/sat_base.h" @@ -91,7 +90,13 @@ #include "ortools/sat/simplification.h" #include "ortools/sat/subsolver.h" #include "ortools/sat/synchronization.h" +#include "ortools/sat/util.h" #include "ortools/util/logging.h" +#include "ortools/util/random_engine.h" +#if !defined(__PORTABLE_PLATFORM__) +#include "ortools/util/sigint.h" +#endif // __PORTABLE_PLATFORM__ +#include "ortools/base/version.h" #include "ortools/util/sorted_interval_list.h" #include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" @@ -338,17 +343,54 @@ std::string CpModelStats(const CpModelProto& model_proto) { "\n"); } - const std::string objective_string = - model_proto.has_objective() - ? absl::StrCat(" (", model_proto.objective().vars_size(), - " in objective)") - : (model_proto.has_floating_point_objective() - ? absl::StrCat( - " (", model_proto.floating_point_objective().vars_size(), - " in floating point objective)") - : ""); - absl::StrAppend(&result, "#Variables: ", model_proto.variables_size(), - objective_string, "\n"); + auto count_variables_by_type = + [&model_proto](const google::protobuf::RepeatedField& vars, + int* num_booleans, int* num_integers) { + for (const int ref : vars) { + const auto& var_proto = model_proto.variables(PositiveRef(ref)); + if (var_proto.domain_size() == 2 && var_proto.domain(0) == 0 && + var_proto.domain(1) == 1) { + (*num_booleans)++; + } + } + *num_integers = model_proto.objective().vars_size() - *num_booleans; + }; + + { + int num_boolean_variables_in_objective = 0; + int num_integer_variables_in_objective = 0; + if (model_proto.has_objective()) { + count_variables_by_type(model_proto.objective().vars(), + &num_boolean_variables_in_objective, + &num_integer_variables_in_objective); + } + if (model_proto.has_floating_point_objective()) { + count_variables_by_type(model_proto.floating_point_objective().vars(), + &num_boolean_variables_in_objective, + &num_integer_variables_in_objective); + } + + std::vector obj_vars_strings; + if (num_boolean_variables_in_objective > 0) { + obj_vars_strings.push_back( + absl::StrCat("#bools:", num_boolean_variables_in_objective)); + } + if (num_integer_variables_in_objective > 0) { + obj_vars_strings.push_back( + absl::StrCat("#ints:", num_integer_variables_in_objective)); + } + + const std::string objective_string = + model_proto.has_objective() + ? absl::StrCat(" (", absl::StrJoin(obj_vars_strings, " "), + " in objective)") + : (model_proto.has_floating_point_objective() + ? absl::StrCat(" (", absl::StrJoin(obj_vars_strings, " "), + " in floating point objective)") + : ""); + absl::StrAppend(&result, "#Variables: ", model_proto.variables_size(), + objective_string, "\n"); + } if (num_vars_per_domains.size() < 100) { for (const auto& entry : num_vars_per_domains) { const std::string temp = absl::StrCat(" - ", entry.second, " in ", diff --git a/ortools/sat/cp_model_symmetries.cc b/ortools/sat/cp_model_symmetries.cc index 5a9acef7ed..bbf1fc1866 100644 --- a/ortools/sat/cp_model_symmetries.cc +++ b/ortools/sat/cp_model_symmetries.cc @@ -13,21 +13,41 @@ #include "ortools/sat/cp_model_symmetries.h" +#include + +#include #include #include #include +#include +#include #include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" #include "absl/memory/memory.h" +#include "absl/meta/type_traits.h" +#include "absl/status/status.h" +#include "absl/strings/str_cat.h" #include "absl/strings/str_join.h" -#include "google/protobuf/repeated_field.h" +#include "google/protobuf/message.h" #include "ortools/algorithms/find_graph_symmetries.h" +#include "ortools/algorithms/sparse_permutation.h" #include "ortools/base/hash.h" +#include "ortools/base/logging.h" #include "ortools/base/map_util.h" +#include "ortools/graph/graph.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/cp_model_utils.h" +#include "ortools/sat/model.h" +#include "ortools/sat/presolve_context.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/symmetry_util.h" +#include "ortools/util/affine_relation.h" +#include "ortools/util/logging.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cp_model_utils.cc b/ortools/sat/cp_model_utils.cc index 7272a15756..3cd9d3d93a 100644 --- a/ortools/sat/cp_model_utils.cc +++ b/ortools/sat/cp_model_utils.cc @@ -14,11 +14,16 @@ #include "ortools/sat/cp_model_utils.h" #include +#include #include +#include +#include #include "absl/container/flat_hash_map.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" #include "ortools/sat/cp_model.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/cumulative.cc b/ortools/sat/cumulative.cc index b804d072b8..0f48630566 100644 --- a/ortools/sat/cumulative.cc +++ b/ortools/sat/cumulative.cc @@ -14,12 +14,17 @@ #include "ortools/sat/cumulative.h" #include -#include +#include +#include #include "ortools/base/logging.h" #include "ortools/sat/cumulative_energy.h" #include "ortools/sat/disjunctive.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/integer_expr.h" +#include "ortools/sat/intervals.h" #include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/pb_constraint.h" #include "ortools/sat/precedences.h" #include "ortools/sat/sat_base.h" diff --git a/ortools/sat/cumulative_energy.cc b/ortools/sat/cumulative_energy.cc index c16935cf9d..46387cd542 100644 --- a/ortools/sat/cumulative_energy.cc +++ b/ortools/sat/cumulative_energy.cc @@ -13,12 +13,16 @@ #include "ortools/sat/cumulative_energy.h" -#include +#include #include +#include #include "ortools/base/iterator_adaptors.h" #include "ortools/base/logging.h" -#include "ortools/sat/sat_base.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/intervals.h" +#include "ortools/sat/model.h" +#include "ortools/sat/theta_tree.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/cuts.cc b/ortools/sat/cuts.cc index ae873c9aa1..e6f3b08731 100644 --- a/ortools/sat/cuts.cc +++ b/ortools/sat/cuts.cc @@ -16,23 +16,34 @@ #include #include #include +#include #include #include #include +#include #include #include #include #include "absl/container/btree_set.h" +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" +#include "absl/memory/memory.h" +#include "absl/meta/type_traits.h" #include "ortools/algorithms/knapsack_solver_for_cuts.h" -#include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" +#include "ortools/sat/clause.h" +#include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" #include "ortools/sat/linear_constraint.h" #include "ortools/sat/linear_constraint_manager.h" +#include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" -#include "ortools/sat/util.h" +#include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/cuts.h b/ortools/sat/cuts.h index 4e6ecce11e..63d26cce77 100644 --- a/ortools/sat/cuts.h +++ b/ortools/sat/cuts.h @@ -15,10 +15,15 @@ #define OR_TOOLS_SAT_CUTS_H_ #include +#include #include #include #include +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" diff --git a/ortools/sat/diffn.cc b/ortools/sat/diffn.cc index 7e646c0dcd..cfda187286 100644 --- a/ortools/sat/diffn.cc +++ b/ortools/sat/diffn.cc @@ -16,22 +16,26 @@ #include #include #include +#include #include -#include "absl/container/flat_hash_map.h" -#include "absl/strings/str_join.h" -#include "ortools/base/iterator_adaptors.h" -#include "ortools/base/map_util.h" -#include "ortools/base/stl_util.h" +#include "absl/container/flat_hash_set.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cumulative_energy.h" #include "ortools/sat/diffn_util.h" #include "ortools/sat/disjunctive.h" #include "ortools/sat/integer.h" +#include "ortools/sat/integer_expr.h" #include "ortools/sat/intervals.h" -#include "ortools/sat/sat_solver.h" -#include "ortools/sat/theta_tree.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/timetable.h" -#include "ortools/util/sort.h" +#include "ortools/sat/util.h" +#include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/diffn.h b/ortools/sat/diffn.h index d8776e156c..4ffc810def 100644 --- a/ortools/sat/diffn.h +++ b/ortools/sat/diffn.h @@ -17,6 +17,8 @@ #include #include +#include "absl/container/flat_hash_set.h" +#include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/macros.h" @@ -26,6 +28,7 @@ #include "ortools/sat/intervals.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/util.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/diffn_util.cc b/ortools/sat/diffn_util.cc index 68b98c74c8..2c2da73e49 100644 --- a/ortools/sat/diffn_util.cc +++ b/ortools/sat/diffn_util.cc @@ -13,12 +13,21 @@ #include "ortools/sat/diffn_util.h" -#include -#include -#include +#include +#include +#include +#include + +#include "absl/container/flat_hash_set.h" +#include "absl/random/bit_gen_ref.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/intervals.h" #include "ortools/util/integer_pq.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/diffn_util.h b/ortools/sat/diffn_util.h index d2976e5e45..2a8f647b86 100644 --- a/ortools/sat/diffn_util.h +++ b/ortools/sat/diffn_util.h @@ -14,14 +14,21 @@ #ifndef OR_TOOLS_SAT_DIFFN_UTIL_H_ #define OR_TOOLS_SAT_DIFFN_UTIL_H_ +#include #include +#include +#include +#include #include #include "absl/container/flat_hash_set.h" +#include "absl/random/bit_gen_ref.h" #include "absl/strings/str_format.h" +#include "absl/types/span.h" #include "ortools/graph/connected_components.h" #include "ortools/sat/integer.h" #include "ortools/sat/intervals.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/disjunctive.cc b/ortools/sat/disjunctive.cc index ea9d65f51a..ee5e46079f 100644 --- a/ortools/sat/disjunctive.cc +++ b/ortools/sat/disjunctive.cc @@ -13,16 +13,24 @@ #include "ortools/sat/disjunctive.h" -#include +#include +#include +#include +#include -#include "ortools/base/iterator_adaptors.h" #include "ortools/base/logging.h" #include "ortools/sat/all_different.h" #include "ortools/sat/integer.h" +#include "ortools/sat/intervals.h" +#include "ortools/sat/model.h" +#include "ortools/sat/precedences.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" +#include "ortools/sat/theta_tree.h" #include "ortools/sat/timetable.h" #include "ortools/util/sort.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/doc/README.md b/ortools/sat/doc/README.md index 8652c0a7ef..e38f0a0eba 100644 --- a/ortools/sat/doc/README.md +++ b/ortools/sat/doc/README.md @@ -87,7 +87,13 @@ solve status, the values for each variable in the model if solve was successful, and some metrics. ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/doc/boolean_logic.md b/ortools/sat/doc/boolean_logic.md index 4d0c6015ee..d54919c067 100644 --- a/ortools/sat/doc/boolean_logic.md +++ b/ortools/sat/doc/boolean_logic.md @@ -67,6 +67,9 @@ LiteralSampleSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" namespace operations_research { @@ -165,6 +168,9 @@ BoolOrSampleSat() ### C++ code ```cpp +#include + +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" namespace operations_research { @@ -281,6 +287,9 @@ ReifiedSampleSat() ### C++ code ```cpp +#include + +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" namespace operations_research { diff --git a/ortools/sat/doc/channeling.md b/ortools/sat/doc/channeling.md index 6868192c66..8e907a4741 100644 --- a/ortools/sat/doc/channeling.md +++ b/ortools/sat/doc/channeling.md @@ -116,7 +116,13 @@ ChannelingSampleSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" @@ -424,7 +430,14 @@ BinpackingProblemSat() ### C++ code ```cpp +#include + +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/doc/integer_arithmetic.md b/ortools/sat/doc/integer_arithmetic.md index 939e4439c0..245ae229dd 100644 --- a/ortools/sat/doc/integer_arithmetic.md +++ b/ortools/sat/doc/integer_arithmetic.md @@ -179,7 +179,13 @@ RabbitsAndPheasantsSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -408,9 +414,15 @@ earliness_tardiness_cost_sample_sat() ### C++ code ```cpp +#include + #include +#include "ortools/base/logging.h" +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" @@ -751,9 +763,19 @@ step_function_sample_sat() ### C++ code ```cpp +#include + +#include + +#include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/doc/model.md b/ortools/sat/doc/model.md index b9d657967e..ae90757f2a 100644 --- a/ortools/sat/doc/model.md +++ b/ortools/sat/doc/model.md @@ -129,8 +129,14 @@ SolutionHintingSampleSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -365,8 +371,13 @@ CopyModelSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" -#include "ortools/sat/model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/doc/scheduling.md b/ortools/sat/doc/scheduling.md index 8a611cc834..67746e4fe7 100644 --- a/ortools/sat/doc/scheduling.md +++ b/ortools/sat/doc/scheduling.md @@ -101,7 +101,11 @@ IntervalSampleSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -271,7 +275,11 @@ OptionalIntervalSampleSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -468,9 +476,17 @@ NoOverlapSampleSat() ### C++ code ```cpp +#include + #include +#include "ortools/base/logging.h" +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/sat/model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -842,7 +858,17 @@ RankingSampleSat() ### C++ code ```cpp +#include +#include + +#include + +#include "ortools/base/logging.h" +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/doc/solver.md b/ortools/sat/doc/solver.md index 42413310a8..576edd898d 100644 --- a/ortools/sat/doc/solver.md +++ b/ortools/sat/doc/solver.md @@ -77,9 +77,15 @@ SolveWithTimeLimitSampleSat() ### Specifying the time limit in C++ ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -274,8 +280,14 @@ SolveAndPrintIntermediateSolutionsSampleSat() ### C++ code ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -528,9 +540,15 @@ SearchForAllSolutionsSampleSat() To search for all solutions, a parameter of the SAT solver must be changed. ```cpp +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { @@ -778,11 +796,17 @@ Stopping search is done by registering an atomic bool on the model-owned time limit, and setting that bool to true. ```cpp +#include + #include +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/drat_checker.cc b/ortools/sat/drat_checker.cc index 4ae8aff292..0732e4af93 100644 --- a/ortools/sat/drat_checker.cc +++ b/ortools/sat/drat_checker.cc @@ -13,15 +13,28 @@ #include "ortools/sat/drat_checker.h" +#include + #include +#include #include #include +#include +#include +#include +#include +#include "absl/container/flat_hash_set.h" #include "absl/strings/numbers.h" #include "absl/strings/str_split.h" +#include "absl/strings/string_view.h" #include "absl/time/clock.h" +#include "absl/types/span.h" #include "ortools/base/hash.h" -#include "ortools/base/stl_util.h" +#include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" +#include "ortools/sat/sat_base.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/drat_checker.h b/ortools/sat/drat_checker.h index 72326febab..ead02691d3 100644 --- a/ortools/sat/drat_checker.h +++ b/ortools/sat/drat_checker.h @@ -15,10 +15,13 @@ #define OR_TOOLS_SAT_DRAT_CHECKER_H_ #include +#include #include +#include #include #include "absl/container/flat_hash_set.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/sat_base.h" diff --git a/ortools/sat/drat_proof_handler.cc b/ortools/sat/drat_proof_handler.cc index 8aaf2415d9..5c655f40a1 100644 --- a/ortools/sat/drat_proof_handler.cc +++ b/ortools/sat/drat_proof_handler.cc @@ -14,10 +14,21 @@ #include "ortools/sat/drat_proof_handler.h" #include +#include +#include +#include +#include -#include "absl/memory/memory.h" #include "ortools/base/logging.h" +#if !defined(__PORTABLE_PLATFORM__) +#include "ortools/base/file.h" +#endif // !defined(__PORTABLE_PLATFORM__) +#include "absl/memory/memory.h" +#include "absl/types/span.h" #include "ortools/base/strong_vector.h" +#include "ortools/sat/drat_checker.h" +#include "ortools/sat/drat_writer.h" +#include "ortools/sat/sat_base.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/drat_proof_handler.h b/ortools/sat/drat_proof_handler.h index 8d5de05e81..0c024861ea 100644 --- a/ortools/sat/drat_proof_handler.h +++ b/ortools/sat/drat_proof_handler.h @@ -18,6 +18,9 @@ #include #include +#if !defined(__PORTABLE_PLATFORM__) +#include "ortools/base/file.h" +#endif // !defined(__PORTABLE_PLATFORM__) #include "absl/types/span.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/drat_checker.h" diff --git a/ortools/sat/drat_writer.cc b/ortools/sat/drat_writer.cc index bbf6392091..89e6761b71 100644 --- a/ortools/sat/drat_writer.cc +++ b/ortools/sat/drat_writer.cc @@ -13,14 +13,16 @@ #include "ortools/sat/drat_writer.h" -#include +#include -#include "absl/strings/str_format.h" #include "ortools/base/logging.h" #if !defined(__PORTABLE_PLATFORM__) #include "ortools/base/file.h" #endif // !__PORTABLE_PLATFORM__ #include "absl/status/status.h" +#include "absl/strings/str_format.h" +#include "absl/types/span.h" +#include "ortools/sat/sat_base.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/encoding.cc b/ortools/sat/encoding.cc index fe8e0a058f..acc75dcc77 100644 --- a/ortools/sat/encoding.cc +++ b/ortools/sat/encoding.cc @@ -16,10 +16,16 @@ #include #include #include -#include #include +#include +#include "ortools/base/logging.h" +#include "ortools/sat/boolean_problem.pb.h" +#include "ortools/sat/pb_constraint.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/feasibility_pump.cc b/ortools/sat/feasibility_pump.cc index 26ae6d22fc..0dfa807ddc 100644 --- a/ortools/sat/feasibility_pump.cc +++ b/ortools/sat/feasibility_pump.cc @@ -13,17 +13,38 @@ #include "ortools/sat/feasibility_pump.h" +#include +#include #include +#include #include +#include #include -#include "ortools/base/integral_types.h" +#include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" +#include "ortools/base/logging.h" +#include "ortools/base/map_util.h" +#include "ortools/base/strong_vector.h" +#include "ortools/glop/parameters.pb.h" +#include "ortools/glop/revised_simplex.h" +#include "ortools/glop/status.h" +#include "ortools/lp_data/lp_data.h" +#include "ortools/lp_data/lp_data_utils.h" #include "ortools/lp_data/lp_types.h" -#include "ortools/sat/cp_model.pb.h" +#include "ortools/lp_data/sparse_column.h" +#include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/integer.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" +#include "ortools/sat/synchronization.h" #include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/feasibility_pump.h b/ortools/sat/feasibility_pump.h index 90f91d1999..9fc8b1877f 100644 --- a/ortools/sat/feasibility_pump.h +++ b/ortools/sat/feasibility_pump.h @@ -14,8 +14,12 @@ #ifndef OR_TOOLS_SAT_FEASIBILITY_PUMP_H_ #define OR_TOOLS_SAT_FEASIBILITY_PUMP_H_ +#include #include +#include +#include +#include "absl/container/flat_hash_map.h" #include "ortools/base/strong_vector.h" #include "ortools/glop/revised_simplex.h" #include "ortools/lp_data/lp_data.h" @@ -24,9 +28,13 @@ #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/integer.h" #include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/implied_bounds.cc b/ortools/sat/implied_bounds.cc index 54eda98f21..bec329e531 100644 --- a/ortools/sat/implied_bounds.cc +++ b/ortools/sat/implied_bounds.cc @@ -13,11 +13,28 @@ #include "ortools/sat/implied_bounds.h" +#include + #include #include +#include +#include +#include +#include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" +#include "absl/strings/str_cat.h" +#include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" #include "ortools/sat/integer.h" #include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/util/bitset.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/implied_bounds.h b/ortools/sat/implied_bounds.h index 3ce97cc1a7..2b5f90ad45 100644 --- a/ortools/sat/implied_bounds.h +++ b/ortools/sat/implied_bounds.h @@ -16,6 +16,7 @@ #include #include +#include #include #include "absl/container/flat_hash_map.h" @@ -26,6 +27,8 @@ #include "ortools/sat/linear_constraint.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" #include "ortools/util/bitset.h" #include "ortools/util/strong_integers.h" diff --git a/ortools/sat/inclusion.h b/ortools/sat/inclusion.h index fe14a71747..cd2712315f 100644 --- a/ortools/sat/inclusion.h +++ b/ortools/sat/inclusion.h @@ -14,10 +14,18 @@ #ifndef OR_TOOLS_SAT_INCLUSION_H_ #define OR_TOOLS_SAT_INCLUSION_H_ +#include +#include + #include +#include #include +#include +#include +#include #include +#include "absl/types/span.h" #include "ortools/base/logging.h" namespace operations_research { diff --git a/ortools/sat/integer.cc b/ortools/sat/integer.cc index fe2a45296c..a0b7cf0d7b 100644 --- a/ortools/sat/integer.cc +++ b/ortools/sat/integer.cc @@ -15,13 +15,30 @@ #include #include +#include +#include #include -#include -#include +#include +#include +#include +#include +#include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" #include "absl/strings/str_cat.h" -#include "ortools/base/iterator_adaptors.h" -#include "ortools/base/stl_util.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" +#include "ortools/base/map_util.h" +#include "ortools/base/strong_vector.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/util/bitset.h" +#include "ortools/util/rev.h" +#include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/integer.h b/ortools/sat/integer.h index 2ee55c8392..448f2e053c 100644 --- a/ortools/sat/integer.h +++ b/ortools/sat/integer.h @@ -14,6 +14,9 @@ #ifndef OR_TOOLS_SAT_INTEGER_H_ #define OR_TOOLS_SAT_INTEGER_H_ +#include + +#include #include #include #include @@ -28,6 +31,7 @@ #include "absl/container/flat_hash_map.h" #include "absl/container/inlined_vector.h" #include "absl/strings/str_cat.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/hash.h" #include "ortools/base/integral_types.h" @@ -38,12 +42,14 @@ #include "ortools/graph/iterators.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/util/bitset.h" #include "ortools/util/rev.h" #include "ortools/util/saturated_arithmetic.h" #include "ortools/util/sorted_interval_list.h" #include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/integer_expr.cc b/ortools/sat/integer_expr.cc index 6478ec0212..59a5ff0711 100644 --- a/ortools/sat/integer_expr.cc +++ b/ortools/sat/integer_expr.cc @@ -15,15 +15,27 @@ #include #include -#include +#include +#include +#include #include #include "absl/container/flat_hash_map.h" #include "absl/memory/memory.h" +#include "absl/types/span.h" +#include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" +#include "ortools/base/mathutil.h" #include "ortools/base/stl_util.h" #include "ortools/sat/integer.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_solver.h" #include "ortools/sat/util.h" +#include "ortools/util/saturated_arithmetic.h" #include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { @@ -1404,7 +1416,7 @@ bool FixedModuloPropagator::PropagateOuterBounds() { bool FixedModuloPropagator::PropagateBoundsWhenExprIsPositive( AffineExpression expr, AffineExpression target) { const IntegerValue min_target = integer_trail_->LowerBound(target); - DCHECK_GE(min_target, 0) << target.DebugString(); + DCHECK_GE(min_target, 0); const IntegerValue max_target = integer_trail_->UpperBound(target); // The propagation rules below will not be triggered if the domain of target diff --git a/ortools/sat/integer_expr.h b/ortools/sat/integer_expr.h index 8378ece329..95872a428e 100644 --- a/ortools/sat/integer_expr.h +++ b/ortools/sat/integer_expr.h @@ -14,10 +14,15 @@ #ifndef OR_TOOLS_SAT_INTEGER_EXPR_H_ #define OR_TOOLS_SAT_INTEGER_EXPR_H_ +#include +#include #include +#include #include +#include #include +#include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/macros.h" @@ -30,6 +35,7 @@ #include "ortools/sat/sat_solver.h" #include "ortools/util/rev.h" #include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/integer_search.cc b/ortools/sat/integer_search.cc index 7ffe790e34..0f0ff22044 100644 --- a/ortools/sat/integer_search.cc +++ b/ortools/sat/integer_search.cc @@ -13,26 +13,39 @@ #include "ortools/sat/integer_search.h" +#include #include #include #include -#include +#include #include #include "absl/container/flat_hash_set.h" +#include "absl/strings/str_cat.h" +#include "absl/time/clock.h" #include "absl/time/time.h" -#include "absl/types/span.h" +#include "ortools/base/logging.h" +#include "ortools/base/map_util.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" +#include "ortools/sat/intervals.h" +#include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/probing.h" +#include "ortools/sat/pseudo_costs.h" +#include "ortools/sat/restart.h" #include "ortools/sat/rins.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_decision.h" #include "ortools/sat/sat_inprocessing.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" #include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/integer_search.h b/ortools/sat/integer_search.h index d03e230f81..2ab6af2707 100644 --- a/ortools/sat/integer_search.h +++ b/ortools/sat/integer_search.h @@ -23,16 +23,27 @@ #ifndef OR_TOOLS_SAT_INTEGER_SEARCH_H_ #define OR_TOOLS_SAT_INTEGER_SEARCH_H_ +#include + +#include #include +#include "absl/container/flat_hash_set.h" +#include "absl/time/time.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" +#include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" #include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/probing.h" #include "ortools/sat/pseudo_costs.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/synchronization.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/intervals.cc b/ortools/sat/intervals.cc index 1028c2716e..10a6477d25 100644 --- a/ortools/sat/intervals.cc +++ b/ortools/sat/intervals.cc @@ -14,11 +14,23 @@ #include "ortools/sat/intervals.h" #include -#include #include +#include +#include +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" #include "ortools/sat/integer.h" +#include "ortools/sat/integer_expr.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/precedences.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_solver.h" #include "ortools/util/sort.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/intervals.h b/ortools/sat/intervals.h index 36ae924b17..8b81b9a074 100644 --- a/ortools/sat/intervals.h +++ b/ortools/sat/intervals.h @@ -19,6 +19,8 @@ #include #include +#include "absl/base/attributes.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" @@ -32,6 +34,7 @@ #include "ortools/sat/precedences.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_solver.h" +#include "ortools/util/rev.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/lb_tree_search.cc b/ortools/sat/lb_tree_search.cc index 5ed3a095a3..66b71c2772 100644 --- a/ortools/sat/lb_tree_search.cc +++ b/ortools/sat/lb_tree_search.cc @@ -13,10 +13,34 @@ #include "ortools/sat/lb_tree_search.h" +#include #include +#include +#include +#include +#include +#include +#include "absl/random/distributions.h" +#include "absl/strings/str_cat.h" +#include "absl/time/clock.h" +#include "absl/time/time.h" +#include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" #include "ortools/sat/cp_model_mapping.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/integer_expr.h" #include "ortools/sat/integer_search.h" +#include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_decision.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/sat/synchronization.h" +#include "ortools/sat/util.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/lb_tree_search.h b/ortools/sat/lb_tree_search.h index 4153075fd1..d21e5238f8 100644 --- a/ortools/sat/lb_tree_search.h +++ b/ortools/sat/lb_tree_search.h @@ -14,16 +14,28 @@ #ifndef OR_TOOLS_SAT_LB_TREE_SEARCH_H_ #define OR_TOOLS_SAT_LB_TREE_SEARCH_H_ +#include + +#include +#include #include #include +#include "absl/strings/string_view.h" +#include "absl/time/time.h" +#include "ortools/base/strong_vector.h" #include "ortools/sat/integer.h" #include "ortools/sat/integer_search.h" #include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_decision.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/synchronization.h" +#include "ortools/sat/util.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { @@ -51,7 +63,7 @@ class LbTreeSearch { private: // Code a binary tree. - DEFINE_STRONG_INT_TYPE(NodeIndex, int); + DEFINE_STRONG_INDEX_TYPE(NodeIndex); struct Node { Node(Literal l, IntegerValue lb) : literal(l), true_objective(lb), false_objective(lb) {} diff --git a/ortools/sat/linear_constraint.cc b/ortools/sat/linear_constraint.cc index fb50dd3f30..2c61794349 100644 --- a/ortools/sat/linear_constraint.cc +++ b/ortools/sat/linear_constraint.cc @@ -13,11 +13,25 @@ #include "ortools/sat/linear_constraint.h" +#include +#include #include +#include +#include +#include +#include +#include +#include "absl/base/attributes.h" +#include "absl/container/flat_hash_set.h" +#include "absl/strings/str_cat.h" +#include "ortools/base/logging.h" #include "ortools/base/mathutil.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/integer.h" +#include "ortools/sat/sat_base.h" +#include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/linear_constraint.h b/ortools/sat/linear_constraint.h index 1bbc689613..602b13dda6 100644 --- a/ortools/sat/linear_constraint.h +++ b/ortools/sat/linear_constraint.h @@ -14,11 +14,19 @@ #ifndef OR_TOOLS_SAT_LINEAR_CONSTRAINT_H_ #define OR_TOOLS_SAT_LINEAR_CONSTRAINT_H_ +#include +#include +#include +#include #include +#include "absl/base/attributes.h" +#include "absl/strings/str_cat.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/integer.h" #include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/linear_constraint_manager.cc b/ortools/sat/linear_constraint_manager.cc index 3b63590381..02eb260a74 100644 --- a/ortools/sat/linear_constraint_manager.cc +++ b/ortools/sat/linear_constraint_manager.cc @@ -15,13 +15,27 @@ #include #include +#include +#include #include +#include +#include #include +#include -#include "absl/container/flat_hash_set.h" +#include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" +#include "absl/strings/str_cat.h" +#include "ortools/base/hash.h" +#include "ortools/base/logging.h" #include "ortools/base/strong_vector.h" +#include "ortools/lp_data/lp_types.h" #include "ortools/sat/integer.h" #include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/linear_constraint_manager.h b/ortools/sat/linear_constraint_manager.h index 69befefab9..bf21d66588 100644 --- a/ortools/sat/linear_constraint_manager.h +++ b/ortools/sat/linear_constraint_manager.h @@ -14,18 +14,25 @@ #ifndef OR_TOOLS_SAT_LINEAR_CONSTRAINT_MANAGER_H_ #define OR_TOOLS_SAT_LINEAR_CONSTRAINT_MANAGER_H_ +#include #include #include +#include +#include +#include #include #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" +#include "absl/strings/string_view.h" #include "ortools/base/strong_vector.h" #include "ortools/glop/revised_simplex.h" +#include "ortools/sat/integer.h" #include "ortools/sat/linear_constraint.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/logging.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { @@ -77,7 +84,7 @@ class LinearConstraintManager { // basic preprocessing. If added is given, it will be set to true if this // constraint was actually a new one and to false if it was dominated by an // already existing one. - DEFINE_STRONG_INT_TYPE(ConstraintIndex, int32_t); + DEFINE_STRONG_INDEX_TYPE(ConstraintIndex); ConstraintIndex Add(LinearConstraint ct, bool* added = nullptr); // Same as Add(), but logs some information about the newly added constraint. diff --git a/ortools/sat/linear_programming_constraint.cc b/ortools/sat/linear_programming_constraint.cc index f9fa12736d..f5a8ab04bb 100644 --- a/ortools/sat/linear_programming_constraint.cc +++ b/ortools/sat/linear_programming_constraint.cc @@ -16,30 +16,51 @@ #include #include #include -#include +#include +#include #include +#include +#include #include #include #include #include "absl/container/flat_hash_map.h" +#include "absl/container/inlined_vector.h" +#include "absl/meta/type_traits.h" #include "absl/numeric/int128.h" -#include "ortools/base/commandlineflags.h" -#include "ortools/base/integral_types.h" +#include "absl/random/distributions.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" #include "ortools/base/logging.h" #include "ortools/base/map_util.h" #include "ortools/base/mathutil.h" -#include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" #include "ortools/glop/parameters.pb.h" -#include "ortools/glop/preprocessor.h" +#include "ortools/glop/revised_simplex.h" #include "ortools/glop/status.h" -#include "ortools/graph/strongly_connected_components.h" +#include "ortools/lp_data/lp_data.h" +#include "ortools/lp_data/lp_data_utils.h" #include "ortools/lp_data/lp_types.h" +#include "ortools/lp_data/scattered_vector.h" +#include "ortools/lp_data/sparse_column.h" +#include "ortools/sat/cuts.h" #include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" +#include "ortools/sat/integer_expr.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/linear_constraint_manager.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/sat/util.h" #include "ortools/sat/zero_half_cuts.h" +#include "ortools/util/bitset.h" +#include "ortools/util/rev.h" #include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/linear_programming_constraint.h b/ortools/sat/linear_programming_constraint.h index 78c314331e..dfb2e88f83 100644 --- a/ortools/sat/linear_programming_constraint.h +++ b/ortools/sat/linear_programming_constraint.h @@ -15,7 +15,10 @@ #define OR_TOOLS_SAT_LINEAR_PROGRAMMING_CONSTRAINT_H_ #include +#include #include +#include +#include #include #include @@ -32,6 +35,8 @@ #include "ortools/sat/linear_constraint.h" #include "ortools/sat/linear_constraint_manager.h" #include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/util.h" #include "ortools/sat/zero_half_cuts.h" #include "ortools/util/rev.h" @@ -128,6 +133,7 @@ class ScatteredIntegerVector { // However, by default, we interpret the LP result by recomputing everything // in integer arithmetic, so we are exact. class LinearProgrammingDispatcher; + class LinearProgrammingConstraint : public PropagatorInterface, ReversibleInterface { public: diff --git a/ortools/sat/linear_relaxation.cc b/ortools/sat/linear_relaxation.cc index 6a1bf8a372..f976bdc2f7 100644 --- a/ortools/sat/linear_relaxation.cc +++ b/ortools/sat/linear_relaxation.cc @@ -16,14 +16,20 @@ #include #include #include +#include +#include #include +#include "absl/base/attributes.h" #include "absl/container/flat_hash_set.h" -#include "ortools/base/iterator_adaptors.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" +#include "ortools/base/strong_vector.h" #include "ortools/sat/circuit.h" // for ReindexArcs. +#include "ortools/sat/clause.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" +#include "ortools/sat/cp_model_utils.h" #include "ortools/sat/cuts.h" #include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" @@ -31,10 +37,15 @@ #include "ortools/sat/intervals.h" #include "ortools/sat/linear_constraint.h" #include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" #include "ortools/sat/scheduling_constraints.h" #include "ortools/sat/scheduling_cuts.h" +#include "ortools/util/logging.h" +#include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/linear_relaxation.h b/ortools/sat/linear_relaxation.h index d6a22a15bd..7e61f75bbc 100644 --- a/ortools/sat/linear_relaxation.h +++ b/ortools/sat/linear_relaxation.h @@ -16,11 +16,14 @@ #include +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" +#include "ortools/sat/cuts.h" #include "ortools/sat/integer.h" #include "ortools/sat/linear_constraint.h" #include "ortools/sat/linear_programming_constraint.h" #include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/lp_utils.cc b/ortools/sat/lp_utils.cc index 4cffe12d01..7cfb34c447 100644 --- a/ortools/sat/lp_utils.cc +++ b/ortools/sat/lp_utils.cc @@ -13,26 +13,31 @@ #include "ortools/sat/lp_utils.h" -#include - #include #include #include +#include #include #include +#include #include #include "absl/strings/str_cat.h" -#include "ortools/base/integral_types.h" #include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" #include "ortools/glop/lp_solver.h" #include "ortools/glop/parameters.pb.h" +#include "ortools/linear_solver/linear_solver.pb.h" +#include "ortools/lp_data/lp_data.h" #include "ortools/lp_data/lp_types.h" #include "ortools/sat/boolean_problem.h" +#include "ortools/sat/boolean_problem.pb.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/integer.h" -#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/fp_utils.h" +#include "ortools/util/logging.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/lp_utils.h b/ortools/sat/lp_utils.h index 919b2330f1..d2cb0bc4fd 100644 --- a/ortools/sat/lp_utils.h +++ b/ortools/sat/lp_utils.h @@ -16,6 +16,11 @@ #ifndef OR_TOOLS_SAT_LP_UTILS_H_ #define OR_TOOLS_SAT_LP_UTILS_H_ +#include + +#include +#include + #include "ortools/linear_solver/linear_solver.pb.h" #include "ortools/lp_data/lp_data.h" #include "ortools/sat/boolean_problem.pb.h" diff --git a/ortools/sat/max_hs.cc b/ortools/sat/max_hs.cc index 1a0d3180cc..b27b8ca332 100644 --- a/ortools/sat/max_hs.cc +++ b/ortools/sat/max_hs.cc @@ -14,42 +14,37 @@ #include "ortools/sat/max_hs.h" #include +#include #include -#include -#include -#include #include #include -#include -#include -#include -#include #include +#include #include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" -#include "absl/random/bit_gen_ref.h" +#include "absl/flags/flag.h" +#include "absl/meta/type_traits.h" #include "absl/random/random.h" -#include "absl/strings/str_cat.h" -#include "absl/strings/str_format.h" +#include "absl/strings/string_view.h" #include "ortools/base/cleanup.h" #include "ortools/base/logging.h" -#include "ortools/base/macros.h" -#include "ortools/base/timer.h" +#include "ortools/base/strong_vector.h" #if !defined(__PORTABLE_PLATFORM__) && defined(USE_SCIP) #include "ortools/linear_solver/linear_solver.h" #endif // __PORTABLE_PLATFORM__ #include "ortools/linear_solver/linear_solver.pb.h" -#include "ortools/port/proto_utils.h" -#include "ortools/sat/boolean_problem.h" -#include "ortools/sat/cp_model_utils.h" -#include "ortools/sat/encoding.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/integer.h" -#include "ortools/sat/integer_expr.h" +#include "ortools/sat/integer_search.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/linear_relaxation.h" #include "ortools/sat/model.h" #include "ortools/sat/optimization.h" -#include "ortools/sat/pb_constraint.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" #include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" #include "ortools/util/strong_integers.h" @@ -300,17 +295,9 @@ void HittingSetOptimizer::ProjectAndAddAtMostOne( } } - int num_extracted_variables = 0; - const LinearConstraint linear = builder.Build(); - for (const IntegerVariable var : linear.vars) { - if (GetExtractedIndex(var) != kUnextracted) num_extracted_variables++; + if (ProjectAndAddLinear(builder.Build()) != nullptr) { + num_extracted_at_most_ones_++; } - - if (num_extracted_variables <= 1) return; - - MPConstraintProto* ct = request_.mutable_model()->add_constraint(); - ProjectLinear(linear, ct); - num_extracted_at_most_ones_++; } MPConstraintProto* HittingSetOptimizer::ProjectAndAddLinear( diff --git a/ortools/sat/max_hs.h b/ortools/sat/max_hs.h index 60cc6738b2..c1801fa6d6 100644 --- a/ortools/sat/max_hs.h +++ b/ortools/sat/max_hs.h @@ -14,19 +14,29 @@ #ifndef OR_TOOLS_SAT_MAX_HS_H_ #define OR_TOOLS_SAT_MAX_HS_H_ +#include + +#include #include +#include +#include #include "absl/container/flat_hash_map.h" +#include "ortools/base/strong_vector.h" #include "ortools/linear_solver/linear_solver.pb.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/integer.h" #include "ortools/sat/integer_search.h" +#include "ortools/sat/linear_constraint.h" #include "ortools/sat/linear_relaxation.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/model.h b/ortools/sat/model.h index e24aad13e5..8500ef5b4e 100644 --- a/ortools/sat/model.h +++ b/ortools/sat/model.h @@ -15,12 +15,17 @@ #define OR_TOOLS_SAT_MODEL_H_ #include +#include +#include #include #include #include +#include +#include #include #include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" #include "ortools/base/logging.h" #include "ortools/base/macros.h" #include "ortools/base/map_util.h" diff --git a/ortools/sat/optimization.cc b/ortools/sat/optimization.cc index 45e9e07f4a..403531b3ec 100644 --- a/ortools/sat/optimization.cc +++ b/ortools/sat/optimization.cc @@ -14,17 +14,19 @@ #include "ortools/sat/optimization.h" #include +#include #include -#include #include #include +#include #include #include -#include #include #include #include +#include +#include "absl/container/flat_hash_set.h" #include "absl/random/bit_gen_ref.h" #include "absl/random/random.h" #include "absl/strings/str_cat.h" @@ -34,13 +36,19 @@ #include "ortools/base/macros.h" #include "ortools/base/map_util.h" #include "ortools/base/stl_util.h" -#include "ortools/base/timer.h" #include "ortools/port/proto_utils.h" #include "ortools/sat/boolean_problem.h" +#include "ortools/sat/boolean_problem.pb.h" #include "ortools/sat/encoding.h" +#include "ortools/sat/integer.h" #include "ortools/sat/integer_expr.h" +#include "ortools/sat/integer_search.h" +#include "ortools/sat/model.h" #include "ortools/sat/pb_constraint.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/sat/synchronization.h" #include "ortools/sat/util.h" #include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" diff --git a/ortools/sat/optimization.h b/ortools/sat/optimization.h index 58d160744e..f28d2f4f83 100644 --- a/ortools/sat/optimization.h +++ b/ortools/sat/optimization.h @@ -17,13 +17,17 @@ #include #include +#include "absl/random/bit_gen_ref.h" #include "ortools/sat/boolean_problem.pb.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/integer.h" #include "ortools/sat/integer_search.h" #include "ortools/sat/model.h" +#include "ortools/sat/pb_constraint.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/parameters_validation.cc b/ortools/sat/parameters_validation.cc index adf4a46b71..ae058505d9 100644 --- a/ortools/sat/parameters_validation.cc +++ b/ortools/sat/parameters_validation.cc @@ -13,6 +13,10 @@ #include "ortools/sat/parameters_validation.h" +#include + +#include "ortools/sat/sat_parameters.pb.h" + namespace operations_research { namespace sat { diff --git a/ortools/sat/pb_constraint.cc b/ortools/sat/pb_constraint.cc index 48cc2b1c93..63d864e861 100644 --- a/ortools/sat/pb_constraint.cc +++ b/ortools/sat/pb_constraint.cc @@ -13,12 +13,24 @@ #include "ortools/sat/pb_constraint.h" +#include +#include +#include #include +#include +#include "absl/container/flat_hash_map.h" #include "absl/hash/hash.h" #include "absl/strings/str_format.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/base/strong_vector.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/bitset.h" #include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/stats.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/pb_constraint.h b/ortools/sat/pb_constraint.h index cf8da241f5..0fcf9f44a9 100644 --- a/ortools/sat/pb_constraint.h +++ b/ortools/sat/pb_constraint.h @@ -22,11 +22,11 @@ #include #include "absl/container/flat_hash_map.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/macros.h" -#include "ortools/base/strong_int.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" diff --git a/ortools/sat/precedences.cc b/ortools/sat/precedences.cc index 0e7cf8f527..b163094cf5 100644 --- a/ortools/sat/precedences.cc +++ b/ortools/sat/precedences.cc @@ -14,14 +14,26 @@ #include "ortools/sat/precedences.h" #include -#include +#include +#include +#include +#include "absl/container/inlined_vector.h" +#include "absl/types/span.h" #include "ortools/base/cleanup.h" #include "ortools/base/logging.h" +#include "ortools/base/map_util.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/clause.h" #include "ortools/sat/cp_constraints.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/util/bitset.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/precedences.h b/ortools/sat/precedences.h index a699785bd0..44545b065d 100644 --- a/ortools/sat/precedences.h +++ b/ortools/sat/precedences.h @@ -20,6 +20,8 @@ #include #include "absl/container/inlined_vector.h" +#include "absl/strings/string_view.h" +#include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/macros.h" #include "ortools/base/strong_vector.h" diff --git a/ortools/sat/presolve_context.cc b/ortools/sat/presolve_context.cc index 6386023a28..3eacb87fc6 100644 --- a/ortools/sat/presolve_context.cc +++ b/ortools/sat/presolve_context.cc @@ -15,16 +15,41 @@ #include #include +#include #include +#include +#include #include +#include +#include +#include +#include "absl/base/attributes.h" +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" +#include "absl/meta/type_traits.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/base/map_util.h" #include "ortools/base/mathutil.h" #include "ortools/port/proto_utils.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_loader.h" +#include "ortools/sat/cp_model_mapping.h" +#include "ortools/sat/cp_model_utils.h" +#include "ortools/sat/integer.h" #include "ortools/sat/lp_utils.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/sat/util.h" +#include "ortools/util/affine_relation.h" +#include "ortools/util/bitset.h" +#include "ortools/util/logging.h" #include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/presolve_context.h b/ortools/sat/presolve_context.h index 3b0e1c027f..58d313581c 100644 --- a/ortools/sat/presolve_context.h +++ b/ortools/sat/presolve_context.h @@ -17,9 +17,16 @@ #include #include #include +#include +#include #include #include "absl/base/attributes.h" +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" #include "ortools/sat/model.h" diff --git a/ortools/sat/presolve_util.cc b/ortools/sat/presolve_util.cc index f7273f35f2..b23115bfee 100644 --- a/ortools/sat/presolve_util.cc +++ b/ortools/sat/presolve_util.cc @@ -13,10 +13,23 @@ #include "ortools/sat/presolve_util.h" +#include #include +#include +#include +#include +#include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/base/map_util.h" +#include "ortools/base/strong_vector.h" +#include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_utils.h" +#include "ortools/util/bitset.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/presolve_util.h b/ortools/sat/presolve_util.h index 3e0b521097..c016b264e4 100644 --- a/ortools/sat/presolve_util.h +++ b/ortools/sat/presolve_util.h @@ -16,9 +16,12 @@ #include #include +#include #include #include "absl/container/flat_hash_map.h" +#include "absl/strings/string_view.h" +#include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/strong_vector.h" diff --git a/ortools/sat/probing.cc b/ortools/sat/probing.cc index 523ae0ce55..eb1296dbb8 100644 --- a/ortools/sat/probing.cc +++ b/ortools/sat/probing.cc @@ -15,18 +15,26 @@ #include #include -#include +#include +#include -#include "ortools/base/iterator_adaptors.h" +#include "absl/container/inlined_vector.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/base/strong_vector.h" #include "ortools/base/timer.h" #include "ortools/sat/clause.h" #include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" +#include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/util.h" +#include "ortools/util/bitset.h" #include "ortools/util/logging.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/probing.h b/ortools/sat/probing.h index 003f67d34a..005dabe257 100644 --- a/ortools/sat/probing.h +++ b/ortools/sat/probing.h @@ -14,14 +14,22 @@ #ifndef OR_TOOLS_SAT_PROBING_H_ #define OR_TOOLS_SAT_PROBING_H_ +#include +#include +#include + +#include "absl/strings/str_cat.h" #include "absl/types/span.h" #include "ortools/sat/clause.h" #include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_solver.h" #include "ortools/sat/util.h" +#include "ortools/util/bitset.h" #include "ortools/util/logging.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/pseudo_costs.cc b/ortools/sat/pseudo_costs.cc index 1ad9e7db35..599b8da726 100644 --- a/ortools/sat/pseudo_costs.cc +++ b/ortools/sat/pseudo_costs.cc @@ -13,13 +13,18 @@ #include "ortools/sat/pseudo_costs.h" -#include +#include +#include #include +#include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" #include "ortools/sat/integer.h" -#include "ortools/sat/sat_decision.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/util.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/pseudo_costs.h b/ortools/sat/pseudo_costs.h index b47bc7e994..e10cd79a63 100644 --- a/ortools/sat/pseudo_costs.h +++ b/ortools/sat/pseudo_costs.h @@ -16,9 +16,14 @@ #include +#include "ortools/base/logging.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/integer.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/util.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/restart.cc b/ortools/sat/restart.cc index 7a74e6b776..ff28cf5828 100644 --- a/ortools/sat/restart.cc +++ b/ortools/sat/restart.cc @@ -13,9 +13,16 @@ #include "ortools/sat/restart.h" +#include +#include + #include "absl/strings/str_format.h" #include "absl/strings/str_split.h" +#include "ortools/base/logging.h" #include "ortools/port/proto_utils.h" +#include "ortools/sat/sat_decision.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/running_stat.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/restart.h b/ortools/sat/restart.h index 906a5f4374..4549a29c86 100644 --- a/ortools/sat/restart.h +++ b/ortools/sat/restart.h @@ -14,8 +14,10 @@ #ifndef OR_TOOLS_SAT_RESTART_H_ #define OR_TOOLS_SAT_RESTART_H_ +#include #include +#include "ortools/base/logging.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_decision.h" #include "ortools/sat/sat_parameters.pb.h" diff --git a/ortools/sat/rins.cc b/ortools/sat/rins.cc index bb5f516a00..aaaa06a600 100644 --- a/ortools/sat/rins.cc +++ b/ortools/sat/rins.cc @@ -13,12 +13,19 @@ #include "ortools/sat/rins.h" +#include #include +#include #include +#include +#include -#include "ortools/sat/cp_model_mapping.h" +#include "absl/random/bit_gen_ref.h" +#include "ortools/base/logging.h" #include "ortools/sat/integer.h" #include "ortools/sat/linear_programming_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/synchronization.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/rins.h b/ortools/sat/rins.h index af12c7a381..6cd8acffbe 100644 --- a/ortools/sat/rins.h +++ b/ortools/sat/rins.h @@ -15,6 +15,7 @@ #define OR_TOOLS_SAT_RINS_H_ #include +#include #include #include "absl/container/flat_hash_map.h" @@ -25,6 +26,7 @@ #include "ortools/sat/linear_programming_constraint.h" #include "ortools/sat/model.h" #include "ortools/sat/synchronization.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/assignment_groups_sat.cc b/ortools/sat/samples/assignment_groups_sat.cc index ab4b124a8a..12c84e0026 100644 --- a/ortools/sat/samples/assignment_groups_sat.cc +++ b/ortools/sat/samples/assignment_groups_sat.cc @@ -14,11 +14,19 @@ // [START program] // Solve assignment problem for given group of workers. // [START import] +#include + +#include #include #include #include "absl/strings/str_format.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" + // [END import] namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/assignment_sat.cc b/ortools/sat/samples/assignment_sat.cc index ff3e085b96..56bc69102a 100644 --- a/ortools/sat/samples/assignment_sat.cc +++ b/ortools/sat/samples/assignment_sat.cc @@ -13,7 +13,15 @@ // [START program] // [START import] +#include + +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" + // [END import] namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/assignment_task_sizes_sat.cc b/ortools/sat/samples/assignment_task_sizes_sat.cc index 9755220e03..c6541fe99d 100644 --- a/ortools/sat/samples/assignment_task_sizes_sat.cc +++ b/ortools/sat/samples/assignment_task_sizes_sat.cc @@ -14,11 +14,18 @@ // [START program] // Solve assignment problem. // [START import] +#include + +#include #include #include #include "absl/strings/str_format.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" + // [END import] namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/assignment_teams_sat.cc b/ortools/sat/samples/assignment_teams_sat.cc index 3e73a26633..75805fb28c 100644 --- a/ortools/sat/samples/assignment_teams_sat.cc +++ b/ortools/sat/samples/assignment_teams_sat.cc @@ -14,12 +14,17 @@ // [START program] // Solve a simple assignment problem. // [START import] -#include +#include + #include #include #include "absl/strings/str_format.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" + // [END import] namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/assumptions_sample_sat.cc b/ortools/sat/samples/assumptions_sample_sat.cc index 2527213d06..a04ee24ee3 100644 --- a/ortools/sat/samples/assumptions_sample_sat.cc +++ b/ortools/sat/samples/assumptions_sample_sat.cc @@ -1,4 +1,4 @@ -// Copyright 2021 Xiang Chen +// Copyright 2010-2021 Google LLC // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. // You may obtain a copy of the License at @@ -13,8 +13,15 @@ // [START program] // [START import] +#include + +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" -#include "ortools/sat/model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" + // [END import] namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/binpacking_problem_sat.cc b/ortools/sat/samples/binpacking_problem_sat.cc index 5218ee0e0a..de1f46823b 100644 --- a/ortools/sat/samples/binpacking_problem_sat.cc +++ b/ortools/sat/samples/binpacking_problem_sat.cc @@ -11,7 +11,14 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/bool_or_sample_sat.cc b/ortools/sat/samples/bool_or_sample_sat.cc index bc4faad1d9..6b1572722f 100644 --- a/ortools/sat/samples/bool_or_sample_sat.cc +++ b/ortools/sat/samples/bool_or_sample_sat.cc @@ -11,6 +11,9 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" namespace operations_research { diff --git a/ortools/sat/samples/channeling_sample_sat.cc b/ortools/sat/samples/channeling_sample_sat.cc index 702471a413..3f4650058e 100644 --- a/ortools/sat/samples/channeling_sample_sat.cc +++ b/ortools/sat/samples/channeling_sample_sat.cc @@ -11,7 +11,13 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" diff --git a/ortools/sat/samples/code_samples.bzl b/ortools/sat/samples/code_samples.bzl index d98c48e388..fbda48207d 100644 --- a/ortools/sat/samples/code_samples.bzl +++ b/ortools/sat/samples/code_samples.bzl @@ -1,23 +1,26 @@ """Helper macro to compile and test code samples.""" def code_sample_cc(name): - native.cc_binary( - name = name, - srcs = [name + ".cc"], - deps = [ - "//ortools/sat:cp_model", - "//ortools/sat:cp_model_solver", - ], - ) - - native.cc_test( - name = name+"_test", - size = "small", - srcs = [name + ".cc"], - deps = [ - ":"+name, - "//ortools/sat:cp_model", - "//ortools/sat:cp_model_solver", - ], - ) + native.cc_binary( + name = name, + srcs = [name + ".cc"], + deps = [ + "//ortools/sat:cp_model", + "//ortools/sat:cp_model_solver", + "//ortools/util:sorted_interval_list", + "@com_google_absl//absl/types:span", + ], + ) + native.cc_test( + name = name + "_test", + size = "small", + srcs = [name + ".cc"], + deps = [ + ":" + name, + "//ortools/sat:cp_model", + "//ortools/sat:cp_model_solver", + "//ortools/util:sorted_interval_list", + "@com_google_absl//absl/types:span", + ], + ) diff --git a/ortools/sat/samples/copy_model_sample_sat.cc b/ortools/sat/samples/copy_model_sample_sat.cc index 4bd02b0eb6..eb5448889c 100644 --- a/ortools/sat/samples/copy_model_sample_sat.cc +++ b/ortools/sat/samples/copy_model_sample_sat.cc @@ -12,8 +12,13 @@ // limitations under the License. // [START program] +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" -#include "ortools/sat/model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/cp_is_fun_sat.cc b/ortools/sat/samples/cp_is_fun_sat.cc index 8c8a8559ba..e7a5285dd8 100644 --- a/ortools/sat/samples/cp_is_fun_sat.cc +++ b/ortools/sat/samples/cp_is_fun_sat.cc @@ -19,12 +19,17 @@ // // This problem has 72 different solutions in base 10. // [START import] -#include -#include +#include +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" // [END import] namespace operations_research { diff --git a/ortools/sat/samples/cp_sat_example.cc b/ortools/sat/samples/cp_sat_example.cc index 9de29000d5..174026ab88 100644 --- a/ortools/sat/samples/cp_sat_example.cc +++ b/ortools/sat/samples/cp_sat_example.cc @@ -13,9 +13,16 @@ // [START program] // [START import] +#include +#include + #include +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" // [END import] namespace operations_research { diff --git a/ortools/sat/samples/earliness_tardiness_cost_sample_sat.cc b/ortools/sat/samples/earliness_tardiness_cost_sample_sat.cc index 4ffe5b1440..df1d61a1f5 100644 --- a/ortools/sat/samples/earliness_tardiness_cost_sample_sat.cc +++ b/ortools/sat/samples/earliness_tardiness_cost_sample_sat.cc @@ -11,9 +11,15 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + #include +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" diff --git a/ortools/sat/samples/interval_sample_sat.cc b/ortools/sat/samples/interval_sample_sat.cc index f6e04ea491..eca1852bfe 100644 --- a/ortools/sat/samples/interval_sample_sat.cc +++ b/ortools/sat/samples/interval_sample_sat.cc @@ -11,7 +11,11 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/literal_sample_sat.cc b/ortools/sat/samples/literal_sample_sat.cc index 8db8c86a05..4c1bb90542 100644 --- a/ortools/sat/samples/literal_sample_sat.cc +++ b/ortools/sat/samples/literal_sample_sat.cc @@ -11,6 +11,9 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" namespace operations_research { diff --git a/ortools/sat/samples/minimal_jobshop_sat.cc b/ortools/sat/samples/minimal_jobshop_sat.cc index dba74501bb..7f078e4392 100644 --- a/ortools/sat/samples/minimal_jobshop_sat.cc +++ b/ortools/sat/samples/minimal_jobshop_sat.cc @@ -14,15 +14,21 @@ // [START program] // Nurse scheduling problem with shift requests. // [START import] -#include +#include + +#include +#include #include #include +#include +#include #include #include "absl/strings/str_format.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" -#include "ortools/sat/model.h" -#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" // [END import] namespace operations_research { diff --git a/ortools/sat/samples/multiple_knapsack_sat.cc b/ortools/sat/samples/multiple_knapsack_sat.cc index d0f5523826..f37d7081ad 100644 --- a/ortools/sat/samples/multiple_knapsack_sat.cc +++ b/ortools/sat/samples/multiple_knapsack_sat.cc @@ -14,13 +14,18 @@ // [START program] // Solves a multiple knapsack problem using the CP-SAT solver. // [START import] +#include + #include #include #include #include #include "absl/strings/str_format.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" // [END import] namespace operations_research { diff --git a/ortools/sat/samples/no_overlap_sample_sat.cc b/ortools/sat/samples/no_overlap_sample_sat.cc index f45305c62e..6b3bc05827 100644 --- a/ortools/sat/samples/no_overlap_sample_sat.cc +++ b/ortools/sat/samples/no_overlap_sample_sat.cc @@ -11,9 +11,17 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + #include +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/sat/model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/nqueens_sat.cc b/ortools/sat/samples/nqueens_sat.cc index 16f88b1aff..f5a37612e9 100644 --- a/ortools/sat/samples/nqueens_sat.cc +++ b/ortools/sat/samples/nqueens_sat.cc @@ -14,13 +14,20 @@ // [START program] // OR-Tools solution to the N-queens problem. // [START import] -#include +#include + +#include +#include #include #include "absl/strings/numbers.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" // [END import] namespace operations_research { diff --git a/ortools/sat/samples/nurses_sat.cc b/ortools/sat/samples/nurses_sat.cc index 61780051ce..64c6840cde 100644 --- a/ortools/sat/samples/nurses_sat.cc +++ b/ortools/sat/samples/nurses_sat.cc @@ -14,14 +14,20 @@ // [START program] // Example of a simple nurse scheduling problem. // [START import] +#include + #include #include #include +#include #include #include #include "absl/strings/str_format.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/time_limit.h" diff --git a/ortools/sat/samples/optional_interval_sample_sat.cc b/ortools/sat/samples/optional_interval_sample_sat.cc index fd876e39b0..d6ba7a42f1 100644 --- a/ortools/sat/samples/optional_interval_sample_sat.cc +++ b/ortools/sat/samples/optional_interval_sample_sat.cc @@ -11,7 +11,11 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/rabbits_and_pheasants_sat.cc b/ortools/sat/samples/rabbits_and_pheasants_sat.cc index 43ab382b20..2a2fcb4cb2 100644 --- a/ortools/sat/samples/rabbits_and_pheasants_sat.cc +++ b/ortools/sat/samples/rabbits_and_pheasants_sat.cc @@ -11,7 +11,13 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/ranking_sample_sat.cc b/ortools/sat/samples/ranking_sample_sat.cc index cc05e970f5..7685f452e4 100644 --- a/ortools/sat/samples/ranking_sample_sat.cc +++ b/ortools/sat/samples/ranking_sample_sat.cc @@ -11,7 +11,17 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include +#include + +#include + +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/reified_sample_sat.cc b/ortools/sat/samples/reified_sample_sat.cc index 0d9ddddffd..815cffd0fc 100644 --- a/ortools/sat/samples/reified_sample_sat.cc +++ b/ortools/sat/samples/reified_sample_sat.cc @@ -11,6 +11,9 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include "absl/types/span.h" #include "ortools/sat/cp_model.h" namespace operations_research { diff --git a/ortools/sat/samples/schedule_requests_sat.cc b/ortools/sat/samples/schedule_requests_sat.cc index a0f59cbea8..a49d5d6e92 100644 --- a/ortools/sat/samples/schedule_requests_sat.cc +++ b/ortools/sat/samples/schedule_requests_sat.cc @@ -14,14 +14,20 @@ // [START program] // Nurse scheduling problem with shift requests. // [START import] -#include +#include + +#include +#include #include +#include +#include #include #include "absl/strings/str_format.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" -#include "ortools/sat/model.h" -#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" // [END import] namespace operations_research { diff --git a/ortools/sat/samples/search_for_all_solutions_sample_sat.cc b/ortools/sat/samples/search_for_all_solutions_sample_sat.cc index 99f3d0a98f..04c612e274 100644 --- a/ortools/sat/samples/search_for_all_solutions_sample_sat.cc +++ b/ortools/sat/samples/search_for_all_solutions_sample_sat.cc @@ -12,9 +12,15 @@ // limitations under the License. // [START program] +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/simple_sat_program.cc b/ortools/sat/samples/simple_sat_program.cc index 51dfcd493a..3c396773d2 100644 --- a/ortools/sat/samples/simple_sat_program.cc +++ b/ortools/sat/samples/simple_sat_program.cc @@ -13,7 +13,13 @@ // [START program] // [START import] +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" +#include "ortools/util/sorted_interval_list.h" // [END import] namespace operations_research { diff --git a/ortools/sat/samples/solution_hinting_sample_sat.cc b/ortools/sat/samples/solution_hinting_sample_sat.cc index c7086dd7d6..854c7a78a4 100644 --- a/ortools/sat/samples/solution_hinting_sample_sat.cc +++ b/ortools/sat/samples/solution_hinting_sample_sat.cc @@ -12,8 +12,14 @@ // limitations under the License. // [START program] +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.cc b/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.cc index eba1e2fde9..4f18a5510a 100644 --- a/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.cc +++ b/ortools/sat/samples/solve_and_print_intermediate_solutions_sample_sat.cc @@ -12,8 +12,14 @@ // limitations under the License. // [START program] +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/solve_with_time_limit_sample_sat.cc b/ortools/sat/samples/solve_with_time_limit_sample_sat.cc index 7805d25650..d944a54f84 100644 --- a/ortools/sat/samples/solve_with_time_limit_sample_sat.cc +++ b/ortools/sat/samples/solve_with_time_limit_sample_sat.cc @@ -12,9 +12,15 @@ // limitations under the License. // [START program] +#include + +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/step_function_sample_sat.cc b/ortools/sat/samples/step_function_sample_sat.cc index 0cd4c90223..6fe913421e 100644 --- a/ortools/sat/samples/step_function_sample_sat.cc +++ b/ortools/sat/samples/step_function_sample_sat.cc @@ -11,9 +11,19 @@ // See the License for the specific language governing permissions and // limitations under the License. +#include + +#include + +#include "absl/types/span.h" +#include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/samples/stop_after_n_solutions_sample_sat.cc b/ortools/sat/samples/stop_after_n_solutions_sample_sat.cc index 8584bf5590..5f0104270e 100644 --- a/ortools/sat/samples/stop_after_n_solutions_sample_sat.cc +++ b/ortools/sat/samples/stop_after_n_solutions_sample_sat.cc @@ -12,11 +12,17 @@ // limitations under the License. // [START program] +#include + #include +#include "ortools/base/logging.h" #include "ortools/sat/cp_model.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_solver.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/sorted_interval_list.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/sat_base.h b/ortools/sat/sat_base.h index f0b6c60775..85c34a9057 100644 --- a/ortools/sat/sat_base.h +++ b/ortools/sat/sat_base.h @@ -25,6 +25,7 @@ #include "absl/base/attributes.h" #include "absl/strings/str_format.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" diff --git a/ortools/sat/sat_decision.cc b/ortools/sat/sat_decision.cc index 7ce21d02a0..0806c4683e 100644 --- a/ortools/sat/sat_decision.cc +++ b/ortools/sat/sat_decision.cc @@ -13,9 +13,22 @@ #include "ortools/sat/sat_decision.h" +#include #include +#include +#include +#include +#include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" +#include "ortools/sat/model.h" +#include "ortools/sat/pb_constraint.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/util.h" +#include "ortools/util/bitset.h" +#include "ortools/util/integer_pq.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/sat_decision.h b/ortools/sat/sat_decision.h index d0d575c327..52f8742c79 100644 --- a/ortools/sat/sat_decision.h +++ b/ortools/sat/sat_decision.h @@ -15,6 +15,7 @@ #define OR_TOOLS_SAT_SAT_DECISION_H_ #include +#include #include #include "ortools/base/integral_types.h" diff --git a/ortools/sat/sat_inprocessing.cc b/ortools/sat/sat_inprocessing.cc index d481f9dd1d..7bba8241b4 100644 --- a/ortools/sat/sat_inprocessing.cc +++ b/ortools/sat/sat_inprocessing.cc @@ -13,15 +13,32 @@ #include "ortools/sat/sat_inprocessing.h" +#include +#include #include +#include #include +#include +#include #include "absl/container/inlined_vector.h" +#include "absl/random/distributions.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" #include "ortools/base/timer.h" +#include "ortools/sat/clause.h" +#include "ortools/sat/drat_checker.h" #include "ortools/sat/probing.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_decision.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/util/bitset.h" +#include "ortools/util/integer_pq.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/sat_inprocessing.h b/ortools/sat/sat_inprocessing.h index 763a9d53b4..eb85caccf2 100644 --- a/ortools/sat/sat_inprocessing.h +++ b/ortools/sat/sat_inprocessing.h @@ -22,15 +22,22 @@ #define OR_TOOLS_SAT_SAT_INPROCESSING_H_ #include +#include +#include +#include "absl/strings/string_view.h" +#include "absl/types/span.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/clause.h" +#include "ortools/sat/drat_checker.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_decision.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/sat_solver.h" #include "ortools/sat/util.h" #include "ortools/util/integer_pq.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { @@ -49,9 +56,9 @@ struct PostsolveClauses { std::deque> clauses; }; -class StampingSimplifier; class BlockedClauseSimplifier; class BoundedVariableElimination; +class StampingSimplifier; struct SatPresolveOptions { // The time budget to spend. diff --git a/ortools/sat/sat_solver.cc b/ortools/sat/sat_solver.cc index 72cc49740e..0f4e0840d2 100644 --- a/ortools/sat/sat_solver.cc +++ b/ortools/sat/sat_solver.cc @@ -16,21 +16,39 @@ #include #include #include +#include +#include #include -#include +#include #include -#include +#include #include +#include "absl/base/attributes.h" +#include "absl/container/flat_hash_map.h" +#include "absl/meta/type_traits.h" +#include "absl/strings/str_cat.h" #include "absl/strings/str_format.h" -#include "ortools/base/integral_types.h" +#include "absl/types/span.h" #include "ortools/base/logging.h" -#include "ortools/base/map_util.h" -#include "ortools/base/stl_util.h" +#include "ortools/base/timer.h" #include "ortools/port/proto_utils.h" #include "ortools/port/sysinfo.h" +#include "ortools/sat/clause.h" +#include "ortools/sat/drat_proof_handler.h" +#include "ortools/sat/model.h" +#include "ortools/sat/pb_constraint.h" +#include "ortools/sat/restart.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_decision.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/sat/util.h" +#include "ortools/util/bitset.h" +#include "ortools/util/logging.h" #include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/stats.h" +#include "ortools/util/strong_integers.h" +#include "ortools/util/time_limit.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/sat_solver.h b/ortools/sat/sat_solver.h index bff1e24bef..86ba1fe442 100644 --- a/ortools/sat/sat_solver.h +++ b/ortools/sat/sat_solver.h @@ -28,6 +28,7 @@ #include #include "absl/container/flat_hash_map.h" +#include "absl/strings/string_view.h" #include "absl/types/span.h" #include "ortools/base/hash.h" #include "ortools/base/integral_types.h" @@ -42,6 +43,7 @@ #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_decision.h" #include "ortools/sat/sat_parameters.pb.h" +#include "ortools/util/bitset.h" #include "ortools/util/logging.h" #include "ortools/util/stats.h" #include "ortools/util/strong_integers.h" diff --git a/ortools/sat/scheduling_constraints.cc b/ortools/sat/scheduling_constraints.cc index 1dd01a12ef..ab7aa38473 100644 --- a/ortools/sat/scheduling_constraints.cc +++ b/ortools/sat/scheduling_constraints.cc @@ -13,8 +13,22 @@ #include "ortools/sat/scheduling_constraints.h" +#include +#include +#include + +#include "absl/types/span.h" +#include "ortools/base/logging.h" +#include "ortools/base/macros.h" #include "ortools/sat/integer.h" +#include "ortools/sat/integer_expr.h" +#include "ortools/sat/intervals.h" +#include "ortools/sat/linear_constraint.h" +#include "ortools/sat/model.h" +#include "ortools/sat/precedences.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/scheduling_constraints.h b/ortools/sat/scheduling_constraints.h index 93bab20f43..0738631663 100644 --- a/ortools/sat/scheduling_constraints.h +++ b/ortools/sat/scheduling_constraints.h @@ -15,6 +15,7 @@ #define OR_TOOLS_SAT_SCHEDULING_CONSTRAINTS_H_ #include +#include #include #include "ortools/base/integral_types.h" diff --git a/ortools/sat/scheduling_cuts.cc b/ortools/sat/scheduling_cuts.cc index fec5cd0471..6ad7f1ff94 100644 --- a/ortools/sat/scheduling_cuts.cc +++ b/ortools/sat/scheduling_cuts.cc @@ -15,10 +15,8 @@ #include #include -#include +#include #include -#include -#include #include #include #include @@ -26,18 +24,20 @@ #include #include "absl/strings/str_cat.h" -#include "ortools/base/integral_types.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" +#include "ortools/sat/cuts.h" #include "ortools/sat/diffn_util.h" #include "ortools/sat/implied_bounds.h" #include "ortools/sat/integer.h" #include "ortools/sat/intervals.h" #include "ortools/sat/linear_constraint.h" #include "ortools/sat/linear_constraint_manager.h" +#include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" -#include "ortools/sat/util.h" -#include "ortools/util/time_limit.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/simplification.cc b/ortools/sat/simplification.cc index 86c19a135e..47a47ba22a 100644 --- a/ortools/sat/simplification.cc +++ b/ortools/sat/simplification.cc @@ -15,21 +15,33 @@ #include #include +#include #include +#include #include #include +#include #include "absl/memory/memory.h" +#include "absl/types/span.h" #include "ortools/algorithms/dynamic_partition.h" #include "ortools/base/adjustable_priority_queue-inl.h" +#include "ortools/base/adjustable_priority_queue.h" #include "ortools/base/logging.h" +#include "ortools/base/macros.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" #include "ortools/base/timer.h" #include "ortools/graph/strongly_connected_components.h" +#include "ortools/sat/drat_proof_handler.h" +#include "ortools/sat/model.h" #include "ortools/sat/probing.h" +#include "ortools/sat/sat_base.h" #include "ortools/sat/sat_inprocessing.h" -#include "ortools/sat/util.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/util/logging.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/simplification.h b/ortools/sat/simplification.h index 0a2f8ef0f0..9688bd2002 100644 --- a/ortools/sat/simplification.h +++ b/ortools/sat/simplification.h @@ -23,6 +23,7 @@ #include #include #include +#include #include #include "absl/types/span.h" diff --git a/ortools/sat/subsolver.cc b/ortools/sat/subsolver.cc index 5b99b3ffc9..6971675f1b 100644 --- a/ortools/sat/subsolver.cc +++ b/ortools/sat/subsolver.cc @@ -14,12 +14,19 @@ #include "ortools/sat/subsolver.h" #include +#include +#include +#include +#include -#include "ortools/base/logging.h" - -#if !defined(__PORTABLE_PLATFORM__) +#include "absl/flags/flag.h" +#include "absl/strings/string_view.h" #include "absl/synchronization/mutex.h" #include "absl/time/clock.h" +#include "absl/time/time.h" +#include "ortools/base/logging.h" +#if !defined(__PORTABLE_PLATFORM__) +#include "ortools/base/threadpool.h" #endif // __PORTABLE_PLATFORM__ namespace operations_research { diff --git a/ortools/sat/subsolver.h b/ortools/sat/subsolver.h index 91406f7156..b0056b8ee8 100644 --- a/ortools/sat/subsolver.h +++ b/ortools/sat/subsolver.h @@ -21,7 +21,9 @@ #include #include #include +#include #include +#include #include #include "ortools/base/integral_types.h" diff --git a/ortools/sat/swig_helper.h b/ortools/sat/swig_helper.h index 3a9161e396..175b262c79 100644 --- a/ortools/sat/swig_helper.h +++ b/ortools/sat/swig_helper.h @@ -16,7 +16,10 @@ #include #include +#include +#include +#include "absl/status/status.h" #include "absl/strings/match.h" #include "ortools/base/file.h" #include "ortools/sat/cp_model.pb.h" @@ -26,6 +29,7 @@ #include "ortools/sat/model.h" #include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/logging.h" +#include "ortools/util/sorted_interval_list.h" #include "ortools/util/time_limit.h" namespace operations_research { diff --git a/ortools/sat/symmetry.cc b/ortools/sat/symmetry.cc index 6ae3d6ec13..94e2ecbc90 100644 --- a/ortools/sat/symmetry.cc +++ b/ortools/sat/symmetry.cc @@ -13,7 +13,15 @@ #include "ortools/sat/symmetry.h" +#include +#include + +#include "absl/types/span.h" +#include "ortools/algorithms/sparse_permutation.h" #include "ortools/base/logging.h" +#include "ortools/base/strong_vector.h" +#include "ortools/sat/sat_base.h" +#include "ortools/util/stats.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/symmetry_util.cc b/ortools/sat/symmetry_util.cc index 29f20755f7..284a5ec2aa 100644 --- a/ortools/sat/symmetry_util.cc +++ b/ortools/sat/symmetry_util.cc @@ -13,9 +13,14 @@ #include "ortools/sat/symmetry_util.h" +#include #include +#include +#include #include "ortools/algorithms/dynamic_partition.h" +#include "ortools/algorithms/sparse_permutation.h" +#include "ortools/base/logging.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/symmetry_util.h b/ortools/sat/symmetry_util.h index 9b79f10e87..7cda764f95 100644 --- a/ortools/sat/symmetry_util.h +++ b/ortools/sat/symmetry_util.h @@ -14,6 +14,9 @@ #ifndef OR_TOOLS_SAT_SYMMETRY_UTIL_H_ #define OR_TOOLS_SAT_SYMMETRY_UTIL_H_ +#include +#include + #include "ortools/algorithms/sparse_permutation.h" namespace operations_research { diff --git a/ortools/sat/synchronization.cc b/ortools/sat/synchronization.cc index 1951355f1d..3b7e597c81 100644 --- a/ortools/sat/synchronization.cc +++ b/ortools/sat/synchronization.cc @@ -13,19 +13,36 @@ #include "ortools/sat/synchronization.h" +#include +#include +#include #include +#include +#include +#include #include +#include +#include +#include +#include +#include "ortools/base/logging.h" +#include "ortools/base/timer.h" #if !defined(__PORTABLE_PLATFORM__) #include "ortools/base/file.h" #endif // __PORTABLE_PLATFORM__ - #include "absl/container/btree_map.h" +#include "absl/container/flat_hash_map.h" #include "absl/container/flat_hash_set.h" -#include "absl/random/random.h" +#include "absl/flags/flag.h" +#include "absl/status/status.h" +#include "absl/strings/str_cat.h" +#include "absl/strings/str_format.h" +#include "absl/strings/string_view.h" +#include "absl/synchronization/mutex.h" +#include "absl/time/clock.h" #include "absl/time/time.h" -#include "ortools/base/integral_types.h" -#include "ortools/base/stl_util.h" +#include "ortools/base/strong_vector.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/cp_model_mapping.h" #include "ortools/sat/cp_model_utils.h" @@ -33,7 +50,13 @@ #include "ortools/sat/linear_programming_constraint.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" +#include "ortools/sat/sat_solver.h" +#include "ortools/sat/util.h" +#include "ortools/util/bitset.h" #include "ortools/util/logging.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" #include "ortools/util/time_limit.h" ABSL_FLAG(bool, cp_model_dump_solutions, false, diff --git a/ortools/sat/synchronization.h b/ortools/sat/synchronization.h index fa4bc8426e..7cdeb2b9fb 100644 --- a/ortools/sat/synchronization.h +++ b/ortools/sat/synchronization.h @@ -16,16 +16,24 @@ #include #include +#include #include +#include #include +#include #include +#include "absl/base/thread_annotations.h" +#include "absl/container/flat_hash_map.h" +#include "absl/container/flat_hash_set.h" #include "absl/random/bit_gen_ref.h" #include "absl/random/random.h" #include "absl/synchronization/mutex.h" +#include "absl/time/time.h" #include "ortools/base/integral_types.h" #include "ortools/base/logging.h" #include "ortools/base/stl_util.h" +#include "ortools/base/timer.h" #include "ortools/sat/cp_model.pb.h" #include "ortools/sat/integer.h" #include "ortools/sat/model.h" diff --git a/ortools/sat/table.cc b/ortools/sat/table.cc index 6d995ca263..871da000a3 100644 --- a/ortools/sat/table.cc +++ b/ortools/sat/table.cc @@ -13,24 +13,15 @@ #include "ortools/sat/table.h" -#include -#include -#include -#include -#include +#include #include +#include #include "absl/container/flat_hash_map.h" -#include "absl/container/flat_hash_set.h" -#include "absl/strings/str_cat.h" -#include "absl/strings/str_join.h" #include "ortools/base/logging.h" -#include "ortools/base/map_util.h" -#include "ortools/base/stl_util.h" +#include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_solver.h" -#include "ortools/sat/util.h" -#include "ortools/util/sorted_interval_list.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/theta_tree.cc b/ortools/sat/theta_tree.cc index a8b669aa1d..87da864fc1 100644 --- a/ortools/sat/theta_tree.cc +++ b/ortools/sat/theta_tree.cc @@ -15,9 +15,9 @@ #include #include -#include -#include "ortools/util/strong_integers.h" +#include "ortools/base/logging.h" +#include "ortools/sat/integer.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/timetable.cc b/ortools/sat/timetable.cc index 5306a52156..dfaeab4c9e 100644 --- a/ortools/sat/timetable.cc +++ b/ortools/sat/timetable.cc @@ -15,11 +15,15 @@ #include #include -#include -#include +#include +#include #include "ortools/base/logging.h" -#include "ortools/util/sort.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/intervals.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" +#include "ortools/util/saturated_arithmetic.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/timetable.h b/ortools/sat/timetable.h index a70c72bfec..d71fbeba6f 100644 --- a/ortools/sat/timetable.h +++ b/ortools/sat/timetable.h @@ -20,7 +20,10 @@ #include "ortools/base/macros.h" #include "ortools/sat/integer.h" #include "ortools/sat/intervals.h" +#include "ortools/sat/model.h" +#include "ortools/sat/sat_base.h" #include "ortools/util/rev.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/timetable_edgefinding.cc b/ortools/sat/timetable_edgefinding.cc index 99ab42fa80..56c5c726b3 100644 --- a/ortools/sat/timetable_edgefinding.cc +++ b/ortools/sat/timetable_edgefinding.cc @@ -15,14 +15,12 @@ #include #include -#include -#include #include -#include "ortools/base/integral_types.h" #include "ortools/base/iterator_adaptors.h" #include "ortools/base/logging.h" -#include "ortools/util/sort.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/intervals.h" #include "ortools/util/strong_integers.h" namespace operations_research { diff --git a/ortools/sat/util.cc b/ortools/sat/util.cc index 51bb9f9cb7..cb6ce8044d 100644 --- a/ortools/sat/util.cc +++ b/ortools/sat/util.cc @@ -16,11 +16,29 @@ #include #include #include +#include +#include +#include +#include +#include +#include +#include +#include "absl/container/flat_hash_map.h" #include "absl/numeric/int128.h" +#include "absl/random/bit_gen_ref.h" +#include "absl/random/distributions.h" +#include "absl/types/span.h" +#include "google/protobuf/descriptor.h" +#include "ortools/base/integral_types.h" +#include "ortools/base/logging.h" +#include "ortools/base/map_util.h" #include "ortools/base/mathutil.h" #include "ortools/base/stl_util.h" +#include "ortools/sat/sat_base.h" +#include "ortools/sat/sat_parameters.pb.h" #include "ortools/util/saturated_arithmetic.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/util.h b/ortools/sat/util.h index c2e4e40c80..bac35062e2 100644 --- a/ortools/sat/util.h +++ b/ortools/sat/util.h @@ -16,9 +16,13 @@ #include #include +#include +#include #include "absl/random/bit_gen_ref.h" #include "absl/random/random.h" +#include "absl/types/span.h" +#include "ortools/base/logging.h" #include "ortools/sat/model.h" #include "ortools/sat/sat_base.h" #include "ortools/sat/sat_parameters.pb.h" diff --git a/ortools/sat/var_domination.cc b/ortools/sat/var_domination.cc index 60e62d53e5..cf59e3fa6b 100644 --- a/ortools/sat/var_domination.cc +++ b/ortools/sat/var_domination.cc @@ -13,11 +13,30 @@ #include "ortools/sat/var_domination.h" -#include -#include +#include +#include +#include +#include +#include +#include +#include +#include + +#include "absl/memory/memory.h" +#include "absl/strings/str_cat.h" +#include "absl/types/span.h" +#include "ortools/algorithms/dynamic_partition.h" +#include "ortools/base/logging.h" #include "ortools/base/stl_util.h" #include "ortools/base/strong_vector.h" +#include "ortools/sat/cp_model.pb.h" +#include "ortools/sat/cp_model_utils.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/presolve_context.h" +#include "ortools/util/affine_relation.h" +#include "ortools/util/sorted_interval_list.h" +#include "ortools/util/strong_integers.h" namespace operations_research { namespace sat { diff --git a/ortools/sat/var_domination.h b/ortools/sat/var_domination.h index d9225615cd..e4e57871e1 100644 --- a/ortools/sat/var_domination.h +++ b/ortools/sat/var_domination.h @@ -15,7 +15,11 @@ #define OR_TOOLS_SAT_VAR_DOMINATION_H_ #include +#include +#include +#include +#include "absl/types/span.h" #include "ortools/algorithms/dynamic_partition.h" #include "ortools/base/strong_vector.h" #include "ortools/sat/cp_model_utils.h" diff --git a/ortools/sat/zero_half_cuts.cc b/ortools/sat/zero_half_cuts.cc index 0f0e9ce530..7296c008c0 100644 --- a/ortools/sat/zero_half_cuts.cc +++ b/ortools/sat/zero_half_cuts.cc @@ -13,6 +13,17 @@ #include "ortools/sat/zero_half_cuts.h" +#include +#include +#include +#include + +#include "ortools/base/logging.h" +#include "ortools/lp_data/lp_types.h" +#include "ortools/sat/integer.h" +#include "ortools/sat/util.h" +#include "ortools/util/strong_integers.h" + namespace operations_research { namespace sat { diff --git a/ortools/sat/zero_half_cuts.h b/ortools/sat/zero_half_cuts.h index be0fc2eb95..0b0af9e1bb 100644 --- a/ortools/sat/zero_half_cuts.h +++ b/ortools/sat/zero_half_cuts.h @@ -14,6 +14,8 @@ #ifndef OR_TOOLS_SAT_ZERO_HALF_CUTS_H_ #define OR_TOOLS_SAT_ZERO_HALF_CUTS_H_ +#include +#include #include #include "ortools/lp_data/lp_types.h"