Learn how easy it is to sync an existing GitHub or Google Code repo to a SourceForge project! See Demo

Close

[r1813]: trunk / Toss / Formula / BoolFormula.ml Maximize Restore History

Download this file

BoolFormula.ml    1451 lines (1345 with data), 59.2 kB

   1
   2
   3
   4
   5
   6
   7
   8
   9
  10
  11
  12
  13
  14
  15
  16
  17
  18
  19
  20
  21
  22
  23
  24
  25
  26
  27
  28
  29
  30
  31
  32
  33
  34
  35
  36
  37
  38
  39
  40
  41
  42
  43
  44
  45
  46
  47
  48
  49
  50
  51
  52
  53
  54
  55
  56
  57
  58
  59
  60
  61
  62
  63
  64
  65
  66
  67
  68
  69
  70
  71
  72
  73
  74
  75
  76
  77
  78
  79
  80
  81
  82
  83
  84
  85
  86
  87
  88
  89
  90
  91
  92
  93
  94
  95
  96
  97
  98
  99
 100
 101
 102
 103
 104
 105
 106
 107
 108
 109
 110
 111
 112
 113
 114
 115
 116
 117
 118
 119
 120
 121
 122
 123
 124
 125
 126
 127
 128
 129
 130
 131
 132
 133
 134
 135
 136
 137
 138
 139
 140
 141
 142
 143
 144
 145
 146
 147
 148
 149
 150
 151
 152
 153
 154
 155
 156
 157
 158
 159
 160
 161
 162
 163
 164
 165
 166
 167
 168
 169
 170
 171
 172
 173
 174
 175
 176
 177
 178
 179
 180
 181
 182
 183
 184
 185
 186
 187
 188
 189
 190
 191
 192
 193
 194
 195
 196
 197
 198
 199
 200
 201
 202
 203
 204
 205
 206
 207
 208
 209
 210
 211
 212
 213
 214
 215
 216
 217
 218
 219
 220
 221
 222
 223
 224
 225
 226
 227
 228
 229
 230
 231
 232
 233
 234
 235
 236
 237
 238
 239
 240
 241
 242
 243
 244
 245
 246
 247
 248
 249
 250
 251
 252
 253
 254
 255
 256
 257
 258
 259
 260
 261
 262
 263
 264
 265
 266
 267
 268
 269
 270
 271
 272
 273
 274
 275
 276
 277
 278
 279
 280
 281
 282
 283
 284
 285
 286
 287
 288
 289
 290
 291
 292
 293
 294
 295
 296
 297
 298
 299
 300
 301
 302
 303
 304
 305
 306
 307
 308
 309
 310
 311
 312
 313
 314
 315
 316
 317
 318
 319
 320
 321
 322
 323
 324
 325
 326
 327
 328
 329
 330
 331
 332
 333
 334
 335
 336
 337
 338
 339
 340
 341
 342
 343
 344
 345
 346
 347
 348
 349
 350
 351
 352
 353
 354
 355
 356
 357
 358
 359
 360
 361
 362
 363
 364
 365
 366
 367
 368
 369
 370
 371
 372
 373
 374
 375
 376
 377
 378
 379
 380
 381
 382
 383
 384
 385
 386
 387
 388
 389
 390
 391
 392
 393
 394
 395
 396
 397
 398
 399
 400
 401
 402
 403
 404
 405
 406
 407
 408
 409
 410
 411
 412
 413
 414
 415
 416
 417
 418
 419
 420
 421
 422
 423
 424
 425
 426
 427
 428
 429
 430
 431
 432
 433
 434
 435
 436
 437
 438
 439
 440
 441
 442
 443
 444
 445
 446
 447
 448
 449
 450
 451
 452
 453
 454
 455
 456
 457
 458
 459
 460
 461
 462
 463
 464
 465
 466
 467
 468
 469
 470
 471
 472
 473
 474
 475
 476
 477
 478
 479
 480
 481
 482
 483
 484
 485
 486
 487
 488
 489
 490
 491
 492
 493
 494
 495
 496
 497
 498
 499
 500
 501
 502
 503
 504
 505
 506
 507
 508
 509
 510
 511
 512
 513
 514
 515
 516
 517
 518
 519
 520
 521
 522
 523
 524
 525
 526
 527
 528
 529
 530
 531
 532
 533
 534
 535
 536
 537
 538
 539
 540
 541
 542
 543
 544
 545
 546
 547
 548
 549
 550
 551
 552
 553
 554
 555
 556
 557
 558
 559
 560
 561
 562
 563
 564
 565
 566
 567
 568
 569
 570
 571
 572
 573
 574
 575
 576
 577
 578
 579
 580
 581
 582
 583
 584
 585
 586
 587
 588
 589
 590
 591
 592
 593
 594
 595
 596
 597
 598
 599
 600
 601
 602
 603
 604
 605
 606
 607
 608
 609
 610
 611
 612
 613
 614
 615
 616
 617
 618
 619
 620
 621
 622
 623
 624
 625
 626
 627
 628
 629
 630
 631
 632
 633
 634
 635
 636
 637
 638
 639
 640
 641
 642
 643
 644
 645
 646
 647
 648
 649
 650
 651
 652
 653
 654
 655
 656
 657
 658
 659
 660
 661
 662
 663
 664
 665
 666
 667
 668
 669
 670
 671
 672
 673
 674
 675
 676
 677
 678
 679
 680
 681
 682
 683
 684
 685
 686
 687
 688
 689
 690
 691
 692
 693
 694
 695
 696
 697
 698
 699
 700
 701
 702
 703
 704
 705
 706
 707
 708
 709
 710
 711
 712
 713
 714
 715
 716
 717
 718
 719
 720
 721
 722
 723
 724
 725
 726
 727
 728
 729
 730
 731
 732
 733
 734
 735
 736
 737
 738
 739
 740
 741
 742
 743
 744
 745
 746
 747
 748
 749
 750
 751
 752
 753
 754
 755
 756
 757
 758
 759
 760
 761
 762
 763
 764
 765
 766
 767
 768
 769
 770
 771
 772
 773
 774
 775
 776
 777
 778
 779
 780
 781
 782
 783
 784
 785
 786
 787
 788
 789
 790
 791
 792
 793
 794
 795
 796
 797
 798
 799
 800
 801
 802
 803
 804
 805
 806
 807
 808
 809
 810
 811
 812
 813
 814
 815
 816
 817
 818
 819
 820
 821
 822
 823
 824
 825
 826
 827
 828
 829
 830
 831
 832
 833
 834
 835
 836
 837
 838
 839
 840
 841
 842
 843
 844
 845
 846
 847
 848
 849
 850
 851
 852
 853
 854
 855
 856
 857
 858
 859
 860
 861
 862
 863
 864
 865
 866
 867
 868
 869
 870
 871
 872
 873
 874
 875
 876
 877
 878
 879
 880
 881
 882
 883
 884
 885
 886
 887
 888
 889
 890
 891
 892
 893
 894
 895
 896
 897
 898
 899
 900
 901
 902
 903
 904
 905
 906
 907
 908
 909
 910
 911
 912
 913
 914
 915
 916
 917
 918
 919
 920
 921
 922
 923
 924
 925
 926
 927
 928
 929
 930
 931
 932
 933
 934
 935
 936
 937
 938
 939
 940
 941
 942
 943
 944
 945
 946
 947
 948
 949
 950
 951
 952
 953
 954
 955
 956
 957
 958
 959
 960
 961
 962
 963
 964
 965
 966
 967
 968
 969
 970
 971
 972
 973
 974
 975
 976
 977
 978
 979
 980
 981
 982
 983
 984
 985
 986
 987
 988
 989
 990
 991
 992
 993
 994
 995
 996
 997
 998
 999
