Version 1.2 - 07/01/2005 ======================== Switched to DARCS as the version control system. This version contains some minor optimizations wrt. version 1.1, but nothing major. It was only released because it participated in CASC20. Features: --------- - Time Limit A limit on the prover's runtime can be imposed with the flags --timeout-cpu and --timeout-wc - Zipped Input Problem files can be read from a zipped input file using the flag --zipped-source. Requires the library camlzip to be installed. Version 1.1 - 12/28/2004 ========================= CVS tag: version-1.1 Features: - New Restart strategies (see darwin -help) The old one, which restarts eagerly, a second one, which tries to backtrack along the branch to a choice point where the derivation can be resumed and completed to find an exhausted branch, and a third one, which does not eagerly drop candidates, but only tests for exceeding candidates when an 'exhausted' branch has been found, and then backtracks and resumes the derivation. - Iterative Deepening over Term Weight Provided as an alternative to Term Depth. - Horn Negative candidate literals can be handled in several ways: - ignored - they are not used at all. - lookahead - they are merely used for the Close lookahead. - use - they are used for all purposes just like the positive candidates. - Extended Close Look-ahead It can be specified by a command line option that all candidates are used for the Close look-ahead, not only the candidates obeying the depth bound. - Equality Axiomatization The predicate symbol '=' can be interpreted as the equality relation by adding the axioms of equality needed for the problem specification. - Interface Short and verbose interface (with backward incompatible flags), integrating the new features. - Input format The input format is as previously deduced from the extension, but now additionaly a default can be specified for an unknown extension. - DIG output A prototypical implementation for printing a found model in the DIG (Disjunctions of Implicit Generalizations) format. - Derivation Output Various methods to print a derivation to stdout or a file, in text or dot graph format. Also, choice points with no impact on the derivation can be removed from the printed derivation (experimental). - Default changes Backjumping is used by default, Mixed literals are used by default. Implementation: - Admissible Admissible remainders with mixed literals were not always computed in the most general form due to a relict of the earlier implementation of parameter- or variable-free admissible remainders. Fixed. - Heavy Source Cleanup effecting most modules. Backtracking is handled more cleanly and solely within module state, instead of in state as well as darwin. - Classes: Classes are used for the first time in some new modules (flags, bound, log), also transformed module term_indexing to a class. This eases replacing one term indexing module with another. - Delayed computation of Split candidates Split candidates are only computed when no more Assert candidates are applicable, that is for problems solvable by means of Assert only no Split candidates are computed at all. - Inactive Candidates There is no seperation between active and inactive candidates anymore. Basically, the active candidates have been dropped as a complication which didn't gain much in performance. - Performance: Some minor performance optimizations (~5-10%), mostly by instantiating some heavily parameterized core routines (unification, context unifier computation) as modules. Version 1.0 - 09/22/2004 ======================== CVS tag: master_thesis Version used for the evaluation in the master's thesis of Alexander Fuchs. Features: - Mixed context literals can be enabled with -umx Bug fixes: - Dynamic Backtracking was unsound: Backtracking didn't remove _all_ right splits, right splits not involved in closing unifiers were kept. Version CASC-J2 - 06/10/2004 ============================ CVS tag: CASC-J2 Participated in the CASC-J2 competition. Notable changes (based on the ESFOR-04 evaluation): Features: - NO SOLUTION is printed if darwin terminates without solving the problem. this might happen if there are too many - inactive candidates (> 4 000 000 on a 32 Bit processor) - variables created on the fly (e.g. when making context unifiers admissible) - skolem constants generated In practice this doesn't happen anymore for any currently tested problem. - derivations can be output as graphs in the graphviz dot format, see option -pdf - dynamic backtracking is now used by default instead of backjumping - interactive.py in the main directory starts darwin in an interactive ocaml top level environment. darwin's interactive capabilities are fairly restricted, though, this is currently only useful for development/debugging. Implementation: - the term database (and binding database in Problem_literals) is managed by weak pointers instead of reference counting. this is slightly slower but significantly less intrusive to code outside of the term module and much more fun to use. - added (non-perfect) discrimination trees implemented by John Wheeler - auto selection of the context indexing technique: discrimination trees for Horn problems, substitution trees for non-Horn problems. - inactive candidates are managed in a heap instead of a fifo, thus the best and not the oldest inactive candidate is activated, but more memory is needed as the comparison attributes must be kept. - lookahead of conflicting mandatory candidate literals, i.e. Assert and Unit Split candidates. it there are two contradictory candidates (one of which must be active) one is immediately selected bypassing the heuristic, causing the computation of a closing context unifier in the next phase. - optimization of a core function (Subst.get) leading to performance gains of about 10%. - minor optimization for substitution tree requests (the queries are now tail-recursive) - compacted literals are removed from the context term index, previously they were only excluded from the computation of context unifiers. Bug fixes: - backtracking dependencies between states were incomplete. (Split decisions were treated as dependency free as in propositional logic) Version ESFOR-04 - 04/27/2004 ============================= CVS tag: ESFOR-04 The first fixed stable version of Darwin. Used for the TPTP Evaluation as published in the Darwin paper submitted for the ESFOR workshop at the IJCAR 2004: http://www.cs.miami.edu/~tptp/Workshops/ESFOR/ See the paper for a detailed description of the implementation features.