Next: Version 2.4 (April 1996)
Up: Release Notes
Previous: Release Notes
Contents
- We admit general clauses with general first-order formulas
as literals and integrate a kind of lazy CNF transformation into saturation.
- AC-superposition is now fully implemented.
However, the AC-unification and matching module is a rather slow
prototype.
The AC-LPO is available as the default ordering in the presence of
AC-symbols. Constraint solving happens by means of a generic solver
for ordering constraints which is necessarily incomplete.
- Saturate can also read input files in DFG notation.
Harald Ganzinger
2002-12-04
Imprint | Data Protection