172 val vampire_failure_strs = |
172 val vampire_failure_strs = |
173 ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; |
173 ["Satisfiability detected", "Refutation not found", "CANNOT PROVE"]; |
174 val vampire_max_new_clauses = 60; |
174 val vampire_max_new_clauses = 60; |
175 val vampire_insert_theory_const = false; |
175 val vampire_insert_theory_const = false; |
176 |
176 |
177 fun vampire_prover_config full : prover_config = |
177 fun vampire_prover_config isar : prover_config = |
178 {command = Path.explode "$VAMPIRE_HOME/vampire", |
178 {command = Path.explode "$VAMPIRE_HOME/vampire", |
179 arguments = (fn timeout => "--output_syntax tptp --mode casc" ^ |
179 arguments = (fn timeout => "--output_syntax tptp --mode casc" ^ |
180 " -t " ^ string_of_int timeout), |
180 " -t " ^ string_of_int timeout), |
181 failure_strs = vampire_failure_strs, |
181 failure_strs = vampire_failure_strs, |
182 max_new_clauses = vampire_max_new_clauses, |
182 max_new_clauses = vampire_max_new_clauses, |
183 insert_theory_const = vampire_insert_theory_const, |
183 insert_theory_const = vampire_insert_theory_const, |
184 emit_structured_proof = full}; |
184 emit_structured_proof = isar}; |
185 |
185 |
186 val vampire = tptp_prover ("vampire", vampire_prover_config false); |
186 val vampire = tptp_prover ("vampire", vampire_prover_config false); |
187 val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true); |
187 val vampire_isar = tptp_prover ("vampire_isar", vampire_prover_config true); |
188 |
188 |
189 |
189 |
194 "SZS status: ResourceOut", "SZS status ResourceOut", |
194 "SZS status: ResourceOut", "SZS status ResourceOut", |
195 "# Cannot determine problem status"]; |
195 "# Cannot determine problem status"]; |
196 val eprover_max_new_clauses = 100; |
196 val eprover_max_new_clauses = 100; |
197 val eprover_insert_theory_const = false; |
197 val eprover_insert_theory_const = false; |
198 |
198 |
199 fun eprover_config full : prover_config = |
199 fun eprover_config isar : prover_config = |
200 {command = Path.explode "$E_HOME/eproof", |
200 {command = Path.explode "$E_HOME/eproof", |
201 arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^ |
201 arguments = (fn timeout => "--tstp-in --tstp-out -l5 -xAutoDev -tAutoDev" ^ |
202 " --silent --cpu-limit=" ^ string_of_int timeout), |
202 " --silent --cpu-limit=" ^ string_of_int timeout), |
203 failure_strs = eprover_failure_strs, |
203 failure_strs = eprover_failure_strs, |
204 max_new_clauses = eprover_max_new_clauses, |
204 max_new_clauses = eprover_max_new_clauses, |
205 insert_theory_const = eprover_insert_theory_const, |
205 insert_theory_const = eprover_insert_theory_const, |
206 emit_structured_proof = full}; |
206 emit_structured_proof = isar}; |
207 |
207 |
208 val eprover = tptp_prover ("e", eprover_config false); |
208 val eprover = tptp_prover ("e", eprover_config false); |
209 val eprover_isar = tptp_prover ("e_isar", eprover_config true); |
209 val eprover_isar = tptp_prover ("e_isar", eprover_config true); |
210 |
210 |
211 |
211 |