86 (* "best_slices" must be found empirically, taking a wholistic approach since |
86 (* "best_slices" must be found empirically, taking a wholistic approach since |
87 the ATPs are run in parallel. The "real" components give the faction of the |
87 the ATPs are run in parallel. The "real" components give the faction of the |
88 time available given to the slice and should add up to 1.0. The "bool" |
88 time available given to the slice and should add up to 1.0. The "bool" |
89 component indicates whether the slice's strategy is complete; the "int", the |
89 component indicates whether the slice's strategy is complete; the "int", the |
90 preferred number of facts to pass; the first "string", the preferred type |
90 preferred number of facts to pass; the first "string", the preferred type |
91 system; the second "string", extra information to the prover (e.g., SOS or no |
91 system (which should be sound or quasi-sound); the second "string", extra |
92 SOS). |
92 information to the prover (e.g., SOS or no SOS). |
93 |
93 |
94 The last slice should be the most "normal" one, because it will get all the |
94 The last slice should be the most "normal" one, because it will get all the |
95 time available if the other slices fail early and also because it is used if |
95 time available if the other slices fail early and also because it is used if |
96 slicing is disabled (e.g., by the minimizer). *) |
96 slicing is disabled (e.g., by the minimizer). *) |
97 |
97 |