18 known_failures: (failure * string) list, |
18 known_failures: (failure * string) list, |
19 default_max_relevant: int, |
19 default_max_relevant: int, |
20 explicit_forall: bool, |
20 explicit_forall: bool, |
21 use_conjecture_for_hypotheses: bool} |
21 use_conjecture_for_hypotheses: bool} |
22 |
22 |
|
23 datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight |
|
24 |
23 (* for experimentation purposes -- do not use in production code *) |
25 (* for experimentation purposes -- do not use in production code *) |
24 val e_weights : bool Unsynchronized.ref |
26 val e_weight_method : e_weight_method Unsynchronized.ref |
25 val e_weight_factor : real Unsynchronized.ref |
27 val e_default_fun_weight : real Unsynchronized.ref |
26 val e_default_weight : real Unsynchronized.ref |
28 val e_fun_weight_base : real Unsynchronized.ref |
|
29 val e_fun_weight_factor : real Unsynchronized.ref |
|
30 val e_default_sym_offs_weight : real Unsynchronized.ref |
|
31 val e_sym_offs_weight_base : real Unsynchronized.ref |
|
32 val e_sym_offs_weight_factor : real Unsynchronized.ref |
27 |
33 |
28 val eN : string |
34 val eN : string |
29 val spassN : string |
35 val spassN : string |
30 val vampireN : string |
36 val vampireN : string |
31 val sine_eN : string |
37 val sine_eN : string |
93 if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000 |
99 if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000 |
94 |
100 |
95 val tstp_proof_delims = |
101 val tstp_proof_delims = |
96 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
102 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
97 |
103 |
98 val e_weights = Unsynchronized.ref true |
104 datatype e_weight_method = E_Auto | E_Fun_Weight | E_Sym_Offset_Weight |
99 val e_weight_factor = Unsynchronized.ref 40.0 |
105 |
100 val e_default_weight = Unsynchronized.ref 0.5 |
106 val e_weight_method = Unsynchronized.ref E_Fun_Weight |
|
107 val e_default_fun_weight = Unsynchronized.ref 0.5 |
|
108 val e_fun_weight_base = Unsynchronized.ref 0.0 |
|
109 val e_fun_weight_factor = Unsynchronized.ref 40.0 |
|
110 val e_default_sym_offs_weight = Unsynchronized.ref 0.0 |
|
111 val e_sym_offs_weight_base = Unsynchronized.ref ~30.0 |
|
112 val e_sym_offs_weight_factor = Unsynchronized.ref ~30.0 |
|
113 |
|
114 fun e_weight_method_case fw sow = |
|
115 case !e_weight_method of |
|
116 E_Auto => raise Fail "Unexpected \"E_Auto\"" |
|
117 | E_Fun_Weight => fw |
|
118 | E_Sym_Offset_Weight => sow |
|
119 |
|
120 fun scaled_e_weight w = |
|
121 e_weight_method_case (!e_fun_weight_base) (!e_sym_offs_weight_base) |
|
122 + w * e_weight_method_case (!e_fun_weight_factor) (!e_sym_offs_weight_factor) |
|
123 |> Real.ceil |> signed_string_of_int |
101 |
124 |
102 fun e_weight_arguments weights = |
125 fun e_weight_arguments weights = |
103 if !e_weights andalso string_ord (getenv "E_VERSION", "1.2w") <> LESS then |
126 if !e_weight_method = E_Auto orelse |
|
127 string_ord (getenv "E_VERSION", "1.2w") = LESS then |
|
128 "-xAutoDev" |
|
129 else |
104 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
130 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
105 \--destructive-er-aggressive --destructive-er --presat-simplify \ |
131 \--destructive-er-aggressive --destructive-er --presat-simplify \ |
106 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
132 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
107 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
133 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
108 \-H'(4*FunWeight(SimulateSOS, " ^ |
134 \-H'(4*" ^ e_weight_method_case "FunWeight" "SymOffsetWeight" ^ |
109 string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^ |
135 "(SimulateSOS, " ^ |
|
136 scaled_e_weight (e_weight_method_case (!e_default_fun_weight) |
|
137 (!e_default_sym_offs_weight)) ^ |
110 ",20,1.5,1.5,1" ^ |
138 ",20,1.5,1.5,1" ^ |
111 (weights () |
139 (weights () |> map (fn (s, w) => "," ^ s ^ ":" ^ scaled_e_weight w) |
112 |> map (fn (s, w) => "," ^ s ^ ":" ^ |
140 |> implode) ^ |
113 string_of_int (Real.ceil (w * !e_weight_factor))) |
|
114 |> implode) ^ |
|
115 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ |
141 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ |
116 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ |
142 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ |
117 \FIFOWeight(PreferProcessed))'" |
143 \FIFOWeight(PreferProcessed))'" |
118 else |
|
119 "-xAutoDev" |
|
120 |
144 |
121 val e_config : atp_config = |
145 val e_config : atp_config = |
122 {exec = ("E_HOME", "eproof"), |
146 {exec = ("E_HOME", "eproof"), |
123 required_execs = [], |
147 required_execs = [], |
124 arguments = fn _ => fn timeout => fn weights => |
148 arguments = fn _ => fn timeout => fn weights => |