Project

General

Profile

Statistics
| Branch: | Revision:

cool / src / fuzzy / fuzzytest.ml @ b75e5a66

History | View | Annotate | Download (7.34 KB)

1
open CoolUtils
2
open FuzzyALCReasoner
3
open Printf
4
module AF = FuzzyALCABox
5

    
6
let timelimit = 15.
7

    
8
let conceptnames = [ "AA"; "AB"; "AC"; "AD"; "AE"; "AF"; "AG"; "AH"; "AI"; "AJ"; "AK"; "AL"; "AM"; "AN"; "AO"; "AP"; "AQ"; "AR"; "AS"; "AT"; "AU"; "AV"; "AW"; "AX"; "AY"; "AZ"; "BA"; "BB"; "BC"; "BD"; "BE"; "BF"; "BG"; "BH"; "BI"; "BJ"; "BK"; "BL"; "BM"; "BN"; "BO"; "BP"; "BQ"; "BR"; "BS"; "BT"; "BU"; "BV"; "BW"; "BX"; "BY"; "BZ"; "CA"; "CB"; "CC"; "CD"; "CE"; "CF"; "CG"; "CH"; "CI"; "CJ"; "CK"; "CL"; "CM"; "CN"; "CO"; "CP"; "CQ"; "CR"; "CS"; "CT"; "CU"; "CV"; "CW"; "CX"; "CY"; "CZ"; "DA"; "DB"; "DC"; "DD"; "DE"; "DF"; "DG"; "DH"; "DI"; "DJ"; "DK"; "DL"; "DM"; "DN"; "DO"; "DP"; "DQ"; "DR"; "DS"; "DT"; "DU"; "DV"; "DW"; "DX"; "DY"; "DZ"; "EA"; "EB"; "EC"; "ED"; "EE"; "EF"; "EG"; "EH"; "EI"; "EJ"; "EK"; "EL"; "EM"; "EN"; "EO"; "EP"; "EQ"; "ER"; "ES"; "ET"; "EU"; "EV"; "EW"; "EX"; "EY"; "EZ"; "FA"; "FB"; "FC"; "FD"; "FE"; "FF"; "FG"; "FH"; "FI"; "FJ"; "FK"; "FL"; "FM"; "FN"; "FO"; "FP"; "FQ"; "FR"; "FS"; "FT"; "FU"; "FV"; "FW"; "FX"; "FY"; "FZ"; "GA"; "GB"; "GC"; "GD"; "GE"; "GF"; "GG"; "GH"; "GI"; "GJ"; "GK"; "GL"; "GM"; "GN"; "GO"; "GP"; "GQ"; "GR"; "GS"; "GT"; "GU"; "GV"; "GW"; "GX"; "GY"; "GZ"; "HA"; "HB"; "HC"; "HD"; "HE"; "HF"; "HG"; "HH"; "HI"; "HJ"; "HK"; "HL"; "HM"; "HN"; "HO"; "HP"; "HQ"; "HR"; "HS"; "HT"; "HU"; "HV"; "HW"; "HX"; "HY"; "HZ"; "IA"; "IB"; "IC"; "ID"; "IE"; "IF"; "IG"; "IH"; "II"; "IJ"; "IK"; "IL"; "IM"; "IN"; "IO"; "IP"; "IQ"; "IR"; "IS"; "IT"; "IU"; "IV"; "IW"; "IX"; "IY"; "IZ"; "JA"; "JB"; "JC"; "JD"; "JE"; "JF"; "JG"; "JH"; "JI"; "JJ"; "JK"; "JL"; "JM"; "JN"; "JO"; "JP"; "JQ"; "JR"; "JS"; "JT"; "JU"; "JV"; "JW"; "JX"; "JY"; "JZ"; "KA"; "KB"; "KC"; "KD"; "KE"; "KF"; "KG"; "KH"; "KI"; "KJ"; "KK"; "KL"; "KM"; "KN"; "KO"; "KP"; "KQ"; "KR"; "KS"; "KT"; "KU"; "KV"; "KW"; "KX"; "KY"; "KZ"; "LA"; "LB"; "LC"; "LD"; "LE"; "LF"; "LG"; "LH"; "LI"; "LJ"; "LK"; "LL"; "LM"; "LN"; "LO"; "LP"; "LQ"; "LR"; "LS"; "LT"; "LU"; "LV"; "LW"; "LX"; "LY"; "LZ"; "MA"; "MB"; "MC"; "MD"; "ME"; "MF"; "MG"; "MH"; "MI"; "MJ"; "MK"; "ML"; "MM"; "MN"; "MO"; "MP"; "MQ"; "MR"; "MS"; "MT"; "MU"; "MV"; "MW"; "MX"; "MY"; "MZ"; "NA"; "NB"; "NC"; "ND"; "NE"; "NF"; "NG"; "NH"; "NI"; "NJ"; "NK"; "NL"; "NM"; "NN"; "NO"; "NP"; "NQ"; "NR"; "NS"; "NT"; "NU"; "NV"; "NW"; "NX"; "NY"; "NZ"; "OA"; "OB"; "OC"; "OD"; "OE"; "OF"; "OG"; "OH"; "OI"; "OJ"; "OK"; "OL"; "OM"; "ON"; "OO"; "OP"; "OQ"; "OR"; "OS"; "OT"; "OU"; "OV"; "OW"; "OX"; "OY"; "OZ"; "PA"; "PB"; "PC"; "PD"; "PE"; "PF"; "PG"; "PH"; "PI"; "PJ"; "PK"; "PL"; "PM"; "PN"; "PO"; "PP"; "PQ"; "PR"; "PS"; "PT"; "PU"; "PV"; "PW"; "PX"; "PY"; "PZ"; "QA"; "QB"; "QC"; "QD"; "QE"; "QF"; "QG"; "QH"; "QI"; "QJ"; "QK"; "QL"; "QM"; "QN"; "QO"; "QP"; "QQ"; "QR"; "QS"; "QT"; "QU"; "QV"; "QW"; "QX"; "QY"; "QZ"; "RA"; "RB"; "RC"; "RD"; "RE"; "RF"; "RG"; "RH"; "RI"; "RJ"; "RK"; "RL"; "RM"; "RN"; "RO"; "RP"; "RQ"; "RR"; "RS"; "RT"; "RU"; "RV"; "RW"; "RX"; "RY"; "RZ"; "SA"; "SB"; "SC"; "SD"; "SE"; "SF"; "SG"; "SH"; "SI"; "SJ"; "SK"; "SL"; "SM"; "SN"; "SO"; "SP"; "SQ"; "SR"; "SS"; "ST"; "SU"; "SV"; "SW"; "SX"; "SY"; "SZ"; "TA"; "TB"; "TC"; "TD"; "TE"; "TF"; "TG"; "TH"; "TI"; "TJ"; "TK"; "TL"; "TM"; "TN"; "TO"; "TP"; "TQ"; "TR"; "TS"; "TT"; "TU"; "TV"; "TW"; "TX"; "TY"; "TZ"; "UA"; "UB"; "UC"; "UD"; "UE"; "UF"; "UG"; "UH"; "UI"; "UJ"; "UK"; "UL"; "UM"; "UN"; "UO"; "UP"; "UQ"; "UR"; "US"; "UT"; "UU"; "UV"; "UW"; "UX"; "UY"; "UZ"; "VA"; "VB"; "VC"; "VD"; "VE"; "VF"; "VG"; "VH"; "VI"; "VJ"; "VK"; "VL"; "VM"; "VN"; "VO"; "VP"; "VQ"; "VR"; "VS"; "VT"; "VU"; "VV"; "VW"; "VX"; "VY"; "VZ"; "WA"; "WB"; "WC"; "WD"; "WE"; "WF"; "WG"; "WH"; "WI"; "WJ"; "WK"; "WL"; "WM"; "WN"; "WO"; "WP"; "WQ"; "WR"; "WS"; "WT"; "WU"; "WV"; "WW"; "WX"; "WY"; "WZ"; "XA"; "XB"; "XC"; "XD"; "XE"; "XF"; "XG"; "XH"; "XI"; "XJ"; "XK"; "XL"; "XM"; "XN"; "XO"; "XP"; "XQ"; "XR"; "XS"; "XT"; "XU"; "XV"; "XW"; "XX"; "XY"; "XZ"; "YA"; "YB"; "YC"; "YD"; "YE"; "YF"; "YG"; "YH"; "YI"; "YJ"; "YK"; "YL"; "YM"; "YN"; "YO"; "YP"; "YQ"; "YR"; "YS"; "YT"; "YU"; "YV"; "YW"; "YX"; "YY"; "YZ"; "ZA"; "ZB"; "ZC"; "ZD"; "ZE"; "ZF"; "ZG"; "ZH"; "ZI"; "ZJ"; "ZK"; "ZL"; "ZM"; "ZN"; "ZO"; "ZP"; "ZQ"; "ZR"; "ZS"; "ZT"; "ZU"; "ZV"; "ZW"; "ZX"; "ZY"; "ZZ" ] (* XXX *)
9

    
10
let funConcat f1 f2 x = f1 (f2 x) (* XXX can't this be done better? *)
11

    
12
let fuzzyDL_print concept =
13
    "(define-fuzzy-logic lukasiewicz)\n" ^
14
    "(max-sat? " ^ (FuzzyALCABox.print_fuzzyDL concept) ^ ")"
15

    
16
let fuzzyDL_input concept sat =
17
    let sat_s =
18
        if sat == 1 then "0"
19
        else "1"
20
    in
21
    "if [ $(echo \"" ^ (fuzzyDL_print concept) ^ "\" | sh check-fuzzydl.sh | grep \"<= 0.0\" | wc -l) -eq " ^ sat_s ^ " ]\n" ^ (
22
        if sat == 2 then "then echo UNKNOWN; else echo UNKNOWN; fi"
23
        else "then echo SUCCESS; else echo MISMATCH; fi"
24
    )
25
let fuzzyDL_time concept x =
26
    "echo \"" ^ (fuzzyDL_print concept) ^ "\" | sh time-fuzzydl.sh " ^ (string_of_int x)
27

    
28
let measureRuntime ab =
29
    let t = Unix.gettimeofday() in
30
    FuzzyALCReasoner.setMaxRuntime timelimit;
31
    true
32

    
33
let _ =
34
    (* Generate exponentially large concepts *)
35
    let rec generate l =
36
        match l with
37
        | (a :: (b :: t)) ->
38
                AF.AND(AF.EXISTS(0, AF.AP(a)),
39
                        AF.AND(AF.EXISTS(0, AF.AP(b)),
40
                        AF.FORALL(0, generate t)))
41
        | _ -> TRUE
42
    in
43
    (
44
        let con = AF.OR(AF.AP("C"), generate conceptnames) in
45
        let exp_in = ([AF.CONCEPT(0, con)], 0, []) in
46
        (*print_endline ("Trying to solve worst-case formula using COOL:");*)
47
        let sat = fuzzyALCsat [exp_in] in
48
        (*print_endline ("Success");*)
49
        print_endline (fuzzyDL_input con (if sat then 1 else 0));
50
    );
51
    let generate_testout concept file x =
52
        let ab = ([FuzzyALCABox.CONCEPT(0, concept)], 0, []) in
53
        print_endline ("# Formula/ABox:\n# " ^ (FuzzyALCABox.printAssertion ab));
54
        try
55
            (*print_endline ("echo '" ^ (FuzzyALCABox.printAssertion ab) ^ "'");*)
56
            let (time, sat) =
57
                if -1 < x then fuzzyALCsat_time [ab] 3. else
58
                    (-1., true) in
59
            if time +. 1. < 0.01 then (
60
                fprintf file "999\n";
61
                raise BranchCountExhausted
62
            ) else (
63
                fprintf file "%f\n" time;
64
                (*
65
                if sat then
66
                    fprintf file "# SAT\n"
67
                else
68
                    fprintf file "# NOT SAT\n";
69
                *)
70
                (*print_endline (fuzzyDL_input concept (if sat then 1 else 0));*)
71
            );
72
            print_endline (fuzzyDL_input concept (if sat then 1 else 0));
73
            (*print_endline (fuzzyDL_time concept x);*)
74
            flush file;
75
            sat
76
        with
77
        BranchCountExhausted -> (
78
            print_endline "echo 'Solver too slow for this formula!'";
79
            print_endline (fuzzyDL_input concept 2);
80
            false
81
        );
82
    in
83
    let file = open_out "timing-fuzzyCOOL" in
84
    let feas = open_out "feasible-fuzzyCOOL" in
85
    for i = 1 to 110 do
86
        Random.init i;
87
        let cnt = ref 0 in
88
        for j = 1 to 15 do
89
            let concept = (FuzzyALCABox.random_concept_opcount 30 i 3 [1; 2; 3; 0]) in
90
            fprintf file "%d " i;
91
            let sat = generate_testout concept file i in
92
            flush file;
93
            if sat then
94
                incr cnt
95
            else
96
                ()
97
        done;
98
        fprintf feas "%d %d\n" i !cnt;
99
        flush feas;
100
        flush file;
101
    done;
102
    close_out file;
103
    close_out feas;