97 else 1000 |
97 else 1000 |
98 |
98 |
99 val tstp_proof_delims = |
99 val tstp_proof_delims = |
100 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
100 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
101 |
101 |
102 val e_generate_weights = Unsynchronized.ref false |
102 val e_generate_weights = Unsynchronized.ref true |
103 val e_weight_factor = Unsynchronized.ref 4.0 |
103 val e_weight_factor = Unsynchronized.ref 60.0 |
104 val e_default_weight = Unsynchronized.ref 0.5 |
104 val e_default_weight = Unsynchronized.ref 0.5 |
105 |
105 |
106 fun e_weights weights = |
106 fun e_weights weights = |
107 if !e_generate_weights then |
107 if !e_generate_weights then |
108 "(1*FunWeight(ConstPrio," ^ |
108 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
|
109 \--destructive-er-aggressive --destructive-er --presat-simplify \ |
|
110 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
|
111 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
|
112 \-H'(4*FunWeight(SimulateSOS, " ^ |
109 string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^ |
113 string_of_int (Real.ceil (!e_default_weight * !e_weight_factor)) ^ |
110 ",1,1.5,1.5,1.5" ^ |
114 ",20,1.5,1.5,1" ^ |
111 (weights () |
115 (weights () |
112 |> map (fn (s, w) => "," ^ s ^ ":" ^ |
116 |> map (fn (s, w) => "," ^ s ^ ":" ^ |
113 string_of_int (Real.ceil (w * !e_weight_factor))) |
117 string_of_int (Real.ceil (w * !e_weight_factor))) |
114 |> implode) ^ ")+5*AutoDev)" |
118 |> implode) ^ |
|
119 "),3*ConjectureGeneralSymbolWeight(PreferNonGoals,200,100,200,50,50,1,100,\ |
|
120 \1.5,1.5,1),1*Clauseweight(PreferProcessed,1,1,1),1*\ |
|
121 \FIFOWeight(PreferProcessed))'" |
115 else |
122 else |
116 "AutoDev" |
123 "-xAutoDev" |
117 |
124 |
118 val e_config : atp_config = |
125 val e_config : atp_config = |
119 {exec = ("E_HOME", "eproof"), |
126 {exec = ("E_HOME", "eproof"), |
120 required_execs = [], |
127 required_execs = [], |
121 arguments = fn _ => fn timeout => fn weights => |
128 arguments = fn _ => fn timeout => fn weights => |
122 "--tstp-in --tstp-out -l5 -x'" ^ e_weights weights ^ "' -tAutoDev \ |
129 "--tstp-in --tstp-out -l5 " ^ e_weights weights ^ " -tAutoDev \ |
123 \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), |
130 \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), |
124 has_incomplete_mode = false, |
131 has_incomplete_mode = false, |
125 proof_delims = [tstp_proof_delims], |
132 proof_delims = [tstp_proof_delims], |
126 known_failures = |
133 known_failures = |
127 [(Unprovable, "SZS status: CounterSatisfiable"), |
134 [(Unprovable, "SZS status: CounterSatisfiable"), |