88 (* Give E an extra second to reconstruct the proof. Older versions even get two |
88 (* Give E an extra second to reconstruct the proof. Older versions even get two |
89 seconds, because the "eproof" script wrongly subtracted an entire second to |
89 seconds, because the "eproof" script wrongly subtracted an entire second to |
90 account for the overhead of the script itself, which is in fact much |
90 account for the overhead of the script itself, which is in fact much |
91 lower. *) |
91 lower. *) |
92 fun e_bonus () = |
92 fun e_bonus () = |
93 case getenv "E_VERSION" of |
93 if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000 |
94 "" => 2000 |
|
95 | version => |
|
96 if exists (fn s => String.isPrefix s version) ["0.9", "1.0"] then 2000 |
|
97 else 1000 |
|
98 |
94 |
99 val tstp_proof_delims = |
95 val tstp_proof_delims = |
100 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
96 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
101 |
97 |
102 val e_generate_weights = Unsynchronized.ref false |
98 val e_generate_weights = Unsynchronized.ref true |
103 val e_weight_factor = Unsynchronized.ref 60.0 |
99 val e_weight_factor = Unsynchronized.ref 40.0 |
104 val e_default_weight = Unsynchronized.ref 0.5 |
100 val e_default_weight = Unsynchronized.ref 0.5 |
105 |
101 |
106 fun e_weights weights = |
102 fun e_weights weights = |
107 if !e_generate_weights then |
103 if !e_generate_weights andalso |
|
104 string_ord (getenv "E_VERSION", "1.2B") <> LESS then |
108 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
105 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
109 \--destructive-er-aggressive --destructive-er --presat-simplify \ |
106 \--destructive-er-aggressive --destructive-er --presat-simplify \ |
110 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
107 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
111 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
108 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
112 \-H'(4*FunWeight(SimulateSOS, " ^ |
109 \-H'(4*FunWeight(SimulateSOS, " ^ |