1000
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
(* Represent Boolean combinations of integer literals. *)
(* 0 : no generation is performed and to_cnf transforms a DNF
1 : use Tseitin to construct a NF with auxiliary variables
2 : use Plaisted-Greenbaum to construct a CNF with auxiliary variables *)
let auxcnf_generation = ref 2
let set_auxcnf i = (auxcnf_generation := i)
let simplification = ref 2
let set_simplification i = (simplification := i)
(* bit 0 : subsumption test after cnf conversion
bit 1 : full-fledged simplification
bit 2 : resolution during simplification *)
exception FormulaError of string
(* ----------------------- BASIC TYPE DEFINITIONS -------------------------- *)
(* This type describes formulas of relational logic with equality.
We allow only simple boolean junctors, other are resolved during parsing. *)
type bool_formula =
| BVar of int
| BNot of bool_formula
| BAnd of bool_formula list
| BOr of bool_formula list
(* ----------------------- BASIC TYPE CONVERSIONS -------------------------- *)
let int_of_lit lit =
match lit with BVar v -> v | _ -> failwith ("This is not a literal!")
let lit_of_int v = BVar v
(* ----------------------- PRINTING FUNCTIONS ------------------------------- *)
(** Print a variable as a string. *)
let var_str = string_of_int
(** Print a Boolean formula as a string. *)
let rec str ?names bf =
let name s = match names with None -> var_str s | Some tbl ->
try Hashtbl.find tbl s with Not_found -> var_str s in
let rec str_rec = function
| BVar v -> if v < 0 then "-" ^ (name (-v)) else name v
| BNot phi -> "(not " ^ (str_rec phi) ^ ")"
| BAnd [] -> "true"
| BOr [] -> "false"
| BAnd (bflist) -> bf_list_str " and " bflist
| BOr (bflist) -> bf_list_str " or " bflist
and bf_list_str sep = function
| [] -> "[]"
| [phi] -> str_rec phi
| lst -> "(" ^ (String.concat sep (List.map str_rec lst)) ^ ")" in
str_rec bf
(* ------------------------ ORDER ON FORMULAS ------------------------------- *)
(** Compare two variables. We assume that FO < MSO < Real. *)
let compare_vars x y =
let abs lit = if lit < 0 then (-lit) else lit in
(abs x) - (abs y)
(* Helper function: compare lists lexicographically by [cmp]. *)
let rec compare_lists_lex cmp = function
| ([], []) -> 0
| ([], _) -> -1
| (_, []) -> 1
| (x :: xs, y :: ys) ->
let c = cmp x y in
if c <> 0 then c else compare_lists_lex cmp (xs, ys)
let rec compare_var_lists l1 l2 =
if l1 = l2 then 0 else
compare_lists_lex compare_vars (l1, l2)
let rec size ?(acc=0) = function
| BVar _ -> acc + 1
| BNot phi -> size ~acc:(acc + 1) phi
| BAnd flist | BOr flist ->
List.fold_left (fun i f -> size ~acc:i f) (acc + 1) flist
let rec rec_compare phi1 phi2 =
let cmp_lists = compare_lists_lex rec_compare in
match (phi1, phi2) with
| (BVar v1, BVar v2) -> compare_vars v1 v2
| (BVar _, _) -> -1
| (_, BVar _) -> 1
| (BNot psi1, BNot psi2) -> rec_compare psi1 psi2
| (BNot _, _) -> -1
| (_, BNot _) -> 1
| (BAnd fl1, BAnd fl2)
| (BOr fl1, BOr fl2) -> cmp_lists (fl1, fl2)
| (BAnd _, _) -> -1
| (_, BAnd _) -> 1
let compare phi1 phi2 =
if phi1 == phi2 then 0 else
let (s1, s2) = (size phi1, size phi2) in
if s1 <> s2 then s1 - s2 else rec_compare phi1 phi2
let rec sort phi =
match phi with
| BVar _ -> phi
| BNot psi -> BNot (sort psi)
| BOr psis -> BOr (List.sort compare (List.map sort psis))
| BAnd psis -> BAnd (List.sort compare (List.map sort psis))
let rec subst vars = function
| BVar v when (List.mem v vars) -> BAnd []
| BVar v when (List.mem (-v) vars) -> BOr []
| BVar v -> BVar v
| BNot f -> subst vars f
| BOr fs -> BOr (List.map (subst vars) fs)
| BAnd fs -> BAnd (List.map (subst vars) fs)
(* Convert a Boolean combination into reduced form (over 'not' and 'or') *)
let rec to_reduced_form ?(neg=false) = function
| BVar v -> if neg then BVar (-1 * v) else BVar v
| BNot phi ->
if neg then to_reduced_form ~neg:false phi else
to_reduced_form ~neg:true phi
| BAnd [f] | BOr [f] -> to_reduced_form ~neg f
| BOr (bflist) when neg ->
BNot (BOr (List.rev_map (to_reduced_form ~neg:false) bflist))
| BOr (bflist) -> BOr (List.rev_map (to_reduced_form ~neg:false) bflist)
| BAnd (bflist) when neg ->
BOr (List.rev_map (to_reduced_form ~neg:true) bflist)
| BAnd (bflist) ->
BNot (BOr (List.rev_map (to_reduced_form ~neg:true) bflist))
(* Convert a Boolean formula to NNF and additionally negate if [neg] is set. *)
let rec to_nnf ?(neg=false) = function
| BVar v -> if neg then BVar (-1 * v) else BVar v
| BNot phi -> if neg then to_nnf ~neg:false phi else to_nnf ~neg:true phi
| BAnd (flist) when neg ->
BOr (List.rev (List.rev_map (to_nnf ~neg:true) flist))
| BAnd (flist) -> BAnd (List.rev (List.rev_map (to_nnf ~neg:false) flist))
| BOr (flist) when neg ->
BAnd (List.rev (List.rev_map (to_nnf ~neg:true) flist))
| BOr (flist) -> BOr (List.rev (List.rev_map (to_nnf ~neg:false) flist))
(* Helper function to flatten multiple or's and and's and sort by compare. *)
let rec flatten_sort = function
| BVar _ as phi -> phi
| BNot (BAnd []) -> BOr[]
| BNot (BOr []) -> BAnd[]
| BNot phi -> BNot (flatten_sort phi)
| BOr flist_orig ->
let flist = List.map flatten_sort flist_orig in
let is_or = function BOr _ -> true | _ -> false in
let (ors_all, non_ors) = List.partition is_or flist in
let ors = List.filter (fun v -> v <> BOr []) ors_all in
let flat_non_ors = List.rev_map flatten_sort non_ors in
if List.exists (fun v -> v = BAnd []) flat_non_ors then BAnd [] else
if ors = [] then BOr (List.sort compare flat_non_ors) else
let fl = flatten_sort_ors [] ors in
BOr (List.sort compare (List.rev_append fl flat_non_ors))
| BAnd flist_orig ->
let flist = List.map flatten_sort flist_orig in
let is_and = function BAnd _ -> true | _ -> false in
let (ands_all, non_ands) = List.partition is_and flist in
let ands = List.filter (fun v -> v <> BAnd []) ands_all in
let flat_non_ands = List.rev_map flatten_sort non_ands in
if List.exists (fun v -> v = BOr []) flat_non_ands then BOr [] else
if ands = [] then BAnd (List.sort compare flat_non_ands) else
let fl = flatten_sort_ands [] ands in
BAnd (List.sort compare (List.rev_append fl flat_non_ands))
and flatten_sort_ors acc = function
| [] -> acc
| (BOr fl) :: ls ->
let handle accu phi =
match flatten_sort phi with
| BOr fl -> List.rev_append fl accu
| _ -> phi::accu in
let new_acc = List.fold_left handle acc fl in
flatten_sort_ors new_acc ls
| _ -> failwith "flatten_sort_ors on a non-or"
and flatten_sort_ands acc = function
| [] -> acc
| (BAnd fl) :: ls ->
let handle accu phi =
match flatten_sort phi with
| BAnd fl -> List.rev_append fl accu
| _ -> phi::accu in
let new_acc = List.fold_left handle acc fl in
flatten_sort_ands new_acc ls
| _ -> failwith "flatten_sort_ands on a non-and"
(* Convert an arbitrary formula to a Boolean combination of literals *)
let bool_formula_of_formula_arg phi (ids, rev_ids, free_id) =
let rec get_id ?(pos=true) = function
| Formula.Not (phi) -> get_id ~pos:(not pos) phi
(* TODO: we could check also: all x not R(x) = not ex x R(x)!*)
| phi ->
try
let id = Hashtbl.find ids phi in if pos then id else -1 * id
with Not_found ->
LOG 3 "Added %s as %i" (Formula.str phi) !free_id;
Hashtbl.add ids phi (!free_id);
Hashtbl.add rev_ids (!free_id) phi;
Hashtbl.add rev_ids (-1 * !free_id) (Formula.Not phi);
free_id := !free_id + 1;
if pos then !free_id - 1 else -1 * (!free_id - 1) in
let rec bool_formula ?(pos=true) = function
| Formula.Not (phi) when pos -> bool_formula ~pos:false phi
| Formula.Not (phi) -> bool_formula ~pos:true phi
| Formula.And (flist) when pos ->
BAnd (List.rev_map (bool_formula ~pos:true) flist)
| Formula.And (flist) ->
BNot (BAnd (List.rev_map (bool_formula ~pos:true) flist))
| Formula.Or (flist) when pos ->
BOr (List.rev_map (bool_formula ~pos:true) flist)
| Formula.Or (flist) ->
BNot (BOr (List.rev_map (bool_formula ~pos:true) flist))
| phi -> BVar (get_id ~pos:pos phi) in
bool_formula phi
let bool_formula_of_formula phi =
let (ids, rev_ids, free_id) = (Hashtbl.create 7, Hashtbl.create 7, ref 1) in
bool_formula_of_formula_arg phi (ids, rev_ids, free_id)
(* Convert a Boolean combination back to a formula *)
let formula_of_bool_formula_arg phi (ids, rev_ids, free_id) =
let rec formula ?(pos=true) = function
| BNot (phi) when pos -> formula ~pos:false phi
| BNot (phi) -> formula ~pos:true phi
| BAnd (flist) when pos ->
Formula.And (List.rev_map (formula ~pos:true) flist)
| BAnd (flist) ->
Formula.Not (Formula.And (List.rev_map (formula ~pos:true) flist))
| BOr (flist) when pos ->
Formula.Or (List.rev_map (formula ~pos:true) flist)
| BOr (flist) ->
Formula.Not (Formula.Or (List.rev_map (formula ~pos:true) flist))
| BVar id -> try (Hashtbl.find rev_ids id) with
Not_found ->
failwith ("Boolean combination contains a non-hashed literal!") in
formula phi
(* Flatten conjunctions and disjunctions. *)
let rec flatten phi =
let get_conjunctions = function BAnd fl -> fl | f -> [f] in
let get_disjunctions = function BOr fl -> fl | f -> [f] in
let fold_acc f xl =
List.fold_left (fun acc x -> List.rev_append (List.rev (f x)) acc) [] xl in
let rev_collect_conj xl = fold_acc get_conjunctions xl in
let rev_collect_disj xl = fold_acc get_disjunctions xl in
match phi with
| BNot (BNot psi) -> flatten psi
| BNot (BVar v) -> BVar (-v)
| BNot psi -> BNot (flatten psi)
| BOr (flist) ->
let res = rev_collect_disj (List.rev_map flatten flist) in
if List.mem (BAnd []) res then BAnd [] else BOr (res)
| BAnd (flist) ->
let res = rev_collect_conj (List.rev_map flatten flist) in
if List.mem (BOr []) res then BOr [] else BAnd (res)
| _ -> phi
(* Absorb trues and falses *)
let rec neutral_absorbing = function
| BVar _ as lit -> lit
| BNot psi -> BNot (neutral_absorbing psi)
| BOr psis ->
if (List.exists (fun psi -> psi = BAnd []) psis) then (BAnd []) else
let filtered_once = List.filter (fun psi -> psi <> BOr []) psis in
let new_psis = List.map neutral_absorbing filtered_once in
let filtered = List.filter (fun psi -> psi <> BOr []) new_psis in
if (List.exists (fun psi -> psi = BAnd []) filtered) then (BAnd []) else
BOr filtered
| BAnd psis ->
if (List.exists (fun psi -> psi = BOr []) psis) then (BOr []) else
let filtered_once = List.filter (fun psi -> psi <> BAnd []) psis in
let new_psis = List.map neutral_absorbing filtered_once in
let filtered = List.filter (fun psi -> psi <> BAnd []) new_psis in
if (List.exists (fun psi -> psi = BOr []) filtered) then (BOr []) else
BAnd filtered
(* Simplify a Boolean combination *)
let rec simplify phi =
let is_conjunction = function BAnd _ -> true | _ -> false in
let is_disjunction = function BOr _ -> true | _ -> false in
let is_literal = function BNot (BVar _) | BVar _ -> true | _ -> false in
let invcmp x y =
let c = compare x y in if c <> 0 then -c else Pervasives.compare x y in
let rec singularise phi =
let rec neg_occurrence = function
(* check whether a _sorted_ uniqued list contains a pair (phi,not phi)
for now only works for literals due to implementation of compare! *)
| [] | [_] -> false
| a :: b :: xs ->
if (compare a b) = 0 then true else neg_occurrence (b :: xs) in
match phi with
| BVar _ -> phi
| BNot psi -> BNot (singularise psi)
| BOr psis ->
let unique_psis = Aux.unique_sorted ~cmp:invcmp psis in
let lits = List.filter is_literal unique_psis in
if neg_occurrence lits then BAnd [] else
BOr (List.rev_map singularise unique_psis)
| BAnd psis ->
let unique_psis = Aux.unique_sorted ~cmp:invcmp psis in
let lits = List.filter is_literal unique_psis in
if neg_occurrence lits then BOr [] else
BAnd (List.rev_map singularise unique_psis) in
let rec subsumption phi =
LOG 2 "simplify: subsumption";
let subclause a b =
match (a,b) with
| (BOr psis, BOr thetas)
| (BAnd psis, BAnd thetas) ->
List.for_all (fun x -> List.exists (fun y -> y=x) thetas) psis
| (_, _) -> false in
let subformula psi theta =
match theta with
| BOr thetas
| BAnd thetas -> List.exists (fun theta -> theta = psi) thetas
| _ -> false in
match phi with
| BVar _ | BNot _ -> phi
| BAnd psis ->
let (disjnctns,non_disjnctns) = List.partition is_disjunction psis in
BAnd (List.rev_append (List.rev non_disjnctns) (
List.filter
(fun theta ->
(List.for_all (fun phi -> phi=theta ||
not (subformula phi theta)) non_disjnctns)
&& (List.for_all (fun phi -> phi=theta ||
not (subclause phi theta)) disjnctns)
) disjnctns))
| BOr psis ->
let (conjnctns,non_conjnctns) = List.partition is_conjunction psis in
BOr (List.rev_append (List.rev non_conjnctns) (
List.filter
(fun theta ->
(List.for_all (fun phi -> phi=theta ||
not (subformula phi theta)) non_conjnctns)
&& (List.for_all (fun phi -> phi=theta ||
not (subclause phi theta)) conjnctns)
) conjnctns)) in
let unit_propagation phi =
LOG 2 "simplify: unit_propagation";
(* beware that unit_propagation might introduce the subformula true,
and hence should be followed by neutral_absorbing before
starting the next fixed-point iteration *)
match phi with
| BAnd phis ->
let units = List.rev (List.rev_map (
function | BVar v -> v | _ -> failwith ("not a literal!")
) (List.filter is_literal phis)) in
let rec propagate units phi =
match phi with
| BVar v ->
if List.exists (fun unit -> v=unit) units then BAnd [] else phi
| BNot psi -> BNot (propagate units psi)
| BAnd psis -> BAnd (List.rev (List.rev_map (propagate units) psis))
| BOr psis-> BOr (List.rev (List.rev_map (propagate units) psis)) in
BAnd (List.rev_append (List.rev_map (fun v -> BVar v) units)
(List.rev (List.rev_map (propagate units) phis)))
| _ -> phi in
let rec resolution phi =
LOG 2 "simplify: resolution";
match phi with
| BVar v -> phi
| BNot psi -> BNot (resolution psi)
| BOr psis ->
let res_psis = List.rev (List.rev_map resolution psis) in
let neg_phi = to_nnf (BNot (BOr res_psis)) in
let res_neg_phi = resolution neg_phi in
to_nnf (BNot res_neg_phi)
| BAnd psis ->
let (clauses, non_clauses) = List.partition
(fun psi -> is_disjunction psi || is_literal psi) psis in
let resolvent cl1 cl2 =
(* construct the resolvent of clauses cl1 and cl2 and
tag it with the reserved literal 0 *)
let rec split_clause (acc_lits, acc_rest) = function
| BVar v -> (v :: acc_lits, acc_rest)
| BOr phis -> (match phis with
| [] -> (acc_lits, acc_rest)
| psi :: psis ->
if (is_literal psi) then
split_clause ((int_of_lit psi)::acc_lits, acc_rest)
(BOr psis)
else split_clause (acc_lits, psi::acc_rest) (BOr psis)
)
| _ -> failwith ("this is not a clause feasible for resolution!") in
let (cl1_lits,cl1_rest) = split_clause ([],[]) cl1 in
let (cl2_lits,cl2_rest) = split_clause ([],[]) cl2 in
let res_lits = (* obtain list of feasible pivot-literals *)
List.filter (fun lit1 ->
List.exists (fun lit2 -> lit2 = -lit1) cl2_lits) cl1_lits in
LOG 4 "res_lits: %s"
(String.concat ", " (List.map string_of_int res_lits));
(* if there is more than one possible pivot-literal, the resulting
clause will be equivalent to true, so we don't care *)
if (List.length res_lits) <> 1 then BAnd []
else (* construct a resolvent and mark it with the unused literal 0 *)
let lit = List.nth res_lits 0 in
(* construct resolvent of cl1 and cl2 using pivot-literal lit *)
let flist = List.rev_map lit_of_int
(List.rev_append (List.rev (
List.filter (fun lit1 -> lit1 <> lit) cl1_lits))
(List.filter (fun lit2 -> lit2 <> -lit) cl2_lits)) in
BOr ((lit_of_int 0) :: (List.rev_append flist (
List.rev_append (List.rev cl1_rest) cl2_rest))) in
let res_clauses = ref [] in
let subsumed = ref [] in
(* Construct all possible resolvents and check each new resolvent
whether it is subsumed by some existing clause.
In fact, the following does not work: If this is the case we can
remove two initial clauses (ie add them to the list subsumed).
Instead, we discard the resolved but subsumed clause directly.
*)
List.iter (fun cl1 ->
(List.iter
(fun cl2 ->
let cl_res = resolvent cl1 cl2 in
let subclause a b = (* i.e. a \subseteq b *)
match (a,b) with
| ((BVar v as lit), BOr thetas)
| ((BVar v as lit), BAnd thetas) ->
List.exists (fun y -> y=lit) thetas
| (BOr psis, (BVar v as lit))
| (BAnd psis, (BVar v as lit)) ->
List.for_all (fun x -> x=lit) psis
| (BOr psis, BOr thetas)
| (BAnd psis, BAnd thetas) ->
List.for_all
(fun x -> List.exists (fun y -> y=x) thetas) psis
| (_, _) -> false in
if
(List.exists (fun clause -> subclause clause cl_res) clauses)
then ( (* do nothing, since the resolvent is useless *) ) else
res_clauses := cl_res :: !res_clauses;
) clauses)) clauses;
LOG 2 "simplify: resolution: filtering; clauses: %i subsumed: %i"
(List.length clauses) (List.length !subsumed);
LOG 3 "Resolvents: %s\nSubsumed clauses: %s\nReduced Resolvents: %s"
(String.concat ", " (List.rev (List.rev_map str !res_clauses)))
(String.concat ", " (List.rev (List.rev_map str !subsumed)))
(str (singularise (BAnd !res_clauses)));
let filtered =
List.filter
(fun clause ->
not (List.exists (fun sub -> clause=sub) !subsumed)) clauses in
LOG 2 "simplify: resolution: computing total";
let total = List.rev_append (List.rev filtered)
(List.rev_append (List.rev !res_clauses) non_clauses) in
singularise (neutral_absorbing (BAnd total)) in
let choose_resolvents phi =
LOG 2 "simplify: choose_resolvents";
(* check the resolvents for "good" ones (at the moment these are clauses
that subsume clauses in the original formula) and discard the rest *)
let rec filter_by_subsumption = function
| BOr psis ->
let filtered_psis= List.rev (List.rev_map filter_by_subsumption psis) in
let neg_phi = to_nnf (BNot (BOr filtered_psis)) in
let filtered_neg_phi = filter_by_subsumption neg_phi in
to_nnf (BNot filtered_neg_phi)
| BAnd psis ->
let subclause a b =
(* here, a is a resolvent, so we should not consider the literal 0! *)
match (a,b) with
| ((BVar v as lit), BOr thetas)
| ((BVar v as lit), BAnd thetas) ->
List.exists (fun y -> y=lit) thetas
| (BOr psis, (BVar v as lit))
| (BAnd psis, (BVar v as lit)) ->
List.for_all (fun x -> x=lit || x=(lit_of_int 0)) psis
| (BOr psis, BOr thetas)
| (BAnd psis, BAnd thetas) ->
List.for_all
(fun x -> x=(lit_of_int 0) || List.exists (fun y-> y=x) thetas)
psis
| (_, _) -> false in
let (clauses, non_clauses) =
List.partition (fun phi -> is_disjunction phi || is_literal phi)
psis in
let (resolvents, non_resolvents) = List.partition
(fun clause ->
(* actually these clauses do not necessarily contain only
literals but maybe also more complex subformulas! *)
let lits =
match clause with
| BOr lits -> lits
| BVar v as lit -> [lit]
| _ ->
failwith("[filter_by_subsumption] This is not a clause!") in
(is_disjunction clause &&
List.exists (fun lit -> lit=(lit_of_int 0)) lits)) clauses in
let useful_resolvents = List.filter
(fun resolvent ->
List.exists (fun phi -> subclause resolvent phi) non_resolvents)
resolvents in
LOG 3 "Useful resolvents: %s"
(String.concat ", " (List.map str useful_resolvents));
let new_clauses =
List.rev_map (function
| BOr lits ->
BOr (List.filter (fun lit -> lit <> (lit_of_int 0)) lits)
| _ -> failwith ("trying to remove literals from a non-clause!")
) useful_resolvents in
BAnd (List.rev_append new_clauses (
List.rev_append (List.rev non_resolvents)
(List.rev (List.rev_map filter_by_subsumption non_clauses))))
| BNot psi -> BNot (filter_by_subsumption psi)
| BVar v as lit ->
if v=0 then failwith "There should not be empty resolved clauses!" else
lit in
filter_by_subsumption phi in
let simplified =
let simp_resolution = fun phi ->
if ((!simplification lsr 2) land 1) > 0 then
choose_resolvents (subsumption (resolution phi))
else phi in
let simp_fun = fun phi ->
(simp_resolution
(neutral_absorbing
(unit_propagation
(subsumption
(singularise
(neutral_absorbing
(flatten
(to_nnf phi)))))))) in
let rec fp f x =
let y = f x in
if y=x then x else fp f y in
fp (fun phi -> (simp_fun phi)) phi in
LOG 2 "Simplification:\nphi %s\nwas simplified to %s"
(str phi) (str simplified);
simplified
let full_simplify f =
set_simplification 7;
let res = simplify f in
set_simplification 2;
res
let subst_simp vars f =
let mem_simp = !simplification in
simplification := 2;
let res = simplify (subst vars f) in
simplification := mem_simp;
res
(* Convert reduced Boolean combination into CNF with aux variables (Tseitin) *)
let auxcnf_of_bool_formula phi =
let max_abs m lit = if lit < 0 then max m (-lit) else max m lit in
let rec get_max_lit m = function
| BVar v -> max_abs m v
| BNot phi -> get_max_lit m phi
| BAnd [] | BOr [] -> m
| BAnd (bflist) | BOr (bflist) -> List.fold_left get_max_lit m bflist in
let max_lit = get_max_lit 0 phi in
let (clauses, free_idx) = (ref [], ref max_lit) in
let bv l = List.rev_map (fun i -> BVar i) l in
let rec index_formula = function
| BVar v -> v
| BNot phi -> - (index_formula phi)
| BOr bflist ->
let indlist = List.rev_map index_formula bflist in
free_idx := !free_idx + 1;
List.iter (fun i -> clauses := (BOr (bv [-i; !free_idx])) :: !clauses)
indlist;
clauses := BOr (bv ((- !free_idx) :: indlist)) :: !clauses;
!free_idx
| _ -> failwith "auxcnf_to_bool_formula: converting non-reduced formula" in
let res_var = index_formula (to_reduced_form phi) in
(max_lit + 1, BAnd ((BOr [BVar (- res_var)]) :: !clauses))
(* Convert an arbitrary Boolean combination into a CNF with auxiliary variables
using the approach by Plaisted and Greenbaum *)
let pg_auxcnf_of_bool_formula ?(setmax=0) phi =
let max_abs m lit = if lit < 0 then max m (-lit) else max m lit in
let rec get_max_lit m = function
| BVar v -> max_abs m v
| BNot phi -> get_max_lit m phi
| BAnd [] | BOr [] -> m
| BAnd (bflist) | BOr (bflist) -> List.fold_left get_max_lit m bflist in
let max_lit, index_tbl = max (get_max_lit 0 phi) setmax, Hashtbl.create 63 in
let (clauses, free_idx) = (ref [], ref max_lit) in
let bv l = List.rev_map (fun i -> BVar i) l in
let rec index_formula ?(neg=false) = function
| BVar v -> v
| BNot phi -> - index_formula ~neg:(not neg) phi
| BOr [phi] -> index_formula ~neg phi
| BAnd [phi] -> index_formula ~neg phi
| BOr bflist ->
(try Hashtbl.find index_tbl (BOr bflist) with Not_found ->
let indlist = List.rev_map (index_formula ~neg:neg) bflist in
free_idx := !free_idx + 1;
if neg then
List.iter (fun i -> clauses := (BOr (bv [-i; !free_idx])) :: !clauses)
indlist
else
clauses := BOr (bv ((- !free_idx) :: indlist)) :: !clauses;
Hashtbl.add index_tbl (BOr bflist) !free_idx;
!free_idx
)
| BAnd bflist ->
(try Hashtbl.find index_tbl (BAnd bflist) with Not_found ->
let indlist = List.rev_map (index_formula ~neg:neg) bflist in
free_idx := !free_idx + 1;
if neg then
clauses :=
BOr (bv (!free_idx :: (List.rev_map (fun i -> -i) indlist))) ::
!clauses
else
List.iter
(fun i -> clauses := (BOr (bv [i; (- !free_idx)])) :: !clauses)
indlist;
Hashtbl.add index_tbl (BAnd bflist) !free_idx;
!free_idx
) in
let res_var =
match phi with
| BNot psi -> - index_formula ~neg:false psi
| _ -> index_formula ~neg:true phi in
(max_lit + 1, BAnd ((BOr [BVar (- res_var)]) :: !clauses))
let listcnf_of_boolcnf phi =
let int_of_literal = function
| BVar v -> v
| _ -> raise (FormulaError "Clauses must not contain non-literals!") in
let list_of_clause = function
| BVar v -> [v]
| BOr (bflist) -> List.rev_map int_of_literal bflist
| _ -> raise (FormulaError "This is not a clause!") in
match phi with
| BVar v -> [[v]]
| BAnd (bflist) -> List.rev_map list_of_clause bflist
| _ -> raise (FormulaError "This is not a CNF!")
let subsumption_filter cnf =
let subset a b =
List.for_all (fun x -> List.exists (fun y -> y=x) b) a in
List.filter (fun x -> List.for_all (fun y -> x=y || not(subset y x)) cnf) cnf
(* Check if a CNF formula is satisfiable and find a model.
Faster than Sat.sat due to lack of formula registration *)
let find_sat cnf =
MiniSAT.reset ();
let vars = Hashtbl.create 15 in
let var v = try Hashtbl.find vars v with Not_found ->
(let w = MiniSAT.new_var () in Hashtbl.add vars v w; w) in
let lit v = let w = var (abs v) in
if v > 0 then MiniSAT.pos_lit w else MiniSAT.neg_lit w in
let add_clause cl = MiniSAT.add_clause (List.rev_map lit cl) in
List.iter add_clause cnf;
match MiniSAT.solve () with
| MiniSAT.UNSAT -> MiniSAT.reset (); None
| MiniSAT.TIMEOUT -> MiniSAT.reset (); failwith "do_sat: timeout"
| MiniSAT.SAT ->
let res = ref [] in
let update v mv =
if MiniSAT.value_of mv = 0 then res := (-v) :: !res
else if MiniSAT.value_of mv = 1 then res := v :: !res in
Hashtbl.iter update vars;
MiniSAT.reset ();
Some (!res)
(* Print the CNF formula in dimacs format. *)
let print_dimacs cnf =
let maxvar cl = List.fold_left (fun acc b -> max acc (abs b)) 0 cl in
let mvar = List.fold_left (fun acc cl -> max acc (maxvar cl)) 0 cnf in
let cl_str cl = (String.concat " " (List.map string_of_int cl)) ^ " 0\n" in
AuxIO.print ("p cnf " ^ (string_of_int mvar) ^ " " ^
(string_of_int (List.length cnf)) ^ "\n");
List.iter (fun cl -> AuxIO.print (cl_str cl)) cnf
let print_dimacs_str cnf =
let maxvar cl = List.fold_left (fun acc b -> max acc (abs b)) 0 cl in
let mvar = List.fold_left (fun acc cl -> max acc (maxvar cl)) 0 cnf in
let cl_str cl = (String.concat " " (List.map string_of_int cl)) ^ " 0\n" in
"p cnf " ^ (string_of_int mvar) ^ " " ^ (string_of_int (List.length cnf)) ^
"\n" ^ (String.concat "" (List.rev_map cl_str (List.rev cnf)))
let cnf_of_bool_formula ?(use_pg=false) ?(setmax=0) phi =
let rec aux free_id = function
| BVar v -> [[v]], (max (abs v) free_id)
| BNot (BVar v) -> [[-v]], (max (abs v) free_id)
| BNot _ -> failwith "cnf_of_bool_formula: arg not in nnf"
| BAnd fl -> List.fold_left (fun (cls, fid) phi ->
let (fcls, nfid) = aux fid phi in
(List.rev_append fcls cls, nfid) ) ([], free_id) fl
| BOr [] -> [[]], free_id
| BOr fl ->
let (new_cl, to_name, fid) = List.fold_left (fun (cl, names, fid) phi ->
match aux fid phi with
| ([], _) -> failwith "cnf_of_bool_formula: true in flattened phi";
| ([ncl], nfid) -> (List.rev_append ncl cl, names, nfid)
| (l, nfid) -> (nfid::cl, (nfid, l)::names, nfid+1)
) ([], [], free_id) fl in
let name_cl (var, cnf) =
(* X -> (a v b v c) and (d v e v f) and g =
-X v ( (a v b v c) and (d v e v f) and g ) =
(-X v a v b v c) and (-X v d v e v f) and (-X v g) *)
List.rev_map (fun cl -> Aux.unique_sorted ((-var)::cl)) cnf in
let name_cls = List.rev_map name_cl to_name in
(new_cl :: (List.concat name_cls), fid) in
if use_pg then
let arg = flatten (to_nnf ~neg:true phi) in
let (sep, aux_phi) = pg_auxcnf_of_bool_formula ~setmax arg in
sep, listcnf_of_boolcnf aux_phi
else (
let phi = flatten (to_nnf phi) in
let max_lit = ref setmax in
let rec bf_lit_iter f phi = match phi with
| BVar v -> f v | BNot x -> bf_lit_iter f x
| BOr l | BAnd l -> List.iter (bf_lit_iter f) l in
bf_lit_iter (fun l -> max_lit := max !max_lit (abs l)) phi;
let cnf = fst (aux (!max_lit + 1) phi) in
!max_lit + 1, cnf
)
(* Find a model of a Boolean formula. Uses P.-G. conversion. *)
let find_model ?logtime ?(logprefix="") phi =
let sep, cnf = cnf_of_bool_formula ~use_pg:true phi in
(match logtime with None -> () | Some t ->
LOG 0 "%sCNF constructed at %.3fs" logprefix (AuxIO.gettimeofday () -. t));
if logprefix = "__PRINTCNF__" then print_dimacs cnf;
let reg_t = AuxIO.gettimeofday () in
let log_finish () =
match logtime with None -> () | Some t ->
let cur_t = AuxIO.gettimeofday () in
LOG 0 "%sSolver finished at %.3fs (ran %.3fs)" logprefix
(cur_t-.t) (cur_t-.reg_t) in
match find_sat cnf with
| None -> log_finish (); None
| Some l ->
log_finish ();
let valid = List.filter (fun v -> v < sep && v > -sep) l in
Some (Aux.unique_sorted valid)
let convert ?(disc_vars=[]) phi =
(* input is a Boolean combination; output is a list of list of integers
interpreted as a cnf *)
let (aux_separator, aux_cnf_formula) =
match !auxcnf_generation with
| 0 -> failwith "this function must not be called w/o auxcnf-converion"
| 1 -> (* use Tseitin conversion *)
auxcnf_of_bool_formula
(to_reduced_form (flatten (to_nnf ~neg:false phi)))
| 2 -> (* or Plaisted-Greenbaum conversion *)
let arg = flatten (to_nnf ~neg:false phi) in
LOG 1 "CNF conv: arg computed";
pg_auxcnf_of_bool_formula arg
| _ -> failwith "undefined parameter value" in
LOG 1 "Separator is: %i" aux_separator;
LOG 2 "Converting Aux-CNF: %s" (str aux_cnf_formula);
let aux_cnf = listcnf_of_boolcnf aux_cnf_formula in
let cnf_llist = Sat.convert_aux_cnf ~disc_vars aux_separator aux_cnf in
LOG 1 "Converted CNF. ";
LOG 2 "Converted CNF: %s" (Sat.cnf_str cnf_llist);
let simplified =
if (!simplification land 1) > 0 then
subsumption_filter cnf_llist
else cnf_llist in
LOG 2 "Subsumption %b; Simplified CNF: %s"
((!simplification land 1) > 0) (Sat.cnf_str simplified);
simplified
(* given a formula, convert to CNF. *)
let formula_to_cnf phi =
let (ids, rev_ids, free_id) = (Hashtbl.create 7, Hashtbl.create 7, ref 1) in
let boolean_phi = bool_formula_of_formula_arg phi (ids, rev_ids, free_id) in
let cnf_llist = convert boolean_phi in
LOG 2 "formula_to_cnf: converted";
let bool_cnf =
BAnd (List.rev (List.rev_map (
fun literals -> BOr (List.rev (List.rev_map lit_of_int literals))
) cnf_llist)) in
LOG 2 "formula_to_cnf: bool_cnf";
let simplified =
if ((!simplification lsr 1) land 1) > 0 then
simplify bool_cnf
else bool_cnf in
LOG 2 "formula_to_cnf: simplified";
let formula_cnf =
formula_of_bool_formula_arg simplified (ids, rev_ids, free_id) in
formula_cnf
(* ------- Boolean quantifier elimination using CNF conversion ------- *)
let to_cnf_basic ?(disc_vars=[]) phi =
let cnf = convert ~disc_vars phi in
neutral_absorbing
(BAnd (List.rev_map (fun lits -> BOr (List.map lit_of_int lits)) cnf))
let to_cnf ?(disc_vars=[]) ?(tm=1200.) phi =
try
Sat.set_timeout tm;
let res = to_cnf_basic ~disc_vars phi in
Sat.clear_timeout ();
Some (res)
with Aux.Timeout _ -> None
let try_cnf ?(disc_vars=[]) tm phi =
match to_cnf ~disc_vars ~tm phi with None -> phi | Some psi -> psi
let to_dnf_basic ?(disc_vars=[]) phi =
to_nnf ~neg:true (to_cnf_basic ~disc_vars (to_nnf ~neg:true phi))
let to_dnf ?(disc_vars=[]) ?(tm=1200.) phi =
match to_cnf ~disc_vars ~tm (to_nnf ~neg:true phi) with
| None -> None
| Some psi -> Some (to_nnf ~neg:true psi)
let try_dnf ?(disc_vars=[]) tm phi =
match to_dnf ~disc_vars ~tm phi with None -> phi | Some psi -> psi
let univ ?(dbg=0) v phi =
if dbg > 0 then AuxIO.printf "Univ subst in %s\n%!" (str phi);
let simp1 = subst_simp [v] phi in
if dbg > 0 then AuxIO.printf "Univ subst POS: %s\n%!" (str simp1);
let simp2 = subst_simp [-v] phi in
if dbg > 0 then AuxIO.printf "Univ subst NEG: %s\n%!" (str simp2);
BAnd [simp1; simp2]
let to_sat ?(tm=1200.) phi =
let rec all_vars acc = function
| BVar v -> (abs v) :: acc
| BNot f -> all_vars acc f
| BOr fl | BAnd fl -> List.fold_left all_vars acc fl in
to_dnf ~disc_vars:(all_vars [] phi) ~tm phi
let sort_freq phi vars =
let rec occ v acc = function
| BVar w -> if abs v = abs w then acc + 1 else acc
| BNot f -> occ v acc f
| BOr fl | BAnd fl -> List.fold_left (occ v) acc fl in
let freqs = Hashtbl.create (List.length vars) in
List.iter (fun v -> Hashtbl.add freqs v (occ v 0 phi)) vars;
let fq v = Hashtbl.find freqs v in
List.sort (fun v w -> (fq v) - (fq w)) vars
let (tm_jump, cutvar, has_vars_mem) = (1.1, 2, Hashtbl.create 31)
(* Returns a quantifier-free formula equivalent to All (vars, phi).
The list [vars] contains only positive literals and [phi] is in NNF. *)
let rec elim_all_rec ?(nocheck=false) prefix tout vars in_phi =
if List.length vars = 0 then in_phi else match in_phi with
| BVar v -> if List.mem (abs v) vars then BOr [] else (BVar v)
| BNot _ -> failwith "error (elim_all_rec): BNot in NNF Boolean formula"
| BAnd fs ->
if prefix.[0] <> 'S' then
LOG 1 "%s vars %i list %i (same sign)"
prefix (List.length vars) (List.length fs);
let do_elim (acc, i) f =
if f = BOr [] || acc = [BOr []] then ([BOr []], i+1) else
let new_pref = prefix ^ (string_of_int i) ^ ":" in
let elim_f = elim_all_rec new_pref tout vars f in
if elim_f = BOr [] then ([BOr []], i+1) else
if elim_f = BAnd [] then (acc, i+1) else (elim_f :: acc, i+1) in
let (simp_fs, _) = List.fold_left do_elim ([], 0) fs in
if prefix.[0] <> 'S' then LOG 1 "%s done " prefix;
let res = match to_dnf ~tm:(5. *. tout) (BAnd simp_fs) with
| None ->
if prefix.[0] <> 'S' then LOG 1 "(non-dnf %i)" (size (BAnd simp_fs));
BAnd simp_fs
| Some psi ->
if prefix.[0] <> 'S' then LOG 1 "(dnf %i)" (size psi);
psi in
neutral_absorbing (flatten res)
| BOr [] -> BOr []
| BOr [f] -> elim_all_rec prefix tout vars f
| BOr fs when List.for_all (function BVar _ -> true | _ -> false) fs ->
let is_univ_quant = function
| BVar v -> List.mem (abs v) vars
| _ -> failwith "error (elim_all_rec): non-BVar in BVar-only list" in
BOr (List.filter (fun v -> not (is_univ_quant v)) fs)
| BOr fs as phi ->
let rec has_vars sgn vl = function (* check if any var occurs *)
| BVar v -> if sgn then List.mem v vl else List.mem (abs v) vl
| BNot f -> has_vars sgn vl f
| BOr fl | BAnd fl -> List.exists (has_vars sgn vl) fl in
let has_vars_memo sgn vl =
try Hashtbl.find has_vars_mem (sgn, vl) with Not_found ->
let res = has_vars sgn vl in
Hashtbl.add has_vars_mem (sgn, vl) res;
res in
if prefix.[0] <> 'S' then
LOG 1 "%s vars %i list %i (partition)"
prefix (List.length vars) (List.length fs);
let (fs_yes, fs_no) = List.partition (has_vars_memo false vars) fs in
if Hashtbl.length has_vars_mem > 10000 then Hashtbl.clear has_vars_mem;
if fs_no <> [] then (
let elim_yes = elim_all_rec prefix tout vars (BOr fs_yes) in
neutral_absorbing (flatten (BOr (elim_yes :: fs_no)))
) else if List.length vars = 1 then (
let sub = univ (List.hd vars) phi in
if prefix.[0] = 'S' then simplify (to_dnf_basic sub) else
let (res, msg ) = match to_dnf ~tm:(5. *. tout) sub with
| None -> (simplify sub, "no dnf")
| Some dnf -> (simplify dnf, "dnf") in
LOG 1 "%s vars %i list %i (%s)"
prefix (List.length vars) (List.length fs) msg;
res
) else if List.length vars < cutvar then (
let insert psi v = neutral_absorbing (flatten (univ v psi)) in
let sub = List.fold_left insert phi vars in
let (res, msg ) = match to_dnf ~tm:(3. *. tout) sub with
| None -> (simplify sub, "no dnf")
| Some dnf -> (simplify dnf, "dnf") in
LOG 1 "%s vars %i list %i (%s)"
prefix (List.length vars) (List.length fs) msg;
res
) else (
LOG 1 "%s vars %i list %i (inside %i)"
prefix (List.length vars) (List.length fs) (size phi);
try
if nocheck then raise (Aux.Timeout "!!out");
LOG 1 "%s vars %i list %i (cnf conv) "
prefix (List.length vars) (List.length fs);
let bool_cnf = match to_cnf ~disc_vars:vars ~tm:(3.*.tout) phi with
| None -> raise (Aux.Timeout "!!none")
| Some psi -> psi in
LOG 1 "success";
let cnf = elim_all_rec prefix tout vars bool_cnf in
let xsize = function BAnd l -> List.length l | _ -> 0 in
if prefix.[0] <> 'S' then
LOG 1 "%s vars %i list %i (cnf after conv %i)"
prefix (List.length vars) (List.length fs) (xsize cnf);
match to_dnf ~tm:(5. *. tout) cnf with
| None ->
if prefix.[0] <> 'S' then LOG 1 "(none)"; cnf
| Some dnf ->
if prefix.[0] <> 'S' then LOG 1 "(dnf)"; dnf
with Aux.Timeout s ->
if s <> "!!out" then LOG 1 "failed";
let elim nbr_left timeout psi v =
try
LOG 1 "%s eliminating %i" prefix v;
if nbr_left > 2 then (
Sat.set_timeout (timeout);
) else ( Sat.set_timeout (3. *. timeout) );
let res = elim_all_rec "S" tout [v] psi in
Sat.clear_timeout ();
LOG 1 " success.";
Some res
with Aux.Timeout _ ->
LOG 1 " failed.";
None in
let try_elim_var timeout (left_vars,cur_phi,elim_nbr,step,all_nbr) v =
if not (has_vars_memo true [-v] cur_phi) then (
LOG 1 "%s elimineted %i (only pos)" prefix v;
(left_vars, subst_simp [-v] cur_phi, elim_nbr+1, step+1, all_nbr)
) else if not (has_vars_memo true [v] cur_phi) then (
LOG 1 "%s elimineted %i (only neg)" prefix v;
(left_vars, subst_simp [v] cur_phi, elim_nbr+1, step+1, all_nbr)
) else if 2*step > all_nbr && elim_nbr > 0 &&
step+2 < all_nbr && all_nbr - elim_nbr > cutvar then
(v :: left_vars, cur_phi, elim_nbr, step + 1, all_nbr)
else match elim (all_nbr - step) timeout cur_phi v with
| None -> (v :: left_vars, cur_phi, elim_nbr, step + 1, all_nbr)
| Some psi -> (left_vars, psi, elim_nbr + 1, step + 1, all_nbr) in
let (left_vars, new_phi, elim_nbr, _, all_nbr) =
List.fold_left (try_elim_var tout) ([], phi,0,0, List.length vars)
(sort_freq phi vars) in
if elim_nbr > 0 then
elim_all_rec prefix tout left_vars new_phi
else
let (big_v, rest_vars) = (List.hd left_vars, List.tl left_vars) in
LOG 1 "branch %i" big_v;
elim_all_rec prefix (tm_jump *.tout) rest_vars (univ big_v new_phi)
)
(* Returns a quantifier-free formula equivalent to All (vars, phi). *)
let elim_all vars phi =
elim_all_rec " " 0.4 (List.map (fun v -> abs v) vars) (to_nnf phi)
(* Returns a quantifier-free formula equivalent to Ex (vars, phi). *)
let elim_ex vars phi =
set_simplification 6;
let res = to_nnf ~neg:true (elim_all vars (to_nnf ~neg:true phi)) in
set_simplification 2;
res
(* ------ Reading and reducing QBF --------- *)
open HashCons
(* Type for quantified Boolean formulas. *)
type qbf_raw =
| QVar of int
| QNot of qbf
| QAnd of qbf list
| QOr of qbf list
| QEx of int list * qbf
| QAll of int list * qbf
and qbf = qbf_raw hc
let hashSIZE = 699967
let smallSIZE = 9973
module QBFHash = struct
type t = qbf_raw
let rec equal qbf1 qbf2 = match qbf1, qbf2 with
| QVar i, QVar j -> i = j
| QNot f, QNot g -> f == g
| QAnd l, QAnd m | QOr l, QOr m ->
(try List.for_all2 (fun f g -> f == g) l m with Invalid_argument _->false)
| QEx (vs, f), QEx (ws, g) | QAll (vs, f), QAll (ws, g) ->
f == g && vs = ws
| _ -> false
let hash = function
| QVar i -> 3*i
| QNot f -> 3*f.tag+1
| QOr l -> 3*(Hashtbl.hash (List.rev_map (fun f -> f.tag) l))+1
| QAnd l -> 3*(Hashtbl.hash (List.rev_map (fun f -> f.tag) l))+2
| QEx (vs, f) -> 3*(Hashtbl.hash (f.tag, vs))+1
| QAll (vs, f) -> 3*(Hashtbl.hash (f.tag, vs))+2
end
module IListHash = struct
type t = int list
let equal l1 l2 = l1 = l2
let hash l = Hashtbl.hash l
end
module QBFCons = HashCons.Make(QBFHash)(IListHash)
module H1 = QBFCons.H1
module H2 = QBFCons.H2
module HV = QBFCons.HV
let qbf_tbl = QBFCons.create hashSIZE
let cVar i = QBFCons.hashcons qbf_tbl (QVar i)
let cNot f = QBFCons.hashcons qbf_tbl (QNot f)
let cOr l = QBFCons.hashcons qbf_tbl (QOr l)
let cAnd l = QBFCons.hashcons qbf_tbl (QAnd l)
let cEx (vs, f) = QBFCons.hashcons qbf_tbl (QEx (vs, f))
let cAll (vs, f) = QBFCons.hashcons qbf_tbl (QAll (vs, f))
let qbf_hc = function
| QVar i -> cVar i | QNot f -> cNot f
| QOr l -> cOr l | QAnd l -> cAnd l
| QEx (vs, f) -> cEx (vs, f) | QAll (vs, f) -> cAll (vs, f)
(* Print a QBF formula. *)
let qbf_str ?names phi =
let name s = match names with None -> var_str s | Some tbl ->
try Hashtbl.find tbl s with Not_found -> var_str s in
let rec qbf_str_rec phi = match phi.x with
| QVar v -> if v < 0 then "-" ^ (name (-v)) else name v
| QNot phi -> "(not " ^ (qbf_str_rec phi) ^ ")"
| QAnd [] -> "true"
| QOr [] -> "false"
| QAnd (qbflist) -> qbf_list_str " and " qbflist
| QOr (qbflist) -> qbf_list_str " or " qbflist
| QEx (vars, phi) ->
"(ex " ^ (String.concat ", " (List.map name vars)) ^
" " ^ qbf_str_rec phi ^ ")"
| QAll (vars, phi) ->
"(all " ^ (String.concat ", " (List.map name vars)) ^
" " ^ qbf_str_rec phi ^ ")"
and qbf_list_str sep = function
| [] -> "[]"
| [phi] -> qbf_str_rec phi
| lst -> "(" ^ (String.concat sep (List.map qbf_str_rec lst)) ^ ")"
in qbf_str_rec phi
(* Convert a QBF to NNF and additionally negate if [neg] is set. *)
let rec nnf ?(neg=false) qbf = match qbf.x with
| QVar v -> if neg then cVar (-1 * v) else cVar v
| QNot phi -> if neg then nnf ~neg:false phi else nnf ~neg:true phi
| QAnd (flist) when neg ->
cOr (List.rev (List.rev_map (nnf ~neg:true) flist))
| QAnd (flist) -> cAnd (List.rev (List.rev_map (nnf ~neg:false) flist))
| QOr (flist) when neg ->
cAnd (List.rev (List.rev_map (nnf ~neg:true) flist))
| QOr (flist) -> cOr (List.rev (List.rev_map (nnf ~neg:false) flist))
| QEx (vs, f) when neg -> cAll (vs, nnf ~neg:true f)
| QEx (vs, f) -> cEx (vs, nnf ~neg:false f)
| QAll (vs, f) when neg -> cEx (vs, nnf ~neg:true f)
| QAll (vs, f) -> cAll (vs, nnf ~neg:false f)
(* Free variables in a QBF. *)
let rec free_vars phi = match phi.x with
| QVar (v) -> [abs v]
| QNot (f) -> free_vars f
| QAnd (l) | QOr (l) -> Aux.unique_sorted (Aux.concat_map free_vars l)
| QEx (vs, phi) | QAll (vs, phi) ->
let free, vs = free_vars phi, Aux.unique_sorted vs in
Aux.sorted_diff free vs
(* Flatten a QBF. *)
let rec flatten_qbf phi =
let get_conjunctions = function {x=QAnd fl} -> fl | f -> [f] in
let get_disjunctions = function {x=QOr fl} -> fl | f -> [f] in
let fold_acc f xl =
List.fold_left (fun acc x -> List.rev_append (List.rev (f x)) acc) [] xl in
let rev_collect_conj xl = fold_acc get_conjunctions xl in
let rev_collect_disj xl = fold_acc get_disjunctions xl in
match phi.x with
| QNot ({x=QNot psi}) -> flatten_qbf psi
| QNot ({x=QVar v}) -> cVar (-v)
| QNot psi -> cNot (flatten_qbf psi)
| QOr (flist) ->
let res = rev_collect_disj (List.rev_map flatten_qbf flist) in
if List.mem (cAnd []) res then cAnd [] else cOr (res)
| QAnd (flist) ->
let res = rev_collect_conj (List.rev_map flatten_qbf flist) in
if List.mem (cOr []) res then cOr [] else cAnd (res)
| QEx (vs, f) -> cEx (vs, flatten_qbf f)
| QAll (vs, f) -> cAll (vs, flatten_qbf f)
| _ -> phi
(* Read a qdimacs description of a QBF from [in_ch]. *)
let read_qdimacs in_str =
let in_pos, in_len = ref 0, String.length in_str in
let sinput_one_line () =
try
let i = String.index_from in_str !in_pos '\n' in
let line = String.sub in_str !in_pos (i - !in_pos) in
in_pos := i+1;
line
with Not_found | Invalid_argument _ ->
if !in_pos >= in_len then raise End_of_file else
let line = String.sub in_str !in_pos (in_len - !in_pos) in
in_pos := in_len;
line in
let rec sinput_line () =
let l = sinput_one_line () in if l = "" then sinput_line () else l in
(* Read the starting 'c' comment lines, and the first 'p' line.
Set the number of variables and the number of clauses. *)
let rec read_header () =
let line = sinput_line () in
let line = Aux.strip_spaces line in
if line.[0] = 'c' then read_header () else
(* Scanf.sscanf line "p cnf %i %i" (fun x y -> y) in *)
let i = String.index_from line 6 ' ' in
int_of_string (String.sub line (i+1) ((String.length line) - i - 1)) in
(* Read one clause from a line. *)
let read_clause line =
let (s, i, clause, len) = (ref "", ref 0, ref [], String.length line) in
let is_end i = i > 0 && line.[i] = '0' && Aux.is_space (line.[i-1]) in
while !i < len && Aux.is_space (line.[!i]) do incr i done;
while (!i < len && not (is_end !i)) do
if Aux.is_space (line.[!i]) then (
while Aux.is_space (line.[!i]) do incr i done;
let lit = int_of_string !s in
clause := lit :: !clause;
s := "";
) else (
s := !s ^ (String.make 1 line.[!i]);
i := !i + 1;
)
done;
!clause in
let list_int line =
let split = Aux.split_spaces line in
List.rev (List.tl (List.rev_map
(fun s -> int_of_string s) (List.tl split))) in
let read_formula () =
let no_cl = read_header () in
LOG 5 "read_formula: header read";
let rec read_phi () =
let line = sinput_line () in
if line.[0] == 'a' then
cAll (list_int line, read_phi ())
else if line.[0] == 'e' then
cEx (list_int line, read_phi ())
else (
let cls = ref [read_clause (line)] in
for i = 1 to (no_cl-1) do
let line = sinput_line () in
LOG 5 "read_formula: line: %s (cl %i of %i)" line i no_cl;
cls := (read_clause line) :: !cls
done;
cAnd (List.map (fun lits -> cOr (List.map (fun v -> cVar v) lits)) !cls)
) in
read_phi () in
read_formula ()
(* Print a QBF formula in qpro format. *)
let print_qpro phi =
let is_lit f = match f.x with | QVar _ | QNot ({x=QVar _})->true | _->false in
let get_lit f = match f.x with | QVar v -> v | QNot ({x=QVar v}) -> -v
| _ -> failwith "get_lit: not a literal" in
let rec print_qrec phi = match phi.x with
| QVar _ | QNot _ -> failwith "print_qpro: error - var or negation"
| QAnd [] -> "d\n1\n1\n/d"
| QOr [] -> "c\n1\n1\n/c"
| QAnd l ->
let (lits, other) = List.partition is_lit l in
let lits = List.rev_map get_lit lits in
let (pos_lit, neg_lit) = List.partition (fun v -> v > 0) lits in
let oth_s = String.concat "\n" (List.rev_map print_qrec other) in
let ls l = String.concat " " (List.rev_map (fun s ->
string_of_int (abs s)) l) in
let pos_s, neg_s = ls pos_lit, ls neg_lit in
if oth_s = "" then Printf.sprintf "c\n%s\n%s\n/c" pos_s neg_s else
Printf.sprintf "c\n%s\n%s\n%s\n/c" pos_s neg_s oth_s
| QOr l ->
let (lits, other) = List.partition is_lit l in
let lits = List.rev_map get_lit lits in
let (pos_lit, neg_lit) = List.partition (fun v -> v > 0) lits in
let oth_s = String.concat "\n" (List.rev_map print_qrec other) in
let ls l = String.concat " " (List.rev_map (fun s ->
string_of_int (abs s)) l) in
let pos_s, neg_s = ls pos_lit, ls neg_lit in
if oth_s = "" then Printf.sprintf "d\n%s\n%s\n/d" pos_s neg_s else
Printf.sprintf "d\n%s\n%s\n%s\n/d" pos_s neg_s oth_s
| QEx (vs, ({x=QVar _} as f)) -> print_qrec (cEx (vs, cAnd [f]))
| QEx (vs, ({x=QNot _} as f)) -> print_qrec (cEx (vs, cAnd [f]))
| QEx ([], f) | QAll ([], f) -> print_qrec f
| QEx (vs, f) ->
let vs_s = String.concat " " (List.map string_of_int vs) in
Printf.sprintf "q\ne %s\n%s\n/q" vs_s (print_qrec f)
| QAll (vs, ({x=QVar _} as f)) -> print_qrec (cAll (vs, cAnd [f]))
| QAll (vs, ({x=QNot _} as f)) -> print_qrec (cAll (vs, cAnd [f]))
| QAll (vs, f) ->
let vs_s = String.concat " " (List.map string_of_int vs) in
Printf.sprintf "q\na %s\n%s\n/q" vs_s (print_qrec f) in
let rec qbf_lit_iter f phi = match phi.x with
| QVar i -> f i
| QOr l | QAnd l -> List.iter (qbf_lit_iter f) l
| QNot x | QEx (_, x) | QAll (_, x) -> qbf_lit_iter f x in
let maxvar = ref 1 in
qbf_lit_iter (fun i -> maxvar := max i !maxvar) phi;
let pre = Printf.sprintf "QBF\n%i\n" !maxvar in
pre ^ (print_qrec (flatten_qbf (nnf phi))) ^ "\nQBF\n"
(* Print a QBF formula in lparse format. *)
let print_lparse ?(universal_vars=[]) phi =
let free_expr_id, rules, vars = ref 1, ref [], ref [] in
let expr_id_int () = incr free_expr_id; !free_expr_id - 1 in
let expr_id () = let i = expr_id_int () in "expr" ^ (string_of_int i) in
let lp_var x = vars := x :: !vars; "x" ^ (string_of_int x) ^ "e" in
let lp_var_truth x =
if x >0 then "t(" ^ (lp_var x) ^")" else "f(" ^ (lp_var (-x)) ^")" in
let rec print_lprec phi = match phi.x with
| QVar v -> lp_var_truth v
| QNot ({x=QVar v}) -> lp_var_truth (-v)
| QNot _ -> failwith "print_lparse: error - not in nnf"
| QAnd [] | QOr [] ->
let left = expr_id () in
rules := (left) :: !rules;
left
| QAnd l ->
let left, l_ids = expr_id (), List.rev_map print_lprec l in
rules := (left ^ " :- " ^ (String.concat ", " l_ids)) :: !rules;
left
| QOr l ->
let left, l_ids = expr_id (), List.rev_map print_lprec l in
List.iter (fun i -> rules := (left ^ " :- " ^ i) :: !rules) l_ids;
left
| QEx ([], f) -> print_lprec f
| QAll ([], f) -> print_lprec f
| _ -> failwith "print_lparse: quantifier in 2QBF; call with parameters" in
rules := ["t(X) | f(X) :- exists(X)"; "t(X) | f(X) :- forall(X)"];
let final = print_lprec (flatten_qbf (nnf phi)) in
let final_subst = Aux.str_subst_all "Xv" "xv" final in
rules := [":- not w"; "f(X) :- w, forall(X)"; "t(X) :- w, forall(X)";
("w :- " ^ final_subst)] @ !rules;
vars := Aux.unique_sorted !vars;
let univs = Aux.unique_sorted universal_vars in
let exists = Aux.sorted_diff !vars univs in
let ufacts = List.rev_map (fun v -> "forall(" ^ (lp_var v) ^ ")") univs in
let exfacts = List.rev_map (fun v -> "exists(" ^ (lp_var v) ^ ")") exists in
let lst l = if l = [] then "" else (String.concat ".\n" l) ^ ".\n" in
(lst (List.rev exfacts)) ^ (lst (List.rev ufacts)) ^ (lst (List.rev !rules))
(* Eliminating quantifiers from QBF formulas. *)
let rec elim_quant_rec phi = match phi.x with
| QVar (v) -> BVar (v)
| QNot (f) -> BNot (elim_quant_rec f)
| QAnd (l) -> BAnd (List.rev_map elim_quant_rec l)
| QOr (l) -> BOr (List.rev_map elim_quant_rec l)
| QEx (vars, qphi) ->
Hashtbl.clear has_vars_mem;
let inside, len = elim_quant_rec qphi, List.length vars in
LOG 1 "EX %i START" len;
let res_raw = elim_ex vars (inside) in
let res = match to_dnf ~tm:3. res_raw with
| None ->
LOG 1 "EX ELIM NO DNF";
res_raw
| Some r ->
LOG 1 "EX ELIM IN DNF";
r in
LOG 1 "EX %i FIN" len;
res
| QAll (vars, qphi) ->
Hashtbl.clear has_vars_mem;
let inside, len = elim_quant_rec qphi, List.length vars in
LOG 1 "ALL %i START" len;
let res_raw = elim_all vars (inside) in
let res = match to_cnf ~tm:3. res_raw with
| None ->
LOG 1 "ALL ELIM NO CNF";
res_raw
| Some r ->
LOG 1 "ALL ELIM IN CNF";
r in
LOG 1 "ALL %i FIN" len;
res
let elim_quant phi =
set_simplification 6;
let res = elim_quant_rec phi in
set_simplification 2;
res
(* Reduce QBF to SAT by taking all possibilities for universal variables *)
let sat_of_qbf phi =
let ids, free_id = Hashtbl.create 7, ref 0 in
let get_id x = try Hashtbl.find ids x with Not_found ->
(Hashtbl.add ids x (!free_id +1); incr free_id; !free_id ) in
(* reduce QBF to SAT (recursive helper)*)
let rec sat_of_qbf_rec phi asgn =
match phi.x with
| QVar v -> (try List.assoc v asgn with Not_found -> (BVar v))
| QAnd l ->
let resl = Aux.unique_sorted (List.filter (fun x -> x <> BAnd []) (
List.rev_map (fun x -> sat_of_qbf_rec x asgn) l)) in
(try List.find (fun x -> x = BOr []) resl with Not_found -> (BAnd resl))
| QOr l ->
let resl = Aux.unique_sorted (List.filter (fun x -> x <> BOr []) (
List.rev_map (fun x -> sat_of_qbf_rec x asgn) l)) in
(try List.find (fun x -> x = BAnd []) resl with Not_found -> (BOr resl))
| QNot f ->
let res = sat_of_qbf_rec f asgn in
if res = BAnd [] then BOr []
else if res = BOr [] then BAnd []
else BNot res
| QEx (var::vl, f) ->
sat_of_qbf_rec (cEx (vl, f)) ((var, BVar (get_id (var, asgn)))::asgn)
| QEx ([], f) -> (sat_of_qbf_rec f asgn)
| QAll (var::tl, f) ->
let redl = [(sat_of_qbf_rec (cAll (tl, f)) ((var, BOr [])::asgn));
(sat_of_qbf_rec (cAll (tl, f)) ((var, BAnd [])::asgn))] in
let resl = Aux.unique_sorted (List.filter (fun x->x <> BAnd []) redl) in
(try (List.find (fun x-> x = BOr []) resl) with Not_found-> (BAnd resl))
| QAll ([], f) -> (sat_of_qbf_rec f asgn)
in (sat_of_qbf_rec phi [])
(* Print a QBF formula in qdimacs format. *)
let print_qdimacs ?(negate=false) qbf =
let fv = free_vars qbf in
match qbf.x with
| QAll (vs, phi) ->
let il sep l = String.concat sep (List.map string_of_int l) in
LOG 1 "all-vars %s" (il ", " vs);
let bphi = sat_of_qbf phi in
LOG 1 "bphi done";
let bphi = if negate then to_nnf ~neg:true bphi else bphi in
let mvs = if vs = [] then 0 else List.fold_left max (List.hd vs) vs in
let sep, cnf = cnf_of_bool_formula ~use_pg:true ~setmax:mvs bphi in
let maxvar cl = List.fold_left (fun acc b -> max acc (abs b)) 0 cl in
let mvar = List.fold_left (fun acc cl -> max acc (maxvar cl)) 0 cnf in
let dimacs = print_dimacs_str cnf in
let i, len = String.index dimacs '\n', String.length dimacs in
let p, l = String.sub dimacs 0 i, String.sub dimacs (i+1) (len-i-1) in
let quant kind vars = if vars = [] then "" else
kind ^ " " ^ (il " " vars) ^ " 0\n" in
if negate then
p ^ "\n" ^ (quant "a" fv) ^ (quant "e"
(vs @ (Aux.range ~from:sep (mvar+1)))) ^ l
else
p ^ "\n" ^ (quant "e" fv) ^ (quant "a" vs) ^
(quant "e" (Aux.range ~from:sep (mvar+1))) ^ l
| _ -> failwith "nested qbf -> qdimacs not supported yet" (* FIXME!!!TODO *)
(* Variable ordering heuristiv called FORCE, a center-of-gravity positioning
based simulation of MINCE, from the paper by Aloul, Markov and Sakallah. *)
let force_order qbf =
let rec qbf_lit_iter f phi = match phi.x with
| QVar i -> f i
| QOr l | QAnd l -> List.iter (qbf_lit_iter f) l
| QNot x | QEx (_, x) | QAll (_, x) -> qbf_lit_iter f x in
let maxvar = ref 1 in
qbf_lit_iter (fun i -> maxvar := max i !maxvar) qbf;
(* Variable frequency array. *)
let freq_array = Array.make (!maxvar+1) 0 in
let incr_var_stat v = freq_array.(abs v) <- freq_array.(abs v) + 1 in
qbf_lit_iter incr_var_stat qbf;
(* Maximal and minimal position, span, total position sum and size. *)
let rec max_min_span_sum_size pos phi = match phi.x with
| QVar v -> (pos.(abs v), pos.(abs v), 0, pos.(abs v), 1)
| QNot f | QEx (_, f) | QAll (_, f) -> max_min_span_sum_size pos f
| QAnd fl | QOr fl ->
let (mi, ma, sp, su, si) = List.fold_left (fun (mi, ma, sp, su, si) f ->
let (fmi, fma, fsp, fsu, fsi) = max_min_span_sum_size pos f in
(min mi fmi, max ma fma, sp + fsp, su + fsu, si + fsi))
(!maxvar, 0, 0, 0, 0) fl in
(mi, ma, sp + ma - mi, su, si) in
(* Iterate f on a qbf formula. *)
let rec qbf_iter f phi = match phi.x with
| QVar _ -> f phi | QNot x | QEx (_, x) | QAll (_, x) -> qbf_iter f x; f phi
| QOr l | QAnd l -> List.iter (qbf_iter f) l; f phi in
(* Create variable position array from comparison function. *)
let pos_of_cmp cmp =
let vars = Aux.range ~from:1 (!maxvar + 1) in
let vars = Array.of_list (List.sort cmp vars) in
let positions = Array.make (!maxvar+1) 0 in
Array.iteri (fun i v -> positions.(v) <- i) vars;
positions in
(* New positions of variables. *)
let newpos pos =
let fpos = Array.make (!maxvar+1) 0. in
let incr f =
let (_, _, _, pos_sum, size) = max_min_span_sum_size pos f in
let cog = (float pos_sum) /. (float size) in
qbf_lit_iter (fun l -> fpos.(abs l) <- fpos.(abs l) +. cog) f in
qbf_iter incr qbf;
let score v = fpos.(v) /. ( (float freq_array.(v)) ** 1. ) in
let cmp v1 v2 = let s1, s2 = score v1, score v2 in
if s1 > s2 then 1 else if s2 > s1 then -1 else 0 in
pos_of_cmp cmp in
(* Reorder positions until span decreases, but not more than maxiter times. *)
let maxiter = 12 in
let span pos = let (_, _, s, _, _) = max_min_span_sum_size pos qbf in s in
let rec minimize_span n pos =
let npos = newpos pos in
let (s, ns) = span pos, span npos in
LOG 1 "spans %i %i" s ns;
if ns < s && n < maxiter then minimize_span (n+1) npos else pos in
let pos = minimize_span 0 (pos_of_cmp (fun v1 v2 ->
freq_array.(v2) - freq_array.(v1))) in
Array.mapi (fun v p -> 2 * !maxvar (* + 0 * freq_array.(v) *) - p) pos