abella-prover / abella

An interactive theorem prover based on lambda-tree syntax
https://abella-prover.org/
GNU General Public License v3.0
89 stars 18 forks source link

Non iterative use of search depth bound #67

Closed robblanco closed 8 years ago

robblanco commented 8 years ago

This commit modifies the internal behavior of the search tactic (while preserving its semantics) by moving from IDDFS on the range of dephts from 1 to the effective maximum depth to a single execution of Tactics.search on said maximum depth.

The rationale for this change is the following. If an explicit bound is not given, the system falls back to the (small) default, and any penalty incurred by trying to explore deeper and initially missing shallow solutions is negligible.

If, on the other hand, an explicit bound is given, the responsibility for its adequacy falls on the user, as do any adverse effects of excessive slack on runtime. On the upside, this strategy avoids the quadratic time factor that results from multiple executions of the search tactic with increasing bounds, which becomes problematic for higher values of these.

chaudhuri commented 8 years ago

Manually cherry-picked.