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 (* for experimentation purposes -- do not use in production code *) |
23 (* for experimentation purposes -- do not use in production code *) |
24 val e_generate_weights : bool Unsynchronized.ref |
24 val e_weights : bool Unsynchronized.ref |
25 val e_weight_factor : real Unsynchronized.ref |
25 val e_weight_factor : real Unsynchronized.ref |
26 val e_default_weight : real Unsynchronized.ref |
26 val e_default_weight : real Unsynchronized.ref |
27 |
27 |
28 val eN : string |
28 val eN : string |
29 val spassN : string |
29 val spassN : string |
93 if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000 |
93 if string_ord (getenv "E_VERSION", "1.1") = LESS then 2000 else 1000 |
94 |
94 |
95 val tstp_proof_delims = |
95 val tstp_proof_delims = |
96 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
96 ("# SZS output start CNFRefutation.", "# SZS output end CNFRefutation") |
97 |
97 |
98 val e_generate_weights = Unsynchronized.ref true |
98 val e_weights = Unsynchronized.ref true |
99 val e_weight_factor = Unsynchronized.ref 40.0 |
99 val e_weight_factor = Unsynchronized.ref 40.0 |
100 val e_default_weight = Unsynchronized.ref 0.5 |
100 val e_default_weight = Unsynchronized.ref 0.5 |
101 |
101 |
102 fun e_weights weights = |
102 fun e_weight_arguments weights = |
103 if !e_generate_weights andalso |
103 if !e_weights andalso string_ord (getenv "E_VERSION", "1.2w") <> LESS then |
104 string_ord (getenv "E_VERSION", "1.2B") <> LESS then |
|
105 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
104 "--split-clauses=4 --split-reuse-defs --simul-paramod --forward-context-sr \ |
106 \--destructive-er-aggressive --destructive-er --presat-simplify \ |
105 \--destructive-er-aggressive --destructive-er --presat-simplify \ |
107 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
106 \--prefer-initial-clauses -tKBO6 -winvfreqrank -c1 -Ginvfreqconjmax -F1 \ |
108 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
107 \--delete-bad-limit=150000000 -WSelectMaxLComplexAvoidPosPred \ |
109 \-H'(4*FunWeight(SimulateSOS, " ^ |
108 \-H'(4*FunWeight(SimulateSOS, " ^ |
121 |
120 |
122 val e_config : atp_config = |
121 val e_config : atp_config = |
123 {exec = ("E_HOME", "eproof"), |
122 {exec = ("E_HOME", "eproof"), |
124 required_execs = [], |
123 required_execs = [], |
125 arguments = fn _ => fn timeout => fn weights => |
124 arguments = fn _ => fn timeout => fn weights => |
126 "--tstp-in --tstp-out -l5 " ^ e_weights weights ^ " -tAutoDev \ |
125 "--tstp-in --tstp-out -l5 " ^ e_weight_arguments weights ^ " -tAutoDev \ |
127 \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), |
126 \--silent --cpu-limit=" ^ string_of_int (to_secs (e_bonus ()) timeout), |
128 has_incomplete_mode = false, |
127 has_incomplete_mode = false, |
129 proof_delims = [tstp_proof_delims], |
128 proof_delims = [tstp_proof_delims], |
130 known_failures = |
129 known_failures = |
131 [(Unprovable, "SZS status: CounterSatisfiable"), |
130 [(Unprovable, "SZS status: CounterSatisfiable"), |