[r1813]: trunk / Toss / Solver / Structure.ml  Maximize  Restore  History

Download this file

1432 lines (1285 with data), 57.9 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
(* Representing Structures *)
(* Default increment for building boards. *)
let cBOARD_DX = 15.0
let cBOARD_DY = -15.0
(* ------------------------- TYPE DEFINITIONS -------------------------- *)
module IntMap = Map.Make (* Maps from int to 'alpha *)
(struct type t = int let compare x y = x - y end)
module FloatMap = Map.Make (* Maps from float to 'alpha *)
(struct type t = float
let compare x y = let d = x -. y in
if d > 0. then 1 else if d < 0. then -1 else 0 end)
module StringMap = Map.Make (* Maps from string to 'alpha *)
(struct type t = string let compare = String.compare end)
module Elems = Set.Make
(struct type t = int let compare x y = x - y end)
let add_elems nes es =
List.fold_left (fun es ne -> Elems.add ne es) es nes
let elems_of_list nes =
add_elems nes Elems.empty
module Tuples = Set.Make
(struct type t = int array let compare = Pervasives.compare end)
type tuple = Tuples.elt
let add_tuples nes es =
List.fold_left (fun es ne -> Tuples.add ne es) es nes
let tuples_of_list nes =
add_tuples nes Tuples.empty
module TIntMap = struct
type t = Tuples.t array
let empty = Array.make 4 Tuples.empty
let is_empty a =
let res = ref true in
Array.iter (fun t -> if not (Tuples.is_empty t) then res := false) a;
!res
let find i a = if i < 0 || i+1 > Array.length a then Tuples.empty else a.(i)
let add i tuples a =
let l = Array.length a in
if i < l then let b = Array.copy a in b.(i) <- tuples; b else
let b = Array.make (max (i-l+1) l) Tuples.empty in
let c = Array.append a b in c.(i) <- tuples; c
let remove i a =
if i < 0 || i+1 > Array.length a || Tuples.is_empty a.(i) then a else
let b = Array.copy a in b.(i) <- Tuples.empty; b
end
type structure = {
rel_signature : int StringMap.t ;
elements : Elems.t ;
constants : (string * int) list ;
relations : Tuples.t StringMap.t ;
functions : (float IntMap.t) StringMap.t ;
fun_vals : (int list FloatMap.t) StringMap.t ;
models : (structure IntMap.t) StringMap.t ;
incidence : (TIntMap.t) StringMap.t ;
names : int StringMap.t ;
inv_names : string IntMap.t ;
}
(* Make sure we use the same order on elements in all modules. *)
let compare_elems x y = x - y
let compare s1 s2 =
if s1 == s2 then 0 else
let c = StringMap.compare Tuples.compare s1.relations s2.relations in
if c <> 0 then c else
let d = Elems.compare s1.elements s2.elements in
if d <> 0 then d else
StringMap.compare (IntMap.compare Pervasives.compare)
s1.functions s2.functions
let equal s1 s2 = (compare s1 s2 = 0)
let elements s = Elems.elements s.elements
let elems s = s.elements
let constants s = s.constants
let elem_nbr s el = StringMap.find el s.names
let elem_name s e = IntMap.find e s.inv_names
let nbr_elems s = Elems.cardinal s.elements
let names s = s.names
let inv_names s = s.inv_names
let replace_names s nms inms = { s with names = nms; inv_names = inms }
let functions s = s.functions
let relations s = s.relations
(* ----------------------- BASIC HELPER FUNCTIONS --------------------------- *)
(* Number of tuples in a relation. *)
let rel_size struc rel =
try
Tuples.cardinal (StringMap.find rel struc.relations)
with Not_found -> 0
(* Reverse a map: make a string IntMap from an int StringMap. *)
let rev_string_to_int_map map =
StringMap.fold (fun n e m -> IntMap.add e n m) map IntMap.empty
(* Reverse a map: make an int StringMap from a string IntMap. *)
let rev_int_to_string_map map =
IntMap.fold (fun n e m -> StringMap.add e n m) map StringMap.empty
(* Return the empty structure. *)
let empty_structure () = {
elements = Elems.empty ;
constants = [] ;
relations = StringMap.empty ;
functions = StringMap.empty ;
fun_vals = StringMap.empty ;
models = StringMap.empty ;
incidence = StringMap.empty ;
names = StringMap.empty ;
inv_names = IntMap.empty ;
rel_signature = StringMap.empty ;
}
let rel_signature struc =
StringMap.fold (fun r ar si -> (r,ar)::si)
struc.rel_signature []
let rel_sizes struc =
StringMap.fold (fun r tups si -> (r,Tuples.cardinal tups)::si)
struc.relations []
(* Return the list of relation tuples incident to an element [e] in [struc]. *)
let incident struc e =
let acc_incident rname inc_map acc =
let tps = TIntMap.find e inc_map in
if Tuples.is_empty tps then acc else (rname, Tuples.elements tps) :: acc in
StringMap.fold acc_incident struc.incidence []
(* Check if a relation holds for a tuple. *)
let check_rel struc rel tp =
try
let tups = StringMap.find rel struc.relations in
Tuples.mem tp tups
with Not_found -> false
(* Return the value of function [f] on [e] in [struc]. *)
let fun_val struc f e =
let f_vals = StringMap.find f struc.functions in
IntMap.find e f_vals
(* Return the elements on which function [f] has value [x] in [struc]. *)
let elems_with_val struc f x =
let fvals = StringMap.find f struc.fun_vals in
try FloatMap.find x fvals with Not_found -> []
(* Return the model assigned by [f] to [e] in [struc]. *)
let model_val struc f e =
let f_vals = StringMap.find f struc.models in
IntMap.find e f_vals
(* Return the list of functions. *)
let f_signature struc =
StringMap.fold (fun f _ acc -> f :: acc) struc.functions []
(* Find a relation in a model. *)
let rel_graph relname model =
try StringMap.find relname model.relations
with Not_found -> Tuples.empty
(* Incidences of a relation in a model. *)
let rel_incidence relname model =
try StringMap.find relname model.incidence with Not_found -> TIntMap.empty
(* ---------- ADDING ELEMENTS POSSIBLY WITH HASHED STRING NAMES ---------- *)
(* Nonexisting elements or relations, signature mismatch, etc. *)
exception Structure_mismatch of string
(* Add element [e] to [struc] if it is not yet there. Return new structure. *)
let add_elem struc ?name e =
if e <= 0 then raise (
Structure_mismatch
"only positive integers allowed as elements")
else
{ struc with elements = Elems.add e struc.elements;
names = (match name with None -> struc.names
| Some n ->
if Aux.is_digit n.[0] then raise (Structure_mismatch
"Structure.add_elem: explicit names cannot be digits");
if StringMap.mem n struc.names
&& StringMap.find n struc.names <> e then raise (
Structure_mismatch
("repeating names of elements not allowed (name "^n^")"));
StringMap.add n e struc.names);
inv_names = (match name with None -> struc.inv_names
| Some n ->
IntMap.add e n struc.inv_names) }
(* Add new element to [struc], return the updated structure and the
element. Recall that elements not named explicitly are implicitly
named by their number in decimal. *)
let add_new_elem struc ?name () =
let free_e = if Elems.is_empty struc.elements then 1 else
Elems.max_elt struc.elements + 1 in
(* while StringMap.mem (string_of_int !free_e) names do
free_e := !free_e + 1
done; *)
add_elem struc ?name free_e, free_e
let find_elem struc name =
try StringMap.find name struc.names
with Not_found ->
let e =
try int_of_string name
with Failure _ | Invalid_argument _ -> -1 in
if Elems.mem e struc.elements then e
else raise Not_found
(* Add an element by name, return the updated structure and the
element. Search for an element with the given name in the
structure, and if not found, add new element with this name. *)
let find_or_new_elem struc name =
if StringMap.mem name struc.names
then struc, StringMap.find name struc.names
else
let e =
try int_of_string name
with Failure _ | Invalid_argument _ -> -1 in
if Elems.mem e struc.elements then struc, e
else if e = -1 then add_new_elem struc ~name ()
else {struc with elements = Elems.add e struc.elements}, e
(* --------- ADDING RELATION TUPLES POSSIBLY WITH NAMED ELEMENTS ---------- *)
(* Ensure relation named [rn] exists in [struc], check arity, add the
relation if needed. *)
let add_rel_name rn arity struc =
if StringMap.mem rn struc.relations then
let old_arity = StringMap.find rn struc.rel_signature in
if arity <> old_arity then
raise (Structure_mismatch
(Printf.sprintf
"arity mismatch for %s: expected %d, given %d"
rn old_arity arity));
struc
else
{ struc with
rel_signature = StringMap.add rn arity struc.rel_signature;
relations = StringMap.add rn Tuples.empty struc.relations;
incidence = StringMap.add rn TIntMap.empty struc.incidence; }
let empty_with_signat signat =
List.fold_right (fun (rn,ar) -> add_rel_name rn ar) signat
(empty_structure ())
(* Add empty relation named [rn] to [struc], with given arity,
regardless of whether it already existed. *)
let force_add_rel_name rn arity struc =
{ struc with
rel_signature = StringMap.add rn arity struc.rel_signature;
relations = StringMap.add rn Tuples.empty struc.relations;
incidence = StringMap.add rn TIntMap.empty struc.incidence; }
(* Add tuple [tp] to relation [rn] in structure [struc]. *)
let add_rel struc rn tp =
let new_struc =
Array.fold_left (fun struc e -> add_elem struc e)
(add_rel_name rn (Array.length tp) struc) tp in
let add_to_relmap rmap =
let tps = StringMap.find rn rmap in
StringMap.add rn (Tuples.add tp tps) rmap in
let new_rel = add_to_relmap new_struc.relations in
let add_to_imap imap e =
try
TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
with Not_found ->
TIntMap.add e (Tuples.singleton tp) imap in
let new_incidence_imap =
try
Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
with Not_found ->
Array.fold_left add_to_imap TIntMap.empty tp in
let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
{ new_struc with relations = new_rel ; incidence = new_incidence }
(* Add tuple [tp] to relation [rn] in structure [struc]. *)
let add_rel_named_elems struc rn tp =
let new_struc, tp =
Array.fold_right (fun e (struc, tp) ->
let struc, e = find_or_new_elem struc e in
struc, e::tp) tp
((add_rel_name rn (Array.length tp) struc), []) in
let tp = Array.of_list tp in
let add_to_relmap rmap =
let tps = StringMap.find rn rmap in
StringMap.add rn (Tuples.add tp tps) rmap in
let new_rel = add_to_relmap new_struc.relations in
let add_to_imap imap e =
try
TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
with Not_found ->
TIntMap.add e (Tuples.singleton tp) imap in
let new_incidence_imap =
try
Array.fold_left add_to_imap (StringMap.find rn new_struc.incidence) tp
with Not_found ->
Array.fold_left add_to_imap TIntMap.empty tp in
let new_incidence = StringMap.add rn new_incidence_imap new_struc.incidence in
{ new_struc with relations = new_rel ; incidence = new_incidence }
(* Return a structure with a single relation, over a single tuple, of
different elements. *)
let free_for_rel rel arity =
let tup = Array.init arity (fun i->i+1) in
add_rel (empty_structure ()) rel tup
(* Add tuple [tp] to relation [rn] in structure [struc] without
checking whether it and its elements already exist in the structure
and without checking arity. *)
let unsafe_add_rel struc rn tp =
let new_rel =
let tps = StringMap.find rn struc.relations in
StringMap.add rn (Tuples.add tp tps) struc.relations in
let add_to_imap imap e =
try
TIntMap.add e (Tuples.add tp (TIntMap.find e imap)) imap
with Not_found ->
TIntMap.add e (Tuples.singleton tp) imap in
let new_incidence_imap =
try
Array.fold_left add_to_imap (StringMap.find rn struc.incidence) tp
with Not_found ->
Array.fold_left add_to_imap TIntMap.empty tp in
let new_incidence = StringMap.add rn new_incidence_imap struc.incidence in
{ struc with relations = new_rel ; incidence = new_incidence }
(* Add tuples [tps] to relation [rn] in structure [struc]. *)
let add_rels struc rn tps =
List.fold_left (fun s tp -> add_rel s rn tp) struc tps
(* Add tuples [tps] to relation [rn] in structure [struc] without
checking for elements existence and arity matching. *)
let unsafe_add_rels struc rn tps =
List.fold_left (fun s tp -> unsafe_add_rel s rn tp) struc tps
(* --------- ADDING FUNCTION ASSINGMENTS POSSIBLY TO NAMED ELEMENTS --------- *)
(* Add function assignment [e] -> [x] to function [fn] in structure [struc]. *)
let add_fun struc fn (e, x) =
let new_struc = add_elem struc e in
let new_functions =
try
let assgns = StringMap.find fn new_struc.functions in
StringMap.add fn (IntMap.add e x assgns) new_struc.functions
with Not_found ->
StringMap.add fn (IntMap.add e x IntMap.empty) new_struc.functions in
let new_fun_vals =
try
let fvals = StringMap.find fn new_struc.fun_vals in
let cur_x = try FloatMap.find x fvals with Not_found -> [] in
StringMap.add fn (FloatMap.add x (e::cur_x) fvals) new_struc.fun_vals
with Not_found ->
StringMap.add fn (FloatMap.add x [e] FloatMap.empty) new_struc.fun_vals in
{ new_struc with functions = new_functions ; fun_vals = new_fun_vals }
(* Add function assignments [assgns] to [fn] in structure [struc]. *)
let add_funs struc fn assgns =
List.fold_left (fun s a -> add_fun s fn a) struc assgns
(* Change function [fn] assignment for element [e] to [x] in [struc]. *)
let change_fun_int struc fn e x =
let assgs = StringMap.find fn struc.functions in
let new_functions = StringMap.add fn (IntMap.add e x assgs) struc.functions in
let prev_x = IntMap.find e assgs in
let fvals = StringMap.find fn struc.fun_vals in
let prev_vals = FloatMap.find prev_x fvals in
let cur_vals = try FloatMap.find x fvals with Not_found -> [] in
let new_fvals =
FloatMap.add prev_x (List.filter (fun el -> el <> e) prev_vals) fvals in
let new_fvals = FloatMap.add x cur_vals new_fvals in
let new_fun_vals = StringMap.add fn new_fvals struc.fun_vals in
{ struc with functions = new_functions ; fun_vals = new_fun_vals }
let change_fun struc fn elem x = change_fun_int struc fn (elem_nbr struc elem) x
(* Add model assignment [e] -> [s] to function [fn] in structure [struc].
Assumes [e] is already an element of [struc]. *)
let add_model struc fn (e, s) =
let new_models =
try
let assgns = StringMap.find fn struc.models in
StringMap.add fn (IntMap.add e s assgns) struc.models
with Not_found ->
StringMap.add fn (IntMap.add e s IntMap.empty) struc.models in
{ struc with models = new_models }
let add_models st fn ms = List.fold_left (fun s a -> add_model s fn a) st ms
(* ------------ GLOBAL FUNCTIONS TO CREATE STRUCTURES FROM LISTS ------------ *)
(** Map a function over an array threading an accumulator. *)
let array_fold_map f acc a =
let l = Array.length a in
if l = 0 then acc, [||] else begin
let acc, e = f acc (Array.unsafe_get a 0) in
let prev = ref acc in
let r = Array.create l e in
for i = 1 to l - 1 do
let acc, e = f !prev (Array.unsafe_get a i) in
prev := acc;
Array.unsafe_set r i e
done;
!prev, r
end
(* Add to a named structure elements, relations and functions from the lists. *)
let add_from_lists struc els rels_consts funs =
let rels, csts = ref [], ref [] in
List.iter (function
| Aux.Left r -> rels := r :: !rels
| Aux.Right c -> csts := c :: !csts) rels_consts;
let rels, csts = List.rev !rels, List.rev !csts in
let add_funs s (fn, assgns) =
List.fold_left (fun s (ne, x) ->
let s, e = find_or_new_elem s ne in
add_fun s fn (e, x)) s assgns in
let add_rels s (rn, arity, tps) =
let arity = match arity with
| None ->
if tps = [] then raise (
Structure_mismatch
("Structure.add_from_lists: relation of undetermined arity: " ^ rn))
else Array.length (List.hd tps)
| Some ar -> ar in
let s = add_rel_name rn arity s in
List.fold_left (fun s tp ->
let s, tp = array_fold_map find_or_new_elem s tp in
add_rel s rn tp) s tps in
let add_cst s (c, e) =
let s, e = find_or_new_elem s e in
{ s with constants = Aux.unique_sorted ((c, e) :: s.constants) } in
let add_elem s ne = fst (find_or_new_elem s ne) in
List.fold_left add_funs (List.fold_left add_rels (
List.fold_left add_cst (List.fold_left add_elem struc els) csts) rels) funs
let create_from_lists ?struc els rels funs =
let struc = match struc with
| None -> empty_structure ()
| Some s -> s in
add_from_lists struc els rels funs
let circle_structure rx ry =
create_from_lists ["e"] [Aux.Left ("Circle", None, [[|"e"|]])]
[("rx", [("e", rx)]); ("ry", [("e", ry)]);
("x", [("e", 0.)]); ("y", [("e", 0.)])]
let create_from_lists_position ?struc els rels =
let s = create_from_lists ?struc els rels [] in
let elems = List.sort (fun x y -> x - y) (Elems.elements s.elements) in
let circ = circle_structure (cBOARD_DX /. 3.) (cBOARD_DX /. 3.) in
let shapes = List.map (fun e -> (e, circ)) elems in
let s = add_models s "shape" shapes in
let zero = List.map (fun e -> (e, 0.)) elems in
let (_, next) = List.fold_left (fun (cur, acc) e ->
(cur +. cBOARD_DX, (e, cur) :: acc)) (0., []) elems in
let afuns s (fn, asg) = add_funs s fn asg in
List.fold_left afuns s [("x", next); ("y", zero); ("vx", zero); ("vy", zero)]
let create_from_lists_range start ?struc els rels =
let s = create_from_lists ?struc els rels [] in
let elems = List.sort (fun x y -> x - y) (Elems.elements s.elements) in
let circ = circle_structure (1. /. 3.) (1. /. 3.) in
let shapes = List.map (fun e -> (e, circ)) elems in
let s = add_models s "shape" shapes in
let zero = List.map (fun e -> (e, 0.)) elems in
let (_, nextnbr) = List.fold_left (fun (cur, acc) e ->
(cur +. 1., (e, cur) :: acc)) (start, []) elems in
let (_, nextx) = List.fold_left (fun (cur, acc) e ->
(cur +. cBOARD_DX, (e, cur) :: acc)) (0., []) elems in
let afuns s (fn, asg) = add_funs s fn asg in
List.fold_left afuns s [("x", nextx); ("y", zero); ("nbr", nextnbr);]
(* ---------- REMOVING RELATION TUPLES AND ELEMENTS FROM A STRUCTURE -------- *)
(* Remove the tuple [tp] from relation [rn] in structure [struc]. *)
let del_rel struc rn tp =
let del_rmap rmap =
try StringMap.add rn (Tuples.remove tp (StringMap.find rn rmap)) rmap
with Not_found -> rmap in
let new_rel = del_rmap struc.relations in
let del_imap imap e =
try TIntMap.add e (Tuples.remove tp (TIntMap.find e imap)) imap
with Not_found -> imap in
let new_incidence =
let imap=Array.fold_left del_imap (StringMap.find rn struc.incidence) tp in
StringMap.add rn imap struc.incidence in
{ struc with relations = new_rel ; incidence = new_incidence }
(* Remove the tuples [tps] from relation [rn] in structure [struc]. *)
let del_rels struc rn tps =
List.fold_left (fun s tp -> del_rel s rn tp) struc tps
(* Remove the given relation [rn] in [struc]. *)
let clear_rel remove_from_sig struc rn =
let new_rels = StringMap.remove rn struc.relations in
let new_inc = StringMap.remove rn struc.incidence in
let new_rel_sig =
if remove_from_sig then
StringMap.remove rn struc.rel_signature
else struc.rel_signature in
{ struc with relations = new_rels ; incidence = new_inc ;
rel_signature = new_rel_sig }
(* Remove all relations that meet predicate [p] in [struc]. *)
let clear_rels ?(remove_from_sig=true) struc p =
let p_rels = ref [] in
let _ = StringMap.iter (fun r _ -> if p r then p_rels := r :: !p_rels)
struc.relations in
List.fold_left (clear_rel remove_from_sig) struc !p_rels
(* {struc with
relations = StringMap.mapi (fun rel tups ->
if p rel then Tuples.empty else tups) struc.relations;
incidence = StringMap.mapi (fun rel inctups ->
if p rel then IntMap.empty else inctups) struc.incidence} *)
(* Remove the element [e] and all incident relation tuples from [struc]. *)
let del_elem struc e =
let rel_tuples = incident struc e in
let del_rels_struc =
List.fold_left (fun s (rn, tps) -> del_rels s rn tps) struc rel_tuples in
let del_fun fmap = IntMap.remove e fmap in
let del_elem_add_fval x els map =
FloatMap.add x (List.filter (fun el -> el <> e) els) map in
let del_fval vmap = FloatMap.fold del_elem_add_fval vmap FloatMap.empty in
{ del_rels_struc with elements = Elems.remove e del_rels_struc.elements ;
functions = StringMap.map del_fun del_rels_struc.functions ;
fun_vals = StringMap.map del_fval del_rels_struc.fun_vals }
(* Remove the elements [es] and all incident relation tuples from
[struc]; return the deleted relation tuples. *)
let del_elems struc es =
let rel_tuples =
Aux.map_reduce (fun x->x) List.rev_append []
(Aux.concat_map (incident struc) es) in
let del_rels_struc =
List.fold_left (fun s (rn, tps) -> del_rels s rn tps) struc rel_tuples in
let del_fun fmap =
List.fold_left (fun fmap e -> IntMap.remove e fmap) fmap es in
let del_elem_add_fval x els map =
FloatMap.add x (List.filter (fun el -> not (List.mem el es)) els) map in
let del_fval vmap = FloatMap.fold del_elem_add_fval vmap FloatMap.empty in
{ del_rels_struc with elements =
List.fold_left (fun els e -> Elems.remove e els)
del_rels_struc.elements es;
functions = StringMap.map del_fun del_rels_struc.functions ;
fun_vals = StringMap.map del_fval del_rels_struc.fun_vals },
rel_tuples
(* Remove the elements that are not incident to any relation (and have
no defined properties, unless [ignore_funs] is given). *)
let gc_elems ?(ignore_funs=false) struc =
let all_elems = Elems.elements struc.elements in
let gc_elems =
List.filter
(fun e -> StringMap.fold (fun _ incmap empty ->
empty && try Tuples.is_empty (TIntMap.find e incmap)
with Not_found -> true) struc.incidence true) all_elems in
let gc_elems =
if ignore_funs then gc_elems
else List.filter (fun e -> StringMap.fold (fun _ assgns empty ->
empty && not (IntMap.mem e assgns)) struc.functions true)
gc_elems in
{struc with elements =
List.fold_left (fun els e -> Elems.remove e els)
struc.elements gc_elems}
(* Delete function assignment to element [e] from function [fn] in structure
[struc]. *)
let del_fun struc fn e =
try
let assgns = StringMap.find fn struc.functions in
let prev_x = IntMap.find e assgns in
let new_functions =
StringMap.add fn (IntMap.remove e assgns) struc.functions in
let fvals = StringMap.find fn struc.fun_vals in
let prev_vals_x = FloatMap.find prev_x fvals in
let new_vals_x = List.filter (fun el -> el <> e) prev_vals_x in
let new_fvals = FloatMap.add prev_x new_vals_x fvals in
let new_fun_vals = StringMap.add fn new_fvals struc.fun_vals in
{ struc with functions = new_functions ; fun_vals = new_fun_vals }
with Not_found -> struc
(* Remove the given function from [struc]. *)
let clear_fun struc fn =
{ struc with functions = StringMap.remove fn struc.functions ;
fun_vals = StringMap.remove fn struc.fun_vals }
(* Remove names from structure. *)
let clear_names struc =
{ struc with names = StringMap.empty ; inv_names = IntMap.empty }
(* --- Structure operations by TRS --- *)
let trs_set_struc s = function
| ("addrel", te_rel, te_arglist) ->
let rname = Coding.decode_string ~normalized:true te_rel in
let args = Coding.decode_list ~normalized:true
Coding.term_to_string te_arglist in
let (struc, args) = List.fold_left (fun (st, a) e ->
let (s1, i) = find_or_new_elem st e in (s1, i :: a)) (s, []) args in
add_rel struc rname (Array.of_list (List.rev args))
| (str, te, arg) when String.length str > 3 && String.sub str 0 3 = "fun" ->
let fname = String.sub str 3 ((String.length str) - 3) in
let (struc, i) = find_or_new_elem s
(Coding.term_to_string te) in
let v = Coding.decode_bit_list ~normalized:true arg in
add_fun struc fname (i, float v)
| _-> raise (Coding.DECODE "Structure.trs_set_struc not a struc update set")
let struc_from_trs str =
let (o, trs, _) = TRS.run_shell_str str in
let svals = TRS.set_vals_of_sys trs in
(o, List.fold_left trs_set_struc (empty_structure ()) svals)
(* ------------------------ PRINTING STRUCTURES ----------------------------- *)
(* Helper function: omit k first characters of s. *)
let omit k s =
let l = String.length s in if l > k then String.sub s k (l - k) else ""
(* Print the element [e] as string. *)
let elem_str struc e = try IntMap.find e struc.inv_names
with Not_found -> string_of_int e
(* Print the tuple [tp] as string. *)
let tuple_str ?(with_paren=true) struc tp =
if Array.length tp = 1 && not with_paren then elem_str struc tp.(0) else
"(" ^ (String.concat ", "
(Array.to_list (Array.map (elem_str struc) tp))) ^ ")"
(** {2 Printing of rectangular boards.}
Elements named as in algebraic chess notation: "CR" where C is
column number specified by letter "a..zA..Z" (which provide a
range of 52), and R is a decimal row number (without range limit),
are printed as (and parsed from) boards (grids). Not all elements
need to be present. Positions are represented by rectangular
regions of three consecutive characters on both of two consecutive
lines, but the tab characters "\t" at the beginning of line are
ignored and can serve for indentation. The endline character "\n"
or pair "\r\n" represent advancing to next line (from upper line
to lower line or from bottom line to upper line of next row),
empty lines are ignored. The row and column relations are provided
explicitly or default to "R" and "C". The vertical and horizontal
increments are provided explicitly or default to
{!cBOARD_STEP}. The velocities are assumed 0 (unless provided
explicitly separately). By writing "PQR.." we mean that "PQR" are any
characters and there is exactly one predicate name starting with
"PQR" (trailing spaces and dots truncated) in the signature so
far and we represent this predicate as "PQR..". The following
syntax is allowed in board fields:
- "* ", "** ", "***", "*.." when the other line is " " or has
this form also: nonexisting element (position
without an element, a hole in a board between separate boards /
islands)
- " ", ". ", ".. " and "..." represent an element without
additional predicates
- "? ", "?. ", "?.." represents a special predicate "_any_"
- "+PQ", when there is !1 sigpref "PQ", represents "_new_PQ.. and PQ.."
- "-PQ" represents "_del_PQ.."
- "PQ?" represents "PQ.. and _any_"
- "?PQ" represents "_opt_PQ.."
- "#PQ" represents "_diffthan_PQ.."
- "PQ#" represents "_diffthan_PQ.. and _any_"
- "PQR" represents "PQR.."
For the semantics of these special relations, see
{!DiscreteRule.compile_rule}.
Additionally for printing, there are three styles of using dots: "Go",
"Checkers" and "Plain". "Go" is by default used for 9x9 and 19x19
boards, and "Checkers" is by default used for 8x8 boards. For
clarity, the board is indented by a single tab. Rules for printing:
- the upper line is by default: " " in "Plain" or when on
nonexisting element field or when in "Go" and on firt row, ". "
in "Go" (otherwise), "..." in "Checkers" when the sum of column
and row indices is even (otherwise " ")
- the lower line is by default: ". " in "Plain" or in "Go" when
on last (uppermost) column, " " in "Checkers" when the sum of
column and row indices is odd, "..." in "Go" (otherwise) and in
"Checkers" (otherwise)
- when there is no element in a position, the upper line is
changed to " " and the lower line to "* "
- the predicates on an element longer than one character are
expressed using two characters for relations with unique two
character prefix, and using three characters for unique three
character prefix (but 3 chars only for cases without
modifiers), and the parsing/printing rules, and written over the
default lower, then upper, line, remaining predicates are stored
to print separately
- the row and column relations are determined such that they hold
for all (existing) elements as required (they need not be
distinct), if such relations cannot be found printing the elements
as a board is abandoned
- the initial position, and the horizontal and vertical position
increments are determined from an upper-leftmost existing triangle
of neighbor elements, typically elements "a1", "b1" and
"a2"; for elements that violate the determined increment, the
position is set explicitly later
- if the spanning rectangle would cover more than 3/4 nonexisting
elements, printing as a board is abandoned.
*)
module StringSet = Set.Make
(struct type t = string let compare = String.compare end)
(* Ignore special relations. *)
let find_unique all_preds =
let all_preds = List.filter (fun r -> r.[0] <> '_') all_preds in
(* build a fixed depth trie *)
let uniq1, more_preds =
List.partition (fun r -> String.length r = 1) all_preds in
let uniq1 = List.map (fun p -> p,p) uniq1 in
let trie1 = List.fold_left (fun trie pred ->
if List.mem_assoc pred.[0] trie then
let preds, trie = Aux.pop_assoc pred.[0] trie in
(pred.[0], pred::preds)::trie
else (pred.[0], [pred])::trie
) [] more_preds in
let trie2 = Aux.concat_map (fun (key, preds) ->
let trie2 =
List.fold_left (fun trie pred ->
if List.mem_assoc pred.[1] trie then
let preds, trie = Aux.pop_assoc pred.[1] trie in
(pred.[1], pred::preds)::trie
else (pred.[1], [pred])::trie
) [] preds in
List.map (fun (key2, preds) ->
Char.escaped key ^ Char.escaped key2, preds) trie2
) trie1 in
let uniq2, trie2 = Aux.partition_map
(function (k,[pred]) -> Aux.Left (pred, k)
| subt -> Aux.Right subt) trie2 in
(* deliberately losing two-char long predicates that are not
prefix-unique: they might be confusing *)
let trie2 = List.map
(fun (k, preds) -> k, List.filter
(fun pred -> String.length pred > 2) preds) trie2 in
let trie3 = Aux.concat_map (fun (key, preds) ->
let trie3 =
List.fold_left (fun trie pred ->
if List.mem_assoc pred.[2] trie then
let preds, trie = Aux.pop_assoc pred.[2] trie in
(pred.[2], pred::preds)::trie
else (pred.[2], [pred])::trie
) [] preds in
List.map (fun (key2, preds) ->
key ^ Char.escaped key2, preds) trie3
) trie2 in
let uniq3 = Aux.map_some
(function (k,[pred]) -> Some (pred,k) | _ -> None) trie3 in
uniq1, uniq2, uniq3
(* [uniq_short] and [uniq_long] don't contain special rels. *)
let printing_logic uniq_short uniq_long up_line lo_line predicates =
let is_opt r = String.length r > 5 && String.sub r 0 5 = "_opt_" in
let is_diffthan r =
String.length r > 10 && String.sub r 0 10 = "_diffthan_" in
let is_new r = String.length r > 5 && String.sub r 0 5 = "_new_" in
let is_del r = String.length r > 5 && String.sub r 0 5 = "_del_" in
let use_any = List.mem "_any_" predicates in
let spec_uniq rels =
List.filter (fun r -> List.mem_assoc r uniq_short) rels in
let opts = List.filter is_opt predicates in
let opts =
List.map (fun r -> String.sub r 5 (String.length r - 5)) opts in
let opts = spec_uniq opts in
let diffthans = List.filter is_diffthan predicates in
let diffthans =
List.map (fun r -> String.sub r 10 (String.length r - 10))
diffthans in
let diffthans = spec_uniq diffthans in
let news = List.filter is_new predicates in
let news =
List.map (fun r -> String.sub r 5 (String.length r - 5)) news in
let news = spec_uniq news in
let dels = List.filter is_del predicates in
let dels =
List.map (fun r -> String.sub r 5 (String.length r - 5)) dels in
let dels = spec_uniq dels in
let short_preds =
List.filter (fun r ->
List.mem_assoc r uniq_short && not (List.mem r news))
predicates in
let long_preds =
List.filter (fun r ->
List.mem_assoc r uniq_long && not (List.mem r news)
&& not (List.mem r short_preds))
predicates in
let used1, rep1, short_preds, diffthans, opts, news, dels, long_preds =
if use_any then
match short_preds with
| p::tl -> [p; "_any_"], List.assoc p uniq_short ^ "?",
tl, diffthans, [], news, dels, long_preds
| [] -> match diffthans with
| p::tl -> ["_diffthan_"^p; "_any_"],
List.assoc p uniq_short ^ "#",
[], tl, [], news, dels, long_preds
| [] ->
["_any_"], "?", [], [], [], news, dels, long_preds
else
match diffthans with
| p::tl -> ["_diffthan_"^p], "#" ^ List.assoc p uniq_short,
short_preds, tl, opts, news, dels, long_preds
| [] -> match opts with
| p::tl -> ["_opt_"^p], "?" ^ List.assoc p uniq_short,
short_preds, [], tl, news, dels, long_preds
| [] -> match news with
| p::tl -> ["_new_"^p;p], "+" ^ List.assoc p uniq_short,
short_preds, [], [], tl, dels, long_preds
| [] -> match dels with
| p::tl -> ["_del_"^p], "-" ^ List.assoc p uniq_short,
short_preds, [], [], [], tl, long_preds
| [] -> match short_preds with
| p::tl -> [p], List.assoc p uniq_short,
tl, [], [], [], [], long_preds
| [] -> match long_preds with
| p::tl -> [p], List.assoc p uniq_long,
[], [], [], [], [], tl
| [] -> [], "", [], [], [], [], [], [] in
let used2, rep2, short_preds, diffthans, opts, news, dels, long_preds =
match diffthans with
| p::tl -> ["_diffthan_"^p], "#" ^ List.assoc p uniq_short,
short_preds, tl, opts, news, dels, long_preds
| [] -> match opts with
| p::tl -> ["_opt_"^p], "?" ^ List.assoc p uniq_short,
short_preds, [], tl, news, dels, long_preds
| [] -> match news with
| p::tl -> ["_new_"^p;p], "+" ^ List.assoc p uniq_short,
short_preds, [], [], tl, dels, long_preds
| [] -> match dels with
| p::tl -> ["_del_"^p], "-" ^ List.assoc p uniq_short,
short_preds, [], [], [], tl, long_preds
| [] -> match short_preds with
| p::tl -> [p], List.assoc p uniq_short,
tl, [], [], [], [], long_preds
| [] -> match long_preds with
| p::tl -> [p], List.assoc p uniq_long,
[], [], [], [], [], tl
| [] -> [], "", [], [], [], [], [], [] in
String.blit rep1 0 lo_line 0 (String.length rep1);
String.blit rep2 0 up_line 0 (String.length rep2);
used1 @ used2
(** Print a rectangular board from a structure if the structure
contains it. Return the board specification string with the
inferred parameters (row / column relations and position
increments), and the structure with information already extracted
into the string removed. *)
let rec board_to_string struc =
LOG 2 "printing board";
let col_index =
"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ" in
(* find the spanning rectangle *)
let c_max, r_max =
StringMap.fold (fun name _ (c_max, r_max as acc) ->
try
if String.length name > 1 && Aux.is_letter name.[0] &&
Aux.is_digit name.[1] && name.[1] <> '0' then
let c_cur = String.index col_index name.[0] + 1 in
let r_cur = int_of_string
(String.sub name 1 (String.length name - 1)) in
max c_cur c_max, max r_cur r_max
else acc
with Failure "int_of_string" -> acc
) struc.names (0,0) in
(* find the board elements *)
let board_els =
Array.make_matrix c_max r_max (-1) in
let field_count = ref 0 in
StringMap.iter (fun name elem ->
try
if String.length name > 1 && Aux.is_letter name.[0] &&
Aux.is_digit name.[1] && name.[1] <> '0' then
let c_cur = String.index col_index name.[0] + 1 in
let r_cur = int_of_string
(String.sub name 1 (String.length name - 1)) in
board_els.(c_cur-1).(r_cur-1) <- elem;
incr field_count
with Failure "int_of_string" -> ()
) struc.names;
if c_max = 0 || r_max = 0 ||
float_of_int !field_count < 0.25 *. float_of_int (c_max*r_max)
then "", struc
else
(* find the row/column relations *)
let binary_rels =
StringMap.fold (fun rel arity binary ->
if arity = 2 then rel:: binary else binary)
struc.rel_signature [] in
let col_rels = ref binary_rels
and row_rels = ref binary_rels in
for x=0 to c_max-1 do
for y=0 to r_max-1 do
if x>0 && board_els.(x).(y) <> -1 && board_els.(x-1).(y) <> -1
then
row_rels :=
List.filter (fun rel ->
check_rel struc rel
[|board_els.(x-1).(y); board_els.(x).(y)|]) !row_rels;
if y>0 && board_els.(x).(y) <> -1 && board_els.(x).(y-1) <> -1
then
col_rels :=
List.filter (fun rel ->
check_rel struc rel
[|board_els.(x).(y-1); board_els.(x).(y)|]) !col_rels;
done
done;
if !col_rels = [] || !row_rels = [] then "", struc
else
let col_rel =
if List.mem "C" !col_rels then "C" else List.hd !col_rels
and row_rel =
if List.mem "R" !row_rels then "R" else List.hd !row_rels in
(* find the initial position and position increments *)
let ini_x = ref 0 and ini_y = ref 0 in
while !ini_x < c_max-1 && !ini_y < r_max-1 &&
(board_els.(!ini_x).(!ini_y) = -1 ||
board_els.(!ini_x+1).(!ini_y) = -1 ||
board_els.(!ini_x).(!ini_y+1) = -1) do
incr ini_x;
if !ini_x >= c_max-1 then (ini_x := 0; incr ini_y);
done;
let orig_el = board_els.(!ini_x).(!ini_y)
and right_el =
if !ini_x+1 >= c_max then -1
else board_els.(!ini_x+1).(!ini_y)
and upper_el =
if !ini_y+1 >= r_max then -1
else board_els.(!ini_x).(!ini_y+1) in
if (try
ignore (fun_val struc "x" orig_el);
ignore (fun_val struc "y" orig_el);
if right_el <> -1 then (
ignore (fun_val struc "x" right_el);
ignore (fun_val struc "y" right_el));
if upper_el <> -1 then (
ignore (fun_val struc "x" upper_el);
ignore (fun_val struc "y" upper_el));
false
with Not_found -> true) then "", struc
else
let pos_x = fun_val struc "x" orig_el
and pos_y = fun_val struc "y" orig_el in
let pos_xdx =
if right_el = -1 then pos_x +. cBOARD_DX
else fun_val struc "x" right_el
and pos_ydy =
if upper_el = -1 then pos_y +. cBOARD_DY
else fun_val struc "y" upper_el in
let pos_dx = pos_xdx -. pos_x
and pos_dy = pos_ydy -. pos_y in
let init_pos_x =
if !ini_x = 0 then pos_x
else pos_x -. float_of_int !ini_x *. pos_dx
and init_pos_y =
if !ini_y = 0 then pos_y
else pos_y -. float_of_int !ini_y *. pos_dy in
(* board *)
let kind =
if c_max = 8 && r_max = 8 then `Checkers
else if c_max = 9 && r_max = 9 || c_max = 19 && r_max = 19
then `Go else `Plain in
let board = String.make (c_max*r_max*6 + r_max*2*2) ' ' in
for i=1 to r_max*2 do
board.[(i-1)*c_max*3+(i-1)*2] <- '\t';
board.[i*c_max*3+i*2-1] <- '\n'
done;
(* fill the fields *)
let all_predicates =
StringMap.fold (fun rel arity predicates ->
if arity = 1 then rel::predicates else predicates)
struc.rel_signature [] in
LOG 2 "board_to_string: all_predicates=%s"
(String.concat ", " all_predicates);
let uniq1, uniq2, uniq3 =
find_unique all_predicates in
let uniq_long = uniq1 @ uniq2 @ uniq3 in
let uniq_short = uniq1 @ uniq2 in
LOG 2 "board_to_string: uniq_long=%s"
(String.concat ", " (List.map fst uniq_long));
let ret = ref struc in
for c=1 to c_max do
for r=1 to r_max do
(* let elname =
Char.escaped col_index.[c-1] ^ string_of_int r in *)
let elem = board_els.(c-1).(r-1) in
let upper_left =
(* +2 for endline and tab, +1 for last tab *)
c_max*3*(r_max - r)*2 + 2*(r_max - r)*2 + (c-1)*3 + 1 in
let lower_left =
c_max*3*(r_max - r)*2 + c_max*3 + 2*(r_max - r)*2 + (c-1)*3 + 3 in
if elem = -1 then board.[lower_left] <- '*'
else begin
(* collect the predicates *)
let tup = [|elem|] in
let predicates = List.filter
(fun pred ->
let tmap =
try StringMap.find pred !ret.relations
with Not_found -> Tuples.empty in
Tuples.mem tup tmap &&
let rmap =
try StringMap.find pred !ret.incidence
with Not_found -> TIntMap.empty in
not (Tuples.is_empty (
try TIntMap.find elem rmap
with Not_found -> Tuples.empty)))
all_predicates in
let up_line = String.make 3 ' '
and lo_line = String.make 3 ' ' in
if kind = `Plain then
lo_line.[0] <- '.'
else if kind = `Checkers && (c+r) mod 2 = 0 then (
String.blit "..." 0 up_line 0 3;
String.blit "..." 0 lo_line 0 3;
) else if kind = `Go then (
if r = r_max && c = c_max then
lo_line.[0] <- '.'
else if r = r_max then
String.blit "..." 0 lo_line 0 3
else if c = c_max then (
up_line.[0] <- '.';
lo_line.[0] <- '.';
) else (
up_line.[0] <- '.';
String.blit "..." 0 lo_line 0 3));
(* special relations with syntactic support have
precedence *)
let used_preds =
printing_logic uniq_short uniq_long up_line lo_line
predicates in
String.blit up_line 0 board upper_left 3;
String.blit lo_line 0 board lower_left 3;
if c > 1 && board_els.(c-2).(r-1) <> -1 then
ret := del_rel !ret row_rel
[|board_els.(c-2).(r-1); elem|];
if r > 1 && board_els.(c-1).(r-2) <> -1 then
ret := del_rel !ret col_rel
[|board_els.(c-1).(r-2); elem|];
List.iter (fun pred ->
ret := del_rel !ret pred tup) used_preds;
let pos_x =
init_pos_x +. float_of_int (c - 1) *. pos_dx in
let pos_y =
init_pos_y +. float_of_int (r - 1) *. pos_dy in
if (try fun_val !ret "x" elem = pos_x
with Not_found -> false)
then ret := del_fun !ret "x" elem;
if (try fun_val !ret "y" elem = pos_y
with Not_found -> false)
then ret := del_fun !ret "y" elem;
if (try fun_val !ret "vx" elem = 0.0
with Not_found -> false)
then ret := del_fun !ret "vx" elem;
if (try fun_val !ret "vy" elem = 0.0
with Not_found -> false)
then ret := del_fun !ret "vy" elem;
end
done
done;
let span_rels =
if col_rel = "C" && row_rel = "R" then ""
else row_rel ^ " " ^ col_rel ^ " " in
let init_pos =
if init_pos_x = 0.0 && init_pos_y = 0.0 then ""
else "(" ^ string_of_float init_pos_x ^ ", " ^
string_of_float init_pos_y ^ ") " in
let dx_dy =
if pos_dx = cBOARD_DX && pos_dy = cBOARD_DY && init_pos = ""
then ""
else "(" ^ string_of_float pos_dx ^ ", " ^
string_of_float pos_dy ^ ") " in
let clear_empty struc fn =
try if IntMap.is_empty (StringMap.find fn struc.functions)
then {struc with functions = StringMap.remove fn struc.functions ;
fun_vals = StringMap.remove fn struc.fun_vals }
else struc
with Not_found -> struc in
ret := List.fold_left clear_empty !ret ["x"; "y"; "vx"; "vy"];
(* relations that are in the structure for the sake of
signature, i.e. they're empty *)
let signat_rels =
StringMap.fold (fun rel tups acc ->
if Tuples.is_empty tups then rel::acc else acc)
struc.relations [] in
ret := clear_rels !ret (fun rel ->
not (List.mem rel signat_rels) &&
(try List.assoc rel uniq_long = rel with Not_found -> true) &&
try Tuples.is_empty (StringMap.find rel !ret.relations)
with Not_found -> true);
span_rels ^ init_pos ^ dx_dy ^ "\"\n" ^
board ^ "\"",
gc_elems !ret
let fprint_rel ?(print_arity=true) struc f (rel_name, ts) =
if print_arity && Tuples.is_empty ts then
Format.fprintf f "%s:%d {}" rel_name
(StringMap.find rel_name struc.rel_signature)
else if Tuples.cardinal ts = 1 then
Format.fprintf f "@[<1>%s@ %s@]" rel_name
(tuple_str ~with_paren:true struc (Tuples.choose ts))
else
Format.fprintf f "@[<1>%s@ {@,@[<1>%a@]@,}@]" rel_name
(Aux.fprint_sep_list ";"
(fun f tp->Format.pp_print_string f
(tuple_str ~with_paren:false struc tp)))
(Tuples.elements ts)
(* Print the relation named [rel_name] with tuples [ts] as string. *)
let rel_str ?(print_arity=true) struc rel_name ts =
AuxIO.sprint_of_fprint (fprint_rel ~print_arity struc) (rel_name, ts)
let fprint_fun struc f (fun_name, vals) =
let update f (i, x) =
Format.fprintf f "%s->%s" (elem_str struc i) (string_of_float x) in
let cmp (i,_) (j,_) = String.compare (elem_str struc i) (elem_str struc j) in
let elems = List.sort cmp (IntMap.fold (fun k v acc -> (k,v)::acc) vals []) in
Format.fprintf f "@[<1>%s@ {@,@[<1>%a@]@,}@]" fun_name
(Aux.fprint_sep_list "," update) elems
let fprint_ext_structure ~show_empty f struc =
let rels =
StringMap.fold (fun k v acc ->
if show_empty || not (Tuples.is_empty v) then
(k,v)::acc
else acc) struc.relations [] in
let funs = List.sort (fun (f1,_) (f2,_) -> String.compare f2 f1)
(StringMap.fold (fun k v acc -> (k,v)::acc) struc.functions []) in
let rels = List.rev rels and funs = List.rev funs in
let consts_strs = List.fold_left (fun l (c, e) ->
(c ^ " = " ^ (elem_str struc e)) :: l) [] struc.constants in
let consts_str = String.concat "; " (List.rev consts_strs) in
let consts_str = if consts_strs = [] then consts_str else " ; "^ consts_str in
Format.fprintf f
"[@[<1>@[<1>@,%a@]@ |@,@[<1>@ %a@,%s@]@ |@,@[<1>@ %a@]@]@,]"
(Aux.fprint_sep_list ","
(fun f e->Format.pp_print_string f (elem_str struc e)))
(Elems.elements struc.elements)
(Aux.fprint_sep_list ";" (fprint_rel struc)) rels
consts_str
(Aux.fprint_sep_list ";" (fprint_fun struc)) funs
(* Print the structure [struc] as string, in extensive form (not using
condensed representations like boards). *)
let ext_str ?(show_empty=true) struc =
AuxIO.sprint_of_fprint (fprint_ext_structure ~show_empty) struc
let str ?(show_empty=true) struc =
let board, struc = board_to_string struc in
ext_str ~show_empty struc ^ (if board = "" then "" else " " ^ board)
let fprint ~show_empty f struc =
let board, struc = board_to_string struc in
if board = "" then fprint_ext_structure ~show_empty f struc
else
(* no line break after the closing bracket to stress that it is
the same structure; no formatter breaks inside the board *)
Format.fprintf f "%a @[<h 1>%s@]"
(fprint_ext_structure ~show_empty) struc board
let print ?(show_empty=true) struc =
AuxIO.print_of_fprint (fun fmt s -> fprint ~show_empty fmt s) struc
let sprint ?(show_empty=true) struc =
AuxIO.sprint_of_fprint (fun fmt s -> fprint ~show_empty fmt s) struc
let board_elem_coords name =
let col_index =
"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ" in
let col = String.index col_index name.[0] + 1 in
try col, int_of_string (String.sub name 1 (String.length name - 1))
with Failure _ | Invalid_argument _ ->
raise Not_found
let board_coords_name (col, row) =
if col < 1 || col > 52 || row < 1 then raise Not_found;
let col_index =
"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ" in
Char.escaped col_index.[col-1] ^ string_of_int row
(* Compare two structures and explain the first difference met. *)
exception Diff_result of string
let contained_in cmp_funs s1 s2 other =
let map_elem e1 =
let name = elem_str s1 e1 in
try find_elem s2 name
with Not_found -> raise (Diff_result (
"Element "^name^" not found in the "^other^" structure")) in
Elems.iter (fun e -> ignore (map_elem e)) s1.elements;
StringMap.iter (fun rel tups ->
(let try tups2 = StringMap.find rel s2.relations in
Tuples.iter (fun tup ->
let tup2 = Array.map map_elem tup in
if not (Tuples.mem tup2 tups2)
then raise (Diff_result (
Printf.sprintf
"Relation tuple %s(%s) not found in the %s structure"
rel (String.concat ", "
(List.map (elem_str s1) (Array.to_list tup)))
other))
) tups
with Not_found -> raise (Diff_result (
"Relation "^rel^" not found in the "^other^" structure"))
)) s1.relations;
StringMap.iter (fun fn vals ->
(let try vals2 = StringMap.find fn s2.functions in
IntMap.iter (fun e v ->
let v2 = IntMap.find (map_elem e) vals2 in
try
if not (cmp_funs v v2)
then raise (Diff_result (
Printf.sprintf
"Function %s(%s)->%F is %F instead in the %s structure"
fn (elem_str s1 e) v v2 other))
with Not_found -> raise (Diff_result (
Printf.sprintf
"Function %s(%s) not found in the second structure"
fn (elem_str s1 e)))
) vals
with Not_found -> raise (Diff_result (
"Function "^fn^" not found in the "^other^" structure"))
)) s1.functions
let compare_diff ?(cmp_funs=(=)) s1 s2 =
try
contained_in cmp_funs s1 s2 "second";
contained_in cmp_funs s2 s1 "first";
true, "equal"
with Diff_result expl -> false, expl
let diff_elems s1 s2 =
let rels, _ = List.split (rel_signature s1) in
let elems = Elems.elements s1.elements in
let inc s r e = try TIntMap.find e (StringMap.find r s.incidence) with
Not_found -> Tuples.empty in
let diff_elem_rel e r = not (Tuples.equal (inc s1 r e) (inc s2 r e)) in
let diff_rels e = (e, List.filter (diff_elem_rel e) rels) in
List.filter (fun (_, rs) -> rs <> []) (List.rev_map diff_rels elems)
let diffrels_struc s1 s2 =
if equal { s1 with relations = StringMap.empty; }
{ s2 with relations = StringMap.empty; } then
let is_eq_in map rel tp =
try
Tuples.equal (StringMap.find rel map) tp
with Not_found -> false in
let is_eq_in1, is_eq_in2 = is_eq_in s1.relations, is_eq_in s2.relations in
let diffrels = ref [] in
let appdiff1 r tp = if not (is_eq_in1 r tp) then diffrels := r::!diffrels in
let appdiff2 r tp = if not (is_eq_in2 r tp) then diffrels := r::!diffrels in
StringMap.iter appdiff1 s2.relations;
StringMap.iter appdiff2 s1.relations;
LOG 2 "SOME DIFF: %s" (String.concat ", " !diffrels);
Some (Aux.unique_sorted !diffrels)
else None
(* -------------------- PARSER HELPERS -------------------- *)
let is_uppercase c = c >= 'A' && c <= 'Z'
let is_lowercase c = c >= 'a' && c <= 'z'
let is_letter c = is_uppercase c || is_lowercase c
exception Board_parse_error of string
let add_opt_rel struc pred elem =
struc := add_rel !struc ("_opt_"^pred) [|elem|]
(* Lex and parse a board string into the structure. *)
let parse_board ?(row_col_rels="R","C")
?(pos_initial=0.0, 0.0)
?(pos_increment=cBOARD_DX, cBOARD_DY) ?struc board =
let row, col = row_col_rels in
let struc =
match struc with
| None -> ref (empty_structure ())
| Some struc -> ref struc in
let uniq1, uniq2, uniq3 =
find_unique (StringMap.fold (fun rel _ acc -> rel::acc)
!struc.rel_signature []) in
let uniq = uniq1 @ uniq2 @ uniq3 in
let lines = Aux.split_newlines board in
let lines = List.map (Aux.strip_charprop (fun c -> c = '\t')) lines in
let lines = List.filter (fun s->String.length s > 2) lines in
let rec split_line line =
let is_ok c = c = ' ' || c = '.' || Aux.is_alphanum c || c = '_' ||
c = '*' || c = '?' || c = '#' || c = '+' || c = '-' in
let error txt = raise (Board_parse_error
("Unrecognized field line: \"" ^ txt ^
"\" of board line: \"" ^ line ^"\"")) in
if line = "" then [] else if String.length line < 3 then error line else
if (is_ok line.[0] && is_ok line.[1] && is_ok line.[2]) then
let rest = String.sub line 3 ((String.length line) - 3) in
(String.sub line 0 3) :: (split_line rest)
else error (String.sub line 0 3) in
let rec rev_combine_pairs acc = function
| [] -> acc
| [hd] ->
raise (Board_parse_error
("Odd number of lines, bottom line: " ^ hd))
| hd1::hd2::tl -> rev_combine_pairs ((hd1,hd2)::acc) tl in
let fields =
List.map (fun (up_line, lo_line) ->
List.combine (split_line lo_line) (split_line up_line))
(rev_combine_pairs [] lines) in
let r_max = List.length fields
and c_max =
if fields = [] then -1 else List.length (List.hd fields) in
if fields = [] then raise (Board_parse_error "Empty")
else if c_max > 52 then raise
(Board_parse_error "Board too wide")
else
let fields = ref fields in
let parse s =
let s = String.sub s 0
(min (try String.index s ' ' with Not_found -> 3)
(try String.index s '.' with Not_found -> 3)) in
let sl = String.length s - 1 in
let unabbrev p =
try Aux.rev_assoc uniq p
with Not_found -> struc := add_rel_name p 1 !struc; p in
if sl = -1 then []
else if s.[0] = '*' then ["*"] (* treated specially *)
else if sl = 0 && s.[sl] = '?' then ["_any_"]
else if s.[0] = '+' then
let p = unabbrev (omit 1 s) in ["_new_"^p; p]
else if s.[0] = '-' then ["_del_"^unabbrev (omit 1 s)]
else if s.[sl] = '?' then [unabbrev (String.sub s 0 sl); "_any_"]
else if s.[0] = '?' then ["_opt_"^unabbrev (omit 1 s)]
else if s.[sl] = '#' then
["_diffthan_"^unabbrev (String.sub s 0 sl); "_any_"]
else if s.[0] = '#' then ["_diffthan_"^unabbrev (omit 1 s)]
else [unabbrev s] in
let board_els =
Array.make_matrix c_max r_max (-1) in
let x0, y0 = pos_initial in
let dx, dy = pos_increment in
let col_index =
"abcdefghijklmnopqrstuvwxyzABCDEFGHIJKLMNOPQRSTUVWXYZ" in
let shape = circle_structure (cBOARD_DX /. 3.) (cBOARD_DX /. 3.) in
for r = 1 to r_max do
for c = 1 to c_max do
if List.hd !fields = [] then
raise (Board_parse_error
(Printf.sprintf
"Row %d is too short, column %d expected" r c));
let lo_line, up_line = List.hd (List.hd !fields) in
let parsed_preds = parse lo_line @ parse up_line in
fields := List.tl (List.hd !fields)::List.tl !fields;
if not (List.mem "*" parsed_preds)
then (
let elname = Char.escaped col_index.[c-1] ^ string_of_int r in
let nstruc, elem =
find_or_new_elem !struc elname in
board_els.(c-1).(r-1) <- elem;
struc := nstruc;
let tup = [|elem|] in
List.iter (fun r -> struc := add_rel !struc r tup)
parsed_preds);
let elem = board_els.(c-1).(r-1) in
if c > 1 && elem <> -1 && board_els.(c-2).(r-1) <> -1 then
struc := add_rel !struc row [|board_els.(c-2).(r-1); elem|];
if r > 1 && elem <> -1 && board_els.(c-1).(r-2) <> -1 then
struc := add_rel !struc col [|board_els.(c-1).(r-2); elem|];
if elem <> -1 then begin
struc := add_model !struc "shape" (elem, shape);
struc := add_fun !struc "x"
(elem, x0 +. dx *. float_of_int (c-1));
struc := add_fun !struc "y"
(elem, y0 +. dy *. float_of_int (r-1));
struc := add_fun !struc "vx" (elem, 0.0);
struc := add_fun !struc "vy" (elem, 0.0);
end;
done;
if List.hd !fields <> [] then
raise (Board_parse_error
(Printf.sprintf
"Row %d is too long, expected %d columns" r c_max));
fields := List.tl !fields;
done;
!struc

Get latest updates about Open Source Projects, Conferences and News.

Sign up for the SourceForge newsletter:





No, thanks