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.