Skip to content

Commit 1b4d75c

Browse files
MizuxMizux
committed
sat: backport from main
1 parent b0800ae commit 1b4d75c

File tree

108 files changed

+9063
-3844
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

108 files changed

+9063
-3844
lines changed

‎ortools/sat/BUILD.bazel‎

Lines changed: 95 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -279,6 +279,23 @@ cc_test(
279279
],
280280
)
281281

282+
cc_library(
283+
name = "cp_model_solver_logging",
284+
srcs = ["cp_model_solver_logging.cc"],
285+
hdrs = ["cp_model_solver_logging.h"],
286+
deps = [
287+
":model",
288+
":synchronization",
289+
":util",
290+
"//ortools/base:timer",
291+
"//ortools/util:logging",
292+
"@abseil-cpp//absl/container:btree",
293+
"@abseil-cpp//absl/strings",
294+
"@abseil-cpp//absl/strings:str_format",
295+
"@abseil-cpp//absl/strings:string_view",
296+
],
297+
)
298+
282299
cc_proto_library(
283300
name = "cp_model_cc_proto",
284301
visibility = ["//visibility:public"],
@@ -313,6 +330,7 @@ cc_library(
313330
":cp_model_cc_proto",
314331
":drat_proof_handler",
315332
":sat_base",
333+
"//ortools/base:base_export",
316334
"//ortools/base:file",
317335
"//ortools/base:hash",
318336
"//ortools/base:stl_util",
@@ -322,6 +340,7 @@ cc_library(
322340
"@abseil-cpp//absl/container:flat_hash_map",
323341
"@abseil-cpp//absl/container:flat_hash_set",
324342
"@abseil-cpp//absl/flags:flag",
343+
"@abseil-cpp//absl/functional:function_ref",
325344
"@abseil-cpp//absl/log:check",
326345
"@abseil-cpp//absl/status",
327346
"@abseil-cpp//absl/strings",
@@ -662,6 +681,7 @@ cc_library(
662681
":cp_model_postsolve",
663682
":cp_model_presolve",
664683
":cp_model_search",
684+
":cp_model_solver_logging",
665685
":cp_model_symmetries",
666686
":cp_model_utils",
667687
":cuts",
@@ -671,6 +691,7 @@ cc_library(
671691
":integer",
672692
":integer_base",
673693
":integer_expr",
694+
":integer_resolution",
674695
":integer_search",
675696
":intervals",
676697
":lb_tree_search",
@@ -790,6 +811,7 @@ cc_library(
790811
":cp_model_presolve",
791812
":cp_model_search",
792813
":cp_model_solver_helpers",
814+
":cp_model_solver_logging",
793815
":cp_model_symmetries",
794816
":cp_model_utils",
795817
":cuts",
@@ -810,6 +832,8 @@ cc_library(
810832
":linear_programming_constraint",
811833
":linear_relaxation",
812834
":lp_utils",
835+
":lrat_checker",
836+
":lrat_proof_handler",
813837
":max_hs",
814838
":model",
815839
":optimization",
@@ -832,6 +856,7 @@ cc_library(
832856
":util",
833857
":work_assignment",
834858
"//ortools/base",
859+
"//ortools/base:base_export",
835860
"//ortools/base:file",
836861
"//ortools/base:status_macros",
837862
"//ortools/base:strong_vector",
@@ -1071,6 +1096,7 @@ cc_library(
10711096
":sat_solver",
10721097
":solution_crush",
10731098
":util",
1099+
"//ortools/base:base_export",
10741100
"//ortools/base:logging",
10751101
"//ortools/port:proto_utils",
10761102
"//ortools/util:affine_relation",
@@ -1127,6 +1153,7 @@ cc_library(
11271153
":util",
11281154
"//ortools/algorithms:sparse_permutation",
11291155
"//ortools/util:sorted_interval_list",
1156+
"@abseil-cpp//absl/algorithm:container",
11301157
"@abseil-cpp//absl/container:flat_hash_map",
11311158
"@abseil-cpp//absl/container:flat_hash_set",
11321159
"@abseil-cpp//absl/container:inlined_vector",
@@ -1341,7 +1368,6 @@ cc_library(
13411368
":presolve_context",
13421369
":sat_parameters_cc_proto",
13431370
":solution_crush",
1344-
":util",
13451371
"//ortools/base:logging",
13461372
"//ortools/base:stl_util",
13471373
"//ortools/port:proto_utils",
@@ -1362,6 +1388,7 @@ cc_library(
13621388
cc_test(
13631389
name = "cp_model_expand_test",
13641390
size = "small",
1391+
timeout = "moderate",
13651392
srcs = ["cp_model_expand_test.cc"],
13661393
deps = [
13671394
":cp_model_cc_proto",
@@ -1388,6 +1415,7 @@ cc_library(
13881415
hdrs = ["sat_base.h"],
13891416
deps = [
13901417
"//ortools/base",
1418+
"//ortools/base:intops",
13911419
"//ortools/base:strong_vector",
13921420
"//ortools/util:bitset",
13931421
"//ortools/util:strong_integers",
@@ -1423,6 +1451,7 @@ cc_library(
14231451
":clause",
14241452
":drat_proof_handler",
14251453
":enforcement",
1454+
":lrat_proof_handler",
14261455
":model",
14271456
":pb_constraint",
14281457
":restart",
@@ -1445,10 +1474,10 @@ cc_library(
14451474
"@abseil-cpp//absl/base:core_headers",
14461475
"@abseil-cpp//absl/container:btree",
14471476
"@abseil-cpp//absl/container:flat_hash_map",
1477+
"@abseil-cpp//absl/container:flat_hash_set",
14481478
"@abseil-cpp//absl/log",
14491479
"@abseil-cpp//absl/log:check",
14501480
"@abseil-cpp//absl/log:vlog_is_on",
1451-
"@abseil-cpp//absl/meta:type_traits",
14521481
"@abseil-cpp//absl/strings",
14531482
"@abseil-cpp//absl/strings:str_format",
14541483
"@abseil-cpp//absl/types:span",
@@ -1509,7 +1538,6 @@ cc_library(
15091538
"//ortools/util:strong_integers",
15101539
"//ortools/util:time_limit",
15111540
"@abseil-cpp//absl/container:btree",
1512-
"@abseil-cpp//absl/container:inlined_vector",
15131541
"@abseil-cpp//absl/log",
15141542
"@abseil-cpp//absl/log:check",
15151543
"@abseil-cpp//absl/log:vlog_is_on",
@@ -1543,25 +1571,32 @@ cc_library(
15431571
":clause",
15441572
":drat_checker",
15451573
":linear_programming_constraint",
1574+
":lrat_proof_handler",
15461575
":model",
15471576
":probing",
15481577
":sat_base",
15491578
":sat_decision",
15501579
":sat_parameters_cc_proto",
15511580
":sat_solver",
1581+
":synchronization",
15521582
":util",
15531583
"//ortools/base",
15541584
"//ortools/base:stl_util",
15551585
"//ortools/base:strong_vector",
15561586
"//ortools/base:timer",
1587+
"//ortools/graph:connected_components",
15571588
"//ortools/util:bitset",
15581589
"//ortools/util:integer_pq",
15591590
"//ortools/util:logging",
15601591
"//ortools/util:strong_integers",
15611592
"//ortools/util:time_limit",
15621593
"@abseil-cpp//absl/algorithm:container",
15631594
"@abseil-cpp//absl/cleanup",
1595+
"@abseil-cpp//absl/container:flat_hash_map",
1596+
"@abseil-cpp//absl/container:flat_hash_set",
15641597
"@abseil-cpp//absl/container:inlined_vector",
1598+
"@abseil-cpp//absl/functional:function_ref",
1599+
"@abseil-cpp//absl/hash",
15651600
"@abseil-cpp//absl/log",
15661601
"@abseil-cpp//absl/log:check",
15671602
"@abseil-cpp//absl/log:vlog_is_on",
@@ -1630,11 +1665,13 @@ cc_library(
16301665
":container",
16311666
":drat_proof_handler",
16321667
":inclusion",
1668+
":lrat_proof_handler",
16331669
":model",
16341670
":sat_base",
16351671
":sat_parameters_cc_proto",
16361672
":util",
16371673
"//ortools/base",
1674+
"//ortools/base:intops",
16381675
"//ortools/base:stl_util",
16391676
"//ortools/base:strong_vector",
16401677
"//ortools/base:timer",
@@ -1653,7 +1690,6 @@ cc_library(
16531690
"@abseil-cpp//absl/log",
16541691
"@abseil-cpp//absl/log:check",
16551692
"@abseil-cpp//absl/log:vlog_is_on",
1656-
"@abseil-cpp//absl/random:bit_gen_ref",
16571693
"@abseil-cpp//absl/random:distributions",
16581694
"@abseil-cpp//absl/types:span",
16591695
],
@@ -1877,7 +1913,10 @@ cc_test(
18771913
deps = [
18781914
":integer_base",
18791915
"//ortools/base:gmock_main",
1916+
"@abseil-cpp//absl/log",
18801917
"@abseil-cpp//absl/log:check",
1918+
"@abseil-cpp//absl/random",
1919+
"@abseil-cpp//absl/random:distributions",
18811920
],
18821921
)
18831922

@@ -1906,7 +1945,27 @@ cc_library(
19061945
"@abseil-cpp//absl/container:flat_hash_map",
19071946
"@abseil-cpp//absl/container:inlined_vector",
19081947
"@abseil-cpp//absl/log:check",
1909-
"@abseil-cpp//absl/meta:type_traits",
1948+
"@abseil-cpp//absl/strings",
1949+
"@abseil-cpp//absl/types:span",
1950+
],
1951+
)
1952+
1953+
cc_library(
1954+
name = "integer_resolution",
1955+
srcs = ["integer_resolution.cc"],
1956+
hdrs = ["integer_resolution.h"],
1957+
deps = [
1958+
":clause",
1959+
":integer",
1960+
":integer_base",
1961+
":model",
1962+
":sat_base",
1963+
":sat_solver",
1964+
":synchronization",
1965+
"//ortools/base:strong_vector",
1966+
"//ortools/util:bitset",
1967+
"@abseil-cpp//absl/log",
1968+
"@abseil-cpp//absl/log:check",
19101969
"@abseil-cpp//absl/strings",
19111970
"@abseil-cpp//absl/types:span",
19121971
],
@@ -2113,6 +2172,7 @@ cc_library(
21132172
":precedences",
21142173
":sat_base",
21152174
":sat_solver",
2175+
":util",
21162176
"//ortools/base:logging",
21172177
"//ortools/util:bitset",
21182178
"//ortools/util:sort",
@@ -2172,6 +2232,7 @@ cc_library(
21722232
":clause",
21732233
":cp_constraints",
21742234
":cp_model_mapping",
2235+
":implied_bounds",
21752236
":integer",
21762237
":integer_base",
21772238
":model",
@@ -2187,6 +2248,7 @@ cc_library(
21872248
"//ortools/util:rev",
21882249
"//ortools/util:strong_integers",
21892250
"//ortools/util:time_limit",
2251+
"@abseil-cpp//absl/algorithm:container",
21902252
"@abseil-cpp//absl/container:btree",
21912253
"@abseil-cpp//absl/container:flat_hash_map",
21922254
"@abseil-cpp//absl/container:flat_hash_set",
@@ -2206,6 +2268,7 @@ cc_test(
22062268
deps = [
22072269
":cp_model_mapping",
22082270
":cp_model_solver_helpers",
2271+
":implied_bounds",
22092272
":integer",
22102273
":integer_base",
22112274
":integer_search",
@@ -2249,7 +2312,6 @@ cc_library(
22492312
hdrs = ["integer_expr.h"],
22502313
visibility = ["//visibility:public"],
22512314
deps = [
2252-
":cp_constraints",
22532315
":enforcement",
22542316
":enforcement_helper",
22552317
":integer",
@@ -2456,6 +2518,7 @@ cc_test(
24562518
":precedences",
24572519
":sat_base",
24582520
":sat_solver",
2521+
":util",
24592522
"//ortools/base",
24602523
"//ortools/base:gmock_main",
24612524
"//ortools/util:strong_integers",
@@ -2819,6 +2882,7 @@ cc_library(
28192882
"//ortools/util:strong_integers",
28202883
"//ortools/util:time_limit",
28212884
"@abseil-cpp//absl/algorithm:container",
2885+
"@abseil-cpp//absl/cleanup",
28222886
"@abseil-cpp//absl/container:flat_hash_map",
28232887
"@abseil-cpp//absl/log",
28242888
"@abseil-cpp//absl/log:check",
@@ -2983,6 +3047,7 @@ cc_library(
29833047
":cp_model_cc_proto",
29843048
":cp_model_utils",
29853049
":cuts",
3050+
":implied_bounds",
29863051
":integer",
29873052
":integer_base",
29883053
":linear_constraint",
@@ -3025,6 +3090,7 @@ cc_test(
30253090
":clause",
30263091
":cp_model",
30273092
":cuts",
3093+
":implied_bounds",
30283094
":integer",
30293095
":integer_base",
30303096
":linear_constraint",
@@ -3037,6 +3103,7 @@ cc_test(
30373103
"//ortools/base:parse_test_proto",
30383104
"//ortools/base:strong_vector",
30393105
"//ortools/graph:max_flow",
3106+
"//ortools/util:sorted_interval_list",
30403107
"//ortools/util:strong_integers",
30413108
"@abseil-cpp//absl/container:flat_hash_map",
30423109
"@abseil-cpp//absl/log",
@@ -3069,6 +3136,7 @@ cc_library(
30693136
"//ortools/util:sorted_interval_list",
30703137
"//ortools/util:strong_integers",
30713138
"//ortools/util:time_limit",
3139+
"@abseil-cpp//absl/algorithm:container",
30723140
"@abseil-cpp//absl/base:core_headers",
30733141
"@abseil-cpp//absl/container:btree",
30743142
"@abseil-cpp//absl/container:flat_hash_map",
@@ -3096,11 +3164,11 @@ cc_test(
30963164
":scheduling_cuts",
30973165
":scheduling_helpers",
30983166
"//ortools/base:gmock_main",
3167+
"//ortools/base:stl_util",
30993168
"//ortools/base:strong_vector",
31003169
"//ortools/util:strong_integers",
31013170
"@abseil-cpp//absl/base:log_severity",
31023171
"@abseil-cpp//absl/random",
3103-
"@abseil-cpp//absl/strings",
31043172
"@abseil-cpp//absl/types:span",
31053173
],
31063174
)
@@ -3901,6 +3969,7 @@ cc_library(
39013969
hdrs = ["cp_model_lns.h"],
39023970
visibility = ["//visibility:public"],
39033971
deps = [
3972+
":clause",
39043973
":cp_model_cc_proto",
39053974
":cp_model_copy",
39063975
":cp_model_mapping",
@@ -4171,12 +4240,29 @@ cc_library(
41714240
srcs = ["lrat_checker.cc"],
41724241
hdrs = ["lrat_checker.h"],
41734242
deps = [
4243+
":model",
41744244
":sat_base",
4245+
":synchronization",
41754246
":util",
4176-
"//ortools/base:intops",
41774247
"@abseil-cpp//absl/algorithm:container",
41784248
"@abseil-cpp//absl/container:flat_hash_map",
41794249
"@abseil-cpp//absl/container:flat_hash_set",
4250+
"@abseil-cpp//absl/log",
4251+
"@abseil-cpp//absl/log:check",
4252+
"@abseil-cpp//absl/strings",
4253+
"@abseil-cpp//absl/types:span",
4254+
],
4255+
)
4256+
4257+
cc_library(
4258+
name = "lrat_proof_handler",
4259+
srcs = ["lrat_proof_handler.cc"],
4260+
hdrs = ["lrat_proof_handler.h"],
4261+
deps = [
4262+
":lrat_checker",
4263+
":model",
4264+
":sat_base",
4265+
"@abseil-cpp//absl/log",
41804266
"@abseil-cpp//absl/log:check",
41814267
"@abseil-cpp//absl/strings",
41824268
"@abseil-cpp//absl/types:span",
@@ -4188,6 +4274,7 @@ cc_test(
41884274
srcs = ["lrat_checker_test.cc"],
41894275
deps = [
41904276
":lrat_checker",
4277+
":model",
41914278
":sat_base",
41924279
"//ortools/base:gmock_main",
41934280
"@abseil-cpp//absl/types:span",

0 commit comments

Comments
 (0)